Merge pull request #4830 from diffblue/simplify_sig

simplifier cleanup

Author: Daniel Kroening

src/util/simplify_expr.cpp

@@ -63,21 +63,17 @@ struct simplify_expr_cachet
 simplify_expr_cachet simplify_expr_cache;
 #endif
 
-bool simplify_exprt::simplify_abs(exprt &expr)
+simplify_exprt::resultt<> simplify_exprt::simplify_abs(const abs_exprt &expr)
 {
-  if(expr.operands().size()!=1)
-    return true;
-
-  if(to_unary_expr(expr).op().is_constant())
+  if(expr.op().is_constant())
   {
     const typet &type = to_unary_expr(expr).op().type();
 
     if(type.id()==ID_floatbv)
     {
       ieee_floatt value(to_constant_expr(to_unary_expr(expr).op()));
       value.set_sign(false);
-      expr=value.to_expr();
-      return false;
+      return value.to_expr();
     }
     else if(type.id()==ID_signedbv ||
             type.id()==ID_unsignedbv)
@@ -87,20 +83,18 @@ bool simplify_exprt::simplify_abs(exprt &expr)
       {
         if(*value >= 0)
         {
-          expr = to_unary_expr(expr).op();
-          return false;
+          return to_unary_expr(expr).op();
         }
         else
         {
           value->negate();
-          expr = from_integer(*value, type);
-          return false;
+          return from_integer(*value, type);
         }
       }
     }
   }
 
-  return true;
+  return unchanged(expr);
 }
 
 bool simplify_exprt::simplify_sign(exprt &expr)
@@ -133,7 +127,8 @@ bool simplify_exprt::simplify_sign(exprt &expr)
   return true;
 }
 
-bool simplify_exprt::simplify_popcount(popcount_exprt &expr)
+simplify_exprt::resultt<>
+simplify_exprt::simplify_popcount(const popcount_exprt &expr)
 {
   const exprt &op = expr.op();
 
@@ -151,41 +146,35 @@ bool simplify_exprt::simplify_popcount(popcount_exprt &expr)
         if(get_bvrep_bit(value, width, i))
           result++;
 
-      auto result_expr = from_integer(result, expr.type());
-      expr.swap(result_expr);
-
-      return false;
+      return from_integer(result, expr.type());
     }
   }
 
-  return true;
+  return unchanged(expr);
 }
 
-bool simplify_exprt::simplify_function_application(exprt &expr)
+simplify_exprt::resultt<> simplify_exprt::simplify_function_application(
+  const function_application_exprt &expr)
 {
-  const function_application_exprt &function_app =
-    to_function_application_expr(expr);
-
-  if(function_app.function().id() != ID_symbol)
-    return true;
+  if(expr.function().id() != ID_symbol)
+    return unchanged(expr);
 
-  const irep_idt func_id =
-    to_symbol_expr(function_app.function()).get_identifier();
+  const irep_idt &func_id = to_symbol_expr(expr.function()).get_identifier();
 
   // Starts-with is used for .equals.
   if(func_id == ID_cprover_string_startswith_func)
   {
     // We want to get both arguments of any starts-with comparison, and
     // trace them back to the actual string instance. All variables on the
     // way must be constant for us to be sure this will work.
-    auto &first_argument = to_string_expr(function_app.arguments().at(0));
-    auto &second_argument = to_string_expr(function_app.arguments().at(1));
+    auto &first_argument = to_string_expr(expr.arguments().at(0));
+    auto &second_argument = to_string_expr(expr.arguments().at(1));
 
     const auto first_value_opt = try_get_string_data_array(first_argument, ns);
 
     if(!first_value_opt)
     {
-      return true;
+      return unchanged(expr);
     }
 
     const array_exprt &first_value = first_value_opt->get();
@@ -195,17 +184,17 @@ bool simplify_exprt::simplify_function_application(exprt &expr)
 
     if(!second_value_opt)
     {
-      return true;
+      return unchanged(expr);
     }
 
     const array_exprt &second_value = second_value_opt->get();
 
     mp_integer offset_int = 0;
-    if(function_app.arguments().size() == 3)
+    if(expr.arguments().size() == 3)
     {
-      auto &offset = function_app.arguments()[2];
+      auto &offset = expr.arguments()[2];
       if(offset.id() != ID_constant)
-        return true;
+        return unchanged(expr);
       offset_int = numeric_cast_v<mp_integer>(to_constant_expr(offset));
     }
 
@@ -232,26 +221,25 @@ bool simplify_exprt::simplify_function_application(exprt &expr)
           ++second_it;
       }
     }
-    expr = from_integer(is_prefix ? 1 : 0, expr.type());
-    return false;
+
+    return from_integer(is_prefix ? 1 : 0, expr.type());
   }
   else if(func_id == ID_cprover_string_char_at_func)
   {
-    if(function_app.arguments().at(1).id() != ID_constant)
+    if(expr.arguments().at(1).id() != ID_constant)
     {
-      return true;
+      return unchanged(expr);
     }
 
-    const auto &index = to_constant_expr(function_app.arguments().at(1));
+    const auto &index = to_constant_expr(expr.arguments().at(1));
 
-    const refined_string_exprt &s =
-      to_string_expr(function_app.arguments().at(0));
+    const refined_string_exprt &s = to_string_expr(expr.arguments().at(0));
 
     const auto char_seq_opt = try_get_string_data_array(s, ns);
 
     if(!char_seq_opt)
     {
-      return true;
+      return unchanged(expr);
     }
 
     const array_exprt &char_seq = char_seq_opt->get();
@@ -260,22 +248,20 @@ bool simplify_exprt::simplify_function_application(exprt &expr)
 
     if(!i_opt || *i_opt >= char_seq.operands().size())
     {
-      return true;
+      return unchanged(expr);
     }
 
     const auto &c = to_constant_expr(char_seq.operands().at(*i_opt));
 
     if(c.type() != expr.type())
     {
-      return true;
+      return unchanged(expr);
     }
 
-    expr = c;
-
-    return false;
+    return c;
   }
 
-  return true;
+  return unchanged(expr);
 }
 
 simplify_exprt::resultt<>
@@ -862,38 +848,39 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
   return unchanged(expr);
 }
 
-bool simplify_exprt::simplify_dereference(exprt &expr)
+simplify_exprt::resultt<>
+simplify_exprt::simplify_dereference(const dereference_exprt &expr)
 {
-  const exprt &pointer=to_dereference_expr(expr).pointer();
+  const exprt &pointer = expr.pointer();
 
   if(pointer.type().id()!=ID_pointer)
-    return true;
+    return unchanged(expr);
 
   if(pointer.id()==ID_if && pointer.operands().size()==3)
   {
     const if_exprt &if_expr=to_if_expr(pointer);
 
-    exprt tmp_op1=expr;
-    tmp_op1.op0()=if_expr.true_case();
-    simplify_dereference(tmp_op1);
-    exprt tmp_op2=expr;
-    tmp_op2.op0()=if_expr.false_case();
-    simplify_dereference(tmp_op2);
+    auto tmp_op1 = expr;
+    tmp_op1.op() = if_expr.true_case();
+    exprt tmp_op1_result = simplify_dereference(tmp_op1);
 
-    expr=if_exprt(if_expr.cond(), tmp_op1, tmp_op2);
+    auto tmp_op2 = expr;
+    tmp_op2.op() = if_expr.false_case();
+    exprt tmp_op2_result = simplify_dereference(tmp_op2);
 
-    simplify_if(to_if_expr(expr));
+    if_exprt tmp{if_expr.cond(), tmp_op1_result, tmp_op2_result};
 
-    return false;
+    simplify_if(tmp);
+
+    return tmp;
   }
 
   if(pointer.id()==ID_address_of)
   {
     exprt tmp=to_address_of_expr(pointer).object();
     // one address_of is gone, try again
     simplify_rec(tmp);
-    expr.swap(tmp);
-    return false;
+    return tmp;
   }
   // rewrite *(&a[0] + x) to a[x]
   else if(pointer.id()==ID_plus &&
@@ -912,13 +899,12 @@ bool simplify_exprt::simplify_dereference(exprt &expr)
           pointer_offset_sum(old.index(), pointer.op1()),
           old.array().type().subtype());
         simplify_rec(idx);
-        expr.swap(idx);
-        return false;
+        return idx;
       }
     }
   }
 
-  return true;
+  return unchanged(expr);
 }
 
 bool simplify_exprt::simplify_if_implies(
@@ -2505,7 +2491,14 @@ bool simplify_exprt::simplify_node(exprt &expr)
           expr.id()==ID_and)
     no_change = simplify_boolean(expr) && no_change;
   else if(expr.id()==ID_dereference)
-    no_change = simplify_dereference(expr) && no_change;
+  {
+    auto r = simplify_dereference(to_dereference_expr(expr));
+    if(r.has_changed())
+    {
+      no_change = false;
+      expr = r.expr;
+    }
+  }
   else if(expr.id()==ID_address_of)
     no_change = simplify_address_of(expr) && no_change;
   else if(expr.id()==ID_pointer_offset)
@@ -2528,13 +2521,34 @@ bool simplify_exprt::simplify_node(exprt &expr)
   else if(expr.id()==ID_isnormal)
     no_change = simplify_isnormal(expr) && no_change;
   else if(expr.id()==ID_abs)
-    no_change = simplify_abs(expr) && no_change;
+  {
+    auto r = simplify_abs(to_abs_expr(expr));
+    if(r.has_changed())
+    {
+      no_change = false;
+      expr = r.expr;
+    }
+  }
   else if(expr.id()==ID_sign)
     no_change = simplify_sign(expr) && no_change;
   else if(expr.id() == ID_popcount)
-    no_change = simplify_popcount(to_popcount_expr(expr)) && no_change;
+  {
+    auto r = simplify_popcount(to_popcount_expr(expr));
+    if(r.has_changed())
+    {
+      no_change = false;
+      expr = r.expr;
+    }
+  }
   else if(expr.id() == ID_function_application)
-    no_change = simplify_function_application(expr) && no_change;
+  {
+    auto r = simplify_function_application(to_function_application_expr(expr));
+    if(r.has_changed())
+    {
+      no_change = false;
+      expr = r.expr;
+    }
+  }
   else if(expr.id() == ID_complex_real || expr.id() == ID_complex_imag)
     no_change = simplify_complex(expr) && no_change;
 

src/util/simplify_expr_class.h

@@ -25,12 +25,15 @@ Author: Daniel Kroening, [email protected]
 #include "replace_expr.h"
 #endif
 
+class abs_exprt;
 class array_exprt;
 class bswap_exprt;
 class byte_extract_exprt;
 class byte_update_exprt;
+class dereference_exprt;
 class exprt;
 class extractbits_exprt;
+class function_application_exprt;
 class if_exprt;
 class index_exprt;
 class member_exprt;
@@ -152,21 +155,21 @@ class simplify_exprt
   bool simplify_object(exprt &expr);
   bool simplify_unary_minus(exprt &expr);
   bool simplify_unary_plus(exprt &expr);
-  bool simplify_dereference(exprt &expr);
+  resultt<> simplify_dereference(const dereference_exprt &);
   bool simplify_address_of(exprt &expr);
   bool simplify_pointer_offset(exprt &expr);
   bool simplify_bswap(bswap_exprt &expr);
   bool simplify_isinf(exprt &expr);
   bool simplify_isnan(exprt &expr);
   bool simplify_isnormal(exprt &expr);
-  bool simplify_abs(exprt &expr);
+  resultt<> simplify_abs(const abs_exprt &);
   bool simplify_sign(exprt &expr);
-  bool simplify_popcount(popcount_exprt &expr);
+  resultt<> simplify_popcount(const popcount_exprt &);
   bool simplify_complex(exprt &expr);
 
   /// Attempt to simplify mathematical function applications if we have
   /// enough information to do so. Currently focused on constant comparisons.
-  bool simplify_function_application(exprt &expr);
+  resultt<> simplify_function_application(const function_application_exprt &);
 
   // auxiliary
   bool simplify_if_implies(