From 5ce3bc3738c143265cf2e66378d437f43e7d275a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 3 Jun 2022 11:13:31 +0000 Subject: [PATCH 1/2] Support non-tag typed struct/union member expressions The SAT back-end assumed that all struct/union expressions had a tag instead of the full type, which is not actually a GOTO program invariant. --- src/solvers/flattening/boolbv_member.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/solvers/flattening/boolbv_member.cpp b/src/solvers/flattening/boolbv_member.cpp index c754640ed8c..ede61cc2a6a 100644 --- a/src/solvers/flattening/boolbv_member.cpp +++ b/src/solvers/flattening/boolbv_member.cpp @@ -47,10 +47,14 @@ bvt boolbvt::convert_member(const member_exprt &expr) { const bvt &compound_bv = convert_bv(expr.compound()); - if(expr.compound().type().id() == ID_struct_tag) + const typet &compound_type = expr.compound().type(); + + if(compound_type.id() == ID_struct_tag || compound_type.id() == ID_struct) { const struct_typet &struct_op_type = - ns.follow_tag(to_struct_tag_type(expr.compound().type())); + compound_type.id() == ID_struct_tag + ? ns.follow_tag(to_struct_tag_type(compound_type)) + : to_struct_type(compound_type); const auto &member_bits = bv_width.get_member(struct_op_type, expr.get_component_name()); @@ -66,7 +70,8 @@ bvt boolbvt::convert_member(const member_exprt &expr) } else { - PRECONDITION(expr.compound().type().id() == ID_union_tag); + PRECONDITION( + compound_type.id() == ID_union_tag || compound_type.id() == ID_union); return convert_member_union(expr, compound_bv, *this, ns); } } From 5ea97b3e8ec0379db7ceeb9bb44817356a96c612 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 2 Jun 2022 10:04:02 +0000 Subject: [PATCH 2/2] Add overflow_result_exprt: compute result and overflow in one expression Doing both the arithmetic operation and determining whether or not there was an overflow previously required either multiple expressions or going via `__builtin_X_overflow`, which should be specific to the C front-end. The new expression returns a struct with two components, the first of which has the type of the arithmetic operation, and the second is Boolean. Fixes: #6841 --- .../goto_convert_side_effect.cpp | 130 +++---- src/solvers/flattening/boolbv.cpp | 6 + src/solvers/flattening/boolbv.h | 2 + src/solvers/flattening/boolbv_overflow.cpp | 319 +++++++++++++----- src/solvers/smt2/smt2_conv.cpp | 138 +++++++- src/util/bitvector_expr.cpp | 57 ++++ src/util/bitvector_expr.h | 140 ++++++++ src/util/irep_ids.def | 5 + src/util/simplify_expr.cpp | 185 ++++++++++ src/util/simplify_expr_class.h | 7 + 10 files changed, 812 insertions(+), 177 deletions(-) diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp index fbd99e6dbbb..b6630a44c89 100644 --- a/src/goto-programs/goto_convert_side_effect.cpp +++ b/src/goto-programs/goto_convert_side_effect.cpp @@ -12,14 +12,14 @@ Author: Daniel Kroening, kroening@kroening.com #include "goto_convert_class.h" #include +#include +#include #include #include #include #include #include -#include - #include bool goto_convertt::has_function_call(const exprt &expr) @@ -589,91 +589,65 @@ void goto_convertt::remove_overflow( const exprt &rhs = expr.rhs(); const exprt &result = expr.result(); - // actual logic implementing the operators: perform operations on signed - // bitvector types of sufficiently large size to hold the result - auto const make_operation = [&statement](exprt lhs, exprt rhs) -> exprt { - std::size_t lhs_ssize = to_bitvector_type(lhs.type()).get_width(); - if(lhs.type().id() == ID_unsignedbv) - ++lhs_ssize; - std::size_t rhs_ssize = to_bitvector_type(rhs.type()).get_width(); - if(rhs.type().id() == ID_unsignedbv) - ++rhs_ssize; - - if(statement == ID_overflow_plus) - { - std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1; - integer_bitvector_typet ssize_type{ID_signedbv, ssize}; - return plus_exprt{typecast_exprt{lhs, ssize_type}, - typecast_exprt{rhs, ssize_type}}; - } - else if(statement == ID_overflow_minus) + if(result.type().id() != ID_pointer) + { + // result of the arithmetic operation is _not_ used, just evaluate side + // effects + exprt tmp = result; + clean_expr(tmp, dest, mode, false); + + // the is-there-an-overflow result may be used + if(result_is_used) { - std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1; - integer_bitvector_typet ssize_type{ID_signedbv, ssize}; - return minus_exprt{typecast_exprt{lhs, ssize_type}, - typecast_exprt{rhs, ssize_type}}; + binary_overflow_exprt overflow_check{ + typecast_exprt::conditional_cast(lhs, result.type()), + statement, + typecast_exprt::conditional_cast(rhs, result.type())}; + overflow_check.add_source_location() = expr.source_location(); + expr.swap(overflow_check); } else - { - INVARIANT( - statement == ID_overflow_mult, - "the three overflow operations are add, sub and mul"); - std::size_t ssize = lhs_ssize + rhs_ssize; - integer_bitvector_typet ssize_type{ID_signedbv, ssize}; - return mult_exprt{typecast_exprt{lhs, ssize_type}, - typecast_exprt{rhs, ssize_type}}; - } - }; - - // Generating the following sequence of statements: - // large_signedbv tmp = (large_signedbv)lhs OP (large_signedbv)rhs; - // *result = (result_type)tmp; // only if result is a pointer - // (large_signedbv)(result_type)tmp != tmp; - // This performs the operation (+, -, *) on a signed bitvector type of - // sufficiently large width to store the precise result, cast to result - // type, check if the cast result is not equivalent to the full-length - // result. - auto operation = make_operation(lhs, rhs); - // Disable overflow checks as the operation cannot overflow on the larger - // type - operation.add_source_location() = expr.source_location(); - operation.add_source_location().add_pragma("disable:signed-overflow-check"); - - make_temp_symbol(operation, "large_bv", dest, mode); - - optionalt result_type; - if(result.type().id() == ID_pointer) - { - result_type = to_pointer_type(result.type()).base_type(); - code_assignt result_assignment{dereference_exprt{result}, - typecast_exprt{operation, *result_type}, - expr.source_location()}; - convert_assign(result_assignment, dest, mode); + expr.make_nil(); } else { - result_type = result.type(); - // evaluate side effects - exprt tmp = result; - clean_expr(tmp, dest, mode, false); // result _not_ used - } - - if(result_is_used) - { - typecast_exprt inner_tc{operation, *result_type}; - inner_tc.add_source_location() = expr.source_location(); - inner_tc.add_source_location().add_pragma("disable:conversion-check"); - typecast_exprt outer_tc{inner_tc, operation.type()}; - outer_tc.add_source_location() = expr.source_location(); - outer_tc.add_source_location().add_pragma("disable:conversion-check"); + const typet &arith_type = to_pointer_type(result.type()).base_type(); + irep_idt arithmetic_operation = + statement == ID_overflow_plus + ? ID_plus + : statement == ID_overflow_minus + ? ID_minus + : statement == ID_overflow_mult ? ID_mult : ID_nil; + CHECK_RETURN(arithmetic_operation != ID_nil); + exprt overflow_with_result = overflow_result_exprt{ + typecast_exprt::conditional_cast(lhs, arith_type), + arithmetic_operation, + typecast_exprt::conditional_cast(rhs, arith_type)}; + overflow_with_result.add_source_location() = expr.source_location(); + + if(result_is_used) + make_temp_symbol(overflow_with_result, "overflow_result", dest, mode); + + const struct_typet::componentst &result_comps = + to_struct_type(overflow_with_result.type()).components(); + CHECK_RETURN(result_comps.size() == 2); + code_assignt result_assignment{ + dereference_exprt{result}, + typecast_exprt::conditional_cast( + member_exprt{overflow_with_result, result_comps[0]}, arith_type), + expr.source_location()}; + convert_assign(result_assignment, dest, mode); - notequal_exprt overflow_check{outer_tc, operation}; - overflow_check.add_source_location() = expr.source_location(); + if(result_is_used) + { + member_exprt overflow_check{overflow_with_result, result_comps[1]}; + overflow_check.add_source_location() = expr.source_location(); - expr.swap(overflow_check); + expr.swap(overflow_check); + } + else + expr.make_nil(); } - else - expr.make_nil(); } void goto_convertt::remove_side_effect( diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 266df646a15..c26cd7acee8 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -228,6 +228,12 @@ bvt boolbvt::convert_bitvector(const exprt &expr) return convert_bitreverse(to_bitreverse_expr(expr)); else if(expr.id() == ID_saturating_minus || expr.id() == ID_saturating_plus) return convert_saturating_add_sub(to_binary_expr(expr)); + else if( + const auto overflow_with_result = + expr_try_dynamic_cast(expr)) + { + return convert_overflow_result(*overflow_with_result); + } return conversion_failed(expr); } diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index d221ed18876..74081b2e1f3 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -38,6 +38,7 @@ class extractbits_exprt; class floatbv_typecast_exprt; class ieee_float_op_exprt; class member_exprt; +class overflow_result_exprt; class replication_exprt; class unary_overflow_exprt; class union_typet; @@ -197,6 +198,7 @@ class boolbvt:public arrayst const function_application_exprt &expr); virtual bvt convert_bitreverse(const bitreverse_exprt &expr); virtual bvt convert_saturating_add_sub(const binary_exprt &expr); + virtual bvt convert_overflow_result(const overflow_result_exprt &expr); void convert_with( const typet &type, diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp index 44fd3f7d1f9..f9a0a3ea188 100644 --- a/src/solvers/flattening/boolbv_overflow.cpp +++ b/src/solvers/flattening/boolbv_overflow.cpp @@ -6,12 +6,111 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include #include #include #include #include "boolbv.h" +static bvt mult_overflow_result( + propt &prop, + const bvt &bv0, + const bvt &bv1, + bv_utilst::representationt rep) +{ + bv_utilst bv_utils{prop}; + + std::size_t old_size = bv0.size(); + std::size_t new_size = old_size * 2; + + // sign/zero extension + const bvt &bv0_extended = bv_utils.extension(bv0, new_size, rep); + const bvt &bv1_extended = bv_utils.extension(bv1, new_size, rep); + + bvt result_extended = bv_utils.multiplier(bv0_extended, bv1_extended, rep); + bvt bv{result_extended.begin(), result_extended.begin() + old_size}; + bvt bv_overflow{result_extended.begin() + old_size, result_extended.end()}; + + if(rep == bv_utilst::representationt::UNSIGNED) + { + bv.push_back(prop.lor(bv_overflow)); + } + else + { + // get top result bits, plus one more + bv_overflow.push_back(bv.back()); + + // these need to be either all 1's or all 0's + literalt all_one = prop.land(bv_overflow); + literalt all_zero = !prop.lor(bv_overflow); + bv.push_back(!prop.lor(all_one, all_zero)); + } + + return bv; +} + +static bvt shl_overflow_result( + propt &prop, + const bvt &bv0, + const bvt &bv1, + bv_utilst::representationt rep0, + bv_utilst::representationt rep1) +{ + bv_utilst bv_utils{prop}; + + std::size_t old_size = bv0.size(); + std::size_t new_size = old_size * 2; + + bvt result_extended = bv_utils.shift( + bv_utils.extension(bv0, new_size, rep0), + bv_utilst::shiftt::SHIFT_LEFT, + bv1); + bvt bv{result_extended.begin(), result_extended.begin() + old_size}; + bvt bv_overflow{result_extended.begin() + old_size, result_extended.end()}; + + // a negative shift is undefined; yet this isn't an overflow + literalt neg_shift = rep1 == bv_utilst::representationt::UNSIGNED + ? const_literal(false) + : bv_utils.sign_bit(bv1); + + // an undefined shift of a non-zero value always results in overflow + std::size_t cmp_width = std::max(bv1.size(), address_bits(old_size) + 1); + literalt undef = bv_utils.rel( + bv_utils.extension(bv1, cmp_width, rep1), + ID_gt, + bv_utils.build_constant(old_size, cmp_width), + rep1); + + if(rep0 == bv_utilst::representationt::UNSIGNED) + { + // one of the top bits is non-zero + bv.push_back(prop.lor(bv_overflow)); + } + else + { + // get top result bits, plus one more + bv_overflow.push_back(bv.back()); + + // the sign bit has changed + literalt sign_change = + !prop.lequal(bv_utils.sign_bit(bv0), bv_utils.sign_bit(bv)); + + // these need to be either all 1's or all 0's + literalt all_one = prop.land(bv_overflow); + literalt all_zero = !prop.lor(bv_overflow); + + bv.push_back(prop.lor(sign_change, !prop.lor(all_one, all_zero))); + } + + // a negative shift isn't an overflow; else check the conditions built + // above + bv.back() = + prop.land(!neg_shift, prop.lselect(undef, prop.lor(bv0), bv.back())); + + return bv; +} + literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) { const bvt &bv0 = convert_bv(expr.lhs()); @@ -55,112 +154,170 @@ literalt boolbvt::convert_binary_overflow(const binary_overflow_exprt &expr) mult_overflow->lhs().type() == mult_overflow->rhs().type(), "operands of overflow_mult expression shall have same type"); - std::size_t old_size=bv0.size(); - std::size_t new_size=old_size*2; - - // sign/zero extension - const bvt &bv0_extended = bv_utils.extension(bv0, new_size, rep); - const bvt &bv1_extended = bv_utils.extension(bv1, new_size, rep); - - bvt result = bv_utils.multiplier(bv0_extended, bv1_extended, rep); + DATA_INVARIANT(!bv0.empty(), "zero-sized operand"); - if(rep==bv_utilst::representationt::UNSIGNED) - { - bvt bv_overflow; - bv_overflow.reserve(old_size); - - // get top result bits - for(std::size_t i=old_size; i(expr)) { - std::size_t old_size = bv0.size(); - std::size_t new_size = old_size * 2; + DATA_INVARIANT(!bv0.empty(), "zero-sized operand"); + + return shl_overflow_result( + prop, + bv0, + bv1, + rep, + can_cast_type(expr.op1().type()) + ? bv_utilst::representationt::SIGNED + : bv_utilst::representationt::UNSIGNED) + .back(); + } - bvt bv_ext=bv_utils.extension(bv0, new_size, rep); + return SUB::convert_rest(expr); +} - bvt result=bv_utils.shift(bv_ext, bv_utilst::shiftt::SHIFT_LEFT, bv1); +literalt boolbvt::convert_unary_overflow(const unary_overflow_exprt &expr) +{ + if( + const auto unary_minus_overflow = + expr_try_dynamic_cast(expr)) + { + const bvt &bv = convert_bv(unary_minus_overflow->op()); - // a negative shift is undefined; yet this isn't an overflow - literalt neg_shift = rep == bv_utilst::representationt::UNSIGNED - ? const_literal(false) - : bv1.back(); // sign bit + return bv_utils.overflow_negate(bv); + } - // an undefined shift of a non-zero value always results in overflow; the - // use of unsigned comparision is safe here as we cover the signed negative - // case via neg_shift - literalt undef = - bv_utils.rel( - bv1, - ID_gt, - bv_utils.build_constant(old_size, bv1.size()), - bv_utilst::representationt::UNSIGNED); + return SUB::convert_rest(expr); +} + +bvt boolbvt::convert_overflow_result(const overflow_result_exprt &expr) +{ + const typet &type = expr.type(); + const std::size_t width = boolbv_width(type); + + if(expr.id() == ID_overflow_result_unary_minus) + { + const bvt op_bv = convert_bv(expr.op0()); + bvt bv = bv_utils.negate(op_bv); + bv.push_back(bv_utils.overflow_negate(op_bv)); + CHECK_RETURN(bv.size() == width); + return bv; + } + else if(expr.operands().size() != 2) + return conversion_failed(expr); - literalt overflow; + const bvt &bv0 = convert_bv(expr.op0()); + const bvt &bv1 = convert_bv(expr.op1()); + CHECK_RETURN(!bv0.empty() && !bv1.empty()); - if(rep == bv_utilst::representationt::UNSIGNED) + const bv_utilst::representationt rep = + can_cast_type(expr.op0().type()) + ? bv_utilst::representationt::SIGNED + : bv_utilst::representationt::UNSIGNED; + + if(expr.id() == ID_overflow_result_plus) + { + CHECK_RETURN(bv0.size() == bv1.size()); + + if(rep == bv_utilst::representationt::SIGNED) { - // get top result bits - result.erase(result.begin(), result.begin() + old_size); + // An overflow occurs if the signs of the two operands are the same + // and the sign of the sum is the opposite. + bvt bv = bv_utils.add(bv0, bv1); + + literalt old_sign = bv_utils.sign_bit(bv0); + literalt sign_the_same = prop.lequal(old_sign, bv_utils.sign_bit(bv1)); + literalt new_sign = bv_utils.sign_bit(bv); + bv.push_back(prop.land(sign_the_same, prop.lxor(new_sign, old_sign))); - // one of the top bits is non-zero - overflow=prop.lor(result); + CHECK_RETURN(bv.size() == width); + return bv; } else { - // get top result bits plus sign bit - DATA_INVARIANT(old_size != 0, "zero-size operand"); - result.erase(result.begin(), result.begin() + old_size - 1); + // overflow is simply carry-out + bvt bv; + bv.reserve(width); + literalt carry = const_literal(false); - // the sign bit has changed - literalt sign_change=!prop.lequal(bv0.back(), result.front()); + for(std::size_t i = 0; i < bv0.size(); i++) + bv.push_back(bv_utils.full_adder(bv0[i], bv1[i], carry, carry)); - // these need to be either all 1's or all 0's - literalt all_one=prop.land(result); - literalt all_zero=!prop.lor(result); + bv.push_back(carry); - overflow=prop.lor(sign_change, !prop.lor(all_one, all_zero)); + CHECK_RETURN(bv.size() == width); + return bv; } - - // a negative shift isn't an overflow; else check the conditions built - // above - return - prop.land(!neg_shift, prop.lselect(undef, prop.lor(bv0), overflow)); } + else if(expr.id() == ID_overflow_result_minus) + { + CHECK_RETURN(bv0.size() == bv1.size()); - return SUB::convert_rest(expr); -} + if(rep == bv_utilst::representationt::SIGNED) + { + bvt bv1_neg = bv_utils.negate(bv1); + bvt bv = bv_utils.add(bv0, bv1_neg); + + // We special-case x-INT_MIN, which is >=0 if + // x is negative, always representable, and + // thus not an overflow. + literalt op1_is_int_min = bv_utils.is_int_min(bv1); + literalt op0_is_negative = bv_utils.sign_bit(bv0); + + literalt old_sign = bv_utils.sign_bit(bv0); + literalt sign_the_same = + prop.lequal(old_sign, bv_utils.sign_bit(bv1_neg)); + literalt new_sign = bv_utils.sign_bit(bv); + bv.push_back(prop.lselect( + op1_is_int_min, + !op0_is_negative, + prop.land(sign_the_same, prop.lxor(new_sign, old_sign)))); + + CHECK_RETURN(bv.size() == width); + return bv; + } + else if(rep == bv_utilst::representationt::UNSIGNED) + { + // overflow is simply _negated_ carry-out + bvt bv; + bv.reserve(width); + literalt carry = const_literal(true); -literalt boolbvt::convert_unary_overflow(const unary_overflow_exprt &expr) -{ - if( - const auto unary_minus_overflow = - expr_try_dynamic_cast(expr)) + for(std::size_t i = 0; i < bv0.size(); i++) + bv.push_back(bv_utils.full_adder(bv0[i], !bv1[i], carry, carry)); + + bv.push_back(!carry); + + CHECK_RETURN(bv.size() == width); + return bv; + } + else + UNREACHABLE; + } + else if(expr.id() == ID_overflow_result_mult) { - const bvt &bv = convert_bv(unary_minus_overflow->op()); + CHECK_RETURN(bv0.size() == bv1.size()); - return bv_utils.overflow_negate(bv); + bvt bv = mult_overflow_result(prop, bv0, bv1, rep); + + CHECK_RETURN(bv.size() == width); + return bv; + } + else if(expr.id() == ID_overflow_result_shl) + { + bvt bv = shl_overflow_result( + prop, + bv0, + bv1, + rep, + can_cast_type(expr.op1().type()) + ? bv_utilst::representationt::SIGNED + : bv_utilst::representationt::UNSIGNED); + + CHECK_RETURN(bv.size() == width); + return bv; } - return SUB::convert_rest(expr); + return conversion_failed(expr); } diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 874ad8fb05c..14665809dba 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1865,16 +1865,21 @@ void smt2_convt::convert_expr(const exprt &expr) } else if( can_cast_expr(expr) || - can_cast_expr(expr)) + can_cast_expr(expr) || + expr.id() == ID_overflow_result_plus || + expr.id() == ID_overflow_result_minus) { + const bool keep_result = can_cast_expr(expr); + const auto &op0 = to_binary_expr(expr).op0(); const auto &op1 = to_binary_expr(expr).op1(); DATA_INVARIANT( - expr.type().id() == ID_bool, + keep_result || expr.type().id() == ID_bool, "overflow plus and overflow minus expressions shall be of Boolean type"); - bool subtract = can_cast_expr(expr); + bool subtract = can_cast_expr(expr) || + expr.id() == ID_overflow_result_minus; const typet &op_type = op0.type(); std::size_t width=boolbv_width(op_type); @@ -1888,26 +1893,67 @@ void smt2_convt::convert_expr(const exprt &expr) out << ")"; out << " ((_ sign_extend 1) "; convert_expr(op1); - out << ")))) "; // sign_extend, bvadd/sub let2 + out << ")))) "; // sign_extend, bvadd/sub + if(keep_result) + { + if(use_datatypes) + { + const std::string &smt_typename = datatype_map.at(expr.type()); + + // use the constructor for the Z3 datatype + out << "(mk-" << smt_typename; + } + else + out << "(concat"; + + out << " ((_ extract " << width - 1 << " 0) ?sum) "; + if(!use_datatypes) + out << "(ite "; + } out << "(not (= " "((_ extract " << width << " " << width << ") ?sum) " "((_ extract " << (width-1) << " " << (width-1) << ") ?sum)"; - out << ")))"; // =, not, let + out << "))"; // =, not + if(keep_result) + { + if(!use_datatypes) + out << " #b1 #b0)"; + out << ")"; // concat + } + out << ")"; // let } else if(op_type.id()==ID_unsignedbv || op_type.id()==ID_pointer) { // overflow is simply carry-out - out << "(= "; - out << "((_ extract " << width << " " << width << ") "; - out << "(" << (subtract?"bvsub":"bvadd"); + out << "(let ((?sum (" << (subtract ? "bvsub" : "bvadd"); out << " ((_ zero_extend 1) "; convert_expr(op0); out << ")"; out << " ((_ zero_extend 1) "; convert_expr(op1); - out << ")))"; // zero_extend, bvsub/bvadd, extract - out << " #b1)"; // = + out << "))))"; // zero_extend, bvsub/bvadd + if(keep_result && !use_datatypes) + out << " ?sum"; + else + { + if(keep_result && use_datatypes) + { + const std::string &smt_typename = datatype_map.at(expr.type()); + + // use the constructor for the Z3 datatype + out << "(mk-" << smt_typename; + out << " ((_ extract " << width - 1 << " 0) ?sum) "; + } + + out << "(= "; + out << "((_ extract " << width << " " << width << ") ?sum)"; + out << "#b1)"; // = + + if(keep_result && use_datatypes) + out << ")"; // mk + } + out << ")"; // let } else INVARIANT_WITH_DIAGNOSTICS( @@ -1916,13 +1962,16 @@ void smt2_convt::convert_expr(const exprt &expr) op_type.id_string()); } else if( - const auto mult_overflow = expr_try_dynamic_cast(expr)) + can_cast_expr(expr) || + expr.id() == ID_overflow_result_mult) { - const auto &op0 = mult_overflow->op0(); - const auto &op1 = mult_overflow->op1(); + const bool keep_result = can_cast_expr(expr); + + const auto &op0 = to_binary_expr(expr).op0(); + const auto &op1 = to_binary_expr(expr).op1(); DATA_INVARIANT( - mult_overflow->type().id() == ID_bool, + keep_result || expr.type().id() == ID_bool, "overflow mult expression shall be of Boolean type"); // No better idea than to multiply with double the bits and then compare @@ -1938,18 +1987,65 @@ void smt2_convt::convert_expr(const exprt &expr) out << ") ((_ sign_extend " << width << ") "; convert_expr(op1); out << ")) )) "; + if(keep_result) + { + if(use_datatypes) + { + const std::string &smt_typename = datatype_map.at(expr.type()); + + // use the constructor for the Z3 datatype + out << "(mk-" << smt_typename; + } + else + out << "(concat"; + + out << " ((_ extract " << width - 1 << " 0) prod) "; + if(!use_datatypes) + out << "(ite "; + } out << "(or (bvsge prod (_ bv" << power(2, width-1) << " " << width*2 << "))"; - out << " (bvslt prod (bvneg (_ bv" << power(2, width-1) << " " - << width*2 << ")))))"; + out << " (bvslt prod (bvneg (_ bv" << power(2, width - 1) << " " + << width * 2 << "))))"; + if(keep_result) + { + if(!use_datatypes) + out << " #b1 #b0)"; + out << ")"; // concat + } + out << ")"; } else if(op_type.id()==ID_unsignedbv) { - out << "(bvuge (bvmul ((_ zero_extend " << width << ") "; + out << "(let ((prod (bvmul ((_ zero_extend " << width << ") "; convert_expr(op0); out << ") ((_ zero_extend " << width << ") "; convert_expr(op1); - out << ")) (_ bv" << power(2, width) << " " << width*2 << "))"; + out << ")))) "; + if(keep_result) + { + if(use_datatypes) + { + const std::string &smt_typename = datatype_map.at(expr.type()); + + // use the constructor for the Z3 datatype + out << "(mk-" << smt_typename; + } + else + out << "(concat"; + + out << " ((_ extract " << width - 1 << " 0) prod) "; + if(!use_datatypes) + out << "(ite "; + } + out << "(bvuge prod (_ bv" << power(2, width) << " " << width * 2 << "))"; + if(keep_result) + { + if(!use_datatypes) + out << " #b1 #b0)"; + out << ")"; // concat + } + out << ")"; } else INVARIANT_WITH_DIAGNOSTICS( @@ -2901,6 +2997,8 @@ void smt2_convt::convert_struct(const struct_exprt &expr) // may need to flatten array-theory arrays in there if(op.type().id() == ID_array) flatten_array(op); + else if(op.type().id() == ID_bool) + flatten2bv(op); else convert_expr(op); @@ -4228,10 +4326,14 @@ void smt2_convt::convert_member(const member_exprt &expr) // we extract const auto member_offset = boolbv_width.get_member(struct_type, name); + if(expr.type().id() == ID_bool) + out << "(= "; out << "((_ extract " << (member_offset.offset + member_offset.width - 1) << " " << member_offset.offset << ") "; convert_expr(struct_op); out << ")"; + if(expr.type().id() == ID_bool) + out << " #b1)"; } } else if( diff --git a/src/util/bitvector_expr.cpp b/src/util/bitvector_expr.cpp index ddc7296f943..66230ae9847 100644 --- a/src/util/bitvector_expr.cpp +++ b/src/util/bitvector_expr.cpp @@ -152,3 +152,60 @@ exprt bitreverse_exprt::lower() const return let_exprt{to_reverse, op(), concatenation_exprt{result_bits, type()}}; } + +exprt plus_overflow_exprt::lower() const +{ + std::size_t lhs_ssize = to_bitvector_type(lhs().type()).get_width(); + if(lhs().type().id() == ID_unsignedbv) + ++lhs_ssize; + std::size_t rhs_ssize = to_bitvector_type(rhs().type()).get_width(); + if(rhs().type().id() == ID_unsignedbv) + ++rhs_ssize; + + std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1; + signedbv_typet ssize_type{ssize}; + plus_exprt exact_result{ + typecast_exprt{lhs(), ssize_type}, typecast_exprt{rhs(), ssize_type}}; + + return notequal_exprt{ + typecast_exprt{typecast_exprt{exact_result, lhs().type()}, ssize_type}, + exact_result}; +} + +exprt minus_overflow_exprt::lower() const +{ + std::size_t lhs_ssize = to_bitvector_type(lhs().type()).get_width(); + if(lhs().type().id() == ID_unsignedbv) + ++lhs_ssize; + std::size_t rhs_ssize = to_bitvector_type(rhs().type()).get_width(); + if(rhs().type().id() == ID_unsignedbv) + ++rhs_ssize; + + std::size_t ssize = std::max(lhs_ssize, rhs_ssize) + 1; + signedbv_typet ssize_type{ssize}; + minus_exprt exact_result{ + typecast_exprt{lhs(), ssize_type}, typecast_exprt{rhs(), ssize_type}}; + + return notequal_exprt{ + typecast_exprt{typecast_exprt{exact_result, lhs().type()}, ssize_type}, + exact_result}; +} + +exprt mult_overflow_exprt::lower() const +{ + std::size_t lhs_ssize = to_bitvector_type(lhs().type()).get_width(); + if(lhs().type().id() == ID_unsignedbv) + ++lhs_ssize; + std::size_t rhs_ssize = to_bitvector_type(rhs().type()).get_width(); + if(rhs().type().id() == ID_unsignedbv) + ++rhs_ssize; + + std::size_t ssize = lhs_ssize + rhs_ssize; + signedbv_typet ssize_type{ssize}; + mult_exprt exact_result{ + typecast_exprt{lhs(), ssize_type}, typecast_exprt{rhs(), ssize_type}}; + + return notequal_exprt{ + typecast_exprt{typecast_exprt{exact_result, lhs().type()}, ssize_type}, + exact_result}; +} diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h index ae6fe906ee8..360501ef5f1 100644 --- a/src/util/bitvector_expr.h +++ b/src/util/bitvector_expr.h @@ -801,6 +801,10 @@ class plus_overflow_exprt : public binary_overflow_exprt : binary_overflow_exprt(std::move(_lhs), ID_overflow_plus, std::move(_rhs)) { } + + /// Lower a plus_overflow_exprt to arithmetic and logic expressions. + /// \return Semantically equivalent expression + exprt lower() const; }; template <> @@ -816,6 +820,10 @@ class minus_overflow_exprt : public binary_overflow_exprt : binary_overflow_exprt(std::move(_lhs), ID_overflow_minus, std::move(_rhs)) { } + + /// Lower a minus_overflow_exprt to arithmetic and logic expressions. + /// \return Semantically equivalent expression + exprt lower() const; }; template <> @@ -831,6 +839,10 @@ class mult_overflow_exprt : public binary_overflow_exprt : binary_overflow_exprt(std::move(_lhs), ID_overflow_mult, std::move(_rhs)) { } + + /// Lower a mult_overflow_exprt to arithmetic and logic expressions. + /// \return Semantically equivalent expression + exprt lower() const; }; template <> @@ -1287,4 +1299,132 @@ inline saturating_minus_exprt &to_saturating_minus_expr(exprt &expr) return ret; } +/// \brief An expression returning both the result of the arithmetic operation +/// under wrap-around semantics as well as a Boolean to signify overflow. +class overflow_result_exprt : public expr_protectedt +{ +public: + overflow_result_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs) + : expr_protectedt( + make_id(kind), + struct_typet{ + {{ID_value, _lhs.type()}, + {"overflow-" + id2string(kind), bool_typet{}}}}, + {_lhs, std::move(_rhs)}) + { + INVARIANT( + valid_id(id()), + "The kind used to construct overflow_result_exprt should be in the set " + "of expected valid kinds."); + } + + overflow_result_exprt(exprt _op, const irep_idt &kind) + : expr_protectedt( + make_id(kind), + struct_typet{ + {{ID_value, _op.type()}, + {"overflow-" + id2string(kind), bool_typet{}}}}, + {_op}) + { + INVARIANT( + valid_id(id()), + "The kind used to construct overflow_result_exprt should be in the set " + "of expected valid kinds."); + } + + // make op0 and op1 public + using exprt::op0; + using exprt::op1; + + const exprt &op2() const = delete; + exprt &op2() = delete; + const exprt &op3() const = delete; + exprt &op3() = delete; + + static void check( + const exprt &expr, + const validation_modet vm = validation_modet::INVARIANT) + { + if(expr.id() != ID_overflow_result_unary_minus) + binary_exprt::check(expr, vm); + + if( + expr.id() != ID_overflow_result_unary_minus && + expr.id() != ID_overflow_result_shl) + { + const binary_exprt &binary_expr = to_binary_expr(expr); + DATA_CHECK( + vm, + binary_expr.lhs().type() == binary_expr.rhs().type(), + "operand types must match"); + } + } + + static void validate( + const exprt &expr, + const namespacet &, + const validation_modet vm = validation_modet::INVARIANT) + { + check(expr, vm); + } + + /// Returns true iff \p id is a valid identifier of an `overflow_exprt`. + static bool valid_id(const irep_idt &id) + { + return id == ID_overflow_result_plus || id == ID_overflow_result_mult || + id == ID_overflow_result_minus || id == ID_overflow_result_shl || + id == ID_overflow_result_unary_minus; + } + +private: + static irep_idt make_id(const irep_idt &kind) + { + return "overflow_result-" + id2string(kind); + } +}; + +template <> +inline bool can_cast_expr(const exprt &base) +{ + return overflow_result_exprt::valid_id(base.id()); +} + +inline void validate_expr(const overflow_result_exprt &value) +{ + if(value.id() == ID_overflow_result_unary_minus) + { + validate_operands( + value, 1, "unary overflow expression must have two operands"); + } + else + { + validate_operands( + value, 2, "binary overflow expression must have two operands"); + } +} + +/// \brief Cast an exprt to a \ref overflow_result_exprt +/// +/// \a expr must be known to be \ref overflow_result_exprt. +/// +/// \param expr: Source expression +/// \return Object of type \ref overflow_result_exprt +inline const overflow_result_exprt &to_overflow_result_expr(const exprt &expr) +{ + PRECONDITION(overflow_result_exprt::valid_id(expr.id())); + const overflow_result_exprt &ret = + static_cast(expr); + validate_expr(ret); + return ret; +} + +/// \copydoc to_overflow_result_expr(const exprt &) +inline overflow_result_exprt &to_overflow_result_expr(exprt &expr) +{ + PRECONDITION(overflow_result_exprt::valid_id(expr.id())); + overflow_result_exprt &ret = static_cast(expr); + validate_expr(ret); + return ret; +} + #endif // CPROVER_UTIL_BITVECTOR_EXPR_H diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 13855affb7e..1648d003008 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -871,6 +871,11 @@ IREP_ID_TWO(C_flexible_array_member, #flexible_array_member) IREP_ID_ONE(state) IREP_ID_ONE(evaluate) IREP_ID_ONE(update_state) +IREP_ID_TWO(overflow_result_plus, overflow_result-+) +IREP_ID_TWO(overflow_result_minus, overflow_result--) +IREP_ID_TWO(overflow_result_mult, overflow_result-*) +IREP_ID_TWO(overflow_result_shl, overflow_result-shl) +IREP_ID_TWO(overflow_result_unary_minus, overflow_result-unary-) // Projects depending on this code base that wish to extend the list of // available ids should provide a file local_irep_ids.def in their source tree diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 0302da75c94..9c67d4862a9 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -2295,6 +2295,185 @@ simplify_exprt::simplify_overflow_unary(const unary_overflow_exprt &expr) return false_exprt{}; } +simplify_exprt::resultt<> +simplify_exprt::simplify_overflow_result(const overflow_result_exprt &expr) +{ + if(expr.id() == ID_overflow_result_unary_minus) + { + // zero is a neutral element + if(expr.op0().is_zero()) + return struct_exprt{{expr.op0(), false_exprt{}}, expr.type()}; + + // catch some cases over mathematical types + const irep_idt &op_type_id = expr.op0().type().id(); + if( + op_type_id == ID_integer || op_type_id == ID_rational || + op_type_id == ID_real) + { + return struct_exprt{{expr.op0(), false_exprt{}}, expr.type()}; + } + + // always an overflow for natural numbers, but the result is not + // representable + if(op_type_id == ID_natural) + return unchanged(expr); + + // we only handle constants over signedbv/unsignedbv for the remaining cases + if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv) + return unchanged(expr); + + if(!expr.op0().is_constant()) + return unchanged(expr); + + const auto op_value = numeric_cast(expr.op0()); + if(!op_value.has_value()) + return unchanged(expr); + + mp_integer no_overflow_result = -*op_value; + + const std::size_t width = to_bitvector_type(expr.op0().type()).get_width(); + const integer_bitvector_typet bv_type{op_type_id, width}; + if( + no_overflow_result < bv_type.smallest() || + no_overflow_result > bv_type.largest()) + { + return struct_exprt{ + {from_integer(no_overflow_result, expr.op0().type()), true_exprt{}}, + expr.type()}; + } + else + { + return struct_exprt{ + {from_integer(no_overflow_result, expr.op0().type()), false_exprt{}}, + expr.type()}; + } + } + else + { + // When one operand is zero, an overflow can only occur for a subtraction + // from zero. + if(expr.op0().is_zero()) + { + if( + expr.id() == ID_overflow_result_plus || + expr.id() == ID_overflow_result_shl) + { + return struct_exprt{{expr.op1(), false_exprt{}}, expr.type()}; + } + else if(expr.id() == ID_overflow_result_mult) + { + return struct_exprt{ + {from_integer(0, expr.op0().type()), false_exprt{}}, expr.type()}; + } + } + else if(expr.op1().is_zero()) + { + if( + expr.id() == ID_overflow_result_plus || + expr.id() == ID_overflow_result_minus || + expr.id() == ID_overflow_result_shl) + { + return struct_exprt{{expr.op0(), false_exprt{}}, expr.type()}; + } + else + { + return struct_exprt{ + {from_integer(0, expr.op0().type()), false_exprt{}}, expr.type()}; + } + } + + // One is neutral element for multiplication + if( + expr.id() == ID_overflow_result_mult && + (expr.op0().is_one() || expr.op1().is_one())) + { + return struct_exprt{ + {expr.op0().is_one() ? expr.op1() : expr.op0(), false_exprt{}}, + expr.type()}; + } + + // we only handle the case of same operand types + if( + expr.id() != ID_overflow_result_shl && + expr.op0().type() != expr.op1().type()) + { + return unchanged(expr); + } + + // catch some cases over mathematical types + const irep_idt &op_type_id = expr.op0().type().id(); + if( + expr.id() != ID_overflow_result_shl && + (op_type_id == ID_integer || op_type_id == ID_rational || + op_type_id == ID_real)) + { + irep_idt id = + expr.id() == ID_overflow_result_plus + ? ID_plus + : expr.id() == ID_overflow_result_minus ? ID_minus : ID_mult; + return struct_exprt{ + {simplify_node(binary_exprt{expr.op0(), id, expr.op1()}), + false_exprt{}}, + expr.type()}; + } + + if( + (expr.id() == ID_overflow_result_plus || + expr.id() == ID_overflow_result_mult) && + op_type_id == ID_natural) + { + return struct_exprt{ + {simplify_node(binary_exprt{ + expr.op0(), + expr.id() == ID_overflow_result_plus ? ID_plus : ID_mult, + expr.op1()}), + false_exprt{}}, + expr.type()}; + } + + // we only handle constants over signedbv/unsignedbv for the remaining cases + if(op_type_id != ID_signedbv && op_type_id != ID_unsignedbv) + return unchanged(expr); + + if(!expr.op0().is_constant() || !expr.op1().is_constant()) + return unchanged(expr); + + const auto op0_value = numeric_cast(expr.op0()); + const auto op1_value = numeric_cast(expr.op1()); + if(!op0_value.has_value() || !op1_value.has_value()) + return unchanged(expr); + + mp_integer no_overflow_result; + if(expr.id() == ID_overflow_result_plus) + no_overflow_result = *op0_value + *op1_value; + else if(expr.id() == ID_overflow_result_minus) + no_overflow_result = *op0_value - *op1_value; + else if(expr.id() == ID_overflow_result_mult) + no_overflow_result = *op0_value * *op1_value; + else if(expr.id() == ID_overflow_result_shl) + no_overflow_result = *op0_value << *op1_value; + else + UNREACHABLE; + + const std::size_t width = to_bitvector_type(expr.op0().type()).get_width(); + const integer_bitvector_typet bv_type{op_type_id, width}; + if( + no_overflow_result < bv_type.smallest() || + no_overflow_result > bv_type.largest()) + { + return struct_exprt{ + {from_integer(no_overflow_result, expr.op0().type()), true_exprt{}}, + expr.type()}; + } + else + { + return struct_exprt{ + {from_integer(no_overflow_result, expr.op0().type()), false_exprt{}}, + expr.type()}; + } + } +} + bool simplify_exprt::simplify_node_preorder(exprt &expr) { bool result=true; @@ -2559,6 +2738,12 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node) { r = simplify_overflow_unary(*unary_overflow); } + else if( + const auto overflow_result = + expr_try_dynamic_cast(expr)) + { + r = simplify_overflow_result(*overflow_result); + } else if(expr.id() == ID_bitreverse) { r = simplify_bitreverse(to_bitreverse_expr(expr)); diff --git a/src/util/simplify_expr_class.h b/src/util/simplify_expr_class.h index 0e536cd5efb..4cffa7bb2e2 100644 --- a/src/util/simplify_expr_class.h +++ b/src/util/simplify_expr_class.h @@ -59,6 +59,7 @@ class mult_exprt; class namespacet; class not_exprt; class object_size_exprt; +class overflow_result_exprt; class plus_exprt; class pointer_object_exprt; class pointer_offset_exprt; @@ -203,6 +204,12 @@ class simplify_exprt /// type of the operand has an infinite domain. NODISCARD resultt<> simplify_overflow_unary(const unary_overflow_exprt &); + /// Try to simplify overflow_result-+, overflow_result-*, overflow_result--, + /// overflow_result-shl, overflow_result-unary--. + /// Simplification will be possible when the operands are constants or the + /// types of the operands have infinite domains. + NODISCARD resultt<> simplify_overflow_result(const overflow_result_exprt &); + /// Attempt to simplify mathematical function applications if we have /// enough information to do so. Currently focused on constant comparisons. NODISCARD resultt<>