add arguments of function calls to goto_trace

Author: Daniel Kroening

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.ssa_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_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_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_arguments = ssa_arguments;
 
   merge_ireps(SSA_step);
 }
@@ -705,6 +707,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_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_arguments,
     const sourcet &source);
 
   // record return from a function
@@ -232,6 +233,9 @@ class symex_target_equationt:public symex_targett
     // for function call/return
     irep_idt function_identifier;
 
+    // for function calls
+    std::vector<exprt> ssa_arguments;
+
     // for SHARED_READ/SHARED_WRITE and ATOMIC_BEGIN/ATOMIC_END
     unsigned atomic_section_id=0;