| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|\
| |
| |
| | |
gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
|
| |\
| | |
| | |
| | | |
mppa-work-upstream-merge
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | | | |
|
| |\| |
| | | |
| | | |
| | | | |
mppa-work-upstream-merge
|
| |\ \ \
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Conflicts:
.gitignore
backend/Lineartyping.v
common/Values.v
configure
cparser/Machine.ml
cparser/Machine.mli
driver/Configuration.ml
driver/Frontend.ml
runtime/Makefile
test/c/Makefile
test/c/aes.c
test/compression/Makefile
test/regression/Makefile
test/regression/extasm.c
test/regression/floats-basics.c
test/regression/floats.c
Note : test/regression should be checked, didn't test it yet
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
"Hint Resolve foo." becomes "Hint Resolve foo : core", or
"Local Hint Resolve foo : core".
|
|\ \ \ \ \
| | |_|_|/
| |/| | | |
|
| | |_|/
| |/| |
| | | |
| | | | |
Just moved a frequent failure case ahead of a costly "simpl".
|
| | | | |
|
| | | | |
|
| | | | |
|
|/ / / |
|
| | |
| | |
| | |
| | | |
A stronger `intuition` in the near future would break this use of `intuition`.
|
| | |
| | |
| | |
| | | |
The proposed proof only uses `zify` for closing the goal. This is
needed for Coq PR #10982 which changes the inner working of `zify`.
|
| |/
|/|
| |
| |
| |
| |
| | |
Some hints will move from the core database to the `ordered_type` database
(see https://github.com/coq/coq/pull/9772).
This commit prepares for this move by adding `with ordered_type` to the invocations
of `auto` and `eauto` that use the hints in question.
|
| |
| |
| |
| |
| | |
This commit adds a back-end for the AArch64 architecture, namely ARMv8
in 64-bit mode.
|
| | |
|
| |
| |
| |
| | |
Should simplify reasoning over Boolean equalities.
|
| | |
|
| |
| |
| |
| | |
Just ensure sign_ext 0 x = zero. This simplifies some statements and proofs.
|
| | |
|
| | |
|
|/
|
|
|
| |
"Hint Resolve foo." becomes "Hint Resolve foo : core", or
"Local Hint Resolve foo : core".
|
|
|
|
|
| |
It supports a branch-free implementation of floatofintu.
Not used yet in any of the ports.
|
|
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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 previous implementation used to build the full powers-of-two decomposition
of the number. The present implementation recognizes powers of two directly,
then takes the log2.
|