| Commit message (Collapse) | Author | Age | Files | Lines |
|\ |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
|/
|
|
|
|
|
| |
Before, the line number had to start with a nonzero digit. However,
the GCC 11 preprocessor was observed to produce `# 0 ...` directives.
Fixes: #398
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
|
|
| |
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>
|
|
|
|
|
|
|
|
|
|
|
|
| |
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>
|
|
|
|
|
|
|
|
|
| |
- Use pipeline notation `|>` for legibility and better GC behavior
(in bytecode at least).
- Introduce auxiliary functions.
- Remove useless function parameters.
- Fix the timing of the "Emulations" pass
(because of an extra parameter, what was timed took zero time).
|
|
|
|
|
|
|
|
| |
After Menhir version 20210310, the `Fail_pr` constructor of the
`parse_result` type becomes `Fail_pr_full` with two extra arguments.
This PR enables CompCert to handle both versions of the `parse_result`
type in MenhirLib.
|
|
|
|
|
| |
The configure script still accepts "macosx" for backward compatibility,
but every other part of CompCert now uses "macos".
|
|
|
|
|
|
|
| |
Follow-up to 35e2b11db.
Put the warning "pragmas are ignored inside functions" inside the Unnamed
category, so that it is displayed by default and cannot be disabled.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Pragmas can occur either outside external declarations, at the top level
of a compilation unit, or within a compound statement, inside a function
definition.
The parse tree in cparse/C.mli cannot represent pragmas occuring within
a compound statement.
In this case, the elaborator used to silently move the pragma to top
level, just before the function definition where the pragma occurs.
It looks safer to just ignore pragmas occurring inside a function
definition, and emit a specific warning.
|
|
|
|
|
| |
This commit adds support for macOS (and probably iOS) running on
AArch64 / ARM 64-bit / "Apple silicon" processors.
|
|
|
|
|
| |
All the built-in types declared in $ARCH/CBuiltins.ml are now recognized
as type names initially.
|
|
|
|
|
| |
Also: improve check for ptr - integer.
(Added by Xavier Leroy <xavier.leroy@college-de-france.fr>)
|
| |
|
| |
|
|
|
|
|
|
| |
Not all pre-processors concatenate string literal lists, however they
are allowed in _Static_assert. This is similar to the rules for inline
assembly etc.
|
|
|
|
| |
We check that this builtin function is only called from within a variadic
function and has the correct number of arguments.
|
| |
|
|
|
|
|
| |
Added error descriptions for the new syntax errors introduced by
'_Static_assert'.
|
| |
|
|
|
|
|
| |
Returns 1 if the argument is a constant expression, 0 otherwise.
Closes: #366
|
| |
|
|
|
|
|
|
| |
We check in the initial environment if a function is already defined to
avoid redefinition of functions that are part of the builtin
environment.
|
| |
|
|
|
|
|
| |
The name_of_register and register_of_name function are shared between
all architectures and can be moved in a common file.
|
|
|
|
|
|
|
| |
The function String.uppercase was deprecated and the replacement
function String.upercase_ascii was only available from OCaml 4.03.0.
Since the minimal OCaml version is now 4.05.0 we can use the function
String.upercase_ascii.
|
|
|
|
|
| |
Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None`
by a call to the function Hashtbl.find_opt.
|
| |
|
| |
|
| |
|
|
|
| |
In case of redefinition of a typedef name with a different type.
|
|
|
|
| |
See ISO C2011 standard, section 6.4.4.4 para 11.
|
|
|
|
|
|
| |
"open!" is the form used in the examples in the OCaml manual.
Based on a quick poll it seems to be the preferred form of the OCaml
core dev team.
|
|
|
|
| |
Some preprocessors don't remove the vertical tab from the input
so we should be able to handle them in the lexer.
|
|
|
|
|
|
|
|
|
| |
Previously, using an unknown builtin function was treated like any
other call to an undeclared function: a warning was emitted, and
an error occurred at link-time.
With this commit, using an unknown builtin function is an error,
like in Clang.
|
| |
|
|
|
|
|
|
|
| |
Instead of constructing four different lists for maintaining the
state of the warnings only one list is now used. This list contains
the name of the warning and a boolean indicating whether this option
should be active by default. The rest is computed from this list.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Extend check for incomplete type.
Extended the check to also include a check for variables with
incomplete object type that are not arrays, that have an
initializer. Furthermore the warning includes the type and variable
name.
* Warning for incomplete type in compound literals.
Incomplete types are not allowed for compound literals, except for
array types.
* Extend type printing function.
The type of a typedeof of an anonymous type should not be printed.
Furthermore added '<anonymous>' to the printing of anonymous types.
* Unify incomplete type errors message.
The incomplete type error messages should all look the same including
name of the variable, parameter, etc. and then the incomplete type.
|
|
|
|
|
|
| |
In ISO C, inline functions behaves differently whether they have been declared `extern` at least once or not (i.e. all the declarations have no `extern` and no `static` modifier).
Hence, functions that have been declared / defined `extern` once should remain `extern` when redeclared without `extern`. This gives the ISO C behavior for inline functions and has no impact for non-inline functions.
|
|
|
|
|
| |
This commit adds a back-end for the AArch64 architecture, namely ARMv8
in 64-bit mode.
|
|
|
|
|
| |
It is type-checked like a conditional expression then translated to
a call to the known builtin function.
|
|
|
|
|
|
|
|
|
| |
Move its definitions to modules C (the type `builtins`) and Env
(the operations that deal with the initial environment).
Reasons for the refactoring:
1- The name "Builtins" will soon be reused for a Coq module
2- `Env.initial()` makes more sense than `Builtins.environment()`.
|
|
|
|
|
|
| |
The warning should only be active if the optimization is active,
so the check is only performed when the warning is active and
additionally the command line flag -Obranchless is specified.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Do not use `Pervasives.xxx` qualified names
Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`,
and uses of `Pervasives` cause fatal warnings.
This commit uses unqualified names instead, as no ambiguity occurs.
* Clarify "open" statements
OCaml 4.08.0 has stricter warnings concerning open statements that
shadow module names.
Closes: #300
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
What's new:
1. A rewrite of the Coq interpreter of Menhir automaton, with
dependent types removing the need for runtime checks for the
well-formedness of the LR stack. This seem to cause some speedup on
the parsing time (~10% for lexing + parsing).
2. Thanks to 1., it is now possible to avoid the use of int31 for
comparing symbols: Since this is only used for validation,
positives are enough.
3. Speedup of Validation: on my machine, the time needed for compiling
Parser.v goes from about 2 minutes to about 1 minute. This seem to
be related to a performance bug in the completeness validator and
to the use of positive instead of int31.
3. Menhir now generates a dedicated inductive type for
(semantic-value-carrying) tokens (in addition to the already
existing inductive type for (non-semantic-value-carrying)
terminals. The end result is that the OCaml support code for the
parser no longer contain calls to Obj.magic. The bad side of this
change is that the formal specification of the parser is perhaps
harder to read.
4. The parser and its library are now free of axioms (I used to use
axiom K and proof irrelevance for easing proofs involving dependent
types).
5. Use of a dedicated custom negative coinductive type for the input
stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a
positive coinductive type, which are now deprecated by Coq.
6. The fuel of the parser is now specified using its logarithm instead
of its actual value. This makes it possible to give large fuel
values instead of using the `let rec fuel = S fuel` hack.
7. Some refactoring in the lexer, the parser and the Cabs syntax tree.
The corresponding changes in Menhir have been released as part of
version 20190626. The `MenhirLib` directory is identical to the
content of the `src` directory of the corresponding `coq-menhirlib`
opam package except that:
- In order to try to make CompCert compatible with several Menhir
versions without updates, we do not check the version of menhir
is compatible with the version of coq-menhirlib. Hence the
`Version.v` file is not present in CompCert's copy.
- Build-system related files have been removed.
|