aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)AuthorAgeFilesLines
* Fixing wrong predictions on imbricated loopsCyril SIX2020-12-111-104/+114
* Fixing exponential blowup on get_loop_info.mark_path.exploreCyril SIX2020-12-091-33/+44
* Flushing debug outputCyril SIX2020-12-091-1/+1
* The last fix for get_loop_info was giving false positives. Fixing that.Cyril SIX2020-12-081-2/+12
* Fixing get_loop_info : part 2Cyril SIX2020-12-081-8/+28
* Fixing loop detection in get_loop_info - part 1Cyril SIX2020-12-081-16/+8
* Moving codeCyril SIX2020-12-081-71/+72
* More debugCyril SIX2020-12-081-6/+21
* More debugCyril SIX2020-12-081-3/+3
* Do not duplicate nodes that don't need to when unrolling the bodyCyril SIX2020-12-081-4/+18
* Fix on find_last_node_before_loopCyril SIX2020-12-081-3/+7
* Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-0411-286/+1393
|\
| * CommentCyril SIX2020-12-041-0/+1
| * Less aggressive tail duplicationCyril SIX2020-12-041-6/+11
| * Clean-up debugCyril SIX2020-12-041-4/+2
| * Fixed infinite loop on find_last_node_before_loopCyril SIX2020-12-041-3/+6
| * 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
| |\|
| * | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-053-28/+109
| |\ \
| * \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-041-1/+2
| |\ \ \
| * \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-034-35/+114
| |\ \ \ \
| * \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-313-17/+118
| |\ \ \ \ \
| * \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-304-168/+78
| |\ \ \ \ \ \
| * \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-294-48/+107
| |\ \ \ \ \ \ \
| * \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-283-40/+24
| |\ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-274-19/+110
| |\ \ \ \ \ \ \ \ \
| * | | | | | | | | | 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
| * | | | | | | | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-188-143/+845
| |\ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-10-021-2/+9
| |\ \ \ \ \ \ \ \ \ \ \
| * \ \ \ \ \ \ \ \ \ \ \ Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepassDavid Monniaux2020-09-211-1/+482
| |\ \ \ \ \ \ \ \ \ \ \ \
| | * | | | | | | | | | | | risc-V now without trapping instructionsDavid Monniaux2020-09-211-0/+24
generated by cgit (git 2.34.1) at 2024-06-02 23:19:23 +0000