aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/ExpansionOracle.ml
Commit message (Collapse)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 ↵Léo Gourdin2021-05-241-1/+1
| | | | | | | | generation oracle
* | 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
| | | | bugfix in the expansion liveness modification
* 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