diff --git a/regression/cbmc-java/invalid_classpath/Test.class b/regression/cbmc-java/invalid_classpath/Test.class new file mode 100644 index 00000000000..aaa01c760f2 Binary files /dev/null and b/regression/cbmc-java/invalid_classpath/Test.class differ diff --git a/regression/cbmc-java/invalid_classpath/Test.java b/regression/cbmc-java/invalid_classpath/Test.java new file mode 100644 index 00000000000..e3957a5157d --- /dev/null +++ b/regression/cbmc-java/invalid_classpath/Test.java @@ -0,0 +1,3 @@ +public class Test { + public void main() {} +} diff --git a/regression/cbmc-java/invalid_classpath/test-jar.desc b/regression/cbmc-java/invalid_classpath/test-jar.desc new file mode 100644 index 00000000000..ad020054856 --- /dev/null +++ b/regression/cbmc-java/invalid_classpath/test-jar.desc @@ -0,0 +1,10 @@ +CORE symex-driven-lazy-loading-expected-failure +Test.class +--classpath ./NotHere.jar +^EXIT=6$ +^SIGNAL=0$ +^the program has no entry point$ +^failed to load class `Test'$ +-- +-- +symex-driven lazy loading should emit "the program has no entry point" but currently doesn't diff --git a/regression/cbmc-java/invalid_classpath/test-path.desc b/regression/cbmc-java/invalid_classpath/test-path.desc new file mode 100644 index 00000000000..282ae0209f8 --- /dev/null +++ b/regression/cbmc-java/invalid_classpath/test-path.desc @@ -0,0 +1,10 @@ +CORE symex-driven-lazy-loading-expected-failure +Test.class +--classpath ./NotHere +^EXIT=6$ +^SIGNAL=0$ +^the program has no entry point$ +^failed to load class `Test'$ +-- +-- +symex-driven lazy loading should emit "the program has no entry point" but currently doesn't diff --git a/regression/cbmc-java/provide_object_implementation/java/lang/Object.class b/regression/cbmc-java/provide_object_implementation/java/lang/Object.class new file mode 100644 index 00000000000..868d3dbea58 Binary files /dev/null and b/regression/cbmc-java/provide_object_implementation/java/lang/Object.class differ diff --git a/regression/cbmc-java/provide_object_implementation/java/lang/Object.java b/regression/cbmc-java/provide_object_implementation/java/lang/Object.java new file mode 100644 index 00000000000..0ba3304a00c --- /dev/null +++ b/regression/cbmc-java/provide_object_implementation/java/lang/Object.java @@ -0,0 +1,33 @@ +package java.lang; + +public class Object { + public final Class getClass() { + return null; + } + + public int hashCode() { return 0; } + + public boolean equals(Object obj) { return (this == obj); } + + protected Object clone() throws CloneNotSupportedException { + throw new CloneNotSupportedException(); + } + + public String toString() { return "object"; } + + public final void notify() {} + + public final void notifyAll() {} + + public final void wait(long timeout) throws InterruptedException { + throw new InterruptedException(); + } + + public final void wait(long timeout, int nanos) throws InterruptedException { + wait(timeout); + } + + public final void wait() throws InterruptedException { wait(0); } + + protected void finalize() throws Throwable { } +} diff --git a/regression/cbmc-java/provide_object_implementation/test.desc b/regression/cbmc-java/provide_object_implementation/test.desc new file mode 100644 index 00000000000..381ae109d1e --- /dev/null +++ b/regression/cbmc-java/provide_object_implementation/test.desc @@ -0,0 +1,10 @@ +CORE symex-driven-lazy-loading-expected-failure +java/lang/Object.class + +^EXIT=6$ +^SIGNAL=0$ +^the program has no entry point$ +-- +^failed to add class symbol java::java\.lang\.Object$ +-- +symex-driven lazy loading should emit "the program has no entry point" but currently doesn't diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 996d54985ba..fe393c6fcf5 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -185,6 +185,12 @@ void java_bytecode_convert_classt::operator()( PRECONDITION(!parse_trees.empty()); const irep_idt &class_name = parse_trees.front().parsed_class.name; + if(symbol_table.has_symbol("java::" + id2string(class_name))) + { + debug() << "Skip class " << class_name << " (already loaded)" << eom; + return; + } + // Add array types to the symbol table add_array_types(symbol_table); diff --git a/src/java_bytecode/java_class_loader.cpp b/src/java_bytecode/java_class_loader.cpp index e44cf8d3052..2196b9b7bbf 100644 --- a/src/java_bytecode/java_class_loader.cpp +++ b/src/java_bytecode/java_class_loader.cpp @@ -81,9 +81,9 @@ java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()( optionalt java_class_loadert::get_class_from_jar( const irep_idt &class_name, const std::string &jar_file, + const jar_indext &jar_index, java_class_loader_limitt &class_loader_limit) { - jar_indext &jar_index = jars_by_path.at(jar_file); auto jar_index_it = jar_index.find(class_name); if(jar_index_it == jar_index.end()) return {}; @@ -112,9 +112,11 @@ java_class_loadert::get_parse_tree( // First add all given JAR files for(const auto &jar_file : jar_files) { - read_jar_file(class_loader_limit, jar_file); + jar_index_optcreft index = read_jar_file(class_loader_limit, jar_file); + if(!index) + continue; optionalt parse_tree = - get_class_from_jar(class_name, jar_file, class_loader_limit); + get_class_from_jar(class_name, jar_file, *index, class_loader_limit); if(parse_tree) parse_trees.push_back(*parse_tree); } @@ -130,12 +132,14 @@ java_class_loadert::get_parse_tree( // This does not read from the jar file but from the jar_filet object we // just created - read_jar_file(class_loader_limit, core_models); - - optionalt parse_tree = - get_class_from_jar(class_name, core_models, class_loader_limit); - if(parse_tree) - parse_trees.push_back(*parse_tree); + jar_index_optcreft index = read_jar_file(class_loader_limit, core_models); + if(index) + { + optionalt parse_tree = + get_class_from_jar(class_name, core_models, *index, class_loader_limit); + if(parse_tree) + parse_trees.push_back(*parse_tree); + } } // Then add everything on the class path @@ -143,10 +147,11 @@ java_class_loadert::get_parse_tree( { if(has_suffix(cp_entry, ".jar")) { - read_jar_file(class_loader_limit, cp_entry); - + jar_index_optcreft index = read_jar_file(class_loader_limit, cp_entry); + if(!index) + continue; optionalt parse_tree = - get_class_from_jar(class_name, cp_entry, class_loader_limit); + get_class_from_jar(class_name, cp_entry, *index, class_loader_limit); if(parse_tree) parse_trees.push_back(*parse_tree); } diff --git a/src/java_bytecode/java_class_loader.h b/src/java_bytecode/java_class_loader.h index cfc098e899c..6f46072aaa2 100644 --- a/src/java_bytecode/java_class_loader.h +++ b/src/java_bytecode/java_class_loader.h @@ -160,6 +160,7 @@ class java_class_loadert:public messaget optionalt get_class_from_jar( const irep_idt &class_name, const std::string &jar_file, + const jar_indext &jar_index, java_class_loader_limitt &class_loader_limit); };