From d6017bdf463c39c8134c3356df7474a70ac836cd Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@cs.ox.ac.uk>
Date: Mon, 10 Sep 2018 19:48:26 +0100
Subject: [PATCH 1/3] Error handling cleanup in solvers/flattening

Files boolbv_map.cpp to boolbv_overflow.cpp
---
 src/solvers/flattening/boolbv_map.cpp      | 24 ++++++++----
 src/solvers/flattening/boolbv_member.cpp   | 43 +++++++++------------
 src/solvers/flattening/boolbv_mod.cpp      | 20 +++++-----
 src/solvers/flattening/boolbv_mult.cpp     | 45 ++++++++--------------
 src/solvers/flattening/boolbv_not.cpp      |  4 +-
 src/solvers/flattening/boolbv_onehot.cpp   | 12 ++++--
 src/solvers/flattening/boolbv_overflow.cpp | 39 ++++++++++---------
 7 files changed, 93 insertions(+), 94 deletions(-)

diff --git a/src/solvers/flattening/boolbv_map.cpp b/src/solvers/flattening/boolbv_map.cpp
index fd12b81ebd7..ab90f63a873 100644
--- a/src/solvers/flattening/boolbv_map.cpp
+++ b/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)
diff --git a/src/solvers/flattening/boolbv_member.cpp b/src/solvers/flattening/boolbv_member.cpp
index e6dbf1c0b5f..9c41aa3c37a 100644
--- a/src/solvers/flattening/boolbv_member.cpp
+++ b/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));
   }
 }
diff --git a/src/solvers/flattening/boolbv_mod.cpp b/src/solvers/flattening/boolbv_mod.cpp
index 1692fbc6a2f..c4a846dba65 100644
--- a/src/solvers/flattening/boolbv_mod.cpp
+++ b/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;
 
diff --git a/src/solvers/flattening/boolbv_mult.cpp b/src/solvers/flattening/boolbv_mult.cpp
index 15803b7ead5..b626d9c0bde 100644
--- a/src/solvers/flattening/boolbv_mult.cpp
+++ b/src/solvers/flattening/boolbv_mult.cpp
@@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 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,22 +23,19 @@ 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();
@@ -44,16 +43,14 @@ bvt boolbvt::convert_mult(const exprt &expr)
     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 +65,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);
diff --git a/src/solvers/flattening/boolbv_not.cpp b/src/solvers/flattening/boolbv_not.cpp
index d57cb1e9dff..039707a1acb 100644
--- a/src/solvers/flattening/boolbv_not.cpp
+++ b/src/solvers/flattening/boolbv_not.cpp
@@ -12,9 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 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();
 
diff --git a/src/solvers/flattening/boolbv_onehot.cpp b/src/solvers/flattening/boolbv_onehot.cpp
index 168185e00f8..78d5a126d7b 100644
--- a/src/solvers/flattening/boolbv_onehot.cpp
+++ b/src/solvers/flattening/boolbv_onehot.cpp
@@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 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;
+  }
 }
diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp
index f7e4798f780..20f3c138fdc 100644
--- a/src/solvers/flattening/boolbv_overflow.cpp
+++ b/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,8 @@ 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 +162,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 +173,19 @@ 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)

From baa45f1de03d097387e17c6cab5b09d010bd33d6 Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Fri, 21 Sep 2018 12:02:12 +0100
Subject: [PATCH 2/3] Remove "no-overflow-mult" expression

---
 src/solvers/flattening/boolbv.cpp            |  5 ++---
 src/solvers/flattening/boolbv.h              |  2 +-
 src/solvers/flattening/boolbv_mult.cpp       | 11 ++---------
 src/solvers/refinement/bv_refinement.h       |  2 +-
 src/solvers/refinement/refine_arithmetic.cpp |  4 ++--
 5 files changed, 8 insertions(+), 16 deletions(-)

diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index 53f1cdcb44e..ea001385f9b 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -224,9 +224,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)
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
index c51f3a3803b..ffcce81c9da 100644
--- a/src/solvers/flattening/boolbv.h
+++ b/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);
diff --git a/src/solvers/flattening/boolbv_mult.cpp b/src/solvers/flattening/boolbv_mult.cpp
index b626d9c0bde..6c5fc553789 100644
--- a/src/solvers/flattening/boolbv_mult.cpp
+++ b/src/solvers/flattening/boolbv_mult.cpp
@@ -10,10 +10,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/std_types.h>
 
-bvt boolbvt::convert_mult(const exprt &expr)
+bvt boolbvt::convert_mult(const mult_exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_mult || expr.id() == "no-overflow-mult");
-
   std::size_t width=boolbv_width(expr.type());
 
   if(width==0)
@@ -27,8 +25,6 @@ bvt boolbvt::convert_mult(const exprt &expr)
 
   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");
@@ -80,10 +76,7 @@ bvt boolbvt::convert_mult(const exprt &expr)
 
       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;
diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h
index b371a9feda8..29c265b3c42 100644
--- a/src/solvers/refinement/bv_refinement.h
+++ b/src/solvers/refinement/bv_refinement.h
@@ -51,7 +51,7 @@ class bv_refinementt:public bv_pointerst
   void post_process_arrays() override;
 
   // Refine arithmetic
-  bvt convert_mult(const exprt &expr) override;
+  bvt convert_mult(const mult_exprt &expr) override;
   bvt convert_div(const div_exprt &expr) override;
   bvt convert_mod(const mod_exprt &expr) override;
   bvt convert_floatbv_op(const exprt &expr) override;
diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp
index 86641b8ffa4..0dc3673be39 100644
--- a/src/solvers/refinement/refine_arithmetic.cpp
+++ b/src/solvers/refinement/refine_arithmetic.cpp
@@ -50,7 +50,7 @@ bvt bv_refinementt::convert_floatbv_op(const exprt &expr)
   return bv;
 }
 
-bvt bv_refinementt::convert_mult(const exprt &expr)
+bvt bv_refinementt::convert_mult(const mult_exprt &expr)
 {
   if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
     return SUB::convert_mult(expr);
@@ -65,7 +65,7 @@ bvt bv_refinementt::convert_mult(const exprt &expr)
   PRECONDITION(operands.size()>=2);
 
   if(operands.size()>2)
-    return convert_mult(make_binary(expr)); // make binary
+    return convert_mult(to_mult_expr(make_binary(expr))); // make binary
 
   // we keep multiplication by a constant for integers
   if(type.id()!=ID_floatbv)

From d57737aff1745ef5d48fcf97f7f4b4e30ea39b51 Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Fri, 21 Sep 2018 12:04:59 +0100
Subject: [PATCH 3/3] Remove "overflow-typecast-*" expression

---
 src/solvers/flattening/boolbv_overflow.cpp | 35 ----------------------
 1 file changed, 35 deletions(-)

diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp
index 20f3c138fdc..01e4672739d 100644
--- a/src/solvers/flattening/boolbv_overflow.cpp
+++ b/src/solvers/flattening/boolbv_overflow.cpp
@@ -170,41 +170,6 @@ literalt boolbvt::convert_overflow(const exprt &expr)
 
     return bv_utils.overflow_negate(bv);
   }
-  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();
-
-    DATA_INVARIANT(
-      operands.size() == 1,
-      "expression " + expr.id_string() + " should have one operand");
-
-    const exprt &op=operands[0];
-
-    const bvt &bv=convert_bv(op);
-
-    INVARIANT(bits < bv.size(), "");
-
-    // signed or unsigned?
-    if(op.type().id()==ID_signedbv)
-    {
-      bvt tmp_bv;
-      for(std::size_t i=bits; i<bv.size(); i++)
-        tmp_bv.push_back(prop.lxor(bv[bits-1], bv[i]));
-
-      return prop.lor(tmp_bv);
-    }
-    else
-    {
-      bvt tmp_bv;
-      for(std::size_t i=bits; i<bv.size(); i++)
-        tmp_bv.push_back(bv[i]);
-
-      return prop.lor(tmp_bv);
-    }
-  }
 
   return SUB::convert_rest(expr);
 }