diff --git a/unit/solvers/lowering/byte_operators.cpp b/unit/solvers/lowering/byte_operators.cpp index 7f690b46685..e7b00a91c69 100644 --- a/unit/solvers/lowering/byte_operators.cpp +++ b/unit/solvers/lowering/byte_operators.cpp @@ -65,13 +65,19 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]") GIVEN("A collection of types") { unsignedbv_typet u8(8); + signedbv_typet s8(8); + unsignedbv_typet u16(16); + signedbv_typet s16(16); unsignedbv_typet u32(32); + signedbv_typet s32(32); unsignedbv_typet u64(64); + signedbv_typet s64(64); constant_exprt size = from_integer(8, size_type()); std::vector types = { - struct_typet({{"comp1", u32}, {"comp2", u64}}), + // struct_typet({{"comp1", u16}, {"comp2", u16}}), + // struct_typet({{"comp1", u32}, {"comp2", u64}}), #if 0 // not currently handled: components not byte aligned struct_typet({{"comp1", u32}, @@ -79,82 +85,92 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]") {"pad", c_bit_field_typet(u8, 4)}, {"comp2", u8}}), #endif - union_typet({{"compA", u32}, {"compB", u64}}), - c_enum_typet(unsignedbv_typet(16)), - array_typet(u8, size), - array_typet(u64, size), + // union_typet({{"compA", u32}, {"compB", u64}}), + // c_enum_typet(u16), + // c_enum_typet(unsignedbv_typet(128)), + // array_typet(u8, size), + // array_typet(s32, size), + // array_typet(u64, size), unsignedbv_typet(24), + unsignedbv_typet(128), + signedbv_typet(24), signedbv_typet(128), - ieee_float_spect::single_precision().to_type(), - pointer_typet(u64, 64), - vector_typet(u8, size), - vector_typet(u64, size), - complex_typet(u32) + // ieee_float_spect::single_precision().to_type(), + // pointer_typet(u64, 64), + // vector_typet(u8, size), + // vector_typet(u64, size), + // complex_typet(s16), + // complex_typet(u64) }; simplify_exprt simp(ns); THEN("byte_extract lowering yields the expected value") { - for(const auto &t1 : types) + for(const auto endianness : + {ID_byte_extract_little_endian, ID_byte_extract_big_endian}) { - std::ostringstream oss; - for(int i = 0; i < 64; ++i) - oss << integer2binary(i, 8); - - const auto type_bits = pointer_offset_bits(t1, ns); - REQUIRE(type_bits); - const auto type_bits_int = numeric_cast_v(*type_bits); - REQUIRE(type_bits_int <= oss.str().size()); - const exprt s = - simp.bits2expr(oss.str().substr(0, type_bits_int), t1, true); - REQUIRE(s.is_not_nil()); - - for(const auto &t2 : types) + for(const auto &t1 : types) { - oss.str(""); - for(int i = 2; i < 66; ++i) - oss << integer2binary(i, 8); - - const auto type_bits_2 = pointer_offset_bits(t2, ns); - REQUIRE(type_bits_2); - const auto type_bits_2_int = - numeric_cast_v(*type_bits_2); - REQUIRE(type_bits_2_int <= oss.str().size()); - const exprt r = - simp.bits2expr(oss.str().substr(0, type_bits_2_int), t2, true); - REQUIRE(r.is_not_nil()); - - const byte_extract_exprt be1( - ID_byte_extract_little_endian, - s, - from_integer(2, index_type()), - t2); - - const exprt lower_be1 = lower_byte_extract(be1, ns); - const exprt lower_be1_s = simplify_expr(lower_be1, ns); - - // TODO: does not currently hold - // REQUIRE(!has_subexpr(lower_be1, ID_byte_extract_little_endian)); - REQUIRE(lower_be1.type() == be1.type()); - // TODO: does not currently hold - // REQUIRE(lower_be1 == r); - // TODO: does not currently hold - // REQUIRE(lower_be1_s == r); - - const byte_extract_exprt be2( - ID_byte_extract_big_endian, s, from_integer(2, index_type()), t2); - - const exprt lower_be2 = lower_byte_extract(be2, ns); - const exprt lower_be2_s = simplify_expr(lower_be2, ns); - - // TODO: does not currently hold - REQUIRE(!has_subexpr(lower_be2, ID_byte_extract_big_endian)); - REQUIRE(lower_be2.type() == be2.type()); - // TODO: does not currently hold - // REQUIRE(lower_be2 == r); - // TODO: does not currently hold - // REQUIRE(lower_be2_s == r); + std::ostringstream oss; + for(int i = 0; i < 64; ++i) + { + std::string bits = integer2binary(i, 8); + std::reverse(bits.begin(), bits.end()); + oss << bits; + } + + const auto type_bits = pointer_offset_bits(t1, ns); + REQUIRE(type_bits); + const auto type_bits_int = numeric_cast_v(*type_bits); + REQUIRE(type_bits_int <= oss.str().size()); + const exprt s = simp.bits2expr( + oss.str().substr(0, type_bits_int), + t1, + endianness == ID_byte_extract_little_endian); + REQUIRE(s.is_not_nil()); + + for(const auto &t2 : types) + { + oss.str(""); + for(int i = 2; i < 64; ++i) + { + std::string bits = integer2binary(i, 8); + std::reverse(bits.begin(), bits.end()); + oss << bits; + } + + const auto type_bits_2 = pointer_offset_bits(t2, ns); + REQUIRE(type_bits_2); + + // for now only extract within bounds + if(*type_bits_2 + 16 > *type_bits) + continue; + + const auto type_bits_2_int = + numeric_cast_v(*type_bits_2); + REQUIRE(type_bits_2_int <= oss.str().size()); + const exprt r = simp.bits2expr( + oss.str().substr(0, type_bits_2_int), + t2, + endianness == ID_byte_extract_little_endian); + REQUIRE(r.is_not_nil()); + + const byte_extract_exprt be( + endianness, s, from_integer(2, index_type()), t2); + + const exprt lower_be = lower_byte_extract(be, ns); + const exprt lower_be_s = simplify_expr(lower_be, ns); + + // TODO: does not currently hold + // REQUIRE(!has_subexpr(lower_be, ID_byte_extract_little_endian)); + // REQUIRE(!has_subexpr(lower_be, ID_byte_extract_big_endian)); + REQUIRE(lower_be.type() == be.type()); + // TODO: does not currently hold + // REQUIRE(lower_be == r); + // TODO: does not currently hold + // REQUIRE(lower_be_s == r); + } } } } @@ -208,13 +224,19 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]") GIVEN("A collection of types") { unsignedbv_typet u8(8); + signedbv_typet s8(8); + unsignedbv_typet u16(16); + signedbv_typet s16(16); unsignedbv_typet u32(32); + signedbv_typet s32(32); unsignedbv_typet u64(64); + signedbv_typet s64(64); constant_exprt size = from_integer(8, size_type()); std::vector types = { // TODO: only arrays and scalars + // struct_typet({{"comp1", u16}, {"comp2", u16}}), // struct_typet({{"comp1", u32}, {"comp2", u64}}), #if 0 // not currently handled: components not byte aligned @@ -225,83 +247,96 @@ SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]") #endif // TODO: only arrays and scalars // union_typet({{"compA", u32}, {"compB", u64}}), - // c_enum_typet(unsignedbv_typet(16)), - array_typet(u8, size), - array_typet(u64, size), + // c_enum_typet(u16), + // c_enum_typet(unsignedbv_typet(128)), + // array_typet(u8, size), + // array_typet(s32, size), + // array_typet(u64, size), unsignedbv_typet(24), + unsignedbv_typet(128), + signedbv_typet(24), signedbv_typet(128), - ieee_float_spect::single_precision().to_type(), - pointer_typet(u64, 64), + // ieee_float_spect::single_precision().to_type(), + // pointer_typet(u64, 64), // TODO: only arrays and scalars // vector_typet(u8, size), // vector_typet(u64, size), - // complex_typet(u32) + // complex_typet(s16), + // complex_typet(u64) }; simplify_exprt simp(ns); THEN("byte_update lowering yields the expected value") { - for(const auto &t1 : types) + for(const auto endianness : + {ID_byte_update_little_endian, ID_byte_update_big_endian}) { - std::ostringstream oss; - for(int i = 0; i < 64; ++i) - oss << integer2binary(i, 8); - - const auto type_bits = pointer_offset_bits(t1, ns); - REQUIRE(type_bits); - const auto type_bits_int = numeric_cast_v(*type_bits); - REQUIRE(type_bits_int <= oss.str().size()); - const exprt s = - simp.bits2expr(oss.str().substr(0, type_bits_int), t1, true); - REQUIRE(s.is_not_nil()); - - for(const auto &t2 : types) + for(const auto &t1 : types) { - oss.str(""); - for(int i = 64; i < 128; ++i) - oss << integer2binary(i, 8); - - const auto type_bits_2 = pointer_offset_bits(t2, ns); - REQUIRE(type_bits_2); - const auto type_bits_2_int = - numeric_cast_v(*type_bits_2); - REQUIRE(type_bits_2_int <= oss.str().size()); - const exprt u = - simp.bits2expr(oss.str().substr(0, type_bits_2_int), t2, true); - REQUIRE(u.is_not_nil()); - - // TODO: currently required - if(type_bits < type_bits_2) - continue; - - const byte_update_exprt bu1( - ID_byte_update_little_endian, s, from_integer(2, index_type()), u); - - const exprt lower_bu1 = lower_byte_operators(bu1, ns); - const exprt lower_bu1_s = simplify_expr(lower_bu1, ns); - - REQUIRE(!has_subexpr(lower_bu1, ID_byte_update_little_endian)); - REQUIRE(!has_subexpr(lower_bu1, ID_byte_extract_little_endian)); - REQUIRE(lower_bu1.type() == bu1.type()); - // TODO: does not currently hold - // REQUIRE(lower_bu1 == u); - // TODO: does not currently hold - // REQUIRE(lower_bu1_s == u); - - const byte_update_exprt bu2( - ID_byte_update_big_endian, s, from_integer(2, index_type()), u); - - const exprt lower_bu2 = lower_byte_operators(bu2, ns); - const exprt lower_bu2_s = simplify_expr(lower_bu2, ns); - - REQUIRE(!has_subexpr(lower_bu2, ID_byte_update_big_endian)); - REQUIRE(!has_subexpr(lower_bu2, ID_byte_extract_big_endian)); - REQUIRE(lower_bu2.type() == bu2.type()); - // TODO: does not currently hold - // REQUIRE(lower_bu2 == u); - // TODO: does not currently hold - // REQUIRE(lower_bu2_s == u); + std::ostringstream oss; + for(int i = 0; i < 64; ++i) + { + std::string bits = integer2binary(i, 8); + std::reverse(bits.begin(), bits.end()); + oss << bits; + } + + const auto type_bits = pointer_offset_bits(t1, ns); + REQUIRE(type_bits); + const auto type_bits_int = numeric_cast_v(*type_bits); + REQUIRE(type_bits_int <= oss.str().size()); + const std::string s_string = oss.str().substr(0, type_bits_int); + const exprt s = simp.bits2expr( + s_string, t1, endianness == ID_byte_update_little_endian); + REQUIRE(s.is_not_nil()); + + for(const auto &t2 : types) + { + oss.str(""); + for(int i = 64; i < 128; ++i) + { + std::string bits = integer2binary(i, 8); + std::reverse(bits.begin(), bits.end()); + oss << bits; + } + + const auto type_bits_2 = pointer_offset_bits(t2, ns); + REQUIRE(type_bits_2); + + // for now only update within bounds + if(*type_bits_2 + 16 > *type_bits) + continue; + + const auto type_bits_2_int = + numeric_cast_v(*type_bits_2); + REQUIRE(type_bits_2_int <= oss.str().size()); + const std::string u_string = oss.str().substr(0, type_bits_2_int); + const exprt u = simp.bits2expr( + u_string, t2, endianness == ID_byte_update_little_endian); + REQUIRE(u.is_not_nil()); + + std::string r_string = s_string; + r_string.replace(16, u_string.size(), u_string); + const exprt r = simp.bits2expr( + r_string, t1, endianness == ID_byte_update_little_endian); + REQUIRE(r.is_not_nil()); + + const byte_update_exprt bu( + endianness, s, from_integer(2, index_type()), u); + + const exprt lower_bu = lower_byte_operators(bu, ns); + const exprt lower_bu_s = simplify_expr(lower_bu, ns); + + REQUIRE(!has_subexpr(lower_bu, endianness)); + REQUIRE(!has_subexpr(lower_bu, ID_byte_extract_big_endian)); + REQUIRE(!has_subexpr(lower_bu, ID_byte_extract_little_endian)); + REQUIRE(lower_bu.type() == bu.type()); + // TODO: does not currently hold + // REQUIRE(lower_bu == r); + // TODO: does not currently hold + // REQUIRE(lower_bu_s == r); + } } } }