Merge pull request #2934 from danpoe/refactor/error-handling-solvers-flattening-from-boolbv-quantifier

Error handling cleanup in solvers/flattening 4

Author: danpoe

src/solvers/flattening/boolbv.cpp

@@ -462,9 +462,9 @@ literalt boolbvt::convert_rest(const exprt &expr)
   else if(expr.id()==ID_extractbit)
     return convert_extractbit(to_extractbit_expr(expr));
   else if(expr.id()==ID_forall)
-    return convert_quantifier(expr);
+    return convert_quantifier(to_quantifier_expr(expr));
   else if(expr.id()==ID_exists)
-    return convert_quantifier(expr);
+    return convert_quantifier(to_quantifier_expr(expr));
   else if(expr.id()==ID_let)
   {
     bvt bv=convert_let(to_let_expr(expr));

src/solvers/flattening/boolbv.h

@@ -131,7 +131,7 @@ class boolbvt:public arrayst
   virtual literalt convert_verilog_case_equality(
     const binary_relation_exprt &expr);
   virtual literalt convert_ieee_float_rel(const exprt &expr);
-  virtual literalt convert_quantifier(const exprt &expr);
+  virtual literalt convert_quantifier(const quantifier_exprt &expr);
 
   virtual bvt convert_index(const exprt &array, const mp_integer &index);
   virtual bvt convert_index(const index_exprt &expr);

src/solvers/flattening/boolbv_quantifier.cpp

@@ -8,9 +8,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <cassert>
-
 #include <util/arith_tools.h>
+#include <util/invariant.h>
+#include <util/optional.h>
 #include <util/replace_expr.h>
 #include <util/simplify_expr.h>
 
@@ -32,8 +32,8 @@ exprt get_quantifier_var_min(
   const exprt &var_expr,
   const exprt &quantifier_expr)
 {
-  assert(quantifier_expr.id()==ID_or ||
-         quantifier_expr.id()==ID_and);
+  PRECONDITION(quantifier_expr.id() == ID_or || quantifier_expr.id() == ID_and);
+
   exprt res;
   res.make_false();
   if(quantifier_expr.id()==ID_or)
@@ -80,8 +80,7 @@ exprt get_quantifier_var_max(
   const exprt &var_expr,
   const exprt &quantifier_expr)
 {
-  assert(quantifier_expr.id()==ID_or ||
-         quantifier_expr.id()==ID_and);
+  PRECONDITION(quantifier_expr.id() == ID_or || quantifier_expr.id() == ID_and);
   exprt res;
   res.make_false();
   if(quantifier_expr.id()==ID_or)
@@ -137,78 +136,74 @@ exprt get_quantifier_var_max(
   return res;
 }
 
-bool instantiate_quantifier(exprt &expr,
-                            const namespacet &ns)
+optionalt<exprt>
+instantiate_quantifier(const quantifier_exprt &expr, const namespacet &ns)
 {
-  if(!(expr.id()==ID_forall || expr.id()==ID_exists))
-    return true;
-
-  assert(expr.operands().size()==2);
-  assert(expr.op0().id()==ID_symbol);
+  PRECONDITION(expr.id() == ID_forall || expr.id() == ID_exists);
 
-  exprt var_expr=expr.op0();
+  const symbol_exprt &var_expr = expr.symbol();
 
   /**
    * We need to rewrite the forall/exists quantifier into
    * an OR/AND expr.
    **/
-  exprt re(expr);
-  exprt tmp(re.op1());
-  re.swap(tmp);
-  re=simplify_expr(re, ns);
+
+  const exprt &re = simplify_expr(expr.where(), ns);
 
   if(re.is_true() || re.is_false())
   {
-    expr=re;
-    return true;
+    return re;
   }
 
-  exprt min_i=get_quantifier_var_min(var_expr, re);
-  exprt max_i=get_quantifier_var_max(var_expr, re);
-  exprt body_expr=re;
-  if(var_expr.is_false() ||
-     min_i.is_false() ||
-     max_i.is_false() ||
-     body_expr.is_false())
-    return false;
+  const exprt &min_i = get_quantifier_var_min(var_expr, re);
+  const exprt &max_i = get_quantifier_var_max(var_expr, re);
+
+  if(min_i.is_false() || max_i.is_false())
+    return nullopt;
 
-  mp_integer lb, ub;
-  to_integer(min_i, lb);
-  to_integer(max_i, ub);
+  mp_integer lb = numeric_cast_v<mp_integer>(min_i);
+  mp_integer ub = numeric_cast_v<mp_integer>(max_i);
 
   if(lb>ub)
-    return false;
+    return nullopt;
 
-  bool res=true;
   std::vector<exprt> expr_insts;
   for(mp_integer i=lb; i<=ub; ++i)
   {
-    exprt constraint_expr=body_expr;
+    exprt constraint_expr = re;
     replace_expr(var_expr,
                  from_integer(i, var_expr.type()),
                  constraint_expr);
     expr_insts.push_back(constraint_expr);
   }
+
   if(expr.id()==ID_forall)
   {
-    expr=conjunction(expr_insts);
+    return conjunction(expr_insts);
   }
-  if(expr.id()==ID_exists)
+  else if(expr.id() == ID_exists)
   {
-    expr=disjunction(expr_insts);
+    return disjunction(expr_insts);
   }
 
-  return res;
+  UNREACHABLE;
+  return nullopt;
 }
 
-literalt boolbvt::convert_quantifier(const exprt &src)
+literalt boolbvt::convert_quantifier(const quantifier_exprt &src)
 {
-  exprt expr(src);
-  if(!instantiate_quantifier(expr, ns))
+  PRECONDITION(src.id() == ID_forall || src.id() == ID_exists);
+
+  quantifier_exprt expr(src);
+  const auto res = instantiate_quantifier(expr, ns);
+
+  if(!res)
+  {
     return SUB::convert_rest(src);
+  }
 
   quantifiert quantifier;
-  quantifier.expr=expr;
+  quantifier.expr = *res;
   quantifier_list.push_back(quantifier);
 
   literalt l=prop.new_variable();

src/solvers/flattening/boolbv_reduction.cpp

@@ -13,8 +13,9 @@ literalt boolbvt::convert_reduction(const unary_exprt &expr)
 {
   const bvt &op_bv=convert_bv(expr.op());
 
-  if(op_bv.empty())
-    throw "reduction operators take one non-empty operand";
+  INVARIANT(
+    !op_bv.empty(),
+    "reduction operand bitvector shall have width at least one");
 
   enum { O_OR, O_AND, O_XOR } op;
 
@@ -27,7 +28,7 @@ literalt boolbvt::convert_reduction(const unary_exprt &expr)
   else if(id==ID_reduction_xor || id==ID_reduction_xnor)
     op=O_XOR;
   else
-    throw "unexpected reduction operator";
+    UNREACHABLE;
 
   literalt l=op_bv[0];
 
@@ -53,8 +54,9 @@ bvt boolbvt::convert_bv_reduction(const unary_exprt &expr)
 {
   const bvt &op_bv=convert_bv(expr.op());
 
-  if(op_bv.empty())
-    throw "reduction operators take one non-empty operand";
+  INVARIANT(
+    !op_bv.empty(),
+    "reduction operand bitvector shall have width at least one");
 
   enum { O_OR, O_AND, O_XOR } op;
 
@@ -67,7 +69,7 @@ bvt boolbvt::convert_bv_reduction(const unary_exprt &expr)
   else if(id==ID_reduction_xor || id==ID_reduction_xnor)
     op=O_XOR;
   else
-    throw "unexpected reduction operator";
+    UNREACHABLE;
 
   const typet &op_type=expr.op().type();
 

src/solvers/flattening/boolbv_replication.cpp

@@ -17,30 +17,29 @@ bvt boolbvt::convert_replication(const replication_exprt &expr)
   if(width==0)
     return conversion_failed(expr);
 
-  mp_integer times;
-  if(to_integer(expr.op0(), times))
-    throw "replication takes constant as first parameter";
+  mp_integer times = numeric_cast_v<mp_integer>(expr.times());
 
   bvt bv;
   bv.resize(width);
 
   const std::size_t u_times=integer2unsigned(times);
-  const bvt &op=convert_bv(expr.op1());
-  std::size_t offset=0;
+  const bvt &op = convert_bv(expr.op());
 
-  for(std::size_t i=0; i<u_times; i++)
-  {
-    if(op.size()+offset>width)
-      throw "replication operand width too big";
+  INVARIANT(
+    op.size() * u_times == bv.size(),
+    "result bitvector width shall be equal to the operand bitvector width times"
+    "the number of replications");
 
-    for(std::size_t i=0; i<op.size(); i++)
-      bv[i+offset]=op[i];
+  std::size_t bit_idx = 0;
 
-    offset+=op.size();
+  for(std::size_t i = 0; i < u_times; i++)
+  {
+    for(const auto &bit : op)
+    {
+      bv[bit_idx] = bit;
+      bit_idx++;
+    }
   }
 
-  if(offset!=bv.size())
-    throw "replication operand width too small";
-
   return bv;
 }

src/solvers/flattening/boolbv_shift.cpp

@@ -30,10 +30,7 @@ bvt boolbvt::convert_shift(const binary_exprt &expr)
   if(width==0)
     return conversion_failed(expr);
 
-  const bvt &op=convert_bv(expr.op0());
-
-  if(op.size()!=width)
-    throw "convert_shift: unexpected operand 0 width";
+  const bvt &op = convert_bv(expr.op0(), width);
 
   bv_utilst::shiftt shift;
 
@@ -48,15 +45,13 @@ bvt boolbvt::convert_shift(const binary_exprt &expr)
   else if(expr.id()==ID_ror)
     shift=bv_utilst::shiftt::ROTATE_RIGHT;
   else
-    throw "unexpected shift operator";
+    UNREACHABLE;
 
   // we allow a constant as shift distance
 
   if(expr.op1().is_constant())
   {
-    mp_integer i;
-    if(to_integer(expr.op1(), i))
-      throw "convert_shift: failed to convert constant";
+    mp_integer i = numeric_cast_v<mp_integer>(expr.op1());
 
     std::size_t distance;
 

src/solvers/flattening/boolbv_struct.cpp

@@ -19,53 +19,52 @@ bvt boolbvt::convert_struct(const struct_exprt &expr)
 
   const struct_typet::componentst &components=struct_type.components();
 
-  if(expr.operands().size()!=components.size())
-  {
-    error().source_location=expr.find_source_location();
-    error() << "struct: wrong number of arguments" << eom;
-    throw 0;
-  }
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    expr.operands().size() == components.size(),
+    "number of operands of a struct expression shall equal the number of"
+    "components as indicated by its type",
+    expr.find_source_location());
 
   bvt bv;
   bv.resize(width);
 
-  std::size_t offset=0;
+  std::size_t bit_idx = 0;
 
   exprt::operandst::const_iterator op_it=expr.operands().begin();
   for(const auto &comp : components)
   {
     const typet &subtype=comp.type();
     const exprt &op=*op_it;
 
-    if(!base_type_eq(subtype, op.type(), ns))
-    {
-      error().source_location=expr.find_source_location();
-      error() << "struct: component type does not match: "
-              << subtype.pretty() << " vs. "
-              << op.type().pretty() << eom;
-      throw 0;
-    }
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
+      base_type_eq(subtype, op.type(), ns),
+      "type of a struct expression operand shall equal the type of the "
+      "corresponding struct component",
+      expr.find_source_location(),
+      subtype.pretty(),
+      op.type().pretty());
 
     std::size_t subtype_width=boolbv_width(subtype);
 
     if(subtype_width!=0)
     {
-      const bvt &op_bv=convert_bv(op);
-
-      assert(offset<width);
-      assert(op_bv.size()==subtype_width);
-      assert(offset+op_bv.size()<=width);
+      const bvt &op_bv = convert_bv(op, subtype_width);
 
-      for(std::size_t j=0; j<op_bv.size(); j++)
-        bv[offset+j]=op_bv[j];
+      INVARIANT(
+        bit_idx + op_bv.size() <= width, "bit index shall be within bounds");
 
-      offset+=op_bv.size();
+      for(const auto &bit : op_bv)
+      {
+        bv[bit_idx] = bit;
+        bit_idx++;
+      }
     }
 
     ++op_it;
   }
 
-  assert(offset==width);
+  INVARIANT(
+    bit_idx == width, "all bits in the bitvector shall have been assigned");
 
   return bv;
 }