Merge pull request #1499 from smowton/smowton/feature/vsa_take_two

Templatize value-set analysis

Author: tautschnig

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

@@ -33,6 +33,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "add_failed_symbols.h"
 
+// Due to a large number of functions defined inline, `value_sett` and
+// associated types are documented in its header file, `value_set.h`.
+
 const value_sett::object_map_dt value_sett::object_map_dt::blank{};
 object_numberingt value_sett::object_numbering;
 
@@ -1205,6 +1208,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 +1493,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 +1502,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)
   {
@@ -1611,6 +1620,10 @@ void value_sett::apply_code(
   {
     // doesn't do anything
   }
+  else if(statement==ID_dead)
+  {
+    // Ignore by default; could prune the value set.
+  }
   else
   {
     // std::cerr << code.pretty() << '\n';