From af1d428180b6867e95d85673367360331d030c53 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen 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(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(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 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(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 * 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; i0); + DATA_INVARIANT( + array_size > 0, + "non-positive array sizes are forbidden in goto programs"); for(mp_integer i=0; i