From 6eaec293af111d6cab4c1f40f20f820629945668 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 18 Feb 2020 18:30:08 +0000 Subject: [PATCH 1/3] Adding in printing code for each unwind --- .../single_loop_incremental_symex_checker.cpp | 3 ++- .../symex_bmc_incremental_one_loop.cpp | 15 +++++++++++++-- src/goto-checker/symex_bmc_incremental_one_loop.h | 6 +++++- 3 files changed, 20 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 2c473d2aff7..0c2e12770f7 100644 --- a/src/goto-checker/single_loop_incremental_symex_checker.cpp +++ b/src/goto-checker/single_loop_incremental_symex_checker.cpp @@ -34,7 +34,8 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert( equation, options, path_storage, - guard_manager), + guard_manager, + ui_message_handler.get_ui()), property_decider(options, ui_message_handler, equation, ns) { setup_symex(symex, ns, options, ui_message_handler); diff --git a/src/goto-checker/symex_bmc_incremental_one_loop.cpp b/src/goto-checker/symex_bmc_incremental_one_loop.cpp index 1e10f4e7c88..5d508f05be7 100644 --- a/src/goto-checker/symex_bmc_incremental_one_loop.cpp +++ b/src/goto-checker/symex_bmc_incremental_one_loop.cpp @@ -19,7 +19,8 @@ symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt( symex_target_equationt &target, const optionst &options, path_storaget &path_storage, - guard_managert &guard_manager) + guard_managert &guard_manager, + ui_message_handlert::uit output_ui) : symex_bmct( message_handler, outer_symbol_table, @@ -33,7 +34,8 @@ symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt( : std::numeric_limits::max()), incr_min_unwind( options.is_set("unwind-min") ? options.get_signed_int_option("unwind-min") - : 0) + : 0), + output_ui(output_ui) { ignore_assertions = incr_min_unwind >= 1 && @@ -56,6 +58,7 @@ bool symex_bmc_incremental_one_loopt::should_stop_unwind( this_loop_limit = incr_max_unwind; if(unwind + 1 >= incr_min_unwind) ignore_assertions = false; + abort_unwind_decision = tvt(unwind >= this_loop_limit); } else @@ -85,6 +88,14 @@ bool symex_bmc_incremental_one_loopt::should_stop_unwind( abort_unwind_decision.is_known(), "unwind decision should be taken by now"); bool abort = abort_unwind_decision.is_true(); + + if(output_ui == ui_message_handlert::uit::XML_UI) + { + xmlt xml("current-unwinding"); + xml.data = std::to_string(unwind); + log.statistics() << xml; + } + log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id << " iteration " << unwind; diff --git a/src/goto-checker/symex_bmc_incremental_one_loop.h b/src/goto-checker/symex_bmc_incremental_one_loop.h index d3c0726d31b..6f45d3b959b 100644 --- a/src/goto-checker/symex_bmc_incremental_one_loop.h +++ b/src/goto-checker/symex_bmc_incremental_one_loop.h @@ -10,6 +10,7 @@ #define CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H #include "symex_bmc.h" +#include class symex_bmc_incremental_one_loopt : public symex_bmct { @@ -20,7 +21,8 @@ class symex_bmc_incremental_one_loopt : public symex_bmct symex_target_equationt &, const optionst &, path_storaget &, - guard_managert &); + guard_managert &, + ui_message_handlert::uit output_ui); /// Return true if symex can be resumed bool from_entry_point_of( @@ -44,6 +46,8 @@ class symex_bmc_incremental_one_loopt : public symex_bmct const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) override; + + ui_message_handlert::uit output_ui; }; #endif // CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H From 89203e2692c67b5bc93627605047f0ead2b18937 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 20 Feb 2020 10:37:48 +0000 Subject: [PATCH 2/3] Add test for checking the xml output contains required nodes --- .../cbmc-incr-oneloop/alarm2/test-xml-output.desc | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc diff --git a/regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc b/regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc new file mode 100644 index 00000000000..90a3dfe16e2 --- /dev/null +++ b/regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc @@ -0,0 +1,10 @@ +CORE +main.c +--incremental-loop main.0 --unwind-min 5 --unwind-max 10 --xml-ui +^EXIT=10$ +^SIGNAL=0$ +VERIFICATION FAILED +1 +1 +-- +^warning: ignoring From 019afa75a7c64c0ffaf3bfa278dd2b483137c7b2 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 20 Feb 2020 13:18:28 +0000 Subject: [PATCH 3/3] Extend the printing to be enabled for both json and plain text ouput --- .../alarm2/test-json-output.desc | 9 +++++ regression/cbmc-incr-oneloop/alarm2/test.desc | 1 + .../symex_bmc_incremental_one_loop.cpp | 35 ++++++++++++++----- .../symex_bmc_incremental_one_loop.h | 2 ++ 4 files changed, 39 insertions(+), 8 deletions(-) create mode 100644 regression/cbmc-incr-oneloop/alarm2/test-json-output.desc diff --git a/regression/cbmc-incr-oneloop/alarm2/test-json-output.desc b/regression/cbmc-incr-oneloop/alarm2/test-json-output.desc new file mode 100644 index 00000000000..0e8d52fad24 --- /dev/null +++ b/regression/cbmc-incr-oneloop/alarm2/test-json-output.desc @@ -0,0 +1,9 @@ +CORE +main.c +--incremental-loop main.0 --unwind-min 5 --unwind-max 10 --json-ui +^EXIT=10$ +^SIGNAL=0$ +"messageText": "VERIFICATION FAILED" +"currentUnwinding": 1 +-- +^warning: ignoring diff --git a/regression/cbmc-incr-oneloop/alarm2/test.desc b/regression/cbmc-incr-oneloop/alarm2/test.desc index 817773abe11..2c5f198ab70 100644 --- a/regression/cbmc-incr-oneloop/alarm2/test.desc +++ b/regression/cbmc-incr-oneloop/alarm2/test.desc @@ -1,6 +1,7 @@ CORE main.c --incremental-loop main.0 --unwind-min 5 --unwind-max 10 +Current unwinding: 1 ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/src/goto-checker/symex_bmc_incremental_one_loop.cpp b/src/goto-checker/symex_bmc_incremental_one_loop.cpp index 5d508f05be7..32b6156d98e 100644 --- a/src/goto-checker/symex_bmc_incremental_one_loop.cpp +++ b/src/goto-checker/symex_bmc_incremental_one_loop.cpp @@ -88,14 +88,7 @@ bool symex_bmc_incremental_one_loopt::should_stop_unwind( abort_unwind_decision.is_known(), "unwind decision should be taken by now"); bool abort = abort_unwind_decision.is_true(); - - if(output_ui == ui_message_handlert::uit::XML_UI) - { - xmlt xml("current-unwinding"); - xml.data = std::to_string(unwind); - log.statistics() << xml; - } - + log_unwinding(unwind); log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id << " iteration " << unwind; @@ -142,3 +135,29 @@ bool symex_bmc_incremental_one_loopt::resume( return should_pause_symex; } +void symex_bmc_incremental_one_loopt::log_unwinding(unsigned unwind) +{ + const std::string unwind_num = std::to_string(unwind); + switch(output_ui) + { + case ui_message_handlert::uit::PLAIN: + { + log.statistics() << "Current unwinding: " << unwind_num << messaget::eom; + break; + } + case ui_message_handlert::uit::XML_UI: + { + xmlt xml("current-unwinding"); + xml.data = unwind_num; + log.statistics() << xml << messaget::eom; + break; + } + case ui_message_handlert::uit::JSON_UI: + { + json_objectt json; + json["currentUnwinding"] = json_numbert(unwind_num); + log.statistics() << json << messaget::eom; + break; + } + } +} diff --git a/src/goto-checker/symex_bmc_incremental_one_loop.h b/src/goto-checker/symex_bmc_incremental_one_loop.h index 6f45d3b959b..9c3bc7ed14e 100644 --- a/src/goto-checker/symex_bmc_incremental_one_loop.h +++ b/src/goto-checker/symex_bmc_incremental_one_loop.h @@ -47,6 +47,8 @@ class symex_bmc_incremental_one_loopt : public symex_bmct const call_stackt &context, unsigned unwind) override; + void log_unwinding(unsigned unwind); + ui_message_handlert::uit output_ui; };