Merge pull request #4187 from tautschnig/byte-op-union

byte_extract lowering of unions [blocks: #2068]

Author: tautschnig

regression/cbmc/equality_through_union1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/equality_through_union2/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/equality_through_union3/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/trace_address_arithmetic1/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --trace
 ^EXIT=10$

regression/cbmc/union11/union_list.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 union_list.c
 
 ^EXIT=0$

regression/cbmc/union8/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 
 ^EXIT=0$

src/solvers/lowering/byte_operators.cpp

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

unit/solvers/lowering/byte_operators.cpp

@@ -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),