Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | omega -> lia | David Monniaux | 2021-06-08 | 1 | -8/+8 |
| | |||||
* | Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1 | Cyril SIX | 2021-06-01 | 1 | -86/+751 |
|\ | |||||
| * | Adding both RV expansion methods in kvx-work | Léo Gourdin | 2021-05-19 | 1 | -24/+895 |
| | | |||||
| * | Removing expansions from Asmgen | Léo Gourdin | 2021-04-09 | 1 | -895/+24 |
| | | |||||
| * | Removing addptrofs draft, next will be merging | Léo Gourdin | 2021-04-09 | 1 | -3/+2 |
| | | |||||
| * | Important commit on expansions' mini CSE, and a draft for addptrofs | Léo Gourdin | 2021-04-06 | 1 | -10/+46 |
| | | |||||
| * | a more general way to manage special registers before introducing SP | Léo Gourdin | 2021-03-30 | 1 | -69/+73 |
| | | |||||
| * | Now a more general way to perform imm operations | Léo Gourdin | 2021-03-30 | 1 | -1/+6 |
| | | |||||
| * | Adding more expansions, improving miniCSE, and tuning prepass | Léo Gourdin | 2021-03-26 | 1 | -4/+8 |
| | | |||||
| * | Merge remote-tracking branch 'origin/riscv-work' into riscv-work-fpinit-stillexp | Léo Gourdin | 2021-03-06 | 1 | -3/+3 |
| |\ | |||||
| | * | Adding a mini CSE pass in the expansion oracle | Léo Gourdin | 2021-03-06 | 1 | -3/+3 |
| | | | |||||
| * | | Asmcondexp branche useful to benchmark expansions | Léo Gourdin | 2021-03-02 | 1 | -78/+695 |
| |/ | |||||
* | | fix riscv merge? | Léo Gourdin | 2021-03-29 | 1 | -0/+965 |
| | | |||||
* | | Merge branch 'master' into merge_master_8.13.1 | Sylvain Boulmé | 2021-03-23 | 1 | -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 appropriate | Xavier Leroy | 2021-01-21 | 1 | -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 Leroy | 2020-12-29 | 1 | -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 expansion | Léo Gourdin | 2021-03-02 | 1 | -747/+87 |
| | | |||||
* | | Merge remote-tracking branch 'origin/riscV-cmov' into riscv-work | Léo Gourdin | 2021-03-02 | 1 | -0/+48 |
|\ \ | |||||
| * | | asmgen Oselectl | David Monniaux | 2021-02-02 | 1 | -0/+4 |
| | | | |||||
* | | | Proof of fsval condition cmp ok | Léo Gourdin | 2021-03-01 | 1 | -4/+5 |
| | | | |||||
* | | | Proof of Ocmp expansions without immediate and some drafts in comment | Léo Gourdin | 2021-02-18 | 1 | -1/+1 |
| | | | |||||
* | | | [Admitted checker] Duplicating Asm Ceq/Cne and draft checker proof | Léo Gourdin | 2021-02-11 | 1 | -5/+64 |
| | | | |||||
* | | | [Admitted checker] Checker expansion for reg Ocmp (without scratch) | Léo Gourdin | 2021-02-10 | 1 | -8/+8 |
| | | | |||||
* | | | cond and branches expanded | Léo Gourdin | 2021-02-06 | 1 | -10/+71 |
| | | | |||||
* | | | All Ocmp expanded in RTL | Léo Gourdin | 2021-02-03 | 1 | -6/+6 |
| | | | |||||
* | | | Ccomp for long | Léo Gourdin | 2021-02-03 | 1 | -6/+8 |
| | | | |||||
* | | | Ccompu expansion | Léo Gourdin | 2021-02-02 | 1 | -161/+154 |
| | | | |||||
* | | | Expansion of Ccompimm in RTL [Admitted checker] | Léo Gourdin | 2021-02-02 | 1 | -0/+11 |
|/ / | |||||
* | | maketotal mod & div | David Monniaux | 2020-09-21 | 1 | -2/+43 |
| | | |||||
* | | Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-work | David Monniaux | 2020-01-15 | 1 | -16/+29 |
|\ \ | |||||
| * | | 64-bit signed division by two code | David Monniaux | 2020-01-14 | 1 | -8/+15 |
| | | | |||||
| * | | rv32: 3-instruction signed divide-by-two sequence (as opposed to 4) | David Monniaux | 2020-01-14 | 1 | -8/+14 |
| |/ | |||||
* | | Merge tag 'v3.6_mppa_2019-09-20' of ↵ | David Monniaux | 2019-09-20 | 1 | -20/+4 |
|\| | | | | | | | gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-non-trapping-load | ||||
| * | Fix compile for architectures other than AArch64 (#192) | Bernhard Schommer | 2019-08-17 | 1 | -4/+4 |
| | | | | | | Some changes were not correctly propagated to all architectures. | ||||
| * | AArch64 port | Xavier Leroy | 2019-08-08 | 1 | -16/+0 |
| | | | | | | | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode. | ||||
* | | fix for Risc-V | David Monniaux | 2019-09-07 | 1 | -3/+4 |
|/ | |||||
* | Move Z definitions out of Integers and into Zbits | Xavier Leroy | 2019-04-26 | 1 | -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 changes | Xavier Leroy | 2017-04-28 | 1 | -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. |