| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |\
| |
| |
| | |
Mostly changes in PTree
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The previous code for elaborating character constants has a small bug:
the value of a wide character constant consisting of several characters
was normalized to type `int`, while, statically, it has type `wchar_t`.
If `wchar_t` is `unsigned short`, for example, the constant `L'ab'`
would elaborate to 6357090, which is not of type `unsigned short`.
This commit fixes the bug by normalizing wide character constants to type
`wchar_t`, regardless of how many characters they contain.
The previous code was odd in another respect: leading `\0` characters
in multi-character constants were ignored. Hence, `'\0bcde'` was accepted
while `'abcde'` caused a warning.
This commit implements a more predictable behavior: the number of characters
in a character literal is limited a priori to
sizeof(type of result) / sizeof(type of each character)
So, for non-wide character constants we can typically have up to 4
characters (sizeof(int) / sizeof(char)), while for wide character
constants we can only have one character.
In effect, multiple-character wide character literals are not supported.
This is allowed by the ISO C99 standard and seems consistent with GCC
and Clang.
Finally, a multi-character constant with too many characters was
reported either as an error (if the computation overflowed the 64-bit
accumulator) or as a warning (otherwise). Here, we make this an error
in all cases.
GCC and Clang only produce warnings, and truncate the value of the
character constant, but an error feels safer.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Earlier CompCert versions would warn if a bit field of width N and
type enum E was too small for the values of the enumeration: whether
the field is interpreted as a N-bit signed integer or a N-bit unsigned
integer, some values of the enumeration are not representable.
This warning was performed in the Bitfields emulation pass, which went
away during the reimplementation of bit fields within the verified
part of CompCert.
In this commit, we resurrect the warning and perform it during the Elab pass.
In passing, some of the code that elaborates bit fields was moved to a
separate function "check_bitfield".
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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
|
| |\| |
|
| | |\ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| |\ \ |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
cfrontend/C2C.ml
|
| |\ \ \
| |/ /
|/| /
| |/
| |
| |
| |
| |
| | |
PARTIAL MERGE (PARTLY BROKEN).
See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE
WARNING:
interface of va_args and assembly sections have changed
|
| | |
| |
| |
| |
| | |
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.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
