Skip to content

Refinement iteration printing #5237

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 3 commits into from
Feb 21, 2020
Merged

Refinement iteration printing #5237

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
6eaec29
Adding in printing code for each unwind
Feb 18, 2020
89203e2
Add test for checking the xml output contains required nodes
Feb 20, 2020
019afa7
Extend the printing to be enabled for both json and plain text ouput
Feb 20, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 9 additions & 0 deletions regression/cbmc-incr-oneloop/alarm2/test-json-output.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
10 changes: 10 additions & 0 deletions regression/cbmc-incr-oneloop/alarm2/test-xml-output.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
main.c
--incremental-loop main.0 --unwind-min 5 --unwind-max 10 --xml-ui
^EXIT=10$
^SIGNAL=0$
<text>VERIFICATION FAILED</text>
<current-unwinding>1</current-unwinding>
<refinement-iteration>1</refinement-iteration>
--
^warning: ignoring
1 change: 1 addition & 0 deletions regression/cbmc-incr-oneloop/alarm2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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$
Expand Down
3 changes: 2 additions & 1 deletion src/goto-checker/single_loop_incremental_symex_checker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
34 changes: 32 additions & 2 deletions src/goto-checker/symex_bmc_incremental_one_loop.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand All @@ -33,7 +34,8 @@ symex_bmc_incremental_one_loopt::symex_bmc_incremental_one_loopt(
: std::numeric_limits<unsigned>::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 &&
Expand All @@ -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
Expand Down Expand Up @@ -85,6 +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();

log_unwinding(unwind);
log.statistics() << (abort ? "Not unwinding" : "Unwinding") << " loop " << id
<< " iteration " << unwind;

Expand Down Expand Up @@ -131,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:
Copy link
Contributor

@chrisr-diffblue chrisr-diffblue Feb 20, 2020 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I know there are a few other places in the codebase where this sort of switch happens, so I'm not going to block this PR on this issue :-) But it's really ugly in general... I'm wondering if we could come up with an API extension to message handlers. Perhaps some pseudo code like this:

/// Individual implementations inside message handlers
keyValueMessagePair(string[] words, string value) {
/// words == ["current","unwinding"]
/// output would be:
/// "Current unwinding: value" for PLAIN
/// xmlt xml("current-unwinding"); xml.data = value; for XML
/// json_objectt json; json["currentUnwinding"] = json_numbert(value); for JSON
}

// then as a client, we could just use:
log.statistics() << output_ui.keyValueMessagePair(["current","unwinding"],unwind) << messaget::eom;

Obviously suitable C++ plumbing needed :-) - but hopefully that explains the idea

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes I started having a go at making just a general way of logging structured data, but didn't want to hold up this PR for t

{
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;
}
}
}
8 changes: 7 additions & 1 deletion src/goto-checker/symex_bmc_incremental_one_loop.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@
#define CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H

#include "symex_bmc.h"
#include <util/ui_message.h>
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Guess you don't need this one anymore.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Needed for ui_message_handlert::uit declaration


class symex_bmc_incremental_one_loopt : public symex_bmct
{
Expand All @@ -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(
Expand All @@ -44,6 +46,10 @@ class symex_bmc_incremental_one_loopt : public symex_bmct
const symex_targett::sourcet &source,
const call_stackt &context,
unsigned unwind) override;

void log_unwinding(unsigned unwind);

ui_message_handlert::uit output_ui;
};

#endif // CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H