| Commit message (Collapse) | Author | Age | Files | Lines |
|\ |
|
| | |
|
|\ \
| |/
|/|
| | |
mppa-non-trapping-load
|
|\|
| |
| |
| | |
mppa-work-upstream-merge
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
|\|
| |
| |
| | |
mppa-work-upstream-merge
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| |
| | |
This module is similar to RTLtyping: it performs type inference and
type checking, but on the Cminor intermediate representation rather
than the RTL IR. For each function, it returns a mapping from variables
to types. Its first use will be if-conversion optimization.
|
|\ \
| | |
| | |
| | | |
mppa-if-conversion
|
| |/
| |
| |
| |
| |
| |
| | |
This module is similar to RTLtyping: it performs type inference and
type checking, but on the Cminor intermediate representation rather
than the RTL IR. For each function, it returns a mapping from variables
to types. Its first use will be if-conversion optimization.
|
| |
| |
| |
| |
| |
| |
| |
| | |
Following the gnu Makefile Conventions the variable $(DESTDIR)
should be prepended to all installation commands. This allows
staged installs.
|
| |
| |
| |
| |
| | |
To match the new module names from version 3 of Flocq.
Plus, it's shorter.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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).
|
| | |
|
|\|
| |
| |
| |
| |
| | |
Conflicts:
.gitignore
runtime/include/stdbool.h
|
| |
| |
| |
| | |
This file is created by Coq when running some tactics
|
| |
| |
| | |
Previously, the coqchk type- and proof-checker would take forever on some of CompCert's modules. This commit makes minimal changes to the problematic proofs so that all of CompCert can be checked with coqchk. Tested with Coq versions 8.8.2 and 8.9.0.
|
| | |
|
| | |
|
| | |
|
| | |
|
|\|
| |
| |
| |
| | |
Conflicts:
.gitignore
|
| |
| |
| |
| |
| |
| |
| | |
For consistency with other generated .v files, and because it protects
against editing the generated file, see Github issue #248.
Closes: #248
|
| |
| |
| |
| | |
Inspired by and adapted from pull request #235 by Benoît Viguier.
|
| | |
|
| |
| |
| |
| |
| | |
coq2html is now a standalone project (https://github.com/xavierleroy/coq2html)
packaged as coq-coq2html in OPAM-Coq.
|
| |
| |
| | |
This is useful for the VST project and can be useful for others.
|
| |
| |
| |
| |
| |
| |
| |
| |
| | |
.vo files are installed if configure options
-install-coqdev or -clightgen or -coqdevdir are given.
Installation directory is $(PREFIX)/lib/compcert/coq by default and
can be changed by configure option -coqdevdir.
Closes: #227
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We were previously at 2.5.2. Quoting the NEWS from upstream:
Version 2.6.1:
- ensured compatibility from Coq 8.4 to 8.8
Version 2.6.0:
- ensured compatibility from Coq 8.4 to 8.7
- removed some hypotheses on some lemmas of Fcore_ulp
- added lemmas to Fprop_plus_error
- improved examples
Also: in preparation for Coq 8.8, silence warning "compatibility-notation"
when building Flocq, because this warning is on by default in 8.8,
and Flocq triggers it a lot.
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Asmblock.v:
- Rajout de "header" dans wf_bblock
- Remplacer "code" par "bblocks". Pour la suite, je trouve plus clair
de manipuler des bblocks, plutôt qu'un "code constitué de bblocks".
ça permet de minimiser les modifications dans Asmblockgen.v
- fn_code --> fn_blocks . fn_code ne devrait pas être utilisé dans le
code OCaml de toute façon (vu la translation Asmblock -> Asm)
- Rajout d'un type instruction qui regroupe les basic et les control ;
facilite certaines définitions
Asmblockgen.v:
- Copie conforme de Asmgen.v, avec quelques changements (pas fini). Ce
vers quoi je m'oriente : garder les fonctions existantes de
génération de code ; on leur donne à manger la liste de basics de
Machblock. On traduit le exit (qui peut spiller sur la liste de
basics déjà traduite), et on met la dernière instruction de la trad
du exit (qui doit être un control) dans le exit du bblock.
- Pour le prologue : chaque instruction rajoutée "à la main" est dans
son propre bblock. Voir la notation ::b pour le faire. A terme, il
devrait y avoir moyen "d'accumuler" l'instruction au code généré ;
pour l'instant je préfère ne pas compliquer la génération.
|
|/ |
|
|
|
|
|
|
|
| |
Implicit Arguments is deprecated in Coq since 8.6 or so.
Some Implicit Arguments remained in Flocq but were recently changed to Arguments.
Apply the same change to our local copy of Flocq.
As a positive consequence, we no longer need to suppress the deprecation warnings while compiling Flocq.
|
| |
|
|
|
|
| |
We simply fully qualify the modules. This is backward compatible.
|
|
|
|
|
| |
The latter, in conjunction with some values of the umask, gives weird messages
"new permissions are ... not ...".
|
|
|
|
| |
`-admit Floats` is no longer needed, but Integers and SelectDivproof still need admitting.
|
|
|
|
| |
Perhaps for reasons of backward compatibility with Coq 8.4, Flocq 2.5.2 still uses the "Implicit Arguments foo" idiom, which is deprecated in Coq 8.6.
|
| |
|
|
|
|
|
|
|
|
| |
Applied to the 92-constructor 'operation' type, 'decide equality' produces a huge transparent term that causes the VM compiler to generate huge code and exceeed a memory limit of Coq on 32-bit platforms. (The limit is OCaml's, really.)
The lib/BoolEqual.v file defines alternative tactics to build decidable equalities where the transparent part of the definition is smaller (O(N^2) instead of O(N^3)). The proof parts are still huge (O(N^3)) but they are opaque.
Fixes #151
|
|\
| |
| |
| | |
Support for 64-bit target processors + support for x86 in 64-bit mode
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
-> x86/x86_32/x86_64
Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq.
This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86.
While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures.
Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
|