byte_extract lowering of unions
We previously handled unions like PODs.
This commit is contained in:
parent
bd307906f6
commit
761ad8a2cb
|
@ -1,4 +1,4 @@
|
|||
CORE broken-smt-backend
|
||||
CORE
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE broken-smt-backend
|
||||
CORE
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE broken-smt-backend
|
||||
CORE
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE broken-smt-backend
|
||||
CORE
|
||||
main.c
|
||||
--trace
|
||||
^EXIT=10$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE broken-smt-backend
|
||||
CORE
|
||||
union_list.c
|
||||
|
||||
^EXIT=0$
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
CORE broken-smt-backend
|
||||
CORE
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
|
|
|
@ -236,6 +236,34 @@ static exprt unpack_rec(
|
|||
std::move(byte_operands),
|
||||
array_typet(unsignedbv_typet(8), from_integer(size, size_type())));
|
||||
}
|
||||
else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
|
||||
{
|
||||
const union_typet &union_type = to_union_type(ns.follow(src.type()));
|
||||
const union_typet::componentst &components = union_type.components();
|
||||
|
||||
mp_integer max_width = 0;
|
||||
typet max_comp_type;
|
||||
irep_idt max_comp_name;
|
||||
|
||||
for(const auto &comp : components)
|
||||
{
|
||||
auto element_width = pointer_offset_bits(comp.type(), ns);
|
||||
|
||||
if(!element_width.has_value() || *element_width <= max_width)
|
||||
continue;
|
||||
|
||||
max_width = *element_width;
|
||||
max_comp_type = comp.type();
|
||||
max_comp_name = comp.get_name();
|
||||
}
|
||||
|
||||
if(max_width > 0)
|
||||
{
|
||||
member_exprt member(src, max_comp_name, max_comp_type);
|
||||
return unpack_rec(
|
||||
member, little_endian, offset_bytes, max_bytes, ns, true);
|
||||
}
|
||||
}
|
||||
else if(src.type().id()!=ID_empty)
|
||||
{
|
||||
// a basic type; we turn that into extractbits while considering
|
||||
|
@ -455,6 +483,36 @@ exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
|
|||
if(!failed)
|
||||
return simplify_expr(s, ns);
|
||||
}
|
||||
else if(src.type().id() == ID_union || src.type().id() == ID_union_tag)
|
||||
{
|
||||
const union_typet &union_type = to_union_type(ns.follow(src.type()));
|
||||
const union_typet::componentst &components = union_type.components();
|
||||
|
||||
mp_integer max_width = 0;
|
||||
typet max_comp_type;
|
||||
irep_idt max_comp_name;
|
||||
|
||||
for(const auto &comp : components)
|
||||
{
|
||||
auto element_width = pointer_offset_bits(comp.type(), ns);
|
||||
|
||||
if(!element_width.has_value() || *element_width <= max_width)
|
||||
continue;
|
||||
|
||||
max_width = *element_width;
|
||||
max_comp_type = comp.type();
|
||||
max_comp_name = comp.get_name();
|
||||
}
|
||||
|
||||
if(max_width > 0)
|
||||
{
|
||||
byte_extract_exprt tmp(unpacked);
|
||||
tmp.type() = max_comp_type;
|
||||
|
||||
return union_exprt(
|
||||
max_comp_name, lower_byte_extract(tmp, ns), union_type);
|
||||
}
|
||||
}
|
||||
|
||||
const exprt &root=unpacked.op();
|
||||
const exprt &offset=unpacked.offset();
|
||||
|
|
|
@ -113,7 +113,7 @@ 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}}),
|
||||
union_typet({{"compA", u32}, {"compB", u64}}),
|
||||
c_enum_typet(u16),
|
||||
c_enum_typet(unsignedbv_typet(128)),
|
||||
array_typet(u8, size),
|
||||
|
|
Loading…
Reference in New Issue