From d07bba74eb891c64080c8ac6e199b49f8aa993e9 Mon Sep 17 00:00:00 2001 From: Daniel Poetzl Date: Thu, 13 Sep 2018 12:12:18 +0100 Subject: [PATCH] Error handling cleanup in solvers/flattening Files equality.cpp to pointer_logic.h --- src/solvers/flattening/equality.cpp | 10 +- .../flattening/flatten_byte_operators.cpp | 136 +++++++++--------- src/solvers/flattening/functions.cpp | 4 +- src/solvers/flattening/pointer_logic.cpp | 19 ++- 4 files changed, 85 insertions(+), 84 deletions(-) diff --git a/src/solvers/flattening/equality.cpp b/src/solvers/flattening/equality.cpp index 79890ab8979..e07bf114eed 100644 --- a/src/solvers/flattening/equality.cpp +++ b/src/solvers/flattening/equality.cpp @@ -24,10 +24,9 @@ literalt equalityt::equality(const exprt &e1, const exprt &e2) literalt equalityt::equality2(const exprt &e1, const exprt &e2) { - const typet &type=e1.type(); + PRECONDITION(e1.type() == e2.type()); - if(e2.type()!=e1.type()) - throw "equality got different types"; + const typet &type = e1.type(); // check for syntactical equality @@ -36,9 +35,8 @@ literalt equalityt::equality2(const exprt &e1, const exprt &e2) // check for boolean equality - if(type.id()==ID_bool) - throw "equalityt got boolean equality"; - // return lequal(convert(e1), convert(e2)); + INVARIANT( + type.id() != ID_bool, "method shall not be used to compare Boolean types"); // look it up diff --git a/src/solvers/flattening/flatten_byte_operators.cpp b/src/solvers/flattening/flatten_byte_operators.cpp index c5f27caaaf0..e6639810fb5 100644 --- a/src/solvers/flattening/flatten_byte_operators.cpp +++ b/src/solvers/flattening/flatten_byte_operators.cpp @@ -51,12 +51,15 @@ static exprt unpack_rec( mp_integer element_width=pointer_offset_bits(subtype, ns); // this probably doesn't really matter #if 0 - if(element_width<=0) - throw "cannot unpack array with non-constant element width:\n"+ - type.pretty(); - else if(element_width%8!=0) - throw "cannot unpack array of non-byte aligned elements:\n"+ - type.pretty(); + INVARIANT( + element_width > 0, + "element width of array should be constant", + irep_pretty_diagnosticst(type)); + + INVARIANT( + element_width % 8 == 0, + "elements in array should be byte-aligned", + irep_pretty_diagnosticst(type)); #endif if(!unpack_byte_array && element_width==8) @@ -199,8 +202,6 @@ exprt flatten_byte_extract( // big-endian: (short)concatenation(01,02)=0x0102 // little-endian: (short)concatenation(03,04)=0x0304 - assert(src.operands().size()==2); - PRECONDITION( src.id() == ID_byte_extract_little_endian || src.id() == ID_byte_extract_big_endian); @@ -345,14 +346,14 @@ exprt flatten_byte_update( const namespacet &ns, bool negative_offset) { - assert(src.operands().size()==3); + mp_integer element_size = pointer_offset_size(src.value().type(), ns); - mp_integer element_size= - pointer_offset_size(src.op2().type(), ns); - if(element_size<0) - throw "byte_update of unknown width:\n"+src.pretty(); + INVARIANT_WITH_DIAGNOSTICS( + element_size >= 0, + "size of type in bytes must be known", + irep_pretty_diagnosticst(src)); - const typet &t=ns.follow(src.op0().type()); + const typet &t = ns.follow(src.op().type()); if(t.id()==ID_array) { @@ -368,44 +369,48 @@ exprt flatten_byte_update( { mp_integer sub_size=pointer_offset_size(subtype, ns); - if(sub_size==-1) - throw "can't flatten byte_update for sub-type without size"; + INVARIANT( + sub_size >= 0, + "bit width (rounded to full bytes) of subtype must be known"); // byte array? if(sub_size==1) { // apply 'array-update-with' element_size times - exprt result=src.op0(); + exprt result = src.op(); for(mp_integer i=0; i0); + CHECK_RETURN(type_width > 0); std::size_t width=integer2size_t(type_width); - if(element_size*8>width) - throw "flatten_byte_update to update element that is too large"; + INVARIANT( + element_size * 8 <= width, + "element bit width must not be larger than width indicated by type"); // build mask exprt mask= @@ -544,16 +550,16 @@ exprt flatten_byte_update( exprt value_extended; if(width>integer2unsigned(element_size)*8) - value_extended= - concatenation_exprt( - from_integer( - 0, unsignedbv_typet(width-integer2unsigned(element_size)*8)), - src.op2(), t); + value_extended = concatenation_exprt( + from_integer( + 0, unsignedbv_typet(width - integer2unsigned(element_size) * 8)), + src.value(), + t); else - value_extended=src.op2(); + value_extended = src.value(); - const typet &offset_type=ns.follow(src.op1().type()); - mult_exprt offset_times_eight(src.op1(), from_integer(8, offset_type)); + const typet &offset_type = ns.follow(src.offset().type()); + mult_exprt offset_times_eight(src.offset(), from_integer(8, offset_type)); binary_predicate_exprt offset_ge_zero( offset_times_eight, @@ -578,7 +584,7 @@ exprt flatten_byte_update( } // original_bits &= ~mask - bitand_exprt bitand_expr(src.op0(), bitnot_exprt(mask_shifted)); + bitand_exprt bitand_expr(src.op(), bitnot_exprt(mask_shifted)); // original_bits |= newvalue bitor_exprt bitor_expr(bitand_expr, value_shifted); @@ -587,8 +593,10 @@ exprt flatten_byte_update( } else { - throw "flatten_byte_update can only do array and scalars " - "right now, but got "+t.id_string(); + PRECONDITION_WITH_DIAGNOSTICS( + false, + "flatten_byte_update can only do arrays and scalars right now", + t.id_string()); } } diff --git a/src/solvers/flattening/functions.cpp b/src/solvers/flattening/functions.cpp index 181d901fd5e..c650efc4f8f 100644 --- a/src/solvers/flattening/functions.cpp +++ b/src/solvers/flattening/functions.cpp @@ -8,8 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "functions.h" -#include - #include #include @@ -32,7 +30,7 @@ void functionst::add_function_constraints() exprt functionst::arguments_equal(const exprt::operandst &o1, const exprt::operandst &o2) { - assert(o1.size()==o2.size()); + PRECONDITION(o1.size() == o2.size()); if(o1.empty()) return true_exprt(); diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp index ffc2eae4755..74bf8ea118c 100644 --- a/src/solvers/flattening/pointer_logic.cpp +++ b/src/solvers/flattening/pointer_logic.cpp @@ -11,8 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "pointer_logic.h" -#include - #include #include #include @@ -52,13 +50,11 @@ std::size_t pointer_logict::add_object(const exprt &expr) if(expr.id()==ID_index) { - assert(expr.operands().size()==2); - return add_object(expr.op0()); + return add_object(to_index_expr(expr).array()); } else if(expr.id()==ID_member) { - assert(expr.operands().size()==1); - return add_object(expr.op0()); + return add_object(to_member_expr(expr).compound()); } return objects.number(expr); @@ -149,12 +145,15 @@ exprt pointer_logict::object_rec( for(const auto &c : components) { - assert(offset>=current_offset); + INVARIANT( + offset >= current_offset, + "when the object has not been found yet its offset must not be smaller" + "than the offset of the current struct component"); const typet &subtype=c.type(); mp_integer sub_size=pointer_offset_size(subtype, ns); - assert(sub_size>0); + CHECK_RETURN(sub_size > 0); mp_integer new_offset=current_offset+sub_size; if(new_offset>offset) @@ -166,9 +165,7 @@ exprt pointer_logict::object_rec( offset-current_offset, pointer_type, tmp); } - assert(new_offset<=offset); current_offset=new_offset; - assert(current_offset<=offset); } return src; @@ -183,7 +180,7 @@ pointer_logict::pointer_logict(const namespacet &_ns):ns(_ns) { // add NULL null_object=objects.number(exprt(ID_NULL)); - assert(null_object==0); + CHECK_RETURN(null_object == 0); // add INVALID invalid_object=objects.number(exprt("INVALID"));