From 3c0f01c764b75def3486b22a66dddab580a8d845 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 10 Jun 2026 10:33:49 +0000
Subject: [PATCH] Simplify member access into a compound literal

simplify_member now folds `member(compound_literal(v), .m)` by
unwrapping the compound literal to its single initializer operand `v`
and recursing, so the existing struct/union member-extraction rules
apply.

This fixes a constant-folding gap that made the C front-end reject valid
constant static initializers nesting a compound literal: the kernel's
dynamic-debug `_ddebug` descriptor initialises its `.key` union from the
`STATIC_KEY_FALSE_INIT` compound literal (under CONFIG_JUMP_LABEL),
which projected to `member(compound_literal{...},
.key.enabled.counter)`.  That member-of-compound-literal was not
simplified, so make_constant's is_compile_time_constantt rejected it
with "expected constant expression" -- blocking goto-cc on every
linux-6.12 translation unit that uses dynamic debug (sound/usb,
fs/hfsplus, fs/jfs, ...).  With the fix sound/usb/format.c (and the
rest) goto-cc cleanly.

regression/ansi-c/compound_literal_member_static reproduces the _ddebug
shape (a static struct whose union field is initialised from a compound
literal) and checks the projected member folds to its constant.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 .../compound_literal_member_static/main.c     | 66 +++++++++++++++++++
 .../compound_literal_member_static/test.desc  |  7 ++
 src/util/simplify_expr_struct.cpp             | 14 ++++
 3 files changed, 87 insertions(+)
 create mode 100644 regression/cbmc/compound_literal_member_static/main.c
 create mode 100644 regression/cbmc/compound_literal_member_static/test.desc

diff --git a/regression/cbmc/compound_literal_member_static/main.c b/regression/cbmc/compound_literal_member_static/main.c
new file mode 100644
index 00000000000..f60430133d9
--- /dev/null
+++ b/regression/cbmc/compound_literal_member_static/main.c
@@ -0,0 +1,66 @@
+// A constant static initializer that nests a compound literal projected
+// through a union member -- the shape of the kernel's dynamic-debug
+// _ddebug descriptor whose .key union is initialised from the
+// STATIC_KEY_FALSE_INIT compound literal.  Before member-of-compound-
+// literal simplification, the typechecker rejected this with "expected
+// constant expression".
+typedef struct
+{
+  int counter;
+} atomic_t;
+
+struct static_key
+{
+  atomic_t enabled;
+  union
+  {
+    unsigned long type;
+    void *entries;
+  };
+};
+
+struct static_key_false
+{
+  struct static_key key;
+};
+struct static_key_true
+{
+  struct static_key key;
+};
+
+#define STATIC_KEY_INIT_FALSE                                                  \
+  {                                                                            \
+    .enabled = {0},                                                            \
+    {                                                                          \
+      .type = 0ul                                                              \
+    }                                                                          \
+  }
+#define STATIC_KEY_FALSE_INIT                                                  \
+  (struct static_key_false)                                                    \
+  {                                                                            \
+    .key = STATIC_KEY_INIT_FALSE,                                              \
+  }
+
+struct ddebug
+{
+  const char *function;
+  unsigned flags;
+  union
+  {
+    struct static_key_true dd_key_true;
+    struct static_key_false dd_key_false;
+  } key;
+};
+
+int main(void)
+{
+  static struct ddebug d = {
+    .function = __func__,
+    .flags = 0,
+    .key.dd_key_false = (STATIC_KEY_FALSE_INIT),
+  };
+  __CPROVER_assert(
+    d.key.dd_key_false.key.enabled.counter == 0,
+    "compound-literal member folds to its constant");
+  return 0;
+}
diff --git a/regression/cbmc/compound_literal_member_static/test.desc b/regression/cbmc/compound_literal_member_static/test.desc
new file mode 100644
index 00000000000..9c96469df12
--- /dev/null
+++ b/regression/cbmc/compound_literal_member_static/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index 3993484ad48..ea16815e0cd 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -125,6 +125,20 @@ simplify_exprt::simplify_member(const member_exprt &expr)
       return op.operands()[number];
     }
   }
+  else if(op.id() == ID_compound_literal && op.operands().size() == 1)
+  {
+    // member(compound_literal(v), .m) -> member(v, .m)
+    // A compound literal `(TYPE){ ... }` wraps its initializer value (a
+    // struct/union/array expression) as its single operand; unwrap it so
+    // the struct/union member-extraction rules below can fold the access.
+    // This is needed for constant static initializers that nest a
+    // compound literal (e.g. the kernel's dynamic-debug _ddebug descriptor
+    // whose .key field is initialised from the STATIC_KEY_FALSE_INIT
+    // compound literal).
+    auto new_expr = expr;
+    new_expr.struct_op() = op.operands().front();
+    return changed(simplify_member(new_expr));
+  }
   else if(op.id()==ID_byte_extract_little_endian ||
           op.id()==ID_byte_extract_big_endian)
   {