aboutsummaryrefslogtreecommitdiffstats
path: root/runtime
Commit message (Collapse)AuthorAgeFilesLines
...
* 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
* Adapt to the two different calling conventions for floats.xleroy2014-05-026-0/+14
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2476 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* stdarg.h: assorted fixes for PowerPCxleroy2014-01-011-5/+5
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2397 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fine hair splitting depending on whether va_list is a scalar type (IA32, ↵xleroy2014-01-011-3/+3
| | | | | | ARM) or an array type (PowerPC). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2395 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Experimental support for <stdarg.h>, the GCC way. Works on IA32. To be ↵xleroy2014-01-014-1/+310
| | | | | | tested on PowerPC and ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2394 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* powerpc: faster implementation of long division modeled on that for IA32xleroy2013-07-035-70/+220
| | | | | | | | test: add one test (2^64-1) / (2^32+3) to exercise a special case of this long division. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2288 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Merge of the "princeton" branch:xleroy2013-06-161-0/+8
| | | | | | | | | | | | | | - Define type "block" as "positive" instead of "Z". - Strengthen mem_unchanged_on so that the permissions are identical, instead of possibly increasing. - Move mem_unchanged_on from Events to Memory.Mem. - Define it in terms of mem_contents rather than in terms of Mem.load. - ExportClight: try to name temporaries introduced by SimplExpr - SimplExpr: avoid reusing temporaries between different functions, instead, thread a single generator through all functions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2276 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Fix compilation of runtime system.xleroy2013-05-291-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2263 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Syntax errorsxleroy2013-05-062-31/+31
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2237 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Wrong pseudo-instrxleroy2013-05-061-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2236 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for in64 -> float conversions w/ correct rounding.xleroy2013-05-0610-7/+414
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2235 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* ia32/i64_dtou: wrong play on rounding modexleroy2013-05-058-52/+145
| | | | | | | | | arm, powerpc: expand shifts inline in dtos and dtou arm: branchless code for shl and shr test: more tests for double -> long long conversions. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2234 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Typos in commentsxleroy2013-04-302-3/+3
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2220 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-298-392/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2218 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-06-13 04:10:18 +0000