aboutsummaryrefslogtreecommitdiffstats
path: root/runtime
Commit message (Collapse)AuthorAgeFilesLines
* (#157) Fixing warning for desactivated afaddd builtin. No implementation yetCyril SIX2019-09-051-0/+6
|
* macros for fma() fmaf()David Monniaux2019-08-301-0/+2
|
* fmin/fmax/fminf/fmaxf non bien testésDavid Monniaux2019-08-291-0/+9
|
* merge upstream including fma fixesDavid Monniaux2019-08-2822-1870/+0
|
* Merge branch 'if-conversion' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-06-031-4/+4
|\ | | | | | | mppa-if-conversion
| * 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.
* | use all same exact include filesv3.5_k1c_1.2David Monniaux2019-06-031-15/+7
| |
* | added some include filesDavid Monniaux2019-05-292-0/+2
| |
* | more builtinsDavid Monniaux2019-05-291-0/+2
| |
* | fixes for COSDavid Monniaux2019-05-282-0/+12
| |
* | directly call float and double division from gcc lib instead of a stubDavid Monniaux2019-05-151-42/+0
| |
* | 32-bit modulo now uses sign extend then call to the 64-bit functionDavid Monniaux2019-05-131-23/+0
| |
* | we directly call 64-bit unsigned divisionDavid Monniaux2019-05-131-22/+0
| |
* | feclearexcept / fetestexceptDavid Monniaux2019-04-131-0/+15
| |
* | better #include handlingDavid Monniaux2019-04-121-1/+5
| |
* | workaround for non-standard C isfinite macro in math.hDavid Monniaux2019-04-122-1/+4
| |
* | simplification of the varargs procedure: they are leaf procedures, there is ↵David Monniaux2019-04-121-40/+1
| | | | | | | | no need to save $ra
* | __builtin_k1_acswapwDavid Monniaux2019-04-112-1/+12
| |
* | builtin acswapdDavid Monniaux2019-04-112-2/+16
| |
* | cleaner: put all the special types, defines etc. in one header fileDavid Monniaux2019-04-112-0/+14
| |
* | passage de structures en varargs (fonctionne avec une convention "passage ↵David Monniaux2019-03-221-0/+3
| | | | | | | | par référence" cohérente avec CompCert mais pas forcément avec gcc)
* | la division flottante fonctionneDavid Monniaux2019-03-202-1/+12
| |
* | les divisions entieres passentDavid Monniaux2019-03-203-0/+43
| |
* | sdiv worksDavid Monniaux2019-03-202-1/+15
| |
* | Added i64_shl and i64_shr to the runtime Makefile, needed by i64_dtosCyril SIX2019-03-191-1/+2
| |
* | Merge branch 'master' into mppa_postpassCyril SIX2019-03-132-1/+2
|\| | | | | | | | | | | Conflicts: .gitignore runtime/include/stdbool.h
| * <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
* | varargsDavid Monniaux2019-03-101-0/+2
| |
* | Float conversion fixes + some more conversionsCyril SIX2019-02-271-2/+4
| |
* | C99 7.16 mandates __bool_true_false_are_definedDavid Monniaux2019-01-301-1/+1
| |
* | Fixed div64 and mod64Cyril SIX2018-12-112-31/+1
| |
* | Finished implementation of va_arg + testing doneCyril SIX2018-11-302-1/+73
| |
* | Merge tag 'v3.4' into mppa_k1cCyril SIX2018-11-211-0/+9
|\| | | | | | | | | Conflicts: .gitignore
| * 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
* | Fixed MPPA runtimes not compilingCyril SIX2018-11-202-5/+8
| |
* | MPPA - Changed division to include the builtinCyril SIX2018-06-051-23/+2
| |
* | MPPA - div and mod, replaced gcc implementation by C files + ccompCyril SIX2018-05-2113-460/+29
| |
* | MPPA - Added modulo and division 64 bits. Non certifiedCyril SIX2018-05-2114-0/+595
|/ | | | | | | 32 bits version are not yet there. Right now the code is directly from libgcc, compiled with k1-gcc because of builtins.
* 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).
generated by cgit (git 2.34.1) at 2024-07-06 14:59:53 +0000