aboutsummaryrefslogtreecommitdiffstats
path: root/backend
Commit message (Expand)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
| |\| | | | | | | | | | | | | | | |
| * | | | | | | | | | | | | | | | | [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
| |_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | |
* | | | | | | | | | | | | | | 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-04 01:37:45 +0000