Fixes to the byte_operator lowering unit test
Let's only test byte extracts within bounds for now (there is ample work to be done to get those right), but make sure there is possible combination for each pair of types. Endianness needs to be taken into account when constructing the expected value. Disable any non-POD tests as they all need more work.
This commit is contained in:
Michael Tautschnig
Daniel Kroening
parent
7027037d3c
commit
5a2df0d8b5
|
|
@ -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<typet> 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<std::size_t>(*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);
|
||||
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_2 = pointer_offset_bits(t2, ns);
|
||||
REQUIRE(type_bits_2);
|
||||
const auto type_bits_2_int =
|
||||
numeric_cast_v<std::size_t>(*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 auto type_bits = pointer_offset_bits(t1, ns);
|
||||
REQUIRE(type_bits);
|
||||
const auto type_bits_int = numeric_cast_v<std::size_t>(*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());
|
||||
|
||||
const byte_extract_exprt be1(
|
||||
ID_byte_extract_little_endian,
|
||||
s,
|
||||
from_integer(2, index_type()),
|
||||
t2);
|
||||
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 exprt lower_be1 = lower_byte_extract(be1, ns);
|
||||
const exprt lower_be1_s = simplify_expr(lower_be1, ns);
|
||||
const auto type_bits_2 = pointer_offset_bits(t2, ns);
|
||||
REQUIRE(type_bits_2);
|
||||
|
||||
// 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);
|
||||
// for now only extract within bounds
|
||||
if(*type_bits_2 + 16 > *type_bits)
|
||||
continue;
|
||||
|
||||
const byte_extract_exprt be2(
|
||||
ID_byte_extract_big_endian, s, from_integer(2, index_type()), t2);
|
||||
const auto type_bits_2_int =
|
||||
numeric_cast_v<std::size_t>(*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 exprt lower_be2 = lower_byte_extract(be2, ns);
|
||||
const exprt lower_be2_s = simplify_expr(lower_be2, ns);
|
||||
const byte_extract_exprt be(
|
||||
endianness, s, from_integer(2, index_type()), t2);
|
||||
|
||||
// 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);
|
||||
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<typet> 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<std::size_t>(*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);
|
||||
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_2 = pointer_offset_bits(t2, ns);
|
||||
REQUIRE(type_bits_2);
|
||||
const auto type_bits_2_int =
|
||||
numeric_cast_v<std::size_t>(*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());
|
||||
const auto type_bits = pointer_offset_bits(t1, ns);
|
||||
REQUIRE(type_bits);
|
||||
const auto type_bits_int = numeric_cast_v<std::size_t>(*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());
|
||||
|
||||
// TODO: currently required
|
||||
if(type_bits < type_bits_2)
|
||||
continue;
|
||||
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 byte_update_exprt bu1(
|
||||
ID_byte_update_little_endian, s, from_integer(2, index_type()), u);
|
||||
const auto type_bits_2 = pointer_offset_bits(t2, ns);
|
||||
REQUIRE(type_bits_2);
|
||||
|
||||
const exprt lower_bu1 = lower_byte_operators(bu1, ns);
|
||||
const exprt lower_bu1_s = simplify_expr(lower_bu1, ns);
|
||||
// for now only update within bounds
|
||||
if(*type_bits_2 + 16 > *type_bits)
|
||||
continue;
|
||||
|
||||
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 auto type_bits_2_int =
|
||||
numeric_cast_v<std::size_t>(*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());
|
||||
|
||||
const byte_update_exprt bu2(
|
||||
ID_byte_update_big_endian, s, from_integer(2, index_type()), u);
|
||||
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 exprt lower_bu2 = lower_byte_operators(bu2, ns);
|
||||
const exprt lower_bu2_s = simplify_expr(lower_bu2, ns);
|
||||
const byte_update_exprt bu(
|
||||
endianness, s, from_integer(2, index_type()), u);
|
||||
|
||||
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);
|
||||
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);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
Loading…
Reference in New Issue