goto traces now show pretty function names #3194

kroening · 2018-10-17T19:02:17Z

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
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.
White-space or formatting changes outside the feature-related changed lines are in commits of their own.

tautschnig

There is one (in my opinion: major) issue I have commented on below. Other than that I think we should consider moving this kind of code to source_locationt rather than doing it in here as the very same should be useful in other places as well.

tautschnig · 2018-10-17T19:19:17Z

src/goto-programs/goto_trace.cpp

+    out << ' ';
+
+    const symbolt *function_symbol;
+    if(ns.lookup(source_location.get_function(), function_symbol))


I think this is sort of a type error: source_location.get_function() is what may be in the source code, but need not match what we use for symbol names. It may work, but I think we should not encourage more of this sort.

allredj

Passed Diffblue compatibility checks (cbmc commit: 34f9ec1).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/88312033

kroening · 2018-10-20T18:23:08Z

Now with different approach, but same goal.

tautschnig · 2018-10-20T18:57:57Z

This reminds me of #2149 (review). We should probably turn this into a concerted effort.

smowton · 2018-10-21T06:07:04Z

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -856,7 +856,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
    code_declt declare_cloned(local_symexpr);

    source_locationt location;
-    location.set_function(local_name);
+    location.set_function(local_symbol.pretty_name);


This isn't a function name (clone_symbol refers to a function name in this case)

smowton · 2018-10-21T06:12:13Z

Surely pretty vs., full name choices should be made in the pretty-printer rather than chosen when making the function symbols to begin with? goto_tracet::output has the namespace available, so if goto_tracet::stept::function_identifier was always a canonical name (i.e. in the namespace) that would seem like a natural place to choose to go for a particular representation

kroening · 2018-10-21T12:19:01Z

Some discussion in #2149

kroening · 2018-10-22T16:13:56Z

The current view is that the function (pretty name or identifier) should not be in source_locationt.
I.e., I will do a third, and entirely different approach to the goal of this PR.

kroening · 2018-10-23T09:59:18Z

A problem with that view is that gcc (not clang) prints error messages such as this:

x3.cpp: In function 'int main()':
x3.cpp:3:3: error: 'z' was not declared in this scope
   z;
   ^

This suggests use the pretty name.

kroening · 2018-11-05T15:22:22Z

Here's yet another, completely new approach.

kroening · 2018-11-05T15:23:02Z

Please only review last commit.

tautschnig · 2018-11-05T15:25:58Z

src/goto-programs/goto_trace.cpp

+  {
+    if(!result.empty())
+      result += ' ';
+    result += " line " + id2string(source_location.get_line());


Remove the extra space before line

tautschnig · 2018-11-05T15:26:57Z

src/goto-programs/goto_trace.cpp

@@ -335,7 +366,10 @@ void show_full_goto_trace(
        out << '\n';
        out << messaget::red << "Violated property:" << messaget::reset << '\n';
        if(!step.pc->source_location.is_nil())
-          out << "  " << step.pc->source_location << '\n';
+        {
+          out << "  " << state_location(step, ns) << '\n';


This will now have an extra thread number but I suppose that's ok.

Yes; did contemplate that, and decided that this is desirable. There may well be a context switch just before the failing assertion.

allredj

⚠️
Diffblue compatibility check is currently unavailable.
Please create manual bump.
(cbmc commit: 9375710).
Build URL: https://travis-ci.com/diffblue/test-gen/builds/90721202

kroening added the enhancement label Oct 17, 2018

kroening requested review from peterschrammel, pkesseli, smowton and tautschnig as code owners October 17, 2018 19:02

tautschnig reviewed Oct 17, 2018

View reviewed changes

kroening force-pushed the trace-function-name branch from 34db084 to 34f9ec1 Compare October 17, 2018 19:32

allredj reviewed Oct 17, 2018

View reviewed changes

tautschnig assigned kroening Oct 18, 2018

kroening force-pushed the trace-function-name branch from 34f9ec1 to 2d954a2 Compare October 20, 2018 18:22

kroening requested review from cesaro, cristina-david, NathanJPhillips and thk123 as code owners October 20, 2018 18:22

kroening assigned smowton and unassigned kroening Oct 20, 2018

smowton reviewed Oct 21, 2018

View reviewed changes

kroening force-pushed the trace-function-name branch from 2d954a2 to 0610eaf Compare November 5, 2018 15:22

kroening assigned tautschnig Nov 5, 2018

tautschnig reviewed Nov 5, 2018

View reviewed changes

smowton approved these changes Nov 5, 2018

View reviewed changes

kroening force-pushed the trace-function-name branch from 0610eaf to 1c44079 Compare November 5, 2018 15:37

kroening force-pushed the trace-function-name branch from 1c44079 to 1c4af7c Compare November 5, 2018 15:41

tautschnig assigned kroening and peterschrammel and unassigned smowton Nov 5, 2018

kroening force-pushed the trace-function-name branch 2 times, most recently from 0a08ee6 to 121ab0c Compare November 8, 2018 13:20

kroening unassigned kroening, tautschnig and peterschrammel Nov 8, 2018

use display_name() to show function in goto traces

9375710

kroening force-pushed the trace-function-name branch from 121ab0c to 9375710 Compare November 8, 2018 13:52

allredj reviewed Nov 8, 2018

View reviewed changes

kroening merged commit 4ecd33c into develop Nov 8, 2018

kroening deleted the trace-function-name branch November 8, 2018 15:16

goto traces now show pretty function names #3194

goto traces now show pretty function names #3194

Uh oh!

Conversation

kroening commented Oct 17, 2018

Uh oh!

tautschnig left a comment

Choose a reason for hiding this comment

Uh oh!

tautschnig Oct 17, 2018

Choose a reason for hiding this comment

Uh oh!

allredj left a comment

Choose a reason for hiding this comment

Uh oh!

kroening commented Oct 20, 2018

Uh oh!

tautschnig commented Oct 20, 2018

Uh oh!

smowton Oct 21, 2018

Choose a reason for hiding this comment

Uh oh!

smowton commented Oct 21, 2018

Uh oh!

kroening commented Oct 21, 2018

Uh oh!

kroening commented Oct 22, 2018

Uh oh!

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

Uh oh!

Uh oh!

kroening commented Nov 5, 2018

Uh oh!

kroening commented Nov 5, 2018

Uh oh!

tautschnig Nov 5, 2018

Choose a reason for hiding this comment

Uh oh!

kroening Nov 5, 2018

Choose a reason for hiding this comment

Uh oh!

tautschnig Nov 5, 2018

Choose a reason for hiding this comment

Uh oh!

kroening Nov 5, 2018

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 Oct 23, 2018 •

edited

Loading