aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Slight perf improvementCyril SIX2020-12-021-2/+2
* [expensive] Behavior change when the loop has two final instructionsCyril SIX2020-12-021-9/+57
* Duplicateaux: Generalization of look_aheadCyril SIX2020-12-011-3/+5
* Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassCyril SIX2020-12-013-8/+161
|\
| * 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
* | Ignore loopback edges on tail-duplicateCyril SIX2020-12-011-0/+2
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-241-2/+2
|\|
| * tiny simplification in Tunnelingaux.mlSylvain Boulmé2020-11-241-2/+2
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-194-257/+672
|\|
| * minor fix in coq2html commentSylvain Boulmé2020-11-161-1/+2
| * Tunneling: improved elimination of conditionsSylvain Boulmé2020-11-164-256/+670
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-062-27/+32
|\|
| * Fixing issue with loops having branches leading to goto backedgeCyril SIX2020-11-052-27/+32
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-053-28/+109
|\|
| * 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
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-041-1/+2
|\|
| * do not print "updates" to nodesDavid Monniaux2020-11-041-1/+2
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-034-35/+114
|\|
| * refixcse3David Monniaux2020-11-032-34/+53
| * Loop Rotate with -flooprotateCyril SIX2020-11-032-1/+61
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-313-17/+118
|\|
| * 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
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-304-168/+78
|\|
| * reinstated old versionDavid Monniaux2020-10-304-216/+39
| * reinstated previous forward_move functionDavid Monniaux2020-10-292-11/+98
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-294-48/+107
|\|
| * CSE3 trivial_ops flagDavid Monniaux2020-10-292-3/+3
| * in CSE3 choose lowest variable as representative for movesDavid Monniaux2020-10-293-45/+104
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-283-40/+24
|\|
| * DuplicateParam -> DuplicateOracle + simpler DuplicatepassesSylvain Boulmé2020-10-283-40/+24
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-274-19/+110
|\|
| * 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
| |/
* | improved CSE3David Monniaux2020-10-271-12/+12
* | progress in proofs on new CSE3David Monniaux2020-10-271-3/+34
* | deactivate LICM by defaultDavid Monniaux2020-10-271-20/+11
* | begin fixing CSE3 to keep more inductive stuffDavid Monniaux2020-10-272-10/+19
* | invariant printing more aligned with RTL dumpsDavid Monniaux2020-10-271-2/+2
* | print invariantsDavid Monniaux2020-10-271-11/+46
* | attempt at store -> load.sDavid Monniaux2020-10-261-2/+3
generated by cgit (git 2.34.1) at 2024-06-03 03:32:23 +0000