Conditionally simplify use of if-then-else conditions

When symbolically executing (and dereferencing) statements like
`*p = *p + 1;` where `p` may point to more than a single object we ended
up with nested if-then-else expressions on the right-hand side that
would use the very same conditions. In this particular case, we should
propagate the conditions into nested if-then-else expressions. This
simplification may be expensive, so we don't enable it in general.

Author: tautschnig

regression/cbmc/Pointer31/main.c

@@ -1,18 +1,16 @@
-int nondet_int();
+struct S
+{
+  int len;
+};
 
-int *p;
-int global;
+__CPROVER_bool nondet_bool();
 
 int main()
 {
-  p = &global;
-
-  for(int i = 0; i < 10; i++)
-  {
-    *p = 1;
-
-    // this is not allowed!
-    int local;
-    p = &local;
-  }
+  struct S *s_p = 0;
+  struct S s;
+  if(nondet_bool())
+    s_p = &s;
+  s_p->len = s_p->len + 1;
+  __CPROVER_assert(0, "");
 }

regression/cbmc/Pointer31/test.desc

@@ -1,8 +1,12 @@
-CORE
+CORE paths-lifo-expected-failure
 main.c
---pointer-check
+--show-vcc
+main::1::s!0@1#2..len = .+ \? .+ : .+
 ^SIGNAL=0$
-^EXIT=10$
-^VERIFICATION FAILED$
+^EXIT=0$
 --
-^warning: ignoring
+main::1::s!0@1#2..len = .+ \? .+ \?
+--
+We should not find nested if-then-else expressions in the right-hand side
+evaluating `len` when simplification works as intended. (With --paths lifo we do
+not have any branching, so it is marked paths-lifo-expected-failure.)

src/goto-symex/symex_assign.cpp

@@ -10,6 +10,7 @@ Author: Daniel Kroening, [email protected]
 /// Symbolic Execution
 
 #include "symex_assign.h"
+#include <util/simplify_expr_class.h>
 
 #include <util/byte_operators.h>
 #include <util/expr_util.h>
@@ -203,7 +204,10 @@ void symex_assignt::assign_non_struct_symbol(
   assignmentt assignment{lhs, full_lhs, l2_rhs};
 
   if(symex_config.simplify_opt)
-    assignment.rhs = simplify_expr(std::move(assignment.rhs), ns);
+  {
+    simplify_exprt simp{ns, true};
+    simp.simplify(assignment.rhs);
+  }
 
   const ssa_exprt l2_lhs = state
                              .assignment(

src/util/simplify_expr.cpp

@@ -3151,22 +3151,21 @@ simplify_exprt::resultt<> simplify_exprt::simplify_rec(const exprt &expr)
       simplify_node_preorder_result.expr_changed;
   }
 
-#ifdef USE_LOCAL_REPLACE_MAP
-  exprt tmp = simplify_node_result.expr;
-#  if 1
-  replace_mapt::const_iterator it =
-    local_replace_map.find(simplify_node_result.expr);
-  if(it!=local_replace_map.end())
-    simplify_node_result = changed(it->second);
+  if(!local_replace_map.empty())
+  {
+#if 1
+    replace_mapt::const_iterator it =
+      local_replace_map.find(simplify_node_result.expr);
+    if(it != local_replace_map.end())
+      simplify_node_result = changed(it->second);
 #  else
   if(
-    !local_replace_map.empty() &&
     !replace_expr(local_replace_map, simplify_node_result.expr))
   {
     simplify_node_result = changed(simplify_rec(simplify_node_result.expr));
   }
-#  endif
 #endif
+  }
 
   if(!simplify_node_result.has_changed())
   {

src/util/simplify_expr_class.h

@@ -21,10 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include "mp_arith.h"
 #include "nodiscard.h"
 #include "type.h"
-// #define USE_LOCAL_REPLACE_MAP
-#ifdef USE_LOCAL_REPLACE_MAP
 #include "replace_expr.h"
-#endif
 
 class abs_exprt;
 class address_of_exprt;
@@ -81,11 +78,12 @@ class with_exprt;
 class simplify_exprt
 {
 public:
-  explicit simplify_exprt(const namespacet &_ns):
-    do_simplify_if(true),
-    ns(_ns)
+  simplify_exprt(const namespacet &_ns, bool propagate_if_cond)
+    : do_simplify_if(propagate_if_cond),
+      ns(_ns)
 #ifdef DEBUG_ON_DEMAND
-    , debug_on(false)
+      ,
+      debug_on(false)
 #endif
   {
 #ifdef DEBUG_ON_DEMAND
@@ -94,6 +92,10 @@ class simplify_exprt
 #endif
   }
 
+  explicit simplify_exprt(const namespacet &_ns) : simplify_exprt(_ns, false)
+  {
+  }
+
   virtual ~simplify_exprt()
   {
   }
@@ -284,10 +286,7 @@ class simplify_exprt
 #ifdef DEBUG_ON_DEMAND
   bool debug_on;
 #endif
-#ifdef USE_LOCAL_REPLACE_MAP
   replace_mapt local_replace_map;
-#endif
-
 };
 
 #endif // CPROVER_UTIL_SIMPLIFY_EXPR_CLASS_H

src/util/simplify_expr_if.cpp

@@ -254,17 +254,16 @@ simplify_exprt::simplify_if_preorder(const if_exprt &expr)
       simplify_rec(r_cond.expr.is_true() ? truevalue : falsevalue));
   }
 
-  if(do_simplify_if)
-  {
-    bool swap_branches = false;
+  bool swap_branches = false;
 
-    if(r_cond.expr.id() == ID_not)
-    {
-      r_cond = changed(to_not_expr(r_cond.expr).op());
-      swap_branches = true;
-    }
+  if(r_cond.expr.id() == ID_not)
+  {
+    r_cond = changed(to_not_expr(r_cond.expr).op());
+    swap_branches = true;
+  }
 
-#ifdef USE_LOCAL_REPLACE_MAP
+  if(do_simplify_if)
+  {
     replace_mapt map_before(local_replace_map);
 
     // a ? b : c  --> a ? b[a/true] : c
@@ -273,7 +272,10 @@ simplify_exprt::simplify_if_preorder(const if_exprt &expr)
       for(const auto &op : r_cond.expr.operands())
       {
         if(op.id() == ID_not)
-          local_replace_map.insert(std::make_pair(op.op0(), false_exprt()));
+        {
+          local_replace_map.insert(
+            std::make_pair(to_not_expr(op).op(), false_exprt()));
+        }
         else
           local_replace_map.insert(std::make_pair(op, true_exprt()));
       }
@@ -291,7 +293,10 @@ simplify_exprt::simplify_if_preorder(const if_exprt &expr)
       for(const auto &op : r_cond.expr.operands())
       {
         if(op.id() == ID_not)
-          local_replace_map.insert(std::make_pair(op.op0(), true_exprt()));
+        {
+          local_replace_map.insert(
+            std::make_pair(to_not_expr(op).op(), true_exprt()));
+        }
         else
           local_replace_map.insert(std::make_pair(op, false_exprt()));
       }
@@ -306,11 +311,13 @@ simplify_exprt::simplify_if_preorder(const if_exprt &expr)
     if(swap_branches)
     {
       // tell build_if_expr to replace truevalue and falsevalue
-      r_truevalue.expr_changed = CHANGED;
-      r_falsevalue.expr_changed = CHANGED;
+      r_truevalue.expr_changed = resultt<>::CHANGED;
+      r_falsevalue.expr_changed = resultt<>::CHANGED;
     }
     return build_if_expr(expr, r_cond, r_truevalue, r_falsevalue);
-#else
+  }
+  else
+  {
     if(!swap_branches)
     {
       return build_if_expr(
@@ -324,12 +331,6 @@ simplify_exprt::simplify_if_preorder(const if_exprt &expr)
         changed(simplify_rec(falsevalue)),
         changed(simplify_rec(truevalue)));
     }
-#endif
-  }
-  else
-  {
-    return build_if_expr(
-      expr, r_cond, simplify_rec(truevalue), simplify_rec(falsevalue));
   }
 }
 
@@ -339,49 +340,46 @@ simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr)
   const exprt &truevalue = expr.true_case();
   const exprt &falsevalue = expr.false_case();
 
-  if(do_simplify_if)
-  {
 #if 0
-    no_change = simplify_if_cond(cond) && no_change;
-    no_change = simplify_if_branch(truevalue, falsevalue, cond) && no_change;
+  no_change = simplify_if_cond(cond) && no_change;
+  no_change = simplify_if_branch(truevalue, falsevalue, cond) && no_change;
 #endif
 
-    if(expr.type() == bool_typet())
-    {
-      // a?b:c <-> (a && b) || (!a && c)
+  if(expr.type() == bool_typet())
+  {
+    // a?b:c <-> (a && b) || (!a && c)
 
-      if(truevalue.is_true() && falsevalue.is_false())
-      {
-        // a?1:0 <-> a
-        return cond;
-      }
-      else if(truevalue.is_false() && falsevalue.is_true())
-      {
-        // a?0:1 <-> !a
-        return changed(simplify_not(not_exprt(cond)));
-      }
-      else if(falsevalue.is_false())
-      {
-        // a?b:0 <-> a AND b
-        return changed(simplify_boolean(and_exprt(cond, truevalue)));
-      }
-      else if(falsevalue.is_true())
-      {
-        // a?b:1 <-> !a OR b
-        return changed(
-          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_boolean(or_exprt(cond, falsevalue)));
-      }
-      else if(truevalue.is_false())
-      {
-        // a?0:b <-> !a && b
-        return changed(simplify_boolean(
-          and_exprt(simplify_not(not_exprt(cond)), falsevalue)));
-      }
+    if(truevalue.is_true() && falsevalue.is_false())
+    {
+      // a?1:0 <-> a
+      return cond;
+    }
+    else if(truevalue.is_false() && falsevalue.is_true())
+    {
+      // a?0:1 <-> !a
+      return changed(simplify_not(not_exprt(cond)));
+    }
+    else if(falsevalue.is_false())
+    {
+      // a?b:0 <-> a AND b
+      return changed(simplify_boolean(and_exprt(cond, truevalue)));
+    }
+    else if(falsevalue.is_true())
+    {
+      // a?b:1 <-> !a OR b
+      return changed(
+        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_boolean(or_exprt(cond, falsevalue)));
+    }
+    else if(truevalue.is_false())
+    {
+      // a?0:b <-> !a && b
+      return changed(
+        simplify_boolean(and_exprt(simplify_not(not_exprt(cond)), falsevalue)));
     }
   }