aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
Commit message (Expand)AuthorAgeFilesLines
* Adding a flag to test fp_init_expLéo Gourdin2021-03-021-150/+157
* Adding fp init expansionsLéo Gourdin2021-03-021-0/+15
* Merge remote-tracking branch 'origin/riscv-still-asmcondexp' into riscv-work-...Léo Gourdin2021-03-023-96/+1088
|\
| * Asmcondexp branche useful to benchmark expansionsLéo Gourdin2021-03-023-96/+1088
* | [Admitted checker] Oracle expansion for float/float32 constant initLéo Gourdin2021-03-022-6/+27
|/
* Merge conflicts solved and cleaning in Asmgenproof after expansionLéo Gourdin2021-03-024-1148/+106
* Merge remote-tracking branch 'origin/riscV-cmov' into riscv-workLéo Gourdin2021-03-0214-19/+624
|\
| * Adding missing operators in PrintOp for debuggingLéo Gourdin2021-02-251-0/+5
| * écrase X31riscV-cmovDavid Monniaux2021-02-031-1/+2
| * Merge remote-tracking branch 'origin/kvx-work' into riscV-cmovDavid Monniaux2021-02-031-1/+1
| |\
| * | detect redundant cmovDavid Monniaux2021-02-022-3/+34
| * | fix code generation for select(b, r, r)David Monniaux2021-02-021-2/+7
| * | fix problem if rt = rfDavid Monniaux2021-02-021-6/+8
| * | Cmov TsingleDavid Monniaux2021-02-023-33/+43
| * | implement for another register configurationDavid Monniaux2021-02-021-1/+8
| * | some more cases implementedDavid Monniaux2021-02-021-12/+25
| * | PselectdDavid Monniaux2021-02-023-0/+33
| * | cmov on integersDavid Monniaux2021-02-022-11/+88
| * | begin synthesizing selectDavid Monniaux2021-02-023-2/+34
| * | asmgen OselectlDavid Monniaux2021-02-022-0/+11
| * | begin implementing selectDavid Monniaux2021-02-027-6/+113
| * | select01_longDavid Monniaux2021-02-011-130/+10
| * | repr etc.David Monniaux2021-02-011-4/+2
| * | bitwise_select_value_correctDavid Monniaux2021-02-011-0/+12
| * | int64_of_value some moreDavid Monniaux2021-02-011-14/+15
| * | int64_of_valueDavid Monniaux2021-02-011-0/+77
| * | Asmgen for bits / floatDavid Monniaux2021-02-011-0/+13
| * | bits to floatDavid Monniaux2021-02-019-5/+82
| * | adding builtinsDavid Monniaux2021-02-014-6/+27
| * | Obits_of_single etcDavid Monniaux2021-02-013-3/+46
| * | define some semantics in AsmDavid Monniaux2021-02-012-3/+24
| * | select_longDavid Monniaux2021-01-301-0/+38
| * | select through bitwise operationsDavid Monniaux2021-01-301-0/+40
* | | Try to save values in virtual registers during expansionLéo Gourdin2021-03-012-94/+117
* | | Proofs finished for expansionLéo Gourdin2021-03-012-19/+62
* | | Debugging fake values finishedLéo Gourdin2021-03-012-14/+20
* | | some bugfixLéo Gourdin2021-03-012-15/+20
* | | Proof of fsval condition cmp okLéo Gourdin2021-03-018-170/+527
* | | [Admitted checker] Some more proof, version with buggy addirw0Léo Gourdin2021-02-251-5/+126
* | | some more proof for fake hsval checker expansionsLéo Gourdin2021-02-252-46/+771
* | | [Intermediate] Adding fake hsval for Ccomp expansionLéo Gourdin2021-02-232-7/+112
* | | Merge remote-tracking branch 'origin/riscv-work-rules' into riscv-workLéo Gourdin2021-02-231-0/+19
|\ \ \
| * | | Separate target_op_simplify for riscVLéo Gourdin2021-02-231-0/+19
| | |/ | |/|
* | | 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-182-6/+6
* | | fix bug in mergeLéo Gourdin2021-02-161-1/+1
* | | [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proofLéo Gourdin2021-02-118-61/+248
* | | [Admitted checker] Adding cbranch expansions (without scratch) to the checkerLéo Gourdin2021-02-102-5/+7
* | | [Admitted checker] Checker expansion for reg Ocmp (without scratch)Léo Gourdin2021-02-104-36/+36
* | | Adding pathmap psize modification during expansion oracleLéo Gourdin2021-02-081-9/+20