aboutsummaryrefslogtreecommitdiffstats
path: root/cparser/Machine.mli
Commit message (Collapse)AuthorAgeFilesLines
* Add target ELFCyril SIX2021-06-011-0/+1
|
* Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-011-1/+2
|\
| * Adding distinction between kvx-cos and kvx-mbr (for trapping loads)Cyril SIX2021-04-131-1/+2
| |
* | [BROKEN] Merge with v3.9 : something broken for __builtin_expect in ↵Cyril SIX2021-06-011-4/+5
| | | | | | | | cfrontend/C2C.ml
* | Merge branch 'master' into merge_master_8.13.1Sylvain Boulmé2021-03-231-1/+2
|\ \ | |/ |/| | | | | | | | | | | | | 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
| * "macosx" is now called "macos"Xavier Leroy2021-01-181-1/+1
| | | | | | | | | | The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos".
| * AArch64: macOS portXavier Leroy2020-12-261-0/+1
| | | | | | | | | | This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors.
* | Turning loads into non-trapping when necessaryCyril SIX2020-12-151-0/+1
| |
* | k1c -> kvx changesDavid Monniaux2020-05-261-1/+1
| |
* | [regression to check!] Merge tag 'v3.6' into mppa-workCyril SIX2019-10-161-0/+1
|\| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Conflicts: .gitignore backend/Lineartyping.v common/Values.v configure cparser/Machine.ml cparser/Machine.mli driver/Configuration.ml driver/Frontend.ml runtime/Makefile test/c/Makefile test/c/aes.c test/compression/Makefile test/regression/Makefile test/regression/extasm.c test/regression/floats-basics.c test/regression/floats.c Note : test/regression should be checked, didn't test it yet
| * AArch64 portXavier Leroy2019-08-081-0/+1
| | | | | | | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* | Tackling struct passing by value for the future K1C ABICyril SIX2019-10-141-0/+1
| |
* | Merge tag 'v3.4' into mppa_k1cCyril SIX2018-11-211-0/+4
|\| | | | | | | | | Conflicts: .gitignore
| * Add sizeof_reg and new Machine configurations (#129)Bernhard Schommer2018-08-201-0/+4
| | | | | | | | | | | | | | | | | | | | | | | | | | Since the size of integer registers is not identical to the size of pointers for the ppc64 and e5500 model the check for register pairs in ExtendedAsm does not work correctly. In order to avoid this a new field sizeof_intreg is introduced in the Machine configuration which describes the size of integer registers. New configurations for the ppc64 and e5500 model are added and used. Bug 24273
* | Hook for MPPA_K1c (generates Risc-V code for now)Cyril SIX2018-04-041-0/+1
|/
* Move struct passing/return style to Machine.Bernhard Schommer2018-02-161-1/+16
| | | | | | Since the used configuration for passing and returning values struct values is pretty much static it can be hardwired into the machine settings.
* RISC-V port and assorted changesXavier Leroy2017-04-281-0/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Implement support for big endian arm targets.Bernhard Schommer2016-08-051-0/+1
| | | | | | | | Adds support for the big endian arm targets by making the target endianess flag configurable, adding support for the big endian calling conventions, rewriting memory access patterns and adding big endian versions of the runtime functions. Bug 19418
* Diab defines w_char to be unsigned short.Bernhard Schommer2015-07-071-0/+1
|
* Improvements in the StructReturn transformation (ABI conformance for passing ↵Xavier Leroy2015-03-201-9/+1
| | | | | | | | composites). - Implement the "1/2/4/8" composite return policy, used by IA32/MacOS X and IA32/BSD. - Move the default passing conventions from Machine.ml to compcert.ini, making it easier to test the various conventions. - More comprehensive interoperability test in regression/interop1.c.
* Improve performance and configurability for the StructReturn pass.Xavier Leroy2015-03-141-0/+1
| | | | | | | | configure: special ABI value for IA32/MacOSX and PowerPC/Linux cparser/Machine: special config for PowerPC/Linux cparser/StructReturn: generate better code for return-as-int driver/Clflags, driver/Driver: add options -fstruct-return=<convention> and -fstruct-passing=<convention> to simplify testing
* ABI compatibility for struct/union function arguments passed by value.Xavier Leroy2015-01-271-3/+16
| | | | | | | | | | The passing of struct/union arguments by value implemented in the verified part of CompCert is not compatible with the ARM, PowerPC and x86 ABI. Here we enrich the StructReturn source-to-source emulation pass so that it implements the calling conventions defined in these ABIs. Plus: for x86, implement the returning of struct/union results by value in a way compatible with the ABI.
* PR#6: fix handling of wchar_t and assignments from wide string literals.Xavier Leroy2014-12-301-0/+2
| | | | | | | | | | - cparser/Machine indicates whether wchar_t is signed or not (it is signed int in Linux and BSD, but unsigned short in Win32) - The type of a wide string literal is "wchar_t *" if the typedef "wchar_t" exists in the environment (e.g. after #include <stddef.h>). Only if wchar_t is not defined do we use the default from Machine. - Permit initialization of any integer array from a wide string literal, not just an array of wchar_t.
* Hack StructReturn to better adhere to PowerPC and ARM calling conventions.xleroy2013-12-201-1/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2382 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Revert suppression of __builtin_{read,write}_reversed for x86 and ARM,xleroy2013-04-291-0/+1
| | | | | | | | for compatibility with earlier CompCert versions. But don't use them in PackedStructs. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2216 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* cparser/*: refactoring of the expansion of read-modify-write operatorsxleroy2011-11-261-1/+1
| | | | | | | | | cparser/PackedStructs: treat r-m-w operations over byte-swapped fields cparser/PackedStructs: allow static initialization of packed structs test/regression: more packedstruct tests git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1738 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Bitfields: MSB-to-LSB in addition to LSB-to-MSBxleroy2011-03-101-2/+9
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1600 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Switching to the new C parser/elaborator/simplifierxleroy2010-03-031-0/+51
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1269 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-05-19 21:54:49 +0000