simplifier: new interface for simplify_node

This improves type safety.

Author: Daniel Kroening

src/util/simplify_expr.cpp

@@ -572,8 +572,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
       op_type.id() == ID_floatbv ? ID_ieee_float_notequal : ID_notequal,
       from_integer(0, op_type));
     inequality.add_source_location()=expr.source_location();
-    simplify_node(inequality);
-    return std::move(inequality);
+    return changed(simplify_node(inequality));
   }
 
   // eliminate casts from proper bool
@@ -612,9 +611,8 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
   {
     // rewrite (_Bool)x to (_Bool)(x!=0)
     exprt inequality = is_not_zero(expr.op(), ns);
-    simplify_node(inequality);
     auto new_expr = expr;
-    new_expr.op() = std::move(inequality);
+    new_expr.op() = simplify_node(std::move(inequality));
     return changed(simplify_typecast(new_expr)); // recursive call
   }
 
@@ -725,9 +723,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
             *it = simplify_typecast(new_operand); // recursive call
           }
 
-          simplify_node(result); // possibly recursive call
-
-          return std::move(result);
+          return changed(simplify_node(result)); // possibly recursive call
         }
       }
       else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl)
@@ -1977,10 +1973,9 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
           {
             exprt compo_offset = from_integer(*i, offset.type());
             plus_exprt new_offset(offset, compo_offset);
-            simplify_node(new_offset);
             exprt new_value(with.new_value());
             auto tmp = expr;
-            tmp.set_offset(std::move(new_offset));
+            tmp.set_offset(simplify_node(std::move(new_offset)));
             tmp.set_value(std::move(new_value));
             return changed(simplify_byte_update(tmp)); // recursive call
           }
@@ -1992,22 +1987,20 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
         if(i.has_value())
         {
           const exprt &index=with.where();
-          mult_exprt index_offset(index, from_integer(*i, index.type()));
-          simplify_node(index_offset);
+          exprt index_offset =
+            simplify_node(mult_exprt(index, from_integer(*i, index.type())));
 
           // index_offset may need a typecast
           if(offset.type() != index.type())
           {
             typecast_exprt tmp(index_offset, offset.type());
-            simplify_node(tmp);
-            index_offset.swap(tmp);
+            index_offset = simplify_node(std::move(tmp));
           }
 
           plus_exprt new_offset(offset, index_offset);
-          simplify_node(new_offset);
           exprt new_value(with.new_value());
           auto tmp = expr;
-          tmp.set_offset(std::move(new_offset));
+          tmp.set_offset(simplify_node(std::move(new_offset)));
           tmp.set_value(std::move(new_value));
           return changed(simplify_byte_update(tmp)); // recursive call
         }
@@ -2225,20 +2218,19 @@ bool simplify_exprt::simplify_node_preorder(exprt &expr)
   return result;
 }
 
-bool simplify_exprt::simplify_node(exprt &expr)
+simplify_exprt::resultt<> simplify_exprt::simplify_node(const exprt &node)
 {
-  if(!expr.has_operands())
-    return true; // no change
+  if(!node.has_operands())
+    return unchanged(node); // no change
 
     // #define DEBUGX
 
 #ifdef DEBUGX
-  exprt old(expr);
+  exprt old(node);
 #endif
 
-  bool no_change = true;
-
-  no_change = sort_and_join(expr) && no_change;
+  exprt expr = node;
+  bool no_change_sort_and_join = sort_and_join(expr);
 
   resultt<> r = unchanged(expr);
 
@@ -2439,26 +2431,23 @@ bool simplify_exprt::simplify_node(exprt &expr)
     r = simplify_complex(to_unary_expr(expr));
   }
 
-  if(r.has_changed())
-  {
-    expr = r.expr;
-    no_change = false;
-  }
+  if(!no_change_sort_and_join)
+    r = changed(r);
 
 #ifdef DEBUGX
   if(
-    !no_change
+    r.has_changed()
 #  ifdef DEBUG_ON_DEMAND
     && debug_on
 #  endif
   )
   {
-    std::cout << "===== " << old.id() << ": " << format(old) << '\n'
-              << " ---> " << format(expr) << '\n';
+    std::cout << "===== " << node.id() << ": " << format(node) << '\n'
+              << " ---> " << format(r.expr) << '\n';
   }
 #endif
 
-  return no_change;
+  return r;
 }
 
 simplify_exprt::resultt<> simplify_exprt::simplify_rec(const exprt &expr)
@@ -2484,30 +2473,35 @@ simplify_exprt::resultt<> simplify_exprt::simplify_rec(const exprt &expr)
 
   // We work on a copy to prevent unnecessary destruction of sharing.
   exprt tmp=expr;
-  bool result = simplify_node_preorder(tmp);
+  bool no_change = simplify_node_preorder(tmp);
 
-  if(!simplify_node(tmp))
-    result=false;
+  auto simplify_node_result = simplify_node(tmp);
+
+  if(simplify_node_result.has_changed())
+  {
+    no_change = false;
+    tmp = simplify_node_result.expr;
+  }
 
 #ifdef USE_LOCAL_REPLACE_MAP
   #if 1
   replace_mapt::const_iterator it=local_replace_map.find(tmp);
   if(it!=local_replace_map.end())
   {
     tmp=it->second;
-    result=false;
+    no_change = false;
   }
   #else
   if(!local_replace_map.empty() &&
      !replace_expr(local_replace_map, tmp))
   {
     simplify_rec(tmp);
-    result=false;
+    no_change = false;
   }
   #endif
 #endif
 
-  if(result) // no change
+  if(no_change) // no change
   {
     return unchanged(expr);
   }

src/util/simplify_expr_array.cpp

@@ -180,8 +180,7 @@ simplify_exprt::simplify_index(const index_exprt &expr)
 
       // add offset to index
       mult_exprt offset(from_integer(*sub_size, array.op1().type()), index);
-      plus_exprt final_offset(array.op1(), offset);
-      simplify_node(final_offset);
+      exprt final_offset = simplify_node(plus_exprt(array.op1(), offset));
 
       exprt result_expr(array.id(), expr.type());
       result_expr.add_to_operands(array.op0(), final_offset);

src/util/simplify_expr_boolean.cpp

@@ -41,8 +41,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_boolean(const exprt &expr)
     binary_exprt new_expr = implies_expr;
     new_expr.id(ID_or);
     new_expr.op0() = boolean_negate(new_expr.op0());
-    simplify_node(new_expr);
-    return std::move(new_expr);
+    return changed(simplify_node(new_expr));
   }
   else if(expr.id()==ID_xor)
   {
@@ -193,8 +192,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr)
 
     Forall_operands(it, tmp)
     {
-      *it = boolean_negate(*it);
-      simplify_node(*it);
+      *it = simplify_node(boolean_negate(*it));
     }
 
     tmp.id(tmp.id() == ID_and ? ID_or : ID_and);
@@ -212,16 +210,16 @@ simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr)
     auto const &op_as_exists = to_exists_expr(op);
     forall_exprt rewritten_op(
       op_as_exists.symbol(), not_exprt(op_as_exists.where()));
-    simplify_node(rewritten_op.where());
+    rewritten_op.where() = simplify_node(rewritten_op.where());
     return std::move(rewritten_op);
   }
   else if(op.id() == ID_forall) // !(forall: a) <-> exists: not a
   {
     auto const &op_as_forall = to_forall_expr(op);
     exists_exprt rewritten_op(
       op_as_forall.symbol(), not_exprt(op_as_forall.where()));
-    simplify_node(rewritten_op.where());
-    return std::move(rewritten_op);
+    rewritten_op.where() = simplify_node(rewritten_op.where());
+    return changed(rewritten_op);
   }
 
   return unchanged(expr);

src/util/simplify_expr_class.h

@@ -210,7 +210,7 @@ class simplify_exprt
   NODISCARD resultt<> simplify_inequality_pointer_object(const exprt &);
 
   // main recursion
-  bool simplify_node(exprt &expr);
+  NODISCARD resultt<> simplify_node(const exprt &);
   bool simplify_node_preorder(exprt &expr);
   NODISCARD resultt<> simplify_rec(const exprt &);
 

src/util/simplify_expr_if.cpp

@@ -350,41 +350,29 @@ simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr)
       else if(truevalue.is_false() && falsevalue.is_true())
       {
         // a?0:1 <-> !a
-        exprt tmp = boolean_negate(cond);
-        simplify_node(tmp);
-        return std::move(tmp);
+        return changed(simplify_node(boolean_negate(cond)));
       }
       else if(falsevalue.is_false())
       {
         // a?b:0 <-> a AND b
-        and_exprt tmp(cond, truevalue);
-        simplify_node(tmp);
-        return std::move(tmp);
+        return changed(simplify_node(and_exprt(cond, truevalue)));
       }
       else if(falsevalue.is_true())
       {
         // a?b:1 <-> !a OR b
-        exprt tmp_not_cond = boolean_negate(cond);
-        simplify_node(tmp_not_cond);
-        or_exprt tmp(tmp_not_cond, truevalue);
-        simplify_node(tmp);
-        return std::move(tmp);
+        return changed(simplify_node(
+          or_exprt(simplify_node(boolean_negate(cond)), truevalue)));
       }
       else if(truevalue.is_true())
       {
         // a?1:b <-> a||(!a && b) <-> a OR b
-        or_exprt tmp(cond, falsevalue);
-        simplify_node(tmp);
-        return std::move(tmp);
+        return changed(simplify_node(or_exprt(cond, falsevalue)));
       }
       else if(truevalue.is_false())
       {
         // a?0:b <-> !a && b
-        exprt tmp_not_cond = boolean_negate(cond);
-        simplify_node(tmp_not_cond);
-        and_exprt tmp(tmp_not_cond, falsevalue);
-        simplify_node(tmp);
-        return std::move(tmp);
+        return changed(simplify_node(
+          and_exprt(simplify_node(boolean_negate(cond)), falsevalue)));
       }
     }
   }

src/util/simplify_expr_int.cpp

@@ -568,9 +568,7 @@ simplify_exprt::simplify_minus(const minus_exprt &expr)
     // rewrite "a-b" to "a+(-b)"
     unary_minus_exprt rhs_negated(operands[1]);
     plus_exprt plus_expr(operands[0], simplify_unary_minus(rhs_negated));
-    simplify_node(plus_expr);
-
-    return std::move(plus_expr);
+    return changed(simplify_node(plus_expr));
   }
   else if(
     minus_expr.type().id() == ID_pointer &&
@@ -649,12 +647,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_bitwise(const exprt &expr)
       }
 
       new_expr.type()=bool_typet();
-      simplify_node(new_expr);
+      new_expr = simplify_node(new_expr);
 
       new_expr = typecast_exprt(new_expr, expr.type());
-      simplify_node(new_expr);
-
-      return std::move(new_expr);
+      return changed(simplify_node(new_expr));
     }
   }
 
@@ -1486,8 +1482,7 @@ simplify_exprt::simplify_inequality_no_constant(const exprt &expr)
     new_expr.id(ID_equal);
     new_expr = simplify_inequality_no_constant(new_expr);
     new_expr = boolean_negate(new_expr);
-    simplify_node(new_expr);
-    return std::move(new_expr);
+    return changed(simplify_node(new_expr));
   }
   else if(expr.id()==ID_gt)
   {
@@ -1497,17 +1492,15 @@ simplify_exprt::simplify_inequality_no_constant(const exprt &expr)
     new_expr.op0().swap(new_expr.op1());
     new_expr = simplify_inequality_no_constant(new_expr);
     new_expr = boolean_negate(new_expr);
-    simplify_node(new_expr);
-    return std::move(new_expr);
+    return changed(simplify_node(new_expr));
   }
   else if(expr.id()==ID_lt)
   {
     auto new_expr = expr;
     new_expr.id(ID_ge);
     new_expr = simplify_inequality_no_constant(new_expr);
     new_expr = boolean_negate(new_expr);
-    simplify_node(new_expr);
-    return std::move(new_expr);
+    return changed(simplify_node(new_expr));
   }
   else if(expr.id()==ID_le)
   {
@@ -1588,10 +1581,9 @@ simplify_exprt::simplify_inequality_no_constant(const exprt &expr)
     if(!eliminate_common_addends(new_expr.op0(), new_expr.op1()))
     {
       // remove zeros
-      simplify_node(new_expr.op0());
-      simplify_node(new_expr.op1());
-      new_expr = simplify_inequality(new_expr); // recursive call
-      return std::move(new_expr);
+      new_expr.op0() = simplify_node(new_expr.op0());
+      new_expr.op1() = simplify_node(new_expr.op1());
+      return changed(simplify_inequality(new_expr)); // recursive call
     }
   }
 
@@ -1625,8 +1617,7 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
       new_expr.id(ID_equal);
       new_expr = simplify_inequality_rhs_is_constant(new_expr);
       new_expr = boolean_negate(new_expr);
-      simplify_node(new_expr);
-      return std::move(new_expr);
+      return changed(simplify_node(new_expr));
     }
 
     // very special case for pointers
@@ -1839,8 +1830,7 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
       new_expr.id(ID_equal);
       new_expr = simplify_inequality_rhs_is_constant(new_expr);
       new_expr = boolean_negate(new_expr);
-      simplify_node(new_expr);
-      return std::move(new_expr);
+      return changed(simplify_node(new_expr));
     }
     else if(expr.id()==ID_gt)
     {
@@ -1863,8 +1853,7 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
       new_expr.id(ID_ge);
       new_expr = simplify_inequality_rhs_is_constant(new_expr);
       new_expr = boolean_negate(new_expr);
-      simplify_node(new_expr);
-      return std::move(new_expr);
+      return changed(simplify_node(new_expr));
     }
     else if(expr.id()==ID_le)
     {
@@ -1881,8 +1870,7 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
       new_expr.op1() = from_integer(i, new_expr.op1().type());
       new_expr = simplify_inequality_rhs_is_constant(new_expr);
       new_expr = boolean_negate(new_expr);
-      simplify_node(new_expr);
-      return std::move(new_expr);
+      return changed(simplify_node(new_expr));
     }
   }
 #endif