| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
|
|
|
|
|
|
|
| |
If the first argument to `isel` is GPR0, it reads as the constant 0.
This cannot occur in code generated by CompCert, due to the fact that
GPR0 is not available as register for register allocation. However the
assembler semantics should be as close as possible to the actual
hardware.
|
| |
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The temporary variables introduced by SimplLocals reuse the same
integer identifiers as the local variables they come from. This commit
ensures that these variables are printed as "$var", where "var"
is the original variable name, instead of "$NNN" as before.
The "$NNN" form is retained for temporary variables that do not
correspond to a source-level local variable, such as the temporary
variables introduced by SimplExpr.
This commit should make no difference for "ccomp -dclight", because
the Clight that is printed is the Clight version 1 produced by
SimplExpr, where every temporary is fresh and does not correspond
to a source-level local variable.
This commit does change the output of "clightgen -dclight", because
the Clight that is printed is the Clight version 2 produced by
SimplLocals. The printed Clight is much more legible thanks to
the more meaningful temporary variable names.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The Clight output of clightgen is Clight version 2, after SimplLocals
conversion, where function parameters are temporary variables, not
variables.
This commit makes sure the function parameters are printed as
temporary variables and not as variables. In passing, it
generalizes the Clight pretty-printer so that it can print
both Clight version 1 and Clight version 2.
Closes: #314
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
|
|
|
| |
"omega" fails in Coq 8.7, but not in 8.8 and later.
|
|\
| |
| |
| | |
Support target architecture AArch64 (ARMv8 in 64-bit mode)
|
| |
| |
| |
| |
| |
| |
| |
| | |
The argument is of type Tlong, not Tint.
This caused spurious errors in RTLtyping.
Also: in AArch64/PrintOp.ml, print Cmaskl{zero,notzero} with "&l"
to distinguish them from Cmask{zero,notzero}.
|
| |
| |
| |
| | |
These instructions are generated by __builtin_memcpy.
|
| |
| |
| | |
Some changes were not correctly propagated to all architectures.
|
| |
| |
| |
| | |
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.
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| | |
Syntax is "pat ?? bexpr => action".
The whole case is selected only when "pat" matches and then "bexpr"
evaluates to "true".
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is a variant of exec_straight where it is allowed to take zero steps.
In other words, exec_straight0 is the "star" relation, while exec_straight
is the "plus" relation.
In the end we need "plus" relations in simulation diagrams, to show
the absence of stuttering. But the "star" relation exec_straight0 is
useful to reason about code fragments that are always preceded or
followed by at least one instruction.
|
| | |
|
| |
| |
| |
| | |
Should simplify reasoning over Boolean equalities.
|
| | |
|
| |
| |
| |
| | |
Just ensure sign_ext 0 x = zero. This simplifies some statements and proofs.
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
There was a misunderstanding on the asm syntax for 3-operand instructions
such as vfmadd132: when the Intel manual reads
vfmadd132 res, arg2, arg3
the corresponding GNU asm syntax is
vfmadd132 arg3, arg2, res
but not
vfmadd132 arg2, arg3, res
Closes: #188
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The "undeclared-scope" warning fires when we use a "notation" scope
before having declared it. This is a good thing, except that
the "Declare Scope" vernacular that declares a scope was introduced
in Coq 8.10 and is not available in earlier versions.
Hence there is no way to avoid triggering the warning yet remain
compatible with pre-8.10 Coq versions.
This commit silences the warning. It will have to revisited when
Coq 8.10 is the oldest version of Coq we support in CompCert.
|
| | |
|
| |
| |
| |
| |
| | |
"Hint Resolve foo." becomes "Hint Resolve foo : core", or
"Local Hint Resolve foo : core".
|
| |
| |
| |
| | |
PG now uses the _Coqproject file and finds relevant paths there.
|
| | |
|
| |
| |
| |
| | |
Unused-variables is disabled by default.
|
| |
| |
| |
| | |
Since the ppc64 has 64 bit registers it is okay to have a 64 bit
constant result.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
* 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.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
There was a misunderstanding on the asm syntax for 3-operand instructions
such as vfmadd132: when the Intel manual reads
vfmadd132 res, arg2, arg3
the corresponding GNU asm syntax is
vfmadd132 arg3, arg2, res
but not
vfmadd132 arg2, arg3, res
Closes: #188
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The "undeclared-scope" warning fires when we use a "notation" scope
before having declared it. This is a good thing, except that
the "Declare Scope" vernacular that declares a scope was introduced
in Coq 8.10 and is not available in earlier versions.
Hence there is no way to avoid triggering the warning yet remain
compatible with pre-8.10 Coq versions.
This commit silences the warning. It will have to revisited when
Coq 8.10 is the oldest version of Coq we support in CompCert.
|
| | |
|
| |
| |
| |
| |
| | |
"Hint Resolve foo." becomes "Hint Resolve foo : core", or
"Local Hint Resolve foo : core".
|
|/
|
|
| |
PG now uses the _Coqproject file and finds relevant paths there.
|
|
|
|
|
| |
It supports a branch-free implementation of floatofintu.
Not used yet in any of the ports.
|
|
|
|
|
|
|
| |
The implementation uses float <-> signed 64-bit integer conversion
instructions, and is both efficient and branchless.
Based on a suggestion by RĂ©mi Hutin.
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
| |
It is type-checked like a conditional expression then translated to
a call to the known builtin function.
|
|
|
|
| |
Known built-in functions are guaranteed not to change memory.
|
|
|
|
|
|
|
| |
When an external function is a known built-in function and it is
applied to compile-time integer or FP constants, we can use
the known semantics of the builtin to compute the result
at compile-time.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|