Merge pull request diffblue#2516 from polgreen/cbmc_trace_options

extend plain trace to show function calls and returns

Author: Daniel Kroening

regression/cbmc/trace_show_code/main.c

@@ -0,0 +1,23 @@
+int function_to_call(int a)
+{
+	int local = 1;
+	return a+local;
+}
+
+
+int main()
+{
+	int a, c;
+	unsigned int b;
+	a = 0;
+	c = -100;
+	a = function_to_call(a) + function_to_call(c);
+	if(a < 0)
+	  b = function_to_call(b);
+
+	if(c < 0)
+	  b = -function_to_call(b);
+
+	__CPROVER_assert(0,"");
+
+}

regression/cbmc/trace_show_code/test.desc

@@ -0,0 +1,19 @@
+CORE
+main.c
+--trace --trace-show-code
+^EXIT=10$
+^SIGNAL=0$
+local = 1
+int a
+int c
+unsigned int b
+a = 0;
+c = -100;
+function_to_call\(a\)
+function_to_call\(c\)
+a = return_value_function_to_call \+ return_value_function_to_call
+function_to_call\(\(signed int\)b\)
+b = \(unsigned int\)return_value_function_to_call
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/trace_show_function_calls/main.c

@@ -0,0 +1,22 @@
+int function_to_call(int a)
+{
+	int local = 1;
+	return a+local;
+}
+
+
+int main()
+{
+	int a;
+	unsigned int b;
+	a = 0;
+	a = -100;
+	a = 2147483647;
+	b = a*2;
+	a = -2147483647;
+	a = function_to_call(a);
+	b = function_to_call(b);
+	
+	__CPROVER_assert(0,"");
+
+}

regression/cbmc/trace_show_function_calls/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--trace --trace-show-function-calls
+^EXIT=10$
+^SIGNAL=0$
+Function call: function_to_call \(depth 2\)
+Function return: function_to_call \(depth 1\)
+Function call: function_to_call \(depth 2\)
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/goto-programs/goto_trace.cpp

@@ -247,20 +247,30 @@ void trace_value(
 
 void show_state_header(
   std::ostream &out,
+  const namespacet &ns,
   const goto_trace_stept &state,
   const source_locationt &source_location,
-  unsigned step_nr)
+  unsigned step_nr,
+  const trace_optionst &options)
 {
   out << "\n";
 
-  if(step_nr==0)
+  if(step_nr == 0)
     out << "Initial State";
   else
     out << "State " << step_nr;
 
-  out << " " << source_location
-      << " thread " << state.thread_nr << "\n";
-  out << "----------------------------------------------------" << "\n";
+  out << " " << source_location << " thread " << state.thread_nr << "\n";
+  out << "----------------------------------------------------"
+      << "\n";
+
+  if(options.show_code)
+  {
+    out << as_string(ns, *state.pc)
+        << "\n";
+    out << "----------------------------------------------------"
+        << "\n";
+  }
 }
 
 bool is_index_member_symbol(const exprt &src)
@@ -283,6 +293,7 @@ void show_goto_trace(
 {
   unsigned prev_step_nr=0;
   bool first_step=true;
+  std::size_t function_depth=0;
 
   for(const auto &step : goto_trace.steps)
   {
@@ -341,7 +352,8 @@ void show_goto_trace(
         {
           first_step=false;
           prev_step_nr=step.step_nr;
-          show_state_header(out, step, step.pc->source_location, step.step_nr);
+          show_state_header(
+            out, ns, step, step.pc->source_location, step.step_nr, options);
         }
 
         // see if the full lhs is something clean
@@ -369,7 +381,8 @@ void show_goto_trace(
       {
         first_step=false;
         prev_step_nr=step.step_nr;
-        show_state_header(out, step, step.pc->source_location, step.step_nr);
+        show_state_header(
+          out, ns, step, step.pc->source_location, step.step_nr, options);
       }
 
       trace_value(
@@ -386,7 +399,8 @@ void show_goto_trace(
       }
       else
       {
-        show_state_header(out, step, step.pc->source_location, step.step_nr);
+        show_state_header(
+          out, ns, step, step.pc->source_location, step.step_nr, options);
         out << "  OUTPUT " << step.io_id << ":";
 
         for(std::list<exprt>::const_iterator
@@ -407,7 +421,8 @@ void show_goto_trace(
       break;
 
     case goto_trace_stept::typet::INPUT:
-      show_state_header(out, step, step.pc->source_location, step.step_nr);
+      show_state_header(
+        out, ns, step, step.pc->source_location, step.step_nr, options);
       out << "  INPUT " << step.io_id << ":";
 
       for(std::list<exprt>::const_iterator
@@ -427,7 +442,17 @@ void show_goto_trace(
       break;
 
     case goto_trace_stept::typet::FUNCTION_CALL:
+      function_depth++;
+      if(options.show_function_calls)
+        out << "\n#### Function call: " << step.identifier << " (depth "
+            << function_depth << ") ####\n";
+      break;
     case goto_trace_stept::typet::FUNCTION_RETURN:
+      function_depth--;
+      if(options.show_function_calls)
+        out << "\n#### Function return: " << step.identifier << " (depth "
+            << function_depth << ") ####\n";
+      break;
     case goto_trace_stept::typet::SPAWN:
     case goto_trace_stept::typet::MEMORY_BARRIER:
     case goto_trace_stept::typet::ATOMIC_BEGIN:

src/goto-programs/goto_trace.h

@@ -200,6 +200,8 @@ struct trace_optionst
   bool json_full_lhs;
   bool hex_representation;
   bool base_prefix;
+  bool show_function_calls;
+  bool show_code;
 
   static const trace_optionst default_options;
 
@@ -208,6 +210,8 @@ struct trace_optionst
     json_full_lhs = options.get_bool_option("trace-json-extended");
     hex_representation = options.get_bool_option("trace-hex");
     base_prefix = hex_representation;
+    show_function_calls = options.get_bool_option("trace-show-function-calls");
+    show_code = options.get_bool_option("trace-show-code");
   };
 
 private:
@@ -216,6 +220,8 @@ struct trace_optionst
     json_full_lhs = false;
     hex_representation = false;
     base_prefix = false;
+    show_function_calls = false;
+    show_code = false;
   };
 };
 
@@ -239,15 +245,23 @@ void trace_value(
 
 
 #define OPT_GOTO_TRACE "(trace-json-extended)" \
+                       "(trace-show-function-calls)" \
+                       "(trace-show-code)" \
                        "(trace-hex)"
 
 #define HELP_GOTO_TRACE                                                        \
-  " --trace-json-extended        add rawLhs property to trace\n"              \
+  " --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"
 
 #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-hex"))                                               \
     options.set_option("trace-hex", true);