introduce 'called_function' into goto traces [blocks: #3126]

regression/cbmc/trace_show_function_calls/test.desc

@@ -4,7 +4,7 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 Function call: function_to_call\(-2147483647\) \(depth 2\)
-Function return: function_to_call \(depth 1\)
+Function return from function_to_call \(depth 1\)
 Function call: function_to_call\(-2\) \(depth 2\)
 ^VERIFICATION FAILED$
 --

src/cbmc/symex_bmc.cpp

@@ -65,10 +65,11 @@ void symex_bmct::symex_step(
 
   goto_symext::symex_step(get_goto_function, state);
 
-  if(record_coverage &&
-     // avoid an invalid iterator in state.source.pc
-     (!cur_pc->is_end_function() ||
-      cur_pc->function!=goto_functionst::entry_point()))
+  if(
+    record_coverage &&
+    // avoid an invalid iterator in state.source.pc
+    (!cur_pc->is_end_function() ||
+     state.source.function != goto_functionst::entry_point()))
   {
     // forward goto will effectively be covered via phi function,
     // which does not invoke symex_step; as symex_step is called

src/goto-programs/goto_trace.cpp

@@ -83,8 +83,8 @@ void goto_trace_stept::output(
 
   if(is_assert() || is_assume() || is_goto())
     out << " (" << cond_value << ')';
-  else if(is_function_call() || is_function_return())
-    out << ' ' << function_identifier;
+  else if(is_function_call())
+    out << ' ' << called_function;
 
   if(hidden)
     out << " hidden";
@@ -344,8 +344,7 @@ void show_full_goto_trace(
         out << "  " << messaget::red << step.comment << messaget::reset << '\n';
 
         if(step.pc->is_assert())
-          out << "  " << from_expr(ns, step.pc->function, step.pc->guard)
-              << '\n';
+          out << "  " << from_expr(ns, step.function, step.pc->guard) << '\n';
 
         out << '\n';
       }
@@ -360,8 +359,7 @@ void show_full_goto_trace(
           out << "  " << step.pc->source_location << '\n';
 
         if(step.pc->is_assume())
-          out << "  " << from_expr(ns, step.pc->function, step.pc->guard)
-              << '\n';
+          out << "  " << from_expr(ns, step.function, step.pc->guard) << '\n';
 
         out << '\n';
       }
@@ -431,7 +429,8 @@ void show_full_goto_trace(
         {
           if(l_it!=step.io_args.begin())
             out << ';';
-          out << ' ' << from_expr(ns, step.pc->function, *l_it);
+
+          out << ' ' << from_expr(ns, step.function, *l_it);
 
           // the binary representation
           out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
@@ -453,7 +452,8 @@ void show_full_goto_trace(
       {
         if(l_it!=step.io_args.begin())
           out << ';';
-        out << ' ' << from_expr(ns, step.pc->function, *l_it);
+
+        out << ' ' << from_expr(ns, step.function, *l_it);
 
         // the binary representation
         out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
@@ -466,7 +466,7 @@ void show_full_goto_trace(
       function_depth++;
       if(options.show_function_calls)
       {
-        out << "\n#### Function call: " << step.function_identifier;
+        out << "\n#### Function call: " << step.called_function;
         out << '(';
 
         bool first = true;
@@ -477,7 +477,7 @@ void show_full_goto_trace(
           else
             out << ", ";
 
-          out << from_expr(ns, step.function_identifier, arg);
+          out << from_expr(ns, step.function, arg);
         }
 
         out << ") (depth " << function_depth << ") ####\n";
@@ -488,8 +488,8 @@ void show_full_goto_trace(
       function_depth--;
       if(options.show_function_calls)
       {
-        out << "\n#### Function return: " << step.function_identifier
-            << " (depth " << function_depth << ") ####\n";
+        out << "\n#### Function return from " << step.function << " (depth "
+            << function_depth << ") ####\n";
       }
       break;
 
@@ -561,7 +561,7 @@ void show_goto_stack_trace(
     }
     else if(step.is_function_call())
     {
-      out << "  " << step.function_identifier;
+      out << "  " << step.called_function;
       out << '(';
 
       bool first = true;
@@ -572,7 +572,7 @@ void show_goto_stack_trace(
         else
           out << ", ";
 
-        out << from_expr(ns, step.function_identifier, arg);
+        out << from_expr(ns, step.function, arg);
       }
 
       out << ')';

src/goto-programs/goto_trace.h

@@ -86,6 +86,9 @@ class goto_trace_stept
   enum class assignment_typet { STATE, ACTUAL_PARAMETER };
   assignment_typet assignment_type;
 
+  // The instruction that created this step
+  // (function calls are in the caller, function returns are in the callee)
+  irep_idt function;
   goto_programt::const_targett pc;
 
   // this transition done by given thread number
@@ -113,8 +116,8 @@ class goto_trace_stept
   io_argst io_args;
   bool formatted;
 
-  // for function call/return
-  irep_idt function_identifier;
+  // for function calls
+  irep_idt called_function;
 
   // for function call
   std::vector<exprt> function_arguments;

src/goto-programs/graphml_witness.cpp

@@ -284,8 +284,8 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
         {
           xmlt &val=edge.new_element("data");
           val.set_attribute("key", "assumption");
-          val.data=from_expr(ns, it->pc->function, it->full_lhs)+" = "+
-                   from_expr(ns, it->pc->function, it->full_lhs_value)+";";
+          val.data = from_expr(ns, it->function, it->full_lhs) + " = " +
+                     from_expr(ns, it->function, it->full_lhs_value) + ";";
 
           xmlt &val_s=edge.new_element("data");
           val_s.set_attribute("key", "assumption.scope");
@@ -296,10 +296,9 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
         {
           xmlt &val=edge.new_element("data");
           val.set_attribute("key", "sourcecode");
-          const std::string cond =
-            from_expr(ns, it->pc->function, it->cond_expr);
-          const std::string neg_cond=
-            from_expr(ns, it->pc->function, not_exprt(it->cond_expr));
+          const std::string cond = from_expr(ns, it->function, it->cond_expr);
+          const std::string neg_cond =
+            from_expr(ns, it->function, not_exprt(it->cond_expr));
           val.data="["+(it->cond_value ? cond : neg_cond)+"]";
 
           #if 0
@@ -481,7 +480,7 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
           xmlt &val=edge.new_element("data");
           val.set_attribute("key", "sourcecode");
           const std::string cond =
-            from_expr(ns, it->source.pc->function, it->cond_expr);
+            from_expr(ns, it->source.function, it->cond_expr);
           val.data="["+cond+"]";
         }
 

src/goto-programs/interpreter.cpp

@@ -759,7 +759,7 @@ void interpretert::execute_function_call()
   const memory_cellt &cell=memory[address];
 #endif
   const irep_idt &identifier = address_to_identifier(address);
-  trace_step.function_identifier = identifier;
+  trace_step.called_function = identifier;
 
   const goto_functionst::function_mapt::const_iterator f_it=
     goto_functions.function_map.find(identifier);

src/goto-programs/json_goto_trace.cpp

@@ -277,10 +277,14 @@ void convert_return(
   json_call_return["internal"] = jsont::json_boolean(step.internal);
   json_call_return["thread"] = json_numbert(std::to_string(step.thread_nr));
 
-  const symbolt &symbol = ns.lookup(step.function_identifier);
+  const irep_idt &function_identifier =
+    (step.type == goto_trace_stept::typet::FUNCTION_CALL) ? step.called_function
+                                                          : step.function;
+
+  const symbolt &symbol = ns.lookup(function_identifier);
   json_objectt &json_function = json_call_return["function"].make_object();
   json_function["displayName"] = json_stringt(symbol.display_name());
-  json_function["identifier"] = json_stringt(step.function_identifier);
+  json_function["identifier"] = json_stringt(function_identifier);
   json_function["sourceLocation"] = json(symbol.location);
 
   if(!location.is_null())

src/goto-programs/xml_goto_trace.cpp

@@ -139,7 +139,7 @@ void convert(
         for(const auto &arg : step.io_args)
         {
           xml_output.new_element("value").data =
-            from_expr(ns, step.pc->function, arg);
+            from_expr(ns, step.function, arg);
           xml_output.new_element("value_expression").
             new_element(xml(arg, ns));
         }
@@ -158,7 +158,7 @@ void convert(
         for(const auto &arg : step.io_args)
         {
           xml_input.new_element("value").data =
-            from_expr(ns, step.pc->function, arg);
+            from_expr(ns, step.function, arg);
           xml_input.new_element("value_expression").
             new_element(xml(arg, ns));
         }
@@ -169,23 +169,40 @@ void convert(
       break;
 
     case goto_trace_stept::typet::FUNCTION_CALL:
+    {
+      std::string tag = "function_call";
+      xmlt &xml_call_return = dest.new_element(tag);
+
+      xml_call_return.set_attribute_bool("hidden", step.hidden);
+      xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
+      xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
+
+      const symbolt &symbol = ns.lookup(step.called_function);
+      xmlt &xml_function = xml_call_return.new_element("function");
+      xml_function.set_attribute(
+        "display_name", id2string(symbol.display_name()));
+      xml_function.set_attribute("identifier", id2string(symbol.name));
+      xml_function.new_element() = xml(symbol.location);
+
+      if(xml_location.name != "")
+        xml_call_return.new_element().swap(xml_location);
+    }
+    break;
+
     case goto_trace_stept::typet::FUNCTION_RETURN:
       {
-        std::string tag=
-          (step.type==goto_trace_stept::typet::FUNCTION_CALL)?
-          "function_call":"function_return";
+        std::string tag = "function_return";
         xmlt &xml_call_return=dest.new_element(tag);
 
         xml_call_return.set_attribute_bool("hidden", step.hidden);
         xml_call_return.set_attribute("thread", std::to_string(step.thread_nr));
         xml_call_return.set_attribute("step_nr", std::to_string(step.step_nr));
 
-        const symbolt &symbol = ns.lookup(step.function_identifier);
+        const symbolt &symbol = ns.lookup(step.function);
         xmlt &xml_function=xml_call_return.new_element("function");
         xml_function.set_attribute(
           "display_name", id2string(symbol.display_name()));
-        xml_function.set_attribute(
-          "identifier", id2string(step.function_identifier));
+        xml_function.set_attribute("identifier", id2string(step.function));
         xml_function.new_element()=xml(symbol.location);
 
         if(xml_location.name!="")

src/goto-symex/build_goto_trace.cpp

@@ -153,7 +153,7 @@ void update_internal_field(
   }
 
   // set internal field to _start function-return step
-  if(SSA_step.source.pc->function==goto_functionst::entry_point())
+  if(SSA_step.source.function == goto_functionst::entry_point())
   {
     // "__CPROVER_*" function calls in __CPROVER_start are already marked as
     // internal. Don't mark any other function calls (i.e. "main"), function
@@ -299,13 +299,14 @@ void build_goto_trace(
 
       goto_trace_step.thread_nr = SSA_step.source.thread_nr;
       goto_trace_step.pc = SSA_step.source.pc;
+      goto_trace_step.function = SSA_step.source.function;
       goto_trace_step.comment = SSA_step.comment;
       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.called_function = SSA_step.called_function;
       goto_trace_step.function_arguments = SSA_step.converted_function_arguments;
 
       for(auto &arg : goto_trace_step.function_arguments)

src/goto-symex/goto_symex.h

@@ -148,11 +148,13 @@ class goto_symext
   /// procedure.
   /// \param state Symex state to start with.
   /// \param goto_functions GOTO model to symex.
+  /// \param function_identifier The function with the instruction range
   /// \param first Entry point in form of a first instruction.
   /// \param limit Final instruction, which itself will not be symexed.
   virtual void symex_instruction_range(
     statet &,
     const goto_functionst &,
+    const irep_idt &function_identifier,
     goto_programt::const_targett first,
     goto_programt::const_targett limit);
 
@@ -162,11 +164,13 @@ class goto_symext
   /// procedure.
   /// \param state Symex state to start with.
   /// \param get_goto_function retrieves a function body
+  /// \param function_identifier The function with the instruction range
   /// \param first Entry point in form of a first instruction.
   /// \param limit Final instruction, which itself will not be symexed.
   virtual void symex_instruction_range(
     statet &state,
     const get_goto_functiont &get_goto_function,
+    const irep_idt &function_identifier,
     goto_programt::const_targett first,
     goto_programt::const_targett limit);
 
@@ -183,13 +187,15 @@ class goto_symext
   /// Initialise the symbolic execution and the given state with <code>pc</code>
   /// as entry point.
   /// \param state Symex state to initialise.
-  /// \param goto_functions GOTO model to symex.
+  /// \param get_goto_function producer for GOTO functions
+  /// \param function_identifier The function in which the instructions are
   /// \param pc first instruction to symex
   /// \param limit final instruction, which itself will not
   /// be symexed.
   void initialize_entry_point(
     statet &state,
     const get_goto_functiont &get_goto_function,
+    const irep_idt &function_identifier,
     goto_programt::const_targett pc,
     goto_programt::const_targett limit);
 

src/goto-symex/show_program.cpp

@@ -29,7 +29,7 @@ void show_program(const namespacet &ns, const symex_target_equationt &equation)
   {
     std::cout << "// " << step.source.pc->location_number << " ";
     std::cout << step.source.pc->source_location.as_string() << "\n";
-    const irep_idt &function = step.source.pc->function;
+    const irep_idt &function = step.source.function;
 
     if(step.is_assignment())
     {

src/goto-symex/symex_builtin_functions.cpp

@@ -55,8 +55,8 @@ void goto_symext::symex_allocate(
 
   exprt size=code.op0();
   typet object_type=nil_typet();
-  auto function_symbol = outer_symbol_table.lookup(state.source.pc->function);
-  INVARIANT(function_symbol, "function associated with instruction not found");
+  auto function_symbol = outer_symbol_table.lookup(state.source.function);
+  INVARIANT(function_symbol, "function associated with allocation not found");
   const irep_idt &mode = function_symbol->mode;
 
   // is the type given?

src/goto-symex/symex_dereference.cpp

@@ -258,7 +258,7 @@ void goto_symext::dereference_rec(
 
     if(state.threads.size() == 1)
     {
-      const irep_idt &expr_function = state.source.pc->function;
+      const irep_idt &expr_function = state.source.function;
       if(!expr_function.empty())
       {
         state.get_original_name(to_check);