aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Collapse)AuthorAgeFilesLines
* 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
|
* New json printing interface.Bernhard Schommer2017-11-143-1/+190
| | | | | The common json export functionallity is moved into an own File. Bug 22472
* Merge pull request #191 from sigurdschneider/masterXavier Leroy2017-10-203-2/+3
|\ | | | | | | Ensure FunInd or Recdef is imported if functional induction is used. This is necessary for Coq 8.7.0.
| * Ensure FunInd or Recdef is imported if functional induction is usedSigurd Schneider2017-07-203-2/+3
| | | | | | | | | | | | 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.
* | Remove coq warnings (#28)Bernhard Schommer2017-09-2211-182/+182
| | | | | | | | Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
* | Some lemmas.Bernhard Schommer2017-09-211-0/+14
|/
* Formatted json printing.Bernhard Schommer2017-06-281-22/+32
| | | | | | | | | 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.
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-035-70/+230
| | | | | | | | | | | | | 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.
* RISC-V port and assorted changesXavier Leroy2017-04-282-3/+25
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes. The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/ This port required the following additional changes: - Integers: More properties about shrx - SelectOp: now provides smart constructors for mulhs and mulhu - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu. - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library. - test/: add SIMU make variable to run tests through a simulator - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers commit da14495c01cf4f66a928c2feff5c53f09bde837f Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Thu Apr 13 17:36:10 2017 +0200 RISC-V port, continued Now working on Asmgen. commit 36f36eb3a5abfbb8805960443d087b6a83e86005 Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Wed Apr 12 17:26:39 2017 +0200 RISC-V port, first steps This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.
* Adapt proofs to future handling of literal constants in Coq.Guillaume Melquiond2017-03-081-5/+2
| | | | | | This commit is mainly a squash of the relevant compatibility commits from Flocq's master. Most of the changes are meant to make the proofs oblivious to the way constants such as 0, 1, 2, and -1 are represented.
* Replace "Implicit Arguments" with "Arguments"Xavier Leroy2017-02-132-6/+4
| | | | | This silences a warning of Coq 8.6. Some "Implicit Arguments" remain in flocq/ but I'd rather not diverge from the released version of flocq if at all possible.
* Use "Local" as prefixXavier Leroy2017-02-131-1/+1
| | | | | Open Local becomes Local Open. This silences Coq 8.6's warning. Also: remove one useless Require-inside-a-module that caused another warning.
* Replace 'decide equality' in x86/Op.v by custom tactics from lib/BoolEqual.vXavier Leroy2016-12-261-0/+167
| | | | | | | | 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
* C2C: revise typing and translation of __builtin_memcpy_alignedXavier Leroy2016-11-171-0/+6
| | | | | | | | | | | | | | | | | | | | This fixes two issues: 1- The 'size' and 'alignment' arguments of __builtin_memcpy_aligned were declared with type 'unsigned int', which is not good for a 64-bit platform. 2- The corresponding arguments were not cast to type 'unsigned int', causing compilation errors if e.g. the size argument is a 64-bit integer. (Reported by Michael Schmidt.) The fix: 1- Evaluate the 3rd and 4th arguments at type size_t 2- Support both Vint and Vlong as results of this evaluation 3- Declare these arguments with type 'unsigned long'. Supporting work: in lib/Camlcoq.ml, add Z.modulo and Z.is_power2 operations. Concerning part 3 of the fix, type size_t would be better for future platforms where size_t is bigger than unsigned long, but some more work is needed to delay the evaluation of C2C.builtins_generic to after Cutil.size_t_ikind() is stable, or, equivalently, to evaluate the cparser/ machine configuration before C2C initializes.
* Finish the proofs of SelectLong for IA32Xavier Leroy2016-10-021-1/+108
|
* Improve code generation for 64-bit signed integer divisionXavier Leroy2016-10-021-0/+37
| | | | | | Implement the 'shift right extended' trick, both in the generic implementation (backend/SplitLong) and in the IA32 port. Note that now SelectDiv depends on SelectLong, and that some work was moved from SelectLong to SelectDiv.
* Support for 64-bit architectures: generic supportXavier Leroy2016-10-011-3/+454
| | | | | | | | | | | - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly.
* IA32: model integer division and modulus closer to the machineXavier Leroy2016-09-181-0/+92
| | | | | | | | lib/Integers.v: define division-remainder of a double word by a word ia32/Asm.v: use it to give Pdiv and Pidiv their "true" semantics like in the processor; add Pcltd as an instruction ia32/*: adapt accordingly Additional benefit: Pcltd could be used for an alternate implementation of shrximm.
* Enrich Decidableplus and use it to simplify Cexec.do_ef_memcpyXavier Leroy2016-09-171-0/+28
| | | | Inline directives in extraction.v make the Caml output efficient and almost nice.
* Decidableplus: remove stuff that was cut-and-paste from Coq 8.5 libraryXavier Leroy2016-09-171-48/+1
| | | | The cut-and-paste was for compatibility with Coq 8.4
* Removed some implict arguments.Bernhard Schommer2016-09-051-5/+3
| | | | Also changed Local Open to Open Local.
* Moved quoting functions in ResponsefileBernhard Schommer2016-08-162-2/+36
| | | | | | Also corrected some typos and corrected exception handling for expandargv. Bug 18308
* Added simplified reader and printer for gnu @filesBernhard Schommer2016-07-203-134/+98
| | | | | | | | The functions expandargv and writeargv resemble the functions from the libiberity that are used by the gnu tools. Additionaly a new configuration is added in order to determine which kind of response files are supported for calls to other tools. Bug 18308
* Added heuristic for passing arg via responsefiles.Bernhard Schommer2016-07-122-20/+0
| | | | | | | Since gnu make and other tools under windows seem to have a limit of around 8000 bytes per command line the arguments should be passed via responsefiles instead. Bug 18308
* Really added the function. Bug 18308Bernhard Schommer2016-07-112-3/+19
|
* Added function to write responsefiles.Bernhard Schommer2016-07-111-0/+24
| | | | | | The arguments are written in the responsefile separated by whitespace. If the argument itself contains a whitespace it is quoted. Bug 18308
* Merge branch 'master' into add-fileBernhard Schommer2016-07-1110-173/+156
|\
| * Port to Coq 8.5pl2Xavier Leroy2016-07-0810-173/+156
| | | | | | | | | | Manual merging of branch jhjourdan:coq8.5. No other change un functionality.
generated by cgit (git 2.34.1) at 2024-06-26 18:38:27 +0000