Merge pull request #1413 from smowton/smowton/feature/prepare_vsa_for_subclasses

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.get_value_set(expr.op0(), expr_set, ns);
+    value_set.read_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.get_value_set(expr, value_set, goto_symex.ns);
+  state.value_set.read_value_set(expr, value_set, goto_symex.ns);
 
   #if 0
   std::cout << "**************************\n";

src/pointer-analysis/Makefile

@@ -11,7 +11,6 @@ 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::get_value_set(
+void value_sett::read_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)
-    simplify(tmp, ns);
+    simplifier(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))
-      simplify(op1, ns);
+      simplifier(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::get_reference_set(
+void value_sett::read_reference_set(
   const exprt &expr,
   value_setst::valuest &dest,
   const namespacet &ns) const
@@ -1205,6 +1205,12 @@ 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);
   }
 }
@@ -1482,7 +1488,7 @@ void value_sett::do_end_function(
   assign(lhs, rhs, ns, false, false);
 }
 
-void value_sett::apply_code(
+void value_sett::apply_code_rec(
   const codet &code,
   const namespacet &ns)
 {
@@ -1491,7 +1497,7 @@ void value_sett::apply_code(
   if(statement==ID_block)
   {
     forall_operands(it, code)
-      apply_code(to_code(*it), ns);
+      apply_code_rec(to_code(*it), ns);
   }
   else if(statement==ID_function_call)
   {
@@ -1609,6 +1615,10 @@ void value_sett::apply_code(
   {
     // doesn't do anything
   }
+  else if(statement==ID_dead)
+  {
+    // ignore (could potentially prune value set in future)
+  }
   else
   {
     // std::cerr << code.pretty() << '\n';
@@ -1694,3 +1704,6 @@ 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,8 +24,20 @@ 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)
+  value_sett():
+    location_number(0),
+    simplifier(default_simplifier)
+  {
+  }
+
+  explicit value_sett(expr_simplifiert simplifier):
+    location_number(0),
+    simplifier(std::move(simplifier))
   {
   }
 
@@ -166,7 +178,7 @@ class value_sett
   typedef std::unordered_map<idt, entryt, string_hash> valuest;
   #endif
 
-  void get_value_set(
+  void read_value_set(
     const exprt &expr,
     value_setst::valuest &dest,
     const namespacet &ns) const;
@@ -213,7 +225,10 @@ class value_sett
 
   void apply_code(
     const codet &code,
-    const namespacet &ns);
+    const namespacet &ns)
+  {
+    apply_code_rec(code, ns);
+  }
 
   void assign(
     const exprt &lhs,
@@ -232,7 +247,7 @@ class value_sett
     const exprt &lhs,
     const namespacet &ns);
 
-  void get_reference_set(
+  void read_reference_set(
     const exprt &expr,
     value_setst::valuest &dest,
     const namespacet &ns) const;
@@ -242,13 +257,6 @@ 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,
@@ -272,13 +280,6 @@ class value_sett
     const exprt &src,
     exprt &dest) const;
 
-  void assign_rec(
-    const exprt &lhs,
-    const object_mapt &values_rhs,
-    const std::string &suffix,
-    const namespacet &ns,
-    bool add_to_sets);
-
   void do_free(
     const exprt &op,
     const namespacet &ns);
@@ -287,6 +288,67 @@ class value_sett
     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(
+    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,
+    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)
+  {
+  }
 };
 
 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_H

src/pointer-analysis/value_set_analysis.cpp

@@ -13,74 +13,9 @@ 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,