Skip to content

Commit d33bd22

Browse files
kroeningkroening
authored
Merge pull request diffblue#2839 from diffblue/java_class_loader_base
factor out classpath functionality into separate class
2 parents f8ef8dc + 0a53059 commit d33bd22

File tree

5 files changed

+254
-190
lines changed

5 files changed

+254
-190
lines changed

‎jbmc/src/java_bytecode/Makefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -20,6 +20,7 @@ SRC = bytecode_info.cpp \
2020
java_bytecode_typecheck_expr.cpp \
2121
java_bytecode_typecheck_type.cpp \
2222
java_class_loader.cpp \
23+
java_class_loader_base.cpp \
2324
java_class_loader_limit.cpp \
2425
java_enum_static_init_unwind_handler.cpp \
2526
java_entry_point.cpp \

‎jbmc/src/java_bytecode/java_class_loader.cpp‎

Lines changed: 3 additions & 149 deletions
Original file line numberDiff line numberDiff line change
@@ -68,44 +68,6 @@ java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()(
6868
return class_map.at(class_name);
6969
}
7070

71-
void java_class_loadert::add_classpath_entry(const std::string &path)
72-
{
73-
if(has_suffix(path, ".jar"))
74-
{
75-
classpath_entries.push_back(classpath_entryt(classpath_entryt::JAR, path));
76-
}
77-
else
78-
{
79-
classpath_entries.push_back(
80-
classpath_entryt(classpath_entryt::DIRECTORY, path));
81-
}
82-
}
83-
84-
/// Load class from jar file.
85-
/// \param class_name: name of class to load in Java source format
86-
/// \param jar_file: path of the jar file
87-
/// \param jar_index: the index of the jar file
88-
/// \return optional value of parse tree, empty if class cannot be loaded
89-
optionalt<java_bytecode_parse_treet> java_class_loadert::get_class_from_jar(
90-
const irep_idt &class_name,
91-
const std::string &jar_file)
92-
{
93-
auto classes = read_jar_file(jar_file);
94-
if(!classes.has_value())
95-
return {};
96-
97-
debug()
98-
<< "Getting class `" << class_name << "' from JAR " << jar_file << eom;
99-
100-
auto data = jar_pool(jar_file).get_entry(class_name_to_jar_file(class_name));
101-
102-
if(!data.has_value())
103-
return {};
104-
105-
std::istringstream istream(*data);
106-
return java_bytecode_parse(istream, get_message_handler());
107-
}
108-
10971
/// Check if class is an overlay class by searching for `ID_overlay_class` in
11072
/// its list of annotations. TODO(nathan) give a short explanation about what
11173
/// overlay classes are.
@@ -148,39 +110,9 @@ java_class_loadert::get_parse_tree(
148110
// Rummage through the class path
149111
for(const auto &cp_entry : classpath_entries)
150112
{
151-
switch(cp_entry.kind)
152-
{
153-
case classpath_entryt::JAR:
154-
{
155-
optionalt<java_bytecode_parse_treet> parse_tree =
156-
get_class_from_jar(class_name, cp_entry.path);
157-
if(parse_tree)
158-
parse_trees.emplace_back(std::move(*parse_tree));
159-
}
160-
break;
161-
162-
case classpath_entryt::DIRECTORY:
163-
{
164-
// Look in the given directory
165-
const std::string class_file = class_name_to_os_file(class_name);
166-
const std::string full_path =
167-
#ifdef _WIN32
168-
cp_entry.path + '\\' + class_file;
169-
#else
170-
cp_entry.path + '/' + class_file;
171-
#endif
172-
173-
if(std::ifstream(full_path))
174-
{
175-
debug() << "Getting class `" << class_name << "' from file "
176-
<< full_path << eom;
177-
optionalt<java_bytecode_parse_treet> parse_tree =
178-
java_bytecode_parse(full_path, get_message_handler());
179-
if(parse_tree)
180-
parse_trees.emplace_back(std::move(*parse_tree));
181-
}
182-
}
183-
}
113+
auto parse_tree = load_class(class_name, cp_entry);
114+
if(parse_tree.has_value())
115+
parse_trees.emplace_back(std::move(*parse_tree));
184116
}
185117

186118
auto parse_tree_it = parse_trees.begin();
@@ -285,81 +217,3 @@ java_class_loadert::read_jar_file(const std::string &jar_path)
285217
}
286218
return classes;
287219
}
288-
289-
/// Convert a file name to the class name. Java interprets folders as packages,
290-
/// therefore a prefix of `./` is removed if necessary, and all `/` are
291-
/// converted to `.`. For example a class file `./com/diffblue/test.class` is
292-
/// converted to the class name `com.diffblue.test`.
293-
/// \param file: the name of the class file
294-
/// \return the file name converted to Java class name
295-
std::string java_class_loadert::file_to_class_name(const std::string &file)
296-
{
297-
std::string result=file;
298-
299-
// Strip .class. Note that the Java class loader would
300-
// not do that.
301-
if(has_suffix(result, ".class"))
302-
result.resize(result.size()-6);
303-
304-
// Strip a "./" prefix. Note that the Java class loader
305-
// would not do that.
306-
#ifdef _WIN32
307-
while(has_prefix(result, ".\\"))
308-
result=std::string(result, 2, std::string::npos);
309-
#else
310-
while(has_prefix(result, "./"))
311-
result=std::string(result, 2, std::string::npos);
312-
#endif
313-
314-
// slash to dot
315-
for(std::string::iterator it=result.begin(); it!=result.end(); it++)
316-
if(*it=='/')
317-
*it='.';
318-
319-
return result;
320-
}
321-
322-
/// Convert a class name to a file name, does the inverse of \ref
323-
/// file_to_class_name.
324-
/// \param class_name: the name of the class
325-
/// \return the class name converted to file name
326-
std::string
327-
java_class_loadert::class_name_to_jar_file(const irep_idt &class_name)
328-
{
329-
std::string result = id2string(class_name);
330-
331-
// dots (package name separators) to slash
332-
for(std::string::iterator it = result.begin(); it != result.end(); it++)
333-
if(*it == '.')
334-
*it = '/';
335-
336-
// add .class suffix
337-
result += ".class";
338-
339-
return result;
340-
}
341-
342-
/// Convert a class name to a file name, with OS-dependent syntax
343-
/// \param class_name: the name of the class
344-
/// \return the class name converted to file name
345-
std::string
346-
java_class_loadert::class_name_to_os_file(const irep_idt &class_name)
347-
{
348-
std::string result=id2string(class_name);
349-
350-
// dots (package name separators) to slash, depending on OS
351-
for(std::string::iterator it=result.begin(); it!=result.end(); it++)
352-
if(*it=='.')
353-
{
354-
#ifdef _WIN32
355-
*it='\\';
356-
#else
357-
*it='/';
358-
#endif
359-
}
360-
361-
// add .class suffix
362-
result+=".class";
363-
364-
return result;
365-
}

‎jbmc/src/java_bytecode/java_class_loader.h‎

Lines changed: 2 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -14,17 +14,16 @@ Author: Daniel Kroening, [email protected]
1414
#include <regex>
1515
#include <set>
1616

17-
#include <util/message.h>
1817
#include <util/fixed_keys_map_wrapper.h>
1918

2019
#include "jar_file.h"
21-
#include "jar_pool.h"
2220
#include "java_bytecode_parse_tree.h"
21+
#include "java_class_loader_base.h"
2322
#include "java_class_loader_limit.h"
2423

2524
/// Class responsible to load .class files. Either directly from a specific
2625
/// file, from a classpath specification or from a Java archive (JAR) file.
27-
class java_class_loadert:public messaget
26+
class java_class_loadert : public java_class_loader_baset
2827
{
2928
public:
3029
/// A list of parse trees supporting overlay classes
@@ -78,22 +77,6 @@ class java_class_loadert:public messaget
7877
java_load_classes.push_back(id);
7978
}
8079

81-
/// Clear all classpath entries
82-
void clear_classpath()
83-
{
84-
classpath_entries.clear();
85-
}
86-
87-
/// Appends an entry to the class path, used for loading classes. The
88-
/// argument may be
89-
/// 1) The name of a directory, used for searching for .class files
90-
/// 2) The name of a JAR file
91-
void add_classpath_entry(const std::string &);
92-
93-
static std::string file_to_class_name(const std::string &);
94-
static std::string class_name_to_os_file(const irep_idt &);
95-
static std::string class_name_to_jar_file(const irep_idt &);
96-
9780
std::vector<irep_idt> load_entire_jar(const std::string &jar_path);
9881

9982
/// Map from class names to the bytecode parse trees
@@ -108,9 +91,6 @@ class java_class_loadert:public messaget
10891
return class_map.at(class_name).front();
10992
}
11093

111-
/// a cache for jar_filet, by path name
112-
jar_poolt jar_pool;
113-
11494
private:
11595
/// Either a regular expression matching files that will be allowed to be
11696
/// loaded or a string of the form `@PATH` where PATH is the file path of a
@@ -119,22 +99,6 @@ class java_class_loadert:public messaget
11999
/// information.
120100
std::string java_cp_include_files;
121101

122-
/// An entry in the classpath
123-
struct classpath_entryt
124-
{
125-
using kindt = enum { JAR, DIRECTORY };
126-
kindt kind;
127-
std::string path;
128-
129-
classpath_entryt(kindt _kind, const std::string &_path)
130-
: kind(_kind), path(_path)
131-
{
132-
}
133-
};
134-
135-
/// List of entries in the classpath
136-
std::list<classpath_entryt> classpath_entries;
137-
138102
/// Classes to be explicitly loaded
139103
std::vector<irep_idt> java_load_classes;
140104
get_extra_class_refs_functiont get_extra_class_refs;
@@ -143,9 +107,6 @@ class java_class_loadert:public messaget
143107
parse_tree_with_overridest_mapt class_map;
144108

145109
optionalt<std::vector<irep_idt>> read_jar_file(const std::string &jar_path);
146-
147-
optionalt<java_bytecode_parse_treet>
148-
get_class_from_jar(const irep_idt &class_name, const std::string &jar_file);
149110
};
150111

151112
#endif // CPROVER_JAVA_BYTECODE_JAVA_CLASS_LOADER_H

0 commit comments

Comments
 (0)