Allow incorrect paths for jar files in the classpath without crashing

Author: NathanJPhillips

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

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 Test.class
 --classpath ./NotHere.jar
 ^EXIT=6$

src/java_bytecode/java_class_loader.cpp

@@ -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_class_loader.h

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