goto_trace_stept now contains 'called_function' field

Daniel Kroening · Daniel Kroening · commit 692d6ef4443c · 2018-11-05T18:14:41.000Z
The previous 'function_identifier' is now 'called_function', which is a
better name as it denotes the identifier of the function that is called.
diff --git a/regression/cbmc/trace_show_function_calls/test.desc b/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$
 --
diff --git a/src/goto-programs/goto_trace.cpp b/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 << ')';
diff --git a/src/goto-programs/goto_trace.h b/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;
diff --git a/src/goto-programs/graphml_witness.cpp b/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+"]";
         }
 
diff --git a/src/goto-programs/interpreter.cpp b/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);
diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp
@@ -277,10 +277,10 @@ 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 symbolt &symbol = ns.lookup(step.function);
   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(step.function);
   json_function["sourceLocation"] = json(symbol.location);
 
   if(!location.is_null())
diff --git a/src/goto-programs/xml_goto_trace.cpp b/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!="")
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
@@ -302,13 +302,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.called_function;
+      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)
