[TG-9219] Add new option --ignore-manifest-main-class

jbmc/regression/jbmc/classpath-jar-load-whole-jar/pom.xml

@@ -0,0 +1,32 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+  <modelVersion>4.0.0</modelVersion>
+  <groupId>org.cprover.regression</groupId>
+  <artifactId>regression</artifactId>
+  <version>1.0-SNAPSHOT</version>
+
+  <build>
+    <finalName>jar-file</finalName>
+    <plugins>
+      <plugin>
+        <groupId>org.apache.maven.plugins</groupId>
+        <artifactId>maven-jar-plugin</artifactId>
+        <configuration>
+          <archive>
+            <manifest>
+              <mainClass>org.cprover.first.RelevantClass</mainClass>
+            </manifest>
+          </archive>
+        </configuration>
+      </plugin>
+    </plugins>
+  </build>
+
+  <properties>
+   <maven.compiler.source>1.8</maven.compiler.source>
+   <maven.compiler.target>1.8</maven.compiler.target>
+  </properties>
+
+</project>

jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/first/IrrelevantClass.java

@@ -0,0 +1,6 @@
+package org.cprover.first;
+
+public class IrrelevantClass {
+
+  public static void notImportant() { assert true; }
+}

jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/first/RelatedClass.java

@@ -0,0 +1,3 @@
+package org.cprover.first;
+
+public class RelatedClass { public int i; }

jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/first/RelevantClass.java

@@ -0,0 +1,10 @@
+package org.cprover.first;
+
+import org.cprover.second.RelatedClassOtherPkg;
+
+public class RelevantClass {
+
+  public static void entry(RelatedClass rc, RelatedClassOtherPkg rcop) {
+    assert false;
+  }
+}

jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/second/IrrelevantClassOtherPkg.java

@@ -0,0 +1,6 @@
+package org.cprover.second;
+
+public class IrrelevantClassOtherPkg {
+
+  public static void notImportant() { assert true; }
+}

jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/second/RelatedClassOtherPkg.java

@@ -0,0 +1,3 @@
+package org.cprover.second;
+
+public class RelatedClassOtherPkg { public int i; }

jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-default.desc

@@ -0,0 +1,16 @@
+CORE
+target/jar-file.jar
+--verbosity 10
+^EXIT=6$
+^SIGNAL=0$
+Getting class 'org\.cprover\.first\.RelevantClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.first\.RelatedClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.second\.RelatedClassOtherPkg' from JAR target\/jar-file.jar
+no entry point
+--
+Getting class 'org\.cprover\.first\.IrrelevantClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.second\.IrrelevantClassOtherPkg' from JAR target\/jar-file.jar
+--
+This test checks that without the --ignore-manifest-main-class method, we only
+load those classes that are referenced by the main class specified in the
+manifest file of a jar file.

jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-ignore-and-function-other.desc

@@ -0,0 +1,18 @@
+CORE
+target/jar-file.jar
+--verbosity 10 --ignore-manifest-main-class --function 'org.cprover.second.IrrelevantClassOtherPkg.<init>'
+^EXIT=0$
+^SIGNAL=0$
+Getting class 'org\.cprover\.second\.IrrelevantClassOtherPkg' from JAR target\/jar-file.jar
+--
+Getting class 'org\.cprover\.first\.RelevantClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.first\.RelatedClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.second\.RelatedClassOtherPkg' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.first\.IrrelevantClass' from JAR target\/jar-file.jar
+--
+This test checks that when both --ignore-manifest-main-class and --function are
+specified, we use the declaring class of the argument of --function as the main
+class from where to start loading other classes.
+The difference from the similar test test-ignore-and-function.desc is that in
+this case, the main class specified by --function is different from the main
+class specified in the JAR manifest file.

jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-ignore-and-function.desc

@@ -0,0 +1,15 @@
+CORE
+target/jar-file.jar
+--verbosity 10 --ignore-manifest-main-class --function org.cprover.first.RelevantClass.entry
+^EXIT=10$
+^SIGNAL=0$
+Getting class 'org\.cprover\.first\.RelevantClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.first\.RelatedClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.second\.RelatedClassOtherPkg' from JAR target\/jar-file.jar
+--
+Getting class 'org\.cprover\.first\.IrrelevantClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.second\.IrrelevantClassOtherPkg' from JAR target\/jar-file.jar
+--
+This test checks that when both --ignore-manifest-main-class and --function are
+specified, we use the declaring class of the argument of --function as the main
+class from where to start loading other classes.

jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-ignore-and-main-class.desc

@@ -0,0 +1,16 @@
+CORE
+target/jar-file.jar
+--verbosity 10 --ignore-manifest-main-class --main-class org.cprover.first.RelevantClass
+^EXIT=6$
+^SIGNAL=0$
+Getting class 'org\.cprover\.first\.RelevantClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.first\.RelatedClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.second\.RelatedClassOtherPkg' from JAR target\/jar-file.jar
+no entry point
+--
+Getting class 'org\.cprover\.first\.IrrelevantClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.second\.IrrelevantClassOtherPkg' from JAR target\/jar-file.jar
+--
+This test checks that when both --ignore-manifest-main-class and --main-class
+are specified, we use the argument of --main-class as the main class from where
+to start loading other classes.

jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-ignore-function-and-main-class.desc

@@ -0,0 +1,16 @@
+CORE
+target/jar-file.jar
+--verbosity 10 --ignore-manifest-main-class --function org.cprover.first.RelevantClass.entry --main-class org.cprover.first.RelevantClass
+^EXIT=10$
+^SIGNAL=0$
+Getting class 'org\.cprover\.first\.RelevantClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.first\.RelatedClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.second\.RelatedClassOtherPkg' from JAR target\/jar-file.jar
+--
+Getting class 'org\.cprover\.first\.IrrelevantClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.second\.IrrelevantClassOtherPkg' from JAR target\/jar-file.jar
+--
+This test checks that when --ignore-manifest-main-class, --main-class and
+--function are specified, the class loading behaviour is the same as for
+--ignore-manifest-main-class and --function (assuming that the declaring class
+of the argument of --function is reachable from the argument of --main-class).

jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-ignore-option.desc

@@ -0,0 +1,18 @@
+CORE
+target/jar-file.jar
+--verbosity 10 --ignore-manifest-main-class
+^EXIT=6$
+^SIGNAL=0$
+Getting class 'org\.cprover\.first\.RelevantClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.first\.RelatedClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.first\.IrrelevantClass' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.second\.RelatedClassOtherPkg' from JAR target\/jar-file.jar
+Getting class 'org\.cprover\.second\.IrrelevantClassOtherPkg' from JAR target\/jar-file.jar
+no entry point
+--
+--
+This test checks that when JBMC is given a JAR file whose manifest specifies a
+main class, we can ignore this main class and instead load all classes of the
+JAR file with the option --ignore-manifest-main-class.
+Without this option, IrrelevantClass and IrrelevantClassOtherPkg would not be
+loaded as they are not reachable from RelevantClass (the main class).

jbmc/src/java_bytecode/java_bytecode_language.cpp

@@ -70,6 +70,9 @@ void parse_java_language_options(const cmdlinet &cmd, optionst &options)
   options.set_option(
     "symex-driven-lazy-loading", cmd.isset("symex-driven-lazy-loading"));
 
+  options.set_option(
+    "ignore-manifest-main-class", cmd.isset("ignore-manifest-main-class"));
+
   if(cmd.isset("context-include"))
     options.set_option("context-include", cmd.get_values("context-include"));
 
@@ -202,6 +205,9 @@ void java_bytecode_languaget::set_language_options(const optionst &options)
   nondet_static = options.get_bool_option("nondet-static");
   static_values_file = options.get_option("static-values");
 
+  ignore_manifest_main_class =
+    options.get_bool_option("ignore-manifest-main-class");
+
   if(options.is_set("context-include") || options.is_set("context-exclude"))
     method_in_context = get_context(options);
 
@@ -289,7 +295,7 @@ bool java_bytecode_languaget::parse(
         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.empty())
+        if(!manifest_main_class.empty() && !ignore_manifest_main_class)
           main_class = manifest_main_class;
       }
     }

jbmc/src/java_bytecode/java_bytecode_language.h

@@ -40,6 +40,7 @@ Author: Daniel Kroening, [email protected]
   "(max-nondet-tree-depth):" \
   "(java-max-vla-length):" \
   "(java-cp-include-files):" \
+  "(ignore-manifest-main-class)" \
   "(context-include):" \
   "(context-exclude):" \
   "(no-lazy-methods)" \
@@ -73,6 +74,11 @@ Author: Daniel Kroening, [email protected]
   " --java-max-vla-length N      limit the length of user-code-created arrays\n" /* NOLINT(*) */ \
   " --java-cp-include-files r    regexp or JSON list of files to load\n" \
   "                              (with '@' prefix)\n" \
+  " --ignore-manifest-main-class ignore Main-Class entries in JAR manifest files.\n" /* NOLINT(*) */ \
+  "                              If this option is specified and the options\n" /* NOLINT(*) */ \
+  "                              --function and --main-class are not, we can be\n" /* NOLINT(*) */ \
+  "                              certain that all classes in the JAR file are\n" /* NOLINT(*) */ \
+  "                              loaded.\n" \
   " --context-include i          only analyze code matching specification i that\n" /* NOLINT(*) */ \
   " --context-exclude e          does not match specification e.\n" \
   "                              A specification is any prefix of a package, class\n" /* NOLINT(*) */ \
@@ -215,6 +221,7 @@ class java_bytecode_languaget:public languaget
   bool language_options_initialized;
   irep_idt main_class;
   std::vector<irep_idt> main_jar_classes;
+  bool ignore_manifest_main_class;
   java_class_loadert java_class_loader;
   bool threading_support;
   bool assume_inputs_non_null;      // assume inputs variables to be non-null