Unwind vsd customisation from simply_exprt.

We can pick up the special case for pointer addition in
abstract_object::expression_transform.

Author: jezhiggins

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -94,7 +94,7 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
     return abstract_object_factory(expr.type(), ns, false, true);
 
   // first try to canonicalise, including constant folding
-  const exprt &simplified_expr = simplify_vsd_expr(expr, ns);
+  const exprt &simplified_expr = simplify_expr(expr, ns);
 
   const irep_idt simplified_id = simplified_expr.id();
   if(simplified_id == ID_symbol)
@@ -845,18 +845,3 @@ exprt assume_greater_than(
 
   return assume_less_than(env, symmetric_expr, ns);
 }
-
-class simplify_vsd_exprt : public simplify_exprt
-{
-public:
-  explicit 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_object.cpp

@@ -10,6 +10,7 @@
 
 #include <analyses/variable-sensitivity/abstract_environment.h>
 
+#include <util/mathematical_types.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
@@ -102,6 +103,12 @@ abstract_object_pointert abstract_objectt::abstract_object_meet_internal(
   return shared_from_this();
 }
 
+static bool is_pointer_addition(const exprt &expr)
+{
+  return (expr.id() == ID_plus) && (expr.type().id() == ID_pointer) &&
+         (expr.operands().size() == 2) && is_number(expr.operands()[1].type());
+}
+
 abstract_object_pointert abstract_objectt::expression_transform(
   const exprt &expr,
   const std::vector<abstract_object_pointert> &operands,
@@ -117,7 +124,8 @@ abstract_object_pointert abstract_objectt::expression_transform(
     op = const_op.is_nil() ? op : const_op;
   }
 
-  simplify_vsd_expr(copy, ns);
+  if(!is_pointer_addition(copy))
+    copy = simplify_expr(copy, ns);
 
   for(const exprt &op : copy.operands())
   {

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp

@@ -14,6 +14,7 @@
 #include <analyses/variable-sensitivity/value_set_pointer_abstract_object.h>
 #include <numeric>
 #include <util/pointer_expr.h>
+#include <util/simplify_expr.h>
 
 #include "abstract_environment.h"
 
@@ -179,7 +180,7 @@ exprt value_set_pointer_abstract_objectt::ptr_comparison_expr(
     {
       auto ops = std::vector<abstract_object_pointert>{lhsp, rhsp};
       auto comparison = lhsp->ptr_comparison_expr(expr, ops, environment, ns);
-      auto result = simplify_vsd_expr(comparison, ns);
+      auto result = simplify_expr(comparison, ns);
       comparisons.insert(result);
     }
   }

src/util/simplify_expr_class.h

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