Merge pull request #2933 from danpoe/refactor/error-handling-solvers-flattening-from-boolbv-map

Error handling cleanup in solvers/flattening 3

Author: tautschnig

src/solvers/flattening/boolbv.cpp

@@ -222,9 +222,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
           expr.id()=="no-overflow-plus" ||
           expr.id()=="no-overflow-minus")
     return convert_add_sub(expr);
-  else if(expr.id()==ID_mult ||
-          expr.id()=="no-overflow-mult")
-    return convert_mult(expr);
+  else if(expr.id() == ID_mult)
+    return convert_mult(to_mult_expr(expr));
   else if(expr.id()==ID_div)
     return convert_div(to_div_expr(expr));
   else if(expr.id()==ID_mod)

src/solvers/flattening/boolbv.h

@@ -152,7 +152,7 @@ class boolbvt:public arrayst
   virtual bvt convert_union(const union_exprt &expr);
   virtual bvt convert_bv_typecast(const typecast_exprt &expr);
   virtual bvt convert_add_sub(const exprt &expr);
-  virtual bvt convert_mult(const exprt &expr);
+  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);

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,18 @@ 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 +133,15 @@ 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();
@@ -43,22 +47,18 @@ bvt boolbvt::convert_member(const member_exprt &expr)
 
       if(c.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];
@@ -69,15 +69,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

@@ -10,7 +10,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/std_types.h>
 
-bvt boolbvt::convert_mult(const exprt &expr)
+bvt boolbvt::convert_mult(const mult_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
 
@@ -21,39 +21,32 @@ 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,33 +61,22 @@ 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);
-      else
-        bv=bv_utils.multiplier(bv, op, rep);
+      bv = bv_utils.multiplier(bv, op, rep);
     }
 
     return bv;

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,12 @@ 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,
+      "should be a onehot0 expression as other onehot expression kind has been "
+      "handled in other branch");
+    return !more_than_one_seen;
+  }
 }