diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/pom.xml b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/pom.xml new file mode 100644 index 00000000000..ec40251b157 --- /dev/null +++ b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/pom.xml @@ -0,0 +1,32 @@ + + + 4.0.0 + org.cprover.regression + regression + 1.0-SNAPSHOT + + + jar-file + + + org.apache.maven.plugins + maven-jar-plugin + + + + org.cprover.first.RelevantClass + + + + + + + + + 1.8 + 1.8 + + + diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/first/IrrelevantClass.java b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/first/IrrelevantClass.java new file mode 100644 index 00000000000..7d0f7a62947 --- /dev/null +++ b/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; } +} diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/first/RelatedClass.java b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/first/RelatedClass.java new file mode 100644 index 00000000000..3ff495db92c --- /dev/null +++ b/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; } diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/first/RelevantClass.java b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/first/RelevantClass.java new file mode 100644 index 00000000000..fbe7bf50c96 --- /dev/null +++ b/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; + } +} diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/second/IrrelevantClassOtherPkg.java b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/second/IrrelevantClassOtherPkg.java new file mode 100644 index 00000000000..339f3e74f19 --- /dev/null +++ b/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; } +} diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/second/RelatedClassOtherPkg.java b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/src/main/java/org/cprover/second/RelatedClassOtherPkg.java new file mode 100644 index 00000000000..f860ddf7ef6 --- /dev/null +++ b/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; } diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/target/jar-file.jar b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/target/jar-file.jar new file mode 100644 index 00000000000..d78794d6973 Binary files /dev/null and b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/target/jar-file.jar differ diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-default.desc b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-default.desc new file mode 100644 index 00000000000..1459981b1aa --- /dev/null +++ b/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. diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-ignore-and-function-other.desc b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-ignore-and-function-other.desc new file mode 100644 index 00000000000..373dc8018ef --- /dev/null +++ b/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.' +^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. diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-ignore-and-function.desc b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-ignore-and-function.desc new file mode 100644 index 00000000000..b2d6b38ce5b --- /dev/null +++ b/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. diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-ignore-and-main-class.desc b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-ignore-and-main-class.desc new file mode 100644 index 00000000000..39d177cf1dd --- /dev/null +++ b/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. diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-ignore-function-and-main-class.desc b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-ignore-function-and-main-class.desc new file mode 100644 index 00000000000..1dae1a5c208 --- /dev/null +++ b/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). diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-ignore-option.desc b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/test-ignore-option.desc new file mode 100644 index 00000000000..a4444da921b --- /dev/null +++ b/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). diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index eca24eeaeac..f63975719e5 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/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; } } diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 92740171ebb..5a344a9be18 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -40,6 +40,7 @@ Author: Daniel Kroening, kroening@kroening.com "(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, kroening@kroening.com " --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 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