aboutsummaryrefslogtreecommitdiffstats
path: root/lib
Commit message (Collapse)AuthorAgeFilesLines
* centralize if_sameDavid Monniaux2020-10-091-0/+6
|
* Adding copyrightsCyril SIX2020-05-044-0/+48
|
* moved to extraDavid Monniaux2020-04-161-0/+0
|
* gmap2_idemDavid Monniaux2020-04-161-65/+111
|
* gmap2_idemDavid Monniaux2020-04-161-0/+16
|
* gmap2_idem_EmptyDavid Monniaux2020-04-161-0/+54
|
* begin HashedMapsDavid Monniaux2020-04-161-0/+332
|
* forward_move_lDavid Monniaux2020-03-101-1/+13
|
* kill_reg_soundDavid Monniaux2020-03-091-1/+1
|
* CSE3 generate lists of killableDavid Monniaux2020-03-051-0/+4
|
* more about extraction and linkingDavid Monniaux2020-03-051-185/+180
|
* streamlined lattice codeDavid Monniaux2020-03-052-30/+15
|
* HashedSet with extractionDavid Monniaux2020-03-051-0/+6
|
* HashedSet with module typesDavid Monniaux2020-03-051-0/+115
|
* move lattice stuff where it belongsDavid Monniaux2020-03-054-0/+1446
|
* Merge branch 'mppa-cse2' of ↵David Monniaux2020-03-033-96/+317
|\ | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work
| * Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2020-02-081-4/+5
| |\ | | | | | | | | | mppa-work-upstream-merge
| * \ Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-1/+178
| |\ \
| | * | shrx'1_shr'David Monniaux2020-01-141-1/+127
| | | |
| | * | shrx1_shrDavid Monniaux2020-01-141-0/+51
| | | |
| * | | set_disjointDavid Monniaux2019-12-131-0/+49
| | | |
| * | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-11-134-12/+15
| |\| | | | | | | | | | | | | | mppa-work-upstream-merge
| * | | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-162-65/+517
| |\ \ \ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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
| * | | | IcondCyril SIX2019-10-071-0/+5
| | | | |
| * | | | Ibuiltin proofCyril SIX2019-10-042-12/+89
| | | | |
| * | | | Adding decidable equality for intCyril SIX2019-10-041-1/+12
| | | | |
| * | | | Coq 8.10 compatibility: tweak Argument commandXavier Leroy2019-08-051-1/+1
| | | | |
| * | | | Coq 8.10 compatibility: make explicit the "core" hint databaseXavier Leroy2019-08-051-2/+2
| | | | | | | | | | | | | | | | | | | | | | | | | "Hint Resolve foo." becomes "Hint Resolve foo : core", or "Local Hint Resolve foo : core".
* | | | | Merge branch 'master' of https://github.com/AbsInt/CompCert into dm-cse2David Monniaux2020-02-271-4/+5
|\ \ \ \ \ | | |_|_|/ | |/| | |
| * | | | 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".
* | | | progress on wellformed regDavid Monniaux2020-02-051-1/+120
| | | |
* | | | gremove_tDavid Monniaux2020-02-041-0/+36
| | | |
* | | | gcombine_nullDavid Monniaux2020-02-041-0/+13
| | | |
* | | | gcombine_nullDavid Monniaux2020-02-041-1/+39
|/ / /
* | | 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.
generated by cgit (git 2.34.1) at 2024-07-02 10:07:00 +0000