| Commit message (Collapse) | Author | Age | Files | Lines |
... | |
| | |
|
| |
| |
| |
| | |
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.
|
|
|
|
|
| |
Cherry-pick of the following commit on upstream Flocq:
https://gitlab.inria.fr/flocq/flocq/commit/28cc6ee3a278878f3df002aab64a6b93e9412d34
|
|
|
|
|
|
|
|
| |
The clightgen tracing options did not result in printing of the
intermediate files, but were ignored.
Added also two new options, `-dprepro` to print the preprocessed
file and `-dall` to dump all intermediate files.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
|
|
|
|
| |
The warning should only be active if the optimization is active,
so the check is only performed when the warning is active and
additionally the command line flag -Obranchless is specified.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
* Do not use `Pervasives.xxx` qualified names
Starting with OCaml 4.08, `Pervasives` is deprecated in favor of `Stdlib`,
and uses of `Pervasives` cause fatal warnings.
This commit uses unqualified names instead, as no ambiguity occurs.
* Clarify "open" statements
OCaml 4.08.0 has stricter warnings concerning open statements that
shadow module names.
Closes: #300
|
|
|
|
|
|
|
| |
Commit 1df887f breaks compilation on some Windows environments,
those where the output of `menhir --suggest-menhirLib` contains `\r\n` end-of-lines
or backslashes in paths. The fix is to filter the output.
Closes: #304 Changes in configure broke Windows build
|
|
|
|
|
|
| |
The generation of some fresh names changes in Coq 8.10 (https://github.com/coq/coq/pull/9160).
The `Hint Mode` declaration that does not specify a hint database now triggers a warning.
Specify the intended database and fix the "auto" tactics accordingly.
|
| |
|
|
|
|
| |
Updated man page + better usage message.
|
|
|
|
|
| |
Easier to type, and consistent with `-Os` (optimize for smaller code /
optimize for fewer conditional branches).
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
What's new:
1. A rewrite of the Coq interpreter of Menhir automaton, with
dependent types removing the need for runtime checks for the
well-formedness of the LR stack. This seem to cause some speedup on
the parsing time (~10% for lexing + parsing).
2. Thanks to 1., it is now possible to avoid the use of int31 for
comparing symbols: Since this is only used for validation,
positives are enough.
3. Speedup of Validation: on my machine, the time needed for compiling
Parser.v goes from about 2 minutes to about 1 minute. This seem to
be related to a performance bug in the completeness validator and
to the use of positive instead of int31.
3. Menhir now generates a dedicated inductive type for
(semantic-value-carrying) tokens (in addition to the already
existing inductive type for (non-semantic-value-carrying)
terminals. The end result is that the OCaml support code for the
parser no longer contain calls to Obj.magic. The bad side of this
change is that the formal specification of the parser is perhaps
harder to read.
4. The parser and its library are now free of axioms (I used to use
axiom K and proof irrelevance for easing proofs involving dependent
types).
5. Use of a dedicated custom negative coinductive type for the input
stream of tokens, instead of Coq stdlib's `Stream`. `Stream` is a
positive coinductive type, which are now deprecated by Coq.
6. The fuel of the parser is now specified using its logarithm instead
of its actual value. This makes it possible to give large fuel
values instead of using the `let rec fuel = S fuel` hack.
7. Some refactoring in the lexer, the parser and the Cabs syntax tree.
The corresponding changes in Menhir have been released as part of
version 20190626. The `MenhirLib` directory is identical to the
content of the `src` directory of the corresponding `coq-menhirlib`
opam package except that:
- In order to try to make CompCert compatible with several Menhir
versions without updates, we do not check the version of menhir
is compatible with the version of coq-menhirlib. Hence the
`Version.v` file is not present in CompCert's copy.
- Build-system related files have been removed.
|
|
|
|
| |
The previous code was unintentionally relying on a strange behavior of `Export` (see https://github.com/coq/coq/issues/10480) that will be removed.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
The new diagnostics is triggered if a conditional is used that
may not be transformed into linear code by the later by the
if conversion.
The new diagnostic is emitted if a conditional may contain an
unsafe expression or is contained within another conditional,
logical and or logical or expression. An expression is unsafe if
it contains a call, changes memory or if its evaluation leads to
undefined behavior, for example division and modulo.
Also fixes a small typo in a comment in Cutil.
|
|
|
|
|
| |
The function determines whether the given type is an array type
or not.
|
|
|
|
|
|
| |
Refactored the checks functions by using higher order traversal
functions for statements. Also introduce helper functions for the
traversal of initializers.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|