Skip to content

Fixes to the byte_operator lowering unit test [blocks: #2068, #4062, #4063] #4061

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Feb 6, 2019
Merged

Fixes to the byte_operator lowering unit test [blocks: #2068, #4062, #4063] #4061

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
297 changes: 166 additions & 131 deletions unit/solvers/lowering/byte_operators.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,96 +65,112 @@ 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},
{"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),
// 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);

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 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<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());

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<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 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);
}
}
}
}
Expand Down Expand Up @@ -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
Expand All @@ -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);

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());

// 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<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());

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<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());

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);
}
}
}
}
Expand Down