aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
Commit message (Expand)AuthorAgeFilesLines
...
| * | | 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
* | | | Merge remote-tracking branch 'origin/CompCert_RTLpath_simuX' into riscv-workLéo Gourdin2021-02-081-1/+1
|\| | |
| * | | fix OpWeightsDavid Monniaux2021-01-301-1/+1
| |/ /
* | | cond and branches expandedLéo Gourdin2021-02-068-293/+691
* | | All Ocmp expanded in RTLLéo Gourdin2021-02-037-202/+417
* | | Ccomp for longLéo Gourdin2021-02-038-52/+408
* | | Ccompu expansionLéo Gourdin2021-02-028-178/+223
* | | Expansion of Ccompimm in RTL [Admitted checker]Léo Gourdin2021-02-028-4/+383
|/ /
* | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-085-26/+136
|\ \
| * \ Merge branch 'kvx-work' into kvx-work-merge3.8Cyril SIX2020-12-0411-242/+577
| |\ \
| * \ \ Merge branch 'master' (Absint 3.8) into kvx-work-merge3.8David Monniaux2020-11-185-26/+136
| |\ \ \ | | | |/ | | |/|
generated by cgit (git 2.34.1) at 2024-07-04 02:21:14 +0000