Revert "Value-set analysis: templatise and virtualise to facilitate customisation"

Author: smowton

src/goto-symex/postcondition.cpp

@@ -174,7 +174,7 @@ bool postconditiont::is_used(
     // aliasing may happen here
 
     value_setst::valuest expr_set;
-    value_set.read_value_set(expr.op0(), expr_set, ns);
+    value_set.get_value_set(expr.op0(), expr_set, ns);
     std::unordered_set<irep_idt, irep_id_hash> symbols;
 
     for(value_setst::valuest::const_iterator

src/goto-symex/symex_dereference_state.cpp

@@ -81,7 +81,7 @@ void symex_dereference_statet::get_value_set(
   const exprt &expr,
   value_setst::valuest &value_set)
 {
-  state.value_set.read_value_set(expr, value_set, goto_symex.ns);
+  state.value_set.get_value_set(expr, value_set, goto_symex.ns);
 
   #if 0
   std::cout << "**************************\n";

src/pointer-analysis/Makefile

@@ -11,6 +11,7 @@ SRC = add_failed_symbols.cpp \
       value_set_analysis_fivr.cpp \
       value_set_analysis_fivrns.cpp \
       value_set_dereference.cpp \
+      value_set_domain.cpp \
       value_set_domain_fi.cpp \
       value_set_domain_fivr.cpp \
       value_set_domain_fivrns.cpp \

src/pointer-analysis/show_value_sets.h

@@ -12,10 +12,10 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_POINTER_ANALYSIS_SHOW_VALUE_SETS_H
 #define CPROVER_POINTER_ANALYSIS_SHOW_VALUE_SETS_H
 
-#include <pointer-analysis/value_set_analysis.h>
 #include <util/ui_message.h>
 
 class goto_modelt;
+class value_set_analysist;
 
 void show_value_sets(
   ui_message_handlert::uit,

src/pointer-analysis/value_set.cpp

@@ -311,7 +311,7 @@ bool value_sett::eval_pointer_offset(
   return mod;
 }
 
-void value_sett::read_value_set(
+void value_sett::get_value_set(
   const exprt &expr,
   value_setst::valuest &dest,
   const namespacet &ns) const
@@ -340,7 +340,7 @@ void value_sett::get_value_set(
 {
   exprt tmp(expr);
   if(!is_simplified)
-    simplifier(tmp, ns);
+    simplify(tmp, ns);
 
   get_value_set_rec(tmp, dest, "", tmp.type(), ns);
 }
@@ -809,7 +809,7 @@ void value_sett::get_value_set_rec(
 
     exprt op1=expr.op1();
     if(eval_pointer_offset(op1, ns))
-      simplifier(op1, ns);
+      simplify(op1, ns);
 
     mp_integer op1_offset;
     const typet &op0_type=ns.follow(expr.op0().type());
@@ -908,7 +908,7 @@ void value_sett::dereference_rec(
     dest=src;
 }
 
-void value_sett::read_reference_set(
+void value_sett::get_reference_set(
   const exprt &expr,
   value_setst::valuest &dest,
   const namespacet &ns) const
@@ -1205,12 +1205,6 @@ void value_sett::assign(
     object_mapt values_rhs;
     get_value_set(rhs, values_rhs, ns, is_simplified);
 
-    // Permit custom subclass to alter the read values prior to write:
-    adjust_assign_rhs_values(rhs, ns, values_rhs);
-
-    // Permit custom subclass to perform global side-effects prior to write:
-    apply_assign_side_effects(lhs, rhs, ns);
-
     assign_rec(lhs, values_rhs, "", ns, add_to_sets);
   }
 }
@@ -1488,7 +1482,7 @@ void value_sett::do_end_function(
   assign(lhs, rhs, ns, false, false);
 }
 
-void value_sett::apply_code_rec(
+void value_sett::apply_code(
   const codet &code,
   const namespacet &ns)
 {
@@ -1497,7 +1491,7 @@ void value_sett::apply_code_rec(
   if(statement==ID_block)
   {
     forall_operands(it, code)
-      apply_code_rec(to_code(*it), ns);
+      apply_code(to_code(*it), ns);
   }
   else if(statement==ID_function_call)
   {
@@ -1615,10 +1609,6 @@ void value_sett::apply_code_rec(
   {
     // doesn't do anything
   }
-  else if(statement==ID_dead)
-  {
-    // ignore (could potentially prune value set in future)
-  }
   else
   {
     // std::cerr << code.pretty() << '\n';
@@ -1704,6 +1694,3 @@ exprt value_sett::make_member(
 
   return member_expr;
 }
-
-value_sett::expr_simplifiert value_sett::default_simplifier=
-  [](exprt &e, const namespacet &ns) { simplify(e, ns); };

src/pointer-analysis/value_set.h

@@ -24,20 +24,8 @@ class namespacet;
 
 class value_sett
 {
-  typedef std::function<void(exprt &, const namespacet &)> expr_simplifiert;
-
-  static expr_simplifiert default_simplifier;
-
 public:
-  value_sett():
-    location_number(0),
-    simplifier(default_simplifier)
-  {
-  }
-
-  explicit value_sett(expr_simplifiert simplifier):
-    location_number(0),
-    simplifier(std::move(simplifier))
+  value_sett():location_number(0)
   {
   }
 
@@ -178,7 +166,7 @@ class value_sett
   typedef std::unordered_map<idt, entryt, string_hash> valuest;
   #endif
 
-  void read_value_set(
+  void get_value_set(
     const exprt &expr,
     value_setst::valuest &dest,
     const namespacet &ns) const;
@@ -225,10 +213,7 @@ class value_sett
 
   void apply_code(
     const codet &code,
-    const namespacet &ns)
-  {
-    apply_code_rec(code, ns);
-  }
+    const namespacet &ns);
 
   void assign(
     const exprt &lhs,
@@ -247,7 +232,7 @@ class value_sett
     const exprt &lhs,
     const namespacet &ns);
 
-  void read_reference_set(
+  void get_reference_set(
     const exprt &expr,
     value_setst::valuest &dest,
     const namespacet &ns) const;
@@ -257,6 +242,13 @@ class value_sett
     const namespacet &ns) const;
 
 protected:
+  void get_value_set_rec(
+    const exprt &expr,
+    object_mapt &dest,
+    const std::string &suffix,
+    const typet &original_type,
+    const namespacet &ns) const;
+
   void get_value_set(
     const exprt &expr,
     object_mapt &dest,
@@ -280,75 +272,21 @@ class value_sett
     const exprt &src,
     exprt &dest) const;
 
-  void do_free(
-    const exprt &op,
-    const namespacet &ns);
-
-  exprt make_member(
-    const exprt &src,
-    const irep_idt &component_name,
-    const namespacet &ns);
-
-  // Expression simplification:
-
-private:
-  /// Expression simplification function; by default, plain old
-  /// util/simplify_expr, but can be customised by subclass.
-  expr_simplifiert simplifier;
-
-protected:
-  /// Run registered expression simplifier
-  void run_simplifier(exprt &e, const namespacet &ns)
-  {
-    simplifier(e, ns);
-  }
-
-  // Subclass customisation points:
-
-protected:
-  /// Subclass customisation point for recursion over RHS expression:
-  virtual void get_value_set_rec(
-    const exprt &expr,
-    object_mapt &dest,
-    const std::string &suffix,
-    const typet &original_type,
-    const namespacet &ns) const;
-
-  /// Subclass customisation point for recursion over LHS expression:
-  virtual void assign_rec(
+  void assign_rec(
     const exprt &lhs,
     const object_mapt &values_rhs,
     const std::string &suffix,
     const namespacet &ns,
     bool add_to_sets);
 
-  /// Subclass customisation point for applying code to this domain:
-  virtual void apply_code_rec(
-    const codet &code,
+  void do_free(
+    const exprt &op,
     const namespacet &ns);
 
- private:
-  /// Subclass customisation point to filter or otherwise alter the value-set
-  /// returned from get_value_set before it is passed into assign. For example,
-  /// this is used in one subclass to tag and thus differentiate values that
-  /// originated in a particular place, vs. those that have been copied.
-  virtual void adjust_assign_rhs_values(
-    const exprt &rhs,
-    const namespacet &ns,
-    object_mapt &rhs_values) const
-  {
-  }
-
-  /// Subclass customisation point to apply global side-effects to this domain,
-  /// after RHS values are read but before they are written. For example, this
-  /// is used in a recency-analysis plugin to demote existing most-recent
-  /// objects to general case ones.
-  virtual void apply_assign_side_effects(
-    const exprt &lhs,
-    const exprt &rhs,
-    const namespacet &ns)
-  {
-  }
+  exprt make_member(
+    const exprt &src,
+    const irep_idt &component_name,
+    const namespacet &ns);
 };
 
 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_H

src/pointer-analysis/value_set_analysis.cpp

@@ -13,9 +13,74 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/prefix.h>
 #include <util/cprover_prefix.h>
+#include <util/xml_expr.h>
+#include <util/xml.h>
 
 #include <langapi/language_util.h>
 
+void value_set_analysist::initialize(
+  const goto_programt &goto_program)
+{
+  baset::initialize(goto_program);
+}
+
+void value_set_analysist::initialize(
+  const goto_functionst &goto_functions)
+{
+  baset::initialize(goto_functions);
+}
+
+void value_set_analysist::convert(
+  const goto_programt &goto_program,
+  const irep_idt &identifier,
+  xmlt &dest) const
+{
+  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=(*this)[i_it].value_set;
+
+    xmlt &i=dest.new_element("instruction");
+    i.new_element()=::xml(location);
+
+    for(value_sett::valuest::const_iterator
+        v_it=value_set.values.begin();
+        v_it!=value_set.values.end();
+        v_it++)
+    {
+      xmlt &var=i.new_element("variable");
+      var.new_element("identifier").data=
+        id2string(v_it->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,