| Commit message (Collapse) | Author | Age | Files | Lines |
|\ |
|
| |\ |
|
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
As proposed in #404.
This is presented as a new option `-clight` to the existing `clightgen` tool.
Revise clightgen testing to test the Csyntax output in addition to
the Clight output.
|
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Split reusable parts of ExportClight.ml off, into
ExportBase.ml and ExportCtypes.ml.
Rename exportclight/ directory to export/
|
| |\ \ |
|
| | |\ \
| | | | |
| | | | |
| | | | | |
into csmith
|
| | | | | |
|
| | | | | |
|
| | |\ \ \ |
|
| |\ \ \ \ \
| | |_|_|/ /
| |/| | | /
| | | |_|/
| | |/| | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
In the Clight AST, padding bit fields (such as `int : 6;`) in composite
declarations are given an ident that corresponds to the empty string.
Previously, clightgen would give name `_` to this ident, but this is
not valid Coq.
This commit gives name `empty_ident` to the empty ident. This name
does not start with an underscore, so it cannot conflict with the
names for regular idents, which all start with `_`.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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.
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
When desugaring a bitfield, allow any integral type that is 32 bits
or smaller. Previously this was checking the rank of the type rather
than the size.
This rank check caused issues with standard headers that
declare `uint32_t` to be an `unsigned long` rather than an
`unsigned int`. Here, any bitfields declared as `uint32_t` were
failing to compile even though they are still actually 32 bits.
Co-authored-by: Amos Robinson <amos@gh.st>
|
| | | | | |
|
|/ / / / |
|
| | | | |
|
| | | | |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
into csmith
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
|/ / / / |
|
| | | | |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
into csmith
|
| | | | | |
|
| | | | | |
|
| |\ \ \ \
| | | | | |
| | | | | |
| | | | | | |
into csmith
|
| | | | | | |
|
| |/ / / /
|/| | | | |
|
|/ / / / |
|
|\ \ \ \
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
into csmith
Z
|
| |\ \ \ \
| | | | | |
| | | | | |
| | | | | | |
into csmith
|
| | |\ \ \ \
| | | | | | |
| | | | | | |
| | | | | | | |
into csmith
|
| | | | | | | |
|
| | |/ / / /
| |/| | | | |
|
| |/ / / / |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
|/ / / / |
|
| | | | |
|
| | | | |
|
|\ \ \ \ |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Squashed commit of the following:
commit 808e72db2022d05a4e34818b33cc9af17aaa4df0
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:53:39 2021 +0200
selectOp for comp0
commit f38e1f15359cceb3c0764635336125a1ceae78ff
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:49:45 2021 +0200
SelectOp for ccomp0 ok
commit ca969280380a593aef590a1fe2ec6f0fc112c2f5
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:46:01 2021 +0200
progress
commit e60a970f541ae6be30ec51cf95d60eb672ade829
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:40:49 2021 +0200
progres sur ltu etc.
commit 6f7d51e59a61d43fca06b1b4bad6dedada6e031e
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:13:07 2021 +0200
change selection
commit c2af349c6dd3e09fec25f3a96e1272377b6450ef
Author: David Monniaux <David.Monniaux@univ-grenoble-alpes.fr>
Date: Fri Sep 17 14:03:31 2021 +0200
begin rewrite selector
|
| | |_|/
| |/| | |
|
|\| | |
| |_|/
|/| | |
|