Add tests for symex-driven lazy loading

This adds variants of the three test directories that use JBMC (cbmc-java, jbmc-strings and
strings-smoke-tests) to run with --symex-driven-lazy-loading, except for the small number of
tests that are expected to fail for harmless reasons, and one that is expected to fail and
which may be a bug (strings-smoke-tests/java_append_char).

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/NondetInit/test_lazy.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 Test.class
 --function Test.check --lazy-methods
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-java/covered1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 covered1.class
 --cover location --json-ui --show-properties
 ^EXIT=0$
@@ -25,3 +25,5 @@ covered1.class
 .*\"coveredLines\": \"35\",$
 --
 ^warning: ignoring
+--
+This fails with symex-driven lazy loading because it does not currently support --show-properties.

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 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,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --verbosity 10 --function test.main
 ^EXIT=0$

regression/cbmc-java/lazyloading10/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
 ^EXIT=6$

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$

regression/cbmc-java/lazyloading2/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --verbosity 10 --function test.main
 ^EXIT=0$

regression/cbmc-java/lazyloading3/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --verbosity 10 --function test.main
 ^EXIT=0$

regression/cbmc-java/lazyloading4/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 Main.class
 --lazy-methods
 ^EXIT=0$

regression/cbmc-java/lazyloading5/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --function test.main
 ^EXIT=0$

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$

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$

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$

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$

regression/cbmc-java/lazyloading_array_parameter/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --verbosity 10 --function test.g
 ^EXIT=0$

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

regression/cbmc-java/lazyloading_indirect_array_parameter/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --verbosity 10 --function test.g
 ^EXIT=0$

regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --verbosity 10 --function test.g
 ^EXIT=0$

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$

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

regression/cbmc-java/lazyloading_multiple_array_types/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 Test.class
 --lazy-methods --verbosity 10 --function Test.check
 ^EXIT=0$

regression/cbmc-java/lazyloading_multiple_generic_parameters/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 test.class
 --lazy-methods --verbosity 10 --function test.g
 ^EXIT=0$

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

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,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 Test.class
 --lazy-methods --show-goto-functions --function Test.main
 --

regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 Test.class
 --lazy-methods --function Test.main
 VERIFICATION SUCCESSFUL

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

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc

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

regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 Test.class
 --lazy-methods --function Test.main
 VERIFICATION SUCCESSFUL

regression/cbmc-java/lazyloading_synthetic_method_cleanup3/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::Opaque\.<clinit>:\(\)V

regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc

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

regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 Test.class
 --lazy-methods --function Test.main
 VERIFICATION SUCCESSFUL

regression/cbmc-java/lvt-groovy/test.desc

@@ -1,7 +1,8 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 DetectSplitPackagesTask.class
 --show-symbol-table
 ^EXIT=0$
 ^SIGNAL=0$
 --
 --
+This doesn't work under lazy loading because no entry-point function is given.

regression/cbmc-java/lvt-unexpected/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 unexpected.class
 --verbosity 10 --show-symbol-table
 ^EXIT=0$
@@ -10,3 +10,5 @@ expected by the bytecode to goto conversion algorithms. Namely, the live range
 of parameter x in that method is not preceeded by a store_i instruction, which
 is perfectly possibly as per the JVM specs but currently additionally required
 in CBMC.
+
+This doesn't work under lazy loading because no entry-point function is given.

regression/cbmc-java/method_parmeters1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 method_parameters.class
 --verbosity 10 --show-symbol-table
 ^EXIT=0$
@@ -7,3 +7,5 @@ method_parameters.class
 --
 The purpose of the test is ensuring that the bytecode -> symbol table AST
 generation happens correctly. The generated .class file does not contain LVTs.
+
+This doesn't work under lazy loading because no entry-point function is given.

regression/cbmc-java/method_parmeters2/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 method_parameters.class
 --verbosity 10 --show-symbol-table
 ^EXIT=0$
@@ -8,3 +8,5 @@ method_parameters.class
 The purpose of the test is ensuring that the bytecode -> symbol table AST
 generation happens correctly. The generated .class file DOES contain LVTs, i.e.,
 it has been compiled with with "javac -g".
+
+This doesn't work under lazy loading because no entry-point function is given.

regression/cbmc-java/package_friendly1/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 main.class
 package_friendly1.class package_friendly2.class --show-goto-functions
 ^main[.]main[\(][\)].*$
@@ -7,3 +7,5 @@ package_friendly1.class package_friendly2.class --show-goto-functions
 ^SIGNAL=0$
 --
 ^warning: ignoring
+--
+This doesn't work under lazy loading because no entry-point function is given.

regression/cbmc-java/remove_virtual_function_typecast/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 VirtualFunctions.class
 --lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --cover location --function VirtualFunctions.check --show-goto-functions
  \(struct VirtualFunctions\$B \*\)a \. VirtualFunctions\$B\.f:\(\)V\(\);$

regression/cbmc-java/removed_virtual_functions/test.desc

@@ -1,4 +1,4 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 ArrayListEquals.class
 --lazy-methods --java-max-vla-length 48 --unwind 8 --java-unwind-enum-static --trace --cover location --function ArrayListEquals.check2 --show-goto-functions
 e2 . ArrayList\$Itr.hasNext:\(\)Z\(\);

regression/cbmc-java/virtual10/test.desc

@@ -1,6 +1,6 @@
 CORE
 E.class
---show-goto-functions
+--function E.f --show-goto-functions
 IF.*"java::D"
 IF.*"java::O"
 IF.*"java::C"

regression/cbmc-java/virtual7/test.desc

@@ -3,6 +3,6 @@ test.class
 --show-goto-functions --function test.main
 ^EXIT=0$
 ^SIGNAL=0$
-IF.*"java::C".*THEN GOTO [12]
-IF.*"java::D".*THEN GOTO [12]
-IF.*"java::A".*THEN GOTO [12]
+IF.*"java::C".*THEN GOTO
+IF.*"java::D".*THEN GOTO
+IF.*"java::A".*THEN GOTO

regression/jbmc-strings/CMakeLists.txt

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

regression/jbmc-strings/StringIndexOf/test.desc

@@ -4,4 +4,3 @@ Test.class
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
---

regression/jbmc-strings/java_char_array_init/test.desc

@@ -7,4 +7,3 @@ assertion.* file test_init.java line 31 .* SUCCESS$
 assertion.* file test_init.java line 33 .* SUCCESS$
 assertion.* file test_init.java line 35 .* FAILURE$
 assertion.* file test_init.java line 37 .* FAILURE$
---

regression/strings-smoke-tests/CMakeLists.txt

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