Move the handling of whole program analysis into the interprocedural …

…code
diffblue · Aug 11, 2022 · d37e4b3 · d37e4b3
1 parent ab93180
commit d37e4b3
Show file tree

Hide file tree

Showing 3 changed files with 30 additions and 24 deletions.
diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
@@ -537,6 +537,25 @@ bool ai_baset::visit_end_function(
   return false;
 }
 
+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,

diff --git a/src/analyses/ai.h b/src/analyses/ai.h
@@ -155,28 +155,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)
@@ -288,9 +272,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);
@@ -537,6 +519,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(

diff --git a/src/analyses/constant_propagator.h b/src/analyses/constant_propagator.h
@@ -212,7 +212,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);
   }