Port value_set_analysist and value_set_domain to the ai framework

This removes the last in-tree use of static_analysis.{h,cpp}.
It also gives the option of using value_set_domain with the history
options to perform per-path value-set analysis.

Author: martin

jbmc/unit/pointer-analysis/custom_value_set_analysis.cpp

@@ -198,12 +198,12 @@ SCENARIO("test_value_set_analysis",
       std::prev(test_function.instructions.end());
 
     value_set_analysist normal_analysis(ns);
-    normal_analysis(goto_model.goto_functions);
+    normal_analysis(TEST_FUNCTION_NAME, test_function, ns);
     const auto &normal_function_end_vs=
       normal_analysis[test_function_end].value_set;
 
     test_value_set_analysist test_analysis(ns);
-    test_analysis(goto_model.goto_functions);
+    test_analysis(TEST_FUNCTION_NAME, test_function, ns);
     const auto &test_function_end_vs=
       test_analysis[test_function_end].value_set;
 

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -319,7 +319,7 @@ int goto_instrument_parse_optionst::doit()
       log.status() << "Pointer Analysis" << messaget::eom;
       namespacet ns(goto_model.symbol_table);
       value_set_analysist value_set_analysis(ns);
-      value_set_analysis(goto_model.goto_functions);
+      value_set_analysis(goto_model);
       show_value_sets(
         ui_message_handler.get_ui(), goto_model, value_set_analysis);
       return CPROVER_EXIT_SUCCESS;
@@ -550,7 +550,7 @@ int goto_instrument_parse_optionst::doit()
 
       log.status() << "Pointer Analysis" << messaget::eom;
       value_set_analysist value_set_analysis(ns);
-      value_set_analysis(goto_model.goto_functions);
+      value_set_analysis(goto_model);
 
       const symbolt &symbol=ns.lookup(ID_main);
       symbol_exprt main(symbol.name, symbol.type);
@@ -1534,7 +1534,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     log.status() << "Pointer Analysis" << messaget::eom;
     const namespacet ns(goto_model.symbol_table);
     value_set_analysist value_set_analysis(ns);
-    value_set_analysis(goto_model.goto_functions);
+    value_set_analysis(goto_model);
 
     if(cmdline.isset("remove-pointers"))
     {

src/pointer-analysis/show_value_sets.cpp

@@ -27,42 +27,39 @@ void show_value_sets(
   switch(ui)
   {
   case ui_message_handlert::uit::XML_UI:
-    {
-      xmlt xml;
-      convert(goto_model.goto_functions, value_set_analysis, xml);
-      std::cout << xml << '\n';
-    }
+    std::cout << value_set_analysis.output_xml(goto_model);
     break;
 
   case ui_message_handlert::uit::PLAIN:
-    value_set_analysis.output(goto_model.goto_functions, std::cout);
+    value_set_analysis.output(goto_model, std::cout);
     break;
 
   case ui_message_handlert::uit::JSON_UI:
-    UNIMPLEMENTED;
+    std::cout << value_set_analysis.output_json(goto_model);
+    break;
   }
 }
 
 void show_value_sets(
   ui_message_handlert::uit ui,
+  const namespacet &ns,
+  const irep_idt &function_name,
   const goto_programt &goto_program,
   const value_set_analysist &value_set_analysis)
 {
   switch(ui)
   {
   case ui_message_handlert::uit::XML_UI:
-    {
-      xmlt xml;
-      convert(goto_program, value_set_analysis, xml);
-      std::cout << xml << '\n';
-    }
+    std::cout << value_set_analysis.output_xml(ns, function_name, goto_program);
     break;
 
   case ui_message_handlert::uit::PLAIN:
-    value_set_analysis.output(goto_program, std::cout);
+    value_set_analysis.output(ns, function_name, goto_program, std::cout);
     break;
 
   case ui_message_handlert::uit::JSON_UI:
-    UNIMPLEMENTED;
+    std::cout << value_set_analysis.output_json(
+      ns, function_name, goto_program);
+    break;
   }
 }

src/pointer-analysis/value_set.cpp

@@ -26,6 +26,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/std_code.h>
 #include <util/symbol.h>
+#include <util/xml.h>
 
 #include <ostream>
 
@@ -217,6 +218,39 @@ void value_sett::output(std::ostream &out, const std::string &indent) const
   });
 }
 
+xmlt value_sett::output_xml(void) const
+{
+  xmlt output;
+
+  value_sett::valuest::viewt view;
+  this->values.get_view(view);
+
+  for(const auto &values_entry : view)
+  {
+    xmlt &var = output.new_element("variable");
+    var.new_element("identifier").data = id2string(values_entry.first);
+
+#if 0
+    const value_sett::expr_sett &expr_set=
+      value_entries.expr_set();
+
+    for(value_sett::expr_sett::const_iterator
+          e_it=expr_set.begin();
+          e_it!=expr_set.end();
+          e_it++)
+      {
+        std::string value_str=
+          from_expr(ns, identifier, *e_it);
+
+        var.new_element("value").data=
+          xmlt::escape(value_str);
+      }
+#endif
+  }
+
+  return output;
+}
+
 exprt value_sett::to_expr(const object_map_dt::value_type &it) const
 {
   const exprt &object=object_numbering[it.first];

src/pointer-analysis/value_set.h

@@ -22,6 +22,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "value_sets.h"
 
 class namespacet;
+class xmlt;
 
 /// State type in value_set_domaint, used in value-set analysis and goto-symex.
 /// Represents a mapping from expressions to the addresses that may be stored
@@ -287,6 +288,9 @@ class value_sett
   /// \param indent: string to use for indentation of the output
   void output(std::ostream &out, const std::string &indent = "") const;
 
+  /// Output the value set formatted as XML
+  xmlt output_xml(void) const;
+
   /// Stores the LHS ID -> RHS expression set map. See `valuest` documentation
   /// for more detail.
   valuest values;

src/pointer-analysis/value_set_analysis.cpp

@@ -11,86 +11,3 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "value_set_analysis.h"
 
-#include <util/xml_irep.h>
-
-void value_sets_to_xml(
-  const std::function<const value_sett &(goto_programt::const_targett)>
-    &get_value_set,
-  const goto_programt &goto_program,
-  xmlt &dest)
-{
-  source_locationt previous_location;
-
-  forall_goto_program_instructions(i_it, goto_program)
-  {
-    const source_locationt &location = i_it->source_location();
-
-    if(location==previous_location)
-      continue;
-
-    if(location.is_nil() || location.get_file().empty())
-      continue;
-
-    // find value set
-    const value_sett &value_set=get_value_set(i_it);
-
-    xmlt &i=dest.new_element("instruction");
-    i.new_element()=::xml(location);
-
-    value_sett::valuest::viewt view;
-    value_set.values.get_view(view);
-
-    for(const auto &values_entry : view)
-    {
-      xmlt &var=i.new_element("variable");
-      var.new_element("identifier").data = id2string(values_entry.first);
-
-#if 0
-      const value_sett::expr_sett &expr_set=
-        v_it->second.expr_set();
-
-      for(value_sett::expr_sett::const_iterator
-          e_it=expr_set.begin();
-          e_it!=expr_set.end();
-          e_it++)
-      {
-        std::string value_str=
-          from_expr(ns, identifier, *e_it);
-
-        var.new_element("value").data=
-          xmlt::escape(value_str);
-      }
-#endif
-    }
-  }
-}
-
-void convert(
-  const goto_functionst &goto_functions,
-  const value_set_analysist &value_set_analysis,
-  xmlt &dest)
-{
-  dest=xmlt("value_set_analysis");
-
-  for(goto_functionst::function_mapt::const_iterator
-      f_it=goto_functions.function_map.begin();
-      f_it!=goto_functions.function_map.end();
-      f_it++)
-  {
-    xmlt &f=dest.new_element("function");
-    f.new_element("identifier").data=id2string(f_it->first);
-    value_set_analysis.convert(f_it->second.body, f);
-  }
-}
-
-void convert(
-  const goto_programt &goto_program,
-  const value_set_analysist &value_set_analysis,
-  xmlt &dest)
-{
-  dest=xmlt("value_set_analysis");
-
-  value_set_analysis.convert(
-    goto_program,
-    dest.new_element("program"));
-}

src/pointer-analysis/value_set_analysis.h

@@ -12,38 +12,29 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_H
 #define CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_H
 
-#define USE_DEPRECATED_STATIC_ANALYSIS_H
-#include <analyses/static_analysis.h>
+#include <analyses/ai.h>
 
 #include "value_set_domain.h"
 #include "value_sets.h"
 
-class xmlt;
-
-void value_sets_to_xml(
-  const std::function<const value_sett &(goto_programt::const_targett)>
-    &get_value_set,
-  const goto_programt &goto_program,
-  xmlt &dest);
-
 /// This template class implements a data-flow analysis which keeps track of
 /// what values different variables might have at different points in the
 /// program. It is used through the alias `value_set_analysist`, so `VSDT` is
 /// `value_set_domain_templatet<value_sett>`.
-///
-/// Note: it is currently based on `static_analysist`, which is obsolete. It
-/// should be moved onto `ait`.
-template<class VSDT>
-class value_set_analysis_templatet:
-  public value_setst,
-  public static_analysist<VSDT>
+template <class VSDT>
+class value_set_analysis_templatet : public value_setst, public ait<VSDT>
 {
+private:
+  const namespacet &ns;
+
 public:
   typedef VSDT domaint;
-  typedef static_analysist<domaint> baset;
+  typedef ait<domaint> baset;
   typedef typename baset::locationt locationt;
 
-  explicit value_set_analysis_templatet(const namespacet &ns):baset(ns)
+  explicit value_set_analysis_templatet(const namespacet &_ns)
+    : baset(util_make_unique<ai_domain_factory_location_constructort<VSDT>>()),
+      ns(_ns)
   {
   }
 
@@ -52,38 +43,17 @@ class value_set_analysis_templatet:
     return (*this)[t].value_set;
   }
 
-  void convert(
-    const goto_programt &goto_program,
-    xmlt &dest) const
-  {
-    using std::placeholders::_1;
-    value_sets_to_xml(
-      std::bind(&value_set_analysis_templatet::get_value_set, *this, _1),
-      goto_program,
-      dest);
-  }
-
 public:
   // interface value_sets
   std::vector<exprt>
   get_values(const irep_idt &, locationt l, const exprt &expr) override
   {
-    return (*this)[l].value_set.get_value_set(expr, baset::ns);
+    return (*this)[l].value_set.get_value_set(expr, ns);
   }
 };
 
 typedef
   value_set_analysis_templatet<value_set_domain_templatet<value_sett>>
   value_set_analysist;
 
-void convert(
-  const goto_functionst &goto_functions,
-  const value_set_analysist &value_set_analysis,
-  xmlt &dest);
-
-void convert(
-  const goto_programt &goto_program,
-  const value_set_analysist &value_set_analysis,
-  xmlt &dest);
-
 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_ANALYSIS_H