aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
Commit message (Expand)AuthorAgeFilesLines
...
| * | | 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
| |\ \ \ | | | |/ | | |/|
| | * | Support the use of already-installed MenhirLib and Flocq librariesXavier Leroy2020-09-211-2/+1
| | * | Add __builtin_sqrt as synonymous for __builtin_fsqrtXavier Leroy2020-07-271-1/+1
| | * | RISC-V implementation of __builtin_clz* and __builtin_ctz*Xavier Leroy2020-07-272-0/+134
| | * | No need to process __builtin_fabs in $ARCH/Asmexpand.mlXavier Leroy2020-07-271-2/+0
| | * | Move shared code in new file.Bernhard Schommer2020-06-282-18/+0
| | * | Remove the `can_reserve_register` function.Bernhard Schommer2020-06-282-3/+0
| | * | Use Hashtbl.find_opt.Bernhard Schommer2020-06-281-1/+1
* | | | Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-029-239/+553
|\ \ \ \ | | |_|/ | |/| |
| * | | Merge remote-tracking branch 'origin/kvx-work' into kvx-test-prepassDavid Monniaux2020-11-242-3/+14
| |\ \ \
| * | | | allow changing the target coreDavid Monniaux2020-10-222-120/+160
| * | | | attempt at modeling RocketDavid Monniaux2020-10-221-0/+83
| * | | | proves op_valid_pointer_eq lemma for RISC-V (necessary for the pre-pass sched...Sylvain Boulmé2020-10-171-0/+10
| * | | | so that all architectures compileDavid Monniaux2020-10-022-8/+16
| * | | | Merge remote-tracking branch 'origin/kvx-work-riscV' into kvx-test-prepassDavid Monniaux2020-09-216-239/+390
| |\ \ \ \
| | * | | | risc-V now without trapping instructionsDavid Monniaux2020-09-214-74/+90
| | * | | | moved Risc-V div ValueAOp to central locationDavid Monniaux2020-09-211-293/+0
| | * | | | maketotal mod & divDavid Monniaux2020-09-216-165/+593
| | | |/ / | | |/| |
| * | | | wrong resourcesDavid Monniaux2020-09-181-1/+1
| * | | | EH1 schedulingDavid Monniaux2020-09-181-5/+18
| * | | | bogus OpWeights for Risc-VDavid Monniaux2020-09-181-0/+19
| |/ / /
* | | | op_depends_on_memory_correctDavid Monniaux2020-11-251-6/+24
* | | | cond_valid_pointer_eqDavid Monniaux2020-11-251-0/+10
generated by cgit (git 2.34.1) at 2024-05-20 01:53:05 +0000