WIP: Use resultt for simplify_node_preorder

Author: tautschnig

src/util/simplify_expr.cpp

@@ -2013,38 +2013,46 @@ simplify_exprt::simplify_complex(const unary_exprt &expr)
   return unchanged(expr);
 }
 
-bool simplify_exprt::simplify_node_preorder(exprt &expr)
+simplify_exprt::resultt<>
+simplify_exprt::simplify_node_preorder(const exprt &expr)
 {
-  bool result=true;
-
   // The ifs below could one day be replaced by a switch()
 
   if(expr.id()==ID_address_of)
   {
     // the argument of this expression needs special treatment
   }
   else if(expr.id()==ID_if)
-    result=simplify_if_preorder(to_if_expr(expr));
-  else
   {
-    if(expr.has_operands())
+    return simplify_if_preorder(to_if_expr(expr));
+  }
+  else if(expr.has_operands())
+  {
+    optionalt<exprt::operandst> new_operands;
+
+    for(std::size_t i = 0; i < expr.operands().size(); ++i)
     {
-      Forall_operands(it, expr)
+      auto r_it = simplify_rec(expr.operands()[i]); // recursive call
+      if(r_it.has_changed())
       {
-        auto r_it = simplify_rec(*it); // recursive call
-        if(r_it.has_changed())
-        {
-          *it = r_it.expr;
-          result=false;
-        }
+        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 result;
+  return unchanged(expr);
 }
 
-simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node)
+simplify_exprt::resultt<> simplify_exprt::simplify_node(const exprt &node)
 {
   if(!node.has_operands())
     return unchanged(node); // no change
@@ -2298,49 +2306,47 @@ simplify_exprt::resultt<> simplify_exprt::simplify_rec(const exprt &expr)
   #endif
 
   // We work on a copy to prevent unnecessary destruction of sharing.
-  exprt tmp=expr;
-  bool no_change = simplify_node_preorder(tmp);
+  auto simplify_node_preorder_result = simplify_node_preorder(expr);
 
-  auto simplify_node_result = simplify_node(tmp);
+  auto simplify_node_result = simplify_node(simplify_node_preorder_result.expr);
 
-  if(simplify_node_result.has_changed())
-  {
-    no_change = false;
-    tmp = simplify_node_result.expr;
-  }
+  if(
+    !simplify_node_result.has_changed() &&
+    simplify_node_preorder_result.has_changed())
+    simplify_node_result.expr_changed =
+      simplify_node_preorder_result.expr_changed;
 
 #ifdef USE_LOCAL_REPLACE_MAP
-  #if 1
-  replace_mapt::const_iterator it=local_replace_map.find(tmp);
+  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);
+#  else
+  if(
+    !local_replace_map.empty() &&
+    !replace_expr(local_replace_map, simplify_node_result.expr))
   {
-    tmp=it->second;
-    no_change = false;
-  }
-  #else
-  if(!local_replace_map.empty() &&
-     !replace_expr(local_replace_map, tmp))
-  {
-    simplify_rec(tmp);
-    no_change = false;
+    simplify_node_result = changed(simplify_rec(simplify_node_result.expr));
   }
-  #endif
+#  endif
 #endif
 
-  if(no_change) // no change
+  if(!simplify_node_result.has_changed())
   {
     return unchanged(expr);
   }
-  else // change, new expression is 'tmp'
+  else
   {
-    POSTCONDITION(as_const(tmp).type() == expr.type());
+    POSTCONDITION(as_const(simplify_node_result.expr).type() == expr.type());
 
 #ifdef USE_CACHE
     // save in cache
-    cache_result.first->second = tmp;
+    cache_result.first->second = simplify_node_result.expr;
 #endif
 
-    return std::move(tmp);
+    return simplify_node_result;
   }
 }
 

src/util/simplify_expr_class.h

@@ -150,7 +150,7 @@ class simplify_exprt
   NODISCARD resultt<> simplify_shifts(const shift_exprt &);
   NODISCARD resultt<> simplify_power(const binary_exprt &);
   NODISCARD resultt<> simplify_bitwise(const multi_ary_exprt &);
-  bool simplify_if_preorder(if_exprt &expr);
+  NODISCARD resultt<> simplify_if_preorder(const if_exprt &expr);
   NODISCARD resultt<> simplify_if(const if_exprt &);
   NODISCARD resultt<> simplify_bitnot(const bitnot_exprt &);
   NODISCARD resultt<> simplify_not(const not_exprt &);
@@ -211,8 +211,8 @@ class simplify_exprt
   simplify_inequality_pointer_object(const binary_relation_exprt &);
 
   // main recursion
-  NODISCARD resultt<> simplify_node(exprt);
-  bool simplify_node_preorder(exprt &expr);
+  NODISCARD resultt<> simplify_node(const exprt &);
+  NODISCARD resultt<> simplify_node_preorder(const exprt &);
   NODISCARD resultt<> simplify_rec(const exprt &);
 
   virtual bool simplify(exprt &expr);

src/util/simplify_expr_if.cpp

@@ -212,47 +212,66 @@ bool simplify_exprt::simplify_if_cond(exprt &expr)
   return no_change;
 }
 
-bool simplify_exprt::simplify_if_preorder(if_exprt &expr)
+static simplify_exprt::resultt<> build_if_expr(
+  const if_exprt &expr,
+  simplify_exprt::resultt<> cond,
+  simplify_exprt::resultt<> truevalue,
+  simplify_exprt::resultt<> falsevalue)
 {
-  exprt &cond = expr.cond();
-  exprt &truevalue = expr.true_case();
-  exprt &falsevalue = expr.false_case();
+  if(
+    !cond.has_changed() && !truevalue.has_changed() &&
+    !falsevalue.has_changed())
+  {
+    return simplify_exprt::resultt<>(
+      simplify_exprt::resultt<>::UNCHANGED, expr);
+  }
+  else
+  {
+    if_exprt result = expr;
+    if(cond.has_changed())
+      result.cond() = std::move(cond.expr);
+    if(truevalue.has_changed())
+      result.true_case() = std::move(truevalue.expr);
+    if(falsevalue.has_changed())
+      result.false_case() = std::move(falsevalue.expr);
+    return result;
+  }
+}
 
-  bool no_change = true;
+simplify_exprt::resultt<>
+simplify_exprt::simplify_if_preorder(const if_exprt &expr)
+{
+  const exprt &cond = expr.cond();
+  const exprt &truevalue = expr.true_case();
+  const exprt &falsevalue = expr.false_case();
 
   // we first want to look at the condition
   auto r_cond = simplify_rec(cond);
-  if(r_cond.has_changed())
-  {
-    cond = r_cond.expr;
-    no_change = false;
-  }
 
   // 1 ? a : b -> a  and  0 ? a : b -> b
-  if(cond.is_constant())
+  if(r_cond.expr.is_constant())
   {
-    exprt tmp = cond.is_true() ? truevalue : falsevalue;
-    tmp = simplify_rec(tmp);
-    expr.swap(tmp);
-    return false;
+    return changed(
+      simplify_rec(r_cond.expr.is_true() ? truevalue : falsevalue));
   }
 
   if(do_simplify_if)
   {
-    if(cond.id() == ID_not)
+    bool swap_branches = false;
+
+    if(r_cond.expr.id() == ID_not)
     {
-      cond = to_not_expr(cond).op();
-      truevalue.swap(falsevalue);
-      no_change = false;
+      r_cond = changed(to_not_expr(r_cond.expr).op());
+      swap_branches = true;
     }
 
 #ifdef USE_LOCAL_REPLACE_MAP
     replace_mapt map_before(local_replace_map);
 
     // a ? b : c  --> a ? b[a/true] : c
-    if(cond.id() == ID_and)
+    if(r_cond.expr.id() == ID_and)
     {
-      forall_operands(it, cond)
+      forall_operands(it, r_cond.expr)
       {
         if(it->id() == ID_not)
           local_replace_map.insert(std::make_pair(it->op0(), false_exprt()));
@@ -261,21 +280,18 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr)
       }
     }
     else
-      local_replace_map.insert(std::make_pair(cond, true_exprt()));
+      local_replace_map.insert(std::make_pair(r_cond.expr, true_exprt()));
 
-    auto r_truevalue = simplify_rec(truevalue);
-    if(r_truevalue.has_changed())
-    {
-      truevalue = r_truevalue.expr;
-      no_change = false;
-    }
+    auto r_truevalue = simplify_rec(swap_branches ? falsevalue : truevalue);
+    if(swap_branches)
+      r_truevalue.expr_changed = CHANGED;
 
     local_replace_map = map_before;
 
     // a ? b : c  --> a ? b : c[a/false]
-    if(cond.id() == ID_or)
+    if(r_cond.expr.id() == ID_or)
     {
-      forall_operands(it, cond)
+      forall_operands(it, r_cond.expr)
       {
         if(it->id() == ID_not)
           local_replace_map.insert(std::make_pair(it->op0(), true_exprt()));
@@ -284,48 +300,36 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr)
       }
     }
     else
-      local_replace_map.insert(std::make_pair(cond, false_exprt()));
+      local_replace_map.insert(std::make_pair(r_cond.expr, false_exprt()));
 
-    auto r_falsevalue = simplify_rec(falsevalue);
-    if(r_falsevalue.has_changed())
-    {
-      falsevalue = r_falsevalue.expr;
-      no_change = false;
-    }
+    auto falsevalue = simplify_rec(swap_branches ? falsevalue : truevalue);
+    if(swap_branches)
+      r_falsevalue.expr_changed = CHANGED;
 
     local_replace_map.swap(map_before);
+
+    return build_if_expr(expr, r_cond, r_truevalue, r_falsevalue);
 #else
-    auto r_truevalue = simplify_rec(truevalue);
-    if(r_truevalue.has_changed())
+    if(!swap_branches)
     {
-      truevalue = r_truevalue.expr;
-      no_change = false;
+      return build_if_expr(
+        expr, r_cond, simplify_rec(truevalue), simplify_rec(falsevalue));
     }
-    auto r_falsevalue = simplify_rec(falsevalue);
-    if(r_falsevalue.has_changed())
+    else
     {
-      falsevalue = r_falsevalue.expr;
-      no_change = false;
+      return build_if_expr(
+        expr,
+        r_cond,
+        changed(simplify_rec(falsevalue)),
+        changed(simplify_rec(truevalue)));
     }
 #endif
   }
   else
   {
-    auto r_truevalue = simplify_rec(truevalue);
-    if(r_truevalue.has_changed())
-    {
-      truevalue = r_truevalue.expr;
-      no_change = false;
-    }
-    auto r_falsevalue = simplify_rec(falsevalue);
-    if(r_falsevalue.has_changed())
-    {
-      falsevalue = r_falsevalue.expr;
-      no_change = false;
-    }
+    return build_if_expr(
+      expr, r_cond, simplify_rec(truevalue), simplify_rec(falsevalue));
   }
-
-  return no_change;
 }
 
 simplify_exprt::resultt<> simplify_exprt::simplify_if(const if_exprt &expr)