aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/Asmgenproof.v
Commit message (Collapse)AuthorAgeFilesLines
* Merge remote-tracking branch 'absint/master' into kvx-workCyril SIX2021-06-011-2/+4
|\
| * Register X1 is destroyed by some built-in functionsXavier Leroy2021-05-131-2/+4
| | | | | | | | E.g. __builtin_bswap. Update Asm modeling of builtins accordingly.
* | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-011-18/+146
|\ \
| * | Adding both RV expansion methods in kvx-workLéo Gourdin2021-05-191-3/+159
| | |
| * | Removing expansions from AsmgenLéo Gourdin2021-04-091-159/+3
| | |
| * | Removing addptrofs draft, next will be mergingLéo Gourdin2021-04-091-2/+0
| | |
| * | Important commit on expansions' mini CSE, and a draft for addptrofsLéo Gourdin2021-04-061-1/+2
| | |
| * | a more general way to manage special registers before introducing SPLéo Gourdin2021-03-301-28/+28
| | |
| * | Now a more general way to perform imm operationsLéo Gourdin2021-03-301-0/+1
| | |
| * | Asmcondexp branche useful to benchmark expansionsLéo Gourdin2021-03-021-18/+146
| | |
* | | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-6/+6
|\ \ \ | |/ / |/| / | |/ | | | | | | | | | | PARTIAL MERGE (PARTLY BROKEN). See unsolved conflicts in: aarch64/TO_MERGE and riscV/TO_MERGE WARNING: interface of va_args and assembly sections have changed
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-6/+6
| | | | | | | | | | | | | | | | | | | | | | Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`.
* | Merge conflicts solved and cleaning in Asmgenproof after expansionLéo Gourdin2021-03-021-146/+18
| |
* | [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proofLéo Gourdin2021-02-111-0/+8
| |
* | [Admitted checker] Checker expansion for reg Ocmp (without scratch)Léo Gourdin2021-02-101-7/+7
| |
* | cond and branches expandedLéo Gourdin2021-02-061-8/+20
| |
* | All Ocmp expanded in RTLLéo Gourdin2021-02-031-3/+3
| |
* | Ccomp for longLéo Gourdin2021-02-031-3/+7
| |
* | Ccompu expansionLéo Gourdin2021-02-021-0/+1
| |
* | Expansion of Ccompimm in RTL [Admitted checker]Léo Gourdin2021-02-021-0/+3
| |
* | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-2/+2
|\ \
| * | 64-bit signed division by two codeDavid Monniaux2020-01-141-1/+1
| | |
| * | rv32: 3-instruction signed divide-by-two sequence (as opposed to 4)David Monniaux2020-01-141-1/+1
| |/
* / fix for Risc-VDavid Monniaux2019-09-071-1/+7
|/
* Model external calls as destroying all caller-save registersXavier Leroy2018-06-011-2/+2
| | | | | | | | | | The semantics of external function calls in LTL, Linear, Mach and Asm now consider that all caller-save registers are set to Vundef by the call. This models that fact that the external function can modify those registers arbitrarily. Update the proofs of the Allocation, Tunneling, Stacking and Asmgen passes accordingly.
* 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.
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+1028
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 11:19:19 +0000