Skip to content

jar_index cleanout #2766

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 2 commits into from
Aug 24, 2018
Merged

jar_index cleanout #2766

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
27d0ae0
java_class_loadert::load_entire_jar now returns the classes loaded
Aug 20, 2018
8d2a748
removed jar_indext types and data structures
Aug 23, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions jbmc/src/java_bytecode/java_bytecode_language.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -235,9 +235,9 @@ bool java_bytecode_languaget::parse(
if(main_class.empty())
{
status() << "JAR file without entry point: loading class files" << eom;
java_class_loader.load_entire_jar(path);
for(const auto &kv : java_class_loader.get_jar_index(path))
main_jar_classes.push_back(kv.first);
const auto classes = java_class_loader.load_entire_jar(path);
for(const auto &c : classes)
main_jar_classes.push_back(c);
}
else
java_class_loader.add_classpath_entry(path);
Expand Down
73 changes: 43 additions & 30 deletions jbmc/src/java_bytecode/java_class_loader.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {};
Expand Down Expand Up @@ -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;
Expand All @@ -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));
}
Expand All @@ -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;
Expand Down Expand Up @@ -238,32 +234,29 @@ java_class_loadert::get_parse_tree(
return parse_trees;
}

/// Load all class files from a .jar file, and store name of .jar in
/// `classpath_entreies`.
/// Load all class files from a .jar file
/// \param jar_path: the path for the .jar to load
void java_class_loadert::load_entire_jar(
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)
return;
auto classes = read_jar_file(jar_path);
if(!classes.has_value())
return {};

classpath_entries.push_front(
classpath_entryt(classpath_entryt::JAR, jar_path));

for(const auto &e : jar_index->get())
operator()(e.first);
for(const auto &c : *classes)
operator()(c);

classpath_entries.pop_front();

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
{
Expand All @@ -272,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"))
Expand All @@ -287,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,
Expand Down Expand Up @@ -330,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);

Expand Down
28 changes: 6 additions & 22 deletions jbmc/src/java_bytecode/java_class_loader.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,10 +27,6 @@ Author: Daniel Kroening, [email protected]
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
Expand Down Expand Up @@ -95,14 +91,11 @@ class java_class_loadert:public messaget
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 &);

void load_entire_jar(const std::string &jar_path);
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()
Expand Down Expand Up @@ -146,22 +139,13 @@ class java_class_loadert:public messaget
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;

jar_index_optcreft read_jar_file(
const std::string &jar_path);
optionalt<std::vector<irep_idt>> 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