Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge branch 'master' into merge_master_8.13.1 | Sylvain Boulmé | 2021-03-23 | 1 | -1/+1 |
|\ | | | | | | | | | | | | | | | | | 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 Leroy | 2020-12-29 | 1 | -1/+1 |
| | | | | | | | | | | | | | | | | | | | | | | 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`. | ||||
* | | quick fixcomments | Léo Gourdin | 2021-02-16 | 1 | -1/+1 |
| | | |||||
* | | Adding fp stores pair | Léo Gourdin | 2021-01-20 | 1 | -3/+4 |
| | | |||||
* | | Adding fp loads pair | Léo Gourdin | 2021-01-20 | 1 | -7/+20 |
| | | |||||
* | | Val_cmp* -> Val.mxcmp* | Sylvain Boulmé | 2021-01-07 | 1 | -60/+6 |
| | | |||||
* | | Merge branch 'kvx-work' into aarch64-peephole | Sylvain Boulmé | 2020-12-17 | 1 | -2/+8 |
|\| | |||||
| * | AArch64 modeling of registers destroyed by pseudo-instructions | Xavier Leroy | 2020-12-06 | 1 | -4/+4 |
| | | | | | | | | | | | | Pfmovimms, Pfmovimmd destroy X16 Pbtbl preserves X17 Inlined built-in functions destroy X16 and X30 | ||||
| * | Added implementation for fmin/fmax for aarch64. | Bernhard Schommer | 2020-11-06 | 1 | -0/+4 |
| | | | | | | | | | | The two built-in function map to the fmax and fmin instruction. Bug 30035 | ||||
| * | AArch64 implementation of __builtin_ctz* | Xavier Leroy | 2020-07-27 | 1 | -0/+2 |
| | | | | | | | | Using the "rbit" instruction (reverse bits). | ||||
* | | Big improvment in peephole, changing LDP/STP semantics | Léo Gourdin | 2020-12-10 | 1 | -20/+20 |
| | | |||||
* | | a first working draft on ldp/stp peephole | Léo Gourdin | 2020-12-04 | 1 | -18/+46 |
| | | |||||
* | | Adding semantics for Pldp | Léo Gourdin | 2020-12-02 | 1 | -3/+27 |
| | | | | | | This commit prepare the backend for a peephole optimization in Asmblock. | ||||
* | | Proof of Pfmovimm fine tuned OK, moving float checks in Asm | Léo Gourdin | 2020-11-26 | 1 | -3/+41 |
| | | | | | | Also some simplifications in Asmblockdeps | ||||
* | | fix the semantics ? | Sylvain Boulmé | 2020-11-18 | 1 | -2/+2 |
| | | |||||
* | | Preparation for postpass in aarch64 and refactoring | Léo Gourdin | 2020-11-02 | 1 | -10/+10 |
| | | |||||
* | | aarch64 compiles again (but ccomp generates incorrect assembly) | Sylvain Boulmé | 2020-10-23 | 1 | -9/+530 |
| | | |||||
* | | Prove exec_body_dont_move_PC | Justus Fasse | 2020-08-18 | 1 | -4/+4 |
| | | | | | | | | | | | | Modify Asmblock.preg to combine iregsp and freg into dreg (dreg might be a misnomer since not all iregs are data regs) TODO: Adjust names of PArithP, PArithPP and the like | ||||
* | | Add dynamically checked assumption to simplify Asmgenproof | Justus Fasse | 2020-07-21 | 1 | -1/+1 |
| | | | | | | | | | | Previously Asmblock.label_pos and Asm.label_pos could point to different memory location for the same label. | ||||
* | | aarch64/Asm: Fix `Error: Pattern "PC" is redundant in this clause.` | Justus Fasse | 2020-07-06 | 1 | -1/+1 |
| | | | | | | | | Introduced by changed definition of preg in aarch64/Asmblock | ||||
* | | [WIP: Coq compilation broken] Stub for Asmgen | Sylvain Boulmé | 2020-06-21 | 1 | -498/+32 |
|/ | |||||
* | Revert "Remove `__builtin_nop` for some architectures. (#208)" | Bernhard Schommer | 2020-01-03 | 1 | -1/+3 |
| | | | | This reverts commit 4dfcd7d4be18e8bc437ca170782212aa06635a95. | ||||
* | Remove `__builtin_nop` for some architectures. (#208) | Bernhard Schommer | 2019-12-21 | 1 | -3/+1 |
| | | | | | | | The `__builtin_nop` function is documented only for PowerPC. It was added to the other architectures by copy paste, but has no known uses. So, remove `__builtin_nop` from all architectures but PowerPC. | ||||
* | AArch64 port | Xavier Leroy | 2019-08-08 | 1 | -0/+1312 |
This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode. |