Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Adding both RV expansion methods in kvx-work | Léo Gourdin | 2021-05-19 | 1 | -0/+344 |
| | |||||
* | Removing expansions from Asmgen | Léo Gourdin | 2021-04-09 | 1 | -344/+0 |
| | |||||
* | Removing addptrofs draft, next will be merging | Léo Gourdin | 2021-04-09 | 1 | -14/+0 |
| | |||||
* | Important commit on expansions' mini CSE, and a draft for addptrofs | Léo Gourdin | 2021-04-06 | 1 | -13/+45 |
| | |||||
* | a more general way to manage special registers before introducing SP | Léo Gourdin | 2021-03-30 | 1 | -68/+89 |
| | |||||
* | Now a more general way to perform imm operations | Léo Gourdin | 2021-03-30 | 1 | -6/+9 |
| | |||||
* | Adding more expansions, improving miniCSE, and tuning prepass | Léo Gourdin | 2021-03-26 | 1 | -0/+24 |
| | |||||
* | Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexp | Léo Gourdin | 2021-03-06 | 1 | -4/+4 |
|\ | |||||
| * | Adding a mini CSE pass in the expansion oracle | Léo Gourdin | 2021-03-06 | 1 | -4/+4 |
| | | |||||
* | | Asmcondexp branche useful to benchmark expansions | Léo Gourdin | 2021-03-02 | 1 | -0/+247 |
|/ | |||||
* | Merge conflicts solved and cleaning in Asmgenproof after expansion | Léo Gourdin | 2021-03-02 | 1 | -253/+0 |
| | |||||
* | Merge remote-tracking branch 'origin/riscV-cmov' into riscv-work | Léo Gourdin | 2021-03-02 | 1 | -0/+25 |
|\ | |||||
| * | asmgen Oselectl | David Monniaux | 2021-02-02 | 1 | -0/+7 |
| | | |||||
| * | Asmgen for bits / float | David Monniaux | 2021-02-01 | 1 | -0/+13 |
| | | |||||
* | | Proof of fsval condition cmp ok | Léo Gourdin | 2021-03-01 | 1 | -4/+4 |
| | | |||||
* | | [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proof | Léo Gourdin | 2021-02-11 | 1 | -0/+32 |
| | | |||||
* | | [Admitted checker] Adding cbranch expansions (without scratch) to the checker | Léo Gourdin | 2021-02-10 | 1 | -1/+1 |
| | | |||||
* | | [Admitted checker] Checker expansion for reg Ocmp (without scratch) | Léo Gourdin | 2021-02-10 | 1 | -14/+14 |
| | | |||||
* | | cond and branches expanded | Léo Gourdin | 2021-02-06 | 1 | -23/+65 |
| | | |||||
* | | All Ocmp expanded in RTL | Léo Gourdin | 2021-02-03 | 1 | -7/+37 |
| | | |||||
* | | Ccomp for long | Léo Gourdin | 2021-02-03 | 1 | -3/+44 |
| | | |||||
* | | Ccompu expansion | Léo Gourdin | 2021-02-02 | 1 | -0/+9 |
| | | |||||
* | | Expansion of Ccompimm in RTL [Admitted checker] | Léo Gourdin | 2021-02-02 | 1 | -2/+38 |
|/ | |||||
* | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-work | David Monniaux | 2020-01-15 | 1 | -10/+20 |
|\ | |||||
| * | 64-bit signed division by two code | David Monniaux | 2020-01-14 | 1 | -5/+10 |
| | | |||||
| * | rv32: 3-instruction signed divide-by-two sequence (as opposed to 4) | David Monniaux | 2020-01-14 | 1 | -5/+10 |
| | | |||||
* | | Merge remote-tracking branch 'origin/mppa-work' into mppa-non-trapping-load | David Monniaux | 2019-12-02 | 1 | -0/+2 |
|\ \ | |||||
| * | | fix compile for rv32 | David Monniaux | 2019-10-16 | 1 | -0/+2 |
| |/ | |||||
* / | fix for Risc-V | David Monniaux | 2019-09-07 | 1 | -4/+9 |
|/ | |||||
* | RISC-V port and assorted changes | Xavier Leroy | 2017-04-28 | 1 | -0/+936 |
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. |