Merge pull request #1759 from smowton/smowton/feature/symex-driven-program-loading

JBMC: Add symex-based program loading

Author: smowton

regression/cbmc-java/CMakeLists.txt

@@ -1,3 +1,10 @@
 add_test_pl_tests(
     "$<TARGET_FILE:jbmc>"
 )
+
+add_test_pl_profile(
+    "cbmc-java-symex-driven-lazy-loading"
+    "$<TARGET_FILE:jbmc> --symex-driven-lazy-loading"
+    "-C;-X;symex-driven-lazy-loading-expected-failure"
+    "CORE"
+)

regression/cbmc-java/Makefile

@@ -2,9 +2,11 @@ default: tests.log
 
 test:
 	@../test.pl -p -c ../../../src/jbmc/jbmc
+	@../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
 
 tests.log: ../test.pl
 	@../test.pl -p -c ../../../src/jbmc/jbmc
+	@../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure
 
 show:
 	@for dir in *; do \

regression/cbmc-java/NondetInit/test_lazy.desc

@@ -1,5 +1,7 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 Test.class
 --function Test.check --lazy-methods
 ^VERIFICATION SUCCESSFUL$
 --
+--
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

regression/cbmc-java/covered1/test.desc

@@ -1,19 +1,19 @@
 CORE
 covered1.class
---cover location --json-ui --show-properties
+--cover location --json-ui --show-properties --function 'covered1.<init>'
 ^EXIT=0$
 ^SIGNAL=0$
 .*\"coveredLines\": \"22\",$
-.*\"coveredLines\": \"4\",$
-.*\"coveredLines\": \"6\",$
-.*\"coveredLines\": \"7\",$
-.*\"coveredLines\": \"23\",$
-.*\"coveredLines\": \"24\",$
-.*\"coveredLines\": \"25\",$
-.*\"coveredLines\": \"31\",$
-.*\"coveredLines\": \"32\",$
-.*\"coveredLines\": \"33\",$
-.*\"coveredLines\": \"36\",$
+(.*\"coveredLines\": \"4\")|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"6\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"7\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"23\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"24\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"25\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"31\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"32\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"33\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
+.*\"coveredLines\": \"36\"|(\"coveredLines\": \"4,6,7,23-25,31-33,36\"),$
 .*\"coveredLines\": \"26\",$
 .*\"coveredLines\": \"28\",$
 .*\"coveredLines\": \"28\",$
@@ -25,3 +25,9 @@ covered1.class
 .*\"coveredLines\": \"35\",$
 --
 ^warning: ignoring
+--
+The alternation between the grouped and ungrouped reporting formats for coveredLines accommodates the
+difference between symex-driven-lazy-loading (which currently causes jbmc to use the grouped format)
+and normal loading (which uses the ungrouped format).
+The cause of the difference appears to be symex-driven loading being more pessimistic about possible
+exceptions coming from callees, which in turn changes the shape of the CFG.

regression/cbmc-java/exceptions26/test.desc

@@ -1,5 +1,6 @@
 CORE
 test.class
+
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring

regression/cbmc-java/exceptions27/test.desc

@@ -1,5 +1,6 @@
 CORE
 test.class
+
 VERIFICATION SUCCESSFUL
 --
 ^warning: ignoring

regression/cbmc-java/generic_class_bound1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 Gn.class
 --cover location
 ^EXIT=0$
@@ -9,3 +9,6 @@ Gn.class
 .*file Gn.java line 11 function java::Gn.foo1:\(LGn;\)V bytecode-index 5 block 3: FAILED
 .*file Gn.java line 13 function java::Gn.main:\(\[Ljava/lang/String;\)V bytecode-index 2 block 2: SATISFIED
 --
+--
+This fails under symex-driven lazy loading because the FAILED blocks occur in functions that are unreachable
+from the entry point, so with symex-driven loading the functions foo1 and the constructor don't get created at all.

regression/cbmc-java/jsr1/test.desc

@@ -1,8 +1,10 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 edu/emory/mathcs/backport/java/util/concurrent/ConcurrentHashMap.class
 --show-goto-functions
 ^EXIT=0$
 ^SIGNAL=0$
 --
 \\"statement\\" \(\\"jsr\\"\)
 \\"statement\\" \(\\"ret\\"\)
+--
+This doesn't work under symex-driven lazy loading because no entry-point function is given.

regression/cbmc-java/lambda2/test_no_crash.desc

@@ -1,8 +1,9 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 SymStream.class
 --verbosity 10 --show-goto-functions
 ^EXIT=0
 ^SIGNAL=0
 --
 --
 just to test that it doesn't crash in this situation, cf. TG-2684
+Doesn't work with symex-driven loading because there is no entry point (we want to load the entire class)

regression/cbmc-java/lazyloading1/test.desc

@@ -1,8 +1,10 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --verbosity 10 --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 elaborate java::A\.f:\(\)V
 --
 elaborate java::B\.g:\(\)V
+--
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods