From a631ed43a9f9ac1fac3c8895aeae4bc2b24f440b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 9 Jun 2026 10:46:24 +0000
Subject: [PATCH] ansi-c: fix self-referential enum from __attribute__((mode))
 fallback

For an enum with __attribute__((mode(M))), when M is not one of the
special-cased mode names (e.g. plain "byte" rather than "__byte__"), the
handler fell back to `result = subtype`, where the subtype is the
c_enum_tag.  It then wrote that back as the enum symbol's underlying
type, making the enum's underlying type its own tag -- a cyclic,
malformed type.  This later caused infinite recursion in alignment() (a
stack-overflow segfault) and a to_bitvector_type precondition abort in
pointer_offset_bits(), crashing goto-cc on real kernel objects
(net/rxrpc/rxgk, rxkad, af_rxrpc via crypto/krb5 headers).

Fall back to the already-resolved underlying bitvector type instead of
the c_enum_tag subtype.  For a non-enum bitvector subtype this is
unchanged (underlying_type == subtype); for an enum subtype it uses the
enum's underlying integer type, so no cycle is created.

Regression test gcc_enum_mode_attribute covers a special-cased mode
(__QI__) and a fall-back mode name (byte).

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 .../cbmc/gcc_enum_mode_attribute/main.c       | 37 +++++++++++++++++++
 .../cbmc/gcc_enum_mode_attribute/test.desc    | 14 +++++++
 src/ansi-c/c_typecheck_type.cpp               |  9 ++++-
 3 files changed, 58 insertions(+), 2 deletions(-)
 create mode 100644 regression/cbmc/gcc_enum_mode_attribute/main.c
 create mode 100644 regression/cbmc/gcc_enum_mode_attribute/test.desc

diff --git a/regression/cbmc/gcc_enum_mode_attribute/main.c b/regression/cbmc/gcc_enum_mode_attribute/main.c
new file mode 100644
index 00000000000..e815340cdfc
--- /dev/null
+++ b/regression/cbmc/gcc_enum_mode_attribute/main.c
@@ -0,0 +1,37 @@
+#include <assert.h>
+
+// An enum with __attribute__((mode(...))).  For a mode name we special-case
+// (__QI__ etc.) the enum gets that width; for one we don't (e.g. plain
+// "byte"), we must fall back to the enum's underlying bitvector -- NOT the
+// c_enum_tag, which previously made the enum's underlying type its own tag
+// (a cycle) and crashed pointer_offset_bits / alignment.  Used by some
+// kernel/crypto headers (net/rxrpc, crypto/krb5).
+enum E
+{
+  A,
+  B,
+  C
+} __attribute__((mode(__QI__)));
+enum F
+{
+  X,
+  Y
+} __attribute__((mode(byte)));
+
+struct s
+{
+  enum E e;
+  enum F f;
+  int tail;
+};
+
+int main(void)
+{
+  struct s v;
+  v.e = A;
+  v.f = X;
+  v.tail = 0;
+  assert(v.e == A);
+  // must be able to compute sizeof/layout without crashing
+  return (int)sizeof(struct s) + v.tail;
+}
diff --git a/regression/cbmc/gcc_enum_mode_attribute/test.desc b/regression/cbmc/gcc_enum_mode_attribute/test.desc
new file mode 100644
index 00000000000..67557b7e34e
--- /dev/null
+++ b/regression/cbmc/gcc_enum_mode_attribute/test.desc
@@ -0,0 +1,14 @@
+CORE gcc-only
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+^CONVERSION ERROR$
+--
+An enum with __attribute__((mode(...))) must not produce a self-referential
+underlying type (enum whose underlying type is its own c_enum_tag), which
+crashed pointer_offset_bits/alignment.  Covers a special-cased mode (__QI__)
+and a fall-back mode name (byte).
diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
index 2362e3966f6..62a23a7d137 100644
--- a/src/ansi-c/c_typecheck_type.cpp
+++ b/src/ansi-c/c_typecheck_type.cpp
@@ -245,8 +245,13 @@ void c_typecheck_baset::typecheck_type(typet &type)
             c_index_type(), unsigned_int_type(), from_integer(4, size_type()));
         }
       }
-      else // give up, just use subtype
-        result = to_type_with_subtype(type).subtype();
+      else // give up, just use the (resolved) underlying type.  For an
+           // enum subtype this is the enum's underlying bitvector, NOT the
+           // c_enum_tag -- using the tag would make the enum's underlying
+           // type its own tag (a cycle), which later crashes
+           // pointer_offset_bits/alignment.  This happens for mode names we
+           // don't special-case (e.g. mode(byte) without underscores).
+        result = underlying_type;
 
       // save the location
       result.add_source_location()=type.source_location();