From 29b284fb8ae0a4c76c983209364090cdd0054f7d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 22 Mar 2021 22:38:05 +0000
Subject: [PATCH] Fix initialization of multiple sub-members within a union

The attached test shows that we could reach recursive initialisation of
unions with a byte_update instead of a union expression, which was added
in a8592a7357. That previous fix did not consider the case of multiple
sub-members being initialised.

The test was constructed using creduce, starting from code included in
the Linux kernel.
---
 .../ansi-c/Union_Initialization3/main.c       | 23 +++++++++++++++
 .../ansi-c/Union_Initialization3/test.desc    | 12 ++++++++
 src/ansi-c/c_typecheck_initializer.cpp        | 29 ++++++++++++-------
 3 files changed, 54 insertions(+), 10 deletions(-)
 create mode 100644 regression/ansi-c/Union_Initialization3/main.c
 create mode 100644 regression/ansi-c/Union_Initialization3/test.desc

diff --git a/regression/ansi-c/Union_Initialization3/main.c b/regression/ansi-c/Union_Initialization3/main.c
new file mode 100644
index 00000000000..878eee374eb
--- /dev/null
+++ b/regression/ansi-c/Union_Initialization3/main.c
@@ -0,0 +1,23 @@
+union {
+  int a;
+  struct
+  {
+    unsigned b : 4;
+    unsigned c : 4;
+  };
+} u1 = {.b = 5, .c = 1};
+
+#ifndef _MSC_VER
+union {
+  int;
+  struct
+  {
+    unsigned b : 4;
+    unsigned c : 4;
+  };
+} u2 = {.b = 5, .c = 1};
+#endif
+
+int main()
+{
+}
diff --git a/regression/ansi-c/Union_Initialization3/test.desc b/regression/ansi-c/Union_Initialization3/test.desc
new file mode 100644
index 00000000000..942848c6dd7
--- /dev/null
+++ b/regression/ansi-c/Union_Initialization3/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+--
+Invariant check failed
+--
+This test previously failed an internal invariant:
+File: ../src/ansi-c/c_typecheck_initializer.cpp:517 function: do_designated_initializer
+Condition: dest->id() == ID_union
+Reason: union should be zero initialized
diff --git a/src/ansi-c/c_typecheck_initializer.cpp b/src/ansi-c/c_typecheck_initializer.cpp
index bf82c39bdca..5e04a751b3e 100644
--- a/src/ansi-c/c_typecheck_initializer.cpp
+++ b/src/ansi-c/c_typecheck_initializer.cpp
@@ -514,22 +514,22 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
 
       const union_typet::componentt &component = components[index];
 
-      DATA_INVARIANT(
-        dest->id() == ID_union, "union should be zero initialized");
-
-      if(dest->get(ID_component_name) == component.get_name())
+      if(
+        dest->id() == ID_union &&
+        to_union_expr(*dest).get_component_name() == component.get_name())
       {
         // Already right union component. We can initialize multiple submembers,
         // so do not overwrite this.
         dest = &(to_union_expr(*dest).op());
       }
-      else
+      else if(dest->id() == ID_union)
       {
-        // The first component is not the maximum member, which the (default)
-        // zero initializer prepared. Replace this by a component-specific
-        // initializer; other bytes have an unspecified value (C Standard
-        // 6.2.6.1(7)). In practice, objects of static lifetime are fully zero
-        // initialized.
+        // The designated initializer does not initialize the maximum member,
+        // which the (default) zero initializer prepared. Replace this by a
+        // component-specific initializer; other bytes have an unspecified value
+        // (C Standard 6.2.6.1(7)). In practice, objects of static lifetime are
+        // fully zero initialized, so we just byte-update on top of the existing
+        // zero initializer.
         const auto zero =
           zero_initializer(component.type(), value.source_location(), *this);
         if(!zero.has_value())
@@ -556,6 +556,15 @@ exprt::operandst::const_iterator c_typecheck_baset::do_designated_initializer(
           dest = &(to_union_expr(*dest).op());
         }
       }
+      else if(
+        dest->id() == ID_byte_update_big_endian ||
+        dest->id() == ID_byte_update_little_endian)
+      {
+        // handle the byte update introduced by an earlier initializer (if
+        // current_symbol.is_static_lifetime)
+        byte_update_exprt &byte_update = to_byte_update_expr(*dest);
+        dest = &byte_update.op2();
+      }
     }
     else
       UNREACHABLE;