From af1d428180b6867e95d85673367360331d030c53 Mon Sep 17 00:00:00 2001
From: Hannes Steffenhagen <hannes.steffenhagen@diffblue.com>
Date: Mon, 24 Sep 2018 17:26:51 +0100
Subject: [PATCH 1/2] Replace to_integer with numeric_cast in boolbv_index

---
 src/solvers/flattening/boolbv_index.cpp | 22 ++++++++++++----------
 1 file changed, 12 insertions(+), 10 deletions(-)

diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp
index ca66fb2c697..b5c27eee064 100644
--- a/src/solvers/flattening/boolbv_index.cpp
+++ b/src/solvers/flattening/boolbv_index.cpp
@@ -61,16 +61,18 @@ bvt boolbvt::convert_index(const index_exprt &expr)
     }
 
     // Must have a finite size
-    mp_integer array_size;
-    if(to_integer(array_type.size(), array_size))
-      throw "failed to convert array size";
-
-    // see if the index address is constant
-    // many of these are compacted by simplify_expr
-    // but variable location writes will block this
-    mp_integer index_value;
-    if(!to_integer(index, index_value))
-      return convert_index(array, index_value);
+    mp_integer array_size = numeric_cast_v<mp_integer>(array_type.size());
+
+    {
+      // see if the index address is constant
+      // many of these are compacted by simplify_expr
+      // but variable location writes will block this
+      auto maybe_index_value = numeric_cast<mp_integer>(index);
+      if(maybe_index_value.has_value())
+      {
+        return convert_index(array, maybe_index_value.value());
+      }
+    }
 
     // Special case : arrays of one thing (useful for constants)
     // TODO : merge with ACTUAL_ARRAY_HACK so that ranges of the same

From 7baf62dc39ac344d9613297244a01c7c3d1a7fb3 Mon Sep 17 00:00:00 2001
From: Hannes Steffenhagen <hannes.steffenhagen@diffblue.com>
Date: Mon, 24 Sep 2018 17:28:12 +0100
Subject: [PATCH 2/2] Replace throws and asserts with invariants in
 boolbv_index

Also use the expected_width parameter to move one check into convert_bv
---
 src/solvers/flattening/boolbv_index.cpp | 30 +++++++++++--------------
 1 file changed, 13 insertions(+), 17 deletions(-)

diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp
index b5c27eee064..f9bf25e6a3a 100644
--- a/src/solvers/flattening/boolbv_index.cpp
+++ b/src/solvers/flattening/boolbv_index.cpp
@@ -62,7 +62,6 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
     // Must have a finite size
     mp_integer array_size = numeric_cast_v<mp_integer>(array_type.size());
-
     {
       // see if the index address is constant
       // many of these are compacted by simplify_expr
@@ -117,12 +116,10 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
       binary_relation_exprt lower_bound(
         from_integer(0, index.type()), ID_le, index);
+      CHECK_RETURN(lower_bound.lhs().is_not_nil());
       binary_relation_exprt upper_bound(
         index, ID_lt, from_integer(array_size, index.type()));
-
-      if(lower_bound.lhs().is_nil() ||
-         upper_bound.rhs().is_nil())
-        throw "number conversion failed (2)";
+      CHECK_RETURN(upper_bound.rhs().is_not_nil());
 
       and_exprt range_condition(lower_bound, upper_bound);
       implies_exprt implication(range_condition, value_equality);
@@ -174,11 +171,12 @@ bvt boolbvt::convert_index(const index_exprt &expr)
       for(mp_integer i=0; i<array_size; i=i+1)
       {
         index_equality.rhs()=from_integer(i, index_equality.lhs().type());
+        CHECK_RETURN(index_equality.rhs().is_not_nil());
 
-        if(index_equality.rhs().is_nil())
-          throw "number conversion failed (1)";
-
-        assert(it != array.operands().end());
+        INVARIANT(
+          it != array.operands().end(),
+          "this loop iterates over the array, so `it` shouldn't be increased "
+          "past the array's end");
 
         value_equality.rhs()=*it++;
 
@@ -200,10 +198,8 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
     // get literals for the whole array
 
-    const bvt &array_bv=convert_bv(array);
-
-    if(array_size*width!=array_bv.size())
-      throw "unexpected array size";
+    const bvt &array_bv =
+      convert_bv(array, numeric_cast_v<std::size_t>(array_size * width));
 
     // TODO: maybe a shifter-like construction would be better
     // Would be a lot more compact but propagate worse
@@ -231,9 +227,7 @@ bvt boolbvt::convert_index(const index_exprt &expr)
       for(mp_integer i=0; i<array_size; i=i+1)
       {
         index_equality.rhs()=from_integer(i, index_equality.lhs().type());
-
-        if(index_equality.rhs().is_nil())
-          throw "number conversion failed (1)";
+        CHECK_RETURN(index_equality.rhs().is_not_nil());
 
         mp_integer offset=i*width;
 
@@ -258,7 +252,9 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
       typet constant_type=index.type(); // type of index operand
 
-      assert(array_size>0);
+      DATA_INVARIANT(
+        array_size > 0,
+        "non-positive array sizes are forbidden in goto programs");
 
       for(mp_integer i=0; i<array_size; i=i+1)
       {