cbmc can now print stack traces

Author: kroening

regression/cbmc/stack-trace/main.c

@@ -0,0 +1,15 @@
+int foo(int foo_a)
+{
+  __CPROVER_assert(foo_a != 2, "assertion");
+}
+
+int bar(int bar_a)
+{
+  foo(bar_a + 1);
+  foo(bar_a + 2);
+}
+
+int main()
+{
+  bar(0);
+}

regression/cbmc/stack-trace/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--stack-trace
+^EXIT=10$
+^SIGNAL=0$
+^  assertion failure file main.c line 3 .*$
+^  main\(\)
+^  bar\(0\)
+^  foo\(2\)
+--
+^warning: ignoring

src/cbmc/cbmc_parse_options.cpp

@@ -201,8 +201,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
      cmdline.isset("outfile"))
     options.set_option("stop-on-fail", true);
 
-  if(cmdline.isset("trace") ||
-     cmdline.isset("stop-on-fail"))
+  if(
+    cmdline.isset("trace") || cmdline.isset("stack-trace") ||
+    cmdline.isset("stop-on-fail"))
     options.set_option("trace", true);
 
   if(cmdline.isset("localize-faults"))

src/goto-programs/goto_trace.cpp

@@ -285,7 +285,7 @@ bool is_index_member_symbol(const exprt &src)
     return false;
 }
 
-void show_goto_trace(
+void show_full_goto_trace(
   std::ostream &out,
   const namespacet &ns,
   const goto_tracet &goto_trace,
@@ -488,6 +488,94 @@ void show_goto_trace(
   }
 }
 
+void show_goto_stack_trace(
+  std::ostream &out,
+  const namespacet &ns,
+  const goto_tracet &goto_trace,
+  const trace_optionst &options)
+{
+  // map from thread number to a call stack
+  std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
+    call_stacks;
+
+  // by default, we show thread 0
+  unsigned thread_to_show = 0;
+
+  for(auto s_it = goto_trace.steps.begin(); s_it != goto_trace.steps.end();
+      s_it++)
+  {
+    const auto &step = *s_it;
+    auto &stack = call_stacks[step.thread_nr];
+
+    if(step.is_assert())
+    {
+      if(!step.cond_value)
+      {
+        stack.push_back(s_it);
+        thread_to_show = step.thread_nr;
+      }
+    }
+    else if(step.is_function_call())
+    {
+      stack.push_back(s_it);
+    }
+    else if(step.is_function_return())
+    {
+      stack.pop_back();
+    }
+  }
+
+  const auto &stack = call_stacks[thread_to_show];
+
+  // print in reverse order
+  for(auto s_it = stack.rbegin(); s_it != stack.rend(); s_it++)
+  {
+    const auto &step = **s_it;
+    if(step.is_assert())
+    {
+      out << "  assertion failure";
+      if(!step.pc->source_location.is_nil())
+        out << ' ' << step.pc->source_location;
+      out << '\n';
+    }
+    else if(step.is_function_call())
+    {
+      out << "  " << step.function_identifier;
+      out << '(';
+
+      bool first = true;
+      for(auto &arg : step.function_arguments)
+      {
+        if(first)
+          first = false;
+        else
+          out << ", ";
+
+        out << from_expr(ns, step.function_identifier, arg);
+      }
+
+      out << ')';
+
+      if(!step.pc->source_location.is_nil())
+        out << ' ' << step.pc->source_location;
+
+      out << '\n';
+    }
+  }
+}
+
+void show_goto_trace(
+  std::ostream &out,
+  const namespacet &ns,
+  const goto_tracet &goto_trace,
+  const trace_optionst &options)
+{
+  if(options.stack_trace)
+    show_goto_stack_trace(out, ns, goto_trace, options);
+  else
+    show_full_goto_trace(out, ns, goto_trace, options);
+}
+
 void show_goto_trace(
   std::ostream &out,
   const namespacet &ns,

src/goto-programs/goto_trace.h

@@ -205,6 +205,7 @@ struct trace_optionst
   bool base_prefix;
   bool show_function_calls;
   bool show_code;
+  bool stack_trace;
 
   static const trace_optionst default_options;
 
@@ -215,6 +216,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");
+    stack_trace = options.get_bool_option("stack-trace");
   };
 
 private:
@@ -225,6 +227,7 @@ struct trace_optionst
     base_prefix = false;
     show_function_calls = false;
     show_code = false;
+    stack_trace = false;
   };
 };
 
@@ -246,27 +249,30 @@ void trace_value(
   const exprt &full_lhs,
   const exprt &value);
 
-
-#define OPT_GOTO_TRACE "(trace-json-extended)" \
-                       "(trace-show-function-calls)" \
-                       "(trace-show-code)" \
-                       "(trace-hex)"
+#define OPT_GOTO_TRACE                                                         \
+  "(trace-json-extended)"                                                      \
+  "(trace-show-function-calls)"                                                \
+  "(trace-show-code)"                                                          \
+  "(trace-hex)"                                                                \
+  "(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"
+  " --trace-hex                  represent plain trace values in hex\n"        \
+  " --stack-trace                give a stack trace only\n"
 
 #define PARSE_OPTIONS_GOTO_TRACE(cmdline, options)                             \
   if(cmdline.isset("trace-json-extended"))                                     \
     options.set_option("trace-json-extended", true);                           \
   if(cmdline.isset("trace-show-function-calls"))                               \
     options.set_option("trace-show-function-calls", true);                     \
-  if(cmdline.isset("trace-show-code"))                                       \
-      options.set_option("trace-show-code", true);                             \
+  if(cmdline.isset("trace-show-code"))                                         \
+    options.set_option("trace-show-code", true);                               \
   if(cmdline.isset("trace-hex"))                                               \
-    options.set_option("trace-hex", true);
-
+    options.set_option("trace-hex", true);                                     \
+  if(cmdline.isset("stack-trace"))                                             \
+    options.set_option("stack-trace", true);
 
 #endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H