Create a new kind of abstract interpreter that does function-local analysis

Author: martin

src/analyses/ai.cpp

@@ -411,7 +411,7 @@ bool ai_baset::visit_edge(
   return return_value;
 }
 
-bool ai_baset::visit_edge_function_call(
+bool ai_localt::visit_edge_function_call(
   const irep_idt &calling_function_id,
   trace_ptrt p_call,
   locationt l_return,
@@ -422,11 +422,11 @@ bool ai_baset::visit_edge_function_call(
   const namespacet &ns)
 {
   messaget log(message_handler);
-  log.progress() << "ai_baset::visit_edge_function_call from "
+  log.progress() << "ai_localt::visit_edge_function_call from "
                  << p_call->current_location()->location_number << " to "
                  << l_return->location_number << messaget::eom;
 
-  // The default implementation is not interprocedural
+  // This implementation is not interprocedural
   // so the effects of the call are approximated but nothing else
   return visit_edge(
     calling_function_id,
@@ -537,6 +537,27 @@ 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)
 {

src/analyses/ai.h

@@ -469,7 +469,7 @@ class ai_baset
     working_sett &working_set,
     const goto_programt &callee,
     const goto_functionst &goto_functions,
-    const namespacet &ns);
+    const namespacet &ns) = 0;
 
   /// For creating history objects
   std::unique_ptr<ai_history_factory_baset> history_factory;
@@ -505,6 +505,40 @@ class ai_baset
   message_handlert &message_handler;
 };
 
+// Perform function local analysis on all functions in a program.
+// No interprocedural analysis other than what a domain does when
+// visit()'ing an edge that skips a function call.
+class ai_localt : public ai_baset
+{
+public:
+  ai_localt(
+    std::unique_ptr<ai_history_factory_baset> &&hf,
+    std::unique_ptr<ai_domain_factory_baset> &&df,
+    std::unique_ptr<ai_storage_baset> &&st,
+    message_handlert &mh)
+    : ai_baset(std::move(hf), std::move(df), std::move(st), mh)
+  {
+  }
+
+  // Handle every function independently
+  void operator()(const goto_functionst &goto_functions, const namespacet &ns)
+    override;
+  void operator()(const abstract_goto_modelt &goto_model) override;
+
+protected:
+  // Implement the function that handles a single function call edge
+  // by a single edge that gets the domain to approximate the whole function call
+  bool visit_edge_function_call(
+    const irep_idt &calling_function_id,
+    trace_ptrt p_call,
+    locationt l_return,
+    const irep_idt &callee_function_id,
+    working_sett &working_set,
+    const goto_programt &callee,
+    const goto_functionst &goto_functions,
+    const namespacet &ns) override;
+};
+
 // Perform interprocedural analysis by simply recursing in the interpreter
 // This can lead to a call stack overflow if the domain has a large height
 class ai_recursive_interproceduralt : public ai_baset
@@ -525,7 +559,8 @@ class ai_recursive_interproceduralt : public ai_baset
   void operator()(const abstract_goto_modelt &goto_model) override;
 
 protected:
-  // Override the function that handles a single function call edge
+  // Implement the function that handles a single function call edge
+  // by a recursive call to fixpoint
   bool visit_edge_function_call(
     const irep_idt &calling_function_id,
     trace_ptrt p_call,