diff --git a/regression/cbmc-java/CMakeLists.txt b/regression/cbmc-java/CMakeLists.txt index afe0ea5761a..2742f7ba078 100644 --- a/regression/cbmc-java/CMakeLists.txt +++ b/regression/cbmc-java/CMakeLists.txt @@ -1,3 +1,10 @@ add_test_pl_tests( "$" ) + +add_test_pl_profile( + "cbmc-java-symex-driven-lazy-loading" + "$ --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 index e94b327bb43..15894631527 100644 --- 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 index 9ca92cb5696..6840ea97697 100644 --- 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 index 8982c0321db..8f6adc9d0a3 100644 --- a/regression/cbmc-java/covered1/test.desc +++ b/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.' ^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. diff --git a/regression/cbmc-java/exceptions26/test.desc b/regression/cbmc-java/exceptions26/test.desc index 0e2ccfc7f46..eb2dc18d2cb 100644 --- a/regression/cbmc-java/exceptions26/test.desc +++ b/regression/cbmc-java/exceptions26/test.desc @@ -1,5 +1,6 @@ CORE test.class + ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring diff --git a/regression/cbmc-java/exceptions27/test.desc b/regression/cbmc-java/exceptions27/test.desc index b4d6b49e539..459f879662b 100644 --- a/regression/cbmc-java/exceptions27/test.desc +++ b/regression/cbmc-java/exceptions27/test.desc @@ -1,5 +1,6 @@ CORE test.class + VERIFICATION SUCCESSFUL -- ^warning: ignoring diff --git a/regression/cbmc-java/generic_class_bound1/test.desc b/regression/cbmc-java/generic_class_bound1/test.desc index 0195fb3ecc4..0da89d44def 100644 --- 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 index faec2ddbb03..b7cb6825d52 100644 --- a/regression/cbmc-java/jsr1/test.desc +++ b/regression/cbmc-java/jsr1/test.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure edu/emory/mathcs/backport/java/util/concurrent/ConcurrentHashMap.class --show-goto-functions ^EXIT=0$ @@ -6,3 +6,5 @@ edu/emory/mathcs/backport/java/util/concurrent/ConcurrentHashMap.class -- \\"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 index 933732babea..f05242bf10d 100644 --- a/regression/cbmc-java/lambda2/test_no_crash.desc +++ b/regression/cbmc-java/lambda2/test_no_crash.desc @@ -1,4 +1,4 @@ -CORE +CORE symex-driven-lazy-loading-expected-failure SymStream.class --verbosity 10 --show-goto-functions ^EXIT=0 @@ -6,3 +6,4 @@ SymStream.class -- -- 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 index c0011248128..245446c791a 100644 --- a/regression/cbmc-java/lazyloading1/test.desc +++ b/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$ @@ -6,3 +6,5 @@ test.class 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 index 38fb7495a08..3a1f2da5ae8 100644 --- a/regression/cbmc-java/lazyloading10/test.desc +++ b/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$ @@ -6,3 +6,6 @@ test.class 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 index 1114831afb3..ee2ef683627 100644 --- 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 index c0011248128..245446c791a 100644 --- a/regression/cbmc-java/lazyloading2/test.desc +++ b/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$ @@ -6,3 +6,5 @@ test.class 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 index c0011248128..245446c791a 100644 --- a/regression/cbmc-java/lazyloading3/test.desc +++ b/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$ @@ -6,3 +6,5 @@ test.class 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 index e7822c6deba..9df5b91931e 100644 --- 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 index a3226adccaa..fa309520217 100644 --- 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 index dd4bbf33bc9..ce055cbbc7b 100644 --- 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 index 3b2e305f66c..009f489aeff 100644 --- 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 index 777f1673de9..2476aa30841 100644 --- 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 index ddd4fbd51c0..09f407629c7 100644 --- 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 index 15e3f99d782..51ac926c68a 100644 --- 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 index c39c5e62349..fec143df213 100644 --- 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 index 15e3f99d782..51ac926c68a 100644 --- 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 index 15e3f99d782..51ac926c68a 100644 --- 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 index 12ef42a2183..76ed72b1f69 100644 --- 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 index c39c5e62349..fec143df213 100644 --- 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 index f15d1291c02..faa9503717a 100644 --- a/regression/cbmc-java/lazyloading_multiple_array_types/test.desc +++ b/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$ @@ -6,3 +6,6 @@ Test.class 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 index 15e3f99d782..51ac926c68a 100644 --- 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 index ae44ea6da9b..579f3933553 100644 --- 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 index c39c5e62349..fec143df213 100644 --- 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 index ddcd21bd5f2..f05b7408521 100644 --- 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 index 7cb991a807f..49c88acd878 100644 --- 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\.\(\) +-- +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 index 67aa49a0689..0c6c32b0319 100644 --- 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 index 32ea1eabe00..18c1eda7556 100644 --- 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 index 3fb25e852a4..7a6c066bf9d 100644 --- 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\.\(\) +-- +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 index 67aa49a0689..0c6c32b0319 100644 --- 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 index 689fdc3efad..81312c026c4 100644 --- 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\.:\(\)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 index ec1d71302d6..b0256ccbad8 100644 --- 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\.:\(\)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 index 67aa49a0689..0c6c32b0319 100644 --- 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 index 050fcd09c7e..6f8c52c05ca 100644 --- a/regression/cbmc-java/lvt-groovy/test.desc +++ b/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 symex-driven lazy loading because no entry-point function is given. diff --git a/regression/cbmc-java/lvt-unexpected/test.desc b/regression/cbmc-java/lvt-unexpected/test.desc index 7164d59e21f..fed0105ff68 100644 --- a/regression/cbmc-java/lvt-unexpected/test.desc +++ b/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 symex-driven lazy loading because no entry-point function is given. diff --git a/regression/cbmc-java/method_parmeters1/test.desc b/regression/cbmc-java/method_parmeters1/test.desc index 909aa8ab6b4..6960d310ed7 100644 --- a/regression/cbmc-java/method_parmeters1/test.desc +++ b/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 symex-driven lazy loading because no entry-point function is given. diff --git a/regression/cbmc-java/method_parmeters2/test.desc b/regression/cbmc-java/method_parmeters2/test.desc index 507e8d4ef11..da1c3e0267c 100644 --- a/regression/cbmc-java/method_parmeters2/test.desc +++ b/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 symex-driven lazy loading because no entry-point function is given. diff --git a/regression/cbmc-java/package_friendly1/test.desc b/regression/cbmc-java/package_friendly1/test.desc index 527f5b9bfe0..1b9f7ad4080 100644 --- a/regression/cbmc-java/package_friendly1/test.desc +++ b/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 symex-driven lazy loading because no entry-point function is given. diff --git a/regression/cbmc-java/remove_virtual_function_typecast/test.desc b/regression/cbmc-java/remove_virtual_function_typecast/test.desc index 32be1c0c99a..05841fcdc63 100644 --- a/regression/cbmc-java/remove_virtual_function_typecast/test.desc +++ b/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\(\);$ @@ -6,3 +6,5 @@ VirtualFunctions.class b \. VirtualFunctions\$B\.f:\(\)V\(\);$ \(struct VirtualFunctions\$B \*\)c \. VirtualFunctions\$B\.f:\(\)V\(\);$ -- +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/removed_virtual_functions/test.desc b/regression/cbmc-java/removed_virtual_functions/test.desc index 36b47b39757..93a66232f62 100644 --- a/regression/cbmc-java/removed_virtual_functions/test.desc +++ b/regression/cbmc-java/removed_virtual_functions/test.desc @@ -1,6 +1,8 @@ -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\(\); -- e2 . ListIterator.hasNext:\(\)Z\(\); +-- +This doesn't work under symex-driven lazy loading because it is incompatible with --lazy-methods diff --git a/regression/cbmc-java/static_init_order/test1.desc b/regression/cbmc-java/static_init_order/test1.desc index d80e6850004..26702c679cd 100644 --- a/regression/cbmc-java/static_init_order/test1.desc +++ b/regression/cbmc-java/static_init_order/test1.desc @@ -1,7 +1,6 @@ CORE static_init_order.class --function static_init_order.test1 --trace - ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/cbmc-java/static_init_order/test2.desc b/regression/cbmc-java/static_init_order/test2.desc index 367eae926c4..9ed5642c7ef 100644 --- a/regression/cbmc-java/static_init_order/test2.desc +++ b/regression/cbmc-java/static_init_order/test2.desc @@ -1,7 +1,6 @@ CORE static_init_order.class --function static_init_order.test2 - ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-java/virtual10/test.desc b/regression/cbmc-java/virtual10/test.desc index df1d033f0a4..ea746c52c19 100644 --- a/regression/cbmc-java/virtual10/test.desc +++ b/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" diff --git a/regression/cbmc-java/virtual7/test.desc b/regression/cbmc-java/virtual7/test.desc index 6e420f8430c..7d23df44236 100644 --- a/regression/cbmc-java/virtual7/test.desc +++ b/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 diff --git a/regression/jbmc-strings/CMakeLists.txt b/regression/jbmc-strings/CMakeLists.txt index afe0ea5761a..9b4832e9833 100644 --- a/regression/jbmc-strings/CMakeLists.txt +++ b/regression/jbmc-strings/CMakeLists.txt @@ -1,3 +1,10 @@ add_test_pl_tests( "$" ) + +add_test_pl_profile( + "jbmc-strings-symex-driven-lazy-loading" + "$ --symex-driven-lazy-loading" + "-C;-X;symex-driven-lazy-loading-expected-failure" + "CORE" +) diff --git a/regression/jbmc-strings/Makefile b/regression/jbmc-strings/Makefile index 58058dbc77a..79788e2eb69 100644 --- a/regression/jbmc-strings/Makefile +++ b/regression/jbmc-strings/Makefile @@ -2,15 +2,19 @@ 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 testfuture: @../test.pl -p -c ../../../src/jbmc/jbmc -CF + @../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF testall: @../test.pl -p -c ../../../src/jbmc/jbmc -CFTK + @../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK 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/jbmc-strings/StringIndexOf/test.desc b/regression/jbmc-strings/StringIndexOf/test.desc index 8b52eaea4dd..2e22278a15b 100644 --- a/regression/jbmc-strings/StringIndexOf/test.desc +++ b/regression/jbmc-strings/StringIndexOf/test.desc @@ -4,4 +4,3 @@ Test.class ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ --- diff --git a/regression/jbmc-strings/java_char_array_init/test.desc b/regression/jbmc-strings/java_char_array_init/test.desc index 47fcb2fd1ce..5ecb589e1f8 100644 --- a/regression/jbmc-strings/java_char_array_init/test.desc +++ b/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$ --- diff --git a/regression/strings-smoke-tests/CMakeLists.txt b/regression/strings-smoke-tests/CMakeLists.txt index afe0ea5761a..8c8577192c0 100644 --- a/regression/strings-smoke-tests/CMakeLists.txt +++ b/regression/strings-smoke-tests/CMakeLists.txt @@ -1,3 +1,10 @@ add_test_pl_tests( "$" ) + +add_test_pl_profile( + "strings-smoke-tests-symex-driven-lazy-loading" + "$ --symex-driven-lazy-loading" + "-C;-X;symex-driven-lazy-loading-expected-failure" + "CORE" +) diff --git a/regression/strings-smoke-tests/Makefile b/regression/strings-smoke-tests/Makefile index 58058dbc77a..79788e2eb69 100644 --- a/regression/strings-smoke-tests/Makefile +++ b/regression/strings-smoke-tests/Makefile @@ -2,15 +2,19 @@ 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 testfuture: @../test.pl -p -c ../../../src/jbmc/jbmc -CF + @../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CF testall: @../test.pl -p -c ../../../src/jbmc/jbmc -CFTK + @../test.pl -p -c "../../../src/jbmc/jbmc --symex-driven-lazy-loading" -X symex-driven-lazy-loading-expected-failure -CFTK 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/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 8359d4a2d97..c2a1e8db7d4 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -377,6 +377,15 @@ safety_checkert::resultt bmct::execute( const goto_functionst &goto_functions = goto_model.get_goto_functions(); + // This provides the driver program the opportunity to do things like a + // symbol-table or goto-functions dump instead of actually running the + // checker, like show-vcc except driver-program specific. + // In particular clients that use symex-driven program loading need to print + // GOTO functions after symex, as function bodies are not produced until + // symex first requests them. + if(driver_callback_after_symex && driver_callback_after_symex()) + return safety_checkert::resultt::SAFE; // to indicate non-error + // add a partial ordering, if required if(equation.has_threads()) { @@ -616,14 +625,15 @@ void bmct::setup_unwind() // creating those function bodies on demand. /// \param ui: user-interface mode (plain text, XML output, JSON output, ...) /// \param message: used for logging -/// \param frontend_configure_bmc: function provided by the frontend program, -/// which applies frontend-specific configuration to a bmct before running. +/// \param driver_configure_bmc: function provided by the driver program, +/// which applies driver-specific configuration to a bmct before running. int bmct::do_language_agnostic_bmc( const optionst &opts, abstract_goto_modelt &model, const ui_message_handlert::uit &ui, messaget &message, - std::function frontend_configure_bmc) + std::function driver_configure_bmc, + std::function callback_after_symex) { const symbol_tablet &symbol_table = model.get_symbol_table(); message_handlert &mh = message.get_message_handler(); @@ -637,9 +647,10 @@ int bmct::do_language_agnostic_bmc( std::unique_ptr cbmc_solver; cbmc_solver = solvers.get_solver(); prop_convt &pc = cbmc_solver->prop_conv(); - bmct bmc(opts, symbol_table, mh, pc, worklist); + bmct bmc(opts, symbol_table, mh, pc, worklist, callback_after_symex); bmc.set_ui(ui); - frontend_configure_bmc(bmc, symbol_table); + if(driver_configure_bmc) + driver_configure_bmc(bmc, symbol_table); result = bmc.run(model); } INVARIANT( @@ -682,8 +693,10 @@ int bmct::do_language_agnostic_bmc( pc, resume.equation, resume.state, - worklist); - frontend_configure_bmc(pe, symbol_table); + worklist, + callback_after_symex); + if(driver_configure_bmc) + driver_configure_bmc(pe, symbol_table); result &= pe.run(model); worklist.pop_front(); } diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 9daad327d66..d4feb6847e0 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -74,7 +74,8 @@ class bmct:public safety_checkert const symbol_tablet &outer_symbol_table, message_handlert &_message_handler, prop_convt &_prop_conv, - goto_symext::branch_worklistt &_branch_worklist) + goto_symext::branch_worklistt &_branch_worklist, + std::function callback_after_symex) : safety_checkert(ns, _message_handler), options(_options), outer_symbol_table(outer_symbol_table), @@ -83,7 +84,8 @@ class bmct:public safety_checkert branch_worklist(_branch_worklist), symex(_message_handler, outer_symbol_table, equation, branch_worklist), prop_conv(_prop_conv), - ui(ui_message_handlert::uit::PLAIN) + ui(ui_message_handlert::uit::PLAIN), + driver_callback_after_symex(callback_after_symex) { symex.constant_propagation=options.get_bool_option("propagation"); symex.record_coverage= @@ -128,10 +130,9 @@ class bmct:public safety_checkert abstract_goto_modelt &goto_model, const ui_message_handlert::uit &ui, messaget &message, - std::function frontend_configure_bmc = - [](bmct &_bmc, const symbol_tablet &) { // NOLINT (*) - // Empty default implementation - }); + std::function + driver_configure_bmc = nullptr, + std::function callback_after_symex = nullptr); protected: /// \brief Constructor for path exploration from saved state @@ -147,7 +148,8 @@ class bmct:public safety_checkert message_handlert &_message_handler, prop_convt &_prop_conv, symex_target_equationt &_equation, - goto_symext::branch_worklistt &_branch_worklist) + goto_symext::branch_worklistt &_branch_worklist, + std::function callback_after_symex) : safety_checkert(ns, _message_handler), options(_options), outer_symbol_table(outer_symbol_table), @@ -156,7 +158,8 @@ class bmct:public safety_checkert branch_worklist(_branch_worklist), symex(_message_handler, outer_symbol_table, equation, branch_worklist), prop_conv(_prop_conv), - ui(ui_message_handlert::uit::PLAIN) + ui(ui_message_handlert::uit::PLAIN), + driver_callback_after_symex(callback_after_symex) { symex.constant_propagation = options.get_bool_option("propagation"); symex.record_coverage = @@ -238,6 +241,12 @@ class bmct:public safety_checkert /// full-program model-checking from the entry point of the program. virtual void perform_symbolic_execution( goto_symext::get_goto_functiont get_goto_function); + + /// Optional callback, to be run after symex but before handing the resulting + /// equation to the solver. If it returns true then we will skip the solver + /// stage and return "safe" (no assertions violated / coverage goals reached), + /// similar to the behaviour when 'show-vcc' or 'program-only' are specified. + std::function driver_callback_after_symex; }; /// \brief Symbolic execution from a saved branch point @@ -260,14 +269,16 @@ class path_explorert : public bmct prop_convt &_prop_conv, symex_target_equationt &saved_equation, const goto_symex_statet &saved_state, - goto_symext::branch_worklistt &branch_worklist) + goto_symext::branch_worklistt &branch_worklist, + std::function callback_after_symex) : bmct( _options, outer_symbol_table, _message_handler, _prop_conv, saved_equation, - branch_worklist), + branch_worklist, + callback_after_symex), saved_state(saved_state) { } diff --git a/src/goto-programs/remove_exceptions.cpp b/src/goto-programs/remove_exceptions.cpp index 5d2d758edb6..f0a8b9b7e5f 100644 --- a/src/goto-programs/remove_exceptions.cpp +++ b/src/goto-programs/remove_exceptions.cpp @@ -79,23 +79,25 @@ class remove_exceptionst typedef std::vector> catch_handlerst; typedef std::vector stack_catcht; + typedef std::function function_may_throwt; public: explicit remove_exceptionst( - symbol_tablet &_symbol_table, - std::map> &_exceptions_map, + symbol_table_baset &_symbol_table, + function_may_throwt _function_may_throw, bool remove_added_instanceof) : symbol_table(_symbol_table), - exceptions_map(_exceptions_map), + function_may_throw(_function_may_throw), remove_added_instanceof(remove_added_instanceof) { } void operator()(goto_functionst &goto_functions); + void operator()(goto_programt &goto_program); protected: - symbol_tablet &symbol_table; - std::map> &exceptions_map; + symbol_table_baset &symbol_table; + function_may_throwt function_may_throw; bool remove_added_instanceof; symbol_exprt get_inflight_exception_global(); @@ -177,8 +179,7 @@ bool remove_exceptionst::function_or_callees_may_throw( "identifier expected to be a symbol"); const irep_idt &function_name= to_symbol_expr(function_expr).get_identifier(); - bool callee_may_throw = !exceptions_map[function_name].empty(); - if(callee_may_throw) + if(function_may_throw(function_name)) return true; } } @@ -424,9 +425,7 @@ void remove_exceptionst::instrument_function_call( const irep_idt &callee_id= to_symbol_expr(function_call.function()).get_identifier(); - bool callee_may_throw = !exceptions_map[callee_id].empty(); - - if(callee_may_throw) + if(function_may_throw(callee_id)) { add_exception_dispatch_sequence( goto_program, instr_it, stack_catch, locals); @@ -557,22 +556,58 @@ void remove_exceptionst::operator()(goto_functionst &goto_functions) instrument_exceptions(it->second.body); } +void remove_exceptionst::operator()(goto_programt &goto_program) +{ + instrument_exceptions(goto_program); +} + /// removes throws/CATCH-POP/CATCH-PUSH void remove_exceptions( - symbol_tablet &symbol_table, + symbol_table_baset &symbol_table, goto_functionst &goto_functions, remove_exceptions_typest type) { const namespacet ns(symbol_table); std::map> exceptions_map; uncaught_exceptions(goto_functions, ns, exceptions_map); + // NOLINTNEXTLINE + auto function_may_throw = [&exceptions_map](const irep_idt &id) { + return !exceptions_map[id].empty(); + }; remove_exceptionst remove_exceptions( symbol_table, - exceptions_map, + function_may_throw, type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF); remove_exceptions(goto_functions); } +/// removes throws/CATCH-POP/CATCH-PUSH from a single GOTO program, replacing +/// them with explicit exception propagation. +/// Note this is somewhat less accurate than the whole-goto-model version, +/// because we can't inspect other functions to determine whether they throw +/// or not, and therefore must assume they do and always introduce post-call +/// exception dispatch. +/// \param goto_program: program to remove exceptions from +/// \param symbol_table: global symbol table. The `@inflight_exception` global +/// may be added if not already present. It will not be initialised; that is +/// the caller's responsibility. +/// \param type: specifies whether instanceof operations generated by this pass +/// should be lowered to class-identifier comparisons (using +/// remove_instanceof). +void remove_exceptions( + goto_programt &goto_program, + symbol_table_baset &symbol_table, + remove_exceptions_typest type) +{ + auto any_function_may_throw = [](const irep_idt &id) { return true; }; + + remove_exceptionst remove_exceptions( + symbol_table, + any_function_may_throw, + type == remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF); + remove_exceptions(goto_program); +} + /// removes throws/CATCH-POP/CATCH-PUSH void remove_exceptions(goto_modelt &goto_model, remove_exceptions_typest type) { diff --git a/src/goto-programs/remove_exceptions.h b/src/goto-programs/remove_exceptions.h index 632559cbf91..20d83f93807 100644 --- a/src/goto-programs/remove_exceptions.h +++ b/src/goto-programs/remove_exceptions.h @@ -29,6 +29,12 @@ enum class remove_exceptions_typest DONT_REMOVE_INSTANCEOF, }; +void remove_exceptions( + goto_programt &goto_program, + symbol_table_baset &symbol_table, + remove_exceptions_typest type = + remove_exceptions_typest::DONT_REMOVE_INSTANCEOF); + void remove_exceptions( goto_modelt &goto_model, remove_exceptions_typest type = diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index bf226bb38f4..6f4ae143fed 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -58,8 +58,8 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) object_factory_parameters.string_printable = cmd.isset("string-printable"); if(cmd.isset("java-max-vla-length")) max_user_array_length=std::stoi(cmd.get_value("java-max-vla-length")); - if(cmd.isset("lazy-methods-context-sensitive")) - lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_SENSITIVE; + if(cmd.isset("symex-driven-lazy-loading")) + lazy_methods_mode=LAZY_METHODS_MODE_EXTERNAL_DRIVER; else if(cmd.isset("lazy-methods")) lazy_methods_mode=LAZY_METHODS_MODE_CONTEXT_INSENSITIVE; else @@ -814,6 +814,9 @@ void java_bytecode_languaget::methods_provided(id_sett &methods) const // Add all concrete methods to map for(const auto &kv : method_bytecode) methods.insert(kv.first); + // Add all synthetic methods to map + for(const auto &kv : synthetic_methods) + methods.insert(kv.first); } /// \brief Promote a lazy-converted method (one whose type is known but whose diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index dc708eef744..04a70935f37 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -63,7 +63,7 @@ enum lazy_methods_modet { LAZY_METHODS_MODE_EAGER, LAZY_METHODS_MODE_CONTEXT_INSENSITIVE, - LAZY_METHODS_MODE_CONTEXT_SENSITIVE + LAZY_METHODS_MODE_EXTERNAL_DRIVER }; class java_bytecode_languaget:public languaget diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp index 06d429287d5..eb5ba67b98e 100644 --- a/src/jbmc/jbmc_parse_options.cpp +++ b/src/jbmc/jbmc_parse_options.cpp @@ -48,7 +48,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include @@ -378,6 +377,22 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) cmdline.get_value("symex-coverage-report")); PARSE_OPTIONS_GOTO_TRACE(cmdline, options); + + if(cmdline.isset("symex-driven-lazy-loading")) + { + options.set_option("symex-driven-lazy-loading", true); + for(const char *opt : + { "nondet-static", + "full-slice", + "lazy-methods" }) + { + if(cmdline.isset(opt)) + { + throw std::string("Option ") + opt + + " can't be used with --symex-driven-lazy-loading"; + } + } + } } /// invoke main modules @@ -472,24 +487,7 @@ int jbmc_parse_optionst::doit() return 0; } - std::unique_ptr goto_model_ptr; - int get_goto_program_ret=get_goto_program(goto_model_ptr, options); - if(get_goto_program_ret!=-1) - return get_goto_program_ret; - - goto_modelt &goto_model = *goto_model_ptr; - - if(cmdline.isset("show-properties")) - { - show_properties( - goto_model, get_message_handler(), ui_message_handler.get_ui()); - return 0; // should contemplate EX_OK from sysexits.h - } - - if(set_properties(goto_model)) - return 7; // should contemplate EX_USAGE from sysexits.h - - std::function configure_bmc; + std::function configure_bmc = nullptr; if(options.get_bool_option("java-unwind-enum-static")) { configure_bmc = []( @@ -508,15 +506,76 @@ int jbmc_parse_optionst::doit() }); }; } + + if(!cmdline.isset("symex-driven-lazy-loading")) + { + std::unique_ptr goto_model_ptr; + int get_goto_program_ret=get_goto_program(goto_model_ptr, options); + if(get_goto_program_ret!=-1) + return get_goto_program_ret; + + goto_modelt &goto_model = *goto_model_ptr; + + if(cmdline.isset("show-properties")) + { + show_properties( + goto_model, get_message_handler(), ui_message_handler.get_ui()); + return 0; // should contemplate EX_OK from sysexits.h + } + + if(set_properties(goto_model)) + return 7; // should contemplate EX_USAGE from sysexits.h + + // The `configure_bmc` callback passed will enable enum-unwind-static if + // applicable. + return bmct::do_language_agnostic_bmc( + options, goto_model, ui_message_handler.get_ui(), *this, configure_bmc); + } else { - configure_bmc = []( - bmct &bmc, const symbol_tablet &symbol_table) { // NOLINT (*) - // NOOP + // Use symex-driven lazy loading: + lazy_goto_modelt lazy_goto_model=lazy_goto_modelt::from_handler_object( + *this, options, get_message_handler()); + lazy_goto_model.initialize(cmdline); + + // The precise wording of this error matches goto-symex's complaint when no + // __CPROVER_start exists (if we just go ahead and run it anyway it will + // trip an invariant when it tries to load it) + if(!lazy_goto_model.symbol_table.has_symbol(goto_functionst::entry_point())) + { + error() << "the program has no entry point"; + return 6; + } + + // Add failed symbols for any symbol created prior to loading any + // particular function: + add_failed_symbols(lazy_goto_model.symbol_table); + + // If applicable, parse the coverage instrumentation configuration, which + // will be used in process_goto_function: + cover_config = + get_cover_config( + options, lazy_goto_model.symbol_table, get_message_handler()); + + // Provide show-goto-functions and similar dump functions after symex + // executes. If --paths is active, these dump routines run after every + // paths iteration. Its return value indicates that if we ran any dump + // function, then we should skip the actual solver phase. + auto callback_after_symex = [this, &lazy_goto_model]() { // NOLINT (*) + return show_loaded_functions(lazy_goto_model); }; + + // The `configure_bmc` callback passed will enable enum-unwind-static if + // applicable. + return + bmct::do_language_agnostic_bmc( + options, + lazy_goto_model, + ui_message_handler.get_ui(), + *this, + configure_bmc, + callback_after_symex); } - return bmct::do_language_agnostic_bmc( - options, goto_model, ui_message_handler.get_ui(), *this, configure_bmc); } bool jbmc_parse_optionst::set_properties(goto_modelt &goto_model) @@ -643,6 +702,10 @@ void jbmc_parse_optionst::process_goto_function( journalling_symbol_tablet &symbol_table = function.get_symbol_table(); namespacet ns(symbol_table); goto_functionst::goto_functiont &goto_function = function.get_goto_function(); + + bool using_symex_driven_loading = + options.get_bool_option("symex-driven-lazy-loading"); + try { // Removal of RTTI inspection: @@ -650,6 +713,19 @@ void jbmc_parse_optionst::process_goto_function( // Java virtual functions -> explicit dispatch tables: remove_virtual_functions(function); + if(using_symex_driven_loading) + { + // remove exceptions + // If using symex-driven function loading we need to do this now so that + // symex doesn't have to cope with exception-handling constructs; however + // the results are slightly worse than running it in whole-program mode + // (e.g. dead catch sites will be retained) + remove_exceptions( + goto_function.body, + symbol_table, + remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF); + } + auto function_is_stub = [&symbol_table, &model](const irep_idt &id) { // NOLINT(*) return symbol_table.lookup_ref(id).value.is_nil() && @@ -699,6 +775,28 @@ void jbmc_parse_optionst::process_goto_function( symbol_table); } + // If using symex-driven function loading we must insert the coverage goals + // now so symex sees its targets; otherwise we leave this until + // process_goto_functions, as we haven't run remove_exceptions yet, and that + // pass alters the CFG. + if(using_symex_driven_loading) + { + // instrument cover goals + if(cmdline.isset("cover")) + { + INVARIANT( + cover_config != nullptr, "cover config should have been parsed"); + instrument_cover_goals(*cover_config, function, get_message_handler()); + } + + // label the assertions + label_properties(goto_function.body); + + goto_function.body.update(); + function.compute_location_numbers(); + goto_function.body.compute_loop_numbers(); + } + // update the function member in each instruction function.update_instructions_function(); } @@ -722,6 +820,50 @@ void jbmc_parse_optionst::process_goto_function( } } +bool jbmc_parse_optionst::show_loaded_functions( + const abstract_goto_modelt &goto_model) +{ + if(cmdline.isset("show-symbol-table")) + { + show_symbol_table( + goto_model.get_symbol_table(), ui_message_handler.get_ui()); + return true; + } + + if(cmdline.isset("show-loops")) + { + show_loop_ids(ui_message_handler.get_ui(), goto_model.get_goto_functions()); + return true; + } + + if( + cmdline.isset("show-goto-functions") || + cmdline.isset("list-goto-functions")) + { + namespacet ns(goto_model.get_symbol_table()); + show_goto_functions( + ns, + get_message_handler(), + ui_message_handler.get_ui(), + goto_model.get_goto_functions(), + cmdline.isset("list-goto-functions")); + return true; + } + + if(cmdline.isset("show-properties")) + { + namespacet ns(goto_model.get_symbol_table()); + show_properties( + ns, + get_message_handler(), + ui_message_handler.get_ui(), + goto_model.get_goto_functions()); + return true; + } + + return false; +} + bool jbmc_parse_optionst::process_goto_functions( goto_modelt &goto_model, const optionst &options) @@ -729,7 +871,17 @@ bool jbmc_parse_optionst::process_goto_functions( try { status() << "Running GOTO functions transformation passes" << eom; - // remove catch and throw (introduces instanceof but request it is removed) + + bool using_symex_driven_loading = + options.get_bool_option("symex-driven-lazy-loading"); + + // When using symex-driven lazy loading, *all* relevant processing is done + // during process_goto_function, so we have nothing to do here. + if(using_symex_driven_loading) + return false; + + // remove catch and throw + // (introduces instanceof but request it is removed) remove_exceptions( goto_model, remove_exceptions_typest::REMOVE_ADDED_INSTANCEOF); @@ -865,6 +1017,8 @@ void jbmc_parse_optionst::help() // This one is handled by jbmc_parse_options not by the Java frontend, // hence its presence here: " --java-unwind-enum-static try to unwind loops in static initialization of enums\n" // NOLINT(*) + // Currently only supported in the JBMC frontend: + " --symex-driven-lazy-loading only load functions when first entered by symbolic execution\n" // NOLINT(*) "\n" "BMC options:\n" HELP_BMC diff --git a/src/jbmc/jbmc_parse_options.h b/src/jbmc/jbmc_parse_options.h index a2e2aa1cdcd..874a988cbdb 100644 --- a/src/jbmc/jbmc_parse_options.h +++ b/src/jbmc/jbmc_parse_options.h @@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include @@ -72,7 +73,8 @@ class optionst; JAVA_BYTECODE_LANGUAGE_OPTIONS \ "(java-unwind-enum-static)" \ "(localize-faults)(localize-faults-method):" \ - OPT_GOTO_TRACE + OPT_GOTO_TRACE \ + "(symex-driven-lazy-loading)" // clang-format on class jbmc_parse_optionst: @@ -97,11 +99,13 @@ class jbmc_parse_optionst: protected: ui_message_handlert ui_message_handler; + std::unique_ptr cover_config; void eval_verbosity(); void get_command_line_options(optionst &); int get_goto_program( std::unique_ptr &goto_model, const optionst &); + bool show_loaded_functions(const abstract_goto_modelt &goto_model); bool set_properties(goto_modelt &goto_model); };