aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/Asmgenproof1.v
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into towards_3.10David Monniaux2021-09-241-2/+2
|\
| * Int.sign_ext_shr_shl: weaker hypothesisXavier Leroy2021-08-221-2/+2
| | | | | | | | | | | | Works also for sign_ext 32. ARM, RISC-V: adapt Asmgenproof1 accordingly
* | omega -> liaDavid Monniaux2021-06-081-8/+8
| |
* | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-011-86/+751
|\ \
| * | Adding both RV expansion methods in kvx-workLéo Gourdin2021-05-191-24/+895
| | |
| * | Removing expansions from AsmgenLéo Gourdin2021-04-091-895/+24
| | |
| * | Removing addptrofs draft, next will be mergingLéo Gourdin2021-04-091-3/+2
| | |
| * | Important commit on expansions' mini CSE, and a draft for addptrofsLéo Gourdin2021-04-061-10/+46
| | |
| * | a more general way to manage special registers before introducing SPLéo Gourdin2021-03-301-69/+73
| | |
| * | Now a more general way to perform imm operationsLéo Gourdin2021-03-301-1/+6
| | |
| * | Adding more expansions, improving miniCSE, and tuning prepassLéo Gourdin2021-03-261-4/+8
| | |
| * | Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexpLéo Gourdin2021-03-061-3/+3
| |\ \
| | * | Adding a mini CSE pass in the expansion oracleLéo Gourdin2021-03-061-3/+3
| | | |
| * | | Asmcondexp branche useful to benchmark expansionsLéo Gourdin2021-03-021-78/+695
| |/ /
* | | fix riscv merge?Léo Gourdin2021-03-291-0/+965
| | |
* | | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-965/+0
|\ \ \ | |/ / |/| / | |/ | | | | | | | | | | 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
| * Qualify `Hint` as `Global Hint` where appropriateXavier Leroy2021-01-211-1/+1
| | | | | | | | | | | | | | This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`.
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-10/+10
| | | | | | | | | | | | | | | | | | | | | | 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-747/+87
| |
* | Merge remote-tracking branch 'origin/riscV-cmov' into riscv-workLéo Gourdin2021-03-021-0/+48
|\ \
| * | asmgen OselectlDavid Monniaux2021-02-021-0/+4
| | |
* | | Proof of fsval condition cmp okLéo Gourdin2021-03-011-4/+5
| | |
* | | Proof of Ocmp expansions without immediate and some drafts in commentLéo Gourdin2021-02-181-1/+1
| | |
* | | [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proofLéo Gourdin2021-02-111-5/+64
| | |
* | | [Admitted checker] Checker expansion for reg Ocmp (without scratch)Léo Gourdin2021-02-101-8/+8
| | |
* | | cond and branches expandedLéo Gourdin2021-02-061-10/+71
| | |
* | | All Ocmp expanded in RTLLéo Gourdin2021-02-031-6/+6
| | |
* | | Ccomp for longLéo Gourdin2021-02-031-6/+8
| | |
* | | Ccompu expansionLéo Gourdin2021-02-021-161/+154
| | |
* | | Expansion of Ccompimm in RTL [Admitted checker]Léo Gourdin2021-02-021-0/+11
|/ /
* | maketotal mod & divDavid Monniaux2020-09-211-2/+43
| |
* | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-workDavid Monniaux2020-01-151-16/+29
|\ \
| * | 64-bit signed division by two codeDavid Monniaux2020-01-141-8/+15
| | |
| * | rv32: 3-instruction signed divide-by-two sequence (as opposed to 4)David Monniaux2020-01-141-8/+14
| |/
* | Merge tag 'v3.6_mppa_2019-09-20' of ↵David Monniaux2019-09-201-20/+4
|\| | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load
| * Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-4/+4
| | | | | | Some changes were not correctly propagated to all architectures.
| * AArch64 portXavier Leroy2019-08-081-16/+0
| | | | | | | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* | fix for Risc-VDavid Monniaux2019-09-071-3/+4
|/
* Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-8/+8
| | | | | | | | | | The module Integers.Make contained lots of definitions and theorems about Z integers that were independent of the word size. These definitions and theorems are useful outside Integers.Make, but it felt unnatural to fetch them from modules Int or Int64. This commit moves the word-size-independent definitions and theorems to a new module, lib/Zbits.v, and fixes their uses in the code base.
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+1411
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:34:20 +0000