Refinement iteration printing #5237
Conversation
thk123
requested review from
chrisr-diffblue,
kroening,
pkesseli,
smowton and
tautschnig
as code owners
thk123
force-pushed
the
refinement-iteration-printing
branch
from
3faf008 to
c20f285
Compare
| @@ -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_xml) | |||
There was a problem hiding this comment.
I guess the name could be made more accurate.
| @@ -10,6 +10,7 @@ | |||
| #define CPROVER_GOTO_CHECKER_SYMEX_BMC_INCREMENTAL_ONE_LOOP_H | |||
|
|
|||
| #include "symex_bmc.h" | |||
| #include <util/ui_message.h> | |||
There was a problem hiding this comment.
Guess you don't need this one anymore.
There was a problem hiding this comment.
Needed for ui_message_handlert::uit declaration
thk123
force-pushed
the
refinement-iteration-printing
branch
from
c20f285 to
89203e2
Compare
|
@xbauch comments addressed |
| xmlt xml("current-unwinding"); | ||
| xml.data = std::to_string(unwind); | ||
| log.statistics() << xml; | ||
| } |
There was a problem hiding this comment.
Could we also output a current-unwinding item for PLAIN and JSON_UI? So the same information is output independent of the ui.
thk123
force-pushed
the
refinement-iteration-printing
branch
from
eb4bef2 to
019afa7
Compare
| const std::string unwind_num = std::to_string(unwind); | ||
| switch(output_ui) | ||
| { | ||
| case ui_message_handlert::uit::PLAIN: |
There was a problem hiding this comment.
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
There was a problem hiding this comment.
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
I'm not totally convinced by my approach for finding out whether XML is turned on. I'm not really clear on why you can't always just pipe some xml to the message handler, and let it figure out what to do with it. (Ideally, for example, if you send xml to json-ui, then it outputs equivalent json)Went for something much simpler, might raise a seperate PR to make the handling of this stuff less ad-hoc.