Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Conditions now propagated by CSE3 | David Monniaux | 2021-01-20 | 1 | -1/+3 |
|\ | | | | | | | Merge remote-tracking branch 'origin/kvx-better2-cse3' into kvx-work | ||||
| * | begin implementing -fcse3-conditions | David Monniaux | 2020-12-09 | 1 | -0/+2 |
| | | |||||
| * | CSE3 with Abst_same | David Monniaux | 2020-12-08 | 1 | -1/+1 |
| | | |||||
| * | CSE3 now runs on its own fixpoint iterator not based on Kildall.v | David Monniaux | 2020-12-08 | 1 | -1/+1 |
| | | |||||
| * | passage à Equ | David Monniaux | 2020-11-26 | 1 | -1/+1 |
| | | |||||
* | | fix extraction of non-aarch64 targets | Sylvain Boulmé | 2020-12-17 | 1 | -2/+0 |
| | | |||||
* | | Removing OrigAsmgen by moving the necessary functions in Asmgen.v | Léo Gourdin | 2020-11-25 | 1 | -1/+3 |
| | | |||||
* | | Merge remote-tracking branch 'origin/aarch64_Pfmovimm_fix' into aarch64-postpass | Léo Gourdin | 2020-11-18 | 1 | -0/+2 |
|\| | |||||
| * | in CSE3 choose lowest variable as representative for moves | David Monniaux | 2020-10-29 | 1 | -0/+2 |
| | | |||||
* | | aarch64 compiles again (but ccomp generates incorrect assembly) | Sylvain Boulmé | 2020-10-23 | 1 | -1/+3 |
|/ | |||||
* | Changing duplicate verifier to be non optional | Cyril SIX | 2020-10-09 | 1 | -2/+0 |
| | |||||
* | -fcse3-glb | David Monniaux | 2020-05-06 | 1 | -0/+2 |
| | |||||
* | CSE3 across merges | David Monniaux | 2020-05-06 | 1 | -0/+2 |
| | |||||
* | Merge remote-tracking branch 'origin/mppa-licm' into mppa-features | David Monniaux | 2020-04-23 | 1 | -0/+2 |
|\ | |||||
| * | CSE3 across calls | David Monniaux | 2020-04-23 | 1 | -0/+2 |
| | | |||||
* | | Merge remote-tracking branch 'origin/mppa-licm' into mppa-features | David Monniaux | 2020-04-20 | 1 | -1/+10 |
|\| | |||||
| * | add options for controlling madd and notrap selection | David Monniaux | 2020-04-19 | 1 | -0/+2 |
| | | |||||
| * | forgotten extraction | David Monniaux | 2020-04-19 | 1 | -1/+2 |
| | | |||||
| * | route through LICMaux | David Monniaux | 2020-04-01 | 1 | -0/+3 |
| | | |||||
| * | begin adapting for LICM phase | David Monniaux | 2020-04-01 | 1 | -0/+3 |
| | | |||||
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-licm | David Monniaux | 2020-04-01 | 1 | -0/+2 |
| |\ | |||||
* | \ | Merge remote-tracking branch 'origin/mppa-profiling' into mppa-features | David Monniaux | 2020-04-12 | 1 | -1/+13 |
|\ \ \ | |||||
| * | | | reloading and exploiting seems to work | David Monniaux | 2020-04-08 | 1 | -1/+6 |
| | | | | |||||
| * | | | print hashes | David Monniaux | 2020-04-08 | 1 | -0/+2 |
| | | | | |||||
| * | | | installed Profiling (not finished) | David Monniaux | 2020-04-08 | 1 | -1/+6 |
| | |/ | |/| | |||||
* | | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3 | David Monniaux | 2020-04-01 | 1 | -0/+2 |
|\| | | |/ |/| | |||||
| * | -fduplicate -1 really desactivates the pass in Coq now | Cyril SIX | 2020-04-01 | 1 | -0/+2 |
| | | |||||
* | | CSE3 alias analysis | David Monniaux | 2020-03-14 | 1 | -0/+2 |
| | | |||||
* | | removed second analysis phase | David Monniaux | 2020-03-12 | 1 | -1/+1 |
| | | |||||
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse3 | David Monniaux | 2020-03-11 | 1 | -2/+0 |
|\| | |||||
| * | [BROKEN] Replacing the boolean -fduplicate option by an integer | Cyril SIX | 2020-03-09 | 1 | -2/+0 |
| | | | | | | | | To control the threshold for duplication | ||||
* | | printing created hashes | David Monniaux | 2020-03-10 | 1 | -1/+1 |
| | | |||||
* | | starts compiling but still fake | David Monniaux | 2020-03-10 | 1 | -2/+7 |
| | | |||||
* | | just the analysis | David Monniaux | 2020-03-05 | 1 | -2/+2 |
| | | |||||
* | | more about extraction and linking | David Monniaux | 2020-03-05 | 1 | -0/+7 |
|/ | |||||
* | Merge remote-tracking branch 'origin/mppa-work' into mppa-cse2 | David Monniaux | 2020-02-06 | 1 | -0/+2 |
|\ | |||||
| * | Added a flag to desactivate tail duplication | Cyril SIX | 2020-01-27 | 1 | -0/+2 |
| | | |||||
* | | Merge branch 'dm-cse2' of /home/monniaux/progs/CompCert into mppa-cs2 | David Monniaux | 2020-01-28 | 1 | -0/+2 |
|\ \ | |/ |/| | |||||
| * | connected (just a silly problem) | David Monniaux | 2020-01-28 | 1 | -0/+2 |
| | | |||||
* | | connect forward-moves to compiler | David Monniaux | 2020-01-08 | 1 | -0/+2 |
| | | |||||
* | | to v3.6 | David Monniaux | 2019-09-20 | 1 | -1/+1 |
| | | |||||
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load | David Monniaux | 2019-09-20 | 1 | -0/+1 |
|\ \ | |||||
| * | | Timings for Machblockgen, Asmblockgen and postpass scheduling | Cyril SIX | 2019-09-18 | 1 | -0/+1 |
| | | | |||||
* | | | -fall-loads-nontrap | David Monniaux | 2019-09-09 | 1 | -0/+4 |
|/ / | |||||
* | | various fixes | David Monniaux | 2019-07-19 | 1 | -0/+1 |
| | | |||||
* | | helpers broke compilation | David Monniaux | 2019-07-19 | 1 | -5/+0 |
| | | |||||
* | | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵ | David Monniaux | 2019-07-19 | 1 | -11/+6 |
|\| | | | | | | | mppa-work-upstream-merge | ||||
| * | Make __builtin_sel available from C source code | Xavier Leroy | 2019-07-17 | 1 | -1/+2 |
| | | | | | | | | | | It is type-checked like a conditional expression then translated to a call to the known builtin function. | ||||
| * | New parser based on new version of the Coq backend of Menhir (#276) | Jacques-Henri Jourdan | 2019-07-05 | 1 | -11/+1 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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. | ||||
| * | If-conversion optimization | Xavier Leroy | 2019-06-06 | 1 | -0/+1 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Extends the instruction selection pass with an if-conversion optimization: some if/then/else statements are converted into "select" operations, which in turn can be compiled down to branchless instruction sequences if the target architecture supports them. The statements that are converted are of the form if (cond) { x = a1; } else { x = a2; } if (cond) { x = a1; } if (cond) { /*skip*/; } else { x = a2; } where a1, a2 are "safe" expressions, containing no operations that can fail at run-time, such as memory loads or integer divisions. A heuristic in backend/Selectionaux.ml controls when the optimization occurs, depending on command-line flags and the complexity of the "then" and "else" branches. |