Merge pull request diffblue#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

regression/cbmc-java/lazyloading10/test.desc

@@ -1,8 +1,11 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point test.sety
 ^EXIT=6$
 ^SIGNAL=0$
 entry point 'test\.sety' is ambiguous between:
 test\.sety:\(I\)V
 test\.sety:\(F\)V
+--
+--
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

regression/cbmc-java/lazyloading11/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:(I)V' --lazy-methods-extra-entry-point 'test.sety:(F)V'
 ^EXIT=0$
@@ -8,3 +8,5 @@ CI lazy methods: elaborate java::test\.sety:\(I\)V
 CI lazy methods: elaborate java::test\.sety:\(F\)V
 --
 CI lazy methods: elaborate java::test\.setx:\(I\)V
+--
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

regression/cbmc-java/lazyloading2/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

regression/cbmc-java/lazyloading3/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

regression/cbmc-java/lazyloading4/test.desc

@@ -1,6 +1,9 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 Main.class
 --lazy-methods
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
+--
+--
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

regression/cbmc-java/lazyloading5/test.desc

@@ -1,6 +1,9 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
 VERIFICATION SUCCESSFUL
+--
+--
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

regression/cbmc-java/lazyloading6/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point test.setx
 ^EXIT=0$
@@ -8,3 +8,5 @@ CI lazy methods: elaborate java::test\.setx:\(I\)V
 --
 CI lazy methods: elaborate java::test\.sety:\(I\)V
 CI lazy methods: elaborate java::test\.sety:\(F\)V
+--
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

regression/cbmc-java/lazyloading7/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:(I)V'
 ^EXIT=0$
@@ -8,3 +8,5 @@ CI lazy methods: elaborate java::test\.sety:\(I\)V
 --
 CI lazy methods: elaborate java::test\.setx:\(I\)V
 CI lazy methods: elaborate java::test\.sety:\(F\)V
+--
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

regression/cbmc-java/lazyloading8/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.sety:(F)V'
 ^EXIT=0$
@@ -8,3 +8,5 @@ CI lazy methods: elaborate java::test\.sety:\(F\)V
 --
 CI lazy methods: elaborate java::test\.sety:\(I\)V
 CI lazy methods: elaborate java::test\.setx:\(I\)V
+--
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

regression/cbmc-java/lazyloading9/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --verbosity 10 --function test.f --lazy-methods-extra-entry-point 'test.*'
 ^EXIT=0$
@@ -7,3 +7,6 @@ VERIFICATION SUCCESSFUL
 CI lazy methods: elaborate java::test\.setx:\(I\)V
 CI lazy methods: elaborate java::test\.sety:\(I\)V
 CI lazy methods: elaborate java::test\.sety:\(F\)V
+--
+--
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

regression/cbmc-java/lazyloading_array_parameter/test.desc

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

regression/cbmc-java/lazyloading_cyclic_class/test.desc

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

regression/cbmc-java/lazyloading_indirect_array_parameter/test.desc

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

regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.desc

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

regression/cbmc-java/lazyloading_inheritance/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --verbosity 10 --function test.test
 ^EXIT=0$
@@ -7,3 +7,5 @@ elaborate java::Base\.f:\(\)V
 --
 elaborate java::Derived\.f:\(\)V
 elaborate java::Middle\.f:\(\)V
+--
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

regression/cbmc-java/lazyloading_inheritance_field/test.desc

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

regression/cbmc-java/lazyloading_multiple_array_types/test.desc

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

regression/cbmc-java/lazyloading_multiple_generic_parameters/test.desc

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

regression/cbmc-java/lazyloading_nested_generic_parameters/test.desc

@@ -11,3 +11,4 @@ The right methods are loaded, but verification is not successful
 because __CPROVER_start doesn't create appropriately typed input for
 this kind of nested generic parameter, so dynamic cast checks fail upon
 fetching the generic type's field.
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

regression/cbmc-java/lazyloading_recursive_class/test.desc

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

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 Test.class
 --show-goto-functions --function Test.main
 java::Unused::clinit_wrapper

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc

@@ -1,6 +1,8 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 Test.class
 --lazy-methods --show-goto-functions --function Test.main
 --
 java::Unused::clinit_wrapper
 Unused\.<clinit>\(\)
+--
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc

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

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 Test.class
 --show-goto-functions --function Test.main
 java::Unused1::clinit_wrapper