Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Unsoundness of JBMC in the presence of Multithreading. #8264

Open
ben-Draeger opened this issue Apr 26, 2024 · 7 comments
Open

Unsoundness of JBMC in the presence of Multithreading. #8264

ben-Draeger opened this issue Apr 26, 2024 · 7 comments
Assignees
@peterschrammel

Comments

@ben-Draeger
Copy link

CBMC version: 5.95.1
Operating system: MS Windows 11 Enterprise Version 22H2, Build 22621.3447
Java version: openjdk version "17.0.5" 2022-10-18
Exact command line resulting in the issue: "C:\Program Files\cbmc\bin\jbmc.exe" Race
What behaviour did you expect: I would have expected JBMC to see that b[0] == false at the assert() statement.
What happened instead: JBMC reported VERIFICATION SUCCESSFUL.

In the following java program:

    public class Race {

		public volatile boolean[] b;

		public void doSomething() {
			System.out.println("Main: initializing b to true.");
			b = new boolean[] {true};

			Thread t = new Thread() {
				public void run() {
					b[0] = false;
					System.out.println("Thread: set b to " + b[0]);
				}
			};
			t.start();
			
			try {
				t.join();
			} catch (InterruptedException ie) {
			}
			
			System.out.println("Main: b is " + b[0]);
                        assert(b[0] == true);
		}

        public static void main(String[] args) {
	    new Race().doSomething();
        }                           
    }

JBMC verifies all Verification Conditions.and thus reports VERIFICATION SUCCESSFUL.
However, executing this program with java -ea Race gives an AssertionError in 100% of the cases.
@peterschrammel peterschrammel self-assigned this Apr 26, 2024
@peterschrammel
Copy link
Member

The command line needs to be jbmc Race --classpath .:jbmc/lib/java-models-library/target/core-models.jar:jbmc/lib/java-models-library/target/cprover-api.jar --java-threading.

  • core-models provides part of the JCL
  • cprover-api provides the interface between JBMC and the JCL
  • --java-threading turns on thread handling - this is off by default for performance reasons.

@ben-Draeger
Copy link
Author

I'm sorry, I could not get the command-line you provided to work. I always get the Warning failed to access JAR file '.:jbmc/lib/java-models-library/target/core-models.jar:jbmc/lib/java-models-library/target/cprover-api.jar'.

However, when I add the two JAR files to the classpath and the --java-threading option like this, then JBMC runs successfuly:

"C:\Program Files\cbmc\bin\jbmc.exe" Race --classpath ".;C:\Program Files\cbmc\lib\core-models.jar;C:\Program Files\cbmc\lib\cprover-api.jar" --java-threading

However, when I run it like that, then I get the same result as reported above. JBMC states "VERIFICATION SUCCESSFUL" although running the above program with java -ea Race yields an AssertionError.

@peterschrammel
Copy link
Member

peterschrammel commented May 1, 2024 •
edited

However, when I add the two JAR files to the classpath and the --java-threading option like this, then JBMC runs successfuly:
"C:\Program Files\cbmc\bin\jbmc.exe" Race --classpath ".;C:\Program Files\cbmc\lib\core-models.jar;C:\Program Files\cbmc\lib\cprover-api.jar" --java-threading

Yes, that's the correct commandline on Windows.

I get the same result as reported above. JBMC states "VERIFICATION SUCCESSFUL"

I get

...
[java::Race.doSomething:()V.assertion.1] line 23 assertion at file Race.java line 23 function java::Race.doSomething:()V bytecode-index 46: FAILURE
...
** 1 of 106 failed (2 iterations)
VERIFICATION FAILED

We are both using JBMC and the JAR files built from tag cbmc-5.95.1.
The question is what is different:

  1. I'm using OpenJDK 1.8.0_402. You are using OpenJDK 17.0.5
  2. I'm on Ubuntu 20.04. You are on Windows 11.

@ben-Draeger
Copy link
Author

I tried it again in an Ubuntu-VM with jbmc 5.95.1 and java 17.0.10

On Ubuntu, the command-line you provided works.

Result:

JBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Parsing ...
Warning: failed to access JAR file `jbmc/lib/java-models-library/target/core-models.jar'
Warning: failed to access JAR file `jbmc/lib/java-models-library/target/cprover-api.jar'
Trying to load Java main class: Race
Found Java main class: Race
Converting
stub class symbol java::java.lang.Object already exists
Java: added 5 String or Class constant symbols
Generating GOTO Program
Running GOTO functions transformation passes
Running with 16 object bits, 48 offset bits (default)
Starting Bounded Model Checking
Unwinding loop __CPROVER__start.0 iteration 1  thread 0
Unwinding loop __CPROVER__start.0 iteration 2  thread 0
Unwinding loop __CPROVER__start.0 iteration 3  thread 0
Unwinding loop __CPROVER__start.0 iteration 4  thread 0
Unwinding loop __CPROVER__start.0 iteration 5  thread 0
Unwinding recursion java::Race.<clinit_wrapper> iteration 1
Runtime Symex: 0.0208617s
size of program expression: 618 steps
simple slicing removed 0 assignments
Generated 21 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.000770604s

** Results:
[array-create-negative-size.1] Array size should be >= 0: SUCCESS
[array-create-negative-size.2] Array size should be >= 0: SUCCESS
[array-create-negative-size.3] Array size should be >= 0: SUCCESS
[array-create-negative-size.4] Array size should be >= 0: SUCCESS
[array-create-negative-size.5] Array size should be >= 0: SUCCESS
[array-create-negative-size.6] Array size should be >= 0: SUCCESS
[array-create-negative-size.7] Array size should be >= 0: SUCCESS
[array-create-negative-size.8] Array size should be >= 0: SUCCESS
[array-create-negative-size.9] Array size should be >= 0: SUCCESS
Race.java function java::Race$1.<init>:(LRace;)V
[java::Race$1.<init>:(LRace;)V.null-pointer-exception.1] line 9 Null pointer check: SUCCESS
[java::Race$1.<init>:(LRace;)V.null-pointer-exception.2] line 9 Null pointer check: SUCCESS

Race.java function java::Race.<clinit>:()V
[java::Race.<clinit>:()V.null-pointer-exception.1] line 1 Null pointer check: SUCCESS

Race.java function java::Race.<init>:()V
[java::Race.<init>:()V.null-pointer-exception.1] line 1 Null pointer check: SUCCESS

Race.java function java::Race.doSomething:()V
[java::Race.doSomething:()V.null-pointer-exception.1] line 6 Null pointer check: SUCCESS
[java::Race.doSomething:()V.array-create-negative-size.1] line 7 Array size should be >= 0: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-high.1] line 7 Array index should be < length: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-low.1] line 7 Array index should be >= 0: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.2] line 7 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.3] line 7 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.4] line 9 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.5] line 15 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.6] line 18 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.7] line 22 Null pointer check: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-high.2] line 23 Array index should be < length: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-low.2] line 23 Array index should be >= 0: SUCCESS
[java::Race.doSomething:()V.assertion.1] line 23 assertion at file Race.java line 23 function java::Race.doSomething:()V bytecode-index 40: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.8] line 23 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.9] line 23 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.10] line 23 Null pointer check: SUCCESS

Race.java function java::Race.main:([Ljava/lang/String;)V
[java::Race.main:([Ljava/lang/String;)V.1] line 27 no uncaught exception: SUCCESS
[java::Race.main:([Ljava/lang/String;)V.null-pointer-exception.1] line 27 Null pointer check: SUCCESS
[java::Race.main:([Ljava/lang/String;)V.null-pointer-exception.2] line 27 Null pointer check: SUCCESS

** 0 of 32 failed (1 iterations)
VERIFICATION SUCCESSFUL

I hence tried to get even closer to your configuration and replaced the Java 17 JDK by a Java 1.8 JDK.

And when I ran JBMC with the above command-line against the JDK1.8-compiled class files, the verification indeed failed. However, it was not complaining about the assertion in line 23, but the NullPointerCheck for line 22 failed (a System.out.println).
After I commented out that line and compiled Race.java again, I got the following result:

root@UbuntuVM:/home/vboxuser/shared/jbmc# jbmc Race --classpath .:jbmc/lib/java-models-library/target/core-models.jar:jbmc/lib/java-models-library/target/cprover-api.jar --java-threading
JBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Parsing ...
Warning: failed to access JAR file `jbmc/lib/java-models-library/target/core-models.jar'
Warning: failed to access JAR file `jbmc/lib/java-models-library/target/cprover-api.jar'
Trying to load Java main class: Race
Found Java main class: Race
Converting
stub class symbol java::java.lang.Object already exists
Java: added 8 String or Class constant symbols
Generating GOTO Program
Running GOTO functions transformation passes
Running with 16 object bits, 48 offset bits (default)
Starting Bounded Model Checking
Unwinding loop __CPROVER__start.0 iteration 1  thread 0
Unwinding loop __CPROVER__start.0 iteration 2  thread 0
Unwinding loop __CPROVER__start.0 iteration 3  thread 0
Unwinding loop __CPROVER__start.0 iteration 4  thread 0
Unwinding loop __CPROVER__start.0 iteration 5  thread 0
Unwinding recursion java::Race.<clinit_wrapper> iteration 1
Runtime Symex: 0.0435549s
size of program expression: 607 steps
simple slicing removed 0 assignments
Generated 20 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.000110509s

** Results:
[array-create-negative-size.1] Array size should be >= 0: SUCCESS
[array-create-negative-size.2] Array size should be >= 0: SUCCESS
[array-create-negative-size.3] Array size should be >= 0: SUCCESS
[array-create-negative-size.4] Array size should be >= 0: SUCCESS
[array-create-negative-size.5] Array size should be >= 0: SUCCESS
[array-create-negative-size.6] Array size should be >= 0: SUCCESS
[array-create-negative-size.7] Array size should be >= 0: SUCCESS
[array-create-negative-size.8] Array size should be >= 0: SUCCESS
[array-create-negative-size.9] Array size should be >= 0: SUCCESS
Race.java function java::Race$1.<init>:(LRace;)V
[java::Race$1.<init>:(LRace;)V.null-pointer-exception.1] line 9 Null pointer check: SUCCESS
[java::Race$1.<init>:(LRace;)V.null-pointer-exception.2] line 9 Null pointer check: SUCCESS

Race.java function java::Race.<clinit>:()V
[java::Race.<clinit>:()V.null-pointer-exception.1] line 1 Null pointer check: SUCCESS

Race.java function java::Race.<init>:()V
[java::Race.<init>:()V.null-pointer-exception.1] line 1 Null pointer check: SUCCESS

Race.java function java::Race.doSomething:()V
[java::Race.doSomething:()V.null-pointer-exception.1] line 6 Null pointer check: SUCCESS
[java::Race.doSomething:()V.array-create-negative-size.1] line 7 Array size should be >= 0: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-high.1] line 7 Array index should be < length: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-low.1] line 7 Array index should be >= 0: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.2] line 7 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.3] line 7 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.4] line 9 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.5] line 15 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.6] line 18 Null pointer check: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-high.2] line 23 Array index should be < length: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-low.2] line 23 Array index should be >= 0: SUCCESS
[java::Race.doSomething:()V.assertion.1] line 23 assertion at file Race.java line 23 function java::Race.doSomething:()V bytecode-index 33: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.7] line 23 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.8] line 23 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.9] line 23 Null pointer check: SUCCESS

Race.java function java::Race.main:([Ljava/lang/String;)V
[java::Race.main:([Ljava/lang/String;)V.1] line 27 no uncaught exception: SUCCESS
[java::Race.main:([Ljava/lang/String;)V.null-pointer-exception.1] line 27 Null pointer check: SUCCESS
[java::Race.main:([Ljava/lang/String;)V.null-pointer-exception.2] line 27 Null pointer check: SUCCESS

** 0 of 31 failed (1 iterations)
VERIFICATION SUCCESSFUL

I am stunned. We are BOTH using Ubuntu (22.04.4 LTS in my case). We are BOTH using cbmc 5.95.1 and java 1.8.

Why are we still getting different results?

@peterschrammel
Copy link
Member

Here the files that I use:
jbmc-race.zip
and my output:

$ jbmc/src/jbmc/jbmc Race --classpath .:jbmc/lib/java-models-library/target/core-models.jar:jbmc/lib/java-models-library/target/cprover-api.jar --java-threading
JBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Parsing ...
Trying to load Java main class: Race
Found Java main class: Race
Converting
Java: added 2318 String or Class constant symbols
Generating GOTO Program
Running GOTO functions transformation passes
Running with 16 object bits, 48 offset bits (default)
Starting Bounded Model Checking
Unwinding loop __CPROVER__start.0 iteration 1  thread 0
Unwinding loop __CPROVER__start.0 iteration 2  thread 0
Unwinding loop __CPROVER__start.0 iteration 3  thread 0
Unwinding loop __CPROVER__start.0 iteration 4  thread 0
Unwinding loop __CPROVER__start.0 iteration 5  thread 0
Unwinding recursion java::Race.<clinit_wrapper> iteration 1
Unwinding recursion java::org.cprover.CProver.<clinit_wrapper> iteration 1
Unwinding recursion java::org.cprover.CProver.<clinit_wrapper> iteration 1
Unwinding recursion java::org.cprover.CProver.<clinit_wrapper> iteration 1
Unwinding recursion java::java.lang.String.<clinit_wrapper> iteration 1
Unwinding recursion java::java.lang.String.<clinit_wrapper> iteration 1
aborting path on assume(false) at file Race.java line 23 function java::Race.doSomething:()V bytecode-index 46 thread 0
Unwinding recursion java::org.cprover.CProver.<clinit_wrapper> iteration 1
Unwinding recursion java::org.cprover.CProver.<clinit_wrapper> iteration 1
Unwinding recursion java::org.cprover.CProver.<clinit_wrapper> iteration 1
Unwinding recursion java::java.lang.String.<clinit_wrapper> iteration 1
Unwinding recursion java::java.lang.String.<clinit_wrapper> iteration 1
Unwinding recursion java::org.cprover.CProver.<clinit_wrapper> iteration 1
Unwinding recursion java::org.cprover.CProver.<clinit_wrapper> iteration 1
Unwinding recursion java::org.cprover.CProver.<clinit_wrapper> iteration 1
Runtime Symex: 0.0759836s
Adding SC constraints
Shared java::Race.$assertionsDisabled: 1R/2W
Shared java::java.lang.System.out: 8R/3W
Shared java::java.lang.System__CPROVER_clinit_state: 1R/5W
Shared java::org.cprover.CProver__CPROVER_clinit_state: 2R/7W
Shared java::java.lang.String__CPROVER_clinit_state: 2R/5W
Shared __CPROVER__next_thread_id: 1R/2W
Shared java::java.lang.String.Literal.Main_3a_20b_20is_20..length: 1R/1W
Shared java::java.lang.String.Literal.Main_3a_20b_20is_20..data: 1R/1W
Shared java::java.lang.String.Literal.Thread_3a_20set_20b_20to_20..length: 1R/1W
Shared java::java.lang.String.Literal.Thread_3a_20set_20b_20to_20..data: 1R/1W
Shared java::java.lang.String.Literal.false..length: 2R/1W
Shared java::java.lang.String.Literal.false..data: 2R/1W
Shared java::java.lang.String.Literal.true..length: 2R/1W
Shared java::java.lang.String.Literal.true..data: 2R/1W
Shared symex_dynamic::dynamic_object$10..b: 8R/3W
Shared symex_dynamic::dynamic_object$12..length: 8R/3W
Shared symex_dynamic::dynamic_array$0[[0]]: 7R/3W
Shared symex_dynamic::dynamic_object$13..@java.lang.Thread..@java.lang.Object..@class_identifier: 1R/2W
Shared symex_dynamic::dynamic_object$13..@java.lang.Thread..target: 3R/3W
Shared symex_dynamic::dynamic_object$13..this$0: 4R/3W
Shared symex_dynamic::dynamic_object$14..length: 3R/6W
Shared symex_dynamic::dynamic_object$14..data: 3R/6W
Shared symex_dynamic::dynamic_object$15: 2R/3W
Shared symex_dynamic::dynamic_object$16: 2R/3W
Shared symex_dynamic::dynamic_object$18: 2R/3W
Shared symex_dynamic::dynamic_object$22..length: 3R/6W
Shared symex_dynamic::dynamic_object$22..data: 3R/6W
Shared symex_dynamic::dynamic_object$23: 2R/3W
Shared symex_dynamic::dynamic_object$24: 2R/3W
Shared symex_dynamic::dynamic_object$26: 2R/3W
size of program expression: 3485 steps
no slicing due to threads
Generated 103 VCC(s), 20 remaining after simplification
Runtime Postprocess Equation: 0.0347859s
Passing problem to string refinement loop with MiniSAT 2.2.1 without simplifier
converting SSA
Runtime Convert SSA: 0.010883s
Running string refinement loop with MiniSAT 2.2.1 without simplifier
BV-Refinement: post-processing
BV-Refinement: iteration 1
39646 variables, 82055 clauses
SAT checker: instance is SATISFIABLE
BV-Refinement: got SAT, and it simulates => SAT
Total iterations: 1
Runtime Solver: 0.31395s
Runtime decision procedure: 0.325065s
Running string refinement loop with MiniSAT 2.2.1 without simplifier
BV-Refinement: post-processing
BV-Refinement: iteration 1
39646 variables, 68133 clauses
SAT checker: instance is UNSATISFIABLE
BV-Refinement: got UNSAT, and the proof passes => UNSAT
Total iterations: 1
Runtime Solver: 0.0352986s
Runtime decision procedure: 0.0353428s

** Results:
[array-create-negative-size.1] Array size should be >= 0: SUCCESS
[array-create-negative-size.2] Array size should be >= 0: SUCCESS
[array-create-negative-size.3] Array size should be >= 0: SUCCESS
[array-create-negative-size.4] Array size should be >= 0: SUCCESS
[array-create-negative-size.5] Array size should be >= 0: SUCCESS
[array-create-negative-size.6] Array size should be >= 0: SUCCESS
[array-create-negative-size.7] Array size should be >= 0: SUCCESS
[array-create-negative-size.8] Array size should be >= 0: SUCCESS
[array-create-negative-size.9] Array size should be >= 0: SUCCESS
function java::java.lang.StringBuilder.<init>:()V
[java::java.lang.StringBuilder.<init>:()V.1] assertion: SUCCESS

function java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.1] assertion: SUCCESS
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.2] assertion: SUCCESS
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.3] assertion: SUCCESS
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.4] assertion: SUCCESS
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.5] assertion: SUCCESS
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.6] assertion: SUCCESS

function java::java.lang.StringBuilder.toString:()Ljava/lang/String;
[java::java.lang.StringBuilder.toString:()Ljava/lang/String;.1] assertion: SUCCESS
[java::java.lang.StringBuilder.toString:()Ljava/lang/String;.2] assertion: SUCCESS
[java::java.lang.StringBuilder.toString:()Ljava/lang/String;.3] assertion: SUCCESS

Race.java function java::Race$1.<init>:(LRace;)V
[java::Race$1.<init>:(LRace;)V.null-pointer-exception.1] line 9 Null pointer check: SUCCESS
[java::Race$1.<init>:(LRace;)V.null-pointer-exception.2] line 9 Null pointer check: SUCCESS

Race.java function java::Race$1.run:()V
[java::Race$1.run:()V.array-index-out-of-bounds-high.1] line 11 Array index should be < length: SUCCESS
[java::Race$1.run:()V.array-index-out-of-bounds-low.1] line 11 Array index should be >= 0: SUCCESS
[java::Race$1.run:()V.null-pointer-exception.1] line 11 Null pointer check: SUCCESS
[java::Race$1.run:()V.null-pointer-exception.2] line 11 Null pointer check: SUCCESS
[java::Race$1.run:()V.null-pointer-exception.3] line 11 Null pointer check: SUCCESS
[java::Race$1.run:()V.array-index-out-of-bounds-high.2] line 12 Array index should be < length: SUCCESS
[java::Race$1.run:()V.array-index-out-of-bounds-low.2] line 12 Array index should be >= 0: SUCCESS
[java::Race$1.run:()V.null-pointer-exception.4] line 12 Null pointer check: SUCCESS
[java::Race$1.run:()V.null-pointer-exception.5] line 12 Null pointer check: SUCCESS
[java::Race$1.run:()V.null-pointer-exception.6] line 12 Null pointer check: SUCCESS
[java::Race$1.run:()V.null-pointer-exception.7] line 12 Null pointer check: SUCCESS
[java::Race$1.run:()V.null-pointer-exception.8] line 12 Null pointer check: SUCCESS
[java::Race$1.run:()V.null-pointer-exception.9] line 12 Null pointer check: SUCCESS
[java::Race$1.run:()V.null-pointer-exception.10] line 12 Null pointer check: SUCCESS
[java::Race$1.run:()V.null-pointer-exception.11] line 12 Null pointer check: SUCCESS

Race.java function java::Race.<clinit>:()V
[java::Race.<clinit>:()V.null-pointer-exception.1] line 1 Null pointer check: SUCCESS

Race.java function java::Race.<init>:()V
[java::Race.<init>:()V.null-pointer-exception.1] line 1 Null pointer check: SUCCESS

Race.java function java::Race.doSomething:()V
[java::Race.doSomething:()V.null-pointer-exception.1] line 6 Null pointer check: SUCCESS
[java::Race.doSomething:()V.array-create-negative-size.1] line 7 Array size should be >= 0: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-high.1] line 7 Array index should be < length: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-low.1] line 7 Array index should be >= 0: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.2] line 7 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.3] line 7 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.4] line 9 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.5] line 15 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.6] line 18 Null pointer check: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-high.2] line 22 Array index should be < length: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-low.2] line 22 Array index should be >= 0: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.7] line 22 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.8] line 22 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.9] line 22 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.10] line 22 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.11] line 22 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.12] line 22 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.13] line 22 Null pointer check: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-high.3] line 23 Array index should be < length: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-low.3] line 23 Array index should be >= 0: SUCCESS
[java::Race.doSomething:()V.assertion.1] line 23 assertion at file Race.java line 23 function java::Race.doSomething:()V bytecode-index 46: FAILURE
[java::Race.doSomething:()V.null-pointer-exception.14] line 23 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.15] line 23 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.16] line 23 Null pointer check: SUCCESS

Race.java function java::Race.main:([Ljava/lang/String;)V
[java::Race.main:([Ljava/lang/String;)V.1] line 27 no uncaught exception: SUCCESS
[java::Race.main:([Ljava/lang/String;)V.null-pointer-exception.1] line 27 Null pointer check: SUCCESS
[java::Race.main:([Ljava/lang/String;)V.null-pointer-exception.2] line 27 Null pointer check: SUCCESS

java/lang/AssertionError.java function java::java.lang.AssertionError.<init>:()V
[java::java.lang.AssertionError.<init>:()V.null-pointer-exception.1] line 49 Null pointer check: SUCCESS

java/lang/Class.java function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V
[java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V.null-pointer-exception.1] line 473 Null pointer check: SUCCESS
[java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V.null-pointer-exception.2] line 474 Null pointer check: SUCCESS
[java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V.null-pointer-exception.3] line 475 Null pointer check: SUCCESS
[java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V.null-pointer-exception.4] line 476 Null pointer check: SUCCESS
[java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V.null-pointer-exception.5] line 477 Null pointer check: SUCCESS
[java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V.null-pointer-exception.6] line 478 Null pointer check: SUCCESS
[java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V.null-pointer-exception.7] line 479 Null pointer check: SUCCESS
[java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V.null-pointer-exception.8] line 480 Null pointer check: SUCCESS

java/lang/Class.java function java::java.lang.Class.cproverNondetInitialize:()V
[java::java.lang.Class.cproverNondetInitialize:()V.null-pointer-exception.1] line 454 Null pointer check: SUCCESS
[java::java.lang.Class.cproverNondetInitialize:()V.null-pointer-exception.2] line 455 Null pointer check: SUCCESS

java/lang/Class.java function java::java.lang.Class.desiredAssertionStatus:()Z
[java::java.lang.Class.desiredAssertionStatus:()Z.null-pointer-exception.1] line 421 Null pointer check: SUCCESS
[java::java.lang.Class.desiredAssertionStatus:()Z.null-pointer-exception.2] line 428 Null pointer check: SUCCESS
[java::java.lang.Class.desiredAssertionStatus:()Z.null-pointer-exception.3] line 428 Null pointer check: SUCCESS
[java::java.lang.Class.desiredAssertionStatus:()Z.null-pointer-exception.4] line 429 Null pointer check: SUCCESS
[java::java.lang.Class.desiredAssertionStatus:()Z.null-pointer-exception.5] line 430 Null pointer check: SUCCESS
[java::java.lang.Class.desiredAssertionStatus:()Z.null-pointer-exception.6] line 430 Null pointer check: SUCCESS
[java::java.lang.Class.desiredAssertionStatus:()Z.null-pointer-exception.7] line 432 Null pointer check: SUCCESS

java/lang/Class.java function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader;
[java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader;.null-pointer-exception.1] line 191 Null pointer check: SUCCESS

java/lang/Class.java function java::java.lang.Class.getName:()Ljava/lang/String;
[java::java.lang.Class.getName:()Ljava/lang/String;.null-pointer-exception.1] line 158 Null pointer check: SUCCESS

java/lang/Error.java function java::java.lang.Error.<init>:()V
[java::java.lang.Error.<init>:()V.null-pointer-exception.1] line 58 Null pointer check: SUCCESS

java/lang/Exception.java function java::java.lang.Exception.<init>:()V
[java::java.lang.Exception.<init>:()V.null-pointer-exception.1] line 54 Null pointer check: SUCCESS

java/lang/NullPointerException.java function java::java.lang.NullPointerException.<init>:()V
[java::java.lang.NullPointerException.<init>:()V.null-pointer-exception.1] line 33 Null pointer check: SUCCESS

java/lang/Object.java function java::java.lang.Object.<init>:()V
[java::java.lang.Object.<init>:()V.null-pointer-exception.1] line 40 Null pointer check: SUCCESS

java/lang/Object.java function java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V
[java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V.null-pointer-exception.1] line 122 Null pointer check: SUCCESS
[java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V.null-pointer-exception.2] line 122 Null pointer check: SUCCESS
[java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V.null-pointer-exception.3] line 127 Null pointer check: SUCCESS
[java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V.null-pointer-exception.4] line 128 Null pointer check: SUCCESS
[java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V.null-pointer-exception.5] line 128 Null pointer check: SUCCESS

java/lang/Object.java function java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V
[java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V.null-pointer-exception.1] line 152 Null pointer check: SUCCESS
[java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V.null-pointer-exception.2] line 152 Null pointer check: SUCCESS

java/lang/RuntimeException.java function java::java.lang.RuntimeException.<init>:()V
[java::java.lang.RuntimeException.<init>:()V.null-pointer-exception.1] line 32 Null pointer check: SUCCESS

java/lang/StringBuilder.java function java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;
[java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;.null-pointer-exception.1] line 273 Null pointer check: SUCCESS

java/lang/Thread.java function java::java.lang.Thread.<init>:()V
[java::java.lang.Thread.<init>:()V.null-pointer-exception.1] line 399 Null pointer check: SUCCESS
[java::java.lang.Thread.<init>:()V.null-pointer-exception.2] line 400 Null pointer check: SUCCESS
[java::java.lang.Thread.<init>:()V.null-pointer-exception.3] line 401 Null pointer check: SUCCESS

java/lang/Thread.java function java::java.lang.Thread.start:()V
[java::java.lang.Thread.start:()V.null-pointer-exception.1] line 663 Null pointer check: SUCCESS
[java::java.lang.Thread.start:()V.null-pointer-exception.2] line 663 Null pointer check: SUCCESS

java/lang/Throwable.java function java::java.lang.Throwable.<init>:()V
[java::java.lang.Throwable.<init>:()V.null-pointer-exception.2] line 201 Null pointer check: SUCCESS
[java::java.lang.Throwable.<init>:()V.null-pointer-exception.1] line 264 Null pointer check: SUCCESS
[java::java.lang.Throwable.<init>:()V.null-pointer-exception.3] line 266 Null pointer check: SUCCESS

** 1 of 106 failed (2 iterations)
VERIFICATION FAILED

@ben-Draeger
Copy link
Author

ben-Draeger commented May 15, 2024 •
edited

Thanks for posting your files.

I tried to reproduce your result. However, when I ask YOUR jbmc to verify YOUR Race.class using YOUR Jars on my Ubuntu VM, then I get the following output instead:

root@UbuntuVM:/home/vboxuser/shared/jbmc-race# ./jbmc Race --classpath .:core-models.jar:cprover-api.jar --java-threading
JBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Parsing ...
Trying to load Java main class: Race
Found Java main class: Race
Converting
Java: added 2315 String or Class constant symbols
Generating GOTO Program
Running GOTO functions transformation passes
Running with 16 object bits, 48 offset bits (default)
Starting Bounded Model Checking
Unwinding loop __CPROVER__start.0 iteration 1  thread 0
Unwinding loop __CPROVER__start.0 iteration 2  thread 0
Unwinding loop __CPROVER__start.0 iteration 3  thread 0
Unwinding loop __CPROVER__start.0 iteration 4  thread 0
Unwinding loop __CPROVER__start.0 iteration 5  thread 0
Unwinding recursion java::Race.<clinit_wrapper> iteration 1
Unwinding recursion java::org.cprover.CProver.<clinit_wrapper> iteration 1
Unwinding recursion java::org.cprover.CProver.<clinit_wrapper> iteration 1
Unwinding recursion java::org.cprover.CProver.<clinit_wrapper> iteration 1
Unwinding recursion java::java.lang.String.<clinit_wrapper> iteration 1
Unwinding recursion java::java.lang.String.<clinit_wrapper> iteration 1
aborting path on assume(false) at file Race.java line 23 function java::Race.doSomething:()V bytecode-index 46 thread 0
**** WARNING: no body for function java::java.lang.Runnable.run:()V
Unwinding recursion java::org.cprover.CProver.<clinit_wrapper> iteration 1
Unwinding recursion java::org.cprover.CProver.<clinit_wrapper> iteration 1
Unwinding recursion java::org.cprover.CProver.<clinit_wrapper> iteration 1
Runtime Symex: 0.14105s
Adding SC constraints
Shared java::Race.$assertionsDisabled: 1R/2W
Shared java::java.lang.System.out: 4R/2W
Shared java::org.cprover.CProver__CPROVER_clinit_state: 1R/5W
Shared java::java.lang.String__CPROVER_clinit_state: 1R/3W
Shared __CPROVER__next_thread_id: 1R/2W
Shared java::java.lang.String.Literal.Main_3a_20b_20is_20..length: 1R/1W
Shared java::java.lang.String.Literal.Main_3a_20b_20is_20..data: 1R/1W
Shared java::java.lang.String.Literal.false..length: 1R/1W
Shared java::java.lang.String.Literal.false..data: 1R/1W
Shared java::java.lang.String.Literal.true..length: 1R/1W
Shared java::java.lang.String.Literal.true..data: 1R/1W
Shared symex_dynamic::dynamic_object$10..b: 4R/3W
Shared symex_dynamic::dynamic_object$12..length: 4R/3W
Shared symex_dynamic::dynamic_array$0[[0]]: 4R/2W
Shared symex_dynamic::dynamic_object$13..@class_identifier: 3R/2W
Shared symex_dynamic::dynamic_object$14..length: 3R/6W
Shared symex_dynamic::dynamic_object$14..data: 3R/6W
Shared symex_dynamic::dynamic_object$15: 2R/3W
Shared symex_dynamic::dynamic_object$16: 2R/3W
Shared symex_dynamic::dynamic_object$18: 2R/3W
Shared java::java.lang.Thread.start:()V::this_argument$object..@java.lang.Object..@class_identifier: 1R/1W
size of program expression: 2125 steps
no slicing due to threads
Generated 65 VCC(s), 9 remaining after simplification
Runtime Postprocess Equation: 0.0565582s
Passing problem to string refinement loop with MiniSAT 2.2.1 without simplifier
converting SSA
Runtime Convert SSA: 0.0310797s
Running string refinement loop with MiniSAT 2.2.1 without simplifier
BV-Refinement: post-processing
BV-Refinement: iteration 1
24107 variables, 40692 clauses
SAT checker: instance is SATISFIABLE
BV-Refinement: got SAT, and it simulates => SAT
Total iterations: 1
Runtime Solver: 0.179112s
Runtime decision procedure: 0.21305s
Running string refinement loop with MiniSAT 2.2.1 without simplifier
BV-Refinement: post-processing
BV-Refinement: iteration 1
24107 variables, 31621 clauses
SAT checker: instance is UNSATISFIABLE
BV-Refinement: got UNSAT, and the proof passes => UNSAT
Total iterations: 1
Runtime Solver: 0.0140745s
Runtime decision procedure: 0.0141478s

** Results:
[array-create-negative-size.1] Array size should be >= 0: SUCCESS
[array-create-negative-size.2] Array size should be >= 0: SUCCESS
[array-create-negative-size.3] Array size should be >= 0: SUCCESS
[array-create-negative-size.4] Array size should be >= 0: SUCCESS
[array-create-negative-size.5] Array size should be >= 0: SUCCESS
[array-create-negative-size.6] Array size should be >= 0: SUCCESS
[array-create-negative-size.7] Array size should be >= 0: SUCCESS
[array-create-negative-size.8] Array size should be >= 0: SUCCESS
[array-create-negative-size.9] Array size should be >= 0: SUCCESS
function java::java.lang.StringBuilder.<init>:()V
[java::java.lang.StringBuilder.<init>:()V.1] assertion: SUCCESS

function java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.1] assertion: SUCCESS
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.2] assertion: SUCCESS
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.3] assertion: SUCCESS
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.4] assertion: SUCCESS
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.5] assertion: SUCCESS
[java::java.lang.StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;.6] assertion: SUCCESS

function java::java.lang.StringBuilder.toString:()Ljava/lang/String;
[java::java.lang.StringBuilder.toString:()Ljava/lang/String;.1] assertion: SUCCESS
[java::java.lang.StringBuilder.toString:()Ljava/lang/String;.2] assertion: SUCCESS
[java::java.lang.StringBuilder.toString:()Ljava/lang/String;.3] assertion: SUCCESS

Race.java function java::Race.<clinit>:()V
[java::Race.<clinit>:()V.null-pointer-exception.1] line 1 Null pointer check: SUCCESS

Race.java function java::Race.<init>:()V
[java::Race.<init>:()V.null-pointer-exception.1] line 1 Null pointer check: SUCCESS

Race.java function java::Race.doSomething:()V
[java::Race.doSomething:()V.null-pointer-exception.1] line 6 Null pointer check: SUCCESS
[java::Race.doSomething:()V.array-create-negative-size.1] line 7 Array size should be >= 0: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-high.1] line 7 Array index should be < length: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-low.1] line 7 Array index should be >= 0: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.2] line 7 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.3] line 7 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.4] line 9 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.5] line 15 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.6] line 18 Null pointer check: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-high.2] line 22 Array index should be < length: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-low.2] line 22 Array index should be >= 0: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.7] line 22 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.8] line 22 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.9] line 22 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.10] line 22 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.11] line 22 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.12] line 22 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.13] line 22 Null pointer check: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-high.3] line 23 Array index should be < length: SUCCESS
[java::Race.doSomething:()V.array-index-out-of-bounds-low.3] line 23 Array index should be >= 0: SUCCESS
[java::Race.doSomething:()V.assertion.1] line 23 assertion at file Race.java line 23 function java::Race.doSomething:()V bytecode-index 46: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.14] line 23 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.15] line 23 Null pointer check: SUCCESS
[java::Race.doSomething:()V.null-pointer-exception.16] line 23 Null pointer check: SUCCESS

Race.java function java::Race.main:([Ljava/lang/String;)V
[java::Race.main:([Ljava/lang/String;)V.1] line 27 no uncaught exception: SUCCESS
[java::Race.main:([Ljava/lang/String;)V.null-pointer-exception.1] line 27 Null pointer check: SUCCESS
[java::Race.main:([Ljava/lang/String;)V.null-pointer-exception.2] line 27 Null pointer check: SUCCESS

java/lang/AssertionError.java function java::java.lang.AssertionError.<init>:()V
[java::java.lang.AssertionError.<init>:()V.null-pointer-exception.1] line 49 Null pointer check: SUCCESS

java/lang/Class.java function java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V
[java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V.null-pointer-exception.1] line 473 Null pointer check: SUCCESS
[java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V.null-pointer-exception.2] line 474 Null pointer check: SUCCESS
[java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V.null-pointer-exception.3] line 475 Null pointer check: SUCCESS
[java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V.null-pointer-exception.4] line 476 Null pointer check: SUCCESS
[java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V.null-pointer-exception.5] line 477 Null pointer check: SUCCESS
[java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V.null-pointer-exception.6] line 478 Null pointer check: SUCCESS
[java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V.null-pointer-exception.7] line 479 Null pointer check: SUCCESS
[java::java.lang.Class.cproverInitializeClassLiteral:(Ljava/lang/String;ZZZZZZZ)V.null-pointer-exception.8] line 480 Null pointer check: SUCCESS

java/lang/Class.java function java::java.lang.Class.cproverNondetInitialize:()V
[java::java.lang.Class.cproverNondetInitialize:()V.null-pointer-exception.1] line 454 Null pointer check: SUCCESS
[java::java.lang.Class.cproverNondetInitialize:()V.null-pointer-exception.2] line 455 Null pointer check: SUCCESS

java/lang/Class.java function java::java.lang.Class.desiredAssertionStatus:()Z
[java::java.lang.Class.desiredAssertionStatus:()Z.null-pointer-exception.1] line 421 Null pointer check: SUCCESS
[java::java.lang.Class.desiredAssertionStatus:()Z.null-pointer-exception.2] line 428 Null pointer check: SUCCESS
[java::java.lang.Class.desiredAssertionStatus:()Z.null-pointer-exception.3] line 428 Null pointer check: SUCCESS
[java::java.lang.Class.desiredAssertionStatus:()Z.null-pointer-exception.4] line 429 Null pointer check: SUCCESS
[java::java.lang.Class.desiredAssertionStatus:()Z.null-pointer-exception.5] line 430 Null pointer check: SUCCESS
[java::java.lang.Class.desiredAssertionStatus:()Z.null-pointer-exception.6] line 430 Null pointer check: SUCCESS
[java::java.lang.Class.desiredAssertionStatus:()Z.null-pointer-exception.7] line 432 Null pointer check: SUCCESS

java/lang/Class.java function java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader;
[java::java.lang.Class.getClassLoader:()Ljava/lang/ClassLoader;.null-pointer-exception.1] line 191 Null pointer check: SUCCESS

java/lang/Class.java function java::java.lang.Class.getName:()Ljava/lang/String;
[java::java.lang.Class.getName:()Ljava/lang/String;.null-pointer-exception.1] line 158 Null pointer check: SUCCESS

java/lang/Error.java function java::java.lang.Error.<init>:()V
[java::java.lang.Error.<init>:()V.null-pointer-exception.1] line 58 Null pointer check: SUCCESS

java/lang/Exception.java function java::java.lang.Exception.<init>:()V
[java::java.lang.Exception.<init>:()V.null-pointer-exception.1] line 54 Null pointer check: SUCCESS

java/lang/NullPointerException.java function java::java.lang.NullPointerException.<init>:()V
[java::java.lang.NullPointerException.<init>:()V.null-pointer-exception.1] line 33 Null pointer check: SUCCESS

java/lang/Object.java function java::java.lang.Object.<init>:()V
[java::java.lang.Object.<init>:()V.null-pointer-exception.1] line 40 Null pointer check: SUCCESS

java/lang/Object.java function java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V
[java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V.null-pointer-exception.1] line 122 Null pointer check: SUCCESS
[java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V.null-pointer-exception.2] line 122 Null pointer check: SUCCESS
[java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V.null-pointer-exception.3] line 127 Null pointer check: SUCCESS
[java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V.null-pointer-exception.4] line 128 Null pointer check: SUCCESS
[java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V.null-pointer-exception.5] line 128 Null pointer check: SUCCESS

java/lang/Object.java function java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V
[java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V.null-pointer-exception.1] line 152 Null pointer check: SUCCESS
[java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V.null-pointer-exception.2] line 152 Null pointer check: SUCCESS

java/lang/RuntimeException.java function java::java.lang.RuntimeException.<init>:()V
[java::java.lang.RuntimeException.<init>:()V.null-pointer-exception.1] line 32 Null pointer check: SUCCESS

java/lang/StringBuilder.java function java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;
[java::java.lang.StringBuilder.append:(Z)Ljava/lang/StringBuilder;.null-pointer-exception.1] line 273 Null pointer check: SUCCESS

java/lang/Thread.java function java::java.lang.Thread.start:()V
[java::java.lang.Thread.start:()V.null-pointer-exception.1] line 663 Null pointer check: SUCCESS
[java::java.lang.Thread.start:()V.null-pointer-exception.2] line 663 Null pointer check: FAILURE

java/lang/Throwable.java function java::java.lang.Throwable.<init>:()V
[java::java.lang.Throwable.<init>:()V.null-pointer-exception.2] line 201 Null pointer check: SUCCESS
[java::java.lang.Throwable.<init>:()V.null-pointer-exception.1] line 264 Null pointer check: SUCCESS
[java::java.lang.Throwable.<init>:()V.null-pointer-exception.3] line 266 Null pointer check: SUCCESS

** 1 of 86 failed (2 iterations)
VERIFICATION FAILED

As you can see, the Verification also fails, but it does not fail because it cannot verify the assertion in line 23 of Race.java, but it fails because a NullPointerCheck in Thread.java fails to verify.
Also: it generates only 86 verification conditions instead of 106 like in your run.
Also note that the assertion in line 23 of Race.java was verified successfully, which indicates that the original problem still persists.

It still seems to make a significant difference if it is run on my Ubuntu VM or on your Ubuntu Machine. And this difference is NOT due to the Java Bytecode and NOT due to the JBMC binary or its JARs.

@ben-Draeger
Copy link
Author

Since we seem to have a difference in our environment, I reproduced the problem in Docker.
Here are the Dockerfiles to reproduce it:

  • First I tried to compile the java file with JDK11, which leads to the VERIFICATION SUCCESSFUL result:
    problem-jdk11.zip

  • Then I tried to compile it with JDK8 instead, which reports a VERIFICATION FAILED, but fails due to a NullPointer problem in line 22 instead of the assertion in line 23:
    problem-jdk8.zip

In order to reproduce it,

  1. unpack the zipfile into a folder
  2. run "docker build -t problem ." in that folder to build the image (from the Dockerfile - standard Ubuntu with JBMC and the right JDK installed)
  3. run "docker run -it problem" to execute JBMC in a container spawned from the image and see the result.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@peterschrammel peterschrammel

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@peterschrammel @ben-Draeger