Merge pull request #4717 from tautschnig/byte-operator-union

Byte-operator lowering: Add support for byte-extracting unions

regression/cbmc/union17/main.c

@@ -0,0 +1,19 @@
+int main()
+{
+  // create a union type of non-constant, non-zero size
+  unsigned x;
+  __CPROVER_assume(x > 0);
+  union U
+  {
+    unsigned A[x];
+  };
+  // create an integer of arbitrary value
+  int i, i_before;
+  i_before = i;
+  // initialize a union of non-zero size from the integer
+  unsigned u = ((union U *)&i)->A[0];
+  // reading back an integer out of the union should yield the same value for
+  // the integer as it had before
+  i = u;
+  __CPROVER_assert(i == i_before, "going through union works");
+}

regression/cbmc/union17/test.desc

@@ -0,0 +1,13 @@
+CORE broken-smt-backend
+main.c
+--no-simplify
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+This test passes when simplification is enabled (which gets rid of
+byte-extracting a union of non-constant size), but yielded a wrong verification
+outcome with both the SAT back-end before. The SMT back-end fails for it would
+like to flatten an array of non-constant size.

src/solvers/lowering/byte_operators.cpp

@@ -940,6 +940,18 @@ static exprt unpack_rec(
         ns,
         true);
     }
+    else if(!union_type.components().empty())
+    {
+      member_exprt member{src, union_type.components().front()};
+      return unpack_rec(
+        member,
+        little_endian,
+        offset_bytes,
+        max_bytes,
+        bits_per_byte,
+        ns,
+        true);
+    }
   }
   else if(src.type().id() == ID_pointer)
   {