| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
|
|
|
|
|
|
|
|
|
|
|
| |
In Op.v, the definitions of is_rldl_mask and is_rldr_mask mask were
swapped:
- rldl is for [00001111] masks that clear on the left,
hence start with 1s and finish with 0s;
- rldr is for [11110000] masks that clear on the right,
hence start with 0s and finish with 1s.
In Asmgen.v, the case for masks of the form [00011111100] that can
generate a rldic instruction was incorrectly detected.
|
|
|
|
|
|
|
|
| |
CompCert does not support 128-bit integers, but the gcc and clang preprocessors do include support as part of its 'built-in'.
A common way of testing for 128-bit integer support is to check to see if `__SIZEOF_INT128__` is defined.
Eliminating this macro prevents software from believing that 128-bit integers are supported.
|
|\
| |
| | |
Improved compatibility with Coq 8.14
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Warning "deprecated hint rewrite without locality" cannot be addressed:
the suggested fix (qualify with Global or Local or [#export])
is not supported by Coq 8.11 to 8.13 !
Warning "deprecated instance without locality" is turned off
for generated file cparser/Parser.v only.
Menhir needs to be changed so as to generate the `Global` modifier
that would silence this warning.
|
| |
| |
| |
| | |
This avoids a new warning of Coq 8.14.
|
|/ |
|
|
|
|
| |
It remains compatible with earlier Menhir versions.
|
|
|
|
| |
The change is backward compatible with Coq 8.9 to 8.13 (at least).
|
|
|
|
| |
Follow-up to c34d25e01
|
|
|
|
|
|
|
|
|
|
|
|
| |
When a union is initialized with an initializer without designator the
first named member should be initialized. This commit skips members
without names during the elaboration of union initializers.
Note that anonymous members (unnamed members of struct or union type)
should not be skipped, and are not skipped since elaboration give names
to these members.
Bug 31982
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
E.g. `struct { int; int x; };`. The `int;` declaration provides no name,
is not a bit field, and is not a C11 anonymous struct/union member.
Such declarations are not allowed by the C99 grammar, even though GCC,
Clang and CompCert tolerate them. The C11 grammar allows these
declarations but the standard text gives them no meaning.
CompCert used to warn about such declarations, yet include them in the
struct or union as unnamed members, similar to an unnamed bit field.
This is incorrect and inconsistent with what GCC and Clang do.
With this commit, CompCert still warns, then ignores the declaration
and does not create an unnamed member. This is consistent with GCC
and Clang.
Fixes: #411
|
|\
| |
| | |
Add support to clightgen for generating Csyntax AST as .v files
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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/
|
| |
| |
| |
| |
| |
| | |
For compatibility with Coq 8.14.
Cherry-picked from upstream commit 2e3c2441
|
| |
| |
| |
| | |
For compatibility with the upcoming Coq 8.14.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
In the "small" case, there was an error in the choice of temporary
registers to use when one argument is a stack location and the other
is a register. The chosen temporary could conflict with the argument
that resides in a register.
Fixes: #412
|
|/
|
|
|
|
|
|
|
|
| |
Stack offsets must be multiple of 8 when using ldp/stp instructions
and multiple of the transferred size when using other load/store
instructions with offsets greater than 256.
For simplicity, always require that the offset is multiple of 8.
Fixes: #410
|
|
|
|
| |
The return type is Tint8unsigned (i.e. _Bool), not Tint.
|
| |
|
|
|
|
|
|
| |
Instead, add `Set Asymmetric Patterns` to the files that need it,
or use `Arguments` to make inductive types work better with symmetric patterns.
Closes: #403
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 `_`.
|
|
|
|
|
|
|
|
|
|
|
| |
Warning 69 "mutable record field is never mutated":
3 occurrences in backend/IRC.ml
removed the "mutable" qualifier on these fields
Warning 70 "cannot find interface file"
many .ml files have no .mli
no strong motivation to add the .mli files
turned off the warning in Makefile.extr
|
|
|
|
|
|
| |
Instead of duplicating the memory access code in `Asmexpand.ml` we move
the code for each of the different addressings in `Asmgen.v` into
separate functions that then can be reused in `Asmexpand.ml`.
|
|
|
|
|
|
|
|
| |
leaq's offsets can overflow (not fit in 32 bits) in other cases than
those fixed in 4daebb7a0, e.g. in the expansion of __builtin_memcpy_aligned.
This commit implements full normalization of the `leaq` instructions
produced in Asmexpand, following the same method used in Asmgen.
|
|
|
|
|
|
|
|
|
|
|
|
| |
If N does not fit in signed 32 bits, `leaq` cannot be used and
`mov; addq` must be used instead.
This was already the case for `leaq` instructions produced by the Asmgen
pass, but not for some `leaq` instructions produced by Asmexpand.
Normally, assemblers should fail if the `leaq` offset is not representable,
but this is not always the case (see issue #406).
Fixes: #406
|
|\ |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| | |
A more general version of the link_match_program linking theorem.
It supports match_fundef relations parameterized by the source compilation unit.
|
| |
| |
| |
| |
| |
| | |
Works also for sign_ext 32.
ARM, RISC-V: adapt Asmgenproof1 accordingly
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
Don't put them in the C environment used for elaboration.
Instead, add them directly to the generated CompCert C at the end of
the C2C translation.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
As reported in #399, it seems better to use `##` instead of `#` as
comment delimiter under macOS.
For the time being we keep using `#` for Linux and Cygwin.
Closes: #399
|
|/
|
|
|
|
|
| |
Before, the line number had to start with a nonzero digit. However,
the GCC 11 preprocessor was observed to produce `# 0 ...` directives.
Fixes: #398
|
|
|
|
| |
E.g. __builtin_bswap. Update Asm modeling of builtins accordingly.
|
| |
|
| |
|
|
|
|
| |
Also: limit the max width of the page, to avoid very long lines.
|
| |
|
|
|
|
|
|
| |
The GPL makes sense for whole applications, but the dual-licensed Coq
and OCaml files are more like libraries to be combined with other
code, so the LGPL is more appropriate.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
A bitfield assignment `x.b = f()` is expanded into a read-modify-write
on `x.carrier`. Wrong results can occur if `x.carrier` is read before
the call to `f()`, and `f` itself modifies a bitfield with the same
carrier `x.carrier`.
In this temporary fix, we play on the evaluation order implemented by
the SimplExpr pass of CompCert (left-to-right for side-effecting
subexpression) to make sure the read part of the read-modify-write
sequence occurs after the evaluation of the right-hand side.
More substantial fixes will be considered later.
Fixes: #395
|
|
|
|
|
|
|
| |
Not yet used for optimizations.
Actually, __builtin_expect is removed during C2C conversion, otherwise
the conversion to type "long" produces inefficient code on 64-bit platforms.
|
|
|
|
| |
Not yet used for optimizations.
|
|
|
|
|
|
|
|
|
|
|
|
| |
The following is correct but was causing a "wrong type for array initializer"
fatal error.
```
struct s { int n; int d[]; };
void f(void) { struct s x = {0}; }
```
Co-authored-by: Michael Schmidt <github@mschmidt.me>
|
| |
|
|
|
|
|
|
|
| |
Variables without init do not generated any assembly code so no entry in
the json AST should be generated. They correspond to extern variables
without initializer that are defined in another compilation unit.
Bug 30112
|