aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/Op.v
Commit message (Collapse)AuthorAgeFilesLines
* Removing addptrofs draft, next will be mergingLéo Gourdin2021-04-091-116/+55
|
* Important commit on expansions' mini CSE, and a draft for addptrofsLéo Gourdin2021-04-061-109/+187
|
* a more general way to manage special registers before introducing SPLéo Gourdin2021-03-301-144/+152
|
* Now a more general way to perform imm operationsLéo Gourdin2021-03-301-10/+24
|
* Refactoring the mayundef OP to be more general...Léo Gourdin2021-03-301-66/+43
|
* Adding more expansions, improving miniCSE, and tuning prepassLéo Gourdin2021-03-261-13/+107
|
* Adding a mini CSE pass in the expansion oracleLéo Gourdin2021-03-061-36/+27
|
* Merge conflicts solved and cleaning in Asmgenproof after expansionLéo Gourdin2021-03-021-2/+1
|
* Merge remote-tracking branch 'origin/riscV-cmov' into riscv-workLéo Gourdin2021-03-021-2/+42
|\
| * begin implementing selectDavid Monniaux2021-02-021-1/+15
| |
| * bits to floatDavid Monniaux2021-02-011-1/+13
| |
| * Obits_of_single etcDavid Monniaux2021-02-011-3/+16
| |
* | Proof of fsval condition cmp okLéo Gourdin2021-03-011-18/+52
| |
* | [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proofLéo Gourdin2021-02-111-26/+98
| |
* | cond and branches expandedLéo Gourdin2021-02-061-69/+226
| |
* | All Ocmp expanded in RTLLéo Gourdin2021-02-031-1/+43
| |
* | Ccomp for longLéo Gourdin2021-02-031-5/+105
| |
* | Ccompu expansionLéo Gourdin2021-02-021-6/+32
| |
* | Expansion of Ccompimm in RTL [Admitted checker]Léo Gourdin2021-02-021-2/+92
|/
* Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3David Monniaux2020-12-021-122/+153
|\
| * proves op_valid_pointer_eq lemma for RISC-V (necessary for the pre-pass ↵Sylvain Boulmé2020-10-171-0/+10
| | | | | | | | scheduler)
| * risc-V now without trapping instructionsDavid Monniaux2020-09-211-66/+66
| |
| * maketotal mod & divDavid Monniaux2020-09-211-56/+87
| |
* | op_depends_on_memory_correctDavid Monniaux2020-11-251-6/+24
| |
* | cond_valid_pointer_eqDavid Monniaux2020-11-251-0/+10
| |
* | pointer_eq copiedDavid Monniaux2020-11-251-0/+10
|/
* porting to ppc riscV x86David Monniaux2020-04-011-3/+9
|
* trapping ops on rvDavid Monniaux2019-09-241-0/+30
|
* fix for Risc-VDavid Monniaux2019-09-071-0/+14
|
* PowerPC compilesDavid Monniaux2019-09-071-0/+26
|
* Remove coq warnings (#28)Bernhard Schommer2017-09-221-1/+1
| | | | Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-061-0/+21
| | | | | | | | - Add support for PowerPC, with all addressing modes. - Add support for ARM, with "reg + ofs" addressing mode. - Add support for RISC-V, with the one addressing mode. - Constprop.v: forgot to recurse in BA_addptr - volatile4 test: more tests
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+1340
This commits adds code generation for the RISC-V architecture, both in 32- and 64-bit modes. The generated code was lightly tested using the simulator and cross-binutils from https://riscv.org/software-tools/ This port required the following additional changes: - Integers: More properties about shrx - SelectOp: now provides smart constructors for mulhs and mulhu - SelectDiv, 32-bit integer division and modulus: implement constant propagation, use the new smart constructors mulhs and mulhu. - Runtime library: if no asm implementation is provided, run the reference C implementation through CompCert. Since CompCert rejects the definitions of names of special functions such as __i64_shl, the reference implementation now uses "i64_" names, e.g. "i64_shl", and a renaming "i64_ -> __i64_" is performed over the generated assembly file, before assembling and building the runtime library. - test/: add SIMU make variable to run tests through a simulator - test/regression/alignas.c: make sure _Alignas and _Alignof are not #define'd by C headers commit da14495c01cf4f66a928c2feff5c53f09bde837f Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Thu Apr 13 17:36:10 2017 +0200 RISC-V port, continued Now working on Asmgen. commit 36f36eb3a5abfbb8805960443d087b6a83e86005 Author: Xavier Leroy <xavier.leroy@inria.fr> Date: Wed Apr 12 17:26:39 2017 +0200 RISC-V port, first steps This port is based on Prashanth Mundkur's experimental RV32 port and brings it up to date with CompCert, and adds 64-bit support (RV64). Work in progress.
generated by cgit (git 2.34.1) at 2024-05-20 08:23:56 +0000