Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | itemize the proof (better for debugging) | David Monniaux | 2019-04-05 | 1 | -10/+10 |
| | |||||
* | preparing for the builtin connector | David Monniaux | 2019-04-05 | 1 | -3/+69 |
| | |||||
* | removed the unproved hack to get builtins, will be reinstated later | David Monniaux | 2019-04-05 | 2 | -72/+6 |
| | |||||
* | Oselectf, Oselectfs with condition | David Monniaux | 2019-04-05 | 1 | -8/+2 |
| | |||||
* | selectl with condition | David Monniaux | 2019-04-05 | 1 | -4/+1 |
| | |||||
* | more on select | David Monniaux | 2019-04-04 | 1 | -4/+1 |
| | |||||
* | select_sound | David Monniaux | 2019-04-04 | 1 | -1/+1 |
| | |||||
* | ternary ops for float/double | David Monniaux | 2019-04-03 | 1 | -2/+34 |
| | |||||
* | problem in ValueAOp | David Monniaux | 2019-04-03 | 1 | -1/+17 |
| | |||||
* | begin implementing ternary builtin | David Monniaux | 2019-04-03 | 1 | -4/+13 |
| | |||||
* | selection of builtin.. progress... | David Monniaux | 2019-04-03 | 1 | -13/+14 |
| | |||||
* | some more on builtins | David Monniaux | 2019-04-03 | 2 | -3/+20 |
| | |||||
* | attempts at generating builtins, start | David Monniaux | 2019-04-03 | 1 | -3/+6 |
| | |||||
* | ça recompile sur x86 | David Monniaux | 2019-03-22 | 8 | -3/+127 |
| | |||||
* | Merge branch 'mppa_postpass' into mppa-mul | David Monniaux | 2019-03-22 | 3 | -8/+4 |
|\ | |||||
| * | try to be portable across archs | David Monniaux | 2019-03-21 | 3 | -8/+4 |
| | | |||||
* | | Merge branch 'mppa_postpass' into mppa-mul | David Monniaux | 2019-03-20 | 1 | -7/+6 |
|\| | |||||
| * | XLeroy's suggested fix for shared float/int register file. | David Monniaux | 2019-03-20 | 1 | -3/+3 |
| | | |||||
| * | Revert "Better fix for register allocation?" | David Monniaux | 2019-03-20 | 1 | -4/+3 |
| | | | | | | | | This reverts commit 5ad25465f77c3009eaff7e9a124c254c1e9f33cd. | ||||
* | | Proof of div32/mod32/divf32/divf64 lemmas | Cyril SIX | 2019-03-20 | 1 | -3/+3 |
| | | |||||
* | | la division flottante fonctionne | David Monniaux | 2019-03-20 | 3 | -9/+12 |
| | | |||||
* | | begin float division | David Monniaux | 2019-03-20 | 1 | -3/+3 |
| | | |||||
* | | Proving eval_divs_base | Cyril SIX | 2019-03-20 | 2 | -2/+2 |
| | | |||||
* | | added helper functions but strange | David Monniaux | 2019-03-19 | 4 | -89/+10 |
|/ | | | | idiv.c: error: __compcert_i32_sdiv: missing or incorrect declaration | ||||
* | Merge branch 'master' into mppa_postpass | Cyril SIX | 2019-03-13 | 1 | -6/+8 |
|\ | | | | | | | | | | | Conflicts: .gitignore runtime/include/stdbool.h | ||||
| * | Make the checker happy (#272) | Vincent Laporte | 2019-02-12 | 1 | -6/+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. | ||||
* | | Réactivé l'optim mulhs pour 32-bits (Omulhs n'est jamais généré) | Cyril SIX | 2019-02-08 | 2 | -16/+16 |
| | | |||||
* | | Désactivé toutes les optim division par constante --> Omulhs etc.. | Cyril SIX | 2019-02-08 | 2 | -26/+26 |
| | | |||||
* | | Desactivated Omulhs 32-bits optimization (division by constant) | Cyril SIX | 2019-02-08 | 2 | -8/+8 |
| | | |||||
* | | Better fix for register allocation? | Cyril SIX | 2019-02-06 | 1 | -3/+4 |
| | | |||||
* | | compilation Asmexpandaux both for x86/ and mppa_k1c/ | Sylvain Boulmé | 2018-11-28 | 2 | -0/+9 |
| | | |||||
* | | Compiles for x86 and mppa_k1c (except Asmexpandaux.ml) | Sylvain Boulmé | 2018-11-27 | 2 | -9/+10 |
| | | |||||
* | | BROKEN - works for x86, not for k1 anymore | Cyril SIX | 2018-11-26 | 4 | -16/+7 |
| | | |||||
* | | Merge tag 'v3.4' into mppa_k1c | Cyril SIX | 2018-11-21 | 12 | -90/+245 |
|\| | | | | | | | | | Conflicts: .gitignore | ||||
| * | Simplified code. Bug 24067 | Bernhard Schommer | 2018-09-12 | 1 | -8/+8 |
| | | |||||
| * | Generate a nop instruction after some ais annotations (#137) | Bernhard Schommer | 2018-09-12 | 2 | -3/+35 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Generate a nop instruction after ais annotations. In order to prevent the merging of ais annotations with following Labels a nop instruction is inserted, but only if the annotation is followed immediately by a label. The insertion of nop instructions is performed during the expansion of builtin and pseudo assembler instructions and is processor independent, by inserting a __builtin_nop built-in. * Add Pnop instruction to ARM, RISC-V, and x86 ARM as well as RISC-V don't have nop instructions that can be easily encoded by for example add with zero instructions. For x86 we used to use `mov X0, X0` for nop but this may not be as efficient as the true nop instruction. * Implement __builtin_nop on all supported target architectures. This builtin is not yet made available on the C side for all architectures. Bug 24067 | ||||
| * | Various improvements in the wording of diagnostics. | Michael Schmidt | 2018-08-02 | 1 | -4/+4 |
| | | | | | | | | | | | | Fix various typos in diagnostic messages and unified wording and capitalization. Bug 23850 | ||||
| * | Treat Outgoing stack slots as caller-save in LTL/Linear semantics (#237) | Xavier Leroy | 2018-06-17 | 6 | -93/+145 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Outgoing stack slots are set to Vundef on return from a function call, modeling the fact that the callee could write into those stack slots. (CompCert-generated code does not do this, but code generated by other compilers sometimes does.) * Adapt Stackingproof to this new semantics. This requires tighter reasoning on how Linear's locsets are related at call points and at return points. * Most of this reasoning was moved from Stackingproof to Lineartyping, because it can be expressed purely in terms of the Linear semantics, and tracked through the wt_state predicate. * Factor out and into Conventions.v: the notion of callee-save locations, the "agree_callee_save" predicate, and useful lemmas on Locmap.setpair. Now the same "agree_callee_save" predicate is used in Allocproof and in Stackingproof. | ||||
| * | Model external calls as destroying all caller-save registers | Xavier Leroy | 2018-06-01 | 8 | -8/+79 |
| | | | | | | | | | | | | | | | | | | | | The semantics of external function calls in LTL, Linear, Mach and Asm now consider that all caller-save registers are set to Vundef by the call. This models that fact that the external function can modify those registers arbitrarily. Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes accordingly. | ||||
* | | Extraction issue | Cyril SIX | 2018-09-06 | 1 | -7/+9 |
| | | |||||
* | | MPPA - refactored instructions | Cyril SIX | 2018-05-11 | 2 | -7/+7 |
| | | |||||
* | | MPPA - Started Asm.v + Asmgen.v, commenting out some instructions | Cyril SIX | 2018-04-04 | 1 | -1/+3 |
| | | |||||
* | | MPPA - Machregs + Conventions1 + backend proof tweaking | Cyril SIX | 2018-04-04 | 2 | -2/+7 |
|/ | |||||
* | Add newline directly on list in annot. | Bernhard Schommer | 2018-03-13 | 2 | -4/+7 |
| | | | | | | | This should avoid cluttering the assembler output with .ascii "\n" lines if the annotation ends with a string and make for a better readability. Bug 23169 | ||||
* | Print size argument of Init_space as Z not as int32 | Xavier Leroy | 2018-03-13 | 1 | -1/+1 |
| | | | | | Init_space has an argument of type Z and it can exceed the range of a 32-bit integer. Reported by Frédéric Besson. | ||||
* | Introduce more brackets for register annotation. | Bernhard Schommer | 2018-03-12 | 1 | -4/+5 |
| | | | | | | It seems necessary that the mulitplication for the high part of split registers is put into brackets. Bug 23169 | ||||
* | Do not use "Require" inside sections (#224) | Xavier Leroy | 2018-03-12 | 1 | -3/+1 |
| | | | | | | This will soon be deprecated by Coq. Manual merge of pull request #224 by vbgl. Closes: #224 | ||||
* | Added seperator in warning msg. Bug 23179 | Bernhard Schommer | 2018-03-09 | 1 | -1/+1 |
| | |||||
* | Do not use default printer for variable names. | Bernhard Schommer | 2018-03-09 | 1 | -2/+8 |
| | | | | | | Printing variable names with the default expression printer results in newlines in the outputed error message. Bug 23169 | ||||
* | Perform quoting for json. | Bernhard Schommer | 2018-03-08 | 1 | -1/+8 |
| | | | | | | The strings for json need quoting of special characters such as \" and \\. Bug 22438 |