From bf19b3939a1780f610592f4f110db4582de251d8 Mon Sep 17 00:00:00 2001 From: Sonny Martin Date: Thu, 27 Sep 2018 11:04:28 +0100 Subject: [PATCH 1/2] Cleanup asserts & throws - replace with invariants Deprecated c-style asserts in favour of cbmc invariants. Some minor refactoring that was relevant to the cleanup. --- src/util/simplify_expr.cpp | 55 ++++++++++++++---------------- src/util/simplify_expr_boolean.cpp | 14 ++++---- src/util/simplify_expr_floatbv.cpp | 31 ++++++++++------- src/util/std_expr.h | 18 ++++++++++ 4 files changed, 68 insertions(+), 50 deletions(-) diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 96e94afab13..2d9ecf36523 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -8,7 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "simplify_expr.h" -#include #include #include "arith_tools.h" @@ -19,6 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "endianness_map.h" #include "expr_util.h" #include "fixedbv.h" +#include "invariant.h" #include "namespace.h" #include "pointer_offset_size.h" #include "rational.h" @@ -225,7 +225,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr) inequality.add_source_location()=expr.source_location(); inequality.lhs()=expr.op0(); inequality.rhs()=from_integer(0, op_type); - assert(inequality.rhs().is_not_nil()); + CHECK_RETURN(inequality.rhs().is_not_nil()); simplify_node(inequality); expr.swap(inequality); return false; @@ -260,7 +260,7 @@ bool simplify_exprt::simplify_typecast(exprt &expr) inequality.add_source_location()=expr.source_location(); inequality.lhs()=expr.op0(); inequality.rhs()=from_integer(0, op_type); - assert(inequality.rhs().is_not_nil()); + CHECK_RETURN(inequality.rhs().is_not_nil()); simplify_node(inequality); expr.op0()=inequality; simplify_typecast(expr); // recursive call @@ -488,13 +488,13 @@ bool simplify_exprt::simplify_typecast(exprt &expr) if(operand.is_true()) { expr=from_integer(1, expr_type); - assert(expr.is_not_nil()); + CHECK_RETURN(expr.is_not_nil()); return false; } else if(operand.is_false()) { expr=from_integer(0, expr_type); - assert(expr.is_not_nil()); + CHECK_RETURN(expr.is_not_nil()); return false; } } @@ -1365,17 +1365,13 @@ bool simplify_exprt::simplify_update(exprt &expr) { const irep_idt &component_name= e.get(ID_component_name); - - if(!to_struct_type(value_ptr_type). - has_component(component_name)) + const struct_typet &value_ptr_struct_type = + to_struct_type(value_ptr_type); + if(!value_ptr_struct_type.has_component(component_name)) return true; - - std::size_t number=to_struct_type(value_ptr_type). - component_number(component_name); - - assert(numberoperands().size()); - - value_ptr=&value_ptr->operands()[number]; + auto &designator_as_struct_expr = to_struct_expr(*value_ptr); + value_ptr = &designator_as_struct_expr.component(component_name, ns); + CHECK_RETURN(value_ptr->is_not_nil()); } else return true; // give up, unknown designator @@ -1407,16 +1403,13 @@ bool simplify_exprt::simplify_object(exprt &expr) } else if(expr.id()==ID_typecast) { - const typet &op_type=ns.follow(expr.op0().type()); - - assert(expr.operands().size()==1); + auto const &typecast_expr = to_typecast_expr(expr); + const typet &op_type = ns.follow(typecast_expr.op().type()); if(op_type.id()==ID_pointer) { // cast from pointer to pointer - exprt tmp; - tmp.swap(expr.op0()); - expr.swap(tmp); + expr = typecast_expr.op(); simplify_object(expr); return false; } @@ -1427,10 +1420,12 @@ bool simplify_exprt::simplify_object(exprt &expr) // We do a bit of special treatment for (TYPE *)(a+(int)&o) and // (TYPE *)(a+(int)((T*)&o+x)), which are re-written to '&o'. - exprt tmp=expr.op0(); - if(tmp.id()==ID_plus && tmp.operands().size()==2) + const exprt &casted_expr = typecast_expr.op(); + if(casted_expr.id() == ID_plus && casted_expr.operands().size() == 2) { - exprt cand=tmp.op0().id()==ID_typecast?tmp.op0():tmp.op1(); + const exprt &cand = casted_expr.op0().id() == ID_typecast + ? casted_expr.op0() + : casted_expr.op1(); if(cand.id()==ID_typecast && cand.operands().size()==1 && @@ -1545,7 +1540,7 @@ exprt simplify_exprt::bits2expr( for(const auto &component : components) { mp_integer m_size=pointer_offset_bits(component.type(), ns); - assert(m_size>=0); + CHECK_RETURN(m_size >= 0); std::string comp_bits= std::string( @@ -1573,7 +1568,7 @@ exprt simplify_exprt::bits2expr( std::size_t el_size= integer2size_t(pointer_offset_bits(type.subtype(), ns)); - assert(el_size>0); + CHECK_RETURN(el_size > 0); array_exprt result(array_type); result.reserve_operands(n_el); @@ -1829,10 +1824,10 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr) op_type_ptr->id()==ID_array; op_type_ptr=&(ns.follow(*op_type_ptr).subtype())) { - // no arrays of zero-sized objects - assert(el_size>0); - // no arrays of non-byte sized objects - assert(el_size%8==0); + DATA_INVARIANT(el_size > 0, "arrays must not have zero-sized objects"); + DATA_INVARIANT( + el_size % 8 == 0, + "array elements have a size in bits which is a multiple of bytes"); mp_integer el_bytes=el_size/8; if(base_type_eq(expr.type(), op_type_ptr->subtype(), ns) || diff --git a/src/util/simplify_expr_boolean.cpp b/src/util/simplify_expr_boolean.cpp index 06bd5f505a8..89003be5d4a 100644 --- a/src/util/simplify_expr_boolean.cpp +++ b/src/util/simplify_expr_boolean.cpp @@ -8,10 +8,10 @@ Author: Daniel Kroening, kroening@kroening.com #include "simplify_expr_class.h" -#include #include #include "expr.h" +#include "invariant.h" #include "namespace.h" #include "std_expr.h" @@ -213,13 +213,11 @@ bool simplify_exprt::simplify_not(exprt &expr) } else if(op.id()==ID_exists) // !(exists: a) <-> forall: not a { - assert(op.operands().size()==2); - exprt tmp; - tmp.swap(op); - expr.swap(tmp); - expr.id(ID_forall); - expr.op1().make_not(); - simplify_node(expr.op1()); + auto const &op_as_exists = to_exists_expr(op); + forall_exprt rewritten_op( + op_as_exists.symbol(), not_exprt(op_as_exists.where())); + simplify_node(rewritten_op.where()); + expr = rewritten_op; return false; } diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp index 96af383485f..12211ddeb0d 100644 --- a/src/util/simplify_expr_floatbv.cpp +++ b/src/util/simplify_expr_floatbv.cpp @@ -8,13 +8,12 @@ Author: Daniel Kroening, kroening@kroening.com #include "simplify_expr_class.h" -#include - +#include "arith_tools.h" #include "expr.h" -#include "namespace.h" #include "ieee_float.h" +#include "invariant.h" +#include "namespace.h" #include "std_expr.h" -#include "arith_tools.h" bool simplify_exprt::simplify_isinf(exprt &expr) { @@ -286,17 +285,25 @@ bool simplify_exprt::simplify_floatbv_op(exprt &expr) { const typet &type=ns.follow(expr.type()); - if(type.id()!=ID_floatbv) - return true; - - assert(expr.operands().size()==3); + PRECONDITION(type.id() == ID_floatbv); + PRECONDITION( + expr.id() == ID_floatbv_plus || expr.id() == ID_floatbv_minus || + expr.id() == ID_floatbv_mult || expr.id() == ID_floatbv_div); + DATA_INVARIANT( + expr.operands().size() == 3, + "binary operations have two operands, here an addtional parameter " + "is for the rounding mode"); exprt op0=expr.op0(); exprt op1=expr.op1(); exprt op2=expr.op2(); // rounding mode - assert(ns.follow(op0.type())==type); - assert(ns.follow(op1.type())==type); + INVARIANT( + ns.follow(op0.type()) == type, + "expression type of operand must match type of expression"); + INVARIANT( + ns.follow(op1.type()) == type, + "expression type of operand must match type of expression"); // Remember that floating-point addition is _NOT_ associative. // Thus, we don't re-sort the operands. @@ -347,8 +354,8 @@ bool simplify_exprt::simplify_floatbv_op(exprt &expr) bool simplify_exprt::simplify_ieee_float_relation(exprt &expr) { - assert(expr.id()==ID_ieee_float_equal || - expr.id()==ID_ieee_float_notequal); + PRECONDITION( + expr.id() == ID_ieee_float_equal || expr.id() == ID_ieee_float_notequal); exprt::operandst &operands=expr.operands(); diff --git a/src/util/std_expr.h b/src/util/std_expr.h index f7f812f3076..25ab5cef5fb 100644 --- a/src/util/std_expr.h +++ b/src/util/std_expr.h @@ -4512,6 +4512,24 @@ class exists_exprt:public quantifier_exprt } }; +inline const exists_exprt &to_exists_expr(const exprt &expr) +{ + PRECONDITION(expr.id() == ID_exists); + DATA_INVARIANT( + expr.operands().size() == 2, + "exists expressions have exactly two operands"); + return static_cast(expr); +} + +inline exists_exprt &to_exists_expr(exprt &expr) +{ + PRECONDITION(expr.id() == ID_exists); + DATA_INVARIANT( + expr.operands().size() == 2, + "exists expressions have exactly two operands"); + return static_cast(expr); +} + /// \brief The popcount (counting the number of bits set to 1) expression class popcount_exprt: public unary_exprt { From a168b24b8da1a95938a4df6fc65510347fc51e42 Mon Sep 17 00:00:00 2001 From: Hannes Steffenhagen Date: Fri, 28 Sep 2018 15:29:22 +0100 Subject: [PATCH 2/2] Refactor simplify_floatbv_typecast * Use to_XXX_expr functions instead of asserts to make sure invariants are not violated * Use named accessors instead of op0, op1 etc * Rename variables (e.g. "casted_expr" instead of "op0") for readability --- src/util/simplify_expr_floatbv.cpp | 110 ++++++++++++++--------------- 1 file changed, 53 insertions(+), 57 deletions(-) diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp index 12211ddeb0d..2a1226c4a5f 100644 --- a/src/util/simplify_expr_floatbv.cpp +++ b/src/util/simplify_expr_floatbv.cpp @@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "ieee_float.h" #include "invariant.h" #include "namespace.h" +#include "simplify_expr.h" #include "std_expr.h" bool simplify_exprt::simplify_isinf(exprt &expr) @@ -141,43 +142,43 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr) { // These casts usually reduce precision, and thus, usually round. - assert(expr.operands().size()==2); + auto const &floatbv_typecast_expr = to_floatbv_typecast_expr(expr); - const typet &dest_type=ns.follow(expr.type()); - const typet &src_type=ns.follow(expr.op0().type()); + const typet &dest_type = ns.follow(floatbv_typecast_expr.type()); + const typet &src_type = ns.follow(floatbv_typecast_expr.op().type()); // eliminate redundant casts if(dest_type==src_type) { - expr=expr.op0(); + expr = floatbv_typecast_expr.op(); return false; } - exprt op0=expr.op0(); - exprt op1=expr.op1(); // rounding mode + const exprt &casted_expr = floatbv_typecast_expr.op(); + const exprt &rounding_mode = floatbv_typecast_expr.rounding_mode(); // We can soundly re-write (float)((double)x op (double)y) // to x op y. True for any rounding mode! #if 0 - if(op0.id()==ID_floatbv_div || - op0.id()==ID_floatbv_mult || - op0.id()==ID_floatbv_plus || - op0.id()==ID_floatbv_minus) + if(casted_expr.id()==ID_floatbv_div || + casted_expr.id()==ID_floatbv_mult || + casted_expr.id()==ID_floatbv_plus || + casted_expr.id()==ID_floatbv_minus) { - if(op0.operands().size()==3 && - op0.op0().id()==ID_typecast && - op0.op1().id()==ID_typecast && - op0.op0().operands().size()==1 && - op0.op1().operands().size()==1 && - ns.follow(op0.op0().type())==dest_type && - ns.follow(op0.op1().type())==dest_type) + if(casted_expr.operands().size()==3 && + casted_expr.op0().id()==ID_typecast && + casted_expr.op1().id()==ID_typecast && + casted_expr.op0().operands().size()==1 && + casted_expr.op1().operands().size()==1 && + ns.follow(casted_expr.op0().type())==dest_type && + ns.follow(casted_expr.op1().type())==dest_type) { - exprt result(op0.id(), expr.type()); + exprt result(casted_expr.id(), floatbv_typecast_expr.type()); result.operands().resize(3); - result.op0()=op0.op0().op0(); - result.op1()=op0.op1().op0(); - result.op2()=op1; + result.op0()=casted_expr.op0().op0(); + result.op1()=casted_expr.op1().op0(); + result.op2()=rounding_mode; simplify_node(result); expr.swap(result); @@ -187,18 +188,18 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr) #endif // constant folding - if(op0.is_constant() && op1.is_constant()) + if(casted_expr.is_constant() && rounding_mode.is_constant()) { - mp_integer rounding_mode; - if(!to_integer(op1, rounding_mode)) + mp_integer rounding_mode_index; + if(!to_integer(rounding_mode, rounding_mode_index)) { if(src_type.id()==ID_floatbv) { if(dest_type.id()==ID_floatbv) // float to float { - ieee_floatt result(to_constant_expr(op0)); - result.rounding_mode= - (ieee_floatt::rounding_modet)integer2size_t(rounding_mode); + ieee_floatt result(to_constant_expr(casted_expr)); + result.rounding_mode = + (ieee_floatt::rounding_modet)integer2size_t(rounding_mode_index); result.change_spec( ieee_float_spect(to_floatbv_type(dest_type))); expr=result.to_expr(); @@ -207,11 +208,11 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr) else if(dest_type.id()==ID_signedbv || dest_type.id()==ID_unsignedbv) { - if(rounding_mode==ieee_floatt::ROUND_TO_ZERO) + if(rounding_mode_index == ieee_floatt::ROUND_TO_ZERO) { - ieee_floatt result(to_constant_expr(op0)); - result.rounding_mode= - (ieee_floatt::rounding_modet)integer2size_t(rounding_mode); + ieee_floatt result(to_constant_expr(casted_expr)); + result.rounding_mode = + (ieee_floatt::rounding_modet)integer2size_t(rounding_mode_index); mp_integer value=result.to_integer(); expr=from_integer(value, dest_type); return false; @@ -222,13 +223,13 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr) src_type.id()==ID_unsignedbv) { mp_integer value; - if(!to_integer(op0, value)) + if(!to_integer(casted_expr, value)) { if(dest_type.id()==ID_floatbv) // int to float { ieee_floatt result(to_floatbv_type(dest_type)); - result.rounding_mode= - (ieee_floatt::rounding_modet)integer2size_t(rounding_mode); + result.rounding_mode = + (ieee_floatt::rounding_modet)integer2size_t(rounding_mode_index); result.from_integer(value); expr=result.to_expr(); return false; @@ -239,15 +240,16 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr) { // go through underlying type const auto &enum_type = ns.follow_tag(to_c_enum_tag_type(src_type)); - typecast_exprt tmp1(op0, to_c_enum_type(enum_type).subtype()); - simplify_typecast(tmp1); - if(tmp1.is_constant()) + exprt simplified_typecast = simplify_expr( + typecast_exprt(casted_expr, to_c_enum_type(enum_type).subtype()), ns); + if(simplified_typecast.is_constant()) { - exprt tmp2 = expr; - tmp2.op0() = tmp1; - if(!simplify_floatbv_typecast(tmp2)) + floatbv_typecast_exprt new_floatbv_typecast_expr = + floatbv_typecast_expr; + new_floatbv_typecast_expr.op() = simplified_typecast; + if(!simplify_floatbv_typecast(new_floatbv_typecast_expr)) { - expr = tmp2; + expr = new_floatbv_typecast_expr; return false; } } @@ -257,23 +259,17 @@ bool simplify_exprt::simplify_floatbv_typecast(exprt &expr) #if 0 // (T)(a?b:c) --> a?(T)b:(T)c - if(expr.op0().id()==ID_if && - expr.op0().operands().size()==3) + if(casted_expr.id()==ID_if) { - binary_exprt tmp_op1( - expr.op0().op1(), - ID_floatbv_typecast, - expr.op1(), - dest_type); - binary_exprt tmp_op2( - expr.op0().op2(), - ID_floatbv_typecast, - expr.op1(), - dest_type); - simplify_floatbv_typecast(tmp_op1); - simplify_floatbv_typecast(tmp_op2); - expr=if_exprt(expr.op0().op0(), tmp_op1, tmp_op2, dest_type); - simplify_if(expr); + auto const &casted_if_expr = to_if_expr(casted_expr); + + floatbv_typecast_exprt casted_true_case(casted_if_expr.true_case(), rounding_mode, dest_type); + floatbv_typecast_exprt casted_false_case(casted_if_expr.false_case(), rounding_mode, dest_type); + + simplify_floatbv_typecast(casted_true_case); + simplify_floatbv_typecast(casted_false_case); + auto simplified_if_expr = simplify_expr(if_exprt(casted_if_expr.cond(), casted_true_case, casted_false_case, dest_type), ns); + expr = simplified_if_expr; return false; } #endif