aboutsummaryrefslogtreecommitdiffstats
path: root/runtime
Commit message (Collapse)AuthorAgeFilesLines
* "macosx" is now called "macos"Xavier Leroy2021-01-184-4/+4
| | | | | The configure script still accepts "macosx" for backward compatibility, but every other part of CompCert now uses "macos".
* AArch64: macOS portXavier Leroy2020-12-262-4/+66
| | | | | This commit adds support for macOS (and probably iOS) running on AArch64 / ARM 64-bit / "Apple silicon" processors.
* Configure the correct archiver to build runtime/libcompcert.aXavier Leroy2020-12-241-1/+1
| | | | | | | | | - Use `${toolprefix}ar` instead of `ar` so as to match the choice of C compiler (as proposed by Michael Soegtrop in PR #380) - Use the Diab archiver `dar` if configured for powerpc-eabi-diab Closes: #380
* Support Cygwin 64 bitsXavier Leroy2020-10-055-28/+99
| | | | | | - Add support for the Win64 ABI to the x86_64 port - Update vararg support to handle Win64 conventions - Configure support for x86_64-cygwin64
* Double rounding error in int64->float32 conversions on PowerPC and ARMXavier Leroy2020-03-304-24/+22
| | | | | | | | | The "stof" and "utof" runtime functions contain a round-to-odd step that avoids double rounding. However, this step was incorrectly coded on PowerPC (stof and utof), PowerPC64 (utof), and ARM (stof), making round-to-odd ineffective and causing double rounding. Closes: #343
* AArch64 portXavier Leroy2019-08-083-0/+156
| | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* Prepend $(DESTDIR) to the installation target (#169)Bernhard Schommer2019-05-171-4/+4
| | | | | | | | Following the gnu Makefile Conventions the variable $(DESTDIR) should be prepended to all installation commands. This allows staged installs.
* <stddef.h>: define NULL with type void *Xavier Leroy2019-02-041-1/+1
| | | | | | | | | | | | | | ISO C2011 7.19 para 3 says "NULL, which expands to an implementation-defined null pointer constant" ISO C2011 6.3.2.3 para 3 says "An integer constant expression with the value 0, or such an expression cast to type void *, is called a null pointer constant." So, it seems NULL can be defined either as "0" or as "(void *) 0". However, the two definitions are not equivalent in the context of a call to a variadic or unprototyped function: passing 0 when the function expects a pointer value can go wrong if sizeof(int) != sizeof(void *). This commit changes the definition of NULL to the safer one: This is what GCC and Clang do in C mode; they use "#define NULL 0" for C++ only. Fixes issue #265
* <stdbool.h>: add missing macro __bool_true_false_are_definedXavier Leroy2019-02-041-0/+1
| | | | | | As specified in ISO C99 section 7.16 and C11 section 7.18. Fixes issue #266
* Define the C11 type max_align_t (#115)Bernhard Schommer2018-05-241-0/+9
| | | | | | | The definition is similar to that of gcc, however since we don't support long doubles out of the box and long doubles are doubles in compat mode we can directly define max_align_t to be long long. Bug 23380
* Take advantage of ARMv6T2/ARMv7 instructions even if not in Thumb2 mode (#203)Gergö Barany2017-09-181-0/+2
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * Clarify that ARMv6 is in fact ARMv6T2 The ARMv6 comes in two flavors depending on the version of the Thumb instruction set supported: ARMv6 for the original Thumb, ARMv6T2 for Thumb2. CompCert only supports Thumb2, so its ARMv6 architecture should really be called ARMv6T2. This makes a difference: the GNU assembler rejects most of the instructions CompCert generates for ARMv6 with "-mthumb" if the architecture is specified as ".arch armv6" as opposed to ".arch armv6t2". This patch fixes the architecture specification in the target printer and the internal name of the architecture. It does not change the configure script's flags to avoid breaking changes. * Always use ARM movw/movt to load large immediates These move-immediate instructions used to be only emitted in Thumb mode, not in ARM mode. As far as I understand ARM's documentation, these instructions are available in *both* modes in ARMv6T2 and above. This should cover all of CompCert's ARM targets. Tested for ARMv6 and ARMv7, both with and without Thumb2. The behavior is now identical to Clang, and the GNU assembler accepts these instructions in all configurations. * Separate ARMv6 and ARMv6T2; no movw/movt on ARMv6 - define separate architecture models for ARMv6 and ARMv6T2 - introduce `Archi.move_imm` parameter on ARM to identify models with `movw`/`movt` move-immediate instructions (all except ARMv6, in both ARM and Thumb mode) * Fixes for support for architectures with Thumb2 - rename relevant parameter to `Archi.thumb2_support` - on ARMv6 without Thumb2, silently accept -marm flag (but not -mthumb) - allow generation of `sbfx` in ARM mode if Thumb2 is supported
* Prefixed runtime functions.Bernhard Schommer2017-08-2557-208/+208
| | | | | | | The runtime functions are prefixed with compcert in order to avoid potential clashes with runtime/builtin functions of other compilers. Bug 22062
* Hybrid 64bit/32bit PowerPC portBernhard Schommer2017-05-0315-435/+200
| | | | | | | | | | | | | This commit adds code generation for 64bit PowerPC architectures which execute 32bit applications. The main difference to the normal 32bit PowerPC port is that it uses the available 64bit instructions instead of using the runtime library functions. However pointers are still 32bit and the 32bit calling convention is used. In order to use this port the target architecture must be either in Server execution mode or if in Embedded execution mode the high order 32 bits of GPRs must be implemented in 32-bit mode. Furthermore the operating system must preserve the high order 32 bits of GPRs.
* RISC-V vararg.S: a "sw" instruction should be "sptr"Xavier Leroy2017-04-291-1/+1
|
* RISC-V port and assorted changesXavier Leroy2017-04-2820-41/+205
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Change the syntax to gcc/clangs syntax.Bernhard Schommer2017-02-011-1/+1
| | | | | | This only means that there must be one identifier at the begining and then a designator. Bug 20765
* New version to support designators.Bernhard Schommer2017-01-241-1/+1
| | | | | | | | | The c standard allows member designators for offsetof. The current implementation works by recursively combining the offset of each of the member designators. For array access the size of the subtypes is multiplied by the index and for members the offset of the member is calculated. Bug 20765
* Implement offsetof via builtin.Bernhard Schommer2017-01-201-1/+1
| | | | | | | | | | | | The implementation of offsetof as macro in the form ((size_t) &((ty*) NULL)->member) has the problem that it cannot be used everywhere were an integer constant expression is allowed, for example in initiliazers of global variables and there is also no check for the case that member is of bitifield type. The new implementation adds a builtin function for this which is replaced by an integer constant during elaboration. Bug 20765
* powerpc/runtime: add commentsXavier Leroy2016-10-281-1/+2
|
* runtime/powerpc: remove useless files, add commentsXavier Leroy2016-10-282-140/+0
|
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵Xavier Leroy2016-10-2719-1/+3
| | | | | | | | | | | | -> x86/x86_32/x86_64 Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq. This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86. While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures. Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far).
* i64_smulh: revert to conditional branches instead of predicated insnsXavier Leroy2016-10-251-8/+8
| | | | "subslt" changes the flags, affecting the condition of the "sbclt" that follows.
* Update PowerPC port (not tested yet)Xavier Leroy2016-10-252-0/+144
|
* Update ARM port. Not tested yet.Xavier Leroy2016-10-253-0/+139
|
* x86-64 MacOS X supportXavier Leroy2016-10-111-1/+1
| | | | | - Avoid absolute addressing for labels, use RIP-relative addressing - Different, RIP-relative implementation of jump tables
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-048-0/+433
| | | | | | This trick was already implemented for 32-bit integer division and modulus. Here we extend it to the 64-bit case. For 32-bit target processors, the runtime library must implement 64-bit multiply-high (signed and unsigned). Tentative implementations are provided for IA32 and PowerPC, but need testing.
* Support for 64-bit architectures: x86 in 64-bit modeXavier Leroy2016-10-016-0/+404
| | | | | | | | | | | | | | | | | | | This commit enriches the IA32 port so that it supports x86 processors in 64-bit mode as well as in 32-bit mode, depending on the value of Archi.ptr64, which itself is set from the configuration model. To activate x86-64 bit support, configure with "x86_64-linux". Main steps: - Enrich Op.v and Asm.v with 64-bit operations - SelectLong: in 64-bit mode, use 64-bit operations directly; in 32-bit mode, fall back on the old implementation based on pairs of 32-bit integers - Conventions1: support x86-64 ABI in addition to the 32-bit ABI. - Add support for the new 64-bit operations everywhere. - runtime/x86_64: implementation of the supporting library appropriate for x86 in 64-bit mode To do: - More optimizations are possible on 64-bit integer arithmetic operations. - Could add new chunks to load, say, an unsigned byte into a 64-bit long (currently we load as a 32-bit int then zero-extend). - Implements the wrong ABI for struct passing.
* Implement support for big endian arm targets.Bernhard Schommer2016-08-0516-214/+254
| | | | | | | | 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
* Added iso646 header for alternate spellings.Bernhard Schommer2016-04-061-0/+49
| | | | | | | The iso646 header defines some macros that expand to common operators. Both clang and gcc ship with them and they are required by the standard. Bug 18645.
* Added the _Noreturn keyword.Bernhard Schommer2016-03-233-1/+82
| | | | | | | | CompCert now recognizes the C11 _Noreturn function specifier and emits a simple warning for functions declared _Noreturn containing a return statement. Also the stdnoreturn header and additionally the stdalign header are added. Bug 18541
* Include fix for wint_t gcc problem.Bernhard Schommer2016-01-211-12/+16
| | | | | | Gcc defines wint_t in the stddef header (even if it is not stanadard) and additionally defines it if stddef is reincluded. The fix now defines it before stddef is checked for reinclusion.
* Libcompcert should be compiled in thumb mode for armv7m.Bernhard Schommer2015-12-181-2/+2
| | | | | | Libcompcert was defined in thumb mode for armv7r but it should be compild in thumb mode for armv7m. Bug 17808.
* More gcc/newlib compatibility code.Bernhard Schommer2015-12-111-2/+13
| | | | | | | | | | Some newlib headers use the __extension__ keyword which suppresses warnings for gcc extensions in strict mode. CompCert now ignores this keyword for the gnu backends. Also it seems that stddef of the gcc defines wint_t even though it should not. However some libs rely on this. So wint_t is now defined in CompCert's stddef header. Bug 17613.
* VPATH setting for PowerPCXavier Leroy2015-09-131-1/+9
|
* Wrong syntax in fcmp.Xavier Leroy2015-09-131-2/+2
|
* PowerPC 64 bits: alternate, more efficient implementations of int64 operations.Xavier Leroy2015-09-1213-2/+681
|
* Also test if the __VA_LIST macro is defined to avoid problems with the ↵Bernhard Schommer2015-07-091-2/+8
| | | | typedefs in stdio, etc. for the diab compiler.
* Removed brackets around ty in macro of offestof.Bernhard Schommer2015-07-071-1/+1
|
* Diab defines w_char to be unsigned short.Bernhard Schommer2015-07-071-1/+1
|
* Better define the __GNUC__ macro which avoids the inclusion of va_list ↵Bernhard Schommer2015-07-071-0/+4
| | | | header and set the __VA_LIST macro if it is not defined.
* Make also the wchar definition diab compatible.Bernhard Schommer2015-06-261-0/+15
|
* Added diab specific macros for stddef to avoid redefinition of size_t.Bernhard Schommer2015-06-261-0/+9
|
* Typo in #ifndef guard.Xavier Leroy2015-05-091-1/+1
|
* Improve compatibility with MacOS X.Xavier Leroy2015-04-261-0/+3
|
* Provide and use compiler-dependent standard headers.Xavier Leroy2015-04-256-5/+312
| | | | | | | | | | | | This branch provides implementations of the following standard headers: <float.h> <stdarg.h> <stdbool.h> <stddef.h> <varargs.h> These are the headers that are provided by GCC and Clang, as opposed to being provided by Glibc and similar C standard libraries. Configuration flag "-no-standard-headers" deactivates the installation and use of these headers. Lightly tested so far (IA32 Linux).
* Support va_arg for vararg arguments of composite (struct/union) types.Xavier Leroy2015-03-202-0/+19
| | | | Now for IA32 and PowerPC as well.
* Support va_arg for vararg arguments of composite (struct/union) types.Xavier Leroy2015-03-201-0/+12
| | | | ARM is done, IA32 and PowerPC remain to be updated.
* C reference implementation of the int64 helper functions.Xavier Leroy2015-02-1418-8/+928
| | | | In test_int64.c: don't test FP->int64 conversions when the FP argument is out of range.
* configure: distinguish between ABI and processor model.xleroy2014-07-2910-12/+25
| | | | | | | | ARM: various tweaks, incl. support for SDIV and UDIV insns when available. test/regression/funptr2.c: Thumb does weird things with <function ptr>+1. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2555 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ARM port: add support for Thumb2. To be tested.xleroy2014-07-2717-295/+350
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2549 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-02 19:26:06 +0000