Merge pull request #4853 from diffblue/simplifier_arith_ops

Simplifier: new interface for arithmetic expressions

Author: Daniel Kroening

src/util/simplify_expr.cpp

@@ -2000,11 +2000,10 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   {
     auto tmp = expr;
 
-    tmp.offset() =
-      plus_exprt(to_byte_extract_expr(expr.op()).offset(), expr.offset());
-    simplify_plus(tmp.offset());
-
+    tmp.offset() = simplify_plus(
+      plus_exprt(to_byte_extract_expr(expr.op()).offset(), expr.offset()));
     tmp.op() = to_byte_extract_expr(expr.op()).op();
+
     return changed(simplify_byte_extract(tmp)); // recursive call
   }
 
@@ -2595,25 +2594,81 @@ bool simplify_exprt::simplify_node(exprt &expr)
     }
   }
   else if(expr.id()==ID_div)
-    no_change = simplify_div(expr) && no_change;
+  {
+    auto r = simplify_div(to_div_expr(expr));
+    if(r.has_changed())
+    {
+      no_change = false;
+      expr = r.expr;
+    }
+  }
   else if(expr.id()==ID_mod)
-    no_change = simplify_mod(expr) && no_change;
+  {
+    auto r = simplify_mod(to_mod_expr(expr));
+    if(r.has_changed())
+    {
+      no_change = false;
+      expr = r.expr;
+    }
+  }
   else if(expr.id()==ID_bitnot)
     no_change = simplify_bitnot(expr) && no_change;
   else if(expr.id()==ID_bitand ||
           expr.id()==ID_bitor ||
           expr.id()==ID_bitxor)
-    no_change = simplify_bitwise(expr) && no_change;
+  {
+    auto r = simplify_bitwise(expr);
+    if(r.has_changed())
+    {
+      no_change = false;
+      expr = r.expr;
+    }
+  }
   else if(expr.id()==ID_ashr || expr.id()==ID_lshr || expr.id()==ID_shl)
-    no_change = simplify_shifts(expr) && no_change;
+  {
+    auto r = simplify_shifts(expr);
+    if(r.has_changed())
+    {
+      no_change = false;
+      expr = r.expr;
+    }
+  }
   else if(expr.id()==ID_power)
-    no_change = simplify_power(expr) && no_change;
+  {
+    auto r = simplify_power(expr);
+    if(r.has_changed())
+    {
+      no_change = false;
+      expr = r.expr;
+    }
+  }
   else if(expr.id()==ID_plus)
-    no_change = simplify_plus(expr) && no_change;
+  {
+    auto r = simplify_plus(to_plus_expr(expr));
+    if(r.has_changed())
+    {
+      no_change = false;
+      expr = r.expr;
+    }
+  }
   else if(expr.id()==ID_minus)
-    no_change = simplify_minus(expr) && no_change;
+  {
+    auto r = simplify_minus(to_minus_expr(expr));
+    if(r.has_changed())
+    {
+      no_change = false;
+      expr = r.expr;
+    }
+  }
   else if(expr.id()==ID_mult)
-    no_change = simplify_mult(expr) && no_change;
+  {
+    auto r = simplify_mult(to_mult_expr(expr));
+    if(r.has_changed())
+    {
+      no_change = false;
+      expr = r.expr;
+    }
+  }
   else if(expr.id()==ID_floatbv_plus ||
           expr.id()==ID_floatbv_minus ||
           expr.id()==ID_floatbv_mult ||

src/util/simplify_expr_class.h

@@ -34,6 +34,7 @@ class bswap_exprt;
 class byte_extract_exprt;
 class byte_update_exprt;
 class dereference_exprt;
+class div_exprt;
 class exprt;
 class extractbits_exprt;
 class floatbv_typecast_exprt;
@@ -42,7 +43,11 @@ class ieee_float_op_exprt;
 class if_exprt;
 class index_exprt;
 class member_exprt;
+class minus_exprt;
+class mod_exprt;
+class mult_exprt;
 class namespacet;
+class plus_exprt;
 class popcount_exprt;
 class refined_string_exprt;
 class tvt;
@@ -127,16 +132,16 @@ class simplify_exprt
   bool simplify_extractbit(exprt &expr);
   bool simplify_extractbits(extractbits_exprt &expr);
   bool simplify_concatenation(exprt &expr);
-  bool simplify_mult(exprt &expr);
-  bool simplify_div(exprt &expr);
-  bool simplify_mod(exprt &expr);
-  bool simplify_plus(exprt &expr);
-  bool simplify_minus(exprt &expr);
+  NODISCARD resultt<> simplify_mult(const mult_exprt &);
+  NODISCARD resultt<> simplify_div(const div_exprt &);
+  NODISCARD resultt<> simplify_mod(const mod_exprt &);
+  NODISCARD resultt<> simplify_plus(const plus_exprt &);
+  NODISCARD resultt<> simplify_minus(const minus_exprt &);
   NODISCARD resultt<> simplify_floatbv_op(const ieee_float_op_exprt &);
   NODISCARD resultt<> simplify_floatbv_typecast(const floatbv_typecast_exprt &);
-  bool simplify_shifts(exprt &expr);
-  bool simplify_power(exprt &expr);
-  bool simplify_bitwise(exprt &expr);
+  NODISCARD resultt<> simplify_shifts(const exprt &);
+  NODISCARD resultt<> simplify_power(const exprt &);
+  NODISCARD resultt<> simplify_bitwise(const exprt &);
   bool simplify_if_preorder(if_exprt &expr);
   bool simplify_if(if_exprt &expr);
   bool simplify_bitnot(exprt &expr);