From ddf7345ed5ddb2b13c7b781c735b3ea899900c69 Mon Sep 17 00:00:00 2001
From: martin <martin@michael>
Date: Wed, 15 Dec 2021 20:46:46 +0000
Subject: [PATCH] Create a new kind of abstract interpreter that does
 function-local analysis

---
 src/analyses/ai.cpp | 27 ++++++++++++++++++++++++---
 src/analyses/ai.h   | 39 +++++++++++++++++++++++++++++++++++++--
 2 files changed, 61 insertions(+), 5 deletions(-)

diff --git a/src/analyses/ai.cpp b/src/analyses/ai.cpp
index a03ba3270c8..6e52de794e5 100644
--- a/src/analyses/ai.cpp
+++ b/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)
 {
diff --git a/src/analyses/ai.h b/src/analyses/ai.h
index cec1e110cca..934e9ec6297 100644
--- a/src/analyses/ai.h
+++ b/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,