Merge pull request #5025 from diffblue/solvers-opX

fix accesses to exprt::opX() in solvers/

Author: kroening

src/solvers/flattening/arrays.cpp

@@ -186,11 +186,12 @@ void arrayst::collect_arrays(const exprt &a)
   }
   else if(a.id()==ID_member)
   {
+    const auto &struct_op = to_member_expr(a).struct_op();
+
     DATA_INVARIANT(
-      to_member_expr(a).struct_op().id() == ID_symbol ||
-        to_member_expr(a).struct_op().id() == ID_nondet_symbol,
-      ("unexpected array expression: member with '" + a.op0().id_string() + "'")
-        .c_str());
+      struct_op.id() == ID_symbol || struct_op.id() == ID_nondet_symbol,
+      "unexpected array expression: member with '" + struct_op.id_string() +
+        "'");
   }
   else if(a.id()==ID_constant ||
           a.id()==ID_array ||
@@ -209,24 +210,22 @@ void arrayst::collect_arrays(const exprt &a)
   }
   else if(a.id()==ID_typecast)
   {
-    // cast between array types?
-    DATA_INVARIANT(
-      a.operands().size()==1,
-      "typecast must have one operand");
+    const auto &typecast_op = to_typecast_expr(a).op();
 
+    // cast between array types?
     DATA_INVARIANT(
-      a.op0().type().id()==ID_array,
-      ("unexpected array type cast from "+
-       a.op0().type().id_string()).c_str());
+      typecast_op.type().id() == ID_array,
+      "unexpected array type cast from " + typecast_op.type().id_string());
 
-    arrays.make_union(a, a.op0());
-    collect_arrays(a.op0());
+    arrays.make_union(a, typecast_op);
+    collect_arrays(typecast_op);
   }
   else if(a.id()==ID_index)
   {
     // nested unbounded arrays
-    arrays.make_union(a, a.op0());
-    collect_arrays(a.op0());
+    const auto &array_op = to_index_expr(a).array();
+    arrays.make_union(a, array_op);
+    collect_arrays(array_op);
   }
   else if(a.id() == ID_array_comprehension)
   {
@@ -235,8 +234,7 @@ void arrayst::collect_arrays(const exprt &a)
   {
     DATA_INVARIANT(
       false,
-      ("unexpected array expression (collect_arrays): '" + a.id_string() + "'")
-        .c_str());
+      "unexpected array expression (collect_arrays): '" + a.id_string() + "'");
   }
 }
 
@@ -496,16 +494,14 @@ void arrayst::add_array_constraints(
   else if(expr.id()==ID_typecast)
   {
     // we got a=(type[])b
-    DATA_INVARIANT(
-      expr.operands().size()==1,
-      "typecast should have one operand");
+    const auto &expr_typecast_op = to_typecast_expr(expr).op();
 
     // add a[i]=b[i]
     for(const auto &index : index_set)
     {
       const typet &subtype = expr.type().subtype();
       index_exprt index_expr1(expr, index, subtype);
-      index_exprt index_expr2(expr.op0(), index, subtype);
+      index_exprt index_expr2(expr_typecast_op, index, subtype);
 
       DATA_INVARIANT(
         index_expr1.type()==index_expr2.type(),
@@ -524,9 +520,8 @@ void arrayst::add_array_constraints(
   {
     DATA_INVARIANT(
       false,
-      ("unexpected array expression (add_array_constraints): '" +
-       expr.id_string() + "'")
-        .c_str());
+      "unexpected array expression (add_array_constraints): '" +
+        expr.id_string() + "'");
   }
 }
 

src/solvers/flattening/boolbv.cpp

@@ -97,7 +97,7 @@ bool boolbvt::literal(
         const typet &subtype = c.type();
 
         if(c.get_name() == component_name)
-          return literal(expr.op0(), bit+offset, dest);
+          return literal(member_expr.struct_op(), bit + offset, dest);
 
         std::size_t element_width=boolbv_width(subtype);
         CHECK_RETURN(element_width != 0);
@@ -190,7 +190,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   else if(expr.id()==ID_with)
     return convert_with(to_with_expr(expr));
   else if(expr.id()==ID_update)
-    return convert_update(expr);
+    return convert_update(to_update_expr(expr));
   else if(expr.id()==ID_width)
   {
     std::size_t result_width=boolbv_width(expr.type());
@@ -201,7 +201,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
     if(expr.operands().size()!=1)
       return conversion_failed(expr);
 
-    std::size_t op_width=boolbv_width(expr.op0().type());
+    std::size_t op_width = boolbv_width(to_unary_expr(expr).op().type());
 
     if(op_width==0)
       return conversion_failed(expr);
@@ -240,7 +240,9 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   else if(expr.id()==ID_floatbv_plus || expr.id()==ID_floatbv_minus ||
           expr.id()==ID_floatbv_mult || expr.id()==ID_floatbv_div ||
           expr.id()==ID_floatbv_rem)
-    return convert_floatbv_op(expr);
+  {
+    return convert_floatbv_op(to_ieee_float_op_expr(expr));
+  }
   else if(expr.id()==ID_floatbv_typecast)
     return convert_floatbv_typecast(to_floatbv_typecast_expr(expr));
   else if(expr.id()==ID_concatenation)
@@ -425,7 +427,6 @@ bvt boolbvt::convert_function_application(
 literalt boolbvt::convert_rest(const exprt &expr)
 {
   PRECONDITION(expr.type().id() == ID_bool);
-  const exprt::operandst &operands=expr.operands();
 
   if(expr.id()==ID_typecast)
     return convert_typecast(to_typecast_expr(expr));
@@ -436,15 +437,20 @@ literalt boolbvt::convert_rest(const exprt &expr)
     return convert_verilog_case_equality(to_binary_relation_expr(expr));
   else if(expr.id()==ID_notequal)
   {
-    DATA_INVARIANT(expr.operands().size() == 2, "notequal expects two operands");
-    return !convert_equality(equal_exprt(expr.op0(), expr.op1()));
+    const auto &notequal_expr = to_notequal_expr(expr);
+    return !convert_equality(
+      equal_exprt(notequal_expr.lhs(), notequal_expr.rhs()));
   }
   else if(expr.id()==ID_ieee_float_equal ||
           expr.id()==ID_ieee_float_notequal)
-    return convert_ieee_float_rel(expr);
+  {
+    return convert_ieee_float_rel(to_binary_relation_expr(expr));
+  }
   else if(expr.id()==ID_le || expr.id()==ID_ge ||
           expr.id()==ID_lt  || expr.id()==ID_gt)
-    return convert_bv_rel(expr);
+  {
+    return convert_bv_rel(to_binary_relation_expr(expr));
+  }
   else if(expr.id()==ID_extractbit)
     return convert_extractbit(to_extractbit_expr(expr));
   else if(expr.id()==ID_forall)
@@ -486,10 +492,10 @@ literalt boolbvt::convert_rest(const exprt &expr)
   }
   else if(expr.id()==ID_sign)
   {
-    DATA_INVARIANT(expr.operands().size() == 1, "sign expects one operand");
-    const bvt &bv=convert_bv(operands[0]);
+    const auto &op = to_sign_expr(expr).op();
+    const bvt &bv = convert_bv(op);
     CHECK_RETURN(!bv.empty());
-    const irep_idt type_id = operands[0].type().id();
+    const irep_idt type_id = op.type().id();
     if(type_id == ID_signedbv || type_id == ID_fixedbv || type_id == ID_floatbv)
       return bv[bv.size()-1];
     if(type_id == ID_unsignedbv)
@@ -505,53 +511,56 @@ literalt boolbvt::convert_rest(const exprt &expr)
     return convert_overflow(expr);
   else if(expr.id()==ID_isnan)
   {
-    DATA_INVARIANT(expr.operands().size() == 1, "isnan expects one operand");
-    const bvt &bv=convert_bv(operands[0]);
+    const auto &op = to_unary_expr(expr).op();
+    const bvt &bv = convert_bv(op);
 
-    if(expr.op0().type().id()==ID_floatbv)
+    if(op.type().id() == ID_floatbv)
     {
-      float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
+      float_utilst float_utils(prop, to_floatbv_type(op.type()));
       return float_utils.is_NaN(bv);
     }
-    else if(expr.op0().type().id() == ID_fixedbv)
+    else if(op.type().id() == ID_fixedbv)
       return const_literal(false);
   }
   else if(expr.id()==ID_isfinite)
   {
-    DATA_INVARIANT(expr.operands().size() == 1, "isfinite expects one operand");
-    const bvt &bv=convert_bv(operands[0]);
-    if(expr.op0().type().id()==ID_floatbv)
+    const auto &op = to_unary_expr(expr).op();
+    const bvt &bv = convert_bv(op);
+
+    if(op.type().id() == ID_floatbv)
     {
-      float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
+      float_utilst float_utils(prop, to_floatbv_type(op.type()));
       return prop.land(
         !float_utils.is_infinity(bv),
         !float_utils.is_NaN(bv));
     }
-    else if(expr.op0().type().id() == ID_fixedbv)
+    else if(op.id() == ID_fixedbv)
       return const_literal(true);
   }
   else if(expr.id()==ID_isinf)
   {
-    DATA_INVARIANT(expr.operands().size() == 1, "isinf expects one operand");
-    const bvt &bv=convert_bv(operands[0]);
-    if(expr.op0().type().id()==ID_floatbv)
+    const auto &op = to_unary_expr(expr).op();
+    const bvt &bv = convert_bv(op);
+
+    if(op.type().id() == ID_floatbv)
     {
-      float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
+      float_utilst float_utils(prop, to_floatbv_type(op.type()));
       return float_utils.is_infinity(bv);
     }
-    else if(expr.op0().type().id() == ID_fixedbv)
+    else if(op.type().id() == ID_fixedbv)
       return const_literal(false);
   }
   else if(expr.id()==ID_isnormal)
   {
-    DATA_INVARIANT(expr.operands().size() == 1, "isnormal expects one operand");
-    if(expr.op0().type().id()==ID_floatbv)
+    const auto &op = to_unary_expr(expr).op();
+
+    if(op.type().id() == ID_floatbv)
     {
-      const bvt &bv = convert_bv(operands[0]);
-      float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
+      const bvt &bv = convert_bv(op);
+      float_utilst float_utils(prop, to_floatbv_type(op.type()));
       return float_utils.is_normal(bv);
     }
-    else if(expr.op0().type().id() == ID_fixedbv)
+    else if(op.type().id() == ID_fixedbv)
       return const_literal(true);
   }
 

src/solvers/flattening/boolbv.h

@@ -124,7 +124,7 @@ class boolbvt:public arrayst
     const typet &src_type, const bvt &src,
     const typet &dest_type, bvt &dest);
 
-  virtual literalt convert_bv_rel(const exprt &expr);
+  virtual literalt convert_bv_rel(const binary_relation_exprt &);
   virtual literalt convert_typecast(const typecast_exprt &expr);
   virtual literalt convert_reduction(const unary_exprt &expr);
   virtual literalt convert_onehot(const unary_exprt &expr);
@@ -133,7 +133,7 @@ class boolbvt:public arrayst
   virtual literalt convert_equality(const equal_exprt &expr);
   virtual literalt convert_verilog_case_equality(
     const binary_relation_exprt &expr);
-  virtual literalt convert_ieee_float_rel(const exprt &expr);
+  virtual literalt convert_ieee_float_rel(const binary_relation_exprt &);
   virtual literalt convert_quantifier(const quantifier_exprt &expr);
 
   virtual bvt convert_index(const exprt &array, const mp_integer &index);
@@ -158,11 +158,11 @@ class boolbvt:public arrayst
   virtual bvt convert_mult(const mult_exprt &expr);
   virtual bvt convert_div(const div_exprt &expr);
   virtual bvt convert_mod(const mod_exprt &expr);
-  virtual bvt convert_floatbv_op(const exprt &expr);
+  virtual bvt convert_floatbv_op(const ieee_float_op_exprt &);
   virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr);
   virtual bvt convert_member(const member_exprt &expr);
   virtual bvt convert_with(const with_exprt &expr);
-  virtual bvt convert_update(const exprt &expr);
+  virtual bvt convert_update(const update_exprt &);
   virtual bvt convert_case(const exprt &expr);
   virtual bvt convert_cond(const cond_exprt &);
   virtual bvt convert_shift(const binary_exprt &expr);

src/solvers/flattening/boolbv_add_sub.cpp

@@ -41,7 +41,7 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
     !operands.empty(),
     "operator " + expr.id_string() + " takes at least one operand");
 
-  const exprt &op0=expr.op0();
+  const exprt &op0 = to_multi_ary_expr(expr).op0();
   DATA_INVARIANT(
     op0.type() == type, "add/sub with mixed types:\n" + expr.pretty());
 

src/solvers/flattening/boolbv_bitwise.cpp

@@ -17,9 +17,8 @@ bvt boolbvt::convert_bitwise(const exprt &expr)
 
   if(expr.id()==ID_bitnot)
   {
-    DATA_INVARIANT(expr.operands().size() == 1, "bitnot takes one operand");
-    const exprt &op0=expr.op0();
-    const bvt &op_bv = convert_bv(op0, width);
+    const exprt &op = to_bitnot_expr(expr).op();
+    const bvt &op_bv = convert_bv(op, width);
     return bv_utils.inverted(op_bv);
   }
   else if(expr.id()==ID_bitand || expr.id()==ID_bitor ||