Symex: switch to incrementally populating address-taken locals

This populates address-taken locals as each function is first encountered,
rather than analysing every function up front. This lays the groundwork for
moving to incremental function loading.

Author: smowton

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

@@ -235,6 +235,9 @@ void goto_symext::symex_function_call_code(
 
   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,
     state.source.thread_nr,

src/goto-symex/symex_main.cpp

@@ -136,8 +136,17 @@ void goto_symext::initialize_entry_point(
   state.top().end_of_function=limit;
   state.top().calling_location.pc=state.top().end_of_function;
   state.symex_target=⌖
-  state.dirty=util_make_unique<dirtyt>(goto_functions);
-
+  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;
+  }
   symex_transition(state, state.source.pc);
 }