replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

removed jar_indext types and data structures

This commit is contained in:
Daniel Kroening 2018-08-23 14:49:08 +01:00
parent 27d0ae0565
commit 8d2a748f97
2 changed files with 44 additions and 53 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

71
jbmc/src/java_bytecode/java_class_loader.cpp
View File

@ -88,17 +88,16 @@ void java_class_loadert::add_classpath_entry(const std::string &path)
/// \return optional value of parse tree, empty if class cannot be loaded
optionalt<java_bytecode_parse_treet> java_class_loadert::get_class_from_jar(
const irep_idt &class_name,
const std::string &jar_file,
const jar_indext &jar_index)
const std::string &jar_file)
{
auto jar_index_it = jar_index.find(class_name);
if(jar_index_it == jar_index.end())
auto classes = read_jar_file(jar_file);
if(!classes.has_value())
return {};
debug()
<< "Getting class `" << class_name << "' from JAR " << jar_file << eom;
auto data = jar_pool(jar_file).get_entry(jar_index_it->second);
auto data = jar_pool(jar_file).get_entry(class_name_to_jar_file(class_name));
if(!data.has_value())
return {};
@ -137,7 +136,7 @@ java_class_loadert::get_parse_tree(
PRECONDITION(parse_trees.empty());
// do we refuse to load?
if(!class_loader_limit.load_class_file(class_name_to_file(class_name)))
if(!class_loader_limit.load_class_file(class_name_to_jar_file(class_name)))
{
debug() << "not loading " << class_name << " because of limit" << eom;
java_bytecode_parse_treet parse_tree;
@ -153,11 +152,8 @@ java_class_loadert::get_parse_tree(
{
case classpath_entryt::JAR:
{
jar_index_optcreft index = read_jar_file(cp_entry.path);
if(!index)
continue;
optionalt<java_bytecode_parse_treet> parse_tree =
get_class_from_jar(class_name, cp_entry.path, *index);
get_class_from_jar(class_name, cp_entry.path);
if(parse_tree)
parse_trees.emplace_back(std::move(*parse_tree));
}
@ -166,7 +162,7 @@ java_class_loadert::get_parse_tree(
case classpath_entryt::DIRECTORY:
{
// Look in the given directory
const std::string class_file = class_name_to_file(class_name);
const std::string class_file = class_name_to_os_file(class_name);
const std::string full_path =
#ifdef _WIN32
cp_entry.path + '\\' + class_file;
@ -243,33 +239,24 @@ java_class_loadert::get_parse_tree(
std::vector<irep_idt> java_class_loadert::load_entire_jar(
const std::string &jar_path)
{
jar_index_optcreft jar_index = read_jar_file(jar_path);
if(!jar_index)
auto classes = read_jar_file(jar_path);
if(!classes.has_value())
return {};
classpath_entries.push_front(
classpath_entryt(classpath_entryt::JAR, jar_path));
std::vector<irep_idt> classes;
for(const auto &e : jar_index->get())
{
operator()(e.first);
classes.push_back(e.first);
}
for(const auto &c : *classes)
operator()(c);
classpath_entries.pop_front();
return classes;
return *classes;
}
java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file(
const std::string &jar_path)
optionalt<std::vector<irep_idt>>
java_class_loadert::read_jar_file(const std::string &jar_path)
{
auto existing_it = jars_by_path.find(jar_path);
if(existing_it != jars_by_path.end())
return std::cref(existing_it->second);
std::vector<std::string> filenames;
try
{
@ -278,13 +265,13 @@ java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file(
catch(const std::runtime_error &)
{
error() << "failed to open JAR file `" << jar_path << "'" << eom;
return jar_index_optcreft();
return {};
}
debug() << "Adding JAR file `" << jar_path << "'" << eom;
// Create a new entry in the map and initialize using the list of file names
// that are in jar_filet
jar_indext &jar_index = jars_by_path[jar_path];
std::vector<irep_idt> classes;
for(auto &file_name : filenames)
{
if(has_suffix(file_name, ".class"))
@ -293,10 +280,10 @@ java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file(
<< "Found class file " << file_name << " in JAR `" << jar_path << "'"
<< eom;
irep_idt class_name=file_to_class_name(file_name);
jar_index[class_name] = file_name;
classes.push_back(class_name);
}
}
return std::cref(jar_index);
return classes;
}
/// Convert a file name to the class name. Java interprets folders as packages,
@ -336,7 +323,27 @@ std::string java_class_loadert::file_to_class_name(const std::string &file)
/// file_to_class_name.
/// \param class_name: the name of the class
/// \return the class name converted to file name
std::string java_class_loadert::class_name_to_file(const irep_idt &class_name)
std::string
java_class_loadert::class_name_to_jar_file(const irep_idt &class_name)
{
std::string result = id2string(class_name);
// dots (package name separators) to slash
for(std::string::iterator it = result.begin(); it != result.end(); it++)
if(*it == '.')
*it = '/';
// add .class suffix
result += ".class";
return result;
}
/// Convert a class name to a file name, with OS-dependent syntax
/// \param class_name: the name of the class
/// \return the class name converted to file name
std::string
java_class_loadert::class_name_to_os_file(const irep_idt &class_name)
{
std::string result=id2string(class_name);

26
jbmc/src/java_bytecode/java_class_loader.h
View File

@ -27,10 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com
class java_class_loadert:public messaget
{
public:
/// A map associating logical class names with the name of the .class file
/// implementing it for all classes inside a single JAR file
typedef std::map<irep_idt, std::string> jar_indext;
/// A list of parse trees supporting overlay classes
typedef std::list<java_bytecode_parse_treet> parse_tree_with_overlayst;
/// A map from class names to list of parse tree where multiple entries can
@ -95,14 +91,11 @@ public:
void add_classpath_entry(const std::string &);
static std::string file_to_class_name(const std::string &);
static std::string class_name_to_file(const irep_idt &);
static std::string class_name_to_os_file(const irep_idt &);
static std::string class_name_to_jar_file(const irep_idt &);
std::vector<irep_idt> load_entire_jar(const std::string &jar_path);
const jar_indext &get_jar_index(const std::string &jar_path)
{
return jars_by_path.at(jar_path);
}
/// Map from class names to the bytecode parse trees
fixed_keys_map_wrappert<parse_tree_with_overridest_mapt>
get_class_with_overlays_map()
@ -146,22 +139,13 @@ private:
std::vector<irep_idt> java_load_classes;
get_extra_class_refs_functiont get_extra_class_refs;
/// The jar_indext for each jar file we've read
std::map<std::string, jar_indext> jars_by_path;
/// Map from class names to the bytecode parse trees
parse_tree_with_overridest_mapt class_map;
typedef optionalt<std::reference_wrapper<const jar_indext>>
jar_index_optcreft;
optionalt<std::vector<irep_idt>> read_jar_file(const std::string &jar_path);
jar_index_optcreft read_jar_file(
const std::string &jar_path);
optionalt<java_bytecode_parse_treet> get_class_from_jar(
const irep_idt &class_name,
const std::string &jar_file,
const jar_indext &jar_index);
optionalt<java_bytecode_parse_treet>
get_class_from_jar(const irep_idt &class_name, const std::string &jar_file);
};
#endif // CPROVER_JAVA_BYTECODE_JAVA_CLASS_LOADER_H