From 97cb8a30a979a50294af6f662a07e3a4716b076f Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 19 Mar 2024 13:29:08 -0700 Subject: [PATCH] simplify extractbits_exprt representation The current representation of extractbits_exprt stores both the upper and lower indices of the range that is to be extracted, and their difference plus one in form of the width of the type of the expression. This removes the upper index, as it can be deduced from the lower index and the width of the result. The key benefit is reducing burden on the user of the class, who a) doesn't have to remember which index comes first, and b) doesn't have to do the calculation of the upper index. --- src/ansi-c/expr2c.cpp | 13 +++++- src/ansi-c/goto_check_c.cpp | 1 - src/cpp/expr2cpp.cpp | 14 ------- src/solvers/flattening/boolbv_extractbits.cpp | 31 ++++---------- src/solvers/floatbv/float_bv.cpp | 40 +++++++----------- src/solvers/smt2/smt2_conv.cpp | 18 +++----- src/solvers/smt2/smt2_parser.cpp | 7 ++-- .../smt2_incremental/convert_expr_to_smt.cpp | 12 ++++-- .../encoding/struct_encoding.cpp | 6 +-- .../string_constraint_generator_float.cpp | 5 +-- src/util/bitvector_expr.cpp | 9 +--- src/util/bitvector_expr.h | 36 +++++----------- src/util/expr_util.cpp | 15 +++---- src/util/lower_byte_operators.cpp | 23 ++++------- src/util/simplify_expr_int.cpp | 41 ++++++++++--------- .../smt2_incremental/convert_expr_to_smt.cpp | 4 +- .../encoding/struct_encoding.cpp | 32 +++++++-------- unit/util/simplify_expr.cpp | 2 +- 18 files changed, 120 insertions(+), 189 deletions(-) diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 6ca3038e1a9..40eb5785410 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -3494,9 +3494,18 @@ expr2ct::convert_extractbits(const extractbits_exprt &src, unsigned precedence) { std::string dest = convert_with_precedence(src.src(), precedence); dest+='['; - dest += convert_with_precedence(src.upper(), precedence); + auto expr_width_opt = pointer_offset_bits(src.type(), ns); + if(expr_width_opt.has_value()) + { + auto upper = plus_exprt{ + src.index(), + from_integer(expr_width_opt.value() - 1, src.index().type())}; + dest += convert_with_precedence(upper, precedence); + } + else + dest += "?"; dest+=", "; - dest += convert_with_precedence(src.lower(), precedence); + dest += convert_with_precedence(src.index(), precedence); dest+=']'; return dest; diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp index 992d9af33e7..1aa97aef6e3 100644 --- a/src/ansi-c/goto_check_c.cpp +++ b/src/ansi-c/goto_check_c.cpp @@ -973,7 +973,6 @@ void goto_check_ct::integer_overflow_check( const exprt top_bits = extractbits_exprt( op_ext_shifted, - new_type.get_width() - 1, new_type.get_width() - number_of_top_bits, unsignedbv_typet(number_of_top_bits)); diff --git a/src/cpp/expr2cpp.cpp b/src/cpp/expr2cpp.cpp index 37d1c6bc09b..1144b0fb0ce 100644 --- a/src/cpp/expr2cpp.cpp +++ b/src/cpp/expr2cpp.cpp @@ -33,7 +33,6 @@ class expr2cppt:public expr2ct std::string convert_cpp_this(); std::string convert_cpp_new(const exprt &src); std::string convert_extractbit(const exprt &src); - std::string convert_extractbits(const exprt &src); std::string convert_code_cpp_delete(const exprt &src, unsigned indent); std::string convert_code_cpp_new(const exprt &src, unsigned indent); std::string convert_struct(const exprt &src, unsigned &precedence) override; @@ -433,11 +432,6 @@ std::string expr2cppt::convert_with_precedence( precedence = 15; return convert_extractbit(src); } - else if(src.id()==ID_extractbits) - { - precedence = 15; - return convert_extractbits(src); - } else if(src.id()==ID_side_effect && (src.get(ID_statement)==ID_cpp_new || src.get(ID_statement)==ID_cpp_new_array)) @@ -489,14 +483,6 @@ std::string expr2cppt::convert_extractbit(const exprt &src) "]"; } -std::string expr2cppt::convert_extractbits(const exprt &src) -{ - const auto &extractbits_expr = to_extractbits_expr(src); - return convert(extractbits_expr.src()) + ".range(" + - convert(extractbits_expr.upper()) + "," + - convert(extractbits_expr.lower()) + ")"; -} - std::string expr2cpp(const exprt &expr, const namespacet &ns) { expr2cppt expr2cpp(ns); diff --git a/src/solvers/flattening/boolbv_extractbits.cpp b/src/solvers/flattening/boolbv_extractbits.cpp index 3d510b4ec0d..566d030606d 100644 --- a/src/solvers/flattening/boolbv_extractbits.cpp +++ b/src/solvers/flattening/boolbv_extractbits.cpp @@ -17,43 +17,28 @@ bvt boolbvt::convert_extractbits(const extractbits_exprt &expr) auto const &src_bv = convert_bv(expr.src()); - auto const maybe_upper_as_int = numeric_cast(expr.upper()); - auto const maybe_lower_as_int = numeric_cast(expr.lower()); + auto const maybe_index_as_int = numeric_cast(expr.index()); // We only do constants for now. // Should implement a shift here. - if(!maybe_upper_as_int.has_value() || !maybe_lower_as_int.has_value()) + if(!maybe_index_as_int.has_value()) return conversion_failed(expr); - auto upper_as_int = maybe_upper_as_int.value(); - auto lower_as_int = maybe_lower_as_int.value(); + auto index_as_int = maybe_index_as_int.value(); DATA_INVARIANT_WITH_DIAGNOSTICS( - upper_as_int >= 0 && upper_as_int < src_bv.size(), - "upper end of extracted bits must be within the bitvector", + index_as_int >= 0 && index_as_int < src_bv.size(), + "index of extractbits must be within the bitvector", expr.find_source_location(), irep_pretty_diagnosticst{expr}); DATA_INVARIANT_WITH_DIAGNOSTICS( - lower_as_int >= 0 && lower_as_int < src_bv.size(), - "lower end of extracted bits must be within the bitvector", + index_as_int + bv_width - 1 < src_bv.size(), + "index+width-1 of extractbits must be within the bitvector", expr.find_source_location(), irep_pretty_diagnosticst{expr}); - DATA_INVARIANT( - lower_as_int <= upper_as_int, - "upper bound must be greater or equal to lower bound"); - - // now lower_as_int <= upper_as_int - - DATA_INVARIANT_WITH_DIAGNOSTICS( - (upper_as_int - lower_as_int + 1) == bv_width, - "the difference between upper and lower end of the range must have the " - "same width as the resulting bitvector type", - expr.find_source_location(), - irep_pretty_diagnosticst{expr}); - - const std::size_t offset = numeric_cast_v(lower_as_int); + const std::size_t offset = numeric_cast_v(index_as_int); bvt result_bv(src_bv.begin() + offset, src_bv.begin() + offset + bv_width); diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp index 3611abd3632..12e87f923bf 100644 --- a/src/solvers/floatbv/float_bv.cpp +++ b/src/solvers/floatbv/float_bv.cpp @@ -92,8 +92,7 @@ exprt float_bvt::convert(const exprt &expr) const return nil_exprt{}; } - return extractbits_exprt{ - to_typecast_expr(expr).op(), dest_type.get_width() - 1, 0, dest_type}; + return extractbits_exprt{to_typecast_expr(expr).op(), 0, dest_type}; } else if(expr.id()==ID_floatbv_plus) { @@ -669,12 +668,11 @@ exprt float_bvt::limit_distance( return dist; const extractbits_exprt upper_bits( - dist, dist_width - 1, nb_bits, unsignedbv_typet(dist_width - nb_bits)); + dist, nb_bits, unsignedbv_typet(dist_width - nb_bits)); const equal_exprt upper_bits_zero( upper_bits, from_integer(0, upper_bits.type())); - const extractbits_exprt lower_bits( - dist, nb_bits - 1, 0, unsignedbv_typet(nb_bits)); + const extractbits_exprt lower_bits(dist, 0, unsignedbv_typet(nb_bits)); return if_exprt( upper_bits_zero, @@ -924,9 +922,7 @@ exprt float_bvt::get_exponent( const exprt &src, const ieee_float_spect &spec) { - return extractbits_exprt( - src, spec.f+spec.e-1, spec.f, - unsignedbv_typet(spec.e)); + return extractbits_exprt(src, spec.f, unsignedbv_typet(spec.e)); } /// Gets the fraction without hidden bit in a floating-point bit-vector src @@ -934,9 +930,7 @@ exprt float_bvt::get_fraction( const exprt &src, const ieee_float_spect &spec) { - return extractbits_exprt( - src, spec.f-1, 0, - unsignedbv_typet(spec.f)); + return extractbits_exprt(src, 0, unsignedbv_typet(spec.f)); } exprt float_bvt::isnan( @@ -975,10 +969,7 @@ void float_bvt::normalization_shift( // check if first 'distance'-many bits are zeros const extractbits_exprt prefix( - fraction, - fraction_bits - 1, - fraction_bits - distance, - unsignedbv_typet(distance)); + fraction, fraction_bits - distance, unsignedbv_typet(distance)); const equal_exprt prefix_is_zero(prefix, from_integer(0, prefix.type())); // If so, shift the zeros out left by 'distance'. @@ -1147,7 +1138,7 @@ exprt float_bvt::fraction_rounding_decision( // We keep most-significant bits, and thus the tail is made // of least-significant bits. const extractbits_exprt tail( - fraction, extra_bits - 2, 0, unsignedbv_typet(extra_bits - 2 + 1)); + fraction, 0, unsignedbv_typet(extra_bits - 2 + 1)); sticky_bit=notequal_exprt(tail, from_integer(0, tail.type())); } @@ -1216,9 +1207,8 @@ void float_bvt::round_fraction( fraction_size, result.sign, result.fraction, rounding_mode_bits); // chop off all the extra bits - result.fraction=extractbits_exprt( - result.fraction, result_fraction_size-1, extra_bits, - unsignedbv_typet(fraction_size)); + result.fraction = extractbits_exprt( + result.fraction, extra_bits, unsignedbv_typet(fraction_size)); #if 0 // *** does not catch when the overflow goes subnormal -> normal *** @@ -1306,8 +1296,8 @@ void float_bvt::round_exponent( else // exponent gets smaller -- chop off top bits { exprt old_exponent=result.exponent; - result.exponent= - extractbits_exprt(result.exponent, spec.e-1, 0, signedbv_typet(spec.e)); + result.exponent = + extractbits_exprt(result.exponent, 0, signedbv_typet(spec.e)); // max_exponent is the maximum representable // i.e. 1 higher than the maximum possible for a normal number @@ -1374,10 +1364,8 @@ float_bvt::biased_floatt float_bvt::bias( const extractbit_exprt hidden_bit(src.fraction, spec.f); const not_exprt denormal(hidden_bit); - result.fraction= - extractbits_exprt( - src.fraction, spec.f-1, 0, - unsignedbv_typet(spec.f)); + result.fraction = + extractbits_exprt(src.fraction, 0, unsignedbv_typet(spec.f)); // make exponent zero if its denormal // (includes zero) @@ -1490,7 +1478,7 @@ exprt float_bvt::sticky_right_shift( exprt lost_bits; if(d<=width) - lost_bits=extractbits_exprt(result, d-1, 0, unsignedbv_typet(d)); + lost_bits = extractbits_exprt(result, 0, unsignedbv_typet(d)); else lost_bits=result; diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 16967c683cc..0d63d2863c5 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -1831,22 +1831,14 @@ void smt2_convt::convert_expr(const exprt &expr) else if(expr.id()==ID_extractbits) { const extractbits_exprt &extractbits_expr = to_extractbits_expr(expr); + auto width = boolbv_width(expr.type()); - if( - extractbits_expr.upper().is_constant() && - extractbits_expr.lower().is_constant()) + if(extractbits_expr.index().is_constant()) { - mp_integer op1_i = - numeric_cast_v(to_constant_expr(extractbits_expr.upper())); - mp_integer op2_i = - numeric_cast_v(to_constant_expr(extractbits_expr.lower())); - - if(op2_i>op1_i) - std::swap(op1_i, op2_i); - - // now op1_i>=op2_i + mp_integer index_i = + numeric_cast_v(to_constant_expr(extractbits_expr.index())); - out << "((_ extract " << op1_i << " " << op2_i << ") "; + out << "((_ extract " << (width + index_i - 1) << " " << index_i << ") "; flatten2bv(extractbits_expr.src()); out << ")"; } diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index 953be798c47..451436e04a0 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -638,15 +638,14 @@ exprt smt2_parsert::function_application() if(op.size()!=1) throw error("extract takes one operand"); - auto upper_e=from_integer(upper, integer_typet()); - auto lower_e=from_integer(lower, integer_typet()); - if(upper(extract_bits.upper()); - const auto lower_value = numeric_cast(extract_bits.lower()); - if(upper_value && lower_value) - return smt_bit_vector_theoryt::extract(*upper_value, *lower_value)(from); + const auto bit_vector_sort = + convert_type_to_smt_sort(extract_bits.type()).cast(); + INVARIANT( + bit_vector_sort, "Extract can only be applied to bit vector terms."); + const auto index_value = numeric_cast(extract_bits.index()); + if(index_value) + return smt_bit_vector_theoryt::extract( + *index_value + bit_vector_sort->bit_width() - 1, *index_value)(from); UNIMPLEMENTED_FEATURE( "Generation of SMT formula for extract bits expression: " + extract_bits.pretty()); diff --git a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp index 592c9b9b12f..f57b943ff81 100644 --- a/src/solvers/smt2_incremental/encoding/struct_encoding.cpp +++ b/src/solvers/smt2_incremental/encoding/struct_encoding.cpp @@ -195,7 +195,6 @@ static std::size_t count_trailing_bit_width( exprt struct_encodingt::encode_member(const member_exprt &member_expr) const { const auto &type = ns.get().follow(member_expr.compound().type()); - const auto member_bits_width = (*boolbv_width)(member_expr.type()); const auto offset_bits = [&]() -> std::size_t { if(can_cast_type(type)) return 0; @@ -204,10 +203,7 @@ exprt struct_encodingt::encode_member(const member_exprt &member_expr) const struct_type, member_expr.get_component_name(), *boolbv_width); }(); return extractbits_exprt{ - member_expr.compound(), - offset_bits + member_bits_width - 1, - offset_bits, - member_expr.type()}; + member_expr.compound(), offset_bits, member_expr.type()}; } exprt struct_encodingt::encode(exprt expr) const diff --git a/src/solvers/strings/string_constraint_generator_float.cpp b/src/solvers/strings/string_constraint_generator_float.cpp index ce729b7030f..ecc5e044b79 100644 --- a/src/solvers/strings/string_constraint_generator_float.cpp +++ b/src/solvers/strings/string_constraint_generator_float.cpp @@ -28,8 +28,7 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com /// in octuple precision. exprt get_exponent(const exprt &src, const ieee_float_spect &spec) { - const extractbits_exprt exp_bits( - src, spec.f + spec.e - 1, spec.f, unsignedbv_typet(spec.e)); + const extractbits_exprt exp_bits(src, spec.f, unsignedbv_typet(spec.e)); // Exponent is in biased form (numbers from -128 to 127 are encoded with // integer from 0 to 255) we have to remove the bias. @@ -44,7 +43,7 @@ exprt get_exponent(const exprt &src, const ieee_float_spect &spec) /// \return An unsigned value representing the fractional part. exprt get_fraction(const exprt &src, const ieee_float_spect &spec) { - return extractbits_exprt(src, spec.f - 1, 0, unsignedbv_typet(spec.f)); + return extractbits_exprt(src, 0, unsignedbv_typet(spec.f)); } /// Gets the significand as a java integer, looking for the hidden bit. diff --git a/src/util/bitvector_expr.cpp b/src/util/bitvector_expr.cpp index c62a50e594c..940fa07a0b1 100644 --- a/src/util/bitvector_expr.cpp +++ b/src/util/bitvector_expr.cpp @@ -30,16 +30,11 @@ extractbit_exprt::extractbit_exprt(exprt _src, const std::size_t _index) extractbits_exprt::extractbits_exprt( exprt _src, - const std::size_t _upper, - const std::size_t _lower, + const std::size_t _index, typet _type) : expr_protectedt(ID_extractbits, std::move(_type)) { - PRECONDITION(_upper >= _lower); - add_to_operands( - std::move(_src), - from_integer(_upper, integer_typet()), - from_integer(_lower, integer_typet())); + add_to_operands(std::move(_src), from_integer(_index, integer_typet())); } exprt update_bit_exprt::lower() const diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h index 1276bf287ff..55a100c9bb5 100644 --- a/src/util/bitvector_expr.h +++ b/src/util/bitvector_expr.h @@ -447,54 +447,40 @@ inline extractbit_exprt &to_extractbit_expr(exprt &expr) class extractbits_exprt : public expr_protectedt { public: - /// Extract the bits [\p _lower .. \p _upper] from \p _src to produce a result - /// of type \p _type. Note that this specifies a closed interval, i.e., both - /// bits \p _lower and \p _upper are included. Indices count from the - /// least-significant bit, and are not affected by endianness. - /// The ordering upper-lower matches what SMT-LIB uses. - extractbits_exprt(exprt _src, exprt _upper, exprt _lower, typet _type) + /// Extract the bits [\p _index .. \p _index + width - 1] from \p _src + /// to produce a result of type \p _type where width is the number of bits + /// of \p _type. Note that this specifies a closed interval, i.e., both + /// bits \p _lower and \p _index + width - 1 are included. Indices count + /// from the least-significant bit, and are not affected by endianness. + extractbits_exprt(exprt _src, exprt _index, typet _type) : expr_protectedt( ID_extractbits, std::move(_type), - {std::move(_src), std::move(_upper), std::move(_lower)}) + {std::move(_src), std::move(_index)}) { } - extractbits_exprt( - exprt _src, - const std::size_t _upper, - const std::size_t _lower, - typet _type); + extractbits_exprt(exprt _src, const std::size_t _index, typet _type); exprt &src() { return op0(); } - exprt &upper() + exprt &index() { return op1(); } - exprt &lower() - { - return op2(); - } - const exprt &src() const { return op0(); } - const exprt &upper() const + const exprt &index() const { return op1(); } - - const exprt &lower() const - { - return op2(); - } }; template <> @@ -505,7 +491,7 @@ inline bool can_cast_expr(const exprt &base) inline void validate_expr(const extractbits_exprt &value) { - validate_operands(value, 3, "Extract bits must have three operands"); + validate_operands(value, 2, "Extractbits must have two operands"); } /// \brief Cast an exprt to an \ref extractbits_exprt diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index a04952856bc..7e4739a7372 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -276,24 +276,25 @@ bool can_forward_propagatet::is_constant(const exprt &expr) const } else if(auto eb = expr_try_dynamic_cast(expr)) { - if( - !is_constant(eb->src()) || !eb->lower().is_constant() || - !eb->upper().is_constant()) + if(!is_constant(eb->src()) || !eb->index().is_constant()) { return false; } + const auto eb_bits = pointer_offset_bits(eb->type(), ns); + if(!eb_bits.has_value()) + return false; + const auto src_bits = pointer_offset_bits(eb->src().type(), ns); if(!src_bits.has_value()) return false; const mp_integer lower_bound = - numeric_cast_v(to_constant_expr(eb->lower())); - const mp_integer upper_bound = - numeric_cast_v(to_constant_expr(eb->upper())); + numeric_cast_v(to_constant_expr(eb->index())); + const mp_integer upper_bound = lower_bound + eb_bits.value() - 1; return lower_bound >= 0 && lower_bound <= upper_bound && - upper_bound < src_bits; + upper_bound < src_bits.value(); } else { diff --git a/src/util/lower_byte_operators.cpp b/src/util/lower_byte_operators.cpp index a9dc5e4213f..c291c6b4d4b 100644 --- a/src/util/lower_byte_operators.cpp +++ b/src/util/lower_byte_operators.cpp @@ -110,7 +110,7 @@ static struct_exprt bv_to_struct_expr( bitvector_typet type = adjust_width(bitvector_expr.type(), component_bits); PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value()); operands.push_back(bv_to_expr( - extractbits_exprt{bitvector_expr, bounds.ub, bounds.lb, std::move(type)}, + extractbits_exprt{bitvector_expr, bounds.lb, std::move(type)}, comp.type(), endianness_map, ns)); @@ -163,7 +163,7 @@ static exprt bv_to_union_expr( return union_exprt{ component_name, bv_to_expr( - extractbits_exprt{bitvector_expr, bounds.ub, bounds.lb, std::move(type)}, + extractbits_exprt{bitvector_expr, bounds.lb, std::move(type)}, component_type, endianness_map, ns), @@ -209,8 +209,7 @@ static array_exprt bv_to_array_expr( adjust_width(bitvector_expr.type(), subtype_bits_int); PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value()); operands.push_back(bv_to_expr( - extractbits_exprt{ - bitvector_expr, bounds.ub, bounds.lb, std::move(type)}, + extractbits_exprt{bitvector_expr, bounds.lb, std::move(type)}, array_type.element_type(), endianness_map, ns)); @@ -256,8 +255,7 @@ static vector_exprt bv_to_vector_expr( adjust_width(bitvector_expr.type(), subtype_bits_int); PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value()); operands.push_back(bv_to_expr( - extractbits_exprt{ - bitvector_expr, bounds.ub, bounds.lb, std::move(type)}, + extractbits_exprt{bitvector_expr, bounds.lb, std::move(type)}, vector_type.element_type(), endianness_map, ns)); @@ -304,12 +302,12 @@ static complex_exprt bv_to_complex_expr( PRECONDITION(pointer_offset_bits(bitvector_expr.type(), ns).has_value()); return complex_exprt{ bv_to_expr( - extractbits_exprt{bitvector_expr, bounds_real.ub, bounds_real.lb, type}, + extractbits_exprt{bitvector_expr, bounds_real.lb, type}, complex_type.subtype(), endianness_map, ns), bv_to_expr( - extractbits_exprt{bitvector_expr, bounds_imag.ub, bounds_imag.lb, type}, + extractbits_exprt{bitvector_expr, bounds_imag.lb, type}, complex_type.subtype(), endianness_map, ns), @@ -1063,7 +1061,6 @@ static exprt unpack_rec( pointer_offset_bits(src_as_bitvector.type(), ns).has_value()); extractbits_exprt extractbits( src_as_bitvector, - from_integer(bit_offset + bits_per_byte - 1, array_type.index_type()), from_integer(bit_offset, array_type.index_type()), byte_type); @@ -2006,7 +2003,6 @@ static exprt lower_byte_update_single_element( extractbits_exprt bits_to_keep{ element_to_update, - subtype_bits_int - 1, subtype_bits_int - offset_bits_int, bv_typet{offset_bits_int}}; new_value = concatenation_exprt{ @@ -2014,7 +2010,6 @@ static exprt lower_byte_update_single_element( extractbits_exprt{ concatenation_exprt{ update_values, bv_typet{update_size * src.get_bits_per_byte()}}, - update_size * src.get_bits_per_byte() - 1, offset_bits_int, bv_typet{update_size * src.get_bits_per_byte() - offset_bits_int}}, bv_typet{update_size * src.get_bits_per_byte()}}; @@ -2521,8 +2516,7 @@ static exprt lower_byte_update( PRECONDITION(pointer_offset_bits(bitor_expr.type(), ns).has_value()); return simplify_expr( typecast_exprt::conditional_cast( - extractbits_exprt{ - bitor_expr, bounds.ub, bounds.lb, bv_typet{type_bits}}, + extractbits_exprt{bitor_expr, bounds.lb, bv_typet{type_bits}}, src.type()), ns); } @@ -2601,8 +2595,7 @@ exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns) lower_byte_extract(overlapping_byte_extract, ns); size_t n_extra_bits = bits_per_byte - update_bits_int % bits_per_byte; - extractbits_exprt extra_bits{ - overlapping_byte, n_extra_bits - 1, 0, bv_typet{n_extra_bits}}; + extractbits_exprt extra_bits{overlapping_byte, 0, bv_typet{n_extra_bits}}; update_value = concatenation_exprt{ typecast_exprt::conditional_cast( diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index 826cf4ae34d..b66befec5f4 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -923,13 +923,14 @@ simplify_exprt::simplify_concatenation(const concatenation_exprt &expr) const extractbits_exprt &eb_n = to_extractbits_expr(skip_typecast(opn)); if( - eb_i.src() == eb_n.src() && eb_i.lower().is_constant() && - eb_n.upper().is_constant() && - numeric_cast_v(to_constant_expr(eb_i.lower())) == - numeric_cast_v(to_constant_expr(eb_n.upper())) + 1) + eb_i.src() == eb_n.src() && eb_i.index().is_constant() && + eb_n.index().is_constant() && + numeric_cast_v(to_constant_expr(eb_i.index())) == + numeric_cast_v(to_constant_expr(eb_n.index())) + + to_bitvector_type(eb_n.type()).get_width()) { extractbits_exprt eb_merged = eb_i; - eb_merged.lower() = eb_n.lower(); + eb_merged.index() = eb_n.index(); to_bitvector_type(eb_merged.type()) .set_width( to_bitvector_type(eb_i.type()).get_width() + @@ -1138,11 +1139,7 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr) return unchanged(expr); } - const auto start = numeric_cast(expr.upper()); - const auto end = numeric_cast(expr.lower()); - - if(!start.has_value()) - return unchanged(expr); + const auto end = numeric_cast(expr.index()); if(!end.has_value()) return unchanged(expr); @@ -1152,10 +1149,17 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr) if(!width.has_value()) return unchanged(expr); + const auto result_width = pointer_offset_bits(expr.type(), ns); + + if(!result_width.has_value()) + return unchanged(expr); + + const auto start = std::optional(*end + *result_width - 1); + if(*start < 0 || *start >= (*width) || *end < 0 || *end >= (*width)) return unchanged(expr); - DATA_INVARIANT(*start >= *end, "extractbits must have upper() >= lower()"); + DATA_INVARIANT(*start >= *end, "extractbits must have start >= end"); if(expr.src().is_constant()) { @@ -1191,10 +1195,8 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr) { extractbits_exprt result = expr; result.src() = op; - result.lower() = - from_integer(*end - (offset - *op_width), expr.lower().type()); - result.upper() = - from_integer(*start - (offset - *op_width), expr.upper().type()); + result.index() = + from_integer(*end - (offset - *op_width), expr.index().type()); return changed(simplify_extractbits(result)); } @@ -1203,14 +1205,13 @@ simplify_exprt::simplify_extractbits(const extractbits_exprt &expr) } else if(auto eb_src = expr_try_dynamic_cast(expr.src())) { - if(eb_src->upper().is_constant() && eb_src->lower().is_constant()) + if(eb_src->index().is_constant()) { extractbits_exprt result = *eb_src; result.type() = expr.type(); - const mp_integer src_lower = - numeric_cast_v(to_constant_expr(eb_src->lower())); - result.lower() = from_integer(src_lower + *end, eb_src->lower().type()); - result.upper() = from_integer(src_lower + *start, eb_src->lower().type()); + const mp_integer src_index = + numeric_cast_v(to_constant_expr(eb_src->index())); + result.index() = from_integer(src_index + *end, eb_src->index().type()); return changed(simplify_extractbits(result)); } } diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index 5a8f979d3e8..a3ab0005dae 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -1329,13 +1329,12 @@ TEST_CASE( "Bit vector typed bounds", extractbits_exprt{ symbol_exprt{"foo", operand_type}, - from_integer(4, operand_type), from_integer(2, operand_type), unsignedbv_typet{3}}}, rowt{ "Constant integer bounds", extractbits_exprt{ - symbol_exprt{"foo", operand_type}, 4, 2, unsignedbv_typet{3}}}); + symbol_exprt{"foo", operand_type}, 2, unsignedbv_typet{3}}}); const smt_termt expected_result = smt_bit_vector_theoryt::extract(4, 2)( smt_identifier_termt{"foo", smt_bit_vector_sortt{8}}); SECTION(description) @@ -1346,7 +1345,6 @@ TEST_CASE( CHECK_THROWS(test.convert(extractbits_exprt{ symbol_exprt{"foo", operand_type}, symbol_exprt{"bar", operand_type}, - symbol_exprt{"bar", operand_type}, unsignedbv_typet{3}})); } } diff --git a/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp b/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp index 22924801927..96d96cb07e1 100644 --- a/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp +++ b/unit/solvers/smt2_incremental/encoding/struct_encoding.cpp @@ -206,7 +206,7 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") const exprt expected = equal_exprt{ zero, extractbits_exprt{ - symbol_exprt{"breakfast", bv_typet{72}}, 71, 40, field_type}}; + symbol_exprt{"breakfast", bv_typet{72}}, 40, field_type}}; REQUIRE(test.struct_encoding.encode(input) == expected); } SECTION("Second member") @@ -218,7 +218,7 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") const exprt expected = equal_exprt{ dozen, extractbits_exprt{ - symbol_exprt{"breakfast", bv_typet{72}}, 39, 24, field_type}}; + symbol_exprt{"breakfast", bv_typet{72}}, 24, field_type}}; REQUIRE(test.struct_encoding.encode(input) == expected); } SECTION("Third member") @@ -230,7 +230,7 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") const exprt expected = equal_exprt{ two, extractbits_exprt{ - symbol_exprt{"breakfast", bv_typet{72}}, 23, 0, field_type}}; + symbol_exprt{"breakfast", bv_typet{72}}, 0, field_type}}; REQUIRE(test.struct_encoding.encode(input) == expected); } } @@ -244,8 +244,8 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") from_integer(0, signedbv_typet{32})}; const concatenation_exprt expected{ {from_integer(0, signedbv_typet{32}), - extractbits_exprt{symbol_expr_as_bv, 39, 24, unsignedbv_typet{16}}, - extractbits_exprt{symbol_expr_as_bv, 23, 0, signedbv_typet{24}}}, + extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}}, + extractbits_exprt{symbol_expr_as_bv, 0, signedbv_typet{24}}}, bv_typet{72}}; REQUIRE(test.struct_encoding.encode(with) == expected); } @@ -256,9 +256,9 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") make_member_name_expression("eggs"), from_integer(0, unsignedbv_typet{16})}; const concatenation_exprt expected{ - {extractbits_exprt{symbol_expr_as_bv, 71, 40, signedbv_typet{32}}, + {extractbits_exprt{symbol_expr_as_bv, 40, signedbv_typet{32}}, from_integer(0, unsignedbv_typet{16}), - extractbits_exprt{symbol_expr_as_bv, 23, 0, signedbv_typet{24}}}, + extractbits_exprt{symbol_expr_as_bv, 0, signedbv_typet{24}}}, bv_typet{72}}; REQUIRE(test.struct_encoding.encode(with) == expected); } @@ -269,8 +269,8 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") make_member_name_expression("ham"), from_integer(0, signedbv_typet{24})}; const concatenation_exprt expected{ - {extractbits_exprt{symbol_expr_as_bv, 71, 40, signedbv_typet{32}}, - extractbits_exprt{symbol_expr_as_bv, 39, 24, unsignedbv_typet{16}}, + {extractbits_exprt{symbol_expr_as_bv, 40, signedbv_typet{32}}, + extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}}, from_integer(0, signedbv_typet{24})}, bv_typet{72}}; REQUIRE(test.struct_encoding.encode(with) == expected); @@ -280,7 +280,7 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") const concatenation_exprt expected{ {from_integer(0, signedbv_typet{32}), from_integer(1, unsignedbv_typet{16}), - extractbits_exprt{symbol_expr_as_bv, 23, 0, signedbv_typet{24}}}, + extractbits_exprt{symbol_expr_as_bv, 0, signedbv_typet{24}}}, bv_typet{72}}; SECTION("Operands in field order") { @@ -309,7 +309,7 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") { const concatenation_exprt expected{ {from_integer(0, signedbv_typet{32}), - extractbits_exprt{symbol_expr_as_bv, 39, 24, unsignedbv_typet{16}}, + extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}}, from_integer(1, signedbv_typet{24})}, bv_typet{72}}; SECTION("Operands in field order") @@ -337,7 +337,7 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]") SECTION("Second and third members") { const concatenation_exprt expected{ - {extractbits_exprt{symbol_expr_as_bv, 71, 40, signedbv_typet{32}}, + {extractbits_exprt{symbol_expr_as_bv, 40, signedbv_typet{32}}, from_integer(0, unsignedbv_typet{16}), from_integer(1, signedbv_typet{24})}, bv_typet{72}}; @@ -564,8 +564,8 @@ TEST_CASE("encoding of union expressions", "[core][smt2_incremental]") const exprt zero = from_integer(0, field_type); const exprt input = equal_exprt{zero, member_exprt{symbol_expr, "ham", field_type}}; - const exprt expected = equal_exprt{ - zero, extractbits_exprt{symbol_expr_as_bv, 31, 0, field_type}}; + const exprt expected = + equal_exprt{zero, extractbits_exprt{symbol_expr_as_bv, 0, field_type}}; REQUIRE(test.struct_encoding.encode(input) == expected); } SECTION("Member which is smaller than the union as a whole") @@ -573,8 +573,8 @@ TEST_CASE("encoding of union expressions", "[core][smt2_incremental]") const typet field_type = unsignedbv_typet{8}; const exprt input = equal_exprt{dozen, member_exprt{symbol_expr, "eggs", field_type}}; - const exprt expected = equal_exprt{ - dozen, extractbits_exprt{symbol_expr_as_bv, 7, 0, field_type}}; + const exprt expected = + equal_exprt{dozen, extractbits_exprt{symbol_expr_as_bv, 0, field_type}}; REQUIRE(test.struct_encoding.encode(input) == expected); } } diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp index 756666240a6..6d94eaa24e4 100644 --- a/unit/util/simplify_expr.cpp +++ b/unit/util/simplify_expr.cpp @@ -176,7 +176,7 @@ TEST_CASE("Simplify extractbits", "[core][util]") const exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32)); - exprt eb = extractbits_exprt(deadbeef, 15, 8, unsignedbv_typet(8)); + exprt eb = extractbits_exprt(deadbeef, 8, unsignedbv_typet(8)); bool unmodified = simplify(eb, ns); REQUIRE(!unmodified);