Merge pull request #3844 from tautschnig/function-symex

goto-symex: use function and called_function fields [blocks: #3126]

Author: tautschnig

src/goto-checker/symex_bmc.cpp

@@ -69,7 +69,7 @@ void symex_bmct::symex_step(
     record_coverage &&
     // avoid an invalid iterator in state.source.pc
     (!cur_pc->is_end_function() ||
-     state.source.function != goto_functionst::entry_point()))
+     state.source.function_id != goto_functionst::entry_point()))
   {
     // forward goto will effectively be covered via phi function,
     // which does not invoke symex_step; as symex_step is called
@@ -110,7 +110,7 @@ bool symex_bmct::should_stop_unwind(
   const goto_symex_statet::call_stackt &context,
   unsigned unwind)
 {
-  const irep_idt id = goto_programt::loop_id(*source.pc);
+  const irep_idt id = goto_programt::loop_id(source.function_id, *source.pc);
 
   tvt abort_unwind_decision;
   unsigned this_loop_limit = std::numeric_limits<unsigned>::max();

src/goto-instrument/unwind.cpp

@@ -288,8 +288,7 @@ void goto_unwindt::unwind(
     }
 
     PRECONDITION(!function_id.empty());
-    const irep_idt loop_id =
-      id2string(function_id) + "." + std::to_string(i_it->loop_number);
+    const irep_idt loop_id = goto_programt::loop_id(function_id, *i_it);
 
     auto limit=unwindset.get_limit(loop_id, 0);
 

src/goto-programs/goto_program.h

@@ -694,9 +694,10 @@ class goto_programt
   void update();
 
   /// Human-readable loop name
-  static irep_idt loop_id(const instructiont &instruction)
+  static irep_idt
+  loop_id(const irep_idt &function_id, const instructiont &instruction)
   {
-    return id2string(instruction.function)+"."+
+    return id2string(function_id) + "." +
            std::to_string(instruction.loop_number);
   }
 

src/goto-programs/goto_trace.cpp

@@ -292,9 +292,9 @@ state_location(const goto_trace_stept &state, const namespacet &ns)
   if(!source_location.get_file().empty())
     result += "file " + id2string(source_location.get_file());
 
-  if(!state.function.empty())
+  if(!state.function_id.empty())
   {
-    const symbolt &symbol = ns.lookup(state.function);
+    const symbolt &symbol = ns.lookup(state.function_id);
     if(!result.empty())
       result += ' ';
     result += "function " + id2string(symbol.display_name());
@@ -333,7 +333,7 @@ void show_state_header(
 
   if(options.show_code)
   {
-    out << as_string(ns, state.function, *state.pc) << '\n';
+    out << as_string(ns, state.function_id, *state.pc) << '\n';
     out << "----------------------------------------------------" << '\n';
   }
 }
@@ -387,7 +387,10 @@ void show_compact_goto_trace(
         out << "  " << messaget::red << step.comment << messaget::reset << '\n';
 
         if(step.pc->is_assert())
-          out << "  " << from_expr(ns, step.function, step.pc->guard) << '\n';
+        {
+          out << "  " << from_expr(ns, step.function_id, step.pc->guard)
+              << '\n';
+        }
 
         out << '\n';
       }
@@ -442,7 +445,7 @@ void show_compact_goto_trace(
       {
         auto arg_strings = make_range(step.function_arguments)
                              .map([&ns, &step](const exprt &arg) {
-                               return from_expr(ns, step.function, arg);
+                               return from_expr(ns, step.function_id, arg);
                              });
 
         out << '(';
@@ -507,7 +510,10 @@ void show_full_goto_trace(
         out << "  " << messaget::red << step.comment << messaget::reset << '\n';
 
         if(step.pc->is_assert())
-          out << "  " << from_expr(ns, step.function, step.pc->guard) << '\n';
+        {
+          out << "  " << from_expr(ns, step.function_id, step.pc->guard)
+              << '\n';
+        }
 
         out << '\n';
       }
@@ -522,7 +528,10 @@ void show_full_goto_trace(
           out << "  " << step.pc->source_location << '\n';
 
         if(step.pc->is_assume())
-          out << "  " << from_expr(ns, step.function, step.pc->guard) << '\n';
+        {
+          out << "  " << from_expr(ns, step.function_id, step.pc->guard)
+              << '\n';
+        }
 
         out << '\n';
       }
@@ -592,7 +601,7 @@ void show_full_goto_trace(
           if(l_it!=step.io_args.begin())
             out << ';';
 
-          out << ' ' << from_expr(ns, step.function, *l_it);
+          out << ' ' << from_expr(ns, step.function_id, *l_it);
 
           // the binary representation
           out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
@@ -614,7 +623,7 @@ void show_full_goto_trace(
         if(l_it!=step.io_args.begin())
           out << ';';
 
-        out << ' ' << from_expr(ns, step.function, *l_it);
+        out << ' ' << from_expr(ns, step.function_id, *l_it);
 
         // the binary representation
         out << " (" << trace_numeric_value(*l_it, ns, options) << ')';
@@ -638,7 +647,7 @@ void show_full_goto_trace(
           else
             out << ", ";
 
-          out << from_expr(ns, step.function, arg);
+          out << from_expr(ns, step.function_id, arg);
         }
 
         out << ") (depth " << function_depth << ") ####\n";
@@ -649,7 +658,7 @@ void show_full_goto_trace(
       function_depth--;
       if(options.show_function_calls)
       {
-        out << "\n#### Function return from " << step.function << " (depth "
+        out << "\n#### Function return from " << step.function_id << " (depth "
             << function_depth << ") ####\n";
       }
       break;
@@ -732,7 +741,7 @@ static void show_goto_stack_trace(
         else
           out << ", ";
 
-        out << from_expr(ns, step.function, arg);
+        out << from_expr(ns, step.function_id, arg);
       }
 
       out << ')';

src/goto-programs/goto_trace.h

@@ -88,7 +88,7 @@ class goto_trace_stept
 
   // The instruction that created this step
   // (function calls are in the caller, function returns are in the callee)
-  irep_idt function;
+  irep_idt function_id;
   goto_programt::const_targett pc;
 
   // this transition done by given thread number

src/goto-programs/graphml_witness.cpp

@@ -285,8 +285,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->function, it->full_lhs) + " = " +
-                     from_expr(ns, it->function, it->full_lhs_value) + ";";
+          val.data = from_expr(ns, it->function_id, it->full_lhs) + " = " +
+                     from_expr(ns, it->function_id, it->full_lhs_value) + ";";
 
           xmlt &val_s=edge.new_element("data");
           val_s.set_attribute("key", "assumption.scope");
@@ -297,9 +297,10 @@ 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->function, it->cond_expr);
+          const std::string cond =
+            from_expr(ns, it->function_id, it->cond_expr);
           const std::string neg_cond =
-            from_expr(ns, it->function, not_exprt(it->cond_expr));
+            from_expr(ns, it->function_id, not_exprt(it->cond_expr));
           val.data="["+(it->cond_value ? cond : neg_cond)+"]";
 
           #if 0
@@ -483,7 +484,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.function, it->cond_expr);
+            from_expr(ns, it->source.function_id, it->cond_expr);
           val.data="["+cond+"]";
         }
 

src/goto-programs/json_goto_trace.cpp

@@ -179,7 +179,7 @@ void convert_output(
   // Recovering the mode from the function
   irep_idt mode;
   const symbolt *function_name;
-  if(ns.lookup(step.function, function_name))
+  if(ns.lookup(step.function_id, function_name))
     // Failed to find symbol
     mode = ID_unknown;
   else
@@ -221,7 +221,7 @@ void convert_input(
   // Recovering the mode from the function
   irep_idt mode;
   const symbolt *function_name;
-  if(ns.lookup(step.function, function_name))
+  if(ns.lookup(step.function_id, function_name))
     // Failed to find symbol
     mode = ID_unknown;
   else
@@ -265,7 +265,7 @@ void convert_return(
 
   const irep_idt &function_identifier =
     (step.type == goto_trace_stept::typet::FUNCTION_CALL) ? step.called_function
-                                                          : step.function;
+                                                          : step.function_id;
 
   const symbolt &symbol = ns.lookup(function_identifier);
   json_call_return["function"] =

src/goto-programs/loop_ids.cpp

@@ -25,7 +25,7 @@ void show_loop_ids(
 
 void show_loop_ids(
   ui_message_handlert::uit ui,
-  const irep_idt &function_identifier,
+  const irep_idt &function_id,
   const goto_programt &goto_program)
 {
   switch(ui)
@@ -36,9 +36,8 @@ void show_loop_ids(
       {
         if(it->is_backwards_goto())
         {
-          unsigned loop_id=it->loop_number;
-
-          std::cout << "Loop " << function_identifier << "." << loop_id << ":"
+          std::cout << "Loop " << goto_programt::loop_id(function_id, *it)
+                    << ":"
                     << "\n";
 
           std::cout << "  " << it->source_location << "\n";
@@ -53,9 +52,7 @@ void show_loop_ids(
       {
         if(it->is_backwards_goto())
         {
-          unsigned loop_id=it->loop_number;
-          std::string id =
-            id2string(function_identifier) + "." + std::to_string(loop_id);
+          std::string id = id2string(goto_programt::loop_id(function_id, *it));
 
           xmlt xml_loop("loop", {{"name", id}}, {});
           xml_loop.new_element("loop-id").data=id;
@@ -72,7 +69,7 @@ void show_loop_ids(
 
 void show_loop_ids_json(
   ui_message_handlert::uit ui,
-  const irep_idt &function_identifier,
+  const irep_idt &function_id,
   const goto_programt &goto_program,
   json_arrayt &loops)
 {
@@ -82,9 +79,7 @@ void show_loop_ids_json(
   {
     if(it->is_backwards_goto())
     {
-      unsigned loop_id=it->loop_number;
-      std::string id =
-        id2string(function_identifier) + "." + std::to_string(loop_id);
+      std::string id = id2string(goto_programt::loop_id(function_id, *it));
 
       loops.push_back(
         json_objectt({{"name", json_stringt(id)},

src/goto-programs/loop_ids.h

@@ -26,7 +26,7 @@ void show_loop_ids(
 
 void show_loop_ids(
   ui_message_handlert::uit,
-  const irep_idt &function_identifier,
+  const irep_idt &function_id,
   const goto_programt &);
 
 #endif // CPROVER_GOTO_PROGRAMS_LOOP_IDS_H

src/goto-programs/xml_goto_trace.cpp

@@ -127,7 +127,7 @@ void convert(
         for(const auto &arg : step.io_args)
         {
           xml_output.new_element("value").data =
-            from_expr(ns, step.function, arg);
+            from_expr(ns, step.function_id, arg);
           xml_output.new_element("value_expression").
             new_element(xml(arg, ns));
         }
@@ -146,7 +146,7 @@ void convert(
         for(const auto &arg : step.io_args)
         {
           xml_input.new_element("value").data =
-            from_expr(ns, step.function, arg);
+            from_expr(ns, step.function_id, arg);
           xml_input.new_element("value_expression").
             new_element(xml(arg, ns));
         }
@@ -186,11 +186,11 @@ void convert(
         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);
+        const symbolt &symbol = ns.lookup(step.function_id);
         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));
+        xml_function.set_attribute("identifier", id2string(step.function_id));
         xml_function.new_element()=xml(symbol.location);
 
         if(xml_location.name!="")

src/goto-symex/build_goto_trace.cpp

@@ -156,7 +156,7 @@ void update_internal_field(
   }
 
   // set internal field to _start function-return step
-  if(SSA_step.source.function == goto_functionst::entry_point())
+  if(SSA_step.source.function_id == 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
@@ -304,7 +304,7 @@ 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.function_id = SSA_step.source.function_id;
       if(SSA_step.is_assert())
       {
         goto_trace_step.comment = SSA_step.comment;

src/goto-symex/goto_symex_state.cpp

@@ -759,7 +759,7 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
     return;
   }
 
-  out << source.pc->function << " " << source.pc->location_number << "\n";
+  out << source.function_id << " " << source.pc->location_number << "\n";
 
   for(auto stackit = threads[source.thread_nr].call_stack.rbegin(),
            stackend = threads[source.thread_nr].call_stack.rend();
@@ -769,7 +769,7 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
     const auto &frame = *stackit;
     if(frame.calling_location.is_set)
     {
-      out << frame.calling_location.pc->function << " "
+      out << frame.calling_location.function_id << " "
           << frame.calling_location.pc->location_number << "\n";
     }
   }

src/goto-symex/show_program.cpp

@@ -28,11 +28,11 @@ static void show_step(
   const std::string &annotation,
   std::size_t &count)
 {
-  const irep_idt &function = step.source.function;
+  const irep_idt &function_id = step.source.function_id;
 
   std::string string_value = (step.is_shared_read() || step.is_shared_write())
-                               ? from_expr(ns, function, step.ssa_lhs)
-                               : from_expr(ns, function, step.cond_expr);
+                               ? from_expr(ns, function_id, step.ssa_lhs)
+                               : from_expr(ns, function_id, step.cond_expr);
   std::cout << '(' << count << ") ";
   if(annotation.empty())
     std::cout << string_value;
@@ -42,7 +42,7 @@ static void show_step(
 
   if(!step.guard.is_true())
   {
-    const std::string guard_string = from_expr(ns, function, step.guard);
+    const std::string guard_string = from_expr(ns, function_id, step.guard);
     std::cout << std::string(std::to_string(count).size() + 3, ' ');
     std::cout << "guard: " << guard_string << '\n';
   }

src/goto-symex/symex_builtin_functions.cpp

@@ -56,7 +56,7 @@ void goto_symext::symex_allocate(
 
   exprt size=code.op0();
   typet object_type=nil_typet();
-  auto function_symbol = outer_symbol_table.lookup(state.source.function);
+  auto function_symbol = outer_symbol_table.lookup(state.source.function_id);
   INVARIANT(function_symbol, "function associated with allocation not found");
   const irep_idt &mode = function_symbol->mode;
 

src/goto-symex/symex_dereference.cpp

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