| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | [MERGE] BTL into kvx-work (replacing RTLpath) | Léo Gourdin | 2021-09-01 | 1 | -3/+3 |
| |\ | |||||
| | * | Dupmap bugfix and some advance in Livegen | Léo Gourdin | 2021-05-31 | 1 | -1/+1 |
| | | | |||||
| | * | todos | Léo Gourdin | 2021-05-18 | 1 | -1/+1 |
| | | | |||||
| | * | preparing compiler passes and ml oracles | Léo Gourdin | 2021-05-17 | 1 | -3/+3 |
| | | | |||||
| * | | Change "Tunneling" to "LTLTunneling" everywhere | Pierre Goutagny | 2021-06-17 | 1 | -1/+1 |
| | | | | | | | | | To respect the symmetry between RTL- and LTL-Tunneling | ||||
| * | | Move rtl_tunneling to a more interesting place | Pierre Goutagny | 2021-06-15 | 1 | -1/+1 |
| | | | |||||
| * | | Factorise RTL Tunneling pass in compiler_expand | Pierre Goutagny | 2021-06-15 | 1 | -1/+3 |
| | | | |||||
| * | | Add RTL Tunneling as a pass | Pierre Goutagny | 2021-06-14 | 1 | -1/+2 |
| |/ | |||||
| * | insert CSE after constant propagation and before CSE2 | Sylvain Boulmé | 2021-02-10 | 1 | -0/+1 |
| | | | | | => useful to have a nice generated code for || (and also probably &&) | ||||
| * | Slight perf improvement | Cyril SIX | 2020-12-02 | 1 | -2/+2 |
| | | |||||
| * | merge nouveau tunneling | David Monniaux | 2020-11-19 | 1 | -1/+1 |
| | | |||||
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-19 | 1 | -1/+1 |
| |\ | |||||
| | * | Tunneling: improved elimination of conditions | Sylvain Boulmé | 2020-11-16 | 1 | -2/+2 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Previously, the elimination of useless conditions done in the 2nd pass of the tunneling introduced some new "nop" instructions that were not eliminated. This commit solves this issue by anticipating the elimination of conditions in the 1st pass of the tunneling, the 2nd pass being unchanged. In case of cycles in the CFG, the full elimination of useless conditions may require several iterations in the 1st pass. Moreover, in the simulation proof, the measure counting the number of eliminated steps from each node, needs to be adapted according to the modifications on the 1st pass. Hence, this measure results from a quite complex fixpoint computation: proving its properties would be very difficult. This leads us to introduce an oracle, implementing the first pass and producing the expected measure. A certified verifier directly checks that the measure provided by the oracle satisfies the properties expected by the simulation proof. Introducing this oracle/verifier pair has here the following advantage: - the proof is simpler than the original one (e.g. having a certified union-find structure is no more necessary for this pass). - the oracle is very efficient, by using imperative data-structure to compute memoized fixpoints. At runtime, the overhead induced by the verifier computations (and the actual computation of the measure) seems largely compensated by the gains obtained through the imperative oracle. | ||||
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-05 | 1 | -2/+3 |
| |\| | |||||
| | * | move loop rotate down | David Monniaux | 2020-11-04 | 1 | -4/+5 |
| | | | |||||
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-11-03 | 1 | -1/+3 |
| |\| | |||||
| | * | Loop Rotate with -flooprotate | Cyril SIX | 2020-11-03 | 1 | -0/+2 |
| | | | |||||
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-27 | 1 | -43/+54 |
| |\| | |||||
| | * | Splitting Duplicate in several passes | Cyril SIX | 2020-10-27 | 1 | -40/+51 |
| | | | |||||
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepass | David Monniaux | 2020-10-18 | 1 | -2/+3 |
| |\| | |||||
| | * | reorder phases | David Monniaux | 2020-10-16 | 1 | -2/+3 |
| | | | |||||
| | * | Changing duplicate verifier to be non optional | Cyril SIX | 2020-10-09 | 1 | -1/+1 |
| | | | |||||
| * | | Merge branch 'kvx-work' into mppa-RTLpathSE | Cyril SIX | 2020-05-28 | 1 | -1/+4 |
| |/ | | | | | Adapting the new mppa-RTLpathSE passes into the new Compiler.vexpand framework | ||||
| * | add a renumber phase | David Monniaux | 2020-04-30 | 1 | -0/+1 |
| | | |||||
| * | run a separate CSE3 for LICM | David Monniaux | 2020-04-24 | 1 | -1/+3 |
| | | |||||
| * | sync with licm | David Monniaux | 2020-04-23 | 1 | -1/+1 |
| | | |||||
| * | cbn and copyright | David Monniaux | 2020-04-22 | 1 | -0/+10 |
| | | |||||
| * | use cbn in T instead of simpl in T | David Monniaux | 2020-04-22 | 1 | -1/+1 |
| | | |||||
| * | automated writing Compiler.v | David Monniaux | 2020-04-22 | 1 | -8/+79 |
| | | |||||
| * | generate mkpass | David Monniaux | 2020-04-21 | 1 | -1/+13 |
| | | |||||
| * | Require autogen | David Monniaux | 2020-04-21 | 1 | -8/+22 |
| | | |||||
| * | begin scripting the Compiler.v file | David Monniaux | 2020-04-21 | 1 | -0/+62 |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |