Templatize and virtualize value-set analysis

This templates value-set-analysis, so that it can be subclassed
providing a value-set extension, and virtualizes value-set so it
can similarly be extended.

Author: smowton

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

@@ -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);
   }
 }
@@ -1484,7 +1490,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)
 {
@@ -1493,7 +1499,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)
   {

src/pointer-analysis/value_set.h

@@ -248,7 +248,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,
@@ -277,13 +280,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,
@@ -307,13 +303,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);
@@ -322,6 +311,53 @@ class value_sett
     const exprt &src,
     const irep_idt &component_name,
     const namespacet &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

@@ -18,22 +18,11 @@ Author: Daniel Kroening, [email protected]
 
 #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(
+void value_sets_to_xml(
+  std::function<const value_sett &(goto_programt::const_targett)> get_value_set,
   const goto_programt &goto_program,
   const irep_idt &identifier,
-  xmlt &dest) const
+  xmlt &dest)
 {
   source_locationt previous_location;
 
@@ -48,7 +37,7 @@ void value_set_analysist::convert(
       continue;
 
     // find value set
-    const value_sett &value_set=(*this)[i_it].value_set;
+    const value_sett &value_set=get_value_set(i_it);
 
     xmlt &i=dest.new_element("instruction");
     i.new_element()=::xml(location);
@@ -81,6 +70,7 @@ void value_set_analysist::convert(
     }
   }
 }
+
 void convert(
   const goto_functionst &goto_functions,
   const value_set_analysist &value_set_analysis,

src/pointer-analysis/value_set_analysis.h

@@ -20,26 +20,37 @@ Author: Daniel Kroening, [email protected]
 
 class xmlt;
 
-class value_set_analysist:
+void value_sets_to_xml(
+  std::function<const value_sett &(goto_programt::const_targett)> get_value_set,
+  const goto_programt &goto_program,
+  const irep_idt &identifier,
+  xmlt &dest);
+
+template<class VSDT>
+class value_set_analysis_templatet:
   public value_setst,
-  public static_analysist<value_set_domaint>
+  public static_analysist<VSDT>
 {
 public:
-  explicit value_set_analysist(const namespacet &_ns):
-    static_analysist<value_set_domaint>(_ns)
+  typedef VSDT domaint;
+  typedef static_analysist<domaint> baset;
+  typedef typename baset::locationt locationt;
+
+  explicit value_set_analysis_templatet(const namespacet &ns):baset(ns)
   {
   }
 
-  typedef static_analysist<value_set_domaint> baset;
-
-  // overloading
-  virtual void initialize(const goto_programt &goto_program);
-  virtual void initialize(const goto_functionst &goto_functions);
-
   void convert(
     const goto_programt &goto_program,
     const irep_idt &identifier,
-    xmlt &dest) const;
+    xmlt &dest) const
+  {
+    value_sets_to_xml(
+      [this](locationt l) { return (*this)[l].value_set; },
+      goto_program,
+      identifier,
+      dest);
+  }
 
 public:
   // interface value_sets
@@ -48,10 +59,14 @@ class value_set_analysist:
     const exprt &expr,
     value_setst::valuest &dest)
   {
-    (*this)[l].value_set.get_value_set(expr, dest, ns);
+    (*this)[l].value_set.get_value_set(expr, dest, baset::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,

src/pointer-analysis/value_set_domain.h

@@ -17,14 +17,15 @@ Author: Daniel Kroening, [email protected]
 
 #include "value_set.h"
 
-class value_set_domaint:public domain_baset
+template<class VST>
+class value_set_domain_templatet:public domain_baset
 {
 public:
-  value_sett value_set;
+  VST value_set;
 
   // overloading
 
-  bool merge(const value_set_domaint &other, locationt to)
+  bool merge(const value_set_domain_templatet<VST> &other, locationt to)
   {
     return value_set.make_union(other.value_set);
   }
@@ -58,4 +59,8 @@ class value_set_domaint:public domain_baset
   }
 };
 
+typedef value_set_domain_templatet<value_sett> value_set_domaint;
+
+#include "value_set_domain_transform.inc"
+
 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_H

src/pointer-analysis/value_set_domain.cpp renamed to src/pointer-analysis/value_set_domain_transform.inc

@@ -9,11 +9,12 @@ Author: Daniel Kroening, [email protected]
 /// \file
 /// Value Set
 
-#include "value_set_domain.h"
+// The body of value_set_domaint<VST>::transform, included from
+// value_set_domain.h but retained in this out-of-line file to ease
+// git merges:
 
-#include <util/std_code.h>
-
-void value_set_domaint::transform(
+template<class VST>
+void value_set_domain_templatet<VST>::transform(
   const namespacet &ns,
   locationt from_l,
   locationt to_l)
@@ -25,9 +26,13 @@ void value_set_domaint::transform(
     break;
 
   case END_FUNCTION:
-    value_set.do_end_function(static_analysis_baset::get_return_lhs(to_l), ns);
+  {
+    value_set.do_end_function(
+      static_analysis_baset::get_return_lhs(to_l), ns);
     break;
+  }
 
+  // Note intentional fall-through here:
   case RETURN:
   case OTHER:
   case ASSIGN:
@@ -44,7 +49,8 @@ void value_set_domaint::transform(
       const code_function_callt &code=
         to_code_function_call(from_l->code);
 
-      value_set.do_function_call(to_l->function, code.arguments(), ns);
+      value_set.do_function_call(
+        to_l->function, code.arguments(), ns);
     }
     break;