Merge pull request #1982 from NathanJPhillips/bugfix/load-object-once

Fixes related to #1816

Author: Thomas Kiley

regression/cbmc-java/invalid_classpath/Test.class

@@ -0,0 +1,3 @@
+public class Test {
+    public void main() {}
+}

regression/cbmc-java/invalid_classpath/Test.java

@@ -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

regression/cbmc-java/invalid_classpath/test-jar.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

regression/cbmc-java/invalid_classpath/test-path.desc

@@ -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 { }
+}

regression/cbmc-java/provide_object_implementation/java/lang/Object.class

@@ -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

regression/cbmc-java/provide_object_implementation/java/lang/Object.java

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

regression/cbmc-java/provide_object_implementation/test.desc

@@ -81,9 +81,9 @@ java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()(
 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,
   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<java_bytecode_parse_treet> 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,23 +132,26 @@ 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<java_bytecode_parse_treet> 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<java_bytecode_parse_treet> 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
   for(const auto &cp_entry : config.java.classpath)
   {
     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<java_bytecode_parse_treet> 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);
     }

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -160,6 +160,7 @@ class java_class_loadert:public messaget
   optionalt<java_bytecode_parse_treet> 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);
 };