Ignore x86 __seg_fs/__seg_gs named-address-space qualifiers#9054
Open
tautschnig wants to merge 1 commit into
Open
Ignore x86 __seg_fs/__seg_gs named-address-space qualifiers#9054tautschnig wants to merge 1 commit into
tautschnig wants to merge 1 commit into
Conversation
tautschnig
requested review from
kroening,
peterschrammel and
remi-delmas-3000
as code owners
There was a problem hiding this comment.
Pull request overview
Note
Copilot was unable to run its full agentic suite in this review.
Updates the ANSI-C scanner to tolerate GCC/Clang x86 segment named-address-space qualifiers (__seg_fs, __seg_gs) by ignoring them, unblocking analysis of Linux x86 kernel per-CPU accessors and related code.
Changes:
- Teach
src/ansi-c/scanner.lto ignore bare__seg_fs/__seg_gstokens during lexing. - Add a regression test covering usage in pointer declarations, casts, and
__typeof__. - Add regression harness expectations for successful verification.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated 3 comments.
| File | Description |
|---|---|
| src/ansi-c/scanner.l | Ignores __seg_fs / __seg_gs as type qualifiers to prevent scanner syntax errors. |
| regression/ansi-c/gcc_named_address_space/test.desc | Adds a regression test descriptor expecting successful verification. |
| regression/ansi-c/gcc_named_address_space/main.c | New test case exercising segment qualifiers in multiple syntactic positions. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+1026
to
+1033
| /* 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. */ |
Comment on lines
+1
to
+7
| // 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). |
|
|
||
| int main(void) | ||
| { | ||
| struct s obj = {.x = 42}; |
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 <kiro-agent@users.noreply.github.com>
tautschnig
force-pushed
the
extract/ansi-c-seg-fs-qualifiers
branch
from
fa696b0 to
c892b81
Compare
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## develop #9054 +/- ##
===========================================
- Coverage 80.68% 80.68% -0.01%
===========================================
Files 1714 1714
Lines 189501 189504 +3
Branches 73 73
===========================================
Hits 152902 152902
- Misses 36599 36602 +3 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
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 touchescurrent/ 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.