Simplify member access into a compound literal

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;
+}

regression/cbmc/compound_literal_member_static/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--

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)
   {