Add tests for symex-driven lazy loading

smowton · smowton · commit 28a878fee934 · 2018-03-21T17:26:27.000Z
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).
diff --git a/regression/cbmc-java/CMakeLists.txt b/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"
+)
diff --git a/regression/cbmc-java/Makefile b/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 \
diff --git a/regression/cbmc-java/NondetInit/test_lazy.desc b/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
diff --git a/regression/cbmc-java/covered1/test.desc b/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.
diff --git a/regression/cbmc-java/generic_class_bound1/test.desc b/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.
diff --git a/regression/cbmc-java/jsr1/test.desc b/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.
diff --git a/regression/cbmc-java/lambda2/test_no_crash.desc b/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)
diff --git a/regression/cbmc-java/lazyloading1/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading10/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading11/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading2/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading3/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading4/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading5/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading6/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading7/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading8/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading9/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading_array_parameter/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading_cyclic_class/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading_indirect_array_parameter/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading_indirect_generic_array_parameter/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading_inheritance/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading_inheritance_field/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading_multiple_array_types/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading_multiple_generic_parameters/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading_nested_generic_parameters/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading_recursive_class/test.desc b/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
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_normally_present.desc b/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
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_clinit_removed_by_lazy_loading.desc b/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
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup1/check_runs_with_lazy_loading.desc b/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
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_normally_present.desc b/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
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_clinit_removed_by_lazy_loading.desc
@@ -1,7 +1,9 @@
-CORE
+CORE symex-driven-lazy-loading-expected-failure
 Test.class
 --lazy-methods --show-goto-functions --function Test.main
 --
 java::Unused1::clinit_wrapper
 java::Unused2::clinit_wrapper
 Unused2\.<clinit>\(\)
+--
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup2/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
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_normally_present.desc b/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
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_clinit_removed_by_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/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::Opaque\.<clinit>:\(\)V
 java::Opaque::clinit_wrapper
+--
+This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods
diff --git a/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/check_runs_with_lazy_loading.desc b/regression/cbmc-java/lazyloading_synthetic_method_cleanup3/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
diff --git a/regression/cbmc-java/lvt-groovy/test.desc b/regression/cbmc-java/lvt-groovy/test.desc
diff --git a/regression/cbmc-java/lvt-unexpected/test.desc b/regression/cbmc-java/lvt-unexpected/test.desc
diff --git a/regression/cbmc-java/method_parmeters1/test.desc b/regression/cbmc-java/method_parmeters1/test.desc
diff --git a/regression/cbmc-java/method_parmeters2/test.desc b/regression/cbmc-java/method_parmeters2/test.desc
diff --git a/regression/cbmc-java/package_friendly1/test.desc b/regression/cbmc-java/package_friendly1/test.desc
diff --git a/regression/cbmc-java/remove_virtual_function_typecast/test.desc b/regression/cbmc-java/remove_virtual_function_typecast/test.desc
diff --git a/regression/cbmc-java/removed_virtual_functions/test.desc b/regression/cbmc-java/removed_virtual_functions/test.desc
diff --git a/regression/cbmc-java/virtual10/test.desc b/regression/cbmc-java/virtual10/test.desc
diff --git a/regression/cbmc-java/virtual7/test.desc b/regression/cbmc-java/virtual7/test.desc
diff --git a/regression/jbmc-strings/CMakeLists.txt b/regression/jbmc-strings/CMakeLists.txt
diff --git a/regression/jbmc-strings/Makefile b/regression/jbmc-strings/Makefile
diff --git a/regression/jbmc-strings/StringIndexOf/test.desc b/regression/jbmc-strings/StringIndexOf/test.desc
diff --git a/regression/jbmc-strings/java_char_array_init/test.desc b/regression/jbmc-strings/java_char_array_init/test.desc
diff --git a/regression/strings-smoke-tests/CMakeLists.txt b/regression/strings-smoke-tests/CMakeLists.txt
diff --git a/regression/strings-smoke-tests/Makefile b/regression/strings-smoke-tests/Makefile
