From 320da328ef22a0621375d4969ad85170332c72f0 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Wed, 29 Apr 2020 16:40:31 +0100 Subject: [PATCH 1/7] Add tests verifying the incremental status is output --- regression/cbmc-incr-oneloop/alarm2/test-json-output.desc | 1 + regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc | 1 + regression/cbmc-incr-oneloop/alarm2/test.desc | 6 ++++++ 3 files changed, 8 insertions(+) diff --git a/regression/cbmc-incr-oneloop/alarm2/test-json-output.desc b/regression/cbmc-incr-oneloop/alarm2/test-json-output.desc index 0e8d52fad24..904c5d51283 100644 --- a/regression/cbmc-incr-oneloop/alarm2/test-json-output.desc +++ b/regression/cbmc-incr-oneloop/alarm2/test-json-output.desc @@ -5,5 +5,6 @@ main.c ^SIGNAL=0$ "messageText": "VERIFICATION FAILED" "currentUnwinding": 1 +"incrementalStatus": "INCONCLUSIVE" -- ^warning: ignoring diff --git a/regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc b/regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc index 90a3dfe16e2..c967c1fb2db 100644 --- a/regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc +++ b/regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc @@ -6,5 +6,6 @@ main.c VERIFICATION FAILED 1 1 +INCONCLUSIVE -- ^warning: ignoring diff --git a/regression/cbmc-incr-oneloop/alarm2/test.desc b/regression/cbmc-incr-oneloop/alarm2/test.desc index 2c5f198ab70..576ae8bac92 100644 --- a/regression/cbmc-incr-oneloop/alarm2/test.desc +++ b/regression/cbmc-incr-oneloop/alarm2/test.desc @@ -1,9 +1,15 @@ CORE main.c --incremental-loop main.0 --unwind-min 5 --unwind-max 10 +activate-multi-line-match Current unwinding: 1 +Incremental status: INCONCLUSIVE +Current unwinding: 5\nUnwinding .*\nIncremental status: INCONCLUSIVE +Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -- ^warning: ignoring +-- +The multi-line match is added to verify that an incremental status is printed immediately after each unwinding From d4c5e9952c091e7ffd54c0698c445b82c3f9d9df Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Wed, 29 Apr 2020 17:20:47 +0100 Subject: [PATCH 2/7] Tests for incremental status with multiple properties The incremental status should report failure from the first unwinding for which one property is falsified. --- .../multiple-asserts/test-no-cp.desc | 19 +++++++++++++++++++ .../cbmc-incr-oneloop/multiple-asserts/test.c | 9 +++++++++ .../multiple-asserts/test.desc | 17 +++++++++++++++++ 3 files changed, 45 insertions(+) create mode 100644 regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc create mode 100644 regression/cbmc-incr-oneloop/multiple-asserts/test.c create mode 100644 regression/cbmc-incr-oneloop/multiple-asserts/test.desc diff --git a/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc b/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc new file mode 100644 index 00000000000..d581fd8198f --- /dev/null +++ b/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc @@ -0,0 +1,19 @@ +CORE +test.c +--incremental-loop main.0 --no-propagation +activate-multi-line-match +Current unwinding: 1\nUnwinding .*\nIncremental status: INCONCLUSIVE +Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE +Current unwinding: 7\nUnwinding .*\nIncremental status: FAILURE +Current unwinding: 9\nUnwinding .*\nIncremental status: FAILURE +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +-- +Ensure that with multiple properties, the incremental status +switches to failure as soon as one property has been falsified +but keeps unwinding till it has resolved them all + +Use `--no-propagation` to ensure that even the output is the same regardless of whether the asserts are checked via the solver or the constant propagator diff --git a/regression/cbmc-incr-oneloop/multiple-asserts/test.c b/regression/cbmc-incr-oneloop/multiple-asserts/test.c new file mode 100644 index 00000000000..b59f9ef2ad5 --- /dev/null +++ b/regression/cbmc-incr-oneloop/multiple-asserts/test.c @@ -0,0 +1,9 @@ +int main() +{ + for(int i = 0; i < 10; ++i) + { + assert(i != 5); + assert(i != 8); + } + return 0; +} diff --git a/regression/cbmc-incr-oneloop/multiple-asserts/test.desc b/regression/cbmc-incr-oneloop/multiple-asserts/test.desc new file mode 100644 index 00000000000..56cefb5161f --- /dev/null +++ b/regression/cbmc-incr-oneloop/multiple-asserts/test.desc @@ -0,0 +1,17 @@ +CORE +test.c +--incremental-loop main.0 +activate-multi-line-match +Current unwinding: 1\nUnwinding .*\nIncremental status: INCONCLUSIVE +Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE +Current unwinding: 7\nUnwinding .*\nIncremental status: FAILURE +Current unwinding: 9\nUnwinding .*\nIncremental status: FAILURE +^EXIT=10$ +^SIGNAL=0$ +^VERIFICATION FAILED$ +-- +^warning: ignoring +-- +Ensure that with multiple properties, the incremental status +switches to failure as soon as one property has been falsified +but keeps unwinding till it has resolved them all From 22bce6fc6eceb58496130774382f9eee07811ccf Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Wed, 22 Apr 2020 18:24:19 +0100 Subject: [PATCH 3/7] Print incremental-status when doing incremental solving It is not possible to conclude successful verification before the unwinding has finished, so this prints inconclusive until the analysis is complete. However, if one property has been falsified, then even though the analysis can continue to check other properties, the verification will certainly fail. --- .../single_loop_incremental_symex_checker.cpp | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/src/goto-checker/single_loop_incremental_symex_checker.cpp b/src/goto-checker/single_loop_incremental_symex_checker.cpp index 0c2e12770f7..ee3eef4db11 100644 --- a/src/goto-checker/single_loop_incremental_symex_checker.cpp +++ b/src/goto-checker/single_loop_incremental_symex_checker.cpp @@ -47,6 +47,23 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert( prop_conv_solver->set_all_frozen(); } +void output_incremental_status( + const propertiest &properties, + messaget &message_hander) +{ + const auto any_failures = std::any_of( + properties.begin(), + properties.end(), + [](const std::pair &property) { + return property.second.status == property_statust::FAIL; + }); + std::string status = any_failures ? "FAILURE" : "INCONCLUSIVE"; + structured_datat incremental_status{ + {{labelt({"incremental", "status"}), + structured_data_entryt::data_node(json_stringt(status))}}}; + message_hander.statistics() << incremental_status; +} + incremental_goto_checkert::resultt single_loop_incremental_symex_checkert:: operator()(propertiest &properties) { @@ -64,6 +81,8 @@ operator()(propertiest &properties) update_properties_status_from_symex_target_equation( properties, result.updated_properties, equation); + output_incremental_status(properties, log); + initial_equation_generated = true; } @@ -162,6 +181,8 @@ operator()(propertiest &properties) properties, result.updated_properties, equation); current_equation_converted = false; + + output_incremental_status(properties, log); } return result; From fdbbf7e8f2c892e4a20c61ecd2d747649eb481d6 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 1 May 2020 18:13:59 +0100 Subject: [PATCH 4/7] Tweak where we print the incremental status We want to print the status after we've done any solving for that unwind, but before we've done an extra step of symexing. We should not print in the event the full equation has been generated, as then we have a full solution so ins't incremental. Ditto we don't need to print the status if we've found a failure, as this function will be called again to do the next symex invocation if there are further propreties to check --- src/goto-checker/single_loop_incremental_symex_checker.cpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/goto-checker/single_loop_incremental_symex_checker.cpp b/src/goto-checker/single_loop_incremental_symex_checker.cpp index ee3eef4db11..e4fae0efa07 100644 --- a/src/goto-checker/single_loop_incremental_symex_checker.cpp +++ b/src/goto-checker/single_loop_incremental_symex_checker.cpp @@ -81,8 +81,6 @@ operator()(propertiest &properties) update_properties_status_from_symex_target_equation( properties, result.updated_properties, equation); - output_incremental_status(properties, log); - initial_equation_generated = true; } @@ -171,6 +169,8 @@ operator()(propertiest &properties) break; } + output_incremental_status(properties, log); + // We continue symbolic execution full_equation_generated = !symex.resume(goto_symext::get_goto_function(goto_model)); @@ -181,8 +181,6 @@ operator()(propertiest &properties) properties, result.updated_properties, equation); current_equation_converted = false; - - output_incremental_status(properties, log); } return result; From 0e6cfbf190eff86f117049dd8ed7d7ee415b345e Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 1 May 2020 18:15:06 +0100 Subject: [PATCH 5/7] Adapt tests for printing We now print after all solving, and the last thing before the next increment, therefore the printing checks are easier to check immediately precedes the next unwinding, rather than checking appears after the increment we are talking about. --- regression/cbmc-incr-oneloop/alarm1/test.desc | 2 ++ regression/cbmc-incr-oneloop/alarm2/test.desc | 4 ++-- .../cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc | 7 +++---- regression/cbmc-incr-oneloop/multiple-asserts/test.desc | 7 +++---- 4 files changed, 10 insertions(+), 10 deletions(-) diff --git a/regression/cbmc-incr-oneloop/alarm1/test.desc b/regression/cbmc-incr-oneloop/alarm1/test.desc index 70a9179b47d..87b0754ad15 100644 --- a/regression/cbmc-incr-oneloop/alarm1/test.desc +++ b/regression/cbmc-incr-oneloop/alarm1/test.desc @@ -1,8 +1,10 @@ CORE main.c --incremental-loop main.0 --unwind-max 15 +activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ +Incremental status: INCONCLUSIVE\nCurrent unwinding: 15 -- ^warning: ignoring diff --git a/regression/cbmc-incr-oneloop/alarm2/test.desc b/regression/cbmc-incr-oneloop/alarm2/test.desc index 576ae8bac92..e36848a5583 100644 --- a/regression/cbmc-incr-oneloop/alarm2/test.desc +++ b/regression/cbmc-incr-oneloop/alarm2/test.desc @@ -4,8 +4,8 @@ main.c activate-multi-line-match Current unwinding: 1 Incremental status: INCONCLUSIVE -Current unwinding: 5\nUnwinding .*\nIncremental status: INCONCLUSIVE -Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE +Incremental status: INCONCLUSIVE\nCurrent unwinding: 6 +Incremental status: INCONCLUSIVE\nCurrent unwinding: 7 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc b/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc index d581fd8198f..6eff8fddefd 100644 --- a/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc +++ b/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc @@ -2,10 +2,9 @@ CORE test.c --incremental-loop main.0 --no-propagation activate-multi-line-match -Current unwinding: 1\nUnwinding .*\nIncremental status: INCONCLUSIVE -Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE -Current unwinding: 7\nUnwinding .*\nIncremental status: FAILURE -Current unwinding: 9\nUnwinding .*\nIncremental status: FAILURE +Incremental status: INCONCLUSIVE\nCurrent unwinding: 2 +Incremental status: INCONCLUSIVE\nCurrent unwinding: 6 +Incremental status: FAILURE\nCurrent unwinding: 7 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc-incr-oneloop/multiple-asserts/test.desc b/regression/cbmc-incr-oneloop/multiple-asserts/test.desc index 56cefb5161f..11e06f6d641 100644 --- a/regression/cbmc-incr-oneloop/multiple-asserts/test.desc +++ b/regression/cbmc-incr-oneloop/multiple-asserts/test.desc @@ -2,10 +2,9 @@ CORE test.c --incremental-loop main.0 activate-multi-line-match -Current unwinding: 1\nUnwinding .*\nIncremental status: INCONCLUSIVE -Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE -Current unwinding: 7\nUnwinding .*\nIncremental status: FAILURE -Current unwinding: 9\nUnwinding .*\nIncremental status: FAILURE +Incremental status: INCONCLUSIVE\nCurrent unwinding: 2 +Incremental status: INCONCLUSIVE\nCurrent unwinding: 6 +Incremental status: FAILURE\nCurrent unwinding: 7 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ From 3f6f0ca56ad90a9d1e6f9e09a7859a921f3635ef Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 1 May 2020 18:15:36 +0100 Subject: [PATCH 6/7] Add tests for when the program verifies In this case, the status is inconclusive until completion, at which point success will be reported by CBMC overall. --- .../cbmc-incr-oneloop/valid-asserts/test.c | 8 ++++++++ .../cbmc-incr-oneloop/valid-asserts/test.desc | 16 ++++++++++++++++ 2 files changed, 24 insertions(+) create mode 100644 regression/cbmc-incr-oneloop/valid-asserts/test.c create mode 100644 regression/cbmc-incr-oneloop/valid-asserts/test.desc diff --git a/regression/cbmc-incr-oneloop/valid-asserts/test.c b/regression/cbmc-incr-oneloop/valid-asserts/test.c new file mode 100644 index 00000000000..6654dc75460 --- /dev/null +++ b/regression/cbmc-incr-oneloop/valid-asserts/test.c @@ -0,0 +1,8 @@ +int main() +{ + for(int i = 0; i < 10; ++i) + { + assert(i != 10); + } + return 0; +} diff --git a/regression/cbmc-incr-oneloop/valid-asserts/test.desc b/regression/cbmc-incr-oneloop/valid-asserts/test.desc new file mode 100644 index 00000000000..36ddf206c3a --- /dev/null +++ b/regression/cbmc-incr-oneloop/valid-asserts/test.desc @@ -0,0 +1,16 @@ +CORE +test.c +--incremental-loop main.0 +activate-multi-line-match +Incremental status: INCONCLUSIVE\nCurrent unwinding: 2 +Incremental status: INCONCLUSIVE\nCurrent unwinding: 10 +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +^warning: ignoring +Incremental status: SUCCESS +-- +Check that for valid asserts, the incremental status is inconclusive +as it is only after the incrementer has been stopped we conclude is +verified. From 4972f5491793e888bf491bb601d3e0efe17ac129 Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Fri, 1 May 2020 18:19:54 +0100 Subject: [PATCH 7/7] Add test to check for no incremental status when no properties to check --- regression/cbmc-incr-oneloop/no-asserts/test.c | 8 ++++++++ regression/cbmc-incr-oneloop/no-asserts/test.desc | 11 +++++++++++ 2 files changed, 19 insertions(+) create mode 100644 regression/cbmc-incr-oneloop/no-asserts/test.c create mode 100644 regression/cbmc-incr-oneloop/no-asserts/test.desc diff --git a/regression/cbmc-incr-oneloop/no-asserts/test.c b/regression/cbmc-incr-oneloop/no-asserts/test.c new file mode 100644 index 00000000000..1acd435d55a --- /dev/null +++ b/regression/cbmc-incr-oneloop/no-asserts/test.c @@ -0,0 +1,8 @@ +int main() +{ + for(int i = 0; i < 10; ++i) + { + } + // nothing to check + return 0; +} diff --git a/regression/cbmc-incr-oneloop/no-asserts/test.desc b/regression/cbmc-incr-oneloop/no-asserts/test.desc new file mode 100644 index 00000000000..a5c2f27a5d6 --- /dev/null +++ b/regression/cbmc-incr-oneloop/no-asserts/test.desc @@ -0,0 +1,11 @@ +CORE +test.c +--incremental-loop main.0 +activate-multi-line-match +^EXIT=0$ +^SIGNAL=0$ +VERIFICATION SUCCESSFUL +-- +Incremental status +-- +Verify no incremental status updates when no properties to check