aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Collapse)AuthorAgeFilesLines
* Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-213-33/+36
| | | | | | | This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`.
* Define `fold_ind_aux` and `fold_ind` transparentlyXavier Leroy2021-01-211-2/+2
| | | | | | The extraction mechanism wants to extract them (because they are in Type, probably). The current opaque definition causes a warning at extraction-time.
* Add new fold_ind induction principle for foldsXavier Leroy2021-01-131-63/+82
| | | | | | | fold_inv is in Type, hence can prove goals such as `{ x | P x }`. Also, no extensionality property is needed. fold_rec is now derived from fold_inv.
* Add lemma list_norepet_revXavier Leroy2021-01-131-0/+8
|
* Replace `omega` tactic with `lia`Xavier Leroy2020-12-2914-1026/+1022
| | | | | | | | | | | Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
* Remove useless parameters in theorems int_round_odd_bits and int_round_odd_leXavier Leroy2020-12-292-13/+13
| | | | | | | | | IEEE754_extra: clear unused context so that none of the context is picked up by tactics and ends as extra parameters to theorems int_round_odd_bits and int_round_odd_le Floats: simplify uses of int_round_odd_bits and int_round_odd_le accordingly.
* Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-212-4/+3
| | | | configure flags -use-external-Flocq and -use external-MenhirLib.
* Simplify two scripts in Zbits (#369)Maxime Dénès2020-09-181-2/+2
| | | | | Previous scripts were relying on the order in which apply's HO unification performs reductions, for a goal that could be solved by reflexivity.
* Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
| | | | | Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt.
* Add a canonical encoding of identifiers as numbers and use it in clightgen ↵Xavier Leroy2020-05-191-3/+76
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | (#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
* Move Commandline to the lib/ directoryXavier Leroy2020-05-052-0/+196
| | | | | | 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/
* Import ListNotations explicitlyXavier Leroy2020-05-041-0/+1
| | | | | So as not to depend on an implicit import from module Program. (See PR #352.)
* Revert "Do not use the list notation `[]`"Xavier Leroy2020-05-041-8/+8
| | | | | | On some versions of Coq, "nil" is of type "Rlist"... This reverts commit f070949a7559675af3e551e16e5cae95af5d4285.
* Do not use the list notation `[]`Xavier Leroy2020-05-041-8/+8
| | | | | The rest of the code base uses `nil`, so let's be consistent. Also, this avoids depending on `Import ListNotations`.
* Reduce the checking time for the "decidable_equality_from" tacticxavier.leroy2020-01-301-4/+5
| | | | Just moved a frequent failure case ahead of a costly "simpl".
* Use `intuition idtac` instead of `intuition` (#321)Vincent Laporte2019-11-121-1/+1
| | | | A stronger `intuition` in the near future would break this use of `intuition`.
* More robust proof of `size_and` (#320)Frédéric Besson2019-10-301-4/+5
| | | | The proposed proof only uses `zify` for closing the goal. This is needed for Coq PR #10982 which changes the inner working of `zify`.
* Make explicit the use of hints from OrderedType (#316)Vincent Laporte2019-10-022-7/+9
| | | | | | | 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.
* AArch64 portXavier Leroy2019-08-081-24/+136
| | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* More lemmas about powers of 2Xavier Leroy2019-08-071-0/+14
|
* Added Int.same_if_eqXavier Leroy2019-08-071-0/+5
| | | | Should simplify reasoning over Boolean equalities.
* Properties of combinations of shifts and zero-/sign-extensionXavier Leroy2019-08-071-0/+249
|
* Define integer sign extension for zero bitsXavier Leroy2019-08-072-42/+57
| | | | Just ensure sign_ext 0 x = zero. This simplifies some statements and proofs.
* Zbits.v: add bit extraction and bit insertionXavier Leroy2019-08-071-0/+57
|
* Coq 8.10 compatibility: tweak Argument commandXavier Leroy2019-08-071-1/+1
|
* Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-071-2/+2
| | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core".
* Another way to derive floatofintu from floatofintXavier Leroy2019-07-171-0/+41
| | | | | It supports a branch-free implementation of floatofintu. Not used yet in any of the ports.
* Add floating-point square root and fused multiply-addXavier Leroy2019-07-171-3/+51
| | | | | | | | 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.
* Revised specification of NaN payload behaviorXavier Leroy2019-07-121-124/+104
| | | | | | | | | | | | | | 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.
* New parser based on new version of the Coq backend of Menhir (#276)Jacques-Henri Jourdan2019-07-051-51/+0
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Avoid relying on `Export` bug (#301)Maxime Dénès2019-07-041-1/+2
| | | | The previous code was unintentionally relying on a strange behavior of `Export` (see https://github.com/coq/coq/issues/10480) that will be removed.
* More efficient test for powers of twoXavier Leroy2019-05-092-26/+105
| | | | | | 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.
* Rename Fappli_IEEE_extra.v into IEEE754_extra.vXavier Leroy2019-04-262-1/+1
| | | | | To match the new module names from version 3 of Flocq. Plus, it's shorter.
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-263-839/+981
| | | | | | | | | | 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.
* lib/Coqlib.v: remove defns about multiplication, division, modulusXavier Leroy2019-04-233-101/+17
| | | | | Instead, use definitions and lemmas from the Coq standard library (ZArith, Znumtheory).
* Replace nat_of_Z with Z.to_natXavier Leroy2019-04-231-30/+7
| | | | | | | Use Z.to_nat theorems from the standard Coq library in preference to our theorems in lib/Coqlib.v. Simplify lib/Coqlib.v accordingly.
* Floats.v: remove leftover Print commandsXavier Leroy2019-04-041-5/+1
| | | | These were committed by mistake.
* Floats.v: avoid using module Zlogarithm in the proofsXavier Leroy2019-04-031-10/+19
| | | | | | | | Rumor has it that this module is scheduled for removal. This is based on pull request #286, with a different implementation. Closes: #286
* Upgrade embedded version of Flocq to 3.1.Guillaume Melquiond2019-03-272-366/+371
| | | | | | | | | | | | 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).
* Integers.v: add modulus_gt_one (#259)Xavier Leroy2019-03-251-1/+7
| | | | | | | Since the number of bits is > 0, it is guaranteed that modulus > 1, not just that modulus > 0. (Suggested by Jake Waksbaum @jbaum.)
* Minor simplifications in two proofs. (#280)Vincent Laporte2019-03-251-1/+1
| | | Preparation for Coq PR 9725 that may make `eauto` stronger.
* Make the checker happy (#272)Vincent Laporte2019-02-121-8/+8
| | | 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.
* Add functions "ordered" and "compare" to Float and Float32Xavier Leroy2018-12-201-9/+20
| | | | | | | "compare" returns the 4 possible results w/ type "option comparison". "ordered" returns a Boolean. These functions will be used soon in the x86 port.
* Import prim token notations before using themJason Gross2018-08-271-0/+1
| | | | | | | | | 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
* Various improvements in the wording of diagnostics.Michael Schmidt2018-08-021-3/+3
| | | | | | Fix various typos in diagnostic messages and unified wording and capitalization. Bug 23850
* Compatibility with OCaml 4.07 (#241)Xavier Leroy2018-07-101-1/+1
| | | | | | | | | 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
* Removed deprecated lemma.Bernhard Schommer2018-03-121-1/+1
| | | | | The lemma Zquot_1_r is replaced by Z.quot_1_r in coq version > 8.3. Fix 23199
* Resynchronize the LICENSE file and the license headers in individual files (#45)Xavier Leroy2018-01-056-251/+15
| | | | | | | | | | | 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/
* Test for inline. Bug 22642Bernhard Schommer2017-12-081-1/+1
|
* Added simple div_one Theorem variants.Bernhard Schommer2017-12-011-0/+6
|
generated by cgit (git 2.34.1) at 2024-06-26 18:45:10 +0000