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-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..e36848a5583 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 +Incremental status: INCONCLUSIVE\nCurrent unwinding: 6 +Incremental status: INCONCLUSIVE\nCurrent unwinding: 7 ^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 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..6eff8fddefd --- /dev/null +++ b/regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc @@ -0,0 +1,18 @@ +CORE +test.c +--incremental-loop main.0 --no-propagation +activate-multi-line-match +Incremental status: INCONCLUSIVE\nCurrent unwinding: 2 +Incremental status: INCONCLUSIVE\nCurrent unwinding: 6 +Incremental status: FAILURE\nCurrent unwinding: 7 +^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..11e06f6d641 --- /dev/null +++ b/regression/cbmc-incr-oneloop/multiple-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: 6 +Incremental status: FAILURE\nCurrent unwinding: 7 +^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 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 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. diff --git a/src/goto-checker/single_loop_incremental_symex_checker.cpp b/src/goto-checker/single_loop_incremental_symex_checker.cpp index 0c2e12770f7..e4fae0efa07 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) { @@ -152,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));