aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Collapse)AuthorAgeFilesLines
...
| | * | | | | | | | | | | | | | | | moved some "total" value domain functions to a central locationDavid Monniaux2020-09-211-1/+243
| | | | | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | | | | Merge branch 'kvx-work' into mppa-RTLpathSECyril SIX2020-05-2852-391/+6967
| |\| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Adapting the new mppa-RTLpathSE passes into the new Compiler.vexpand framework
| * | | | | | | | | | | | | | | | | [BROKEN] Merge branch 'mppa-work' into mppa-RTLpathSECyril SIX2020-04-1067-473/+5837
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
| * | | | | | | | | | | | | | | | | | Compatibility Coq 8.11.0Cyril SIX2020-04-103-10/+10
| | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | not yet the transfer functions that record predicatesDavid Monniaux2020-11-263-9/+78
| | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | remains one admitDavid Monniaux2020-11-261-8/+46
| | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | is_condition_present_soundDavid Monniaux2020-11-263-5/+23
| | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | begin implementing cond tableDavid Monniaux2020-11-261-6/+13
| | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | ajouté Cond, tout passeDavid Monniaux2020-11-263-40/+168
| | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | passage à EquDavid Monniaux2020-11-263-189/+196
| | | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | | cond_valid_pointer_eqDavid Monniaux2020-11-251-0/+14
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | store2_soundDavid Monniaux2020-11-251-1/+1
| | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | clever_kill_store_soundDavid Monniaux2020-11-251-7/+5
| | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | kill_store_soundDavid Monniaux2020-11-251-0/+49
| | | | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | | two lemmas admittedDavid Monniaux2020-11-253-9/+115
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | | tiny simplification in Tunnelingaux.mlSylvain Boulmé2020-11-241-2/+2
| |_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | minor fix in coq2html commentSylvain Boulmé2020-11-161-1/+2
| | | | | | | | | | | | | | | |
* | | | | | | | | | | | | | | | Tunneling: improved elimination of conditionsSylvain Boulmé2020-11-164-256/+670
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | | | | | | | | | | | | | | Fixing issue with loops having branches leading to goto backedgeCyril SIX2020-11-052-27/+32
| |_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | |
* | | | | | | | | | | | | | Fixing get_loop_headers + alternative get_inner_loops (commented, not active)Cyril SIX2020-11-042-27/+107
| | | | | | | | | | | | | |
* | | | | | | | | | | | | | do not print "refining" unless askedDavid Monniaux2020-11-041-1/+2
| |_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | |
* | | | | | | | | | | | | do not print "updates" to nodesDavid Monniaux2020-11-041-1/+2
| |_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | |
* | | | | | | | | | | | refixcse3David Monniaux2020-11-032-34/+53
| | | | | | | | | | | |
* | | | | | | | | | | | Loop Rotate with -flooprotateCyril SIX2020-11-032-1/+61
| |_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | |
* | | | | | | | | | | refining CSE3 nodesDavid Monniaux2020-10-311-14/+81
| | | | | | | | | | |
* | | | | | | | | | | seems to work betterDavid Monniaux2020-10-312-3/+37
| | | | | | | | | | |
* | | | | | | | | | | also match IstoreDavid Monniaux2020-10-301-1/+2
| |_|_|_|_|_|_|_|/ / |/| | | | | | | | |
* | | | | | | | | | reinstated old versionDavid Monniaux2020-10-304-216/+39
| | | | | | | | | |
* | | | | | | | | | reinstated previous forward_move functionDavid Monniaux2020-10-292-11/+98
| |_|_|_|_|_|_|/ / |/| | | | | | | |
* | | | | | | | | CSE3 trivial_ops flagDavid Monniaux2020-10-292-3/+3
| | | | | | | | |
* | | | | | | | | in CSE3 choose lowest variable as representative for movesDavid Monniaux2020-10-293-45/+104
| |_|_|_|_|_|/ / |/| | | | | | |
* | | | | | | | DuplicateParam -> DuplicateOracle + simpler DuplicatepassesSylvain Boulmé2020-10-283-40/+24
| |_|_|_|_|/ / |/| | | | | |
* | | | | | | Correcting typoCyril SIX2020-10-271-3/+3
| | | | | | |
* | | | | | | Merge branch 'kvx-work' into duplicate-paramCyril SIX2020-10-273-41/+107
|\ \ \ \ \ \ \
| * | | | | | | new CSE3David Monniaux2020-10-273-41/+107
| | |_|_|_|/ / | |/| | | | |
* | | | | | | Oops forgot Duplicatepasses.vCyril SIX2020-10-271-0/+64
| | | | | | |
* | | | | | | Splitting Duplicate in several passesCyril SIX2020-10-271-14/+20
| | | | | | |
* | | | | | | Reworked Duplicate to be parametrizedCyril SIX2020-10-272-5/+26
|/ / / / / /
* | | | | | Loop body unrolling with -funrollbody nCyril SIX2020-10-161-3/+6
| | | | | |
* | | | | | Loop body unrollingCyril SIX2020-10-161-1/+39
| | | | | |
* | | | | | Comment updateCyril SIX2020-10-161-1/+7
| | | | | |
* | | | | | Merge remote-tracking branch 'origin/kvx-work-unroll-fixcse3' into kvx-workDavid Monniaux2020-10-165-14/+458
|\ \ \ \ \ \
| * | | | | | kill useless moves (not yet connected)David Monniaux2020-10-162-0/+401
| | | | | | |
| * | | | | | some more tuning of CSE3David Monniaux2020-10-152-10/+23
| | | | | | |
| * | | | | | a bit of progressDavid Monniaux2020-10-143-4/+34
| | | | | | |
* | | | | | | Comment updateCyril SIX2020-10-161-0/+1
|/ / / / / /
* | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-work-unrollCyril SIX2020-10-141-6/+0
|\ \ \ \ \ \
| * | | | | | centralize if_sameDavid Monniaux2020-10-091-6/+0
| | |_|_|/ / | |/| | | |
* | | | | | Ignoring Inops for counting number of instructionsCyril SIX2020-10-141-6/+15
| | | | | |
* | | | | | Only unrolling on a given instruction limitCyril SIX2020-10-091-12/+16
| | | | | |
generated by cgit (git 2.34.1) at 2024-07-06 15:59:09 +0000