Unwind vsd customisation from simplify_exprt, move to simplify_vsd_exprt

Author: jezhiggins

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -10,6 +10,7 @@
 #include <analyses/variable-sensitivity/abstract_object_statistics.h>
 #include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
 #include <util/expr_util.h>
+#include <util/mathematical_types.h>
 #include <util/simplify_expr.h>
 #include <util/simplify_expr_class.h>
 
@@ -851,7 +852,27 @@ class simplify_vsd_exprt : public simplify_exprt
 public:
   explicit simplify_vsd_exprt(const namespacet &_ns) : simplify_exprt(_ns)
   {
-    vsd_pointers = true;
+  }
+
+  NODISCARD resultt<> simplify_node(exprt expr) override
+  {
+    if(expr.id() == ID_plus)
+      return vsd_simplify_plus(to_plus_expr(expr));
+    return simplify_exprt::simplify_node(expr);
+  }
+
+private:
+  resultt<> vsd_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()))
+    {
+      return unchanged(expr);
+    }
+
+    return simplify_exprt::simplify_plus(expr);
   }
 };
 

src/analyses/variable-sensitivity/context_abstract_object.cpp

@@ -87,6 +87,7 @@ abstract_object_pointert context_abstract_objectt::expression_transform(
   const namespacet &ns) const
 {
   PRECONDITION(expr.operands().size() == operands.size());
+
   std::vector<abstract_object_pointert> child_operands;
 
   std::transform(

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