| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
|
|
|
|
| |
The name_of_register and register_of_name function are shared between
all architectures and can be moved in a common file.
|
|
|
|
|
| |
The function is in fact just a call to the
function`is_callee_save_register` from `Conventions1.v`.
|
|
|
|
|
| |
Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None`
by a call to the function Hashtbl.find_opt.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The "size_arguments" function and its properties can be systematically
derived from the "loc_arguments" function and its properties.
Before, the RISC-V port used this derivation, and all other ports
used hand-written "size_arguments" functions and proofs.
This commit moves the definition of "size_arguments" to the
platform-independent file backend/Conventions.v, using the systematic
derivation, and removes the platform-specific definitions.
This reduces code and proof size, and makes it easier to change the
calling conventions.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Some ABIs leave more flexibility concerning function return values
than CompCert expects.
For example, the x86 ABI says that a function result of type "char" is
returned in register AL, leaving the top 24 bits of register EAX
unspecified, while CompCert expects EAX to contain 32 valid bits,
namely the zero- or sign-extension of the 8-bit result.
This commits adds a general mechanism to insert "re-normalization"
conversions on the results of function calls. Currently, it only
deals with results of small integer types, and inserts zero- or
sign-extensions if so instructed by a platform-dependent function,
Convention1.return_value_needs_normalization.
The conversions in question are inserted early in the front-end, so
that they can be optimized away in the back-end.
The semantic preservation proof is still conducted against the
CompCert model, where the return 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 return values that are not normalized.
|
|
|
|
|
|
|
|
|
|
| |
Before it was "option typ". Now it is a proper inductive type
that can also express small integer types (8/16-bit unsigned/signed integers).
One benefit is that external functions get more precise types that
control better their return values. As a consequence,
the CompCert C type preservation property now holds unconditionally,
without extra typing hypotheses on external functions.
|
|
|
|
| |
This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95.
|
|
|
|
|
|
|
| |
The `__builtin_nop` function is documented only for PowerPC.
It was added to the other architectures by copy paste, but has no
known uses. So, remove `__builtin_nop` from all architectures
but PowerPC.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The json export prints formatted json, which takes a lot of
additional time, however the result is only consumed by other tools
and not meant for human reading.
This commit implements several small changes in order to speedup
the json export:
* Removal of usage of the Format Module
* Replacing `fprintf` calls by calls to function that print
directly, such as `output_string`, etc.
* Replacing list of all instruction names by a set of all
instructions
|
|\
| |
| |
| | |
Support target architecture AArch64 (ARMv8 in 64-bit mode)
|
| |
| |
| | |
Some changes were not correctly propagated to all architectures.
|
| | |
|
|/
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commit adds mechanisms to
- recognize certain built-in and run-time functions by name and signature;
- associate semantics to these functions, as a partial function from
list of values to values;
- interpret external calls to these functions according to this semantics
(pure function from values to values, memory unchanged, no observable
events in the trace);
- external calls to unknown built-in and run-time functions remain
interpreted as generating observable events and possibly changing
memory, like before.
The description of the built-ins is split into a target-independent
part (in common/Builtins0.v) and a target-specific part (in
$ARCH/Builtins1.v).
Instruction selection uses the new mechanism in order to
- recognize some built-in functions and turn them into operations
of the target processor. Currently, this is done for
__builtin_sel and __builtin_fabs; more to come.
- remove the axioms about int64 helper functions from the standard
library. More precisely, the behavior of these functions is
still axiomatized, but now it is specified using the more general
machinery introduced in this commit, rather than ad-hoc axioms
in backend/SplitLongproof.
The only built-ins currently described are __builtin_fsqrt (for all platforms)
and __builtin_fmin / __builtin_fmax (for x86). More built-ins will be
added later.
|
|
|
|
|
|
|
|
|
| |
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()`.
|
|
|
|
|
|
|
|
| |
We just lift the corresponding functions from Flocq and add
the computation of NaN payloads.
NaN payloads for FMA are described in the ARM and RISC-V specifications,
and were determined experimentally for x86 and for Power.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When an FP arithmetic instruction produces a NaN result, the payload
of this NaN depends on the architecture.
Before, the payload behavior was specified by 3 architecture-dependent
parameters: `Archi.choose_binop_pl_64` and `Archi.choose_binop_pl_32`
and `Archi.fpu_results_default_qNaN`. This was adequate for
two-argument operations, but doesn't extend to FMA.
In preparation for FMA support, this commit generalizes the `Archi.choose`
functions from two arguments to any number of arguments. In passing,
`Archi.fpu_results_default_qNaN` is no longer needed.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|
|
|
|
|
| |
The "vmov" instruction (Advanced SIMD) cannot be conditional.
The "vmov.f64" instruction (VFPv2) can be conditional.
|
|
|
|
|
| |
The operation comples down to conditional moves.
Both integer and floating-point conditional moves are supported.
|
|
|
|
|
|
|
|
|
|
| |
The option -fcommon controls whether uninitialized global
variables are placed in the COMMON section. If the option is given
in the negated form, -fno-common, variables are not placed in the
COMMON section. They are placed in the same sections as gcc does.
If the variables are not placed in the COMMON section merging of
tentative definitions is inhibited and multiple definitions lead
to a linker error, as it does for gcc.
|
|
|
|
|
|
|
|
|
|
| |
The module Integers.Make contained lots of definitions and theorems
about Z integers that were independent of the word size. These
definitions and theorems are useful outside Integers.Make, but
it felt unnatural to fetch them from modules Int or Int64.
This commit moves the word-size-independent definitions and theorems
to a new module, lib/Zbits.v, and fixes their uses in the code base.
|
|
|
|
|
| |
Instead, use definitions and lemmas from the Coq standard library
(ZArith, Znumtheory).
|
|
|
|
|
|
|
|
|
|
|
|
| |
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).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Generate a nop instruction after ais annotations.
In order to prevent the merging of ais annotations with following
Labels a nop instruction is inserted, but only if the annotation
is followed immediately by a label.
The insertion of nop instructions is performed during the
expansion of builtin and pseudo assembler instructions and is
processor independent, by inserting a __builtin_nop built-in.
* Add Pnop instruction to ARM, RISC-V, and x86
ARM as well as RISC-V don't have nop instructions that can
be easily encoded by for example add with zero instructions.
For x86 we used to use `mov X0, X0` for nop but this may
not be as efficient as the true nop instruction.
* Implement __builtin_nop on all supported target architectures.
This builtin is not yet made available on the C side for all architectures.
Bug 24067
|
|
|
|
|
| |
Follow-up to f6f537d. "list" scope must be opened to counterbalance
opening of "string" scope.
|
|
|
|
|
|
|
|
|
|
| |
The semantics of external function calls in LTL, Linear, Mach and Asm
now consider that all caller-save registers are set to Vundef by the call.
This models that fact that the external function can modify those registers
arbitrarily.
Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes
accordingly.
|
|
|
|
|
|
| |
This allows us to replacing them by their address in valex and
additionally checking them.
Bug 22438
|
|
|
|
|
|
| |
It should be 'esp' respectively 'rsp' for x86, 'r13' for arm and
'sp' for riscV.
Bug 23176.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When x is known to be either 0 or 1, comparisons such as
x == 0 x != 0 x == 1 x != 1
can be optimized away. This optimization was already performed
for signed comparisons. This commit extends the optimization to
unsigned comparisons as well.
Additionally, for PowerPC only, some unsigned (dis)equality comparisons are
turned into signed comparisons when we know it makes no difference,
i.e. when both arguments are guaranteed not to be pointers. The
reason is that Asmgen can produce shorter instruction sequences for
some signed equality comparisons than for the corresponding unsigned
comparisons.
It's important to optimize unsigned integer comparisons because casts
to the C99 type _Bool are compiled as x !=u 0 unsigned comparisons.
In particular, cascades of casts to _Bool are now reduced to a single
cast much more often than before.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* 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.
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Some files are dual-licensed (GPL + noncommercial license), as marked redundantly in the license headers of those files, and in the LICENSE file. OVer the years those two markings got inconsistent.
This commit updates the LICENSE file and the license headers of some files so that they agree on which files are dual-licensed.
Some build-related files were dual-licensed but some others were not. Fixed by dual-licensing configure, Makefile.menhir, extraction/extraction.v, */extractionMachdep.v
Moved lib/Json* to backend/ because there is no need to dual-license those files, yet lib/* is dual-licensed. Plus: JsonAST did not really belong in lib/ anyway, as it depends on AST
which is not in lib/
|
| |
|
| |
|
|
|
|
| |
immediates can be encoded.
|
|
|
|
|
| |
This commit introduces a new pass which is run after the expansion of the
builtin functions which performs the expansion and placement of
constants inside the function code.
|
|
|
|
| |
assembler (add ra, rb, #-1 --> sub ra, rb, #1)
|
|
|
| |
The architecture which was configured is now exported in a new top-level json field.
|
|
|
|
| |
Signed and unsigned divisions by literal 1 are already optimized away during the Selection phase. This pull request also optimizes those divisions when the 1 divisor is produced by constant propagation.
|
| |
|
|
|
|
|
|
|
| |
The json export for the abstract ARM Assembler is quite similar
to it's PowerPC equivalent expect for the different instruction
arguments.
Bug 22472
|