From 18fbc6097983c271317d1ef91246155233cf5c15 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Mon, 10 Sep 2018 14:31:07 +0100 Subject: [PATCH 1/2] Error handling cleanup in solvers/flattening Files boolbv_constant.cpp, boolbv.cpp --- src/solvers/flattening/boolbv.cpp | 64 +++++++++++++++---------------- 1 file changed, 32 insertions(+), 32 deletions(-) diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 53f1cdcb44e..df3cd5a5af4 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -8,7 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "boolbv.h" -#include +#include #include #include @@ -36,7 +36,10 @@ bool boolbvt::literal( { if(expr.type().id()==ID_bool) { - assert(bit==0); + INVARIANT( + bit == 0, + "boolean expressions shall be represented by a single bit and hence the " + "only valid bit index is 0"); return prop_conv_solvert::literal(to_symbol_expr(expr), dest); } else @@ -54,7 +57,8 @@ bool boolbvt::literal( const boolbv_mapt::map_entryt &map_entry=it_m->second; - assert(bit(index_expr.index()); - mp_integer index; - if(to_integer(index_expr.index(), index)) - throw "literal expects constant index"; - - std::size_t offset=integer2unsigned(index*element_width); + std::size_t offset = numeric_cast_v(index * element_width); return literal(index_expr.array(), bit+offset, dest); } @@ -96,18 +96,16 @@ bool boolbvt::literal( return literal(expr.op0(), bit+offset, dest); std::size_t element_width=boolbv_width(subtype); - - if(element_width==0) - throw "literal expects a bit-vector type"; + CHECK_RETURN(element_width != 0); offset+=element_width; } - throw "failed to find component"; + INVARIANT(false, "struct type should have accessed component"); } } - throw "found no literal for expression"; + INVARIANT(false, "expression should have a corresponding literal"); } const bvt & @@ -308,7 +306,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr) else if(expr.id()==ID_float_debug1 || expr.id()==ID_float_debug2) { - assert(expr.operands().size()==2); + DATA_INVARIANT(expr.operands().size() == 2, ""); bvt bv0=convert_bitvector(expr.op0()); bvt bv1=convert_bitvector(expr.op1()); float_utilst float_utils(prop, to_floatbv_type(expr.type())); @@ -330,8 +328,8 @@ bvt boolbvt::convert_lambda(const exprt &expr) if(width==0) return conversion_failed(expr); - if(expr.operands().size()!=2) - throw "lambda takes two operands"; + DATA_INVARIANT( + expr.operands().size() == 2, "lambda expression should have two operands"); if(expr.type().id()!=ID_array) return conversion_failed(expr); @@ -358,10 +356,12 @@ bvt boolbvt::convert_lambda(const exprt &expr) const bvt &tmp=convert_bv(expr_op1); - std::size_t offset=integer2unsigned(i*tmp.size()); + INVARIANT( + size * tmp.size() == width, + "total bitvector width shall equal the number of operands times the size " + "per operand"); - if(size*tmp.size()!=width) - throw "convert_lambda: unexpected operand width"; + std::size_t offset = numeric_cast_v(i * tmp.size()); for(std::size_t j=0; jvar_no()>=prop.no_variables() && - !it->is_constant()) - { - error() << identifier << eom; - assert(false); - } + INVARIANT_WITH_DIAGNOSTICS( + std::all_of( + bv.begin(), + bv.end(), + [this](const literalt &l) { + return l.var_no() < prop.no_variables() || l.is_constant(); + }), + "variable number of non-constant literals should be within bounds", + id2string(identifier)); } return bv; From ce1963648ea9751204eb8d5bce3cf1cebd089ec6 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Fri, 21 Sep 2018 11:05:47 +0100 Subject: [PATCH 2/2] Remove ID_float_debug1 and ID_float_debug2 expressions --- src/ansi-c/c_typecheck_expr.cpp | 20 -------------------- src/solvers/flattening/boolbv.cpp | 12 ------------ src/util/irep_ids.def | 2 -- 3 files changed, 34 deletions(-) diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index 3040eb60c41..2eb389aa29b 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -2724,26 +2724,6 @@ exprt c_typecheck_baset::do_special_functions( return tmp; } - else if(identifier==CPROVER_PREFIX "float_debug1" || - identifier==CPROVER_PREFIX "float_debug2") - { - if(expr.arguments().size()!=2) - { - err_location(f_op); - error() << "float_debug expects two operands" << eom; - throw 0; - } - - const irep_idt &id= - identifier==CPROVER_PREFIX "float_debug1"? - "float_debug1":"float_debug2"; - - exprt float_debug_expr(id, expr.type()); - float_debug_expr.operands()=expr.arguments(); - float_debug_expr.add_source_location()=source_location; - - return float_debug_expr; - } else if(identifier=="__sync_fetch_and_add" || identifier=="__sync_fetch_and_sub" || identifier=="__sync_fetch_and_or" || diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index df3cd5a5af4..a5afd198811 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -303,18 +303,6 @@ bvt boolbvt::convert_bitvector(const exprt &expr) return convert_not(to_not_expr(expr)); else if(expr.id()==ID_power) return convert_power(to_binary_expr(expr)); - else if(expr.id()==ID_float_debug1 || - expr.id()==ID_float_debug2) - { - DATA_INVARIANT(expr.operands().size() == 2, ""); - bvt bv0=convert_bitvector(expr.op0()); - bvt bv1=convert_bitvector(expr.op1()); - float_utilst float_utils(prop, to_floatbv_type(expr.type())); - bvt bv=expr.id()==ID_float_debug1? - float_utils.debug1(bv0, bv1): - float_utils.debug2(bv0, bv1); - return bv; - } else if(expr.id() == ID_popcount) return convert_bv(lower_popcount(to_popcount_expr(expr), ns)); diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 2c8f19506a2..240b5abd4d1 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -514,8 +514,6 @@ IREP_ID_ONE(ptr_object) IREP_ID_TWO(C_c_sizeof_type, #c_sizeof_type) IREP_ID_ONE(array_update) IREP_ID_ONE(update) -IREP_ID_ONE(float_debug1) -IREP_ID_ONE(float_debug2) IREP_ID_ONE(static_assert) IREP_ID_ONE(gcc_attribute_mode) IREP_ID_TWO(built_in, )