From eb194ca2491ab5ff8138f9cdd7209bd3890cfb21 Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Tue, 11 Sep 2018 16:50:33 +0100
Subject: [PATCH 1/2] Error handling cleanup in solvers/flattening

Files boolbv_quantifier.cpp to boolbv_typecast.cpp
---
 src/solvers/flattening/boolbv_quantifier.cpp  | 23 +++++----
 src/solvers/flattening/boolbv_reduction.cpp   | 14 +++---
 src/solvers/flattening/boolbv_replication.cpp | 29 ++++++------
 src/solvers/flattening/boolbv_shift.cpp       | 11 ++---
 src/solvers/flattening/boolbv_struct.cpp      | 47 +++++++++----------
 src/solvers/flattening/boolbv_typecast.cpp    | 43 +++++++++++------
 src/util/std_expr.h                           |  4 ++
 7 files changed, 93 insertions(+), 78 deletions(-)

diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp
index 23f8857f80d..d079621f014 100644
--- a/src/solvers/flattening/boolbv_quantifier.cpp
+++ b/src/solvers/flattening/boolbv_quantifier.cpp
@@ -8,9 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv.h"
 
-#include <cassert>
-
 #include <util/arith_tools.h>
+#include <util/invariant.h>
 #include <util/replace_expr.h>
 #include <util/simplify_expr.h>
 
@@ -32,8 +31,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 +79,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)
@@ -140,11 +138,14 @@ exprt get_quantifier_var_max(
 bool instantiate_quantifier(exprt &expr,
                             const namespacet &ns)
 {
-  if(!(expr.id()==ID_forall || expr.id()==ID_exists))
-    return true;
+  PRECONDITION(expr.id() == ID_forall || expr.id() == ID_exists);
 
-  assert(expr.operands().size()==2);
-  assert(expr.op0().id()==ID_symbol);
+  DATA_INVARIANT(
+    expr.operands().size() == 2,
+    "quantifier expressions shall have two operands");
+
+  DATA_INVARIANT(
+    expr.op0().id() == ID_symbol, "quantified variable shall be a symbol");
 
   exprt var_expr=expr.op0();
 
@@ -203,6 +204,8 @@ bool instantiate_quantifier(exprt &expr,
 
 literalt boolbvt::convert_quantifier(const exprt &src)
 {
+  PRECONDITION(src.id() == ID_forall || src.id() == ID_exists);
+
   exprt expr(src);
   if(!instantiate_quantifier(expr, ns))
     return SUB::convert_rest(src);
diff --git a/src/solvers/flattening/boolbv_reduction.cpp b/src/solvers/flattening/boolbv_reduction.cpp
index 056f5d05676..ff825f569bd 100644
--- a/src/solvers/flattening/boolbv_reduction.cpp
+++ b/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();
 
diff --git a/src/solvers/flattening/boolbv_replication.cpp b/src/solvers/flattening/boolbv_replication.cpp
index c7368cc1830..c1e8c7068fb 100644
--- a/src/solvers/flattening/boolbv_replication.cpp
+++ b/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;
 }
diff --git a/src/solvers/flattening/boolbv_shift.cpp b/src/solvers/flattening/boolbv_shift.cpp
index be75dce3ef7..d66c9f41e62 100644
--- a/src/solvers/flattening/boolbv_shift.cpp
+++ b/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;
 
diff --git a/src/solvers/flattening/boolbv_struct.cpp b/src/solvers/flattening/boolbv_struct.cpp
index e1dbe90601f..e5a589b915c 100644
--- a/src/solvers/flattening/boolbv_struct.cpp
+++ b/src/solvers/flattening/boolbv_struct.cpp
@@ -19,17 +19,16 @@ 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)
@@ -37,35 +36,35 @@ bvt boolbvt::convert_struct(const struct_exprt &expr)
     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;
 }
diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp
index 724b59b6a78..1260579384d 100644
--- a/src/solvers/flattening/boolbv_typecast.cpp
+++ b/src/solvers/flattening/boolbv_typecast.cpp
@@ -93,7 +93,10 @@ bool boolbvt::type_conversion(
         upper,
         ns.follow(dest_type.subtype()),
         upper_res);
-      assert(lower_res.size()+upper_res.size()==dest_width);
+      INVARIANT(
+        lower_res.size() + upper_res.size() == dest_width,
+        "lower result bitvector size plus upper result bitvector size shall "
+        "equal the destination bitvector size");
       dest=lower_res;
       dest.insert(dest.end(), upper_res.begin(), upper_res.end());
       return false;
@@ -102,7 +105,10 @@ bool boolbvt::type_conversion(
 
   if(src_type.id()==ID_complex)
   {
-    assert(dest_type.id()!=ID_complex);
+    INVARIANT(
+      dest_type.id() == ID_complex,
+      "destination type shall be of complex type when source type is of "
+      "complex type");
     if(dest_type.id()==ID_signedbv ||
        dest_type.id()==ID_unsignedbv ||
        dest_type.id()==ID_floatbv ||
@@ -187,7 +193,9 @@ bool boolbvt::type_conversion(
         return false;
 
       case bvtypet::IS_BV:
-        assert(src_width==dest_width);
+        INVARIANT(
+          src_width == dest_width,
+          "source bitvector size shall equal the destination bitvector size");
         dest=src;
         return false;
 
@@ -202,7 +210,8 @@ bool boolbvt::type_conversion(
 
           dest=convert_bv(f.to_expr());
 
-          assert(src_width==1);
+          INVARIANT(
+            src_width == 1, "bitvector of type boolean shall have width one");
 
           Forall_literals(it, dest)
             *it=prop.land(*it, src[0]);
@@ -245,7 +254,7 @@ bool boolbvt::type_conversion(
       {
         // position in bv
         std::size_t p=dest_fraction_bits+i;
-        assert(p<dest_width);
+        INVARIANT(p < dest_width, "bit index shall be within bounds");
 
         if(i<op_int_bits)
           dest[p]=src[i+op_fraction_bits];
@@ -257,7 +266,9 @@ bool boolbvt::type_conversion(
     }
     else if(src_bvtype==bvtypet::IS_BV)
     {
-      assert(src_width==dest_width);
+      INVARIANT(
+        src_width == dest_width,
+        "source bitvector with shall equal the destination bitvector width");
       dest=src;
       return false;
     }
@@ -299,7 +310,8 @@ bool boolbvt::type_conversion(
       std::size_t fraction_bits=
         to_fixedbv_type(dest_type).get_fraction_bits();
 
-      assert(src_width==1);
+      INVARIANT(
+        src_width == 1, "bitvector of type boolean shall have width one");
 
       for(std::size_t i=0; i<dest_width; i++)
       {
@@ -416,7 +428,8 @@ bool boolbvt::type_conversion(
       {
         // bool to integer
 
-        assert(src_width==1);
+        INVARIANT(
+          src_width == 1, "bitvector of type boolean shall have width one");
 
         for(std::size_t i=0; i<dest_width; i++)
         {
@@ -483,7 +496,9 @@ bool boolbvt::type_conversion(
     break;
 
   case bvtypet::IS_BV:
-    assert(src_width==dest_width);
+    INVARIANT(
+      src_width == dest_width,
+      "source bitvector width shall equal the destination bitvector width");
     dest=src;
     return false;
 
@@ -590,12 +605,10 @@ bool boolbvt::type_conversion(
 /// conversion from bitvector types to boolean
 literalt boolbvt::convert_typecast(const typecast_exprt &expr)
 {
-  assert(expr.operands().size()==1);
-
-  if(expr.op0().type().id()==ID_range)
+  if(expr.op().type().id() == ID_range)
   {
-    mp_integer from=string2integer(expr.op0().type().get_string(ID_from));
-    mp_integer to=string2integer(expr.op0().type().get_string(ID_to));
+    mp_integer from = string2integer(expr.op().type().get_string(ID_from));
+    mp_integer to = string2integer(expr.op().type().get_string(ID_to));
 
     if(from==1 && to==1)
       return const_literal(true);
@@ -603,7 +616,7 @@ literalt boolbvt::convert_typecast(const typecast_exprt &expr)
       return const_literal(false);
   }
 
-  const bvt &bv=convert_bv(expr.op0());
+  const bvt &bv = convert_bv(expr.op());
 
   if(!bv.empty())
     return prop.lor(bv);
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index 8fb40b52609..68cc8f5813f 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -4585,6 +4585,8 @@ inline const quantifier_exprt &to_quantifier_expr(const exprt &expr)
 {
   DATA_INVARIANT(expr.operands().size()==2,
                  "quantifier expressions must have two operands");
+  DATA_INVARIANT(
+    expr.op0().id() == ID_symbol, "quantified variable shall be a symbol");
   return static_cast<const quantifier_exprt &>(expr);
 }
 
@@ -4593,6 +4595,8 @@ inline quantifier_exprt &to_quantifier_expr(exprt &expr)
 {
   DATA_INVARIANT(expr.operands().size()==2,
                  "quantifier expressions must have two operands");
+  DATA_INVARIANT(
+    expr.op0().id() == ID_symbol, "quantified variable shall be a symbol");
   return static_cast<quantifier_exprt &>(expr);
 }
 

From 44503dd06cfa6f08826298d058cd0115365e8384 Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Mon, 24 Sep 2018 20:04:57 +0100
Subject: [PATCH 2/2] Refactor quantifier instantiation in solvers/flattening

---
 src/solvers/flattening/boolbv.cpp            |  4 +-
 src/solvers/flattening/boolbv.h              |  2 +-
 src/solvers/flattening/boolbv_quantifier.cpp | 68 +++++++++-----------
 3 files changed, 33 insertions(+), 41 deletions(-)

diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index 53f1cdcb44e..f3661a3334b 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -463,9 +463,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));
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
index c51f3a3803b..af925e1e437 100644
--- a/src/solvers/flattening/boolbv.h
+++ b/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);
diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp
index d079621f014..1e3dfd55550 100644
--- a/src/solvers/flattening/boolbv_quantifier.cpp
+++ b/src/solvers/flattening/boolbv_quantifier.cpp
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/invariant.h>
+#include <util/optional.h>
 #include <util/replace_expr.h>
 #include <util/simplify_expr.h>
 
@@ -135,83 +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)
 {
   PRECONDITION(expr.id() == ID_forall || expr.id() == ID_exists);
 
-  DATA_INVARIANT(
-    expr.operands().size() == 2,
-    "quantifier expressions shall have two operands");
-
-  DATA_INVARIANT(
-    expr.op0().id() == ID_symbol, "quantified variable shall be a symbol");
-
-  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);
 
-  mp_integer lb, ub;
-  to_integer(min_i, lb);
-  to_integer(max_i, ub);
+  if(min_i.is_false() || max_i.is_false())
+    return nullopt;
+
+  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)
 {
   PRECONDITION(src.id() == ID_forall || src.id() == ID_exists);
 
-  exprt expr(src);
-  if(!instantiate_quantifier(expr, ns))
+  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();