simplifier: simplify_rec has new interface

This improves type safety.

Author: Daniel Kroening

src/util/simplify_expr.cpp

@@ -535,7 +535,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
           from_integer(*sub_size, size_type()),
           typecast_exprt(expr.op().op1(), size_type()));
 
-      simplify_rec(new_expr.op()); // rec. call
+      new_expr.op() = simplify_rec(new_expr.op()); // rec. call
 
       return changed(simplify_typecast(new_expr)); // rec. call
     }
@@ -619,8 +619,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
         }
       }
 
-      simplify_rec(new_expr);
-      return std::move(new_expr);
+      return changed(simplify_rec(new_expr)); // recursive call
     }
   }
 
@@ -959,8 +958,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
       auto result =
         address_of_exprt(index_exprt(o, from_integer(0, size_type())));
 
-      simplify_rec(result);
-      return std::move(result);
+      return changed(simplify_rec(result)); // recursive call
     }
   }
 
@@ -996,8 +994,7 @@ simplify_exprt::simplify_dereference(const dereference_exprt &expr)
   {
     exprt tmp=to_address_of_expr(pointer).object();
     // one address_of is gone, try again
-    simplify_rec(tmp);
-    return tmp;
+    return changed(simplify_rec(tmp));
   }
   // rewrite *(&a[0] + x) to a[x]
   else if(pointer.id()==ID_plus &&
@@ -1015,8 +1012,7 @@ simplify_exprt::simplify_dereference(const dereference_exprt &expr)
           old.array(),
           pointer_offset_sum(old.index(), pointer.op1()),
           old.array().type().subtype());
-        simplify_rec(idx);
-        return idx;
+        return changed(simplify_rec(idx));
       }
     }
   }
@@ -1179,9 +1175,9 @@ bool simplify_exprt::simplify_if_branch(
   }
 
   if(!tresult)
-    simplify_rec(trueexpr);
+    trueexpr = simplify_rec(trueexpr); // recursive call
   if(!fresult)
-    simplify_rec(falseexpr);
+    falseexpr = simplify_rec(falseexpr); // recursive call
 
   return tresult && fresult;
 }
@@ -1214,7 +1210,7 @@ bool simplify_exprt::simplify_if_cond(exprt &expr)
     }
 
     if(!tmp)
-      simplify_rec(expr);
+      expr = simplify_rec(expr); // recursive call
 
     result=tmp && result;
   }
@@ -1228,14 +1224,21 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr)
   exprt &truevalue=expr.true_case();
   exprt &falsevalue=expr.false_case();
 
+  bool result = true;
+
   // we first want to look at the condition
-  bool result=simplify_rec(cond);
+  auto r_cond = simplify_rec(cond);
+  if(r_cond.has_changed())
+  {
+    cond = r_cond.expr;
+    result = false;
+  }
 
   // 1 ? a : b -> a  and  0 ? a : b -> b
   if(cond.is_constant())
   {
     exprt tmp=cond.is_true()?truevalue:falsevalue;
-    simplify_rec(tmp);
+    tmp = simplify_rec(tmp);
     expr.swap(tmp);
     return false;
   }
@@ -1270,7 +1273,12 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr)
     else
       local_replace_map.insert(std::make_pair(cond, true_exprt()));
 
-    result=simplify_rec(truevalue) && result;
+    auto r_truevalue = simplify_rec(truevalue);
+    if(r_truevalue.has_changed())
+    {
+      truevalue = r_truevalue.expr;
+      result = false;
+    }
 
     local_replace_map=map_before;
 
@@ -1290,18 +1298,43 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr)
     else
       local_replace_map.insert(std::make_pair(cond, false_exprt()));
 
-    result=simplify_rec(falsevalue) && result;
+    auto r_falsevalue = simplify_rec(falsevalue);
+    if(r_falsevalue.has_changed())
+    {
+      falsevalue = r_falsevalue.expr;
+      result = false;
+    }
 
     local_replace_map.swap(map_before);
 #else
-    result=simplify_rec(truevalue) && result;
-    result=simplify_rec(falsevalue) && result;
+    auto r_truevalue = simplify_rec(truevalue);
+    if(r_truevalue.has_changed())
+    {
+      truevalue = r_truevalue.expr;
+      result = false;
+    }
+    auto r_falsevalue = simplify_rec(falsevalue);
+    if(r_falsevalue.has_changed())
+    {
+      falsevalue = r_falsevalue.expr;
+      result = false;
+    }
 #endif
   }
   else
   {
-    result=simplify_rec(truevalue) && result;
-    result=simplify_rec(falsevalue) && result;
+    auto r_truevalue = simplify_rec(truevalue);
+    if(r_truevalue.has_changed())
+    {
+      truevalue = r_truevalue.expr;
+      result = false;
+    }
+    auto r_falsevalue = simplify_rec(falsevalue);
+    if(r_falsevalue.has_changed())
+    {
+      falsevalue = r_falsevalue.expr;
+      result = false;
+    }
   }
 
   return result;
@@ -2079,9 +2112,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
     auto tmp = expr;
     tmp.op() = index_exprt(expr.op(), expr.offset());
     tmp.offset() = from_integer(0, expr.offset().type());
-    simplify_rec(tmp);
-
-    return std::move(tmp);
+    return changed(simplify_rec(tmp));
   }
 
   // extract bits of a constant
@@ -2127,8 +2158,7 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   if(!subexpr.has_value() || subexpr.value() == expr)
     return unchanged(expr);
 
-  simplify_rec(subexpr.value());
-  return subexpr.value();
+  return changed(simplify_rec(subexpr.value())); // recursive call
 }
 
 simplify_exprt::resultt<>
@@ -2351,16 +2381,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
     }
 
     if(result_expr.is_not_nil())
-    {
-      simplify_rec(result_expr);
-      return result_expr;
-    }
-
-    if(result_expr.is_not_nil())
-    {
-      simplify_rec(result_expr);
-      return result_expr;
-    }
+      return changed(simplify_rec(result_expr));
   }
 
   // replace elements of array or struct expressions, possibly using
@@ -2404,7 +2425,7 @@ simplify_exprt::simplify_byte_update(const byte_update_exprt &expr)
             *offset_int + val_offset - m_offset_bits / 8, offset.type()),
           new_val);
 
-        simplify_rec(*it);
+        *it = simplify_rec(*it); // recursive call
 
         val_offset+=bytes_req;
       }
@@ -2455,8 +2476,14 @@ bool simplify_exprt::simplify_node_preorder(exprt &expr)
     if(expr.has_operands())
     {
       Forall_operands(it, expr)
-        if(!simplify_rec(*it)) // recursive call
+      {
+        auto r_it = simplify_rec(*it); // recursive call
+        if(r_it.has_changed())
+        {
+          *it = r_it.expr;
           result=false;
+        }
+      }
     }
   }
 
@@ -2699,8 +2726,7 @@ bool simplify_exprt::simplify_node(exprt &expr)
   return no_change;
 }
 
-/// \return returns true if expression unchanged; returns false if changed
-bool simplify_exprt::simplify_rec(exprt &expr)
+simplify_exprt::resultt<> simplify_exprt::simplify_rec(const exprt &expr)
 {
   // look up in cache
 
@@ -2746,34 +2772,45 @@ bool simplify_exprt::simplify_rec(exprt &expr)
   #endif
 #endif
 
-  if(!result)
+  if(result) // no change
   {
-    POSTCONDITION(tmp.type() == expr.type());
-    expr.swap(tmp);
+    return unchanged(expr);
+  }
+  else // change, new expression is 'tmp'
+  {
+    POSTCONDITION(as_const(tmp).type() == expr.type());
 
-    #ifdef USE_CACHE
+#ifdef USE_CACHE
     // save in cache
-    cache_result.first->second=expr;
-    #endif
-  }
+    cache_result.first->second = tmp;
+#endif
 
-  return result;
+    return std::move(tmp);
+  }
 }
 
+/// \return returns true if expression unchanged; returns false if changed
 bool simplify_exprt::simplify(exprt &expr)
 {
 #ifdef DEBUG_ON_DEMAND
   if(debug_on)
     std::cout << "TO-SIMP " << format(expr) << "\n";
 #endif
-  bool res=simplify_rec(expr);
+  auto result = simplify_rec(expr);
 #ifdef DEBUG_ON_DEMAND
   if(debug_on)
-    std::cout << "FULLSIMP " << format(expr) << "\n";
+    std::cout << "FULLSIMP " << format(result.expr) << "\n";
 #endif
-  return res;
+  if(result.has_changed())
+  {
+    expr = result.expr;
+    return false; // change
+  }
+  else
+    return true; // no change
 }
 
+/// \return returns true if expression unchanged; returns false if changed
 bool simplify(exprt &expr, const namespacet &ns)
 {
   return simplify_exprt(ns).simplify(expr);

src/util/simplify_expr_array.cpp

@@ -59,8 +59,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_index(const exprt &expr)
     {
       exprt tmp = comprehension.body();
       replace_expr(comprehension.arg(), index, tmp);
-      simplify_rec(tmp);
-      return std::move(tmp);
+      return changed(simplify_rec(tmp));
     }
   }
   else if(array.id()==ID_with)
@@ -188,9 +187,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_index(const exprt &expr)
       exprt result_expr(array.id(), expr.type());
       result_expr.add_to_operands(array.op0(), final_offset);
 
-      simplify_rec(result_expr);
-
-      return std::move(result_expr);
+      return changed(simplify_rec(result_expr));
     }
   }
   else if(array.id()==ID_if)
@@ -204,9 +201,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_index(const exprt &expr)
     index_expr.array() = if_expr.true_case();
 
     exprt result = if_exprt(cond, index_expr, idx_false, expr.type());
-    simplify_rec(result);
-
-    return std::move(result);
+    return changed(simplify_rec(result));
   }
 
   if(no_change)

src/util/simplify_expr_class.h

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

src/util/simplify_expr_pointer.cpp

@@ -69,8 +69,13 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr)
       new_index_expr.array() = array_result.expr;
     }
 
-    if(!simplify_rec(new_index_expr.index()))
+    auto index_result = simplify_rec(new_index_expr.index());
+
+    if(index_result.has_changed())
+    {
       no_change = false;
+      new_index_expr.index() = index_result.expr;
+    }
 
     // rewrite (*(type *)int) [index] by
     // pushing the index inside
@@ -148,17 +153,25 @@ simplify_exprt::simplify_address_of_arg(const exprt &expr)
   else if(expr.id()==ID_dereference)
   {
     auto new_expr = to_dereference_expr(expr);
-    if(!simplify_rec(new_expr.pointer()))
+    auto r_pointer = simplify_rec(new_expr.pointer());
+    if(r_pointer.has_changed())
+    {
+      new_expr.pointer() = r_pointer.expr;
       return std::move(new_expr);
+    }
   }
   else if(expr.id()==ID_if)
   {
     auto new_if_expr = to_if_expr(expr);
 
     bool no_change = true;
 
-    if(!simplify_rec(new_if_expr.cond()))
+    auto r_cond = simplify_rec(new_if_expr.cond());
+    if(r_cond.has_changed())
+    {
+      new_if_expr.cond() = r_cond.expr;
       no_change = false;
+    }
 
     auto true_result = simplify_address_of_arg(new_if_expr.true_case());
     if(true_result.has_changed())
@@ -547,9 +560,7 @@ simplify_exprt::simplify_pointer_object(const exprt &expr)
     p_o_true.op0() = if_expr.true_case();
 
     auto new_expr = if_exprt(cond, p_o_true, p_o_false, expr.type());
-    simplify_rec(new_expr);
-
-    return new_expr;
+    return changed(simplify_rec(new_expr));
   }
 
   if(op_result.has_changed())