Goto-symex: add support for general function accessor

Previously goto-symex presumed access to goto_functionst; now it only requires a function
that somehow yields a goto_functiont. This will facilitate integration with lazy_goto_modelt,
and in future any other kind of on-demand goto_functiont production.

src/cbmc/symex_bmc.cpp

@@ -31,7 +31,7 @@ symex_bmct::symex_bmct(
 
 /// show progress
 void symex_bmct::symex_step(
-  const goto_functionst &goto_functions,
+  const get_goto_functiont &get_goto_function,
   statet &state)
 {
   const source_locationt &source_location=state.source.pc->source_location;
@@ -63,12 +63,12 @@ void symex_bmct::symex_step(
     log.statistics() << log.eom;
   }
 
-  goto_symext::symex_step(goto_functions, state);
+  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_functions.entry_point()))
+      cur_pc->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/cbmc/symex_bmc.h

@@ -128,7 +128,7 @@ class symex_bmct: public goto_symext
   // overloaded from goto_symext
   //
   virtual void symex_step(
-    const goto_functionst &goto_functions,
+    const get_goto_functiont &get_goto_function,
     statet &state);
 
   virtual void merge_goto(

src/goto-symex/goto_symex.h

@@ -67,6 +67,10 @@ class goto_symext
 
   typedef goto_symex_statet statet;
 
+  typedef
+    std::function<const goto_functionst::goto_functiont &(const irep_idt &)>
+    get_goto_functiont;
+
   /// \brief symex entire program starting from entry point
   ///
   /// The state that goto_symext maintains has a large memory footprint.
@@ -76,6 +80,15 @@ class goto_symext
   virtual void symex_from_entry_point_of(
     const goto_functionst &goto_functions);
 
+  /// \brief symex entire program starting from entry point
+  ///
+  /// The state that goto_symext maintains has a large memory footprint.
+  /// This method deallocates the state as soon as symbolic execution
+  /// has completed, so use it if you don't care about having the state
+  /// around afterwards.
+  virtual void symex_from_entry_point_of(
+    const get_goto_functiont &get_goto_function);
+
   //// \brief symex entire program starting from entry point
   ///
   /// This method uses the `state` argument as the symbolic execution
@@ -88,6 +101,18 @@ class goto_symext
     const goto_functionst &,
     const goto_programt &);
 
+  //// \brief symex entire program starting from entry point
+  ///
+  /// This method uses the `state` argument as the symbolic execution
+  /// state, which is useful for examining the state after this method
+  /// returns. The state that goto_symext maintains has a large memory
+  /// footprint, so if keeping the state around is not necessary,
+  /// clients should instead call goto_symext::symex_from_entry_point_of().
+  virtual void symex_with_state(
+    statet &,
+    const get_goto_functiont &,
+    const goto_programt &);
+
   /// Symexes from the first instruction and the given state, terminating as
   /// soon as the last instruction is reached.  This is useful to explicitly
   /// symex certain ranges of a program, e.g. in an incremental decision
@@ -102,6 +127,20 @@ class goto_symext
     goto_programt::const_targett first,
     goto_programt::const_targett limit);
 
+  /// Symexes from the first instruction and the given state, terminating as
+  /// soon as the last instruction is reached.  This is useful to explicitly
+  /// symex certain ranges of a program, e.g. in an incremental decision
+  /// procedure.
+  /// \param state Symex state to start with.
+  /// \param get_goto_function retrieves a function body
+  /// \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,
+    goto_programt::const_targett first,
+    goto_programt::const_targett limit);
+
 protected:
   /// Initialise the symbolic execution and the given state with <code>pc</code>
   /// as entry point.
@@ -111,21 +150,21 @@ class goto_symext
   /// \param limit final instruction, which itself will not
   /// be symexed.
   void initialize_entry_point(
-    statet &,
-    const goto_functionst &,
+    statet &state,
+    const get_goto_functiont &get_goto_function,
     goto_programt::const_targett pc,
     goto_programt::const_targett limit);
 
   /// Invokes symex_step and verifies whether additional threads can be
   /// executed.
   /// \param state Current GOTO symex step.
-  /// \param goto_functions GOTO model to symex.
+  /// \param get_goto_function function that retrieves function bodies
   void symex_threaded_step(
-    statet &, const goto_functionst &);
+    statet &, const get_goto_functiont &);
 
   /** execute just one step */
   virtual void symex_step(
-    const goto_functionst &,
+    const get_goto_functiont &,
     statet &);
 
 public:
@@ -213,7 +252,7 @@ class goto_symext
   virtual void symex_decl(statet &);
   virtual void symex_decl(statet &, const symbol_exprt &expr);
   virtual void symex_dead(statet &);
-  virtual void symex_other(const goto_functionst &, statet &);
+  virtual void symex_other(statet &);
 
   virtual void vcc(
     const exprt &,
@@ -255,19 +294,19 @@ class goto_symext
   }
 
   virtual void symex_function_call(
-    const goto_functionst &,
+    const get_goto_functiont &,
     statet &,
     const code_function_callt &);
 
   virtual void symex_end_of_function(statet &);
 
   virtual void symex_function_call_symbol(
-    const goto_functionst &,
+    const get_goto_functiont &,
     statet &,
     const code_function_callt &);
 
   virtual void symex_function_call_code(
-    const goto_functionst &,
+    const get_goto_functiont &,
     statet &,
     const code_function_callt &);
 

src/goto-symex/symex_function_call.cpp

@@ -172,14 +172,14 @@ void goto_symext::parameter_assignments(
 }
 
 void goto_symext::symex_function_call(
-  const goto_functionst &goto_functions,
+  const get_goto_functiont &get_goto_function,
   statet &state,
   const code_function_callt &code)
 {
   const exprt &function=code.function();
 
   if(function.id()==ID_symbol)
-    symex_function_call_symbol(goto_functions, state, code);
+    symex_function_call_symbol(get_goto_function, state, code);
   else if(function.id()==ID_if)
     throw "symex_function_call can't do if";
   else if(function.id()==ID_dereference)
@@ -189,7 +189,7 @@ void goto_symext::symex_function_call(
 }
 
 void goto_symext::symex_function_call_symbol(
-  const goto_functionst &goto_functions,
+  const get_goto_functiont &get_goto_function,
   statet &state,
   const code_function_callt &code)
 {
@@ -213,27 +213,20 @@ void goto_symext::symex_function_call_symbol(
     symex_macro(state, code);
   }
   else
-    symex_function_call_code(goto_functions, state, code);
+    symex_function_call_code(get_goto_function, state, code);
 }
 
 /// do function call by inlining
 void goto_symext::symex_function_call_code(
-  const goto_functionst &goto_functions,
+  const get_goto_functiont &get_goto_function,
   statet &state,
   const code_function_callt &call)
 {
   const irep_idt &identifier=
     to_symbol_expr(call.function()).get_identifier();
 
-  // find code in function map
-
-  goto_functionst::function_mapt::const_iterator it=
-    goto_functions.function_map.find(identifier);
-
-  if(it==goto_functions.function_map.end())
-    throw "failed to find `"+id2string(identifier)+"' in function_map";
-
-  const goto_functionst::goto_functiont &goto_function=it->second;
+  const goto_functionst::goto_functiont &goto_function =
+    get_goto_function(identifier);
 
   if(state.dirty)
     state.dirty->populate_dirty_for_function(identifier, goto_function);

src/goto-symex/symex_main.cpp

@@ -126,7 +126,7 @@ void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)
 
 void goto_symext::initialize_entry_point(
   statet &state,
-  const goto_functionst &goto_functions,
+  const get_goto_functiont &get_goto_function,
   const goto_programt::const_targett pc,
   const goto_programt::const_targett limit)
 {
@@ -137,23 +137,19 @@ void goto_symext::initialize_entry_point(
   state.top().calling_location.pc=state.top().end_of_function;
   state.symex_target=⌖
   state.dirty=util_make_unique<incremental_dirtyt>();
-  if(!pc->function.empty())
-  {
-    state.dirty->populate_dirty_for_function(
-      pc->function, goto_functions.function_map.at(pc->function));
-  }
-  else
-  {
-    log.warning() << "Unable to analyse address-taken locals, as start "
-      "instruction does not state its function" << messaget::eom;
-  }
+
+  INVARIANT(
+    !pc->function.empty(), "all symexed instructions should have a function");
+  state.dirty->populate_dirty_for_function(
+    pc->function, get_goto_function(pc->function));
+
   symex_transition(state, state.source.pc);
 }
 
 void goto_symext::symex_threaded_step(
-  statet &state, const goto_functionst &goto_functions)
+  statet &state, const get_goto_functiont &get_goto_function)
 {
-  symex_step(goto_functions, state);
+  symex_step(get_goto_function, state);
 
   // is there another thread to execute?
   if(state.call_stack().empty() &&
@@ -168,21 +164,39 @@ void goto_symext::symex_threaded_step(
   }
 }
 
+static goto_symext::get_goto_functiont get_function_from_goto_functions(
+  const goto_functionst &goto_functions)
+{
+  return [&goto_functions](const irep_idt &key) ->
+    const goto_functionst::goto_functiont & { // NOLINT(*)
+    return goto_functions.function_map.at(key);
+  };
+}
+
 void goto_symext::symex_with_state(
   statet &state,
   const goto_functionst &goto_functions,
   const goto_programt &goto_program)
+{
+  symex_with_state(
+    state, get_function_from_goto_functions(goto_functions), goto_program);
+}
+
+void goto_symext::symex_with_state(
+  statet &state,
+  const get_goto_functiont &get_goto_function,
+  const goto_programt &goto_program)
 {
   PRECONDITION(!goto_program.instructions.empty());
   initialize_entry_point(
     state,
-    goto_functions,
+    get_goto_function,
     goto_program.instructions.begin(),
     prev(goto_program.instructions.end()));
   PRECONDITION(state.top().end_of_function->is_end_function());
 
   while(!state.call_stack().empty())
-    symex_threaded_step(state, goto_functions);
+    symex_threaded_step(state, get_goto_function);
 
   state.dirty=nullptr;
 }
@@ -193,30 +207,48 @@ void goto_symext::symex_instruction_range(
   const goto_programt::const_targett first,
   const goto_programt::const_targett limit)
 {
-  initialize_entry_point(state, goto_functions, first, limit);
+  symex_instruction_range(
+    state, get_function_from_goto_functions(goto_functions), first, limit);
+}
+
+void goto_symext::symex_instruction_range(
+  statet &state,
+  const get_goto_functiont &get_goto_function,
+  const goto_programt::const_targett first,
+  const goto_programt::const_targett limit)
+{
+  initialize_entry_point(state, get_goto_function, first, limit);
   while(state.source.pc->function!=limit->function || state.source.pc!=limit)
-    symex_threaded_step(state, goto_functions);
+    symex_threaded_step(state, get_goto_function);
 }
 
-/// symex from entry point
 void goto_symext::symex_from_entry_point_of(
-    const goto_functionst &goto_functions)
+  const goto_functionst &goto_functions)
 {
-  goto_functionst::function_mapt::const_iterator it=
-    goto_functions.function_map.find(goto_functionst::entry_point());
+  symex_from_entry_point_of(get_function_from_goto_functions(goto_functions));
+}
 
-  if(it==goto_functions.function_map.end())
+/// symex from entry point
+void goto_symext::symex_from_entry_point_of(
+  const get_goto_functiont &get_goto_function)
+{
+  const goto_functionst::goto_functiont *start_function;
+  try
+  {
+    start_function = &get_goto_function(goto_functionst::entry_point());
+  }
+  catch(const std::out_of_range &error)
+  {
     throw "the program has no entry point";
-
-  const goto_programt &body=it->second.body;
+  }
 
   statet state;
-  symex_with_state(state, goto_functions, body);
+  symex_with_state(state, get_goto_function, start_function->body);
 }
 
 /// do just one step
 void goto_symext::symex_step(
-  const goto_functionst &goto_functions,
+  const get_goto_functiont &get_goto_function,
   statet &state)
 {
   #if 0
@@ -321,15 +353,15 @@ void goto_symext::symex_step(
       Forall_expr(it, deref_code.arguments())
         clean_expr(*it, state, false);
 
-      symex_function_call(goto_functions, state, deref_code);
+      symex_function_call(get_goto_function, state, deref_code);
     }
     else
       symex_transition(state);
     break;
 
   case OTHER:
     if(!state.guard.is_false())
-      symex_other(goto_functions, state);
+      symex_other(state);
 
     symex_transition(state);
     break;

src/goto-symex/symex_other.cpp

@@ -79,7 +79,6 @@ void goto_symext::havoc_rec(
 }
 
 void goto_symext::symex_other(
-  const goto_functionst &goto_functions,
   statet &state)
 {
   const goto_programt::instructiont &instruction=*state.source.pc;