C front-end: fix processing of alignment and packing attributes by tautschnig · Pull Request #8454 · diffblue/cbmc

tautschnig · 2024-09-13T15:26:09Z

Packing needs to be evaluated as part of the definition of the type while alignment applies also when using a type. The position of the attribute also requires extra care as some positions are accepted by GCC (and warned about by Clang) while actually being ignored.

Beyond the original fix, this PR now reworks how the C front-end models aggregate layout, driven by differential testing of goto-cc against GCC 13, Clang, and MSVC x64 (the latter via the Compiler Explorer API) on several thousand randomly generated structs/unions combining packed, aligned(n) in all positions, typedefs, nested aggregates, arrays, bit-fields, #pragma pack (incl. changes within a definition), and __declspec(align(n)). On develop, roughly half of these cases had a wrong size, alignment, or member offset; with this PR, none of the last ~3000 do.

Main changes (one commit each):

#pragma pack(n) is tracked as a per-member cap instead of being encoded as packed+aligned(n) attributes. GCC, Clang, and Visual Studio differ in which value applies when the pragma changes within a definition (closing brace, start of the definition, each member, respectively); each mode follows its compiler. dump-c reproduces the pragma.
#pragma pack(n)/#pragma pack() no longer push/clear the stack, and an unmatched pop retains the current value.
Bit-fields in packed aggregates and zero-width bit-fields (with the ARM-specific rule).
Alignment requested by a declaration (member, object, typedef) is kept apart from the alignment of a type: it applies to the declared entity regardless of position, can only increase a member's alignment (also when packed), while typedef/definition alignment is overridden by packing. GCC (unlike Clang) applies attributes after the * of a pointer declarator to the pointer type.
Anonymous aggregates are no longer conflated when they only differ in layout attributes.
__declspec(align(n)) on struct/union definitions is honoured, and Visual Studio's interaction of #pragma pack with trailing padding, __declspec(align(n)), and bit-fields in unions is implemented.

Fixes: #8443

Each commit message has a non-empty body, explaining why the change was made.
Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
n/a My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2024-09-13T16:05:12Z

Codecov Report

❌ Patch coverage is 94.48441% with 23 lines in your changes missing coverage. Please review.
✅ Project coverage is 80.96%. Comparing base (ef62206) to head (1586dfe).
⚠️ Report is 13 commits behind head on develop.

Files with missing lines	Patch %	Lines
src/goto-instrument/dump_c.cpp	77.27%	10 Missing ⚠️
src/ansi-c/c_typecheck_type.cpp	90.21%	9 Missing ⚠️
src/ansi-c/padding.cpp	97.64%	4 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #8454      +/-   ##
===========================================
+ Coverage    80.91%   80.96%   +0.05%     
===========================================
  Files         1719     1719              
  Lines       190344   190945     +601     
  Branches        73       74       +1     
===========================================
+ Hits        154018   154602     +584     
- Misses       36326    36343      +17

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

Copilot

Pull request overview

Fixes C front-end handling of GCC packed and aligned attributes so packing is applied during type definition while alignment also affects later uses, and ignores attribute placements that GCC accepts but ignores.

Changes:

Update grammar action for sue_declaration_specifier to drop ignored packed/aligned attributes before merging specifiers.
Add alignment validation (power-of-two) and introduce align_to to combine alignments across redefinitions / typedef uses.
Add a regression test covering many attribute placements and interactions.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 7 comments.

File	Description
`src/ansi-c/parser.y`	Filters out ignored `packed`/`aligned` attributes in a specific specifier context to match GCC behavior.
`src/ansi-c/c_typecheck_type.cpp`	Validates alignment values and combines alignments when reusing/redefining types.
`regression/ansi-c/gcc_attributes16/test.desc`	Adds expected-output configuration for the new regression test.
`regression/ansi-c/gcc_attributes16/main.c`	Adds C source covering many `packed`/`aligned` placements and expected `sizeof` results.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Packing needs to be evaluated as part of the definition of the type while alignment applies also when using a type. The position of the attribute also requires extra care as some positions are accepted by GCC (and warned about by Clang) while actually being ignored. The alignment validator now rejects non-positive and non-power-of-two values via a small is_power_of_two helper (mp_integer does not provide bitwise operators, so this uses floorPow2). The alignment-combining helper is renamed to combine_alignments and documents/asserts its power-of-two precondition (under which the maximum equals the least common multiple). The grammar action that drops ignored packed/aligned attributes is factored into a strip_ignored_attributes helper so the rule reads like grammar. The regression test gains _Alignof assertions (so alignments that don't change size are actually checked), packed/aligned union cases, a forward-declared-then-completed struct that exercises the alignment-combining path, a single-ignored-attribute-plus-qualifier case, and a direct reduction of diffblue#8443 (a packed-struct typedef used inside an outer struct carrying an alignment attribute). A new negative test, gcc_attributes16_align_error, pins the "not a positive power of 2" error path. Fixes: diffblue#8443 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Replace the five repeated static_cast<const exprt &>(t.find(ID_C_alignment)) casts in c_typecheck_type.cpp with a small alignment_of(const typet &) helper. This centralises the cast (and the assumption that exprt adds no data members to irept, so the cast is safe) in one documented place. This is a pure refactoring with no change in behaviour. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

A union's size must be a multiple of its alignment, including when the alignment comes from an explicit aligned() attribute on a packed union. Previously add_padding(union_typet) discarded any explicit alignment for packed unions (rounding the size up to a single byte only), so e.g. union __attribute__((packed)) __attribute__((aligned(16))) u { uint8_t c; int32_t i; }; had size 4 instead of 16. The alignment is now computed as the maximum member alignment (one byte if packed), raised by an explicit aligned() attribute regardless of packing, matching GCC and Clang. Adds regression test union_packed_aligned. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

The alignment of a struct/union member depends on whether the enclosing aggregate is packed, which a context-free alignment() could not capture: the same type (e.g. int aligned(2)) must align to 4 inside a non-packed struct (an aligned() attribute can only increase alignment there) but to 2 inside a packed struct (where it is honoured verbatim). alignment() now derives an aggregate's alignment from its members' layout alignments, computed in the aggregate's packing context via a new member_layout_alignment helper: - packed field: the explicit alignment verbatim, otherwise one byte; - non-packed field: max(explicit, natural) -- an aligned() request smaller than the natural alignment is ignored. An explicit alignment on the aggregate itself can only raise the result, while on a non-aggregate (e.g. a typedef) it is still taken verbatim. Padding members no longer contribute to an aggregate's alignment (they previously polluted _Alignof of e.g. a union with an array member). add_padding_gcc uses the same per-member computation for member offsets, and a packed struct is now padded up to the alignment forced by an explicitly-aligned member (it previously skipped end-of-struct padding for any packed struct). add_padding(union_typet) is simplified to rely on the corrected alignment(). This makes sizeof/_Alignof match GCC and Clang for member-level and struct/union-level aligned()/packed combinations. Adds regression test struct_member_alignment. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

GCC, Clang and Intel icx allow __attribute__((aligned(n))) on a typedef to *reduce* a type's alignment, and that reduced alignment is kept when the typedef is used as a struct member (the member, and hence the enclosing struct, is aligned to n). An alignment attribute on an object, field or tag declaration, by contrast, can only *increase* the alignment; a smaller request is ignored. The front-end stored both kinds identically as ID_C_alignment, so padding could not tell them apart: member_layout_alignment treated every member alignment as increase-only and over-aligned a reduced-alignment typedef member, inflating the enclosing struct. ID_C_typedef does not disambiguate either, as it is also present when a reducing attribute is attached to the declarator of a plain-typedef'd field. Record the provenance with a new ID_C_alignment_increase_only flag, set by ansi_c_convert_typet::set_attributes whenever an alignment attribute is applied to a non-typedef declaration (the only place that distinction is known). The flag is preserved through type checking -- the already-typechecked rebuild and typedef resolution, where a typedef's own alignment is left verbatim. padding then applies the matching rule: packing caps the alignment at min(n, natural); an increase-only attribute only raises it; a type-level alignment is taken verbatim and may reduce. This promotes regression/ansi-c/struct_member_alignment_typedef from KNOWNBUG to CORE. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

An alignment attribute that follows a declarator, as in a struct member int32_t m __attribute__((aligned(8 + 8))); is attached to the declarator's type outside the already type-checked declaration type. typecheck_type only type-checked and folded the alignment of a type that is not already type-checked, so this alignment remained an unevaluated expression. padding then failed to convert it to a number and silently used the natural alignment instead: the member was placed at offset 4 rather than 16. Literal alignments happened to work, as the unevaluated literal converts to a number, and so did members of array type, whose attributes take a different path. Invalid alignments, such as aligned(5 + 0), were accepted silently. Type-check, fold, and validate such alignments as well, sharing the code with the existing alignment handling, and report errors at the location of the alignment expression, as the type may not carry a location. Extend struct_member_alignment by members with constant-expression alignments, and add the negative test gcc_attributes16_align_error_member. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Anonymous structs and unions are named after their members, and an existing type symbol of the same name is re-used. As the name did not include packing or alignment attributes, `struct { int i; } a1;` and `struct { int i; } __attribute__((packed)) a2;` were conflated, and whichever was declared first determined the layout of both. Include packing and explicit alignment of the aggregate and of its members' types in the name. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

The parser used to communicate #pragma pack(n) by attaching both __attribute__((packed)) and __attribute__((aligned(n))) to each member whose type is not a struct or union, and additionally marked the aggregate as packed for pack(1). This conflated the pragma's cap on member alignment with explicit attributes, and was wrong in several ways: - an aligned attribute on the aggregate was capped by the pragma, but GCC, Clang, and Visual Studio do not cap it (and the aggregate-level packed of pack(1) had no such effect either); - packed on the aggregate no longer reduced member alignment to one; - explicit aligned() on members was replaced rather than capped; - members of struct or union type were not capped at all. Record the applicable #pragma pack value with each member declaration instead (ID_C_pragma_pack), and cap each member's layout alignment at that value in padding, for both GCC and Visual Studio layouts. The value that applies differs between compilers when the pragma changes within a definition: GCC uses the value in effect at the closing brace, Clang the value in effect where the definition starts, and Visual Studio the value in effect at each member. The parser determines the value accordingly. Bit-fields are capped as well. Anonymous aggregates are distinguished by the per-member value, and dump-c reproduces the pragma (which, for pack(1), it previously did via the aggregate-level packed attribute). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

`#pragma pack(n)` sets the current maximum alignment, and `#pragma pack()` resets it to the default; neither changes the stack used by `#pragma pack(push[, n])` and `#pragma pack(pop)`. We instead pushed n, and cleared the whole stack, respectively, so that, e.g., a `#pragma pack(pop)` following `#pragma pack(push, 1)` and `#pragma pack(2)` restored a maximum alignment of 1 rather than the value before the push. Furthermore, a `#pragma pack(pop)` without a matching push reset the current value to the default rather than retaining it. This matches the documentation and behaviour of GCC, Clang, and Visual Studio. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Bit-fields contributed the alignment of their underlying type to the alignment of the enclosing struct (used for end-of-struct padding) even when the struct is packed, so that, e.g., `struct { int m : 7; } __attribute__((packed))` had size 4 instead of 1. Use the member layout alignment instead, which now also covers bit-fields: - in a packed aggregate, bit-fields are densely packed, unless a #pragma pack(n) is in effect, which then caps their alignment at n (GCC and Clang agree on this); - a zero-width bit-field aligns the next member to its underlying type irrespective of packing, but only affects the alignment of the aggregate on ARM (other than Apple's ABI). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

GCC and Clang distinguish the alignment of a declared entity from that of its type: an alignment attribute in a declaration applies to the declared member, object, or typedef, irrespective of its position in the declaration. For members, such an attribute can only increase the alignment, also within packed aggregates and for bit-fields (whose start it then aligns). For objects, it may also reduce the alignment. In contrast, the alignment of a type (set by a typedef or a struct/union definition) may be smaller than its natural alignment, and packing overrides it. We previously recorded every alignment attribute on whichever type it was syntactically attached to, with a flag marking non-typedef attributes as increase-only. This went wrong in several ways: - `__attribute__((aligned(16))) char *p` or `long __attribute__((aligned(2))) m[2]` aligned the pointee or element type rather than the member; - packing did not override the alignment of typedef'd types or of struct/union definitions used as members, but did override member attributes; - a member attribute replaced, rather than combined with, the alignment of a typedef'd type; - the alignment of a struct/union definition was copied to every use of its tag, where it was then taken verbatim, so that `struct S { long l; } __attribute__((aligned(1)))` reduced the alignment of members of type `struct S`; - an attribute on an object could not reduce its alignment (as reported by __alignof__). Record alignments requested by declarations separately (ID_C_declaration_alignment), move them to the outermost level of the declared entity's type, and turn them into the type's alignment for typedefs only. __typeof__ does not carry them over, as they are not part of the type. Struct/union definitions keep their attributes with the type symbol only. GCC (but not Clang) applies an attribute that follows the '*' of a pointer declarator to the pointer type, which the parser now marks accordingly. When combining a plain `__attribute__((aligned))` with an explicit alignment, retain the latter, as we do not determine the target's maximum alignment. Encode declaration alignments in the names of anonymous aggregates. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

The parser accepted Visual Studio's __declspec between `struct`/`union` and the tag, but discarded it, so that, e.g., `struct __declspec(align(8)) S { char c; };` had size 1 and alignment 1 instead of 8. Retain the declspec with the type, which already handles align(n). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

Differential testing against MSVC x64 (via Compiler Explorer) showed three differences in Visual Studio mode: - the trailing padding of a struct or union is capped by the #pragma pack in effect at the end of its definition, whereas the alignment of the aggregate is not; - #pragma pack does not reduce an alignment that __declspec(align(n)) requires (also via a typedef), neither for a member nor for the trailing padding; - bit-fields do not affect the alignment of a union (only its size). Record the #pragma pack value at the end of the definition with the aggregate in Visual Studio mode, and lay out members using the common member layout alignment, which now also implements the latter two rules. dump-c reproduces the value at the end of the definition. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

tautschnig added the C Front End label Sep 13, 2024

tautschnig assigned kroening Sep 13, 2024

tautschnig requested review from kroening, peterschrammel and remi-delmas-3000 as code owners September 13, 2024 15:26

kroening reviewed Nov 26, 2024

View reviewed changes

Comment thread src/ansi-c/c_typecheck_type.cpp Resolved

tautschnig force-pushed the fix-8443-attributes branch from 5eea045 to 0367e2c Compare May 28, 2025 11:16

Copilot AI review requested due to automatic review settings March 9, 2026 16:14

tautschnig force-pushed the fix-8443-attributes branch from 0367e2c to 42011e8 Compare March 9, 2026 16:14

Copilot AI reviewed Mar 9, 2026

View reviewed changes

Copilot started reviewing on behalf of tautschnig March 9, 2026 18:31

View session

tautschnig force-pushed the fix-8443-attributes branch from 42011e8 to 200002c Compare March 9, 2026 21:54

tautschnig force-pushed the fix-8443-attributes branch 6 times, most recently from 7929110 to fa7af65 Compare June 15, 2026 18:00

tautschnig force-pushed the fix-8443-attributes branch from fa7af65 to 6380167 Compare June 16, 2026 18:52

tautschnig and others added 6 commits November 5, 2026 11:29

tautschnig force-pushed the fix-8443-attributes branch from 6380167 to 437ffdb Compare November 5, 2026 16:42

tautschnig requested a review from martin-cs as a code owner November 5, 2026 16:42

tautschnig and others added 2 commits November 5, 2026 18:38

tautschnig and others added 5 commits November 5, 2026 18:38

tautschnig force-pushed the fix-8443-attributes branch from 437ffdb to 1586dfe Compare November 5, 2026 19:20

Navigation Menu

Repository navigation

C front-end: fix processing of alignment and packing attributes - #8454

C front-end: fix processing of alignment and packing attributes#8454
tautschnig wants to merge 13 commits into
diffblue:developfrom
tautschnig:fix-8443-attributes

tautschnig commented Sep 13, 2024 •

edited

Loading

Uh oh!

codecov Bot commented Sep 13, 2024 •

edited

Loading

Uh oh!

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

tautschnig commented Sep 13, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov Bot commented Sep 13, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

tautschnig commented Sep 13, 2024 •

edited

Loading

codecov Bot commented Sep 13, 2024 •

edited

Loading