aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/ExpansionOracle.ml
Commit message (Expand)AuthorAgeFilesLines
* remove todos, cleanLéo Gourdin2021-07-281-1/+0
* branches expansions supportLéo Gourdin2021-07-221-2/+158
* new expansionsLéo Gourdin2021-07-211-1/+197
* bug fix in oracleLéo Gourdin2021-07-201-33/+360
* new expansion oracle for BTLLéo Gourdin2021-07-201-2/+328
* Fix compile on ARM/x86 backendsLéo Gourdin2021-07-201-1054/+2
* Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-101-17/+22
|\
| * removing some Expansion when loading float/single constantsLéo Gourdin2021-06-011-16/+22
| * just remove a debug printLéo Gourdin2021-05-291-1/+0
* | Moving common tools, adding liveness input/output information to BTL generati...Léo Gourdin2021-05-241-1/+1
* | Changing to an opaq record in BTL info, this is a broken commitLéo Gourdin2021-05-201-2/+1
|/
* Adding both RV expansion methods in kvx-workLéo Gourdin2021-05-191-5/+5
* debug prints uniformizedLéo Gourdin2021-05-181-69/+66
* adding missing xorimm expLéo Gourdin2021-04-091-0/+10
* Remove flagsLéo Gourdin2021-04-091-3/+2
* Removing addptrofs draft, next will be mergingLéo Gourdin2021-04-091-30/+0
* bugfixLéo Gourdin2021-04-081-2/+2
* Important commit on expansions' mini CSE, and a draft for addptrofsLéo Gourdin2021-04-061-461/+645
* a more general way to manage special registers before introducing SPLéo Gourdin2021-03-301-60/+61
* Now a more general way to perform imm operationsLéo Gourdin2021-03-301-2/+2
* bugfix and printOpLéo Gourdin2021-03-261-19/+23
* Compiler options to manage expansionsLéo Gourdin2021-03-261-177/+174
* Adding more expansions, improving miniCSE, and tuning prepassLéo Gourdin2021-03-261-173/+414
* Bugfix livenessLéo Gourdin2021-03-231-12/+8
* Remove first nop when doing expansionLéo Gourdin2021-03-211-188/+212
* Adding miniCSE here tooLéo Gourdin2021-03-081-10/+10
* Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexpLéo Gourdin2021-03-061-68/+141
|\
| * some simplification in miniCSELéo Gourdin2021-03-061-17/+14
| * Adding a mini CSE pass in the expansion oracleLéo Gourdin2021-03-061-79/+159
* | Adding a flag to test fp_init_expLéo Gourdin2021-03-021-150/+157
* | [Admitted checker] Oracle expansion for float/float32 constant initLéo Gourdin2021-03-021-2/+23
|/
* Try to save values in virtual registers during expansionLéo Gourdin2021-03-011-89/+100
* Proofs finished for expansionLéo Gourdin2021-03-011-1/+1
* Debugging fake values finishedLéo Gourdin2021-03-011-7/+6
* some bugfixLéo Gourdin2021-03-011-4/+4
* Proof of fsval condition cmp okLéo Gourdin2021-03-011-34/+35
* some more proof for fake hsval checker expansionsLéo Gourdin2021-02-251-2/+2
* [Intermediate] Adding fake hsval for Ccomp expansionLéo Gourdin2021-02-231-4/+4
* Branch expansions activated and configured in the checker (but admitted) and ...Léo Gourdin2021-02-191-5/+6
* Proof of Ocmp expansions without immediate and some drafts in commentLéo Gourdin2021-02-181-5/+5
* fix bug in mergeLéo Gourdin2021-02-161-1/+1
* [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proofLéo Gourdin2021-02-111-9/+9
* [Admitted checker] Adding cbranch expansions (without scratch) to the checkerLéo Gourdin2021-02-101-4/+6
* [Admitted checker] Checker expansion for reg Ocmp (without scratch)Léo Gourdin2021-02-101-7/+7
* Adding pathmap psize modification during expansion oracleLéo Gourdin2021-02-081-9/+20
* cond and branches expandedLéo Gourdin2021-02-061-181/+251
* All Ocmp expanded in RTLLéo Gourdin2021-02-031-185/+315
* Ccomp for longLéo Gourdin2021-02-031-35/+166
* Ccompu expansionLéo Gourdin2021-02-021-9/+18
* Expansion of Ccompimm in RTL [Admitted checker]Léo Gourdin2021-02-021-0/+174