Add switch to make pointer simplication changes VSD only

Author: jezhiggins

scripts/expected_doxygen_warnings.txt

@@ -1,16 +1,16 @@
-/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_glucose.cpp:246: warning: no matching class member found for 
+/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_glucose.cpp:253: warning: no matching class member found for
   template
   satcheck_glucose_baset< Glucose::Solver >::~satcheck_glucose_baset()
 
-/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_glucose.cpp:252: warning: no matching class member found for 
+/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_glucose.cpp:259: warning: no matching class member found for
   template
   satcheck_glucose_baset< Glucose::SimpSolver >::~satcheck_glucose_baset()
 
-/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_minisat2.cpp:313: warning: no matching class member found for 
+/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_minisat2.cpp:316: warning: no matching class member found for
   template
   satcheck_minisat2_baset< Minisat::Solver >::~satcheck_minisat2_baset()
 
-/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_minisat2.cpp:319: warning: no matching class member found for 
+/home/runner/work/cbmc/cbmc/src/solvers/sat/satcheck_minisat2.cpp:322: warning: no matching class member found for
   template
   satcheck_minisat2_baset< Minisat::SimpSolver >::~satcheck_minisat2_baset()
 
@@ -94,7 +94,7 @@ warning: Included by graph for 'message.h' not generated, too many nodes (117),
 warning: Included by graph for 'namespace.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'pointer_expr.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'prefix.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (76), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_expr.h' not generated, too many nodes (243), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_types.h' not generated, too many nodes (117), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -17,6 +17,7 @@
 #include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
 #include <util/pointer_expr.h>
 #include <util/simplify_expr.h>
+#include <util/simplify_expr_class.h>
 
 #include <algorithm>
 #include <functional>
@@ -33,14 +34,16 @@ std::vector<abstract_object_pointert> eval_operands(
   const abstract_environmentt &env,
   const namespacet &ns);
 
+exprt simplify_vsd_expr(exprt src, const namespacet &ns);
+
 abstract_object_pointert
 abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
 {
   if(bottom)
     return abstract_object_factory(expr.type(), ns, false, true);
 
   // first try to canonicalise, including constant folding
-  const exprt &simplified_expr = simplify_expr(expr, ns);
+  const exprt &simplified_expr = simplify_vsd_expr(expr, ns);
 
   const irep_idt simplified_id = simplified_expr.id();
   if(simplified_id == ID_symbol)
@@ -477,3 +480,18 @@ std::vector<abstract_object_pointert> eval_operands(
 
   return operands;
 }
+
+class simplify_vsd_exprt : public simplify_exprt
+{
+public:
+  simplify_vsd_exprt(const namespacet &_ns) : simplify_exprt(_ns)
+  {
+    vsd_pointers = true;
+  }
+};
+
+exprt simplify_vsd_expr(exprt src, const namespacet &ns)
+{
+  simplify_vsd_exprt(ns).simplify(src);
+  return src;
+}

src/analyses/variable-sensitivity/abstract_environment.h

@@ -28,6 +28,8 @@
 #include <util/sharing_map.h>
 #include <util/std_expr.h>
 
+exprt simplify_vsd_expr(exprt src, const namespacet &ns);
+
 class variable_sensitivity_object_factoryt;
 using variable_sensitivity_object_factory_ptrt =
   std::shared_ptr<variable_sensitivity_object_factoryt>;

src/analyses/variable-sensitivity/abstract_object.cpp

@@ -120,7 +120,7 @@ abstract_object_pointert abstract_objectt::expression_transform(
     op = const_op.is_nil() ? op : const_op;
   }
 
-  simplify(copy, ns);
+  simplify_vsd_expr(copy, ns);
 
   for(const exprt &op : copy.operands())
   {

src/util/simplify_expr_class.h

@@ -71,11 +71,13 @@ class with_exprt;
 class simplify_exprt
 {
 public:
-  explicit simplify_exprt(const namespacet &_ns):
-    do_simplify_if(true),
-    ns(_ns)
+  explicit simplify_exprt(const namespacet &_ns)
+    : do_simplify_if(true),
+      ns(_ns),
+      vsd_pointers(false)
 #ifdef DEBUG_ON_DEMAND
-    , debug_on(false)
+      ,
+      debug_on(false)
 #endif
   {
 #ifdef DEBUG_ON_DEMAND
@@ -238,6 +240,8 @@ class simplify_exprt
 
 protected:
   const namespacet &ns;
+  bool vsd_pointers;
+
 #ifdef DEBUG_ON_DEMAND
   bool debug_on;
 #endif

src/util/simplify_expr_int.cpp

@@ -455,8 +455,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_plus(const plus_exprt &expr)
 
     // (T*)p+a - don't simplify any further
     if(
-      expr.type().id() == ID_pointer && expr.operands().size() == 2 &&
-      is_number(expr.op1().type()))
+      vsd_pointers && expr.type().id() == ID_pointer &&
+      expr.operands().size() == 2 && is_number(expr.op1().type()))
     {
       return unchanged(expr);
     }
@@ -599,7 +599,8 @@ simplify_exprt::simplify_minus(const minus_exprt &expr)
     if(operands[0]==operands[1])
       return from_integer(0, minus_expr.type());
 
-    return to_ptr_diff_expr(minus_expr);
+    if(vsd_pointers)
+      return to_ptr_diff_expr(minus_expr);
   }
 
   return unchanged(expr);