added --compact-trace option

Daniel Kroening · Daniel Kroening · commit b62ffe9fa286 · 2018-11-28T17:18:18.000-08:00
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.
diff --git a/regression/cbmc/compact-trace/main.c b/regression/cbmc/compact-trace/main.c
@@ -0,0 +1,14 @@
+int x;
+
+int bar(int bar_a)
+{
+  x = 2;
+  x++;
+  __CPROVER_assert(0, "assertion");
+}
+
+int main()
+{
+  x = 1;
+  bar(0);
+}
diff --git a/regression/cbmc/compact-trace/test.desc b/regression/cbmc/compact-trace/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--compact-trace
+activate-multi-line-match
+^EXIT=10$
+^SIGNAL=0$
+^↳ main\.c:10 main\(\)\n  12: x=1 .*$
+^↳ main.c:13 bar\(0\)\n  13: bar_a=0 .*\n  5: x=2 .*\n  6: x=3 .*$
+--
+^warning: ignoring
diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests
@@ -112,6 +112,7 @@ rm byte_update6/test.desc
 rm byte_update7/test.desc
 rm byte_update8/test.desc
 rm byte_update9/test.desc
+rm compact-trace/test.desc
 rm dynamic_size1/stack_object.desc
 rm equality_through_array1/test.desc
 rm equality_through_array2/test.desc
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -201,9 +201,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("stop-on-fail", true);
 
   if(
-    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"))
+  {
     options.set_option("trace", true);
+  }
 
   if(cmdline.isset("localize-faults"))
     options.set_option("localize-faults", true);
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
@@ -264,7 +264,7 @@ void trace_value(
   if(lhs_object.has_value())
     identifier=lhs_object->get_identifier();
 
-  out << "  " << from_expr(ns, identifier, full_lhs) << '=';
+  out << from_expr(ns, identifier, full_lhs) << '=';
 
   if(value.is_nil())
     out << "(assignment removed)";
@@ -348,6 +348,136 @@ bool is_index_member_symbol(const exprt &src)
     return false;
 }
 
+/// \brief show a compact variant of the goto trace on the console
+/// \param out the output stream
+/// \param ns the namespace
+/// \param goto_trace the trace to be shown
+/// \param options any options, e.g., numerical representation
+void show_compact_goto_trace(
+  messaget::mstreamt &out,
+  const namespacet &ns,
+  const goto_tracet &goto_trace,
+  const trace_optionst &options)
+{
+  std::size_t function_depth = 0;
+
+  for(const auto &step : goto_trace.steps)
+  {
+    if(step.is_function_call())
+      function_depth++;
+    else if(step.is_function_return())
+      function_depth--;
+
+    // hide the hidden ones
+    if(step.hidden)
+      continue;
+
+    switch(step.type)
+    {
+    case goto_trace_stept::typet::ASSERT:
+      if(!step.cond_value)
+      {
+        out << '\n';
+        out << messaget::red << "Violated property:" << messaget::reset << '\n';
+        if(!step.pc->source_location.is_nil())
+          out << "  " << state_location(step, ns) << '\n';
+
+        out << "  " << messaget::red << step.comment << messaget::reset << '\n';
+
+        if(step.pc->is_assert())
+          out << "  " << from_expr(ns, step.function, step.pc->guard) << '\n';
+
+        out << '\n';
+      }
+      break;
+
+    case goto_trace_stept::typet::ASSIGNMENT:
+      if(
+        step.assignment_type ==
+        goto_trace_stept::assignment_typet::ACTUAL_PARAMETER)
+      {
+        break;
+      }
+
+      out << "  ";
+
+      if(!step.pc->source_location.get_line().empty())
+      {
+        out << messaget::faint << step.pc->source_location.get_line() << ':'
+            << messaget::reset << ' ';
+      }
+
+      trace_value(
+        out,
+        ns,
+        step.get_lhs_object(),
+        step.full_lhs,
+        step.full_lhs_value,
+        options);
+      break;
+
+    case goto_trace_stept::typet::FUNCTION_CALL:
+      // downwards arrow
+      out << '\n' << messaget::faint << u8"\u21b3" << messaget::reset << ' ';
+      if(!step.pc->source_location.get_file().empty())
+      {
+        out << messaget::faint << step.pc->source_location.get_file();
+
+        if(!step.pc->source_location.get_line().empty())
+        {
+          out << messaget::faint << ':' << step.pc->source_location.get_line();
+        }
+
+        out << messaget::reset << ' ';
+      }
+
+      {
+        // show the display name
+        const auto &f_symbol = ns.lookup(step.called_function);
+        out << f_symbol.display_name();
+      }
+
+      out << '(';
+
+      {
+        bool first = true;
+        for(auto &arg : step.function_arguments)
+        {
+          if(first)
+            first = false;
+          else
+            out << ", ";
+
+          out << from_expr(ns, step.function, arg);
+        }
+      }
+      out << ")\n";
+      break;
+
+    case goto_trace_stept::typet::FUNCTION_RETURN:
+      // upwards arrow
+      out << messaget::faint << u8"\u21b5" << messaget::reset << '\n';
+      break;
+
+    case goto_trace_stept::typet::ASSUME:
+    case goto_trace_stept::typet::LOCATION:
+    case goto_trace_stept::typet::GOTO:
+    case goto_trace_stept::typet::DECL:
+    case goto_trace_stept::typet::OUTPUT:
+    case goto_trace_stept::typet::INPUT:
+    case goto_trace_stept::typet::SPAWN:
+    case goto_trace_stept::typet::MEMORY_BARRIER:
+    case goto_trace_stept::typet::ATOMIC_BEGIN:
+    case goto_trace_stept::typet::ATOMIC_END:
+    case goto_trace_stept::typet::DEAD:
+      break;
+
+    default:
+      UNREACHABLE;
+    }
+  }
+}
+
 void show_full_goto_trace(
   messaget::mstreamt &out,
   const namespacet &ns,
@@ -419,13 +549,14 @@ void show_full_goto_trace(
           show_state_header(out, ns, step, step.step_nr, options);
         }
 
-       trace_value(
-         out,
-         ns,
-         step.get_lhs_object(),
-         step.full_lhs,
-         step.full_lhs_value,
-         options);
+        out << "  ";
+        trace_value(
+          out,
+          ns,
+          step.get_lhs_object(),
+          step.full_lhs,
+          step.full_lhs_value,
+          options);
       }
       break;
 
@@ -437,6 +568,7 @@ void show_full_goto_trace(
         show_state_header(out, ns, step, step.step_nr, options);
       }
 
+      out << "  ";
       trace_value(
         out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
       break;
@@ -623,6 +755,8 @@ void show_goto_trace(
 {
   if(options.stack_trace)
     show_goto_stack_trace(out, ns, goto_trace);
+  else if(options.compact_trace)
+    show_compact_goto_trace(out, ns, goto_trace, options);
   else
     show_full_goto_trace(out, ns, goto_trace, options);
 }
diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h
@@ -200,6 +200,7 @@ struct trace_optionst
   bool base_prefix;
   bool show_function_calls;
   bool show_code;
+  bool compact_trace;
   bool stack_trace;
 
   static const trace_optionst default_options;
@@ -211,6 +212,7 @@ struct trace_optionst
     base_prefix = hex_representation;
     show_function_calls = options.get_bool_option("trace-show-function-calls");
     show_code = options.get_bool_option("trace-show-code");
+    compact_trace = options.get_bool_option("compact-trace");
     stack_trace = options.get_bool_option("stack-trace");
   };
 
@@ -222,6 +224,7 @@ struct trace_optionst
     base_prefix = false;
     show_function_calls = false;
     show_code = false;
+    compact_trace = false;
     stack_trace = false;
   };
 };
@@ -250,13 +253,15 @@ void trace_value(
   "(trace-show-function-calls)"                                                \
   "(trace-show-code)"                                                          \
   "(trace-hex)"                                                                \
+  "(compact-trace)"                                                            \
   "(stack-trace)"
 
 #define HELP_GOTO_TRACE                                                        \
   " --trace-json-extended        add rawLhs property to trace\n"               \
   " --trace-show-function-calls  show function calls in plain trace\n"         \
   " --trace-show-code            show original code in plain trace\n"          \
   " --trace-hex                  represent plain trace values in hex\n"        \
+  " --compact-trace              give a compact trace\n"                       \
   " --stack-trace                give a stack trace only\n"
 
 #define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)                             \
@@ -268,6 +273,8 @@ void trace_value(
     options.set_option("trace-show-code", true);                               \
   if(cmdline.isset("trace-hex"))                                               \
     options.set_option("trace-hex", true);                                     \
+  if(cmdline.isset("compact-trace"))                                           \
+    options.set_option("compact-trace", true);                                 \
   if(cmdline.isset("stack-trace"))                                             \
     options.set_option("stack-trace", true);
 
