Merge pull request #5764 from tautschnig/simplify-recursive-cleanup

Refine recursive calls within the simplifier

Author: tautschnig

src/util/simplify_expr.cpp

@@ -795,7 +795,8 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
     auto one = from_integer(1, expr_type);
     auto zero = from_integer(0, expr_type);
     exprt new_expr = if_exprt(expr.op(), std::move(one), std::move(zero));
-    return changed(simplify_rec(new_expr)); // recursive call
+    simplify_if_preorder(to_if_expr(new_expr));
+    return new_expr;
   }
 
   // circular casts through types shorter than `int`
@@ -884,16 +885,17 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
       if(sub_size.has_value())
       {
         auto new_expr = expr;
+        exprt offset_expr =
+          simplify_typecast(typecast_exprt(op_plus_expr.op1(), size_type()));
 
         // void*
         if(*sub_size == 0 || *sub_size == 1)
-          new_expr.op() = typecast_exprt(op_plus_expr.op1(), size_type());
+          new_expr.op() = offset_expr;
         else
-          new_expr.op() = mult_exprt(
-            from_integer(*sub_size, size_type()),
-            typecast_exprt(op_plus_expr.op1(), size_type()));
-
-        new_expr.op() = simplify_rec(new_expr.op()); // rec. call
+        {
+          new_expr.op() = simplify_mult(
+            mult_exprt(from_integer(*sub_size, size_type()), offset_expr));
+        }
 
         return changed(simplify_typecast(new_expr)); // rec. call
       }
@@ -965,19 +967,18 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
 
       for(auto &op : new_expr.op().operands())
       {
-        if(op.type().id()==ID_pointer)
+        exprt new_op = simplify_typecast(typecast_exprt(op, size_t_type));
+        if(op.type().id() != ID_pointer && *step > 1)
         {
-          op = typecast_exprt(op, size_t_type);
-        }
-        else
-        {
-          op = typecast_exprt(op, size_t_type);
-          if(*step > 1)
-            op = mult_exprt(from_integer(*step, size_t_type), op);
+          new_op =
+            simplify_mult(mult_exprt(from_integer(*step, size_t_type), new_op));
         }
+        op = std::move(new_op);
       }
 
-      return changed(simplify_rec(new_expr)); // recursive call
+      new_expr.op() = simplify_plus(to_plus_expr(new_expr.op()));
+
+      return changed(simplify_typecast(new_expr)); // recursive call
     }
   }
 
@@ -1316,7 +1317,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
       auto result =
         address_of_exprt(index_exprt(o, from_integer(0, size_type())));
 
-      return changed(simplify_rec(result)); // recursive call
+      return changed(simplify_address_of(result)); // recursive call
     }
   }
 
@@ -1723,9 +1724,9 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
       pointer_offset_bits(to_array_of_expr(expr.op()).what().type(), ns))
   {
     auto tmp = expr;
-    tmp.op() = index_exprt(expr.op(), expr.offset());
+    tmp.op() = simplify_index(index_exprt(expr.op(), expr.offset()));
     tmp.offset() = from_integer(0, expr.offset().type());
-    return changed(simplify_rec(tmp));
+    return changed(simplify_byte_extract(tmp));
   }
 
   // extract bits of a constant
@@ -1970,19 +1971,19 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
         {
           const exprt &index=with.where();
           exprt index_offset =
-            simplify_node(mult_exprt(index, from_integer(*i, index.type())));
+            simplify_mult(mult_exprt(index, from_integer(*i, index.type())));
 
           // index_offset may need a typecast
           if(offset.type() != index.type())
           {
             index_offset =
-              simplify_node(typecast_exprt(index_offset, offset.type()));
+              simplify_typecast(typecast_exprt(index_offset, offset.type()));
           }
 
           plus_exprt new_offset(offset, index_offset);
           exprt new_value(with.new_value());
           auto tmp = expr;
-          tmp.set_offset(simplify_node(std::move(new_offset)));
+          tmp.set_offset(simplify_plus(std::move(new_offset)));
           tmp.set_value(std::move(new_value));
           return changed(simplify_byte_update(tmp)); // recursive call
         }

src/util/simplify_expr_array.cpp

@@ -183,15 +183,16 @@ simplify_exprt::simplify_index(const index_exprt &expr)
         return unchanged(expr);
 
       // add offset to index
-      mult_exprt offset(
-        from_integer(*sub_size, byte_extract_expr.offset().type()), index);
+      exprt offset = simplify_mult(mult_exprt{
+        from_integer(*sub_size, byte_extract_expr.offset().type()), index});
       exprt final_offset =
-        simplify_node(plus_exprt(byte_extract_expr.offset(), offset));
+        simplify_plus(plus_exprt(byte_extract_expr.offset(), offset));
 
-      exprt result_expr(array.id(), expr.type());
-      result_expr.add_to_operands(byte_extract_expr.op(), final_offset);
+      auto result_expr = byte_extract_expr;
+      result_expr.type() = expr.type();
+      result_expr.offset() = final_offset;
 
-      return changed(simplify_rec(result_expr));
+      return changed(simplify_byte_extract(result_expr));
     }
   }
   else if(array.id()==ID_if)

src/util/simplify_expr_boolean.cpp

@@ -38,7 +38,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() = simplify_not(not_exprt(new_expr.op0()));
-    return changed(simplify_node(new_expr));
+    return changed(simplify_boolean(new_expr));
   }
   else if(expr.id()==ID_xor)
   {
@@ -204,18 +204,14 @@ simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr)
   else if(op.id()==ID_exists) // !(exists: a) <-> forall: not a
   {
     auto const &op_as_exists = to_exists_expr(op);
-    forall_exprt rewritten_op(
-      op_as_exists.symbol(), not_exprt(op_as_exists.where()));
-    rewritten_op.where() = simplify_node(rewritten_op.where());
-    return std::move(rewritten_op);
+    return forall_exprt{op_as_exists.symbol(),
+                        simplify_not(not_exprt(op_as_exists.where()))};
   }
   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()));
-    rewritten_op.where() = simplify_node(rewritten_op.where());
-    return std::move(rewritten_op);
+    return exists_exprt{op_as_forall.symbol(),
+                        simplify_not(not_exprt(op_as_forall.where()))};
   }
 
   return unchanged(expr);

src/util/simplify_expr_if.cpp

@@ -357,24 +357,24 @@ simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr)
       else if(falsevalue.is_false())
       {
         // a?b:0 <-> a AND b
-        return changed(simplify_node(and_exprt(cond, truevalue)));
+        return changed(simplify_boolean(and_exprt(cond, truevalue)));
       }
       else if(falsevalue.is_true())
       {
         // a?b:1 <-> !a OR b
         return changed(
-          simplify_node(or_exprt(simplify_not(not_exprt(cond)), truevalue)));
+          simplify_boolean(or_exprt(simplify_not(not_exprt(cond)), truevalue)));
       }
       else if(truevalue.is_true())
       {
         // a?1:b <-> a||(!a && b) <-> a OR b
-        return changed(simplify_node(or_exprt(cond, falsevalue)));
+        return changed(simplify_boolean(or_exprt(cond, falsevalue)));
       }
       else if(truevalue.is_false())
       {
         // a?0:b <-> !a && b
-        return changed(
-          simplify_node(and_exprt(simplify_not(not_exprt(cond)), falsevalue)));
+        return changed(simplify_boolean(
+          and_exprt(simplify_not(not_exprt(cond)), falsevalue)));
       }
     }
   }

src/util/simplify_expr_int.cpp

@@ -570,7 +570,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));
-    return changed(simplify_node(plus_expr));
+    return changed(simplify_plus(plus_expr));
   }
   else if(
     minus_expr.type().id() == ID_pointer &&
@@ -646,10 +646,9 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr)
       }
 
       new_expr.type()=bool_typet();
-      new_expr = simplify_node(new_expr);
+      new_expr = simplify_boolean(new_expr);
 
-      new_expr = typecast_exprt(new_expr, expr.type());
-      return changed(simplify_node(new_expr));
+      return changed(simplify_typecast(typecast_exprt(new_expr, expr.type())));
     }
   }
 

src/util/simplify_expr_pointer.cpp

@@ -281,7 +281,7 @@ simplify_exprt::simplify_pointer_offset(const unary_exprt &expr)
       auto new_expr = expr;
       new_expr.op() = op;
 
-      return changed(simplify_node(new_expr)); // recursive call
+      return changed(simplify_pointer_offset(new_expr)); // recursive call
     }
     else if(op_type.id()==ID_signedbv ||
             op_type.id()==ID_unsignedbv)
@@ -291,8 +291,7 @@ simplify_exprt::simplify_pointer_offset(const unary_exprt &expr)
       if(op.is_constant())
       {
         // (T *)0x1234 -> 0x1234
-        exprt tmp = typecast_exprt(op, expr.type());
-        return changed(simplify_node(tmp));
+        return changed(simplify_typecast(typecast_exprt{op, expr.type()}));
       }
       else
       {
@@ -340,7 +339,7 @@ simplify_exprt::simplify_pointer_offset(const unary_exprt &expr)
       {
         exprt tmp=op;
         if(tmp.type()!=expr.type())
-          tmp = simplify_node(typecast_exprt(tmp, expr.type()));
+          tmp = simplify_typecast(typecast_exprt(tmp, expr.type()));
 
         int_expr.push_back(tmp);
       }
@@ -359,29 +358,23 @@ simplify_exprt::simplify_pointer_offset(const unary_exprt &expr)
       return unchanged(expr);
 
     // this might change the type of the pointer!
-    exprt pointer_offset_expr = simplify_node(pointer_offset(ptr_expr.front()));
+    exprt pointer_offset_expr =
+      simplify_pointer_offset(to_unary_expr(pointer_offset(ptr_expr.front())));
 
     exprt sum;
 
     if(int_expr.size()==1)
       sum=int_expr.front();
     else
-    {
-      sum=exprt(ID_plus, expr.type());
-      sum.operands()=int_expr;
-    }
-
-    sum = simplify_node(sum);
+      sum = simplify_plus(plus_exprt{int_expr, expr.type()});
 
     exprt size_expr = from_integer(*element_size, expr.type());
 
-    exprt product = mult_exprt(sum, size_expr);
-
-    product = simplify_node(product);
+    exprt product = simplify_mult(mult_exprt{sum, size_expr});
 
     auto new_expr = plus_exprt(pointer_offset_expr, product);
 
-    return changed(simplify_node(new_expr));
+    return changed(simplify_plus(new_expr));
   }
   else if(ptr.id()==ID_constant)
   {
@@ -390,8 +383,7 @@ simplify_exprt::simplify_pointer_offset(const unary_exprt &expr)
     if(c_ptr.get_value()==ID_NULL ||
        c_ptr.value_is_zero_string())
     {
-      auto new_expr = from_integer(0, expr.type());
-      return changed(simplify_node(new_expr));
+      return from_integer(0, expr.type());
     }
     else
     {
@@ -408,9 +400,7 @@ simplify_exprt::simplify_pointer_offset(const unary_exprt &expr)
         *pointer_offset_bits(ptr.type(), ns) - config.bv_encoding.object_bits;
       number%=power(2, offset_bits);
 
-      auto new_expr = from_integer(number, expr.type());
-
-      return changed(simplify_node(new_expr));
+      return from_integer(number, expr.type());
     }
   }
 
@@ -679,10 +669,7 @@ simplify_exprt::simplify_object_size(const unary_exprt &expr)
         exprt size = size_opt.value();
 
         if(size.type() != expr_type)
-        {
-          size = typecast_exprt(size, expr_type);
-          size = simplify_node(size);
-        }
+          size = simplify_typecast(typecast_exprt(size, expr_type));
 
         return size;
       }
@@ -708,5 +695,5 @@ simplify_exprt::simplify_good_pointer(const unary_exprt &expr)
   exprt def = good_pointer_def(expr.op(), ns);
 
   // recursive call
-  return changed(simplify_node(def));
+  return changed(simplify_rec(def));
 }

src/util/simplify_expr_struct.cpp

@@ -47,11 +47,8 @@ simplify_exprt::simplify_member(const member_exprt &expr)
           DATA_INVARIANT(
             op2.type() == expr.type(),
             "member expression type must match component type");
-          exprt tmp;
-          tmp.swap(op2);
 
-          // do this recursively
-          return changed(simplify_rec(tmp));
+          return op2;
         }
         else // something else, get rid of it
           new_operands.resize(new_operands.size() - 2);
@@ -71,10 +68,7 @@ simplify_exprt::simplify_member(const member_exprt &expr)
       if(with_expr.where().get(ID_component_name)==component_name)
       {
         // WITH(s, .m, v).m -> v
-        auto tmp = with_expr.new_value();
-
-        // do this recursively
-        return changed(simplify_rec(tmp));
+        return with_expr.new_value();
       }
     }
   }
@@ -93,10 +87,7 @@ simplify_exprt::simplify_member(const member_exprt &expr)
         if(designator.front().get(ID_component_name)==component_name)
         {
           // UPDATE(s, .m, v).m -> v
-          exprt tmp=update_expr.new_value();
-
-          // do this recursively
-          return changed(simplify_rec(tmp));
+          return update_expr.new_value();
         }
         // the following optimization only works on structs,
         // and not on unions
@@ -107,7 +98,7 @@ simplify_exprt::simplify_member(const member_exprt &expr)
           new_expr.struct_op() = update_expr.old();
 
           // do this recursively
-          return changed(simplify_rec(new_expr));
+          return changed(simplify_member(new_expr));
         }
       }
     }
@@ -158,12 +149,12 @@ simplify_exprt::simplify_member(const member_exprt &expr)
       const exprt &struct_offset = byte_extract_expr.offset();
       exprt member_offset = from_integer(*offset_int, struct_offset.type());
       exprt final_offset =
-        simplify_node(plus_exprt(struct_offset, member_offset));
+        simplify_plus(plus_exprt(struct_offset, member_offset));
 
       byte_extract_exprt result(
         op.id(), byte_extract_expr.op(), final_offset, expr.type());
 
-      return changed(simplify_rec(result)); // recursive call
+      return changed(simplify_byte_extract(result)); // recursive call
     }
     else if(op_type.id() == ID_union)
     {