ansi-c: support -fms-extensions anonymous tagged struct/union members

A *tagged* struct/union used as an unnamed (anonymous) member -- e.g.
the Linux kernel's `struct __filename_head;` embedded in struct filename
-- was silently dropped by the C front-end in GCC/Clang mode: it
contributed no bytes (so sizeof was wrong, breaking the kernel's
static_assert(sizeof(struct filename) % 64 == 0)) and its members were
not injected (inaccessible by name).

GCC/Clang accept this only with -fms-extensions (the Plan 9 C
extension); without it they ignore the member, matching the existing
regression/ansi-c/anonymous_member* tests. So:
- config: add ansi_c.allow_anonymous_struct_embedding (default false),
  named to be explicit that only this one MS/Plan 9 extension is
  implemented, not all of -fms-extensions;
- gcc_mode: set it when -fms-extensions is passed (queried as
  "fms-extensions" -- goto_cc_cmdlinet stores long options without the
  leading '-');
- c_typecheck_type: in GCC/Clang mode accept an *untagged* struct/union
  anonymous member always (C11) and a *tagged* one only under
  -fms-extensions; a non-struct/union unnamed member, or a tagged one
  without the flag, keeps the previous "ignore" behaviour.

With the flag the member now contributes its size and its fields are
injected (reachable by name). The new behaviour is documented in the
goto-cc section of the CPROVER manual, and exercised from both sides:
goto-gcc/ms_extensions_anonymous_member checks exact layout and member
access with the flag, and goto-gcc/ms_extensions_anonymous_member_ignored
checks the member is ignored without it. The existing anonymous_member*
tests confirm the default cbmc behaviour is preserved.

Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Author: 3 people

doc/cprover-manual/goto-cc.md

@@ -96,6 +96,13 @@ for i in `find . -name Makefile`; do
 done
 ```
 
+goto-cc honours the `-fms-extensions` flag: when given, it accepts an
+anonymous member that is a *tagged* struct or union (a Microsoft/GCC
+extension used, for instance, throughout the Linux kernel), injecting that
+member's fields into the enclosing struct and accounting for its size.
+Without the flag such a member is ignored, matching the default gcc and
+Clang behaviour.
+
 Here are additional examples on how to use goto-cc:
 
 -   \ref man_goto-cc-linux "Linux Kernel"

regression/goto-gcc/ms_extensions_anonymous_member/main.c

@@ -0,0 +1,51 @@
+// -fms-extensions: a *tagged* struct/union used as an unnamed (anonymous)
+// member.  Its members are injected into the enclosing struct and it
+// contributes its size.  Used pervasively in the Linux kernel (e.g.
+// struct __filename_head embedded in struct filename, whose static_asserts
+// require the size to be exact).  The _Static_asserts here are checked at
+// conversion time, so this fails to compile unless the anonymous tagged
+// member is laid out correctly.  Member types are deliberately fixed-width
+// (no pointers, no long) so the expected sizes are identical on 32-bit and
+// 64-bit targets.
+struct head
+{
+  int name;
+  int refcnt;
+  int aname;
+};
+
+struct filename
+{
+  struct head; // anonymous tagged-struct member
+  char iname[20];
+};
+
+_Static_assert(sizeof(struct head) == 12, "head size");
+_Static_assert(sizeof(struct filename) == 32, "filename size");
+_Static_assert(
+  __builtin_offsetof(struct filename, iname) == 12,
+  "iname offset");
+
+// a tagged union as an anonymous member, too
+struct u_outer
+{
+  union inner
+  {
+    int i;
+    char c[4];
+  };
+  int tail;
+};
+_Static_assert(sizeof(struct u_outer) == 8, "union-anon size");
+
+int main(void)
+{
+  struct filename f;
+  f.refcnt = 7; // inner field reachable through the anonymous member
+  f.name = 0;
+
+  struct u_outer u;
+  u.i = 3; // inner union field reachable
+
+  return f.refcnt + u.i;
+}

regression/goto-gcc/ms_extensions_anonymous_member/test.desc

@@ -0,0 +1,17 @@
+CORE
+main.c
+-fms-extensions -c -o main.gb
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+With -fms-extensions, goto-cc must accept a *tagged* struct/union as an
+anonymous member: it contributes its size and injects its members. The
+_Static_asserts (checked at conversion) require exact layout, and the
+field accesses require member injection. This is the pattern used by the
+Linux kernel's struct filename (struct __filename_head). Member sizes are
+fixed-width so the layout asserts hold on both 32-bit and 64-bit targets.
+Without -fms-extensions the member is ignored (standard GCC), which is
+covered by regression/ansi-c/anonymous_member*.

regression/goto-gcc/ms_extensions_anonymous_member_ignored/main.c

@@ -0,0 +1,31 @@
+// Companion to ms_extensions_anonymous_member, compiled WITHOUT
+// -fms-extensions.  Without that flag goto-cc follows standard gcc/Clang
+// behaviour: a *tagged* struct/union used as an anonymous member declares
+// nothing -- it injects no members and contributes no size.  The
+// _Static_assert (checked at conversion time) therefore requires the
+// enclosing struct to be sized as if the tagged member were absent.
+// Member types are fixed-width so the expected size holds on 32-bit and
+// 64-bit targets.
+struct head
+{
+  int name;
+  int refcnt;
+  int aname;
+};
+
+struct filename
+{
+  struct
+    head; // anonymous tagged-struct member: ignored without -fms-extensions
+  char iname[20];
+};
+
+// The tagged member contributes no size, so the struct is just char[20].
+_Static_assert(sizeof(struct filename) == 20, "tagged anon member ignored");
+
+int main(void)
+{
+  struct filename f;
+  (void)f;
+  return 0;
+}

regression/goto-gcc/ms_extensions_anonymous_member_ignored/test.desc

@@ -0,0 +1,15 @@
+CORE
+main.c
+-c -o main.gb
+^EXIT=0$
+^SIGNAL=0$
+declaration does not declare anything
+--
+^CONVERSION ERROR$
+--
+Without -fms-extensions, goto-cc ignores a tagged struct/union used as an
+anonymous member (standard gcc/Clang behaviour): it injects no members and
+contributes no size.  The _Static_assert requires sizeof(struct filename)
+to exclude the tagged member; were the member accepted (as with
+-fms-extensions) the size would differ and conversion would fail.  This is
+the no-flag counterpart of ms_extensions_anonymous_member.

src/ansi-c/c_typecheck_type.cpp

@@ -986,32 +986,25 @@ void c_typecheck_baset::typecheck_compound_body(
           }
           else
           {
-            // GCC and Clang ignore anything other than an untagged struct or
-            // union; we could print a warning, but there isn't any ambiguity in
-            // semantics here. Printing a warning could elevate this to an error
-            // when compiling code with goto-cc with -Werror.
-            // Note that our type checking always creates a struct_tag/union_tag
-            // type, but only named struct/union types have an ID_tag member.
+            // C11 allows an *untagged* struct/union as an anonymous member.
+            // -fms-extensions (and MSVC) additionally allow a *tagged*
+            // struct/union as an anonymous member, injecting its members
+            // and contributing its size -- used throughout the Linux kernel
+            // (e.g. `struct __filename_head;` embedded in struct filename).
+            // Anything else -- a non-struct/union unnamed member (e.g. a bare
+            // `int;`), or a tagged struct/union without -fms-extensions -- is
+            // ignored (the GCC/Clang behaviour we preserve).
+            const typet &member_type = new_component.type();
             if(
-              new_component.type().id() == ID_struct_tag &&
-              follow_tag(to_struct_tag_type(new_component.type()))
+              member_type.id() != ID_struct_tag &&
+              member_type.id() != ID_union_tag)
+              continue; // not a struct/union: ignore
+            const bool is_untagged =
+              follow_tag(to_struct_or_union_tag_type(member_type))
                 .find(ID_tag)
-                .is_nil())
-            {
-              // ok, anonymous struct
-            }
-            else if(
-              new_component.type().id() == ID_union_tag &&
-              follow_tag(to_union_tag_type(new_component.type()))
-                .find(ID_tag)
-                .is_nil())
-            {
-              // ok, anonymous union
-            }
-            else
-            {
-              continue;
-            }
+                .is_nil();
+            if(!is_untagged && !config.ansi_c.allow_anonymous_struct_embedding)
+              continue; // tagged anonymous member needs -fms-extensions
           }
         }
 

src/goto-cc/gcc_mode.cpp

@@ -579,6 +579,15 @@ int gcc_modet::doit()
     config.ansi_c.wchar_t_is_unsigned=true;
   }
 
+  // -fms-extensions enables MS/GCC extensions such as anonymous members
+  // that are a *tagged* struct/union type (used throughout the Linux
+  // kernel, e.g. struct __filename_head embedded in struct filename).
+  // Only anonymous struct/union embedding is implemented here.
+  // Note: goto_cc_cmdlinet stores long options without the leading '-',
+  // so we query "fms-extensions" (cf. the "fshort-double" check below).
+  if(cmdline.isset("fms-extensions"))
+    config.ansi_c.allow_anonymous_struct_embedding = true;
+
   // -fsingle-precision-constant makes floating-point constants "float"
   // instead of double
   if(cmdline.isset("-fsingle-precision-constant"))

src/util/config.cpp

@@ -867,6 +867,7 @@ bool configt::set(const cmdlinet &cmdline)
   cpp.cpp_standard=cppt::default_cpp_standard();
 
   ansi_c.single_precision_constant=false;
+  ansi_c.allow_anonymous_struct_embedding = false;
   ansi_c.for_has_scope=true; // C99 or later
   ansi_c.ts_18661_3_Floatn_types=false;
   ansi_c.__float128_is_keyword = false;

src/util/config.h

@@ -168,6 +168,7 @@ class configt
     bool bf16_type;               // __bf16 (Clang >= 15, GCC >= 13)
     bool fp16_type;               // __fp16 (GCC >= 4.5 on ARM, Clang >= 6)
     bool single_precision_constant;
+    bool allow_anonymous_struct_embedding; // -fms-extensions (partial)
     enum class c_standardt
     {
       C89,