Prepare symex for lazy loading

src/analyses/dirty.cpp

@@ -72,3 +72,14 @@ void dirtyt::output(std::ostream &out) const
   for(const auto &d : dirty)
     out << d << '\n';
 }
+
+/// Analyse the given function with dirtyt if it hasn't been seen before
+/// \param id: function id to analyse
+/// \param function: function to analyse
+void incremental_dirtyt::populate_dirty_for_function(
+  const irep_idt &id, const goto_functionst::goto_functiont &function)
+{
+  auto insert_result = dirty_processed_functions.insert(id);
+  if(insert_result.second)
+    dirty.add_function(function);
+}

src/analyses/dirty.h

@@ -25,6 +25,10 @@ class dirtyt
   typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
   typedef goto_functionst::goto_functiont goto_functiont;
 
+  dirtyt()
+  {
+  }
+
   explicit dirtyt(const goto_functiont &goto_function)
   {
     build(goto_function);
@@ -53,6 +57,11 @@ class dirtyt
     return dirty;
   }
 
+  void add_function(const goto_functiont &goto_function)
+  {
+    build(goto_function);
+  }
+
 protected:
   void build(const goto_functiont &goto_function);
 
@@ -71,4 +80,27 @@ inline std::ostream &operator<<(
   return out;
 }
 
+/// Wrapper for dirtyt that permits incremental population, ensuring each
+/// function is analysed exactly once.
+class incremental_dirtyt
+{
+public:
+  void populate_dirty_for_function(
+    const irep_idt &id, const goto_functionst::goto_functiont &function);
+
+  bool operator()(const irep_idt &id) const
+  {
+    return dirty(id);
+  }
+
+  bool operator()(const symbol_exprt &expr) const
+  {
+    return dirty(expr);
+  }
+
+private:
+  dirtyt dirty;
+  std::unordered_set<irep_idt, irep_id_hash> dirty_processed_functions;
+};
+
 #endif // CPROVER_ANALYSES_DIRTY_H

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/goto_symex_state.h

@@ -26,7 +26,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "symex_target.h"
 
-class dirtyt;
+class incremental_dirtyt;
 
 // central data structure: state
 class goto_symex_statet final
@@ -340,9 +340,12 @@ class goto_symex_statet final
   bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns);
   bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns);
 
+  void populate_dirty_for_function(
+    const irep_idt &id, const goto_functionst::goto_functiont &);
+
   void switch_to_thread(unsigned t);
   bool record_events;
-  std::unique_ptr<const dirtyt> dirty;
+  std::unique_ptr<incremental_dirtyt> dirty;
 };
 
 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_STATE_H

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,23 @@ 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
+  const goto_functionst::goto_functiont &goto_function =
+    get_goto_function(identifier);
 
-  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;
+  if(state.dirty)
+    state.dirty->populate_dirty_for_function(identifier, goto_function);
 
   const bool stop_recursing=get_unwind_recursion(
     identifier,