diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index e2d083095f6..9d1ce6694da 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1518,10 +1518,10 @@ exprt simplify_exprt::bits2expr( if(!type_bits.has_value() || *type_bits != bits.size()) return nil_exprt(); - if(type.id()==ID_unsignedbv || - type.id()==ID_signedbv || - type.id()==ID_floatbv || - type.id()==ID_fixedbv) + if( + type.id() == ID_unsignedbv || type.id() == ID_signedbv || + type.id() == ID_floatbv || type.id() == ID_fixedbv || + type.id() == ID_c_bit_field || type.id() == ID_pointer) { endianness_mapt map(type, little_endian, ns); @@ -1632,6 +1632,49 @@ exprt simplify_exprt::bits2expr( return std::move(result); } + else if(type.id() == ID_vector) + { + const vector_typet &vector_type = to_vector_type(type); + + const std::size_t n_el = numeric_cast_v(vector_type.size()); + + const auto el_size_opt = pointer_offset_bits(vector_type.subtype(), ns); + CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0); + + const std::size_t el_size = numeric_cast_v(*el_size_opt); + + vector_exprt result({}, vector_type); + result.reserve_operands(n_el); + + for(std::size_t i = 0; i < n_el; ++i) + { + std::string el_bits = std::string(bits, i * el_size, el_size); + exprt el = bits2expr(el_bits, vector_type.subtype(), little_endian); + if(el.is_nil()) + return nil_exprt(); + result.add_to_operands(std::move(el)); + } + + return std::move(result); + } + else if(type.id() == ID_complex) + { + const complex_typet &complex_type = to_complex_type(type); + + const auto sub_size_opt = pointer_offset_bits(complex_type.subtype(), ns); + CHECK_RETURN(sub_size_opt.has_value() && *sub_size_opt > 0); + + const std::size_t sub_size = numeric_cast_v(*sub_size_opt); + + exprt real = bits2expr( + bits.substr(0, sub_size), complex_type.subtype(), little_endian); + exprt imag = + bits2expr(bits.substr(sub_size), complex_type.subtype(), little_endian); + if(real.is_nil() || imag.is_nil()) + return nil_exprt(); + + return complex_exprt(real, imag, complex_type); + } return nil_exprt(); } @@ -1647,10 +1690,10 @@ optionalt simplify_exprt::expr2bits( { const auto &value = to_constant_expr(expr).get_value(); - if(type.id()==ID_unsignedbv || - type.id()==ID_signedbv || - type.id()==ID_floatbv || - type.id()==ID_fixedbv) + if( + type.id() == ID_unsignedbv || type.id() == ID_signedbv || + type.id() == ID_floatbv || type.id() == ID_fixedbv || + type.id() == ID_c_bit_field || type.id() == ID_pointer) { const auto width = to_bitvector_type(type).get_width(); @@ -1678,20 +1721,9 @@ optionalt simplify_exprt::expr2bits( { return expr2bits(to_union_expr(expr).op(), little_endian); } - else if(expr.id()==ID_struct) - { - std::string result; - forall_operands(it, expr) - { - auto tmp=expr2bits(*it, little_endian); - if(!tmp.has_value()) - return {}; // failed - result+=tmp.value(); - } - - return result; - } - else if(expr.id()==ID_array) + else if( + expr.id() == ID_struct || expr.id() == ID_array || expr.id() == ID_vector || + expr.id() == ID_complex) { std::string result; forall_operands(it, expr) diff --git a/unit/Makefile b/unit/Makefile index 6fba9ea2a56..d6a49237bf7 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -34,6 +34,7 @@ SRC += analyses/ai/ai.cpp \ pointer-analysis/value_set.cpp \ solvers/bdd/miniBDD/miniBDD.cpp \ solvers/floatbv/float_utils.cpp \ + solvers/lowering/byte_operators.cpp \ solvers/prop/bdd_expr.cpp \ solvers/strings/array_pool/array_pool.cpp \ solvers/strings/string_constraint_generator_valueof/calculate_max_string_length.cpp \ diff --git a/unit/solvers/lowering/byte_operators.cpp b/unit/solvers/lowering/byte_operators.cpp new file mode 100644 index 00000000000..dfb93ca081b --- /dev/null +++ b/unit/solvers/lowering/byte_operators.cpp @@ -0,0 +1,309 @@ +/*******************************************************************\ + + Module: Unit tests for byte_extract/byte_update lowering + + Author: Michael Tautschnig + +\*******************************************************************/ + +#include + +#include + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +SCENARIO("byte_extract_lowering", "[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); + + GIVEN("A byte_extract over a POD") + { + const exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32)); + const byte_extract_exprt be1( + ID_byte_extract_little_endian, + deadbeef, + from_integer(1, index_type()), + signedbv_typet(8)); + + THEN("byte_extract lowering yields the expected value") + { + const exprt lower_be1 = lower_byte_extract(be1, ns); + const exprt lower_be1_s = simplify_expr(lower_be1, ns); + + REQUIRE(!has_subexpr(lower_be1, ID_byte_extract_little_endian)); + REQUIRE(lower_be1.type() == be1.type()); + REQUIRE(lower_be1_s == from_integer(0xbe, signedbv_typet(8))); + + byte_extract_exprt be2 = be1; + be2.id(ID_byte_extract_big_endian); + const exprt lower_be2 = lower_byte_extract(be2, ns); + const exprt lower_be2_s = simplify_expr(lower_be2, ns); + + REQUIRE(!has_subexpr(lower_be2, ID_byte_extract_big_endian)); + REQUIRE(lower_be2.type() == be2.type()); + REQUIRE(lower_be2_s == from_integer(0xad, signedbv_typet(8))); + } + } + + GIVEN("A collection of types") + { + unsignedbv_typet u8(8); + unsignedbv_typet u32(32); + unsignedbv_typet u64(64); + + exprt size = from_integer(8, size_type()); + + std::vector types = { + struct_typet({{"comp1", u32}, {"comp2", u64}}), +#if 0 + // not currently handled: components not byte aligned + struct_typet({{"comp1", u32}, + {"compX", c_bit_field_typet(u8, 4)}, + {"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), + unsignedbv_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) + }; + + simplify_exprt simp(ns); + + THEN("byte_extract lowering yields the expected value") + { + for(const auto &t1 : types) + { + 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) + { + 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); + } + } + } + } +} + +SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]") +{ + // 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); + + GIVEN("A byte_update of a POD") + { + const exprt deadbeef = from_integer(0xdeadbeef, unsignedbv_typet(32)); + const byte_update_exprt bu1( + ID_byte_update_little_endian, + deadbeef, + from_integer(1, index_type()), + from_integer(0x42, unsignedbv_typet(8))); + + THEN("byte_update lowering yields the expected value") + { + 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_extract_little_endian)); + REQUIRE(!has_subexpr(lower_bu1, ID_byte_update_little_endian)); + REQUIRE(lower_bu1.type() == bu1.type()); + REQUIRE(lower_bu1_s == from_integer(0xdead42ef, unsignedbv_typet(32))); + +#if 0 + // this is currently broken, #2058 will fix it + byte_update_exprt bu2 = bu1; + bu2.id(ID_byte_update_big_endian); + 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_extract_big_endian)); + REQUIRE(!has_subexpr(lower_bu2, ID_byte_update_big_endian)); + REQUIRE(lower_bu2.type() == bu2.type()); + REQUIRE(lower_bu2_s == from_integer(0xde42beef, unsignedbv_typet(32))); +#endif + } + } + + GIVEN("A collection of types") + { + unsignedbv_typet u8(8); + unsignedbv_typet u32(32); + unsignedbv_typet u64(64); + + exprt size = from_integer(8, size_type()); + + std::vector types = { + // TODO: only arrays and scalars + // struct_typet({{"comp1", u32}, {"comp2", u64}}), +#if 0 + // not currently handled: components not byte aligned + struct_typet({{"comp1", u32}, + {"compX", c_bit_field_typet(u8, 4)}, + {"pad", c_bit_field_typet(u8, 4)}, + {"comp2", u8}}), +#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), + unsignedbv_typet(24), + signedbv_typet(128), + 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) + }; + + simplify_exprt simp(ns); + + THEN("byte_update lowering yields the expected value") + { + for(const auto &t1 : types) + { + 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) + { + 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); + } + } + } + } +} diff --git a/unit/solvers/lowering/module_dependencies.txt b/unit/solvers/lowering/module_dependencies.txt new file mode 100644 index 00000000000..146b6f0220c --- /dev/null +++ b/unit/solvers/lowering/module_dependencies.txt @@ -0,0 +1,3 @@ +solvers/lowering +testing-utils +util