Simplify selected ID_if operands in preorder traversal

This avoids repeatedly visiting already-simplified operands. On the
example from #7357 this reduces symex time from 1172 seconds to 922
seconds.

Author: tautschnig

src/util/simplify_expr.cpp

@@ -1376,23 +1376,6 @@ simplify_exprt::simplify_dereference(const dereference_exprt &expr)
   if(pointer.type().id()!=ID_pointer)
     return unchanged(expr);
 
-  if(pointer.id()==ID_if && pointer.operands().size()==3)
-  {
-    const if_exprt &if_expr=to_if_expr(pointer);
-
-    auto tmp_op1 = expr;
-    tmp_op1.op() = if_expr.true_case();
-    exprt tmp_op1_result = simplify_dereference(tmp_op1);
-
-    auto tmp_op2 = expr;
-    tmp_op2.op() = if_expr.false_case();
-    exprt tmp_op2_result = simplify_dereference(tmp_op2);
-
-    if_exprt tmp{if_expr.cond(), tmp_op1_result, tmp_op2_result};
-
-    return changed(simplify_if(tmp));
-  }
-
   if(pointer.id()==ID_address_of)
   {
     exprt tmp=to_address_of_expr(pointer).object();
@@ -1426,6 +1409,30 @@ simplify_exprt::simplify_dereference(const dereference_exprt &expr)
   return unchanged(expr);
 }
 
+simplify_exprt::resultt<>
+simplify_exprt::simplify_dereference_preorder(const dereference_exprt &expr)
+{
+  const exprt &pointer = expr.pointer();
+
+  if(pointer.id() == ID_if)
+  {
+    if_exprt if_expr = lift_if(expr, 0);
+    return changed(simplify_if_preorder(if_expr));
+  }
+  else
+  {
+    auto r_it = simplify_rec(pointer); // recursive call
+    if(r_it.has_changed())
+    {
+      auto tmp = expr;
+      tmp.pointer() = r_it.expr;
+      return tmp;
+    }
+  }
+
+  return unchanged(expr);
+}
+
 simplify_exprt::resultt<>
 simplify_exprt::simplify_lambda(const lambda_exprt &expr)
 {
@@ -1642,17 +1649,6 @@ simplify_exprt::resultt<> simplify_exprt::simplify_object(const exprt &expr)
 simplify_exprt::resultt<>
 simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
 {
-  // lift up any ID_if on the object
-  if(expr.op().id()==ID_if)
-  {
-    if_exprt if_expr=lift_if(expr, 0);
-    if_expr.true_case() =
-      simplify_byte_extract(to_byte_extract_expr(if_expr.true_case()));
-    if_expr.false_case() =
-      simplify_byte_extract(to_byte_extract_expr(if_expr.false_case()));
-    return changed(simplify_if(if_expr));
-  }
-
   const auto el_size = pointer_offset_bits(expr.type(), ns);
   if(el_size.has_value() && *el_size < 0)
     return unchanged(expr);
@@ -1995,6 +1991,41 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   return unchanged(expr);
 }
 
+simplify_exprt::resultt<>
+simplify_exprt::simplify_byte_extract_preorder(const byte_extract_exprt &expr)
+{
+  // lift up any ID_if on the object
+  if(expr.op().id() == ID_if)
+  {
+    if_exprt if_expr = lift_if(expr, 0);
+    return changed(simplify_if_preorder(if_expr));
+  }
+  else
+  {
+    optionalt<exprt::operandst> new_operands;
+
+    for(std::size_t i = 0; i < expr.operands().size(); ++i)
+    {
+      auto r_it = simplify_rec(expr.operands()[i]); // recursive call
+      if(r_it.has_changed())
+      {
+        if(!new_operands.has_value())
+          new_operands = expr.operands();
+        (*new_operands)[i] = std::move(r_it.expr);
+      }
+    }
+
+    if(new_operands.has_value())
+    {
+      exprt result = expr;
+      std::swap(result.operands(), *new_operands);
+      return result;
+    }
+  }
+
+  return unchanged(expr);
+}
+
 simplify_exprt::resultt<>
 simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
 {
@@ -2724,6 +2755,31 @@ simplify_exprt::simplify_node_preorder(const exprt &expr)
   {
     result = simplify_typecast_preorder(to_typecast_expr(expr));
   }
+  else if(
+    expr.id() == ID_byte_extract_little_endian ||
+    expr.id() == ID_byte_extract_big_endian)
+  {
+    result = simplify_byte_extract_preorder(to_byte_extract_expr(expr));
+  }
+  else if(expr.id() == ID_dereference)
+  {
+    result = simplify_dereference_preorder(to_dereference_expr(expr));
+  }
+  else if(expr.id() == ID_index)
+  {
+    result = simplify_index_preorder(to_index_expr(expr));
+  }
+  else if(expr.id() == ID_member)
+  {
+    result = simplify_member_preorder(to_member_expr(expr));
+  }
+  else if(
+    expr.id() == ID_is_dynamic_object || expr.id() == ID_is_invalid_pointer ||
+    expr.id() == ID_object_size || expr.id() == ID_pointer_object ||
+    expr.id() == ID_pointer_offset)
+  {
+    result = simplify_unary_pointer_predicate_preorder(to_unary_expr(expr));
+  }
   else if(expr.has_operands())
   {
     optionalt<exprt::operandst> new_operands;

src/util/simplify_expr_array.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "arith_tools.h"
 #include "byte_operators.h"
+#include "expr_util.h"
 #include "pointer_offset_size.h"
 #include "replace_expr.h"
 #include "std_expr.h"
@@ -196,22 +197,44 @@ simplify_exprt::simplify_index(const index_exprt &expr)
       return changed(simplify_byte_extract(result_expr));
     }
   }
-  else if(array.id()==ID_if)
-  {
-    const if_exprt &if_expr=to_if_expr(array);
-    exprt cond=if_expr.cond();
-
-    index_exprt idx_false=to_index_expr(expr);
-    idx_false.array()=if_expr.false_case();
-
-    new_expr.array() = if_expr.true_case();
-
-    exprt result = if_exprt(cond, new_expr, idx_false, expr.type());
-    return changed(simplify_rec(result));
-  }
 
   if(no_change)
     return unchanged(expr);
   else
     return std::move(new_expr);
 }
+
+simplify_exprt::resultt<>
+simplify_exprt::simplify_index_preorder(const index_exprt &expr)
+{
+  // lift up any ID_if on the array
+  if(expr.array().id() == ID_if)
+  {
+    if_exprt if_expr = lift_if(expr, 0);
+    return changed(simplify_if_preorder(if_expr));
+  }
+  else
+  {
+    optionalt<exprt::operandst> new_operands;
+
+    for(std::size_t i = 0; i < expr.operands().size(); ++i)
+    {
+      auto r_it = simplify_rec(expr.operands()[i]); // recursive call
+      if(r_it.has_changed())
+      {
+        if(!new_operands.has_value())
+          new_operands = expr.operands();
+        (*new_operands)[i] = std::move(r_it.expr);
+      }
+    }
+
+    if(new_operands.has_value())
+    {
+      exprt result = expr;
+      std::swap(result.operands(), *new_operands);
+      return result;
+    }
+  }
+
+  return unchanged(expr);
+}

src/util/simplify_expr_class.h

@@ -175,17 +175,24 @@ class simplify_exprt
   NODISCARD resultt<> simplify_with(const with_exprt &);
   NODISCARD resultt<> simplify_update(const update_exprt &);
   NODISCARD resultt<> simplify_index(const index_exprt &);
+  NODISCARD resultt<> simplify_index_preorder(const index_exprt &);
   NODISCARD resultt<> simplify_member(const member_exprt &);
+  NODISCARD resultt<> simplify_member_preorder(const member_exprt &);
   NODISCARD resultt<> simplify_byte_update(const byte_update_exprt &);
   NODISCARD resultt<> simplify_byte_extract(const byte_extract_exprt &);
+  NODISCARD resultt<>
+  simplify_byte_extract_preorder(const byte_extract_exprt &);
   NODISCARD resultt<> simplify_pointer_object(const pointer_object_exprt &);
+  NODISCARD resultt<>
+  simplify_unary_pointer_predicate_preorder(const unary_exprt &);
   NODISCARD resultt<> simplify_object_size(const object_size_exprt &);
   NODISCARD resultt<> simplify_is_dynamic_object(const unary_exprt &);
   NODISCARD resultt<> simplify_is_invalid_pointer(const unary_exprt &);
   NODISCARD resultt<> simplify_object(const exprt &);
   NODISCARD resultt<> simplify_unary_minus(const unary_minus_exprt &);
   NODISCARD resultt<> simplify_unary_plus(const unary_plus_exprt &);
   NODISCARD resultt<> simplify_dereference(const dereference_exprt &);
+  NODISCARD resultt<> simplify_dereference_preorder(const dereference_exprt &);
   NODISCARD resultt<> simplify_address_of(const address_of_exprt &);
   NODISCARD resultt<> simplify_pointer_offset(const pointer_offset_exprt &);
   NODISCARD resultt<> simplify_bswap(const bswap_exprt &);

src/util/simplify_expr_pointer.cpp

@@ -53,6 +53,32 @@ static bool is_dereference_integer_object(
   return false;
 }
 
+simplify_exprt::resultt<>
+simplify_exprt::simplify_unary_pointer_predicate_preorder(
+  const unary_exprt &expr)
+{
+  const exprt &pointer = expr.op();
+  PRECONDITION(pointer.type().id() == ID_pointer);
+
+  if(pointer.id() == ID_if)
+  {
+    if_exprt if_expr = lift_if(expr, 0);
+    return changed(simplify_if_preorder(if_expr));
+  }
+  else
+  {
+    auto r_it = simplify_rec(pointer); // recursive call
+    if(r_it.has_changed())
+    {
+      auto tmp = expr;
+      tmp.op() = r_it.expr;
+      return tmp;
+    }
+  }
+
+  return unchanged(expr);
+}
+
 simplify_exprt::resultt<>
 simplify_exprt::simplify_address_of_arg(const exprt &expr)
 {
@@ -249,16 +275,6 @@ simplify_exprt::simplify_pointer_offset(const pointer_offset_exprt &expr)
 {
   const exprt &ptr = expr.pointer();
 
-  if(ptr.id()==ID_if && ptr.operands().size()==3)
-  {
-    if_exprt if_expr=lift_if(expr, 0);
-    if_expr.true_case() =
-      simplify_pointer_offset(to_pointer_offset_expr(if_expr.true_case()));
-    if_expr.false_case() =
-      simplify_pointer_offset(to_pointer_offset_expr(if_expr.false_case()));
-    return changed(simplify_if(if_expr));
-  }
-
   if(ptr.type().id()!=ID_pointer)
     return unchanged(expr);
 
@@ -559,16 +575,6 @@ simplify_exprt::simplify_is_dynamic_object(const unary_exprt &expr)
   auto new_expr = expr;
   exprt &op = new_expr.op();
 
-  if(op.id()==ID_if && op.operands().size()==3)
-  {
-    if_exprt if_expr=lift_if(expr, 0);
-    if_expr.true_case() =
-      simplify_is_dynamic_object(to_unary_expr(if_expr.true_case()));
-    if_expr.false_case() =
-      simplify_is_dynamic_object(to_unary_expr(if_expr.false_case()));
-    return changed(simplify_if(if_expr));
-  }
-
   bool no_change = true;
 
   auto op_result = simplify_object(op);

src/util/simplify_expr_struct.cpp

@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include "byte_operators.h"
 #include "c_types.h"
 #include "config.h"
+#include "expr_util.h"
 #include "invariant.h"
 #include "namespace.h"
 #include "pointer_offset_size.h"
@@ -240,20 +241,6 @@ simplify_exprt::simplify_member(const member_exprt &expr)
       }
     }
   }
-  else if(op.id()==ID_if)
-  {
-    const if_exprt &if_expr=to_if_expr(op);
-    exprt cond=if_expr.cond();
-
-    member_exprt member_false=to_member_expr(expr);
-    member_false.compound()=if_expr.false_case();
-
-    member_exprt member_true = to_member_expr(expr);
-    member_true.compound() = if_expr.true_case();
-
-    auto tmp = if_exprt(cond, member_true, member_false, expr.type());
-    return changed(simplify_rec(tmp));
-  }
   else if(op.id() == ID_let)
   {
     // Push a member operator inside a let binding, to avoid the let bisecting
@@ -271,3 +258,27 @@ simplify_exprt::simplify_member(const member_exprt &expr)
 
   return unchanged(expr);
 }
+
+simplify_exprt::resultt<>
+simplify_exprt::simplify_member_preorder(const member_exprt &expr)
+{
+  const exprt &compound = expr.compound();
+
+  if(compound.id() == ID_if)
+  {
+    if_exprt if_expr = lift_if(expr, 0);
+    return changed(simplify_if_preorder(if_expr));
+  }
+  else
+  {
+    auto r_it = simplify_rec(compound); // recursive call
+    if(r_it.has_changed())
+    {
+      auto tmp = expr;
+      tmp.compound() = r_it.expr;
+      return tmp;
+    }
+  }
+
+  return unchanged(expr);
+}