added --compact-trace option [blocks: #3459] #3458

kroening · 2018-11-24T15:30:30Z

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

regression/cbmc/compact-trace/test.desc

tautschnig · 2018-11-24T16:47:25Z

src/goto-programs/goto_trace.cpp

+        // show pretty name until first '('
+        const auto &f_symbol = ns.lookup(step.called_function);
+        const auto display_name = id2string(f_symbol.display_name());
+        const std::size_t open_par_pos = display_name.find('(');


What's the idea behind this filtering?

A pretty name might be some_function(int, int); we want to show some_function(123, 456)

Why would the symbol's name include the type of the arguments? Is that in case of templates? But then operator() would not be handled correctly. I feel I'm missing something.

Ok, will drop for now

tautschnig · 2018-11-24T16:48:01Z

src/goto-programs/goto_trace.cpp

+  const trace_optionst &options)
+{
+//  unsigned prev_step_nr=0;
+//  bool first_step=true;


tautschnig · 2018-11-24T16:50:58Z

src/goto-symex/symex_function_call.cpp

@@ -125,7 +125,21 @@ void goto_symext::parameter_assignments(
        }
      }

-      symex_assign(state, code_assignt(lhs, rhs));
+      assignment_typet assignment_type;


In #3459 it says that this PR might be a candidate to test this, but there isn't a test here either?

Now there! (Note absence of assignments to parameters in the trace).

The test just seems to test what should be there, but does not have any pattern describing strings that should not occur (other than the usual "warning: ignoring")?!

Ok, will revert to the state without #3459, and will then add the test there (after this one here is merged). The diff is then obvious.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: cfc1954).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92451767

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: bc61922).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92461159

tautschnig

Various minor notes, otherwise looks ok.

tautschnig · 2018-11-28T13:54:40Z

src/goto-programs/goto_trace.cpp

+      if(
+        step.assignment_type ==
+        goto_trace_stept::assignment_typet::ACTUAL_PARAMETER)
+        break;


Braces, please.

tautschnig · 2018-11-28T13:54:52Z

src/cbmc/cbmc_parse_options.cpp

-    cmdline.isset("trace") || cmdline.isset("stack-trace") ||
-    cmdline.isset("stop-on-fail"))
+    cmdline.isset("trace") || cmdline.isset("compact-trace") ||
+    cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail"))


Please add braces for readability.

tautschnig · 2018-11-28T13:55:32Z

src/goto-programs/goto_trace.cpp

+        if(!step.pc->source_location.is_nil())
+        {
+          out << "  " << state_location(step, ns) << '\n';
+        }


No braces needed (usually a nit pick, but here it's inconsistent with a few lines further down).

tautschnig · 2018-11-28T13:57:24Z

src/goto-programs/goto_trace.cpp

+      {
+        // show pretty name
+        const auto &f_symbol = ns.lookup(step.called_function);
+        out << f_symbol.display_name();


Actually the above comment might just add confusion: symbolt has a pretty_name...

tautschnig · 2018-11-28T13:58:06Z

src/goto-programs/goto_trace.cpp

+    case goto_trace_stept::typet::CONSTRAINT:
+    case goto_trace_stept::typet::SHARED_READ:
+    case goto_trace_stept::typet::SHARED_WRITE:
+    default:


This shouldn't be necessary.

peterschrammel · 2018-11-28T21:25:46Z

src/goto-programs/goto_trace.cpp

+
+    case goto_trace_stept::typet::FUNCTION_CALL:
+      // downwards arrow
+      out << "\n" << messaget::faint << u8"\u21b3" << messaget::reset << ' ';


could be '\n'

peterschrammel · 2018-11-28T21:37:59Z

src/goto-programs/goto_trace.cpp

+      out << '(';
+
+      {
+        bool first = true;


💡
The pattern is very simple, but given the number of times we have this in the code base, it could be worth introducing something like this:

join( step.function_arguments.begin(), step.function_arguments.end(), [](arg) {out << from_expr(ns, step.function, arg);}, []() {out << ", ";});

I think you can already do this:

auto arg_strings = make_range(step.function_arguments).map<std::string>( [&this](const exprt &arg) { return from_expr(ns, step.function, e); }); join_strings(out, arg_strings.begin(), arg_strings.end(), ", ");

And if the above works we should likely use it in lots of places :-)

The range type doesn't have a difference_type, and thus, that doesn't work.

Separate PR.

This offers a denser way of viewing traces. The rationale is that traces are getting longer; furthermore, the new format makes it easier to spot function calls and the actual function parameters.

allredj

✔️
Passed Diffblue compatibility checks (cbmc commit: b62ffe9).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/92941108

kroening added the enhancement label Nov 24, 2018

kroening requested review from peterschrammel, pkesseli, smowton and tautschnig as code owners November 24, 2018 15:30

kroening mentioned this pull request Nov 24, 2018

bugfix: set assignment type for actual parameters correctly #3459

Merged

2 tasks

kroening force-pushed the compact-trace branch 2 times, most recently from 847d368 to 36768b6 Compare November 24, 2018 16:19

tautschnig reviewed Nov 24, 2018

View reviewed changes

kroening force-pushed the compact-trace branch 2 times, most recently from 0a87ae5 to cfc1954 Compare November 24, 2018 22:28

allredj reviewed Nov 24, 2018

View reviewed changes

kroening force-pushed the compact-trace branch from cfc1954 to bc61922 Compare November 25, 2018 09:00

kroening assigned tautschnig Nov 25, 2018

allredj reviewed Nov 25, 2018

View reviewed changes

tautschnig approved these changes Nov 28, 2018

View reviewed changes

tautschnig assigned kroening and unassigned tautschnig Nov 28, 2018

tautschnig changed the title ~~added --compact-trace option~~ added --compact-trace option [blocks: #3459] Nov 28, 2018

tautschnig added the blocker label Nov 28, 2018

kroening force-pushed the compact-trace branch 2 times, most recently from 7603bec to 3b3e027 Compare November 28, 2018 21:22

peterschrammel approved these changes Nov 28, 2018

View reviewed changes

kroening force-pushed the compact-trace branch from 3b3e027 to 005bc12 Compare November 28, 2018 21:47

added --compact-trace option

b62ffe9

This offers a denser way of viewing traces. The rationale is that traces are getting longer; furthermore, the new format makes it easier to spot function calls and the actual function parameters.

kroening force-pushed the compact-trace branch from 005bc12 to b62ffe9 Compare November 29, 2018 01:18

kroening merged commit 31060e1 into develop Nov 29, 2018

kroening deleted the compact-trace branch November 29, 2018 02:03

allredj reviewed Nov 29, 2018

View reviewed changes

added --compact-trace option [blocks: #3459] #3458

added --compact-trace option [blocks: #3459] #3458

Uh oh!

Conversation

kroening commented Nov 24, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

kroening commented Nov 24, 2018 •

edited

Loading