formatting of debug output of traces #2182
Conversation
kroening
requested review from
peterschrammel,
smowton and
tautschnig
as code owners
kroening
force-pushed
the
trace-debug
branch
2 times, most recently
from
8ac8620 to
eff2e51
Compare
src/goto-programs/goto_trace.cpp
Outdated
| @@ -149,6 +134,10 @@ std::string trace_value_binary( | |||
| if(!to_integer(expr, i) && i>=0) | |||
| return integer2string(i, 2); | |||
| } | |||
| else if(type.id()==ID_string) | |||
| { | |||
| return integer2string(expr.get(ID_value).get_no(), 2); | |||
There was a problem hiding this comment.
This doesn't work with USE_STD_STRING enabled: https://travis-ci.org/diffblue/cbmc/jobs/378446491#L1421
|
|
||
| out << "\n"; | ||
| out << pc->type << '\n'; |
There was a problem hiding this comment.
Why is this one changed but the switch statement at the top of this method isn't?
There was a problem hiding this comment.
Switching over something different!
src/goto-programs/goto_trace.h
Outdated
| @@ -104,14 +104,18 @@ class goto_trace_stept | |||
| // for assert | |||
| std::string comment; | |||
|
|
|||
| // the object being assigned | |||
| // The object being assigned. | |||
| // This will get removed, use full_lhs instead. | |||
| ssa_exprt lhs_object; | |||
There was a problem hiding this comment.
What is blocking immediate removal?
There was a problem hiding this comment.
They are still being output to the XML output, and I am unsure whether there are still any users of this. I have been warning about this for ~3 years.
There was a problem hiding this comment.
The motivation for removal is that the full object may be huge (think of a large array of a big struct). Various users have raised the sheer size of the XMLs as a concern.
There was a problem hiding this comment.
The introduced comment suggests that there equivalent replacements. If that isn't the case (which is what your comments here suggest), then the comment needs to be fixed.
There was a problem hiding this comment.
They are equivalent in the sense that you can reconstruct the lhs_object value from the full_lhs values; same for lhs_object and lhs.
There was a problem hiding this comment.
So ... that should be done?
There was a problem hiding this comment.
Ok, will drop this commit, and will do a separate PR for the removal.
There was a problem hiding this comment.
Makes a lot of sense, thanks!
| if(!comment.empty()) | ||
| out << " " << comment << '\n'; | ||
|
|
||
| out << " " << format(pc->guard) << '\n'; |
There was a problem hiding this comment.
I'm not convinced there is value in making the debug output language-independent when the plain-text user-directed output is and should remain language-specific? Clarified by @peterschrammel's comment.
|
I think that we should make a clear distinction between output that is GOTO and output that is language-specific. We are sometimes a bit fooled by the similarity of GOTO and C, but for Java this is no more the case and language-specific output is indeed required by downstream tools. This mostly concerns the structured (JSON, XML) outputs of goto traces. (Non-front-end) debug output should always be GOTO. For all other output functions, we should provide them with a formatter function supplied by the driver program, as @kroening suggests. The driver program can then decide whether to call format() or a language-specific version of it. Hard-coded calls to from_expr/format should be replaced by that. |
|
To add, some of the "debug output" methods could likely be replaced by a "generic output" method that then gets given format_expr as the formatter. On the side, we will eventually need a uniform name for a "debug output" method. |
da61186 Merge pull request diffblue#2182 from diffblue/trace-debug 5acf313 Merge pull request diffblue#2176 from mgudemann/fix/glucose_build_g++ e82dca0 formatting of debug output of traces f891f37 Merge pull request diffblue#2168 from JohnDumbell/bugfix/phi_merge_uninitialized 6faf376 Enable 'm' flag on regex for multi-line tests 646cf29 Add nondet assignment to non-zero'd allocations in symex 213db5f Remove trailing `;` from namespace closing bracket git-subtree-dir: cbmc git-subtree-split: da61186
This does minor tweaks to the debug output of goto_traces; in particular, this now uses format().