Simplify cond_exprt

This handles all the cases in the simplifier that special-cased if_exprt

Author: smowton

src/util/simplify_expr.cpp

@@ -1237,6 +1237,50 @@ bool simplify_exprt::simplify_if_preorder(if_exprt &expr)
   return result;
 }
 
+bool simplify_exprt::simplify_cond_preorder(cond_exprt &expr)
+{
+  cond_exprt new_expr({}, expr.type(), expr.is_exclusive());
+  bool result = true;
+
+#ifdef USE_LOCAL_REPLACE_MAP
+#  error "TODO: implement simplify_cond_preorder use of replacement maps"
+#endif
+
+  for(std::size_t i = 0; i < expr.get_n_cases(); ++i)
+  {
+    exprt condition = as_const(expr).condition(i);
+    if(!simplify_rec(condition))
+      result = false;
+
+    if(condition.is_true() && (i == 0 || expr.is_exclusive()))
+    {
+      expr.swap(expr.value(i));
+      simplify_rec(expr);
+      return false;
+    }
+
+    if(!condition.is_false())
+    {
+      exprt value = as_const(expr).value(i);
+      if(!simplify_rec(value))
+        result = false;
+      new_expr.add_case(condition, value);
+    }
+    else
+    {
+      result = false;
+    }
+
+    if(condition.is_true())
+      break;
+  }
+
+  if(!result)
+    expr = std::move(new_expr);
+
+  return result;
+}
+
 bool simplify_exprt::simplify_if(if_exprt &expr)
 {
   exprt &cond=expr.cond();
@@ -1343,6 +1387,27 @@ bool simplify_exprt::simplify_if(if_exprt &expr)
   return result;
 }
 
+bool simplify_exprt::simplify_cond(cond_exprt &expr)
+{
+  optionalt<exprt> unique_value;
+  for(std::size_t i = 0; i < expr.get_n_cases(); ++i)
+  {
+    const exprt &value = as_const(expr).value(i);
+    if(!unique_value.has_value())
+      unique_value = value;
+    else if(value != *unique_value)
+      return true;
+  }
+
+  if(unique_value.has_value())
+  {
+    expr.swap(*unique_value);
+    return false;
+  }
+
+  return true;
+}
+
 bool simplify_exprt::get_values(
   const exprt &expr,
   value_listt &value_list)
@@ -1365,6 +1430,14 @@ bool simplify_exprt::get_values(
     return get_values(expr.op1(), value_list) ||
            get_values(expr.operands().back(), value_list);
   }
+  else if(expr.id() == ID_cond)
+  {
+    bool ret = false;
+    const auto &cond = to_cond_expr(expr);
+    for(std::size_t i = 0; i < cond.get_n_cases(); ++i)
+      ret |= get_values(cond.value(i), value_list);
+    return ret;
+  }
 
   return true;
 }
@@ -1877,6 +1950,13 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
     expr.swap(if_expr);
     return false;
   }
+  else if(expr.op().id() == ID_cond)
+  {
+    cond_exprt cond_expr = lift_cond(expr, 0);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      simplify_byte_extract(to_byte_extract_expr(cond_expr.value(i)));
+    simplify_cond(cond_expr);
+  }
 
   const auto el_size = pointer_offset_bits(expr.type(), ns);
 
@@ -2387,6 +2467,8 @@ bool simplify_exprt::simplify_node_preorder(exprt &expr)
   }
   else if(expr.id()==ID_if)
     result=simplify_if_preorder(to_if_expr(expr));
+  else if(expr.id() == ID_cond)
+    result = simplify_cond_preorder(to_cond_expr(expr));
   else
   {
     if(expr.has_operands())
@@ -2423,6 +2505,8 @@ bool simplify_exprt::simplify_node(exprt &expr)
     result=simplify_inequality(expr) && result;
   else if(expr.id()==ID_if)
     result=simplify_if(to_if_expr(expr)) && result;
+  else if(expr.id() == ID_cond)
+    result = simplify_cond(to_cond_expr(expr)) && result;
   else if(expr.id()==ID_lambda)
     result=simplify_lambda(expr) && result;
   else if(expr.id()==ID_with)

src/util/simplify_expr_array.cpp

@@ -219,6 +219,13 @@ bool simplify_exprt::simplify_index(exprt &expr)
 
     return false;
   }
+  else if(array.id() == ID_cond)
+  {
+    expr = lift_cond(expr, 0);
+    simplify_rec(expr);
+
+    return false;
+  }
 
   return result;
 }

src/util/simplify_expr_class.h

@@ -27,6 +27,7 @@ Author: Daniel Kroening, [email protected]
 class bswap_exprt;
 class byte_extract_exprt;
 class byte_update_exprt;
+class cond_exprt;
 class exprt;
 class extractbits_exprt;
 class if_exprt;
@@ -81,6 +82,8 @@ class simplify_exprt
   bool simplify_bitwise(exprt &expr);
   bool simplify_if_preorder(if_exprt &expr);
   bool simplify_if(if_exprt &expr);
+  bool simplify_cond_preorder(cond_exprt &expr);
+  bool simplify_cond(cond_exprt &expr);
   bool simplify_bitnot(exprt &expr);
   bool simplify_not(exprt &expr);
   bool simplify_boolean(exprt &expr);

src/util/simplify_expr_int.cpp

@@ -1319,6 +1319,15 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
     return simplify_inequality(expr);
   }
 
+  // if rhs is ID_cond (and lhs is not), swap operands for == and !=
+  if(
+    (expr.id() == ID_equal || expr.id() == ID_notequal) &&
+    tmp0.id() != ID_cond && tmp1.id() == ID_cond)
+  {
+    expr.op0().swap(expr.op1());
+    return simplify_inequality(expr);
+  }
+
   if(tmp0.id()==ID_if && tmp0.operands().size()==3)
   {
     if_exprt if_expr=lift_if(expr, 0);
@@ -1330,6 +1339,17 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
     return false;
   }
 
+  if(tmp0.id() == ID_cond)
+  {
+    cond_exprt cond_expr = lift_cond(expr, 0);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      simplify_inequality(cond_expr.value(i));
+    simplify_cond(cond_expr);
+    expr.swap(cond_expr);
+
+    return false;
+  }
+
   // see if we are comparing pointers that are address_of
   if((tmp0.id()==ID_address_of ||
         (tmp0.id()==ID_typecast && tmp0.op0().id()==ID_address_of)) &&
@@ -1687,6 +1707,17 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
     return false;
   }
 
+  if(expr.op0().id() == ID_cond)
+  {
+    cond_exprt cond_expr = lift_cond(expr, 0);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      simplify_inequality_constant(cond_expr.value(i));
+    simplify_cond(cond_expr);
+    expr.swap(cond_expr);
+
+    return false;
+  }
+
   // do we deal with pointers?
   if(expr.op1().type().id()==ID_pointer)
   {

src/util/simplify_expr_pointer.cpp

@@ -171,6 +171,49 @@ bool simplify_exprt::simplify_address_of_arg(exprt &expr)
       return result;
     }
   }
+  else if(expr.id() == ID_cond)
+  {
+    bool result = true;
+    const auto &cond_expr = to_cond_expr(expr);
+    cond_exprt new_cond_expr({}, cond_expr.type(), cond_expr.is_exclusive());
+
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+    {
+      exprt condition = cond_expr.condition(i);
+      exprt value = cond_expr.value(i);
+
+      if(!simplify_rec(condition))
+        result = false;
+
+      if(condition.is_false())
+        continue;
+
+      if(!simplify_address_of_arg(value))
+        result = false;
+
+      if(condition.is_true() && (cond_expr.is_exclusive() || i == 0))
+      {
+        expr.swap(value);
+        return false;
+      }
+
+      new_cond_expr.add_case(condition, value);
+
+      if(condition.is_true())
+        break;
+    }
+
+    if(new_cond_expr.get_n_cases() == 1)
+    {
+      expr = new_cond_expr.value(0);
+      return false;
+    }
+
+    if(!result)
+      expr = std::move(new_cond_expr);
+
+    return result;
+  }
 
   return true;
 }
@@ -230,6 +273,16 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
 
     return false;
   }
+  else if(ptr.id() == ID_cond)
+  {
+    cond_exprt cond_expr = lift_cond(expr, 0);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      simplify_pointer_offset(cond_expr.value(i));
+    simplify_cond(cond_expr);
+    expr.swap(cond_expr);
+
+    return false;
+  }
 
   if(ptr.type().id()!=ID_pointer)
     return true;
@@ -506,6 +559,16 @@ bool simplify_exprt::simplify_pointer_object(exprt &expr)
 
     return false;
   }
+  else if(op.id() == ID_cond)
+  {
+    cond_exprt cond_expr = lift_cond(expr, 0);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      simplify_pointer_object(cond_expr.value(i));
+    simplify_cond(cond_expr);
+    expr.swap(cond_expr);
+
+    return false;
+  }
 
   return result;
 }
@@ -527,6 +590,16 @@ bool simplify_exprt::simplify_is_dynamic_object(exprt &expr)
 
     return false;
   }
+  else if(op.id() == ID_cond)
+  {
+    cond_exprt cond_expr = lift_cond(expr, 0);
+    for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+      simplify_is_dynamic_object(cond_expr.value(i));
+    simplify_cond(cond_expr);
+    expr.swap(cond_expr);
+
+    return false;
+  }
 
   bool result=true;
 

src/util/simplify_expr_struct.cpp

@@ -282,6 +282,13 @@ bool simplify_exprt::simplify_member(exprt &expr)
 
     return false;
   }
+  else if(op.id() == ID_cond)
+  {
+    expr = lift_cond(expr, 0);
+    simplify_rec(expr);
+
+    return false;
+  }
 
   return true;
 }