| Commit message (Collapse) | Author | Age | Files | Lines |
|---|
| |
|
|
|
|
| |
Instead, evaluate it for the side effects it may contain.
Fixes: #474
|
| |
|
|
| |
Fixes: #472
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- New elaboration pass: SwitchNorm
- recognizes structured 'switch' statements and puts them in a
normalized form;
- if selected, transforms unstructured 'switch' statements into a
structured switch with goto actions + the original switch body
with appropriate labels and gotos.
- C2C treatment of 'switch' statements is simplified accordingly.
- New language support option `-funstructured-switch`.
- Some tests were added (test/regression/switch3.c).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Support C11 Unicode string literals and character constants
* Add tests for C11 string literals and character constants
* Better error message for ill-formed universal character names
E.g. \u followed by fewer than 4 hex digits, or \U followed by fewer than 8 hex digits.
* Add new warning `invalid-utf8` for byte sequences that are not valid UTF8.
The warning is activated but not fatal by default.
* Warn on uses of C11 Unicode character constants and string literals
This uses the `c11-extensions` warning, which is off by default.
* Support preprocessing option -finput-charset= for GNU toolchains
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
The struct member byte and bit offsets are now set based upon the new
function `struct_layout` from Ctypes.v, thus using the same code to
compute as used to generate the actual struct access.
The struct offset member information is addded using the types computed
after the translation in C2C. Therefore we need to store the new internal
names of the members as well as the composites and use them
when adding the offset information.
Fixes: #445
|
| |
|
|
|
| |
Note that strings containing null characters (code 0) cannot be put in
a mergeable section, as this will confuse the linker's merging criterion.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
On platforms that support them (ELF, macOS), use mergeable sections
(like `.rodata.cst8`) for 4-, 8- and 16-byte wide literals.
Works only if the LITERAL section is the default one. If the user
provided their own LITERAL section, all literals are put in it
regardless of their sizes.
Support for mergeable string sections is introduced in this commit too
but needs further changes in C2C.ml .
|
| |
|
|
|
|
|
| |
If any are found, make sure that `-fstruct-passing` was given.
Previously, we used to check the fixed arguments (as part of a call to
`checkFunctionType`) but not the variable arguments.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |/
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Distinguish between:
- uninitialized variables, which can go in COMM if supported
- variables initialized with fixed, numeric quantities,
which can go in a readonly section if "const"
- variables initialized with symbol addresses which may need relocation,
which cannot go in a readonly section even if "const",
but can go in a special "const_data" section.
Also: on macOS, use ".const" instead of ".literal8" for literals,
as not all literals have size 8.
|
| |
|
|
|
|
| |
Instead of being a simple boolean we now use an option type to record
the number of fixed (non-vararg) arguments. Hence, `None` means
not vararg, and `Some n` means `n` fixed arguments followed with varargs.
|
| |
|
|
|
|
|
| |
When running unit tests with the CompCert reference interpreter, it's nice to be able to start execution at a given test function instead of having to write a main function.
This PR adds a -main command-line option to give the name of the entry point function. The default is still main. Frama-C has a similar option.
The function specified with -main is called with no arguments. If its return type is int, its return value is the exit status of the program. Otherwise, its return value is ignored and the program exits with status 0.
|
| |
|
|
| |
__builtin_sqrt (no "f") is the name used by GCC and Clang.
|
| |
|
|
| |
These functions are now available on all targets.
|
| | |
|
| |
|
|
|
|
|
|
| |
Introduce an error message for section attributes with non string
arguments,and another for multiple, ambiguous section attributes.
This is more consistent with the handling of other
attributes, like packed, than the old behavior of silently
ignoring them.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We can get linker errors for addresses of the form "symbol + offset"
where "symbol" is in the small data area and "offset" is large enough
to overflow the relative displacement from the SDA base register.
To avoid this, this commit enriches `C2C.atom_is_small_data`,
which is the implementation of `Asm.symbol_is_small_data` in the PPC port,
with a check that the offset is within the bounds of the symbol.
If it is not, `Asm.symbol_is_small_data` returns `false` and Asmgen produces
an absolute addressing instead of a SDA-relative addressing.
To implement the check, we record the sizes of symbols in the atom table,
just like we already record their alignments.
|
| |
|
|
|
|
|
|
|
| |
In addressing modes for load and store instructions, the offset must be a multiple of the memory size being accessed. When accessing global variables, this may not be the case if the alignment of the variable is less than its size. Errors occur at link time.
This PR extends the check for a representable offset for the addressing of global
variables to also check whether the variable is correctly aligned. Only if both conditions are
met can we generate the short sequence Padrp / ADadr. Otherwise we go through the generic
loadsymbol sequence.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
* Added semantic for byte swap builtins
The `__builtin_bswap`, `__builtin_bswap16`, `__builtin_bswap32`, `__builtin_bswap64` builtin function are now standard builtin functions with a defined semantics.
The semantics is given in terms of the decode/encode functions used for the memory model.
* Added bswap64 expansion to PowerPC 32 bits.
* Added bswap64 expansion for ARM.
|
| |
|
|
|
| |
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()`.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Currently, the arguments to __builtin_annot, __builtin_ais_annot,
__builtin_debug, and extended asm statements are treated like
arguments to an unprototyped or vararg function call. In particular,
arguments of type "float" are converted to "double", generating useless
code.
To avoid this extra, useless conversion, this commit changes the types
expected for the arguments to these built-ins and to extended asm
statements. Now they are the types of the arguments themselves, after
performing the usual unary conversions (e.g. char -> int), but without
the problematic float -> double conversion. This ensures that no code
is generated to change the representation of the arguments.
|
| |
|
|
|
|
| |
This is a manual, partial merge of Github pull request #296 by @Fourchaux.
flocq/, cparser/MenhirLib/ and parts of test/ have not been changed
because these are local copies and the fixes should be performed upstream.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Main changes to CompCert outside of Flocq are as follows:
- Minimal supported version of Coq is now 8.7, due to Flocq requirements.
- Most modifications are due to Z2R being dropped in favor of IZR and to
the way Flocq now handles NaNs.
- CompCert now correctly handles NaNs for the Risc-V architecture
(hopefully).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is a second step towards mimicking GCC/Clang's handling of attributes.
This commit introduces a distinction between
- Object-related attributes, such as "section", which apply to the object (function, variable) being defined;
- Name-related attributes, such as "aligned", which apply to the name (object, struct/union member, struct/union/enum tag) being defined.
In particular, "aligned" is now attached to "struct" and "union" definitions, while it used to be "floated up" before.
The C11 _Alignas modifier is treated like an object-related attribute, so that
```
struct s { ... };
_Alignas(64) struct s x;
```
correctly associates the alignment with "x" and not with "struct s", where it would be ignored because it was not part of the original definition of s.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* bug 24268: avoid assertion after reporting error for invalid call to builtin_debug
* bug 24268, remove duplicated warning tag in lexer messages
* bug 24268, fix spelling in array element designator message
* bug 24268, unify 'consider adding option ...' messages
* bug 24268, add spacing for icbi operands
* bug 24268, uniform use of Ignored_attributes class for identical warnings
* bug 24268, unify message for 'assignment to const type' to error from error/fatal error
* bug 24268, in handcrafted.messages, "a xxx have been recognized" -> "a xxx has been recognized"
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Refactor common code of alignas.
Instead of working on attributes the function now works directly
on the type since the check always performed an extraction of
attributes from a type.
Bug 23393
* Attach _Alignas to the name.
Bug 23393
* Attach "aligned" attributes to names
So that __attribute((aligned(N))) remains consistent with _Alignas(N).
gcc and clang apply "aligned" attributes to names, with a special case
for typedefs:
typedef __attribute((aligned(16))) int int_al_16;
int_al_16 * p;
__attribute((aligned(16))) int * q;
For gcc, p is naturally-aligned pointer to 16-aligned int and
q is 16-aligned pointer to naturally-aligned int.
For CompCert with this commit, both p and q are 16-aligned pointers
to naturally-aligned int.
* Resurrect the alignment test involving typedef
The test was removed because it involved an _Alignas in a typedef,
which is no longer supported. However the same effect can be achieved
with an "aligned" attribute, which is still supported in typedef.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
CompCert has two implementations of sizeof, alignof and offsetof (byte offset of a struct field):
- the reference implementation, in Coq, from cfrontend/Ctypes.v
- the implementation used during elaboration, in OCaml, from cparser/Cutil.ml
The reference Coq implementation is used as much as possible, but sometimes during elaboration the size of a type must be computed (e.g. to compute array sizes), or the offset of a field (e.g. to evaluate __builtin_offsetof), in which case the OCaml implementation is used.
This causes issues with packed structs. Currently, the cparser/Cutil.ml functions ignore the "packed" attribute on structs. Their results disagree with the "true" sizes, alignments and offsets computed by the cfrontend/Ctypes.v functions after source-to-source transformation of packed structs as done in cparser/PackedStruct.ml. For example:
```
struct __packed__(1) s { char c; short s; int i; };
assert (__builtin_offsetof(struct s, i) == 3);
assert (sizeof(struct s) = sizeof(char[sizeof(struct s)]));
```
The two assertions fail. In the first assertion, __builtin_offsetof is elaborated to 4, because the packed attribute is ignored during elaboration. In the second assertion, the type `char[sizeof(struct s)]` is elaborated to `char[8]`, again because the packed attribute is ignored during elaboration, while the other `sizeof(struct s)` is computed as 7 after the source-to-source transformation of packed structs.
This commit changes the cparser/Cutil.ml functions so that they take the packed attribute into account when computing sizeof, alignof, offsetof, and struct_layout.
Related changes:
* cparser/Cutil: add `packing_parameters` function to extract packing info from attributes
* cparser/Cutil: refactor and share more code between sizeof_struct, offsetof, and struct_layout
* cparser/Elab: check the alignment parameters given in packed attributes. (The check was previously done in cparser/PackedStruct.ml but now it would come too late.)
* cparser/Elab: refactor the checking of alignment parameters between _Alignas, attribute((aligned)), __packed__, and attribute((packed)).
* cparser/PackedStructs: simplify the code, some functionality was moved to cparser/Cutil, other to cparser/Elab
* cfrontend/C2C: raise an "unsupported" error if a packed struct is defined and -fpacked-structs is not given. Before, the packed attribute would be silently ignored, but now doing so would cause inconsistencies between cfrontend/ and cparser/.
* test/regression/packedstruct1.c: add tests to compare the sizes and the offsets produced by the elaborator with those obtained after elaboration.
|
| |
|
|
|
| |
This is a follow-up to commit 6e1a5ce.
Another `open! Floats` is needed.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Allow strings literals as lvalues.
Strings and WStrings literals are lvalues, thus it is allowed to take their
addresses.
Bug 23356.
* String literals have types "array of (wide) char", not "pointer to (wide) char"
The pointer types were a leftover from the early, CIL-based C frontend.
* Remove special case for sizeof("string literal") during elaboration
No longer needed now that literals have array types.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
The Elab pass checks that the argument of 'case' is a compile-time constant
expression. This commit records the value of this expression in the
C.Scase AST generated by Elab, so that it can be used for further
diagnostics, i.e. checking (in Elab) for duplicate cases.
Note that C2C ignores the recorded value and recomputes the value of
the expression using Ceval.integer_expr. This is intentional:
Ceval.integer_expr is more trustworthy, as it is formally verified
against the CompCert C semantics.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
Adds a warning when a volatile struct is assigned to another
struct, that the volatile qualifier is ignored in this context.
Example:
```
volatile struct S s;
struct S t;
t = s; // did not warn before; now it warns
s = t; // did warn already
```
Bug 23489
|
| |
|
|
|
|
|
|
| |
The checks on the argument and format arguments are now performed
during C2C translation by calling the validate_ais_annotations
function and result in an error instead of a warning in the
backend to be more consistent with the rest of the builtin
functions.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The ais annotations are now handled in a separate file shared
between all architectures. Also two different variants of
replacements are supported, %e which expands to ais expressions
and %l which also expands to an ais expression but is guaranted to
be usable as l-value in the ais annotation. Otherwise the new
warning is Wrong_is_parameter is generated.
Also an error message is generated if floating point variables are
used in ais annotations since a3 does not support them at the
moment.
Additionally an error message is generated for plain volatile
variables used, since they will enforce a volatile load and result
in the value being passed to the annotation instead of the address
as other global variables.
|
| |
|
|
|
|
|
|
|
|
| |
The size (number of elements) of an array type is represented as an OCaml int64 in the parse tree, and as a Coq Z in the CompCert C AST. However, the C2C.convertInt function used to do this conversion produces a Coq int (32 bits) type, taking the array size modulo 2^32. This is not correct, esp. on a 64-bit target.
This commit refactors C2C around three integer conversion functions:
convertInt32 producing a Coq "int" (32 bit)
convertInt64 producing a Coq "int64" (64 bit)
convertIntZ producing a Coq "Z" (arbitrary precision)
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Module Cerrors is now called Diagnostic and can be used in parts of CompCert other than cparser/
* Replaced eprintf error. Instead of having eprintf msg; exit 2 use the functions from the
Diagnostics module.
* Raise on error before calling external tools.
* Added diagnostics to clightgen.
* Fix error handling of AsmToJson.
* Cleanup error handling of Elab and C2C.
*The implementation of location printing (file & line) is simplified and correctly prints valid filenames with invalid lines.
|
| | |
|
| | |
|
| |
|
|
|
|
| |
Instead of two Boolean tests C2C.atom_is_{no,}inline, have a single
C2C.atom_inline function that returns one of the three possible values
stored in the the a_inline field.
|
| |
|
|
|
|
|
| |
In order to correctly support the noinline attribute we must store
whether the function was specified with an inline specifer, had
a noinline attribute or nothing.
Bug 22642
|
| | |
|
| |
|
|
|
|
| |
The file and line information are now stored as comment string at
the start of each annotation.
Bug 22462
|
| |
|
|
|
|
|
|
|
|
|
|
| |
The ais annotations can be inserted via the new ais variants of
the builtin annotation. They mainly differe in that they have an
address format specifier '%addr' which will be replaced by the
adress in the binary.
The implementation simply prints a label for the builtin call
alongside a the text of the annotation as comment and inserts the
annotation together as acii string in a separate section
'ais_annotations' and replaces the usages of the address format
specifiers by the address of the label of the builtin call.
|
| | |
|
| |
|
|
|
|
|
| |
The runtime functions are prefixed with compcert in order to
avoid potential clashes with runtime/builtin functions of other
compilers.
Bug 22062
|
