Address-taken locals analysis: support incremental analysis

This adds a constructor and incremental build function so that the set
of address-taken locals can be populated one function at a time. This
will be useful when goto-symex begins to use incremental loading, meaning
it cannot populate the analysis in one operation.

Author: smowton

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