| Commit message (Collapse) | Author | Age | Files | Lines |
|
|
|
|
| |
Previous scripts were relying on the order in which apply's HO
unification performs reductions, for a goal that could be solved by
reflexivity.
|
|
|
|
|
| |
Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None`
by a call to the function Hashtbl.find_opt.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
(#353)
Within CompCert, identifiers (names of C functions, variables, types,
etc) are represented by unique positive numbers, sometimes called
"atoms".
In the original implementation, atoms 1, 2, ..., N are assigned
to identifiers as they are encountered. The resulting number
are small and are efficient when used as keys in data structures
such as PTrees. However, the mapping from C source-level identifiers
to atoms differs between compilation units. This is not a problem
for CompCert but complicates CompCert-based verification tools
that need to combine several compilation units.
This commit introduces an alternate implementation of atoms, suggested
by Andrew Appel. The choice between implementations is governed by
the Boolean reference `Camlcoq.use_canonical_atoms`.
In the alternate implementation, identifiers are converted to bit
sequences via a Huffman encoding, then the bits are represented as
positive numbers. The same identifier is always represented by the
same number. However, the numbers are usually bigger than in the
original implementation, making PTree operations slower: lookups and
updates take time linear in the length of the identifier, instead of
logarithmic time in the number of identifiers encountered.
The CompCert compiler (the `ccomp` executable) still uses the original
implementation, but the `clightgen` tool used in conjunction with the
VST program logic can use either implementations:
- The alternate "canonical atoms" implementation is used by default,
and also if the `-canonical-idents` option is given.
- The original implementation is used if the `-short-idents` option is
given.
Closes: #222
Closes: #311
|
|
|
|
|
|
| |
The Commandline module is reusable in other projects, and its license
(GPL) allows such reuse, so its natural place is in lib/ rather
than in driver/
|
|
|
|
|
| |
So as not to depend on an implicit import from module Program.
(See PR #352.)
|
|
|
|
|
|
| |
On some versions of Coq, "nil" is of type "Rlist"...
This reverts commit f070949a7559675af3e551e16e5cae95af5d4285.
|
|
|
|
|
| |
The rest of the code base uses `nil`, so let's be consistent.
Also, this avoids depending on `Import ListNotations`.
|
|
|
|
| |
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.
|
|
|
|
|
| |
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.
|
|
|
|
|
| |
Instead, use definitions and lemmas from the Coq standard library
(ZArith, Znumtheory).
|
|
|
|
|
|
|
| |
Use Z.to_nat theorems from the standard Coq library in preference to
our theorems in lib/Coqlib.v.
Simplify lib/Coqlib.v accordingly.
|
|
|
|
| |
These were committed by mistake.
|
|
|
|
|
|
|
|
| |
Rumor has it that this module is scheduled for removal.
This is based on pull request #286, with a different implementation.
Closes: #286
|
|
|
|
|
|
|
|
|
|
|
|
| |
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).
|
|
|
|
|
|
|
| |
Since the number of bits is > 0, it is guaranteed that
modulus > 1, not just that modulus > 0.
(Suggested by Jake Waksbaum @jbaum.)
|
|
|
| |
Preparation for Coq PR 9725 that may make `eauto` stronger.
|
|
|
| |
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.
|
|
|
|
|
|
|
| |
"compare" returns the 4 possible results w/ type "option comparison".
"ordered" returns a Boolean.
These functions will be used soon in the x86 port.
|
|
|
|
|
|
|
|
|
| |
This is required for compatibility with
https://github.com/coq/coq/pull/8064, where prim token notations no longer
follow `Require`, but instead follow `Import`.
Closes #246
Closes #250
|
|
|
|
|
|
| |
Fix various typos in diagnostic messages and unified wording and
capitalization.
Bug 23850
|
|
|
|
|
|
|
|
|
| |
OCaml 4.07 introduces a Float submodule of the Stdlib
opened-by-default compilation unit. CompCert's Float compilation unit
also has a Float submodule. This triggers warning 44 when Floats is
opened. The workaround is just to silence the warning with `open! Floats`.
Closes: #241
|
|
|
|
|
| |
The lemma Zquot_1_r is replaced by Z.quot_1_r in coq version > 8.3.
Fix 23199
|
|
|
|
|
|
|
|
|
|
|
| |
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/
|
| |
|
| |
|
|
|
|
|
| |
The common json export functionallity is moved into an own File.
Bug 22472
|
|\
| |
| |
| | |
Ensure FunInd or Recdef is imported if functional induction is used.
This is necessary for Coq 8.7.0.
|
| |
| |
| |
| |
| |
| | |
Coq 8.7 does not load FunInd in prelude anymore, so this is necessary.
Recdef exports FunInd, so if Recdef is imported, importing FunInd
is not required.
|
| |
| |
| |
| | |
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
|
|/ |
|
|
|
|
|
|
|
|
|
| |
Instead of just dumping the json output it is now a little bit
formatted for better reading.
Furthermore the AsmToJson function for the non powerpc targets now
prints the json value "null" sucht that the resulting json file is
valid json.
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
This commit adds code generation for 64bit PowerPC architectures which execute
32bit applications.
The main difference to the normal 32bit PowerPC port is that it uses the
available 64bit instructions instead of using the runtime library functions.
However pointers are still 32bit and the 32bit calling convention is used.
In order to use this port the target architecture must be either in Server
execution mode or if in Embedded execution mode the high order 32 bits of GPRs
must be implemented in 32-bit mode. Furthermore the operating system must
preserve the high order 32 bits of GPRs.
|