Skip to content

Commit e7646df

Browse files
antlechnerantlechner
authored
Merge pull request #5068 from antlechner/antonia/load-whole-jar-option
[TG-9219] Add new option --ignore-manifest-main-class
2 parents a3aee7d + 54ee1a9 commit e7646df

15 files changed

+173
-1
lines changed

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

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
<?xml version="1.0" encoding="UTF-8"?>
2+
<project xmlns="http://maven.apache.org/POM/4.0.0"
3+
xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
4+
xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
5+
<modelVersion>4.0.0</modelVersion>
6+
<groupId>org.cprover.regression</groupId>
7+
<artifactId>regression</artifactId>
8+
<version>1.0-SNAPSHOT</version>
9+
10+
<build>
11+
<finalName>jar-file</finalName>
12+
<plugins>
13+
<plugin>
14+
<groupId>org.apache.maven.plugins</groupId>
15+
<artifactId>maven-jar-plugin</artifactId>
16+
<configuration>
17+
<archive>
18+
<manifest>
19+
<mainClass>org.cprover.first.RelevantClass</mainClass>
20+
</manifest>
21+
</archive>
22+
</configuration>
23+
</plugin>
24+
</plugins>
25+
</build>
26+
27+
<properties>
28+
<maven.compiler.source>1.8</maven.compiler.source>
29+
<maven.compiler.target>1.8</maven.compiler.target>
30+
</properties>
31+
32+
</project>

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
package org.cprover.first;
2+
3+
public class IrrelevantClass {
4+
5+
public static void notImportant() { assert true; }
6+
}

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
package org.cprover.first;
2+
3+
public class RelatedClass { public int i; }

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
package org.cprover.first;
2+
3+
import org.cprover.second.RelatedClassOtherPkg;
4+
5+
public class RelevantClass {
6+
7+
public static void entry(RelatedClass rc, RelatedClassOtherPkg rcop) {
8+
assert false;
9+
}
10+
}

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,6 @@
1+
package org.cprover.second;
2+
3+
public class IrrelevantClassOtherPkg {
4+
5+
public static void notImportant() { assert true; }
6+
}

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
package org.cprover.second;
2+
3+
public class RelatedClassOtherPkg { public int i; }

‎jbmc/regression/jbmc/classpath-jar-load-whole-jar/target/jar-file.jar

4.35 KB
Binary file not shown.

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

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
target/jar-file.jar
3+
--verbosity 10
4+
^EXIT=6$
5+
^SIGNAL=0$
6+
Getting class 'org\.cprover\.first\.RelevantClass' from JAR target\/jar-file.jar
7+
Getting class 'org\.cprover\.first\.RelatedClass' from JAR target\/jar-file.jar
8+
Getting class 'org\.cprover\.second\.RelatedClassOtherPkg' from JAR target\/jar-file.jar
9+
no entry point
10+
--
11+
Getting class 'org\.cprover\.first\.IrrelevantClass' from JAR target\/jar-file.jar
12+
Getting class 'org\.cprover\.second\.IrrelevantClassOtherPkg' from JAR target\/jar-file.jar
13+
--
14+
This test checks that without the --ignore-manifest-main-class method, we only
15+
load those classes that are referenced by the main class specified in the
16+
manifest file of a jar file.

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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CORE
2+
target/jar-file.jar
3+
--verbosity 10 --ignore-manifest-main-class --function 'org.cprover.second.IrrelevantClassOtherPkg.<init>'
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
Getting class 'org\.cprover\.second\.IrrelevantClassOtherPkg' from JAR target\/jar-file.jar
7+
--
8+
Getting class 'org\.cprover\.first\.RelevantClass' from JAR target\/jar-file.jar
9+
Getting class 'org\.cprover\.first\.RelatedClass' from JAR target\/jar-file.jar
10+
Getting class 'org\.cprover\.second\.RelatedClassOtherPkg' from JAR target\/jar-file.jar
11+
Getting class 'org\.cprover\.first\.IrrelevantClass' from JAR target\/jar-file.jar
12+
--
13+
This test checks that when both --ignore-manifest-main-class and --function are
14+
specified, we use the declaring class of the argument of --function as the main
15+
class from where to start loading other classes.
16+
The difference from the similar test test-ignore-and-function.desc is that in
17+
this case, the main class specified by --function is different from the main
18+
class specified in the JAR manifest file.

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

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
CORE
2+
target/jar-file.jar
3+
--verbosity 10 --ignore-manifest-main-class --function org.cprover.first.RelevantClass.entry
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
Getting class 'org\.cprover\.first\.RelevantClass' from JAR target\/jar-file.jar
7+
Getting class 'org\.cprover\.first\.RelatedClass' from JAR target\/jar-file.jar
8+
Getting class 'org\.cprover\.second\.RelatedClassOtherPkg' from JAR target\/jar-file.jar
9+
--
10+
Getting class 'org\.cprover\.first\.IrrelevantClass' from JAR target\/jar-file.jar
11+
Getting class 'org\.cprover\.second\.IrrelevantClassOtherPkg' from JAR target\/jar-file.jar
12+
--
13+
This test checks that when both --ignore-manifest-main-class and --function are
14+
specified, we use the declaring class of the argument of --function as the main
15+
class from where to start loading other classes.

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

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
target/jar-file.jar
3+
--verbosity 10 --ignore-manifest-main-class --main-class org.cprover.first.RelevantClass
4+
^EXIT=6$
5+
^SIGNAL=0$
6+
Getting class 'org\.cprover\.first\.RelevantClass' from JAR target\/jar-file.jar
7+
Getting class 'org\.cprover\.first\.RelatedClass' from JAR target\/jar-file.jar
8+
Getting class 'org\.cprover\.second\.RelatedClassOtherPkg' from JAR target\/jar-file.jar
9+
no entry point
10+
--
11+
Getting class 'org\.cprover\.first\.IrrelevantClass' from JAR target\/jar-file.jar
12+
Getting class 'org\.cprover\.second\.IrrelevantClassOtherPkg' from JAR target\/jar-file.jar
13+
--
14+
This test checks that when both --ignore-manifest-main-class and --main-class
15+
are specified, we use the argument of --main-class as the main class from where
16+
to start loading other classes.

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

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE
2+
target/jar-file.jar
3+
--verbosity 10 --ignore-manifest-main-class --function org.cprover.first.RelevantClass.entry --main-class org.cprover.first.RelevantClass
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
Getting class 'org\.cprover\.first\.RelevantClass' from JAR target\/jar-file.jar
7+
Getting class 'org\.cprover\.first\.RelatedClass' from JAR target\/jar-file.jar
8+
Getting class 'org\.cprover\.second\.RelatedClassOtherPkg' from JAR target\/jar-file.jar
9+
--
10+
Getting class 'org\.cprover\.first\.IrrelevantClass' from JAR target\/jar-file.jar
11+
Getting class 'org\.cprover\.second\.IrrelevantClassOtherPkg' from JAR target\/jar-file.jar
12+
--
13+
This test checks that when --ignore-manifest-main-class, --main-class and
14+
--function are specified, the class loading behaviour is the same as for
15+
--ignore-manifest-main-class and --function (assuming that the declaring class
16+
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

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
CORE
2+
target/jar-file.jar
3+
--verbosity 10 --ignore-manifest-main-class
4+
^EXIT=6$
5+
^SIGNAL=0$
6+
Getting class 'org\.cprover\.first\.RelevantClass' from JAR target\/jar-file.jar
7+
Getting class 'org\.cprover\.first\.RelatedClass' from JAR target\/jar-file.jar
8+
Getting class 'org\.cprover\.first\.IrrelevantClass' from JAR target\/jar-file.jar
9+
Getting class 'org\.cprover\.second\.RelatedClassOtherPkg' from JAR target\/jar-file.jar
10+
Getting class 'org\.cprover\.second\.IrrelevantClassOtherPkg' from JAR target\/jar-file.jar
11+
no entry point
12+
--
13+
--
14+
This test checks that when JBMC is given a JAR file whose manifest specifies a
15+
main class, we can ignore this main class and instead load all classes of the
16+
JAR file with the option --ignore-manifest-main-class.
17+
Without this option, IrrelevantClass and IrrelevantClassOtherPkg would not be
18+
loaded as they are not reachable from RelevantClass (the main class).

‎jbmc/src/java_bytecode/java_bytecode_language.cpp

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -70,6 +70,9 @@ void parse_java_language_options(const cmdlinet &cmd, optionst &options)
7070
options.set_option(
7171
"symex-driven-lazy-loading", cmd.isset("symex-driven-lazy-loading"));
7272

73+
options.set_option(
74+
"ignore-manifest-main-class", cmd.isset("ignore-manifest-main-class"));
75+
7376
if(cmd.isset("context-include"))
7477
options.set_option("context-include", cmd.get_values("context-include"));
7578

@@ -202,6 +205,9 @@ void java_bytecode_languaget::set_language_options(const optionst &options)
202205
nondet_static = options.get_bool_option("nondet-static");
203206
static_values_file = options.get_option("static-values");
204207

208+
ignore_manifest_main_class =
209+
options.get_bool_option("ignore-manifest-main-class");
210+
205211
if(options.is_set("context-include") || options.is_set("context-exclude"))
206212
method_in_context = get_context(options);
207213

@@ -289,7 +295,7 @@ bool java_bytecode_languaget::parse(
289295
std::string manifest_main_class = manifest["Main-Class"];
290296

291297
// if the manifest declares a Main-Class line, we got a main class
292-
if(!manifest_main_class.empty())
298+
if(!manifest_main_class.empty() && !ignore_manifest_main_class)
293299
main_class = manifest_main_class;
294300
}
295301
}

‎jbmc/src/java_bytecode/java_bytecode_language.h

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@ Author: Daniel Kroening, [email protected]
4040
"(max-nondet-tree-depth):" \
4141
"(java-max-vla-length):" \
4242
"(java-cp-include-files):" \
43+
"(ignore-manifest-main-class)" \
4344
"(context-include):" \
4445
"(context-exclude):" \
4546
"(no-lazy-methods)" \
@@ -73,6 +74,11 @@ Author: Daniel Kroening, [email protected]
7374
" --java-max-vla-length N limit the length of user-code-created arrays\n" /* NOLINT(*) */ \
7475
" --java-cp-include-files r regexp or JSON list of files to load\n" \
7576
" (with '@' prefix)\n" \
77+
" --ignore-manifest-main-class ignore Main-Class entries in JAR manifest files.\n" /* NOLINT(*) */ \
78+
" If this option is specified and the options\n" /* NOLINT(*) */ \
79+
" --function and --main-class are not, we can be\n" /* NOLINT(*) */ \
80+
" certain that all classes in the JAR file are\n" /* NOLINT(*) */ \
81+
" loaded.\n" \
7682
" --context-include i only analyze code matching specification i that\n" /* NOLINT(*) */ \
7783
" --context-exclude e does not match specification e.\n" \
7884
" A specification is any prefix of a package, class\n" /* NOLINT(*) */ \
@@ -215,6 +221,7 @@ class java_bytecode_languaget:public languaget
215221
bool language_options_initialized;
216222
irep_idt main_class;
217223
std::vector<irep_idt> main_jar_classes;
224+
bool ignore_manifest_main_class;
218225
java_class_loadert java_class_loader;
219226
bool threading_support;
220227
bool assume_inputs_non_null; // assume inputs variables to be non-null

0 commit comments

Comments
 (0)