Skip to content

factor out classpath functionality into separate class #2839

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 1 commit into from
Aug 27, 2018
Merged

factor out classpath functionality into separate class #2839

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
1 change: 1 addition & 0 deletions jbmc/src/java_bytecode/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ SRC = bytecode_info.cpp \
java_bytecode_typecheck_expr.cpp \
java_bytecode_typecheck_type.cpp \
java_class_loader.cpp \
java_class_loader_base.cpp \
java_class_loader_limit.cpp \
java_enum_static_init_unwind_handler.cpp \
java_entry_point.cpp \
Expand Down
152 changes: 3 additions & 149 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 @@ -68,44 +68,6 @@ java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()(
return class_map.at(class_name);
}

void java_class_loadert::add_classpath_entry(const std::string &path)
{
if(has_suffix(path, ".jar"))
{
classpath_entries.push_back(classpath_entryt(classpath_entryt::JAR, path));
}
else
{
classpath_entries.push_back(
classpath_entryt(classpath_entryt::DIRECTORY, path));
}
}

/// Load class from jar file.
/// \param class_name: name of class to load in Java source format
/// \param jar_file: path of the jar file
/// \param jar_index: the index of the jar file
/// \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)
{
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(class_name_to_jar_file(class_name));

if(!data.has_value())
return {};

std::istringstream istream(*data);
return java_bytecode_parse(istream, get_message_handler());
}

/// Check if class is an overlay class by searching for `ID_overlay_class` in
/// its list of annotations. TODO(nathan) give a short explanation about what
/// overlay classes are.
Expand Down Expand Up @@ -148,39 +110,9 @@ java_class_loadert::get_parse_tree(
// Rummage through the class path
for(const auto &cp_entry : classpath_entries)
{
switch(cp_entry.kind)
{
case classpath_entryt::JAR:
{
optionalt<java_bytecode_parse_treet> parse_tree =
get_class_from_jar(class_name, cp_entry.path);
if(parse_tree)
parse_trees.emplace_back(std::move(*parse_tree));
}
break;

case classpath_entryt::DIRECTORY:
{
// Look in the given directory
const std::string class_file = class_name_to_os_file(class_name);
const std::string full_path =
#ifdef _WIN32
cp_entry.path + '\\' + class_file;
#else
cp_entry.path + '/' + class_file;
#endif

if(std::ifstream(full_path))
{
debug() << "Getting class `" << class_name << "' from file "
<< full_path << eom;
optionalt<java_bytecode_parse_treet> parse_tree =
java_bytecode_parse(full_path, get_message_handler());
if(parse_tree)
parse_trees.emplace_back(std::move(*parse_tree));
}
}
}
auto parse_tree = load_class(class_name, cp_entry);
if(parse_tree.has_value())
parse_trees.emplace_back(std::move(*parse_tree));
}

auto parse_tree_it = parse_trees.begin();
Expand Down Expand Up @@ -285,81 +217,3 @@ java_class_loadert::read_jar_file(const std::string &jar_path)
}
return classes;
}

/// Convert a file name to the class name. Java interprets folders as packages,
/// therefore a prefix of `./` is removed if necessary, and all `/` are
/// converted to `.`. For example a class file `./com/diffblue/test.class` is
/// converted to the class name `com.diffblue.test`.
/// \param file: the name of the class file
/// \return the file name converted to Java class name
std::string java_class_loadert::file_to_class_name(const std::string &file)
{
std::string result=file;

// Strip .class. Note that the Java class loader would
// not do that.
if(has_suffix(result, ".class"))
result.resize(result.size()-6);

// Strip a "./" prefix. Note that the Java class loader
// would not do that.
#ifdef _WIN32
while(has_prefix(result, ".\\"))
result=std::string(result, 2, std::string::npos);
#else
while(has_prefix(result, "./"))
result=std::string(result, 2, std::string::npos);
#endif

// slash to dot
for(std::string::iterator it=result.begin(); it!=result.end(); it++)
if(*it=='/')
*it='.';

return result;
}

/// Convert a class name to a file name, does the inverse of \ref
/// 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_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);

// dots (package name separators) to slash, depending on OS
for(std::string::iterator it=result.begin(); it!=result.end(); it++)
if(*it=='.')
{
#ifdef _WIN32
*it='\\';
#else
*it='/';
#endif
}

// add .class suffix
result+=".class";

return result;
}
43 changes: 2 additions & 41 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 @@ -14,17 +14,16 @@ Author: Daniel Kroening, [email protected]
#include <regex>
#include <set>

#include <util/message.h>
#include <util/fixed_keys_map_wrapper.h>

#include "jar_file.h"
#include "jar_pool.h"
#include "java_bytecode_parse_tree.h"
#include "java_class_loader_base.h"
#include "java_class_loader_limit.h"

/// Class responsible to load .class files. Either directly from a specific
/// file, from a classpath specification or from a Java archive (JAR) file.
class java_class_loadert:public messaget
class java_class_loadert : public java_class_loader_baset
{
public:
/// A list of parse trees supporting overlay classes
Expand Down Expand Up @@ -78,22 +77,6 @@ class java_class_loadert:public messaget
java_load_classes.push_back(id);
}

/// Clear all classpath entries
void clear_classpath()
{
classpath_entries.clear();
}

/// Appends an entry to the class path, used for loading classes. The
/// argument may be
/// 1) The name of a directory, used for searching for .class files
/// 2) The name of a JAR file
void add_classpath_entry(const std::string &);

static std::string file_to_class_name(const std::string &);
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);

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

/// a cache for jar_filet, by path name
jar_poolt jar_pool;

private:
/// Either a regular expression matching files that will be allowed to be
/// loaded or a string of the form `@PATH` where PATH is the file path of a
Expand All @@ -119,22 +99,6 @@ class java_class_loadert:public messaget
/// information.
std::string java_cp_include_files;

/// An entry in the classpath
struct classpath_entryt
{
using kindt = enum { JAR, DIRECTORY };
kindt kind;
std::string path;

classpath_entryt(kindt _kind, const std::string &_path)
: kind(_kind), path(_path)
{
}
};

/// List of entries in the classpath
std::list<classpath_entryt> classpath_entries;

/// Classes to be explicitly loaded
std::vector<irep_idt> java_load_classes;
get_extra_class_refs_functiont get_extra_class_refs;
Expand All @@ -143,9 +107,6 @@ class java_class_loadert:public messaget
parse_tree_with_overridest_mapt class_map;

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);
};

#endif // CPROVER_JAVA_BYTECODE_JAVA_CLASS_LOADER_H
Loading