Merge pull request #2753 from antlechner/antonia/jar-file-loading

Do not load whole jar file when --function is given

Author: antlechner

jbmc/regression/jbmc/classpath-jar-entry-method/IrrelevantClass.java

@@ -0,0 +1,7 @@
+public class IrrelevantClass {
+
+    public static void notImportant() {
+        assert true;
+    }
+
+}

jbmc/regression/jbmc/classpath-jar-entry-method/RelatedClass.java

@@ -0,0 +1,5 @@
+public class RelatedClass {
+
+    public int i;
+
+}

jbmc/regression/jbmc/classpath-jar-entry-method/RelevantClass.java

@@ -0,0 +1,7 @@
+public class RelevantClass {
+
+    public static void entry(RelatedClass rc) {
+        assert false;
+    }
+
+}

jbmc/regression/jbmc/classpath-jar-entry-method/jar_file.jar

@@ -0,0 +1,15 @@
+CORE
+jar_file.jar
+--function RelevantClass.entry --verbosity 10
+^EXIT=10
+^SIGNAL=0
+VERIFICATION FAILED
+Getting class `RelevantClass' from JAR jar_file.jar
+Getting class `RelatedClass' from JAR jar_file.jar
+--
+Getting class `IrrelevantClass' from JAR jar_file.jar
+--
+This test checks that when JBMC is given a jar file as an argument and an entry
+method is specified with --function, only classes that are (possibly
+transitively) referenced from the class containing the entry method are loaded
+by java_class_loadert.

jbmc/regression/jbmc/classpath-jar-entry-method/test.desc

@@ -733,7 +733,12 @@ void janalyzer_parse_optionst::help()
     "Usage:                       Purpose:\n"
     "\n"
     " janalyzer [-?] [-h] [--help] show help\n"
-    " janalyzer class              name of class to be checked\n"
+    " janalyzer class              name of class or JAR file to be checked\n"
+    "                              In the case of a JAR file, if a main class can be\n" // NOLINT(*)
+    "                              inferred from --main-class, --function, or the JAR\n" // NOLINT(*)
+    "                              manifest (checked in this order), the behavior is\n" // NOLINT(*)
+    "                              the same as running janalyzer on the corresponding\n" // NOLINT(*)
+    "                              class file."
     "\n"
     "Task options:\n"
     " --show                       display the abstract domains\n"

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -168,6 +168,15 @@ bool java_bytecode_languaget::preprocess(
   return true;
 }
 
+/// We set the main class (i.e.\ class to start the class loading analysis from,
+/// see \ref java_class_loadert) depending on the file type of `path`.
+/// `path` can be the name of either a .class file or a .jar file.
+/// If it is a .class file, the top-level class in this file is the main class.
+/// If it is a .jar file, we first check for the main class in three steps
+/// 1) the argument of the --main-class command-line option,
+/// 2) the class implied by the argument of the --function option,
+/// 3) the manifest file of the JAR.
+/// If no main class was found, all classes in the JAR file are loaded.
 bool java_bytecode_languaget::parse(
   std::istream &,
   const std::string &path)
@@ -207,12 +216,22 @@ bool java_bytecode_languaget::parse(
       java_cp_include_files);
     if(config.java.main_class.empty())
     {
-      auto manifest = java_class_loader.jar_pool(path).get_manifest();
-      std::string manifest_main_class=manifest["Main-Class"];
+      const std::string &entry_method = config.main;
+      // If we have an entry method, we can derive a main class.
+      if(!entry_method.empty())
+      {
+        const auto last_dot_position = entry_method.find_last_of('.');
+        main_class = entry_method.substr(0, last_dot_position);
+      }
+      else
+      {
+        auto manifest = java_class_loader.jar_pool(path).get_manifest();
+        std::string manifest_main_class = manifest["Main-Class"];
 
-      // if the manifest declares a Main-Class line, we got a main class
-      if(manifest_main_class!="")
-        main_class=manifest_main_class;
+        // if the manifest declares a Main-Class line, we got a main class
+        if(!manifest_main_class.empty())
+          main_class = manifest_main_class;
+      }
     }
     else
       main_class=config.java.main_class;

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -1018,7 +1018,12 @@ void jbmc_parse_optionst::help()
     "Usage:                       Purpose:\n"
     "\n"
     " jbmc [-?] [-h] [--help]      show help\n"
-    " jbmc class                   name of class to be checked\n"
+    " jbmc class                   name of class or JAR file to be checked\n"
+    "                              In the case of a JAR file, if a main class can be\n" // NOLINT(*)
+    "                              inferred from --main-class, --function, or the JAR\n" // NOLINT(*)
+    "                              manifest (checked in this order), the behavior is\n" // NOLINT(*)
+    "                              the same as running jbmc on the corresponding\n" // NOLINT(*)
+    "                              class file."
     "\n"
     "Analysis options:\n"
     HELP_SHOW_PROPERTIES