A new abstract interpreter for performing function-local analysis

src/analyses/ai.cpp

@@ -410,7 +410,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,
@@ -421,11 +421,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,
@@ -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);
@@ -485,7 +467,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;
@@ -521,6 +503,41 @@ 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
+  // using 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
@@ -535,8 +552,14 @@ 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
+  // 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,

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);
   }
 

src/goto-analyzer/build_analyzer.cpp

@@ -39,7 +39,8 @@ std::unique_ptr<ai_baset> build_analyzer(
   // These support all of the option categories
   if(
     options.get_bool_option("recursive-interprocedural") ||
-    options.get_bool_option("three-way-merge"))
+    options.get_bool_option("three-way-merge") ||
+    options.get_bool_option("local") ||)
   {
     // Build the history factory
     std::unique_ptr<ai_history_factory_baset> hf = nullptr;
@@ -111,6 +112,11 @@ std::unique_ptr<ai_baset> build_analyzer(
             std::move(hf), std::move(df), std::move(st), mh);
         }
       }
+      else if(options.get_bool_option("local"))
+      {
+        return util_make_unique<ai_localt>(
+          std::move(hf), std::move(df), std::move(st), mh);
+      }
     }
   }
   else if(options.get_bool_option("legacy-ait"))

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -225,6 +225,8 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
       options.set_option("recursive-interprocedural", true);
     else if(cmdline.isset("three-way-merge"))
       options.set_option("three-way-merge", true);
+    else if(cmdline.isset("local"))
+      options.set_option("local", true);
     else if(cmdline.isset("legacy-ait") || cmdline.isset("location-sensitive"))
     {
       options.set_option("legacy-ait", true);
@@ -758,6 +760,7 @@ void goto_analyzer_parse_optionst::help()
     " reasoning\n"
     " {y--three-way-merge} \t use VSD's three-way merge on return from function"
     " call\n"
+    " {y--local} \t perform function-local analysis for every function\n"
     " {y--legacy-concurrent} \t legacy-ait with an extended fixed-point for"
     " concurrency\n"
     " {y--location-sensitive} \t use location-sensitive abstract interpreter\n"

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -117,7 +117,8 @@ class optionst;
   "(recursive-interprocedural)" \
   "(three-way-merge)" \
   "(legacy-ait)" \
-  "(legacy-concurrent)"
+  "(legacy-concurrent)" \
+  "(local)"
 
 #define GOTO_ANALYSER_OPTIONS_HISTORY \
   "(ahistorical)" \