aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/SelectOpproof.v
Commit message (Collapse)AuthorAgeFilesLines
* fix riscv merge?Léo Gourdin2021-03-291-0/+1093
|
* Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-1093/+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
| * Replace `omega` tactic with `lia`Xavier Leroy2020-12-291-17/+17
| | | | | | | | | | | | | | | | | | | | | | 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`.
* | detect redundant cmovDavid Monniaux2021-02-021-0/+22
| |
* | Cmov TsingleDavid Monniaux2021-02-021-33/+26
| |
* | PselectdDavid Monniaux2021-02-021-0/+19
| |
* | cmov on integersDavid Monniaux2021-02-021-9/+80
| |
* | begin synthesizing selectDavid Monniaux2021-02-021-1/+11
| |
* | adding builtinsDavid Monniaux2021-02-011-1/+4
| |
* | risc-V now without trapping instructionsDavid Monniaux2020-09-211-0/+8
| |
* | maketotal mod & divDavid Monniaux2020-09-211-32/+30
| |
* | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-09-201-2/+2
|\| | | | | | | mppa-work-upstream-merge
| * Fix compile for architectures other than AArch64 (#192)Bernhard Schommer2019-08-171-2/+2
| | | | | | Some changes were not correctly propagated to all architectures.
* | helpers broke compilationDavid Monniaux2019-07-191-4/+1
| |
* | Merge branch 'master' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-07-191-12/+19
|\| | | | | | | mppa-work-upstream-merge
| * Give formal semantics to some built-in functions and run-time functionsXavier Leroy2019-07-171-12/+16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This commit adds mechanisms to - recognize certain built-in and run-time functions by name and signature; - associate semantics to these functions, as a partial function from list of values to values; - interpret external calls to these functions according to this semantics (pure function from values to values, memory unchanged, no observable events in the trace); - external calls to unknown built-in and run-time functions remain interpreted as generating observable events and possibly changing memory, like before. The description of the built-ins is split into a target-independent part (in common/Builtins0.v) and a target-specific part (in $ARCH/Builtins1.v). Instruction selection uses the new mechanism in order to - recognize some built-in functions and turn them into operations of the target processor. Currently, this is done for __builtin_sel and __builtin_fabs; more to come. - remove the axioms about int64 helper functions from the standard library. More precisely, the behavior of these functions is still axiomatized, but now it is specified using the more general machinery introduced in this commit, rather than ad-hoc axioms in backend/SplitLongproof. The only built-ins currently described are __builtin_fsqrt (for all platforms) and __builtin_fmin / __builtin_fmax (for x86). More built-ins will be added later.
* | Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-031-2/+17
|\| | | | | | | mppa-if-conversion
| * Provide a default "select" operation for the RiscV portXavier Leroy2019-05-201-0/+14
| | | | | | | | | | No `Osel` operation for this port, so `SelectOp.select` always returns None.
| * Move Z definitions out of Integers and into ZbitsXavier Leroy2019-04-261-2/+3
| | | | | | | | | | | | | | | | | | | | 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 works again (32/64).David Monniaux2019-03-221-2/+27
|/
* Extend builtin arguments with a pointer addition operator, continuedXavier Leroy2017-07-061-6/+16
| | | | | | | | - Add support for PowerPC, with all addressing modes. - Add support for ARM, with "reg + ofs" addressing mode. - Add support for RISC-V, with the one addressing mode. - Constprop.v: forgot to recurse in BA_addptr - volatile4 test: more tests
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+915
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 04:01:14 +0000