From 7032a1fe4c04252b6c9ab1293792c48a1e236b6d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 28 May 2019 02:20:44 +0000
Subject: [PATCH] Support byte-extract lowering over union of non-constant size

The test included made apparent that we weren't yet handling unbounded
byte extracts (out of a bounded object) for unions, which just fell back
to unpacking an empty array.
---
 regression/cbmc/union17/main.c          | 19 +++++++++++++++++++
 regression/cbmc/union17/test.desc       | 13 +++++++++++++
 src/solvers/lowering/byte_operators.cpp | 12 ++++++++++++
 3 files changed, 44 insertions(+)
 create mode 100644 regression/cbmc/union17/main.c
 create mode 100644 regression/cbmc/union17/test.desc

diff --git a/regression/cbmc/union17/main.c b/regression/cbmc/union17/main.c
new file mode 100644
index 00000000000..73d13b938d7
--- /dev/null
+++ b/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");
+}
diff --git a/regression/cbmc/union17/test.desc b/regression/cbmc/union17/test.desc
new file mode 100644
index 00000000000..cb26454d27c
--- /dev/null
+++ b/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.
diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp
index 6f4deea7674..a4a1e5340d8 100644
--- a/src/solvers/lowering/byte_operators.cpp
+++ b/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)
   {