From c892b81c6ddf388e34bc7300a825ee7394a06732 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 11 Jun 2026 18:11:02 +0000 Subject: [PATCH] Ignore x86 __seg_fs/__seg_gs named-address-space qualifiers The C scanner now ignores the bare type qualifiers __seg_fs and __seg_gs (like __extension__). These are GCC/Clang x86 named-address-space qualifiers for %fs/%gs segment-relative addressing; the Linux kernel uses them directly in its per-CPU accessors (arch/x86/include/asm/percpu.h) when the compiler supports named address spaces (CONFIG_CC_HAS_NAMED_ADDRESS_SPACES) -- e.g. `typeof(x) __seg_gs *` and `__typeof__(struct pcpu_hot __seg_gs)`. Because the system preprocessor treats them as builtin keywords (not macros) in that configuration, they survive preprocessing as bare tokens and previously produced "syntax error before '__seg_gs'", blocking goto-cc on essentially every x86 kernel translation unit that touches `current` / preempt-count / per-CPU state. Segment-relative addressing is irrelevant to functional verification (the pointed-to object is unchanged), so the qualifier is dropped. When the compiler lacks the feature these identifiers are instead macros expanding to __attribute__((address_space(...))), which the GCC_ATTRIBUTE scanner states already discard, so both configurations are handled. regression/ansi-c/gcc_named_address_space exercises the bare-qualifier form in pointer declarations, casts, and __typeof__. Co-authored-by: Kiro --- .../cbmc/gcc_named_address_space/main.c | 23 +++++++++++++++++++ .../cbmc/gcc_named_address_space/test.desc | 7 ++++++ src/ansi-c/scanner.l | 11 +++++++++ 3 files changed, 41 insertions(+) create mode 100644 regression/cbmc/gcc_named_address_space/main.c create mode 100644 regression/cbmc/gcc_named_address_space/test.desc diff --git a/regression/cbmc/gcc_named_address_space/main.c b/regression/cbmc/gcc_named_address_space/main.c new file mode 100644 index 00000000000..a58404e6984 --- /dev/null +++ b/regression/cbmc/gcc_named_address_space/main.c @@ -0,0 +1,23 @@ +// The x86 named-address-space (segment) qualifiers __seg_fs / __seg_gs, +// used by the Linux kernel's per-CPU accessors as BARE type qualifiers +// when the compiler supports named address spaces +// (CONFIG_CC_HAS_NAMED_ADDRESS_SPACES) -- e.g. `typeof(x) __seg_gs *`. +// They denote %fs/%gs segment-relative addressing, irrelevant to +// functional verification, so CBMC ignores the qualifier (the pointed-to +// object is unchanged). +struct s +{ + int x; +}; + +int main(void) +{ + struct s obj = {.x = 42}; + struct s __seg_gs *p = (struct s __seg_gs *)&obj; + struct s __seg_fs *q = (struct s __seg_fs *)&obj; + __typeof__(struct s __seg_gs) *r = &obj; + __CPROVER_assert(p->x == 42, "seg-gs-qualified pointer reads the object"); + __CPROVER_assert(q->x == 42, "seg-fs-qualified pointer reads the object"); + __CPROVER_assert(r->x == 42, "typeof with seg qualifier"); + return 0; +} diff --git a/regression/cbmc/gcc_named_address_space/test.desc b/regression/cbmc/gcc_named_address_space/test.desc new file mode 100644 index 00000000000..9c96469df12 --- /dev/null +++ b/regression/cbmc/gcc_named_address_space/test.desc @@ -0,0 +1,7 @@ +CORE +main.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l index f9c7b8674ce..c2173d5334d 100644 --- a/src/ansi-c/scanner.l +++ b/src/ansi-c/scanner.l @@ -1023,6 +1023,17 @@ enable_or_disable ("enable"|"disable") "__extension__" { /* ignore */ } + /* x86 named-address-space (segment) qualifiers used by the kernel's + per-CPU accessors (arch/x86/include/asm/percpu.h) when the compiler + supports named address spaces (CONFIG_CC_HAS_NAMED_ADDRESS_SPACES). + They denote %fs/%gs segment-relative addressing, which is irrelevant + to functional verification, so we ignore the qualifier (the pointed-to + object is unchanged). When the compiler lacks the feature these are + instead macros expanding to __attribute__((address_space(...))), which + the GCC_ATTRIBUTE states already discard. */ +"__seg_fs" { /* ignore: segment address-space qualifier */ } +"__seg_gs" { /* ignore: segment address-space qualifier */ } + "__restrict" { loc(); return TOK_RESTRICT; } "__restrict__" { loc(); return TOK_RESTRICT; }