Merge pull request #2819 from diffblue/trace-with-arguments2

goto_trace now contains the arguments of function calls

Author: Daniel Kroening

regression/cbmc/trace_show_function_calls/test.desc

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

src/goto-programs/goto_trace.cpp

@@ -444,15 +444,34 @@ void show_goto_trace(
     case goto_trace_stept::typet::FUNCTION_CALL:
       function_depth++;
       if(options.show_function_calls)
-        out << "\n#### Function call: " << step.function_identifier
-            << " (depth " << function_depth << ") ####\n";
+      {
+        out << "\n#### Function call: " << 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 << ") (depth " << function_depth << ") ####\n";
+      }
       break;
+
     case goto_trace_stept::typet::FUNCTION_RETURN:
       function_depth--;
       if(options.show_function_calls)
+      {
         out << "\n#### Function return: " << step.function_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

@@ -122,6 +122,9 @@ class goto_trace_stept
   // for function call/return
   irep_idt function_identifier;
 
+  // for function call
+  std::vector<exprt> function_arguments;
+
   /*! \brief outputs the trace step in ASCII to a given stream
   */
   void output(

src/goto-symex/build_goto_trace.cpp

@@ -304,12 +304,17 @@ void build_goto_trace(
       {
         goto_trace_step.lhs_object.make_nil();
       }
+
       goto_trace_step.type = SSA_step.type;
       goto_trace_step.hidden = SSA_step.hidden;
       goto_trace_step.format_string = SSA_step.format_string;
       goto_trace_step.io_id = SSA_step.io_id;
       goto_trace_step.formatted = SSA_step.formatted;
       goto_trace_step.function_identifier = SSA_step.function_identifier;
+      goto_trace_step.function_arguments = SSA_step.converted_function_arguments;
+
+      for(auto &arg : goto_trace_step.function_arguments)
+        arg = prop_conv.get(arg);
 
       // update internal field for specific variables in the counterexample
       update_internal_field(SSA_step, goto_trace_step, ns);

src/goto-symex/symex_function_call.cpp

@@ -254,8 +254,14 @@ void goto_symext::symex_function_call_code(
     return;
   }
 
+  // read the arguments -- before the locality renaming
+  exprt::operandst arguments = call.arguments();
+  for(auto &a : arguments)
+    state.rename(a, ns);
+
   // record the call
-  target.function_call(state.guard.as_expr(), identifier, state.source);
+  target.function_call(
+    state.guard.as_expr(), identifier, arguments, state.source);
 
   if(!goto_function.body_available())
   {
@@ -276,11 +282,6 @@ void goto_symext::symex_function_call_code(
     return;
   }
 
-  // read the arguments -- before the locality renaming
-  exprt::operandst arguments=call.arguments();
-  for(auto &a : arguments)
-    state.rename(a, ns);
-
   // produce a new frame
   PRECONDITION(!state.call_stack().empty());
   goto_symex_statet::framet &frame=state.new_frame();

src/goto-symex/symex_target.h

@@ -105,7 +105,8 @@ class symex_targett
   virtual void function_call(
     const exprt &guard,
     const irep_idt &function_identifier,
-    const sourcet &source)=0;
+    const std::vector<exprt> &ssa_function_arguments,
+    const sourcet &source) = 0;
 
   // record return from a function
   virtual void function_return(

src/goto-symex/symex_target_equation.cpp

@@ -210,6 +210,7 @@ void symex_target_equationt::location(
 void symex_target_equationt::function_call(
   const exprt &guard,
   const irep_idt &function_identifier,
+  const std::vector<exprt> &ssa_function_arguments,
   const sourcet &source)
 {
   SSA_steps.push_back(SSA_stept());
@@ -219,6 +220,7 @@ void symex_target_equationt::function_call(
   SSA_step.type = goto_trace_stept::typet::FUNCTION_CALL;
   SSA_step.source = source;
   SSA_step.function_identifier = function_identifier;
+  SSA_step.ssa_function_arguments = ssa_function_arguments;
 
   merge_ireps(SSA_step);
 }
@@ -383,6 +385,7 @@ void symex_target_equationt::convert(
     convert_assumptions(prop_conv);
     convert_assertions(prop_conv);
     convert_goto_instructions(prop_conv);
+    convert_function_calls(prop_conv);
     convert_io(prop_conv);
     convert_constraints(prop_conv);
   }
@@ -658,6 +661,39 @@ void symex_target_equationt::convert_assertions(
   prop_conv.set_to_true(disjunction(disjuncts));
 }
 
+/// converts function calls
+/// \par parameters: decision procedure
+/// \return -
+void symex_target_equationt::convert_function_calls(
+  decision_proceduret &dec_proc)
+{
+  std::size_t argument_count=0;
+
+  for(auto &step : SSA_steps)
+    if(!step.ignore)
+    {
+      step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
+
+      for(const auto &arg : step.ssa_function_arguments)
+      {
+        if(arg.is_constant() ||
+           arg.id()==ID_string_constant)
+          step.converted_function_arguments.push_back(arg);
+        else
+        {
+          const irep_idt identifier="symex::args::"+std::to_string(argument_count++);
+          symbol_exprt symbol(identifier, arg.type());
+
+          equal_exprt eq(arg, symbol);
+          merge_irep(eq);
+
+          dec_proc.set_to(eq, true);
+          step.converted_function_arguments.push_back(symbol);
+        }
+      }
+    }
+}
+
 /// converts I/O
 /// \par parameters: decision procedure
 /// \return -
@@ -690,7 +726,6 @@ void symex_target_equationt::convert_io(
     }
 }
 
-
 void symex_target_equationt::merge_ireps(SSA_stept &SSA_step)
 {
   merge_irep(SSA_step.guard);
@@ -705,6 +740,9 @@ void symex_target_equationt::merge_ireps(SSA_stept &SSA_step)
   for(auto &step : SSA_step.io_args)
     merge_irep(step);
 
+  for(auto &arg : SSA_step.ssa_function_arguments)
+    merge_irep(arg);
+
   // converted_io_args is merged in convert_io
 }
 

src/goto-symex/symex_target_equation.h

@@ -75,6 +75,7 @@ class symex_target_equationt:public symex_targett
   virtual void function_call(
     const exprt &guard,
     const irep_idt &function_identifier,
+    const std::vector<exprt> &ssa_function_arguments,
     const sourcet &source);
 
   // record return from a function
@@ -163,6 +164,7 @@ class symex_target_equationt:public symex_targett
   void convert_constraints(decision_proceduret &decision_procedure) const;
   void convert_goto_instructions(prop_convt &prop_conv);
   void convert_guards(prop_convt &prop_conv);
+  void convert_function_calls(decision_proceduret &decision_procedure);
   void convert_io(decision_proceduret &decision_procedure);
 
   exprt make_expression() const;
@@ -232,6 +234,10 @@ class symex_target_equationt:public symex_targett
     // for function call/return
     irep_idt function_identifier;
 
+    // for function calls
+    std::vector<exprt> ssa_function_arguments,
+                       converted_function_arguments;
+
     // for SHARED_READ/SHARED_WRITE and ATOMIC_BEGIN/ATOMIC_END
     unsigned atomic_section_id=0;