symex_targett::sourcet now knows the function identifier

Author: Daniel Kroening

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-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.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

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);

src/goto-symex/symex_function_call.cpp

@@ -310,6 +310,7 @@ void goto_symext::symex_function_call_code(
   frame.loop_iterations[identifier].count++;
 
   state.source.is_set=true;
+  state.source.function = identifier;
   symex_transition(state, goto_function.body.instructions.begin());
 }
 
@@ -358,7 +359,7 @@ void goto_symext::symex_end_of_function(statet &state)
 {
   // first record the return
   target.function_return(
-    state.guard.as_expr(), state.source.pc->function, state.source);
+    state.guard.as_expr(), state.source.function, state.source);
 
   // then get rid of the frame
   pop_frame(state);

src/goto-symex/symex_main.cpp

@@ -121,12 +121,13 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)
 void goto_symext::initialize_entry_point(
   statet &state,
   const get_goto_functiont &get_goto_function,
+  const irep_idt &function_identifier,
   const goto_programt::const_targett pc,
   const goto_programt::const_targett limit)
 {
   PRECONDITION(!state.threads.empty());
   PRECONDITION(!state.call_stack().empty());
-  state.source=symex_targett::sourcet(pc);
+  state.source = symex_targett::sourcet(function_identifier, pc);
   state.top().end_of_function=limit;
   state.top().calling_location.pc=state.top().end_of_function;
   state.symex_target=⌖
@@ -250,22 +251,29 @@ void goto_symext::resume_symex_from_saved_state(
 void goto_symext::symex_instruction_range(
   statet &state,
   const goto_functionst &goto_functions,
+  const irep_idt &function_identifier,
   const goto_programt::const_targett first,
   const goto_programt::const_targett limit)
 {
   symex_instruction_range(
-    state, get_function_from_goto_functions(goto_functions), first, limit);
+    state,
+    get_function_from_goto_functions(goto_functions),
+    function_identifier,
+    first,
+    limit);
 }
 
 void goto_symext::symex_instruction_range(
   statet &state,
   const get_goto_functiont &get_goto_function,
+  const irep_idt &function_identifier,
   const goto_programt::const_targett first,
   const goto_programt::const_targett limit)
 {
-  initialize_entry_point(state, get_goto_function, first, limit);
+  initialize_entry_point(
+    state, get_goto_function, function_identifier, first, limit);
   ns = namespacet(outer_symbol_table, state.symbol_table);
-  while(state.source.pc->function!=limit->function || state.source.pc!=limit)
+  while(state.source.function != limit->function || state.source.pc != limit)
     symex_threaded_step(state, get_goto_function);
 }
 
@@ -296,6 +304,7 @@ void goto_symext::symex_from_entry_point_of(
   initialize_entry_point(
     state,
     get_goto_function,
+    goto_functionst::entry_point(),
     start_function->body.instructions.begin(),
     prev(start_function->body.instructions.end()));
 

src/goto-symex/symex_target.h

@@ -29,27 +29,26 @@ class symex_targett
   struct sourcet
   {
     unsigned thread_nr;
+    irep_idt function;
     goto_programt::const_targett pc;
     bool is_set;
 
-    sourcet():
-      thread_nr(0),
-      is_set(false)
+    sourcet() : thread_nr(0), function(irep_idt()), is_set(false)
     {
     }
 
-    explicit sourcet(
-      goto_programt::const_targett _pc):
-      thread_nr(0),
-      pc(_pc),
-      is_set(true)
+    sourcet(const irep_idt &_function, goto_programt::const_targett _pc)
+      : thread_nr(0), function(_function), pc(_pc), is_set(true)
     {
     }
 
-    explicit sourcet(const goto_programt &_goto_program):
-      thread_nr(0),
-      pc(_goto_program.instructions.begin()),
-      is_set(true)
+    explicit sourcet(
+      const irep_idt &_function,
+      const goto_programt &_goto_program)
+      : thread_nr(0),
+        function(_function),
+        pc(_goto_program.instructions.begin()),
+        is_set(true)
     {
     }
   };

src/goto-symex/symex_target_equation.cpp

@@ -776,10 +776,10 @@ void symex_target_equationt::SSA_stept::output(
   switch(type)
   {
   case goto_trace_stept::typet::ASSERT:
-    out << "ASSERT " << from_expr(ns, source.pc->function, cond_expr) << '\n';
+    out << "ASSERT " << from_expr(ns, source.function, cond_expr) << '\n';
     break;
   case goto_trace_stept::typet::ASSUME:
-    out << "ASSUME " << from_expr(ns, source.pc->function, cond_expr) << '\n';
+    out << "ASSUME " << from_expr(ns, source.function, cond_expr) << '\n';
     break;
   case goto_trace_stept::typet::LOCATION:
     out << "LOCATION" << '\n'; break;
@@ -790,7 +790,7 @@ void symex_target_equationt::SSA_stept::output(
 
   case goto_trace_stept::typet::DECL:
     out << "DECL" << '\n';
-    out << from_expr(ns, source.pc->function, ssa_lhs) << '\n';
+    out << from_expr(ns, source.function, ssa_lhs) << '\n';
     break;
 
   case goto_trace_stept::typet::ASSIGNMENT:
@@ -844,22 +844,22 @@ void symex_target_equationt::SSA_stept::output(
   case goto_trace_stept::typet::MEMORY_BARRIER:
     out << "MEMORY_BARRIER\n"; break;
   case goto_trace_stept::typet::GOTO:
-    out << "IF " << from_expr(ns, source.pc->function, cond_expr) << " GOTO\n";
+    out << "IF " << from_expr(ns, source.function, cond_expr) << " GOTO\n";
     break;
 
   default: UNREACHABLE;
   }
 
   if(is_assert() || is_assume() || is_assignment() || is_constraint())
-    out << from_expr(ns, source.pc->function, cond_expr) << '\n';
+    out << from_expr(ns, source.function, cond_expr) << '\n';
 
   if(is_assert() || is_constraint())
     out << comment << '\n';
 
   if(is_shared_read() || is_shared_write())
-    out << from_expr(ns, source.pc->function, ssa_lhs) << '\n';
+    out << from_expr(ns, source.function, ssa_lhs) << '\n';
 
-  out << "Guard: " << from_expr(ns, source.pc->function, guard) << '\n';
+  out << "Guard: " << from_expr(ns, source.function, guard) << '\n';
 }
 
 void symex_target_equationt::SSA_stept::output(std::ostream &out) const