Move the handling of whole program analysis into the interprocedural code

Author: martin

src/analyses/ai.cpp

@@ -536,6 +536,47 @@ bool ai_baset::visit_end_function(
   return false;
 }
 
+void ai_localt::operator()(
+  const goto_functionst &goto_functions,
+  const namespacet &ns)
+{
+  initialize(goto_functions);
+  for(const auto &gf_entry : goto_functions.function_map)
+  {
+    if(gf_entry.second.body_available())
+    {
+      trace_ptrt p = entry_state(gf_entry.second.body);
+      fixedpoint(p, gf_entry.first, gf_entry.second.body, goto_functions, ns);
+    }
+  }
+  finalize();
+}
+
+void ai_localt::operator()(const abstract_goto_modelt &goto_model)
+{
+  const namespacet ns(goto_model.get_symbol_table());
+  operator()(goto_model.get_goto_functions(), ns);
+}
+
+void ai_recursive_interproceduralt::
+operator()(const goto_functionst &goto_functions, const namespacet &ns)
+{
+  initialize(goto_functions);
+  trace_ptrt p = entry_state(goto_functions);
+  fixedpoint(p, goto_functions, ns);
+  finalize();
+}
+
+void ai_recursive_interproceduralt::operator()(
+  const abstract_goto_modelt &goto_model)
+{
+  const namespacet ns(goto_model.get_symbol_table());
+  initialize(goto_model.get_goto_functions());
+  trace_ptrt p = entry_state(goto_model.get_goto_functions());
+  fixedpoint(p, goto_model.get_goto_functions(), ns);
+  finalize();
+}
+
 bool ai_recursive_interproceduralt::visit_edge_function_call(
   const irep_idt &calling_function_id,
   trace_ptrt p_call,

src/analyses/ai.h

@@ -153,28 +153,12 @@ class ai_baset
   }
 
   /// Run abstract interpretation on a whole program
-  void operator()(
-    const goto_functionst &goto_functions,
-    const namespacet &ns)
-  {
-    initialize(goto_functions);
-    trace_ptrt p = entry_state(goto_functions);
-    fixedpoint(p, goto_functions, ns);
-    finalize();
-  }
-
-  /// Run abstract interpretation on a whole program
-  void operator()(const abstract_goto_modelt &goto_model)
-  {
-    const namespacet ns(goto_model.get_symbol_table());
-    initialize(goto_model.get_goto_functions());
-    trace_ptrt p = entry_state(goto_model.get_goto_functions());
-    fixedpoint(p, goto_model.get_goto_functions(), ns);
-    finalize();
-  }
+  virtual void
+  operator()(const goto_functionst &goto_functions, const namespacet &ns) = 0;
+  virtual void operator()(const abstract_goto_modelt &goto_model) = 0;
 
   /// Run abstract interpretation on a single function
-  void operator()(
+  virtual void operator()(
     const irep_idt &function_id,
     const goto_functionst::goto_functiont &goto_function,
     const namespacet &ns)
@@ -308,9 +292,7 @@ class ai_baset
     std::ostream &out) const;
 
   /// Output the abstract states for a whole program
-  void output(
-    const goto_modelt &goto_model,
-    std::ostream &out) const
+  virtual void output(const goto_modelt &goto_model, std::ostream &out) const
   {
     const namespacet ns(goto_model.symbol_table);
     output(ns, goto_model.goto_functions, out);
@@ -535,6 +517,11 @@ class ai_recursive_interproceduralt : public ai_baset
   {
   }
 
+  // Whole program analysis by starting at the entry function and recursing
+  void operator()(const goto_functionst &goto_functions, const namespacet &ns)
+    override;
+  void operator()(const abstract_goto_modelt &goto_model) override;
+
 protected:
   // Override the function that handles a single function call edge
   bool visit_edge_function_call(

src/analyses/constant_propagator.h

@@ -207,7 +207,7 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
     should_track_valuet should_track_value = track_all_values)
     : dirty(goto_function), should_track_value(should_track_value)
   {
-    operator()(function_identifier, goto_function, ns);
+    ai_baset::operator()(function_identifier, goto_function, ns);
     replace(goto_function, ns);
   }