diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp index cfcfb91277a..fad23110da8 100644 --- a/src/solvers/lowering/byte_operators.cpp +++ b/src/solvers/lowering/byte_operators.cpp @@ -50,10 +50,7 @@ static boundst map_bounds( // big-endian bounds need swapping if(result.ub < result.lb) - { - result.lb = endianness_map.number_of_bits() - result.lb - 1; - result.ub = endianness_map.number_of_bits() - result.ub - 1; - } + std::swap(result.lb, result.ub); } return result; @@ -1295,7 +1292,7 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns) concatenation_exprt concatenation( std::move(op), bitvector_typet(subtype->id(), width_bytes * 8)); - endianness_mapt map(src.type(), little_endian, ns); + endianness_mapt map(concatenation.type(), little_endian, ns); return bv_to_expr(concatenation, src.type(), map, ns); } } @@ -2226,22 +2223,16 @@ static exprt lower_byte_update( // original_bits |= newvalue bitor_exprt bitor_expr{bitand_expr, value_shifted}; - if(!is_little_endian && bit_width > type_bits) - { - return simplify_expr( - typecast_exprt::conditional_cast( - extractbits_exprt{bitor_expr, - bit_width - 1, - bit_width - type_bits, - bv_typet{type_bits}}, - src.type()), - ns); - } - else if(bit_width > type_bits) + if(bit_width > type_bits) { + endianness_mapt endianness_map( + bitor_expr.type(), src.id() == ID_byte_update_little_endian, ns); + const auto bounds = map_bounds(endianness_map, 0, type_bits - 1); + return simplify_expr( typecast_exprt::conditional_cast( - extractbits_exprt{bitor_expr, type_bits - 1, 0, bv_typet{type_bits}}, + extractbits_exprt{ + bitor_expr, bounds.ub, bounds.lb, bv_typet{type_bits}}, src.type()), ns); } diff --git a/src/util/endianness_map.cpp b/src/util/endianness_map.cpp index d861d9aa33d..36f26ae4819 100644 --- a/src/util/endianness_map.cpp +++ b/src/util/endianness_map.cpp @@ -53,12 +53,10 @@ void endianness_mapt::build_big_endian(const typet &src) { if(src.id() == ID_c_enum_tag) build_big_endian(ns.follow_tag(to_c_enum_tag_type(src))); - else if(src.id()==ID_unsignedbv || - src.id()==ID_signedbv || - src.id()==ID_fixedbv || - src.id()==ID_floatbv || - src.id()==ID_c_enum || - src.id()==ID_c_bit_field) + else if( + src.id() == ID_unsignedbv || src.id() == ID_signedbv || + src.id() == ID_fixedbv || src.id() == ID_floatbv || src.id() == ID_c_enum || + src.id() == ID_c_bit_field || src.id() == ID_bv) { // these do get re-ordered! auto bits = pointer_offset_bits(src, ns); // error is -1 diff --git a/unit/solvers/lowering/byte_operators.cpp b/unit/solvers/lowering/byte_operators.cpp index 559012dc6d1..f9eba47c89b 100644 --- a/unit/solvers/lowering/byte_operators.cpp +++ b/unit/solvers/lowering/byte_operators.cpp @@ -24,6 +24,72 @@ #include #include +TEST_CASE("byte extract and bits", "[core][solvers][lowering][byte_extract]") +{ + // this test does require a proper architecture to be set so that byte extract + // uses adequate endianness + cmdlinet cmdline; + config.set(cmdline); + + const symbol_tablet symbol_table; + const namespacet ns(symbol_table); + + const unsignedbv_typet u16{16}; + const exprt sixteen_bits = from_integer(0x1234, u16); + const array_typet bit_array_type{bv_typet{1}, from_integer(16, size_type())}; + + bool little_endian; + GIVEN("Little endian") + { + little_endian = true; + + const auto bit_string = expr2bits(sixteen_bits, little_endian, ns); + REQUIRE(bit_string.has_value()); + REQUIRE(bit_string->size() == 16); + + const auto array_of_bits = + bits2expr(*bit_string, bit_array_type, little_endian, ns); + REQUIRE(array_of_bits.has_value()); + + const auto bit_string2 = expr2bits(*array_of_bits, little_endian, ns); + REQUIRE(bit_string2.has_value()); + REQUIRE(*bit_string == *bit_string2); + + const byte_extract_exprt be1{little_endian ? ID_byte_extract_little_endian + : ID_byte_extract_big_endian, + sixteen_bits, + from_integer(0, index_type()), + bit_array_type}; + const exprt lower_be1 = lower_byte_extract(be1, ns); + REQUIRE(lower_be1 == *array_of_bits); + } + + GIVEN("Big endian") + { + little_endian = false; + + const auto bit_string = expr2bits(sixteen_bits, little_endian, ns); + REQUIRE(bit_string.has_value()); + REQUIRE(bit_string->size() == 16); + + const auto array_of_bits = + bits2expr(*bit_string, bit_array_type, little_endian, ns); + REQUIRE(array_of_bits.has_value()); + + const auto bit_string2 = expr2bits(*array_of_bits, little_endian, ns); + REQUIRE(bit_string2.has_value()); + REQUIRE(*bit_string == *bit_string2); + + const byte_extract_exprt be1{little_endian ? ID_byte_extract_little_endian + : ID_byte_extract_big_endian, + sixteen_bits, + from_integer(0, index_type()), + bit_array_type}; + const exprt lower_be1 = lower_byte_extract(be1, ns); + REQUIRE(lower_be1 == *array_of_bits); + } +} + SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]") { // this test does require a proper architecture to be set so that byte extract