Error handling cleanup in solvers/flattening

Files boolbv_map.cpp to boolbv_overflow.cpp

Author: danpoe

src/solvers/flattening/boolbv_map.cpp

@@ -67,7 +67,9 @@ boolbv_mapt::map_entryt &boolbv_mapt::get_map_entry(
     map_entry.literal_map.resize(map_entry.width);
   }
 
-  assert(map_entry.literal_map.size()==map_entry.width);
+  INVARIANT(
+    map_entry.literal_map.size() == map_entry.width,
+    "number of literals in the literal map shall equal the bitvector width");
 
   return map_entry;
 }
@@ -89,15 +91,19 @@ void boolbv_mapt::get_literals(
 {
   map_entryt &map_entry=get_map_entry(identifier, type);
 
-  assert(literals.size()==width);
-  assert(map_entry.literal_map.size()==width);
+  PRECONDITION(literals.size() == width);
+  INVARIANT(
+    map_entry.literal_map.size() == width,
+    "number of literals in the literal map shall equal the bitvector width");
 
   Forall_literals(it, literals)
   {
     literalt &l=*it;
     const std::size_t bit=it-literals.begin();
 
-    assert(bit<map_entry.literal_map.size());
+    INVARIANT(
+      bit < map_entry.literal_map.size(),
+      "bit index shall be within bounds");
     map_bitt &mb=map_entry.literal_map[bit];
 
     if(mb.is_set)
@@ -128,12 +134,16 @@ void boolbv_mapt::set_literals(
   forall_literals(it, literals)
   {
     const literalt &literal=*it;
-    const std::size_t bit=it-literals.begin();
 
-    assert(literal.is_constant() ||
-           literal.var_no()<prop.no_variables());
+    INVARIANT(
+      literal.is_constant() || literal.var_no() < prop.no_variables(),
+      "variable number of non-constant literals shall be within bounds");
+
+    const std::size_t bit=it-literals.begin();
 
-    assert(bit<map_entry.literal_map.size());
+    INVARIANT(
+      bit < map_entry.literal_map.size(),
+      "bit index shall be within bounds");
     map_bitt &mb=map_entry.literal_map[bit];
 
     if(mb.is_set)

src/solvers/flattening/boolbv_member.cpp

@@ -28,8 +28,12 @@ bvt boolbvt::convert_member(const member_exprt &expr)
                          from_integer(0, index_type()),
                          expr.type()));
   }
-  else if(struct_op_type.id()==ID_struct)
+  else
   {
+    INVARIANT(
+      struct_op_type.id() == ID_struct,
+      "member_exprt should denote access to a union or struct");
+
     const irep_idt &component_name=expr.get_component_name();
     const struct_typet::componentst &components=
       to_struct_type(struct_op_type).components();
@@ -46,22 +50,18 @@ bvt boolbvt::convert_member(const member_exprt &expr)
 
       if(it->get_name()==component_name)
       {
-        if(!base_type_eq(subtype, expr.type(), ns))
-        {
-          #if 0
-          std::cout << "DEBUG " << expr.pretty() << "\n";
-          #endif
-
-          error().source_location=expr.find_source_location();
-          error() << "member: component type does not match: "
-                  << subtype.pretty() << " vs. "
-                  << expr.type().pretty() << eom;
-          throw 0;
-        }
+        DATA_INVARIANT_WITH_DIAGNOSTICS(
+          base_type_eq(subtype, expr.type(), ns),
+          "struct component type shall match the member expression type",
+          subtype.pretty(),
+          expr.type().pretty());
 
         bvt bv;
         bv.resize(sub_width);
-        assert(offset+sub_width<=struct_bv.size());
+        INVARIANT(
+          offset + sub_width <= struct_bv.size(),
+          "bitvector part corresponding to struct element shall be contained "
+          "within the full struct bitvector");
 
         for(std::size_t i=0; i<sub_width; i++)
           bv[i]=struct_bv[offset+i];
@@ -72,15 +72,10 @@ bvt boolbvt::convert_member(const member_exprt &expr)
       offset+=sub_width;
     }
 
-    error().source_location=expr.find_source_location();
-    error() << "component " << component_name
-            << " not found in structure" << eom;
-    throw 0;
-  }
-  else
-  {
-    error().source_location=expr.find_source_location();
-    error() << "member takes struct or union operand" << eom;
-    throw 0;
+    INVARIANT_WITH_DIAGNOSTICS(
+      false,
+      "struct type shall contain component accessed by member expression",
+      expr.find_source_location(),
+      id2string(component_name));
   }
 }

src/solvers/flattening/boolbv_mod.cpp

@@ -27,20 +27,22 @@ bvt boolbvt::convert_mod(const mod_exprt &expr)
   if(width==0)
     return conversion_failed(expr);
 
-  if(expr.op0().type().id()!=expr.type().id() ||
-     expr.op1().type().id()!=expr.type().id())
-    throw "mod got mixed-type operands";
+  DATA_INVARIANT(
+    expr.op0().type().id() == expr.type().id(),
+    "type of the first operand of a modulo operation shall equal the "
+    "expression type");
+
+  DATA_INVARIANT(
+    expr.op1().type().id() == expr.type().id(),
+    "type of the second operand of a modulo operation shall equal the "
+    "expression type");
 
   bv_utilst::representationt rep=
     expr.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
                                   bv_utilst::representationt::UNSIGNED;
 
-  const bvt &op0=convert_bv(expr.op0());
-  const bvt &op1=convert_bv(expr.op1());
-
-  if(op0.size()!=width ||
-     op1.size()!=width)
-    throw "convert_mod: unexpected operand width";
+  const bvt &op0 = convert_bv(expr.op0(), width);
+  const bvt &op1 = convert_bv(expr.op1(), width);
 
   bvt res, rem;
 

src/solvers/flattening/boolbv_mult.cpp

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 
 bvt boolbvt::convert_mult(const exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_mult || expr.id() == "no-overflow-mult");
+
   std::size_t width=boolbv_width(expr.type());
 
   if(width==0)
@@ -21,39 +23,36 @@ bvt boolbvt::convert_mult(const exprt &expr)
   bv.resize(width);
 
   const exprt::operandst &operands=expr.operands();
-  if(operands.empty())
-    throw "mult without operands";
+  DATA_INVARIANT(
+    !operands.empty(),
+    "multiplication must have operands");
 
   const exprt &op0=expr.op0();
 
   bool no_overflow=expr.id()=="no-overflow-mult";
 
+  DATA_INVARIANT(
+    op0->type() == expr.type(),
+    "multiplication operands should have same type as expression");
+
   if(expr.type().id()==ID_fixedbv)
   {
-    if(op0.type()!=expr.type())
-      throw "multiplication with mixed types";
-
-    bv=convert_bv(op0);
-
-    if(bv.size()!=width)
-      throw "convert_mult: unexpected operand width";
+    bv = convert_bv(op0, width);
 
     std::size_t fraction_bits=
       to_fixedbv_type(expr.type()).get_fraction_bits();
 
     for(exprt::operandst::const_iterator it=operands.begin()+1;
         it!=operands.end(); it++)
     {
-      if(it->type()!=expr.type())
-        throw "multiplication with mixed types";
+      DATA_INVARIANT(
+        it->type() == expr.type(),
+        "multiplication operands should have same type as expression");
 
       // do a sign extension by fraction_bits bits
       bv=bv_utils.sign_extension(bv, bv.size()+fraction_bits);
 
-      bvt op=convert_bv(*it);
-
-      if(op.size()!=width)
-        throw "convert_mult: unexpected operand width";
+      bvt op=convert_bv(*it, width);
 
       op=bv_utils.sign_extension(op, bv.size());
 
@@ -68,28 +67,20 @@ bvt boolbvt::convert_mult(const exprt &expr)
   else if(expr.type().id()==ID_unsignedbv ||
           expr.type().id()==ID_signedbv)
   {
-    if(op0.type()!=expr.type())
-      throw "multiplication with mixed types";
-
     bv_utilst::representationt rep=
       expr.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
                                     bv_utilst::representationt::UNSIGNED;
 
-    bv=convert_bv(op0);
-
-    if(bv.size()!=width)
-      throw "convert_mult: unexpected operand width";
+    bv = convert_bv(op0, width);
 
     for(exprt::operandst::const_iterator it=operands.begin()+1;
         it!=operands.end(); it++)
     {
-      if(it->type()!=expr.type())
-        throw "multiplication with mixed types";
-
-      const bvt &op=convert_bv(*it);
+      DATA_INVARIANT(
+        it->type() == expr.type(),
+        "multiplication operands should have same type as expression");
 
-      if(op.size()!=width)
-        throw "convert_mult: unexpected operand width";
+      const bvt &op=convert_bv(*it, width);
 
       if(no_overflow)
         bv=bv_utils.multiplier_no_overflow(bv, op, rep);

src/solvers/flattening/boolbv_not.cpp

@@ -12,9 +12,7 @@ Author: Daniel Kroening, [email protected]
 bvt boolbvt::convert_not(const not_exprt &expr)
 {
   const bvt &op_bv=convert_bv(expr.op());
-
-  if(op_bv.empty())
-    throw "not operator takes one non-empty operand";
+  CHECK_RETURN(!op_bv.empty());
 
   const typet &op_type=expr.op().type();
 

src/solvers/flattening/boolbv_onehot.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 literalt boolbvt::convert_onehot(const unary_exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_onehot || expr.id() == ID_onehot0);
+
   bvt op=convert_bv(expr.op());
 
   literalt one_seen=const_literal(false);
@@ -25,8 +27,9 @@ literalt boolbvt::convert_onehot(const unary_exprt &expr)
 
   if(expr.id()==ID_onehot)
     return prop.land(one_seen, !more_than_one_seen);
-  else if(expr.id()==ID_onehot0)
-    return !more_than_one_seen;
   else
-    throw "unexpected onehot expression";
+  {
+    INVARIANT(expr.id() == ID_onehot0, "");
+    return !more_than_one_seen;
+  }
 }

src/solvers/flattening/boolbv_overflow.cpp

@@ -19,8 +19,9 @@ literalt boolbvt::convert_overflow(const exprt &expr)
   if(expr.id()==ID_overflow_plus ||
      expr.id()==ID_overflow_minus)
   {
-    if(operands.size()!=2)
-      throw "operator "+expr.id_string()+" takes two operands";
+    DATA_INVARIANT(
+      operands.size() == 2,
+      "expression " + expr.id_string() + " should have two operands");
 
     const bvt &bv0=convert_bv(operands[0]);
     const bvt &bv1=convert_bv(operands[1]);
@@ -38,27 +39,25 @@ literalt boolbvt::convert_overflow(const exprt &expr)
   }
   else if(expr.id()==ID_overflow_mult)
   {
-    if(operands.size()!=2)
-      throw "operator "+expr.id_string()+" takes two operands";
+    DATA_INVARIANT(
+      operands.size() == 2,
+      "overflow_mult expression should have two operands");
 
     if(operands[0].type().id()!=ID_unsignedbv &&
        operands[0].type().id()!=ID_signedbv)
       return SUB::convert_rest(expr);
 
     bvt bv0=convert_bv(operands[0]);
-    bvt bv1=convert_bv(operands[1]);
-
-    if(bv0.size()!=bv1.size())
-      throw "operand size mismatch on overflow-*";
+    bvt bv1=convert_bv(operands[1], bv0.size());
 
     bv_utilst::representationt rep=
       operands[0].type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
                                            bv_utilst::representationt::UNSIGNED;
 
-    if(operands[0].type()!=operands[1].type())
-      throw "operand type mismatch on overflow-*";
+    DATA_INVARIANT(
+      operands[0].type() == operands[1].type(),
+      "operands of overflow_mult expression shall have same type");
 
-    DATA_INVARIANT(bv0.size()==bv1.size(), "operands size mismatch");
     std::size_t old_size=bv0.size();
     std::size_t new_size=old_size*2;
 
@@ -97,8 +96,9 @@ literalt boolbvt::convert_overflow(const exprt &expr)
   }
   else if(expr.id() == ID_overflow_shl)
   {
-    if(operands.size() != 2)
-      throw "operator " + expr.id_string() + " takes two operands";
+    DATA_INVARIANT(
+      operands.size() == 2,
+      "overflow_shl expression should have two operands");
 
     const bvt &bv0=convert_bv(operands[0]);
     const bvt &bv1=convert_bv(operands[1]);
@@ -163,8 +163,9 @@ literalt boolbvt::convert_overflow(const exprt &expr)
   }
   else if(expr.id()==ID_overflow_unary_minus)
   {
-    if(operands.size()!=1)
-      throw "operator "+expr.id_string()+" takes one operand";
+    DATA_INVARIANT(
+      operands.size() == 1,
+      "overflow_unary_minus expression should have one operand");
 
     const bvt &bv=convert_bv(operands[0]);
 
@@ -173,18 +174,23 @@ literalt boolbvt::convert_overflow(const exprt &expr)
   else if(has_prefix(expr.id_string(), "overflow-typecast-"))
   {
     std::size_t bits=unsafe_string2unsigned(id2string(expr.id()).substr(18));
+    INVARIANT(
+      bits != 0,
+      "");
 
     const exprt::operandst &operands=expr.operands();
 
-    if(operands.size()!=1)
-      throw "operator "+expr.id_string()+" takes one operand";
+    DATA_INVARIANT(
+      operands.size() == 1,
+      "expression " + expr.id_string() + " should have one operand");
 
     const exprt &op=operands[0];
 
     const bvt &bv=convert_bv(op);
 
-    if(bits>=bv.size() || bits==0)
-      throw "overflow-typecast got wrong number of bits";
+    INVARIANT(
+      bits < bv.size(),
+      "");
 
     // signed or unsigned?
     if(op.type().id()==ID_signedbv)