| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
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
|
|
|
|
|
| |
Seems necessary for the standard headers of a recent version of XCode.
The actual definition in the standard headers is only for GNUC.
|
| |
|
|
|
|
|
|
|
| |
Volatile load and store are expanded later and also use the ld/std
instructions, therefore the same fixes that are applied as well for
them.
Bug 30983
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The offsets immediates used in the ld and std instructions must be a
multiple of the word size. This commit changes the two functions which
are used when generating load/stores in Asmgen, accessind and
transl_memory_access.
For accessind one only needs an additional check that the offset is a
multiple of the word size for the case that the high part of the offset
is zero, since otherwise the immediate is loaded into a register anyway.
The transl_memory_access function needs some slightly more complex
adoption. For all variants that do not construct the address in a
register before hand we must check that the offsets are multiples of the
word size and additionally if a symbol is used that the alignment of the
symbol is also a multiple of the word size. Therefore a new parameter is
introduced that allows checking the alignment.
In order to reduce the code duplication for the proofs these two
functions get an additional parameter in order to indicate wether the
offset needs to be a multiple of the word size or not.
Bug 30983
|
|
|
|
| |
Follow-up to bb5dab848
|
|
|
|
|
| |
The `-version-file` option was removed in commit 600803cae, but remained
in the option summary, as reported in #386.
|
|
|
|
|
|
|
|
|
|
|
| |
This avoids a nasty conflict with Ltac2 notations as reported in #392.
The old `$` notation in scope `string_scope` was not used yet, AFAIK.
The new submodule and the new scope are the right places to add future
notations to facilitate working with the output of clightgen.
Fixes: #392
|
| |
|
|
|
|
| |
This is required to have List.repeat in the standard library (next commit).
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
| |
coq/coq#13852 fixes an oddity in the automatically-generated names for projection parameters.
There was one place in CompCert where one of these automatically-generated names was used.
This commit avoids using this name.
|
|
|
|
| |
Closes: #389
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
On PowerPC/Diab, common declarations must not be used for small data sections.
Add a `~common` option to `PrintAsmaux.variable_section` to control
the use of common declarations. The default is whatever is specified
on the command line using the `-fcommon` and `-fno-common` options.
Use `~common:false` for `Section_small_data` on PowerPC / Diab.
Note that on PowerPC/Linux, GCC uses common declarations for uninitialized
variables in small data section, so we keep doing this in CompCert as well.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
| |
This is a generalization of the previous PrintAsmaux.common_section
function that
- handles initialized variables in addition to uninitialized variables;
- can be used for Section_const, not just for Section_data.
|
|
|
|
|
|
|
|
| |
Either because the code change that would silence the warning is not
desirable, or because it would break compatibility with earlier versions
of Coq.
Explain the silenced warnings as comments in the Makefile.
|
|
|
|
|
|
|
| |
This avoids a new warning of Coq 8.13.
Eventually these `Global Hint` should become `#[export] Hint`,
with a cleaner but different meaning than `Global Hint`.
|
|
|
|
|
|
| |
The extraction mechanism wants to extract them (because they are in
Type, probably). The current opaque definition causes a warning at
extraction-time.
|
|
|
|
|
| |
The configure script still accepts "macosx" for backward compatibility,
but every other part of CompCert now uses "macos".
|
|
|
|
|
| |
The standard includes print irrelevant warnings using `#warning`.
The warnings can be restored by passing `-W#warning` to `ccomp`.
|
|
|
|
| |
Now subsumed by the tests in abi/
|
|
|
|
| |
Using a combination of fixed and randomly-generated function signatures.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This is complementary to 28f235806
Some ABIs leave more flexibility concerning function parameters than
CompCert expects.
For instance, the AArch64/ELF ABI allow the caller of a function to
leave unspecified the "padding bits" of function parameters. As an
example, a parameter of type "unsigned char" may not have zeros in
bits 8 to 63, but may have any bits there.
When the caller is compiled by CompCert, it normalizes argument values
to the parameter types before the call, so padding bits are always
correct w.r.t. the type of the argument. This is no longer guaranteed
in interoperability scenarios, when the caller is not compiled by CompCert.
This commit adds a general mechanism to insert "re-normalization"
conversions on the parameters of a function, at function entry.
This is controlled by the platform-dependent function
Convention1.return_value_needs_normalization.
The semantic preservation proof is still conducted against the
CompCert model, where the argument values of functions are already
normalized. What the proof shows is that the extra conversions have
no effect in this case. In future work we could relax the CompCert
model, allowing functions to pass arguments that are not normalized.
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
| |
In function Asmexpand.next_arg_locations:
If 7 integer parameter passing registers have been used already,
and the next fixed arguments are Tlong then Tint, the Tlong argument
was correctly analyzed as being passed on the stack, but the Tint
argument was incorrectly analyzed as being passed in the 8th register.
|
|
|
|
| |
However it produces new warnings that should be investigated later.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
| |
Follow-up to aba0e740f
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The previous branch tunneling was missing optimization opportunities
introduced by the optimization of conditional branches. For example:
L1: instr; branch L2
L2: if cond then branch L3 else branch L4
L3: branch L4
L4: ...
was transformed into
L1: instr; branch L2
L2: branch L4
L3: branch L4
L4: ...
missing a tunneling opportunity (branch L2 -> branch L4).
This commit improves branch tunneling so that the expected code is produced:
L1: instr; branch L4
L2: branch L4
L3: branch L4
L4: ...
To this end, additional equalities are introduced in the union-find
data structure corresponding to optimizable conditional branches.
In rare cases these additional equalities trigger new opportunities for
optimizing conditional branches. Hence we iterate the analysis
until no optimizable conditional branch remains.
|
|
|
|
|
|
|
|
|
|
| |
We used to define an instrumented version record_goto' that also
builds the measure f, prove it correct, then show equivalence with
record_goto.
The new proofs make do without the instrumented version. They prove
strong existence of the measure, as in
`{ f | branch_map_correct (record_goto fn) f}`.
|
|
|
|
|
|
|
| |
fold_inv is in Type, hence can prove goals such as `{ x | P x }`.
Also, no extensionality property is needed.
fold_rec is now derived from fold_inv.
|