| 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/
|
|
|
|
|
|
|
|
|
|
|
|
| |
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>
|
|
|
|
|
| |
The configure script still accepts "macosx" for backward compatibility,
but every other part of CompCert now uses "macos".
|
|
|
|
| |
Now subsumed by the tests in abi/
|
|
|
|
| |
Using a combination of fixed and randomly-generated function signatures.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is a follow-up to e81d015e3.
In the RISC-V ABI, FP arguments to functions are passed in integer registers
(or pairs of integer registers) in two cases:
1- the FP argument is a variadic argument
2- the FP argument is a fixed argument but all 8 FP registers reserved for
parameter passing have been used already.
The previous implementation handled only case 1, with some problems.
This commit implements both 1 and 2. To this end, 8 extra FP
caller-save registers are used to hold the values of the FP arguments
that must be passed in integer registers. Fixup code moves these FP
registers to integer registers / register pairs. Symmetrically, at
function entry, the integer registers / register pairs are moved back
to the FP registers.
8 extra FP registers is enough because there are only 8 integer
registers used for parameter passing, so at most 8 FP arguments may
need to be moved to integer registers.
|
|
|
|
|
|
|
|
|
| |
This is a follow-up to 2076a3bb3.
Integer registers were wrongly reserved for fixed FP arguments,
causing variadic FP arguments to end up in the wrong integer registers.
Added regression test in test/regression/varargs2.c
|
| |
|
|
|
|
| |
Use different combination of options for different test files.
|
|
|
|
| |
configure flags -use-external-Flocq and -use external-MenhirLib.
|
| |
|
|
|
|
|
|
| |
Share the testing code for built-in functions that are available on
all target platforms.
Improve testing of __builtin_clz* and __builtin_ctz*
|
|
|
|
| |
__builtin_ais_annot is not supported for macOS nor for Cygwin.
|
|
|
|
|
|
|
|
|
|
|
|
| |
The printing of EF_annot and EF_annot_val was missing the extra "kind"
parameter introduced in commit 6a010b4.
Also: the automatic translation of annotations into Coq assertions
was confusing and prevented other uses of __builtin_annot statements
in conjunction with clightgen. I believe it was never used.
This commit removes this translation.
Closes: #360
|
|
|
|
|
| |
This is a special value that causes double rounding with the naive
conversion schema int64 -> float64 -> float32.
|
| |
|
|
|
|
|
| |
A "dollar" sign in a function name or a global variable name was producing
incorrect Coq identifiers. (Issue #319.)
|
|
|
|
|
|
|
|
| |
Initially, the "bench" entries of the test suite used a "xtime" utility
developed in-house and not publically available.
This commit adds a version of "xtime" written in OCaml (tools/xtime.ml)
and updates the "bench" entries of the test/*/Makefile to use it.
|
|
|
|
| |
With special emphasis on the use of the AArch64 fmov #imm instruction.
|
|
|
|
|
| |
This commit adds a back-end for the AArch64 architecture, namely ARMv8
in 64-bit mode.
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Now that some builtin functions have known semantics, constant
propagation can happen in this test. This defeats the purpose,
which is to check that the correct processor instructions are generated.
To prevent this constant propagation, we move the initialized
variables to global scope. Since they are not "const", their
values are not known to the optimizer.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When printing an extended asm code fragment, placeholders %n
are replaced by register names.
Currently we ignore the fact that some assemblers use different
register names depending on the width of the data that resides
in the register.
For example, x86_64 uses %rax for a 64-bit quantity and %eax for
a 32-bit quantity, but CompCert always prints %rax in extended asm
statements. This is problematic if we want to use 32-bit integer
instructions in extended asm, e.g.
int x, y;
asm("addl %1, %0", "=r"(x), "r"(y));
produces
addl %rax, %rdx
which is syntactically incorrect.
Another example is ARM FP registers: D0 is a double-precision float,
but S0 is a single-precision float.
This commit partially solves this issue by taking into account the
Cminor type of the asm parameter when printing the corresponding register.
Continuing the previous example,
int x, y;
asm("addl %1, %0", "=r"(x), "r"(y));
now produces
addl %eax, %edx
This is not perfect yet: we use Cminor types, because this is all we
have at hand, and not source C types, hence "char" and "short" parameters
are still printed like "int" parameters, which is not good for x86.
(I.e. we produce %eax where GCC might have produced %al or %ax.)
We'll leave this issue open.
|
|
|
|
|
| |
A conditional move whose condition is statically known becomes a regular move.
Otherwise, the condition can sometimes be simplified by strength reduction.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Extends the instruction selection pass with an if-conversion optimization:
some if/then/else statements are converted into "select" operations,
which in turn can be compiled down to branchless instruction sequences
if the target architecture supports them.
The statements that are converted are of the form
if (cond) { x = a1; } else { x = a2; }
if (cond) { x = a1; }
if (cond) { /*skip*/; } else { x = a2; }
where a1, a2 are "safe" expressions, containing no operations that can
fail at run-time, such as memory loads or integer divisions.
A heuristic in backend/Selectionaux.ml controls when the optimization occurs,
depending on command-line flags and the complexity of the "then" and "else"
branches.
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Consider:
```
struct s { ... } __attribute((aligned(N)));
struct t { ... }
__attribute((aligned(N))) struct t x;
```
In the first case, the aligned attribute should be attached to struct s, so that further references to struct s are aligned.
In the second case, the aligned attribute should be attached to the variable x, because if we attach it to struct t, it will be ignored and cause a warning.
This commit changes the attachment rule so that it treats both cases right.
Extend regression test for "aligned" attribute accordingly, by testing
aligned attribute applied to a name of struct type.
|
|
|
|
| |
Expected results were obtained with GCC 5.4 and Clang 8.0
|
|
|
|
|
| |
Sometimes a vararg function receives a NULL-terminated list of pointers.
This can fail if sizeof(NULL) < sizeof(void *), as this test illustrates.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
|
|
|
|
|
| |
- Make it possible to skip tests on some platforms
- Make it possible to expect a failure (typically: of the reference interpreter)
- Stop on error
|
|
|
|
|
| |
Follow-up to b9a6a50. clang is not happy with COMPCERT_MODEL=32sse2
("bad suffix on integer"), so use MODEL_32sse2 and ARCH_x86 instead.
|
|
|
|
|
|
|
| |
Pass more info from CompCert's configuration as #define on command line.
Use this info to improve the "64 bit" detection in extasm.c.
(Before it fails with powerpc-ppc64, which has 64-bit int regs but
couldn't be detected with #ifdefs.)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
| |
The `_Alignas(expr)` construct is not C11, only `_Alignas(type)` is.
|
|
|
|
|
| |
It's not really necessary, and under Windows it's really ../../clightgen.exe,
which confuses make.
|
|
|
|
| |
Also: add "parallel" entry to test/Makefile for parallel execution of tests.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
For anonymous bit-fields in structs, carrier fields may
be introduced which are not initialized since no default
initializer are generated earlier. This cause the translation in
C2C to throw an error since too few initializers are available.
Example:
struct s2 {
int : 10;
int a;
int : 10;
char b;
int : 10;
short c;
int : 10;
} s2 = { 42, 'a', 43 };
To work around this issue we need to generate a default inializer
for every new member that does not have a translated member.
Based on P#80, with more efficient algorithms.
Bug 23362
|
|
|
|
|
|
|
|
|
|
|
| |
Bit fields in unions were initialized like normal fields,
causing mismatch on the name of the field.
Also: added function Bitfields.carrier_field and refactored.
Patch by Bernhard Schommer.
Bug 23362
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Consider:
struct P { int x, y; }
struct S { struct P p; }
struct P p0 = { 1,2 };
struct S s1 = { .p = p0; .p.x = 3 };
ISO C99 and recent versions of Clang initialize s1.p.y to 2, i.e.
the initialization of s1.p.y to p0.y implied by ".p = p0" is kept,
even though the initialization of s1.p.x to p0.x is overwritten
by ".p.x = 3".
GCC, old versions of Clang, and previous versions of CompCert
initialize s1.p.y to the default value 0. I.e. the initialization
".p = p0" is forgotten, leaving default values for the fields of .p
before ".p.x = 3" takes effect.
Implementing the proper ISO C99 semantics in CompCert is difficult,
owing to a mismatch between the intended semantics and the C.init
representation of initializers.
This commit turns the delicate case of reinitialization above
(re-initializing a member of a composite that has already been
initialized as a whole) into a compile-time error.
We will then see if the delicate case occurs in practice and needs
further attention.
|
| |
|
| |
|
|
|
|
|
| |
Not very useful in practice (make clean is generally done before make all)
and problematic under Cygwin where ../../ccomp is really ../../ccomp.exe
|
|
|
|
| |
Otherwise the interpreter uses the system's header files instead of CompCert's. This can lead to mismatches e.g. on the definition of wchar_t.
|
| |
|
| |
|