Native support for bit fields #400
Closed
Conversation
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
In CompCert C and Clight, this commit adds a "bitfield" designator to l-value expressions and to the results of their evaluation. Bitfield designators are either - `Full`: no bit field, the value accessed is that contained in memory at the given block and offset - `Bits carrier pos width`: the value accessed is `width` bits starting at bit position `pos` in the integer of size `carrier` contained in memory at the given block and offset. During Csharpminor generation, bitfield accesses are implemented by integer shifts and masks. Currently, all l-value expressions produce a `Full` bitfield, so the `Bits` case is never exercised. This will change next when the layout algorithm for struct members is extended to deal with bitfield members.
- Struct and union declarations in CompCert C and Clight can now contain bitfield members. - Struct layout algorithm entirely revised to handle bitfields following the ELF ABI layout. - Todo: initializers don't handle bitfields yet. - Todo: on big-endian machines, bitfield accesses are wrong. - Todo: adapt C2C.
Reject byte-swapped bitfields. Tolerate (for the time being) bitfields with modified alignment. (But perhaps they should be rejected too, here or in C2C.)
This required major changes in cfrontend/Initializers.v. The proofs in cfrontend/Initializersproof.v still need updating. A "staticinit" test was added in tests/abi. Other tests in test/regression were updated.
Also: more work on Initializers.v and Initializersproof.v.
An unsigned bitfield strictly smaller than its type reads as a signed type. Hence, record the signedness explicitly in the `Bits` constructor, and make explicit the connections between the signedness of the field and the signedness of the type it reads with.
Use them in Cshmgenproof.
Works also for sign_ext 32. ARM, RISC-V: adapt Asmgenproof1 accordingly
A more general version of the link_match_program linking theorem. It supports match_fundef relations parameterized by the source compilation unit.
The value of `lhs = rhs` used to be the value of `rhs` cast to the type of `lhs`. This is incorrect if `lhs` denotes a bitfield in a struct or union. E.g. if `int f: 2`, `x.f = 7` evaluates to `-1`, not `7`. In this commit we modify `assign_loc` and `store_bitfield` to return the value of the assignment expression. We use this in the semantics of assignment expressions in Csem. We then adapt SimplExpr to the revised semantics of assignment return values. The generated Clight code now correctly zero- or sign-extends the assigned value if the lhs is a bitfield.
We try to ensure that all values of the enum can be represented with the chosen signedness and the given number of bits. This logic was in the Bitfields emulation pass, but is moved to C2C by this PR.
bitfields9 is for static initialization bitfields10 is for dynamic initialization. Dynamic initialization currently produces run-time errors with the reference interpreter, so don't test bitfields10 in interpreted mode.
`lia` was less clever about `Z.to_nat` in these versions.
The correctness proof now shows that the generated list of initializers is valid (correctly aligned + referring to known symbols only) so that Genv.store_init_data_list must succeed.
Change the Compcert C semantics to ignore the volatile modifier on access to bit fields, just like it ignores it on accesses by value to structs and unions, and access them as if they were not volatile. (Before, volatile bit field accesses were undefined behavior in Csem.) Change the SimplExpr pass to not generate EF_vload and EF_vstore builtins for accesses to bit fields of volatile type, just like it does not generate them for accesses to volatile structs and unions.
…ption cparse/Bitfields is no longer used. The `-fbitfields` command-line option is kept for backward compatibility but has no effect. The `-fno-bitfields` option is removed and will cause an error, since there is no longer a way to reject programs using bit fields.
A bit field of width 0 and type T means "align current position to T's size". The previous implementation would advance the current position by T's size if the current position was already aligned.
A bit field of type _Bool has maximal width `bitsize_intsize IBool`, that is, 1. However, the storage unit containing this bit field has size `bitsize_carrier IBool`, that is, 8. Rewrite the checks on bit field width and position to distinguish `bitsize_intsize` and `bitsize_carrier`.
This fails when evaluating `((struct foo *) 0)->field`. We really must use `Val.add` or `Val.addl`.
Reject bitfields in packed structs, like before. If we let them through, the resulting CompCert C code implements a strange layout (alignment of regular fields is reduced but alignment of bitfields is unchanged) that is quite different from that of GCC. It's better to reject.
xavierleroy
added a commit
that referenced
this pull request
Aug 22, 2021
This big PR adds support for bit fields in structs and unions to the verified part of CompCert, namely the CompCert C and Clight languages. The compilation of bit field accesses to normal integer accesses + shifts and masks is done and proved correct as part of the Cshmgen pass. The layout of bit fields in memory is done by the functions in module Ctypes. It follows the ELF ABI layout algorithm. As a bonus, basic soundness properties of the layout are shown, such as "two different bit fields do not overlap" or "a bit field and a regular field do not overlap". All this replaces the previous emulation of bit fields by source-to-source rewriting in the unverified front-end of CompCert (module cparse/Bitfield.ml). This emulation was prone to errors (see nonstandard layout instead. The core idea for the PR is that expressions in l-value position denote not just a block, a byte offset and a type, but also a bitfield designator saying whether all the bits of the type are accessed (designator Full) or only some of its bits (designator Bits). Designators of the Bits kind appear when the l-value is a bit field access; the bit width and bit offset in Bits are computed by the functions in Ctypes that implement the layout algorithm. Consequently, both in the semantics of CompCert C and Clight and in the SimplExpr, SimplLocals and Cshmgen compilation passes, pairs of a type and a bitfield designator are used in a number of places where a single type was used before. The introduction of bit fields has a big impact on static initialization (module cfrontend/Initializers.v), which had to be rewritten in large part, along with its soundness proof (cfrontend/Initializersproof.v). Both static initialization and run-time manipulation of bit fields are tested in test/abi using differential testing against GCC and randomly-generated structs. This work exposed subtle interactions between bit fields and the volatile modifier. Currently, the volatile modifier is ignored when accessing a bit field (and a warning is printed at compile-time), just like it is ignored when accessing a struct or union as a r-value. Currently, the natural alignment of bit fields and their storage units cannot be modified with the aligned attribute. _Alignas on bit fields is rejected as per C11, and the packed modifier cannot be applied to a struct containing bit fields.
xavierleroy
added a commit
that referenced
this pull request
Aug 22, 2021
Contributor
Author
|
Manually squashed and merged into master. |
andrew-appel
added a commit
to PrincetonUniversity/VST
that referenced
this pull request
Nov 18, 2021
AbsInt/CompCert#400 Basically, the "member" type describing a field of a struct or union is now more complicated, so many things in VST must be adapted. VST does not fully support bitfield-members, only plain members, but at least it adapts to the new type in the Clight ASTs. In addition, this adapts to a more recent commit to the CompCert master branch, moving exportclight/*.v to export/*.v
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.
This big PR adds support for bit fields in structs and unions to the verified part of CompCert, namely the CompCert C and Clight languages.
The compilation of bit field accesses to normal integer accesses + shifts and masks is done and proved correct as part of the Cshmgen pass.
The layout of bit fields in memory is done by the functions in module Ctypes. It follows the ELF ABI layout algorithm. As a bonus, basic soundness properties of the layout are shown, such as "two different bit fields do not overlap" or "a bit field and a regular field do not overlap".
All this replaces the previous emulation of bit fields by source-to-source rewriting in the unverified front-end of CompCert (module cparse/Bitfield.ml). This emulation was prone to errors (see #395) and could not express the ELF ABI layout, implementing its own nonstandard layout instead.
The core idea for the PR is that expressions in l-value position denote not just a block, a byte offset and a type, but also a bitfield designator saying whether all the bits of the type are accessed (designator
Full) or only some of its bits (designatorBits). Designators of theBitskind appear when the l-value is a bit field access; the bit width and bit offset inBitsare computed by the functions inCtypesthat implement the layout algorithm.Consequently, both in the semantics of CompCert C and Clight and in the SimplExpr, SimplLocals and Cshmgen compilation passes, pairs of a type and a bitfield designator are used in a number of places where a single type was used before.
The introduction of bit fields has a big impact on static initialization (module cfrontend/Initializers.v), which had to be rewritten in large part, along with its soundness proof (cfrontend/Initializersproof.v).
Both static initialization and run-time manipulation of bit fields are tested in
test/abiusing differential testing against GCC and randomly-generated structs.This work exposed subtle interactions between bit fields and the
volatilemodifier. Currently, thevolatilemodifier is ignored when accessing a bit field (and a warning is printed at compile-time), just like it is ignored when accessing a struct or union as a r-value. The alternative -- emitting events in the trace when accessing a volatile bit-field -- raises many semantic difficulties that I was not able to overcome.Currently, the natural alignment of bit fields and their storage units cannot be modified with the
alignedattribute._Alignason bit fields is rejected as per C11, and thepackedmodifier cannot be applied to a struct containing bit fields. It might be possible to support bit fields in packed structs if required.