diff --git a/appveyor.yml b/appveyor.yml index 65e6511e7d4..f17933269bb 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -18,6 +18,7 @@ install: Move-Item win_flex.exe bin\flex.exe -force Move-Item FlexLexer.h include\FlexLexer.h -force Remove-Item bin\data -Force -Recurse -ErrorAction SilentlyContinue + Remove-Item java-models-library-master -Force -Recurse -ErrorAction SilentlyContinue Move-Item data bin\data -force bison -V flex -V @@ -90,7 +91,6 @@ test_script: rmdir /s /q jbmc\classpath1 rmdir /s /q jbmc\jar-file3 rmdir /s /q jbmc\tableswitch2 - rmdir /s /q jbmc-concurrency\explicit_thread_blocks cd ../.. make -C jbmc/regression test diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A$1.class b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A$1.class new file mode 100644 index 00000000000..6fa94cda14f Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A$1.class differ diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A$2.class b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A$2.class new file mode 100644 index 00000000000..70267c266d2 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A$2.class differ diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A.class b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A.class new file mode 100644 index 00000000000..374de28031a Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A.class differ diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A.java b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A.java new file mode 100644 index 00000000000..e7d7ec5f0d3 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/A.java @@ -0,0 +1,39 @@ +import java.lang.Thread; +import org.cprover.CProver; + +public class A +{ + int x = 0; + + // expected verfication success + public void me() + { + Thread t = new Thread() + { + public void run() + { + x = 44; + int local_x = x; + assert(local_x == 44 || x == 10); + } + }; + t.start(); + x = 10; + } + + // expected verfication failure + public void me2() + { + Thread t = new Thread() + { + public void run() + { + x = 44; + int local_x = x; + assert(local_x == 44); + } + }; + t.start(); + x = 10; + } +} diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc new file mode 100644 index 00000000000..e7468745c1d --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc new file mode 100644 index 00000000000..4918125c3a4 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc @@ -0,0 +1,5 @@ +CORE +A.class +--function 'A.me2:()V' --lazy-methods --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^SIGNAL=0$ +^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-concurrency/explicit_thread_blocks/A.class b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/A.class similarity index 100% rename from jbmc/regression/jbmc-concurrency/explicit_thread_blocks/A.class rename to jbmc/regression/jbmc-concurrency/explicit-thread-blocks/A.class diff --git a/jbmc/regression/jbmc-concurrency/explicit_thread_blocks/A.java b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/A.java similarity index 100% rename from jbmc/regression/jbmc-concurrency/explicit_thread_blocks/A.java rename to jbmc/regression/jbmc-concurrency/explicit-thread-blocks/A.java diff --git a/jbmc/regression/jbmc-concurrency/explicit_thread_blocks/test.desc b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc similarity index 51% rename from jbmc/regression/jbmc-concurrency/explicit_thread_blocks/test.desc rename to jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc index 9dd422bc973..1538f4a7c5c 100644 --- a/jbmc/regression/jbmc-concurrency/explicit_thread_blocks/test.desc +++ b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc @@ -1,7 +1,6 @@ CORE A.class ---function "A.me:()V" --lazy-methods --java-threading - +--function 'A.me:()V' --lazy-methods --java-threading ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc new file mode 100644 index 00000000000..f7ae486d700 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc @@ -0,0 +1,5 @@ +CORE +A.class +--function 'A.me2:()V' --lazy-methods --java-threading +^SIGNAL=0$ +^VERIFICATION FAILED diff --git a/jbmc/regression/jbmc-concurrency/explicit_thread_blocks/test2.desc b/jbmc/regression/jbmc-concurrency/explicit_thread_blocks/test2.desc deleted file mode 100644 index 10a64a0e08b..00000000000 --- a/jbmc/regression/jbmc-concurrency/explicit_thread_blocks/test2.desc +++ /dev/null @@ -1,6 +0,0 @@ -CORE -A.class ---function "A.me2:()V" --lazy-methods --java-threading - -^SIGNAL=0$ -^VERIFICATION FAILED diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/A.class b/jbmc/regression/jbmc-concurrency/get-current-thread/A.class new file mode 100644 index 00000000000..b7af59c5440 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/get-current-thread/A.class differ diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/A.java b/jbmc/regression/jbmc-concurrency/get-current-thread/A.java new file mode 100644 index 00000000000..eb10fd5a7aa --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/get-current-thread/A.java @@ -0,0 +1,112 @@ +import java.lang.Thread; +import org.cprover.CProver; + +public class A +{ + public static int g; + + // expected verification success + public void me() + { + int g = CProver.getCurrentThreadID(); + assert(g == 0); + } + + // expected verification success + // -- + // KNOWNBUG + // --- + // For some reason symex assigns 'g' to zero, even though + // the only viable assignment should be one. + // This issue seems to only occur when a variable is + // assigned inside the local scope of a thread-block. + // + // If instead, we call a function from inside the thread-block and + // then assign 'g' to 1 then as expected the only viable + // assignment to 'g' is 1 (see 'me4') + // + // Seems related to: https://github.com/diffblue/cbmc/issues/1630/ + public void me_bug() + { + CProver.startThread(333); + int g = 1; + assert(g == 1); + CProver.endThread(333); + } + + // expected verification success + // -- + // KNOWNBUG: see me_bug() + public void me2() + { + CProver.startThread(333); + g = CProver.getCurrentThreadID(); + assert(g == 1); + CProver.endThread(333); + } + + // expected verification success + // -- + // KNOWNBUG: see me_bug() + public void me3() + { + CProver.startThread(333); + int i = CProver.getCurrentThreadID(); + assert(g == 1); + CProver.endThread(333); + } + + // expected verification success. + public void me4() + { + CProver.startThread(333); + check(); + CProver.endThread(333); + } + + // expected verification success. + public void me5() + { + me(); + B b = new B(); + Thread tmp = new Thread(b); + tmp.start(); + } + + // expected verification success. + public void me6() + { + me(); + C c = new C(); + c.start(); + } + + public void check() + { + g = CProver.getCurrentThreadID(); + assert(g == 1); + } +} + +class B implements Runnable +{ + public static int g; + @Override + public void run() + { + g = CProver.getCurrentThreadID(); + assert(g == 1); + } +} + + +class C extends Thread +{ + public static int g; + @Override + public void run() + { + g = CProver.getCurrentThreadID(); + assert(g == 1); + } +} diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/B.class b/jbmc/regression/jbmc-concurrency/get-current-thread/B.class new file mode 100644 index 00000000000..548d47f8e69 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/get-current-thread/B.class differ diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/C.class b/jbmc/regression/jbmc-concurrency/get-current-thread/C.class new file mode 100644 index 00000000000..1b5081b3c45 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/get-current-thread/C.class differ diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc new file mode 100644 index 00000000000..500630ed419 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc new file mode 100644 index 00000000000..eb912a30fe3 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test2.desc @@ -0,0 +1,9 @@ +KNOWNBUG +A.class +--function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL +-- +-- +Same bug as the one highlighted in 'test_bug.desc' diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test3.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test3.desc new file mode 100644 index 00000000000..ddf8a72a449 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test3.desc @@ -0,0 +1,9 @@ +KNOWNBUG +A.class +--function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL +-- +-- +Same bug as the one highlighted in 'test_bug.desc' diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc new file mode 100644 index 00000000000..f3bc4b1b843 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc new file mode 100644 index 00000000000..88b37371847 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me5:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc new file mode 100644 index 00000000000..7ba18d7a64e --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me6:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test_bug.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test_bug.desc new file mode 100644 index 00000000000..09ba6a5fcb0 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test_bug.desc @@ -0,0 +1,18 @@ +KNOWNBUG +A.class +--function 'A.me_bug:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL +-- +-- +For some reason symex assigns 'g' to zero, even though +the only viable assignment should be one. +This issue seems to only occur when a variable is +assigned inside the local scope of a thread-block. + +If instead, we call a function from inside the thread-block and +then assign 'g' to 1 then as expected the only viable +assignment to 'g' is 1 (see test4.desc) + +Seems related to: https://github.com/diffblue/cbmc/issues/1630/ diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/A.class b/jbmc/regression/jbmc-concurrency/java-lang-runnable/A.class new file mode 100644 index 00000000000..67d8320cfba Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/java-lang-runnable/A.class differ diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/A.java b/jbmc/regression/jbmc-concurrency/java-lang-runnable/A.java new file mode 100644 index 00000000000..b111a123a39 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/A.java @@ -0,0 +1,87 @@ +// JBMC, concurrency tests that make use of +// the java.lang.Runnable model + +import java.lang.Thread; +import org.cprover.CProver; + +public class A +{ + // calling start from outside. + // expected verfication success. + public void me3() + { + C c = new C(); + Thread tmp = new Thread(c); + tmp.start(); + c.setX(); + } + + // calling start from outside, no race-condition on B.x + // expected verfication success. + public void me4() + { + B b = new B(); + Thread tmp = new Thread(b); + tmp.start(); + } + + // expected verfication failed + public void me2() + { + B b = new B(); + b.me(); + } + + // expected verfication success. + public void me() + { + C c = new C(); + c.me(); + } +} + +class B implements Runnable +{ + int x = 0; + + @Override + public void run() + { + x = 44; + int local_x = x; + assert(local_x == 44); + } + + public void me() + { + Thread tmp = new Thread(this); + tmp.start(); + x = 10; + } +} + + +class C implements Runnable +{ + int x = 0; + + @Override + public void run() + { + x = 44; + int local_x = x; + assert(local_x == 44 || x == 10); + } + + public void me() + { + Thread tmp = new Thread(this); + tmp.start(); + setX(); + } + + public void setX() + { + x = 10; + } +} diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/B.class b/jbmc/regression/jbmc-concurrency/java-lang-runnable/B.class new file mode 100644 index 00000000000..f7dcdd34d57 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/java-lang-runnable/B.class differ diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/C.class b/jbmc/regression/jbmc-concurrency/java-lang-runnable/C.class new file mode 100644 index 00000000000..765482752bb Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/java-lang-runnable/C.class differ diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc new file mode 100644 index 00000000000..95ec31a0c1f --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc new file mode 100644 index 00000000000..4ba443c769d --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc @@ -0,0 +1,5 @@ +CORE +A.class +--function 'A.me2:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading +^SIGNAL=0$ +^VERIFICATION FAILED diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc new file mode 100644 index 00000000000..248eae75e64 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me4:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc new file mode 100644 index 00000000000..3db62d553c4 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me3:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/A.class b/jbmc/regression/jbmc-concurrency/java-lang-thread/A.class new file mode 100644 index 00000000000..033ac003821 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/java-lang-thread/A.class differ diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/A.java b/jbmc/regression/jbmc-concurrency/java-lang-thread/A.java new file mode 100644 index 00000000000..5ff394caf12 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/java-lang-thread/A.java @@ -0,0 +1,87 @@ +// JBMC, concurrency tests that make use of +// the java.lang.Thread model + +import java.lang.Thread; +import org.cprover.CProver; + +public class A +{ + // calling start from outside, no race-condition on B.x + // expected verfication success. + public void me4() + { + B b = new B(); + Thread tmp = new Thread(b); + tmp.start(); + } + + // calling start from outside. + // expected verfication success. + public void me3() + { + C c = new C(); + Thread tmp = new Thread(c); + tmp.start(); + c.setX(); + } + + // expected verfication failed + public void me2() + { + B b = new B(); + b.me(); + } + + // expected verfication success. + public void me() + { + C c = new C(); + c.me(); + } +} + +class B extends Thread +{ + int x = 0; + + @Override + public void run() + { + x = 44; + int local_x = x; + assert(local_x == 44); + } + + public void me() + { + Thread tmp = new Thread(this); + tmp.start(); + x = 10; + } +} + + +class C extends Thread +{ + int x = 0; + + @Override + public void run() + { + x = 44; + int local_x = x; + assert(local_x == 44 || x == 10); + } + + public void me() + { + Thread tmp = new Thread(this); + tmp.start(); + setX(); + } + + public void setX() + { + x = 10; + } +} diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/B.class b/jbmc/regression/jbmc-concurrency/java-lang-thread/B.class new file mode 100644 index 00000000000..a0592c07cea Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/java-lang-thread/B.class differ diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/C.class b/jbmc/regression/jbmc-concurrency/java-lang-thread/C.class new file mode 100644 index 00000000000..48a26c48bac Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/java-lang-thread/C.class differ diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc new file mode 100644 index 00000000000..f28b716eea4 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc new file mode 100644 index 00000000000..29e9ced78d0 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc @@ -0,0 +1,5 @@ +CORE +A.class +--function 'A.me2:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading +^SIGNAL=0$ +^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc new file mode 100644 index 00000000000..2ba7df863b5 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading --lazy-methods +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc new file mode 100644 index 00000000000..ad3b3639ce5 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading --lazy-methods +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ diff --git a/jbmc/regression/jbmc-concurrency/several-threads/A.class b/jbmc/regression/jbmc-concurrency/several-threads/A.class new file mode 100644 index 00000000000..6e8378318ac Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/several-threads/A.class differ diff --git a/jbmc/regression/jbmc-concurrency/several-threads/A.java b/jbmc/regression/jbmc-concurrency/several-threads/A.java new file mode 100644 index 00000000000..251bf20cd80 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/several-threads/A.java @@ -0,0 +1,102 @@ +import java.lang.Thread; +import org.cprover.CProver; + +public class A +{ + // expected verification success + public static void me() + { + B b = new B(); + b.me(); + } + + // expected verification failure + public static void me2() + { + C c = new C(); + c.me(); + } + + // Create 2 Threads, no shared variables + // expected verification success + // + // FIXME: attempting to create more threads will + // currently result in an exponential blow-up + // in the number of clauses. + public void me3() + { + for(int i = 0; i<2; i++) + { + D d = new D(); + d.start(); + d.setX(); + } + } +} + +class D extends Thread +{ + int x = 0; + + @Override + public void run() + { + x = 44; + int local_x = x; + assert(local_x == 44 || local_x == 10); + } + public void setX() + { + x = 10; + } +} + +class B implements Runnable +{ + // FIXME: this assertion does not always hold as per the java spec (because x + // is not volatile), but cbmc currently doesn't reason about java volatile + // variables + int x = 0; + @Override + public void run() + { + x += 1; + int local_x = x; + assert(local_x == 1 || local_x == 2 || + local_x == 10 || local_x == 11 || local_x == 12); + } + + // verification success + public void me() + { + Thread t1 = new Thread(this); + t1.start(); + Thread t2 = new Thread(this); + t2.start(); + x = 10; + } +} + +class C implements Runnable +{ + int x = 0; + + @Override + public void run() + { + x += 1; + int local_x = x; + assert(local_x == 1 || local_x == 2); + } + + // verification fails because the assertion does not account for the writes of + // this thread + public void me() + { + Thread t1 = new Thread(this); + t1.start(); + Thread t2 = new Thread(this); + t2.start(); + x = 10; + } +} diff --git a/jbmc/regression/jbmc-concurrency/several-threads/B.class b/jbmc/regression/jbmc-concurrency/several-threads/B.class new file mode 100644 index 00000000000..b78ce261012 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/several-threads/B.class differ diff --git a/jbmc/regression/jbmc-concurrency/several-threads/C.class b/jbmc/regression/jbmc-concurrency/several-threads/C.class new file mode 100644 index 00000000000..87f9d7521cb Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/several-threads/C.class differ diff --git a/jbmc/regression/jbmc-concurrency/several-threads/D.class b/jbmc/regression/jbmc-concurrency/several-threads/D.class new file mode 100644 index 00000000000..7fb115f89a5 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/several-threads/D.class differ diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test.desc b/jbmc/regression/jbmc-concurrency/several-threads/test.desc new file mode 100644 index 00000000000..ffdd51daf44 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/several-threads/test.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function A.me --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test2.desc b/jbmc/regression/jbmc-concurrency/several-threads/test2.desc new file mode 100644 index 00000000000..cdf16ddd945 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/several-threads/test2.desc @@ -0,0 +1,5 @@ +CORE +A.class +--function A.me2 --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading +^SIGNAL=0$ +^VERIFICATION FAILED$ diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test3.desc b/jbmc/regression/jbmc-concurrency/several-threads/test3.desc new file mode 100644 index 00000000000..71b16a75d28 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/several-threads/test3.desc @@ -0,0 +1,6 @@ +CORE +A.class +--function A.me3 --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --java-threading --unwind 3 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/Sync.class b/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/Sync.class new file mode 100644 index 00000000000..97d5db1f4d5 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/Sync.class differ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/Sync.j b/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/Sync.j new file mode 100644 index 00000000000..313a722565c --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/Sync.j @@ -0,0 +1,23 @@ +.class public Sync +.super java/lang/Object + +.method public ()V + aload_0 + invokenonvirtual java/lang/Object/()V + return +.end method + +.method public f()V +Start: + aload_0 + monitorexit +End: + new java/lang/AssertionError + dup + invokespecial java/lang/AssertionError/()V + athrow + return +Handle: + return +.catch java/lang/IllegalMonitorStateException from Start to End using Handle +.end method diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc new file mode 100644 index 00000000000..67a22ad6437 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks-illegal-state/test.desc @@ -0,0 +1,13 @@ +KNOWNBUG +Sync.class +--lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Note: requires jasmin to compile the bytecode instructions +This checks that an extra monitorexit will always trigger an IllegalMonitorException. + +This is currently not working as explicit throws have been removed from the underlying model due to performance considerations. diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/Sync.class b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/Sync.class new file mode 100644 index 00000000000..4dc0adc576b Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/Sync.class differ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/Sync.java b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/Sync.java new file mode 100644 index 00000000000..b1a7bebbf7e --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/Sync.java @@ -0,0 +1,12 @@ +public class Sync { + public static void main(String[] args) { + final Object o=null; + try { + synchronized (o) {} + assert false; + } + catch (NullPointerException e) { + return; + } + } +} diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc new file mode 100644 index 00000000000..70f7c5ebd89 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks-null-throw/test.desc @@ -0,0 +1,10 @@ +KNOWNBUG +Sync.class +--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +This checks that the synchronized keyword on a null object will always throw. + +This is currently not working as explicit throws have been removed from the underlying model due to performance considerations. diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/Sync.class b/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/Sync.class new file mode 100644 index 00000000000..c8ed02a21e2 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/Sync.class differ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/Sync.java b/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/Sync.java new file mode 100644 index 00000000000..3496ab7714f --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/Sync.java @@ -0,0 +1,35 @@ +import org.cprover.CProver; + +public class Sync +{ + int field; + public static void main(String[] args) + { + Sync o = new Sync(); + try + { + o.field=0; + synchronized (o) + { + // Make sure the monitor is taken. + assert(CProver.getMonitorCount(o) == 1); + if (CProver.nondetBoolean()) + throw new RuntimeException(); + o.field++; + } + } + catch(RuntimeException e) + { + o.field++; + } + catch(Throwable e) + {} + + // Make sure we did not execute in an unexpected way. + if (o.field != 1) + assert false; + + // Make sure the monitor is free. + assert(CProver.getMonitorCount(o) == 0); + } +} diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc new file mode 100644 index 00000000000..161c0d0e8b2 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks-throw/test.desc @@ -0,0 +1,10 @@ +KNOWNBUG +Sync.class +--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +-- +Checks all possible paths to ensure monitorexit is executed even after a throw. + +This is currently not working as explicit throws have been removed from the underlying model due to performance considerations. diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/A.class b/jbmc/regression/jbmc-concurrency/synchronized-blocks/A.class new file mode 100644 index 00000000000..b8b5fa6d05e Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/synchronized-blocks/A.class differ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/A.java b/jbmc/regression/jbmc-concurrency/synchronized-blocks/A.java new file mode 100644 index 00000000000..2b4ac81400d --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/A.java @@ -0,0 +1,60 @@ +public class A +{ + public void me0() + { + final Object o = new Object(); + try + { + synchronized (o) {} + } + catch (NullPointerException e) + { + assert false; + return; + } + } + + // expected verification success + // -- + // base-case, no synchronization + public void me1() + { + B t = new B(); + t.shared = 5; + t.start(); + assert(t.shared == 5 || t.shared == 6); + } + + // expected verification success + // -- + // locking mechanism + public void me2() + { + B t = new B(); + synchronized(t.lock) + { + t.shared = 5; + t.start(); + assert(t.shared == 5); + } + } +} + +class B extends Thread +{ + public Object lock = new Object(); + public int shared = 0; + + @Override + public void run() + { + set(); + } + public void set() + { + synchronized(lock) + { + shared++; + } + } +} diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/B.class b/jbmc/regression/jbmc-concurrency/synchronized-blocks/B.class new file mode 100644 index 00000000000..62a64a5c829 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/synchronized-blocks/B.class differ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test.desc new file mode 100644 index 00000000000..7b00c254ec0 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test.desc @@ -0,0 +1,9 @@ +CORE +A.class +--function 'A.me0:()V' --lazy-methods +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Tests that synchronization blocks do not cause issues when the java core models library is not loaded diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc new file mode 100644 index 00000000000..cdc51533471 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc @@ -0,0 +1,7 @@ +CORE +A.class +--function 'A.me0:()V' --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions +ATOMIC_BEGIN +ATOMIC_END +-- +-- diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc new file mode 100644 index 00000000000..228f2385c1a --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc @@ -0,0 +1,8 @@ +CORE +A.class +--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc new file mode 100644 index 00000000000..cb79b066cca --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc @@ -0,0 +1,8 @@ +CORE +A.class +--function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc new file mode 100644 index 00000000000..9db7060779c --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc @@ -0,0 +1,8 @@ +CORE +A.class +--function 'A.me2:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc new file mode 100644 index 00000000000..5a49dc43ea9 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc @@ -0,0 +1,8 @@ +CORE +A.class +--function 'A.me1:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/Sync.class b/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/Sync.class new file mode 100644 index 00000000000..68926d9f5d8 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/Sync.class differ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/Sync.java b/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/Sync.java new file mode 100644 index 00000000000..5fc551d3b64 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/Sync.java @@ -0,0 +1,45 @@ +import java.lang.RuntimeException; +import org.cprover.CProver; + +public class Sync +{ + public int field; + + public static void main(String[] args) + { + final Sync o = new Sync(); + o.field = 0; + // test regular synchronized method (monitorexit on return) + o.f(); + // test synchronized method with throw (monitorexit on catch) + try + { + o.g(); + } + catch (RuntimeException e) + { + o.field++; + } + // Make sure both functions were executed and the second threw + // The object should remain unlocked + if ((o.field !=3) || (CProver.getMonitorCount(o) !=0)) + assert(false); + } + + public synchronized void f() + { + // Check that we acquired the lock + if (CProver.getMonitorCount(this) !=1) + assert(false); + field++; + } + + public synchronized void g() + { + field++; + // Check that we acquired the lock + if (CProver.getMonitorCount(this) !=1) + assert(false); + throw new RuntimeException(); + } +} diff --git a/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc new file mode 100644 index 00000000000..0f19f7ef937 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc @@ -0,0 +1,10 @@ +CORE +Sync.class +--cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --lazy-methods --java-threading +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring +-- +Checks all possible paths to ensure a synchronized method does not end in an illegal monitor state. diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/A.class b/jbmc/regression/jbmc-concurrency/synchronized-methods/A.class new file mode 100644 index 00000000000..5be68554423 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/synchronized-methods/A.class differ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/A.java b/jbmc/regression/jbmc-concurrency/synchronized-methods/A.java new file mode 100644 index 00000000000..5f42a4887af --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/A.java @@ -0,0 +1,80 @@ +public class A +{ + static int g; + + public synchronized void me1() + { + g = 0; + } + + // expected verification success + // -- + // base-case, no synchronization + public void me2() + { + B t = new B(); + t.shared = 5; + t.start(); + assert(t.shared == 5 || t.shared == 6); + } + + // expected verification success + // -- + // locking mechanism + public void me3() + { + B t = new B(); + synchronized(t) + { + t.shared = 5; + t.start(); + assert(t.shared == 5); + } + } + + // expected verification success + // -- + // KNOWNBUG: synchronization of static synchronized + // methods is not yet supported + public void me4() + { + C t = new C(); + synchronized(C.class) + { + C.shared = 5; + t.start(); + assert(C.shared == 5); + } + } +} + +class B extends Thread +{ + public int shared = 0; + + @Override + public void run() + { + set(); + } + public synchronized void set() + { + shared++; + } +} + +class C extends Thread +{ + public static int shared = 0; + + @Override + public void run() + { + C.static_set(); + } + + public static synchronized void static_set() + { + C.shared++; + } +} diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/B.class b/jbmc/regression/jbmc-concurrency/synchronized-methods/B.class new file mode 100644 index 00000000000..6e34cf16cf7 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/synchronized-methods/B.class differ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/C.class b/jbmc/regression/jbmc-concurrency/synchronized-methods/C.class new file mode 100644 index 00000000000..6438f07e4a9 Binary files /dev/null and b/jbmc/regression/jbmc-concurrency/synchronized-methods/C.class differ diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc new file mode 100644 index 00000000000..3f672821a9f --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc @@ -0,0 +1,7 @@ +CORE +A.class +--function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions --lazy-methods +ATOMIC_BEGIN +ATOMIC_END +-- +-- diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc new file mode 100644 index 00000000000..9ac158bd5e6 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc @@ -0,0 +1,8 @@ +CORE +A.class +--function 'A.me1:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` --show-goto-functions +ATOMIC_BEGIN +ATOMIC_END +-- +-- +Making sure that monitorEnter and monitorExit are not removed by lazy-methods diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc new file mode 100644 index 00000000000..5931228cfa1 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc @@ -0,0 +1,8 @@ +CORE +A.class +--function 'A.me1:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL +-- +-- diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc new file mode 100644 index 00000000000..a4e95fbedeb --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc @@ -0,0 +1,8 @@ +CORE +A.class +--function 'A.me3:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc new file mode 100644 index 00000000000..9db7060779c --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc @@ -0,0 +1,8 @@ +CORE +A.class +--function 'A.me2:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_static.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_static.desc new file mode 100644 index 00000000000..c9301aa8459 --- /dev/null +++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_static.desc @@ -0,0 +1,9 @@ +KNOWNBUG +A.class +--function 'A.me4:()V' --java-threading --lazy-methods --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar` +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +-- +Synchronization of static synchronized methods is not yet supported. diff --git a/jbmc/regression/jbmc/json_trace2/test.desc b/jbmc/regression/jbmc/json_trace2/test.desc index 13d8774fb25..390b8c6d3d3 100644 --- a/jbmc/regression/jbmc/json_trace2/test.desc +++ b/jbmc/regression/jbmc/json_trace2/test.desc @@ -5,6 +5,6 @@ activate-multi-line-match EXIT=0 SIGNAL=0 "outputID": "return",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "output",\n *"thread": 0,\n *"values": \[\n *\{\n *"binary": "00000000",\n *"data": "false",\n *"name": "integer",\n *"type": "boolean",\n *"width": 8 -"inputID": "arg1a",\n *"internal": true,\n *"mode": "java",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "input",\n *"thread": 0,\n *"values": \[\n *\{\n *"data": "null",\n *"name": "pointer",\n *"type": "struct java\.lang\.Object \{ __CPROVER_string @class_identifier; boolean @lock; \} \*" +"inputID": "arg1a",\n *"internal": true,\n *"mode": "java",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "input",\n *"thread": 0,\n *"values": \[\n *\{\n *"data": "null",\n *"name": "pointer",\n *"type": "struct java\.lang\.Object \{ __CPROVER_string @class_identifier; \} \*" -- ^warning: ignoring diff --git a/jbmc/regression/jbmc/overlay-class/correct-test.desc b/jbmc/regression/jbmc/overlay-class/correct-test.desc index fea8647abf4..ecde48e8a55 100644 --- a/jbmc/regression/jbmc/overlay-class/correct-test.desc +++ b/jbmc/regression/jbmc/overlay-class/correct-test.desc @@ -1,6 +1,6 @@ CORE Test.class ---classpath `./format_classpath.sh . annotations correct-overlay` --verbosity 10 +--classpath `../../../../scripts/format_classpath.sh . annotations correct-overlay` --verbosity 10 ^Getting class `Test' from file \.[\\/]Test\.class$ ^Getting class `Test' from file correct-overlay[\\/]Test\.class$ ^Adding symbol from overlay class: field 'x'$ diff --git a/jbmc/regression/jbmc/overlay-class/duplicate-test.desc b/jbmc/regression/jbmc/overlay-class/duplicate-test.desc index 1ac968acb9c..2bfce7a5ca3 100644 --- a/jbmc/regression/jbmc/overlay-class/duplicate-test.desc +++ b/jbmc/regression/jbmc/overlay-class/duplicate-test.desc @@ -1,6 +1,6 @@ CORE Test.class ---classpath `./format_classpath.sh . annotations . correct-overlay` --verbosity 10 +--classpath `../../../../scripts/format_classpath.sh . annotations . correct-overlay` --verbosity 10 ^Getting class `Test' from file \.[\\/]Test\.class$ ^Getting class `Test' from file correct-overlay[\\/]Test\.class$ ^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$ diff --git a/jbmc/regression/jbmc/overlay-class/misordered-test.desc b/jbmc/regression/jbmc/overlay-class/misordered-test.desc index acd447a376f..6505d5449d1 100644 --- a/jbmc/regression/jbmc/overlay-class/misordered-test.desc +++ b/jbmc/regression/jbmc/overlay-class/misordered-test.desc @@ -1,6 +1,6 @@ CORE Test.class ---classpath `./format_classpath.sh annotations correct-overlay .` --verbosity 10 +--classpath `../../../../scripts/format_classpath.sh annotations correct-overlay .` --verbosity 10 ^Getting class `Test' from file correct-overlay[\\/]Test\.class$ ^Getting class `Test' from file \.[\\/]Test\.class$ ^Skipping class Test marked with OverlayClassImplementation but found before original definition$ diff --git a/jbmc/regression/jbmc/overlay-class/unmarked-test.desc b/jbmc/regression/jbmc/overlay-class/unmarked-test.desc index 915f857fb87..cbf0430a3a6 100644 --- a/jbmc/regression/jbmc/overlay-class/unmarked-test.desc +++ b/jbmc/regression/jbmc/overlay-class/unmarked-test.desc @@ -1,6 +1,6 @@ CORE Test.class ---classpath `./format_classpath.sh . annotations unmarked-overlay` --verbosity 10 +--classpath `../../../../scripts/format_classpath.sh . annotations unmarked-overlay` --verbosity 10 ^Getting class `Test' from file \.[\\/]Test\.class$ ^Getting class `Test' from file unmarked-overlay[\\/]Test\.class$ ^Skipping duplicate definition of class Test not marked with OverlayClassImplementation$ diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile index df1511612ce..c3964a40375 100644 --- a/jbmc/src/java_bytecode/Makefile +++ b/jbmc/src/java_bytecode/Makefile @@ -8,7 +8,7 @@ SRC = bytecode_info.cpp \ jar_file.cpp \ java_bytecode_convert_class.cpp \ java_bytecode_convert_method.cpp \ - java_bytecode_convert_threadblock.cpp \ + java_bytecode_concurrency_instrumentation.cpp \ java_bytecode_instrument.cpp \ java_bytecode_internal_additions.cpp \ java_bytecode_language.cpp \ diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_threadblock.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp similarity index 58% rename from jbmc/src/java_bytecode/java_bytecode_convert_threadblock.cpp rename to jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp index 13e6c43894d..7f37854913f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_threadblock.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp @@ -6,7 +6,7 @@ Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com \*******************************************************************/ -#include "java_bytecode_convert_threadblock.h" +#include "java_bytecode_concurrency_instrumentation.h" #include "expr2java.h" #include "java_types.h" @@ -14,6 +14,7 @@ Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com #include #include #include +#include #include // Disable linter to allow an std::string constant. @@ -38,7 +39,7 @@ static symbolt add_or_get_symbol( const bool is_thread_local, const bool is_static_lifetime) { - const symbolt* psymbol = nullptr; + const symbolt *psymbol = nullptr; namespacet ns(symbol_table); ns.lookup(name, psymbol); if(psymbol != nullptr) @@ -89,6 +90,186 @@ static const std::string get_thread_block_identifier( return integer2string(lbl_id); } +/// Creates a monitorenter/monitorexit code_function_callt for +/// the given synchronization object. +/// \param symbol_table: a symbol table +/// \param is_enter: indicates whether we are creating a monitorenter or +/// monitorexit. +/// \param object: expression representing a 'java.Lang.Object'. This object is +/// used to achieve object-level locking by calling monitoroenter/monitorexit. +static codet get_monitor_call( + const symbol_tablet &symbol_table, + bool is_enter, + const exprt &object) +{ + const irep_idt symbol = + is_enter ? "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" + : "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V"; + + auto it = symbol_table.symbols.find(symbol); + + // If the 'java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V' or + // 'java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V' method is not + // found symex will rightfully complain as it cannot find the symbol + // associated with the method in question. To avoid this and thereby ensuring + // JBMC works both with and without the models, we replace the aforementioned + // methods with skips when we cannot find them. + // + // Note: this can only happen if the java-core-models library is not loaded. + // + // Note': we explicitly prevent JBMC from stubbing these methods. + if(it == symbol_table.symbols.end()) + return code_skipt(); + + // Otherwise we create a function call + code_function_callt call; + call.function() = symbol_exprt(symbol, it->second.type); + call.lhs().make_nil(); + call.arguments().push_back(object); + return call; +} + +/// Introduces a monitorexit before every return recursively. +/// Note: this breaks sharing on \p code +/// \param [out] code: current element to modify +/// \param monitorexit: codet to insert before the return +static void monitor_exits(codet &code, const codet &monitorexit) +{ + const irep_idt &statement = code.get_statement(); + if(statement == ID_return) + { + // Replace the return with a monitor exit plus return block + code_blockt return_block; + return_block.add(monitorexit); + return_block.move_to_operands(code); + code = return_block; + } + else if( + statement == ID_label || statement == ID_block || + statement == ID_decl_block) + { + // If label or block found, explore the code inside the block + Forall_operands(it, code) + { + codet &sub_code = to_code(*it); + monitor_exits(sub_code, monitorexit); + } + } +} + +/// Transforms the codet stored in \c symbol.value. The \p symbol is expected to +/// be a Java synchronized method. Java synchronized methods do not have +/// explicit calls to the instructions monitorenter and monitorexit, the JVM +/// interprets the synchronized flag in a method and uses monitor of the object +/// to implement locking and unlocking. Therefore JBMC has to emulate this same +/// behavior. We insert a call to our model of monitorenter at the beginning of +/// the method and calls to our model of monitorexit at each return instruction. +/// We wrap the entire body of the method with an exception handler that will +/// call our model of monitorexit if the method returns exceptionally. +/// +/// Example: +/// +/// \code +/// synchronized int amethod(int p) +/// { +/// int x = 0; +/// if(p == 0) +/// return -1; +/// x = p / 10 +/// return x +/// } +/// \endcode +/// +/// Is transformed into the codet equivalent of: +/// +/// \code +/// synchronized int amethod(int p) +/// { +/// try +/// { +/// java::java.lang.Object.monitorenter(this); +/// int x = 0; +/// if(p == 0) +/// { +/// java::java.lang.Object.monitorexit(this); +/// return -1; +/// } +/// java::java.lang.Object.monitorexit(this); +/// return x +/// } +/// catch(java::java.lang.Throwable e) +/// { +/// // catch every exception, including errors! +/// java::java.lang.Object.monitorexit(this); +/// throw e; +/// } +/// } +/// \endcode +/// +/// \param symbol_table: a symbol_table +/// \param symbol: writeable symbol hosting code to synchronize +/// \param sync_object: object to use as a lock +static void instrument_synchronized_code( + symbol_tablet &symbol_table, + symbolt &symbol, + const exprt &sync_object) +{ + PRECONDITION(!symbol.type.get_bool(ID_is_static)); + + codet &code = to_code(symbol.value); + + // Get the calls to the functions that implement the critical section + codet monitorenter = get_monitor_call(symbol_table, true, sync_object); + codet monitorexit = get_monitor_call(symbol_table, false, sync_object); + + // Create a unique catch label and empty throw type (i.e. any) + // and catch-push them at the beginning of the code (i.e. begin try) + code_push_catcht catch_push; + irep_idt handler("pc-synchronized-catch"); + irep_idt exception_id; + code_push_catcht::exception_listt &exception_list = + catch_push.exception_list(); + exception_list.push_back( + code_push_catcht::exception_list_entryt(exception_id, handler)); + + // Create a catch-pop to indicate the end of the try block + code_pop_catcht catch_pop; + + // Create the finally block with the same label targeted in the catch-push + const symbolt &tmp_symbol = get_fresh_aux_symbol( + java_reference_type(symbol_typet("java::java.lang.Throwable")), + id2string(symbol.name), + "caught-synchronized-exception", + code.source_location(), + ID_java, + symbol_table); + symbol_exprt catch_var(tmp_symbol.name, tmp_symbol.type); + catch_var.set(ID_C_base_name, tmp_symbol.base_name); + code_landingpadt catch_statement(catch_var); + codet catch_instruction = catch_statement; + code_labelt catch_label(handler, code_blockt()); + code_blockt &catch_block = to_code_block(catch_label.code()); + catch_block.add(catch_instruction); + catch_block.add(monitorexit); + + // Re-throw exception + side_effect_expr_throwt throw_expr; + throw_expr.copy_to_operands(catch_var); + catch_block.add(code_expressiont(throw_expr)); + + // Write a monitorexit before every return + monitor_exits(code, monitorexit); + + // Wrap the code into a try finally + code_blockt try_block; + try_block.move_to_operands(monitorenter); + try_block.move_to_operands(catch_push); + try_block.move_to_operands(code); + try_block.move_to_operands(catch_pop); + try_block.move_to_operands(catch_label); + code = try_block; +} + /// Transforms the codet stored in in \p f_code, which is a call to function /// CProver.startThread:(I)V into a block of code as described by the /// documentation of function convert_thread_block @@ -284,20 +465,20 @@ static void instrument_getCurrentThreadID( /// /// Note': the ID of the thread is assigned after the thread is created, this /// creates bogus interleavings. Currently, it's not possible to -/// assign the thread ID before the creation of the thead, due to a bug in +/// assign the thread ID before the creation of the thread, due to a bug in /// symex. See https://github.com/diffblue/cbmc/issues/1630/for more details. /// /// \param symbol_table: a symbol table void convert_threadblock(symbol_tablet &symbol_table) { using instrument_callbackt = - std::function; + std::function; using expr_replacement_mapt = - std::unordered_map; + std::unordered_map; namespacet ns(symbol_table); - for(auto entry : symbol_table) + for(const auto &entry : symbol_table) { expr_replacement_mapt expr_replacement_map; const symbolt &symbol = entry.second; @@ -361,3 +542,75 @@ void convert_threadblock(symbol_tablet &symbol_table) } } } + +/// Iterate through the symbol table to find and instrument synchronized +/// methods. +/// +/// Synchronized methods make it impossible for two invocations of the same +/// method on the same object to interleave. In-order to replicate +/// these semantics a call to +/// "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" and +/// "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V" is instrumented +/// at the start and end of the method. Note, that the former is instrumented +/// at every statement where the execution can exit the method in question. +/// Specifically, out of order return statements and exceptions. The latter +/// is dealt with by instrumenting a try catch block. +/// +/// Note: Static synchronized methods are not supported yet as the +/// synchronization semantics for static methods is different (locking on the +/// class instead the of the object). Upon encountering a static synchronized +/// method the current implementation will ignore the synchronized flag. +/// (showing a warning in the process). This may result in superfluous +/// interleavings. +/// +/// Note': This method requires the availability of +/// "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" and +/// "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V". +/// (java-library-models). If they are not available code_skipt will inserted +/// instead of calls to the aforementioned methods. +/// +/// \param symbol_table: a symbol table +/// \param message_handler: status output +void convert_synchronized_methods( + symbol_tablet &symbol_table, + message_handlert &message_handler) +{ + namespacet ns(symbol_table); + for(const auto &entry : symbol_table) + { + const symbolt &symbol = entry.second; + + if(symbol.type.id() != ID_code) + continue; + if(symbol.value.is_nil()) + continue; + if(!symbol.type.get_bool(ID_is_synchronized)) + continue; + + if(symbol.type.get_bool(ID_is_static)) + { + messaget message(message_handler); + message.warning() << "Java method '" << entry.first + << "' is static and synchronized." + << " This is unsupported, the synchronized keyword" + << " will be ignored." + << messaget::eom; + continue; + } + + // find the object to synchronize on + const irep_idt this_id(id2string(symbol.name) + "::this"); + exprt this_expr(this_id); + + auto it = symbol_table.symbols.find(this_id); + + if(it == symbol_table.symbols.end()) + // failed to find object to synchronize on + continue; + + // get writeable reference and instrument the method + symbolt &w_symbol = symbol_table.get_writeable_ref(entry.first); + instrument_synchronized_code( + symbol_table, w_symbol, it->second.symbol_expr()); + } +} diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_threadblock.h b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.h similarity index 53% rename from jbmc/src/java_bytecode/java_bytecode_convert_threadblock.h rename to jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.h index ef02f92b79e..a757e400370 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_threadblock.h +++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.h @@ -5,11 +5,15 @@ Module: Java Convert Thread blocks Author: Kurt Degiogrio, kurt.degiorgio@diffblue.com \*******************************************************************/ -#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_THREADBLOCK_H -#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_THREADBLOCK_H +#ifndef CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONCURRENCY_INSTRUMENTATION_H +#define CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONCURRENCY_INSTRUMENTATION_H #include +#include void convert_threadblock(symbol_tablet &symbol_table); +void convert_synchronized_methods( + symbol_tablet &symbol_table, + message_handlert &message_handler); #endif diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 7829d813b08..3c284340085 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -366,6 +366,11 @@ void java_bytecode_convert_method_lazy( else member_type.set_access(ID_default); + if(m.is_synchronized) + member_type.set(ID_is_synchronized, true); + if(m.is_static) + member_type.set(ID_is_static, true); + // do we need to add 'this' as a parameter? if(!m.is_static) { @@ -1021,6 +1026,8 @@ codet java_bytecode_convert_methodt::convert_instructions( } if(i_it->statement=="athrow" || + i_it->statement=="monitorenter" || + i_it->statement=="monitorexit" || i_it->statement=="putfield" || i_it->statement=="getfield" || i_it->statement=="checkcast" || @@ -1246,6 +1253,20 @@ codet java_bytecode_convert_methodt::convert_instructions( "function expected to have exactly one parameter"); c = replace_call_to_cprover_assume(i_it->source_location, c); } + // replace calls to CProver.atomicBegin + else if(statement == "invokestatic" && + arg0.get(ID_identifier) == + "java::org.cprover.CProver.atomicBegin:()V") + { + c = codet(ID_atomic_begin); + } + // replace calls to CProver.atomicEnd + else if(statement == "invokestatic" && + arg0.get(ID_identifier) == + "java::org.cprover.CProver.atomicEnd:()V") + { + c = codet(ID_atomic_end); + } else if(statement=="invokeinterface" || statement=="invokespecial" || statement=="invokevirtual" || @@ -1634,13 +1655,9 @@ codet java_bytecode_convert_methodt::convert_instructions( results[0]= binary_predicate_exprt(op[0], ID_java_instanceof, arg0); } - else if(statement=="monitorenter") + else if(statement == "monitorenter" || statement == "monitorexit") { - c = convert_monitorenter(i_it->source_location, op); - } - else if(statement=="monitorexit") - { - c = convert_monitorexit(i_it->source_location, op); + c = convert_monitorenterexit(statement, op, i_it->source_location); } else if(statement=="swap") { @@ -1960,6 +1977,29 @@ codet java_bytecode_convert_methodt::convert_switch( return code_switch; } +codet java_bytecode_convert_methodt::convert_monitorenterexit( + const irep_idt &statement, + const exprt::operandst &op, + const source_locationt &source_location) +{ + const irep_idt descriptor = (statement == "monitorenter") ? + "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" : + "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V"; + + // becomes a function call + code_typet type( + {code_typet::parametert(java_reference_type(void_typet()))}, + void_typet()); + code_function_callt call; + call.function() = symbol_exprt(descriptor, type); + call.lhs().make_nil(); + call.arguments().push_back(op[0]); + call.add_source_location() = source_location; + if(needed_lazy_methods && symbol_table.has_symbol(descriptor)) + needed_lazy_methods->add_needed_method(descriptor); + return call; +} + void java_bytecode_convert_methodt::convert_dup2( exprt::operandst &op, exprt::operandst &results) @@ -2399,38 +2439,6 @@ codet &java_bytecode_convert_methodt::do_exception_handling( return c; } -codet java_bytecode_convert_methodt::convert_monitorexit( - const source_locationt &location, - const exprt::operandst &op) const -{ - code_typet type; - type.return_type() = void_typet(); - type.parameters().resize(1); - type.parameters()[0].type() = java_reference_type(void_typet()); - code_function_callt call; - call.function() = symbol_exprt("java::monitorexit", type); - call.lhs().make_nil(); - call.arguments().push_back(op[0]); - call.add_source_location() = location; - return call; -} - -codet java_bytecode_convert_methodt::convert_monitorenter( - const source_locationt &location, - const exprt::operandst &op) const -{ - code_typet type; - type.return_type() = void_typet(); - type.parameters().resize(1); - type.parameters()[0].type() = java_reference_type(void_typet()); - code_function_callt call; - call.function() = symbol_exprt("java::monitorenter", type); - call.lhs().make_nil(); - call.arguments().push_back(op[0]); - call.add_source_location() = location; - return call; -} - void java_bytecode_convert_methodt::convert_multianewarray( const source_locationt &location, const exprt &arg0, diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h index 6e2975ed337..4cb7ca0183b 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method_class.h @@ -420,14 +420,6 @@ class java_bytecode_convert_methodt:public messaget codet &c, exprt::operandst &results); - codet convert_monitorenter( - const source_locationt &location, - const exprt::operandst &op) const; - - codet convert_monitorexit( - const source_locationt &location, - const exprt::operandst &op) const; - codet &do_exception_handling( const methodt &method, const std::set &working_set, @@ -446,6 +438,11 @@ class java_bytecode_convert_methodt:public messaget codet &c, exprt::operandst &results) const; + codet convert_monitorenterexit( + const irep_idt &statement, + const exprt::operandst &op, + const source_locationt &source_location); + codet &replace_call_to_cprover_assume(source_locationt location, codet &c); void convert_invoke( diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index aa88a8c19ac..5c15f43abee 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -22,9 +22,9 @@ Author: Daniel Kroening, kroening@kroening.com #include +#include "java_bytecode_concurrency_instrumentation.h" #include "java_bytecode_convert_class.h" #include "java_bytecode_convert_method.h" -#include "java_bytecode_convert_threadblock.h" #include "java_bytecode_internal_additions.h" #include "java_bytecode_instrument.h" #include "java_bytecode_typecheck.h" @@ -755,9 +755,12 @@ bool java_bytecode_languaget::typecheck( bool res = java_bytecode_typecheck( symbol_table, get_message_handler(), string_refinement_enabled); - // now instrument thread-blocks + // now instrument thread-blocks and synchronized methods. if(threading_support) + { convert_threadblock(symbol_table); + convert_synchronized_methods(symbol_table, get_message_handler()); + } return res; } diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index d4af87e9637..bba09f713f9 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -536,7 +536,7 @@ static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size) /// cprover_associate_length_to_array_func( /// *string_data_pointer, tmp_object_factory); /// arg = { .@java.lang.Object={ -/// .@class_identifier=\"java::java.lang.String\", .@lock=false }, +/// .@class_identifier=\"java::java.lang.String\" }, /// .length=tmp_object_factory, /// .data=*string_data_pointer }; /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -570,11 +570,10 @@ codet initialize_nondet_string_struct( ? "java::java.lang.String" : "java::" + id2string(struct_type.get_tag()); - // @lock = false: const symbol_typet jlo_symbol("java::java.lang.Object"); const struct_typet &jlo_type = to_struct_type(ns.follow(jlo_symbol)); struct_exprt jlo_init(jlo_symbol); - java_root_class_init(jlo_init, jlo_type, false, class_id); + java_root_class_init(jlo_init, jlo_type, class_id); struct_exprt struct_expr(obj.type()); struct_expr.copy_to_operands(jlo_init); @@ -1065,9 +1064,17 @@ void java_object_factoryt::gen_nondet_struct_init( { continue; } - else if(name=="@lock") + else if(name == "cproverMonitorCount") { - continue; + // Zero-initialize 'cproverMonitorCount' field as it is not meant to be + // nondet. This field is only present when the java core models are + // included in the class-path. It is used to implement a critical section, + // which is necessary to support concurrency. + if(update_in_place == update_in_placet::MUST_UPDATE_IN_PLACE) + continue; + code_assignt code(me, from_integer(0, me.type())); + code.add_source_location() = loc; + assignments.copy_to_operands(code); } else { diff --git a/jbmc/src/java_bytecode/java_root_class.cpp b/jbmc/src/java_bytecode/java_root_class.cpp index 4c2d98b43b9..3d33b2b6678 100644 --- a/jbmc/src/java_bytecode/java_root_class.cpp +++ b/jbmc/src/java_bytecode/java_root_class.cpp @@ -13,34 +13,16 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_types.h" -/******************************************************************* - - Function: java_root_class - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - +/// Create components to an object of the root class (usually java.lang.Object) +/// Specifically, we add a new component, '\@class_identifier'. This used +/// primary to replace an expression like 'e instanceof A' with +/// 'e.\@class_identifier == "A"' +/// \param class_symbol: class symbol void java_root_class(symbolt &class_symbol) { struct_typet &struct_type=to_struct_type(class_symbol.type); struct_typet::componentst &components=struct_type.components(); - { - // for monitorenter/monitorexit - struct_typet::componentt component; - component.set_name("@lock"); - component.set_pretty_name("@lock"); - component.type()=java_boolean_type(); - - // add at the beginning - components.insert(components.begin(), component); - } - { // the class identifier is used for stuff such as 'instanceof' struct_typet::componentt component; @@ -56,13 +38,11 @@ void java_root_class(symbolt &class_symbol) /// Adds members for an object of the root class (usually java.lang.Object). /// \param jlo [out] : object to initialize /// \param root_type: type of the root class -/// \param lock: lock field /// \param class_identifier: class identifier field, generally begins with /// "java::" prefix. void java_root_class_init( struct_exprt &jlo, const struct_typet &root_type, - const bool lock, const irep_idt &class_identifier) { jlo.operands().resize(root_type.components().size()); @@ -72,7 +52,15 @@ void java_root_class_init( constant_exprt clsid(class_identifier, clsid_type); jlo.operands()[clsid_nb]=clsid; - const std::size_t lock_nb=root_type.component_number("@lock"); - const typet &lock_type=root_type.components()[lock_nb].type(); - jlo.operands()[lock_nb]=from_integer(lock, lock_type); + // Check if the 'cproverMonitorCount' component exists and initialize it. + // This field is only present when the java core models are embedded. It is + // used to implement a critical section, which is necessary to support + // concurrency. + if(root_type.has_component("cproverMonitorCount")) + { + const std::size_t count_nb = + root_type.component_number("cproverMonitorCount"); + const typet &count_type = root_type.components()[count_nb].type(); + jlo.operands()[count_nb] = from_integer(0, count_type); + } } diff --git a/jbmc/src/java_bytecode/java_root_class.h b/jbmc/src/java_bytecode/java_root_class.h index 583556de857..3c1f148ee0f 100644 --- a/jbmc/src/java_bytecode/java_root_class.h +++ b/jbmc/src/java_bytecode/java_root_class.h @@ -21,7 +21,6 @@ void java_root_class( void java_root_class_init( struct_exprt &jlo, const struct_typet &root_type, - bool lock, const irep_idt &class_identifier); #endif // CPROVER_JAVA_BYTECODE_JAVA_ROOT_CLASS_H diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp index 822fcd46a97..1f901d6bda0 100644 --- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp +++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp @@ -840,12 +840,12 @@ codet java_string_library_preprocesst::code_assign_components_to_java_string( PRECONDITION(implements_java_char_sequence_pointer(lhs.type())); dereference_exprt deref=checked_dereference(lhs, lhs.type().subtype()); - // A String has a field Object with @clsid = String and @lock = false: + // A String has a field Object with @clsid = String const symbolt &jlo_symbol=*symbol_table.lookup("java::java.lang.Object"); const struct_typet &jlo_struct=to_struct_type(jlo_symbol.type); struct_exprt jlo_init(jlo_struct); irep_idt clsid = get_tag(lhs.type().subtype()); - java_root_class_init(jlo_init, jlo_struct, false, clsid); + java_root_class_init(jlo_init, jlo_struct, clsid); struct_exprt struct_rhs(deref.type()); struct_rhs.copy_to_operands(jlo_init); diff --git a/jbmc/src/java_bytecode/java_string_literals.cpp b/jbmc/src/java_bytecode/java_string_literals.cpp index b4de86b1cd4..b090adfaef4 100644 --- a/jbmc/src/java_bytecode/java_string_literals.cpp +++ b/jbmc/src/java_bytecode/java_string_literals.cpp @@ -94,12 +94,12 @@ symbol_exprt get_or_create_string_literal_symbol( namespacet ns(symbol_table); // Regardless of string refinement setting, at least initialize - // the literal with @clsid = String and @lock = false: + // the literal with @clsid = String symbol_typet jlo_symbol("java::java.lang.Object"); const auto &jlo_struct = to_struct_type(ns.follow(jlo_symbol)); struct_exprt jlo_init(jlo_symbol); const auto &jls_struct = to_struct_type(ns.follow(string_type)); - java_root_class_init(jlo_init, jlo_struct, false, "java::java.lang.String"); + java_root_class_init(jlo_init, jlo_struct, "java::java.lang.String"); // If string refinement *is* around, populate the actual // contents as well: @@ -197,7 +197,7 @@ symbol_exprt get_or_create_string_literal_symbol( else if(jls_struct.get_bool(ID_incomplete_class)) { // Case where java.lang.String was stubbed, and so directly defines - // @class_identifier and @lock: + // @class_identifier new_symbol.value = jlo_init; } diff --git a/jbmc/src/java_bytecode/simple_method_stubbing.cpp b/jbmc/src/java_bytecode/simple_method_stubbing.cpp index 099b956e442..4fa38a5ea03 100644 --- a/jbmc/src/java_bytecode/simple_method_stubbing.cpp +++ b/jbmc/src/java_bytecode/simple_method_stubbing.cpp @@ -233,10 +233,17 @@ void java_simple_method_stubst::create_method_stub(symbolt &symbol) void java_simple_method_stubst::check_method_stub(const irep_idt &symname) { const symbolt &sym = *symbol_table.lookup(symname); - if( - !sym.is_type && sym.value.id() == ID_nil && sym.type.id() == ID_code && - // Don't stub internal locking primitives: - sym.name != "java::monitorenter" && sym.name != "java::monitorexit") + if(!sym.is_type && sym.value.id() == ID_nil && + sym.type.id() == ID_code && + // do not stub internal locking calls as 'create_method_stub' does not + // automatically create the appropriate symbols for the formal parameters. + // This means that symex will (rightfully) crash when it encounters the + // function call as it will not be able to find symbols for the fromal + // parameters. + sym.name != + "java::java.lang.Object.monitorenter:(Ljava/lang/Object;)V" && + sym.name != + "java::java.lang.Object.monitorexit:(Ljava/lang/Object;)V") { create_method_stub(*symbol_table.get_writeable(symname)); } diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.cpp b/jbmc/unit/java-testing-utils/require_goto_statements.cpp index 77a91721713..ed6bc73ff04 100644 --- a/jbmc/unit/java-testing-utils/require_goto_statements.cpp +++ b/jbmc/unit/java-testing-utils/require_goto_statements.cpp @@ -355,8 +355,8 @@ const irep_idt &require_goto_statements::require_struct_component_assignment( // After we have found the declaration of the final assignment's // right hand side, then we want to identify that the type // is the one we expect, e.g.: - // struct java.lang.Integer { __CPROVER_string @class_identifier; - // boolean @lock; } tmp_object_factory$2; + // struct java.lang.Integer { __CPROVER_string @class_identifier; } + // tmp_object_factory$2; const auto &component_declaration = require_goto_statements::require_declaration_of_name( component_tmp_name, entry_point_instructions); diff --git a/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp b/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp index 389e1f43056..472e119494d 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp +++ b/jbmc/unit/java_bytecode/goto_program_generics/generic_bases_test.cpp @@ -50,8 +50,8 @@ SCENARIO( // tmp_object_factory$1.@Wrapper.field = // (struct java.lang.Object *) tmp_object_factory$2; // tmp_object_factory$2 = &tmp_object_factory$3; - // struct java.lang.Integer { __CPROVER_string @class_identifier; - // boolean @lock; } tmp_object_factory$3; + // struct java.lang.Integer { __CPROVER_string @class_identifier; } + // tmp_object_factory$3; require_goto_statements::require_struct_component_assignment( this_tmp_name, {"Wrapper"}, @@ -455,8 +455,8 @@ SCENARIO( { // tmp_object_factory$1.@UnsupportedWrapper1.field = // &tmp_object_factory$2; - // struct java.lang.Object { __CPROVER_string @class_identifier; - // boolean @lock; } tmp_object_factory$2; + // struct java.lang.Object { __CPROVER_string @class_identifier; } + // tmp_object_factory$2; require_goto_statements::require_struct_component_assignment( this_tmp_name, {"UnsupportedWrapper1"}, diff --git a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp index 9d7b1633b35..c80824631c6 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp +++ b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp @@ -559,8 +559,8 @@ SCENARIO( THEN("Object 'f' has unspecialized field 'field'") { // tmp_object_factory$2.field = &tmp_object_factory$3; - // struct java.lang.Object { __CPROVER_string @class_identifier; - // boolean @lock; } tmp_object_factory$3; + // struct java.lang.Object { __CPROVER_string @class_identifier; } + // tmp_object_factory$3; require_goto_statements::require_struct_component_assignment( field_input_name, {}, diff --git a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp index 31071dace29..032348e8ed6 100644 --- a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp +++ b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp @@ -83,7 +83,7 @@ SCENARIO( "return_array = cprover_associate_length_to_array_func" "(*string_data_pointer, tmp_object_factory);", "arg = { .@java.lang.Object={ .@class_identifier" - "=\"java::java.lang.String\", .@lock=false }," + "=\"java::java.lang.String\" }," " .length=tmp_object_factory, " ".data=*string_data_pointer };"}; diff --git a/jbmc/regression/jbmc/overlay-class/format_classpath.sh b/scripts/format_classpath.sh similarity index 100% rename from jbmc/regression/jbmc/overlay-class/format_classpath.sh rename to scripts/format_classpath.sh diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp index 330c4c1f152..a15f5833e89 100644 --- a/src/goto-programs/builtin_functions.cpp +++ b/src/goto-programs/builtin_functions.cpp @@ -855,12 +855,14 @@ void goto_convertt::do_function_call_symbol( } else if(identifier==CPROVER_PREFIX "atomic_begin" || identifier=="__CPROVER::atomic_begin" || + identifier=="java::org.cprover.CProver.atomicBegin:()V" || identifier=="__VERIFIER_atomic_begin") { do_atomic_begin(lhs, function, arguments, dest); } else if(identifier==CPROVER_PREFIX "atomic_end" || identifier=="__CPROVER::atomic_end" || + identifier=="java::org.cprover.CProver.atomicEnd:()V" || identifier=="__VERIFIER_atomic_end") { do_atomic_end(lhs, function, arguments, dest); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index c7b233c17ab..05e84f1d9f2 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -384,6 +384,7 @@ IREP_ID_TWO(C_is_anonymous, #is_anonymous) IREP_ID_ONE(is_enum_constant) IREP_ID_ONE(is_inline) IREP_ID_ONE(is_extern) +IREP_ID_ONE(is_synchronized) IREP_ID_ONE(is_global) IREP_ID_ONE(is_thread_local) IREP_ID_ONE(is_parameter)