aboutsummaryrefslogtreecommitdiffstats
path: root/runtime/Makefile
Commit message (Collapse)AuthorAgeFilesLines
* Merge branch 'master' of https://github.com/AbsInt/CompCert into kvx-workDavid Monniaux2021-06-111-0/+2
|\ | | | | | | fix for comments on x86-64 MacOS
| * 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
* | fix need for kvx-elfDavid Monniaux2020-10-021-5/+1
| |
* | Using kvx-elf-ar instead of arCyril SIX2020-05-291-1/+7
| |
* | k1c -> kvx changesDavid Monniaux2020-05-261-4/+4
| |
* | Merge remote-tracking branch 'origin/mppa-fast-div' into mppa-featuresDavid Monniaux2020-04-201-4/+4
|\ \
| * | seems like fixed linking tests?!David Monniaux2020-04-201-1/+1
| | |
| * | Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-divDavid Monniaux2020-04-201-4/+6
| |\ \ | | | | | | | | | | | | (unfinished)
| * | | arranging for selection of divisor as optionDavid Monniaux2019-05-291-2/+3
| | | |
| * | | new routines for 32-bit divisionDavid Monniaux2019-05-211-3/+2
| | | |
* | | | do not print debug stuffDavid Monniaux2020-04-201-1/+1
| | | |
* | | | profiling still crashes on Aarch64David Monniaux2020-04-101-1/+1
| | | |
* | | | library support for writing profiling information to filesDavid Monniaux2020-04-081-0/+2
| |/ / |/| |
* | | Merge tag 'v3.6' of https://github.com/AbsInt/CompCert into ↵David Monniaux2019-09-201-0/+2
|\ \ \ | | |/ | |/| | | | mppa-work-upstream-merge
| * | AArch64 portXavier Leroy2019-08-081-0/+2
| | | | | | | | | | | | | | | This commit adds a back-end for the AArch64 architecture, namely ARMv8 in 64-bit mode.
* | | 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.
* | workaround for non-standard C isfinite macro in math.hDavid Monniaux2019-04-121-1/+1
| |
* | cleaner: put all the special types, defines etc. in one header fileDavid Monniaux2019-04-111-0/+3
| |
* | Added i64_shl and i64_shr to the runtime Makefile, needed by i64_dtosCyril SIX2019-03-191-1/+2
| |
* | Float conversion fixes + some more conversionsCyril SIX2019-02-271-2/+4
| |
* | Finished implementation of va_arg + testing doneCyril SIX2018-11-301-1/+1
| |
* | Fixed MPPA runtimes not compilingCyril SIX2018-11-201-3/+1
| |
* | MPPA - Added modulo and division 64 bits. Non certifiedCyril SIX2018-05-211-0/+5
|/ | | | | | | 32 bits version are not yet there. Right now the code is directly from libgcc, compiled with k1-gcc because of builtins.
* Prefixed runtime functions.Bernhard Schommer2017-08-251-2/+2
| | | | | | | 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-031-8/+10
| | | | | | | | | | | | | 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 port and assorted changesXavier Leroy2017-04-281-1/+12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 ↵Xavier Leroy2016-10-271-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).
* Turn 64-bit integer division and modulus by constants into multiply-highXavier Leroy2016-10-041-0/+1
| | | | | | 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-011-0/+13
| | | | | | | | | | | | | | | | | | | 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-051-1/+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
* Added the _Noreturn keyword.Bernhard Schommer2016-03-231-1/+2
| | | | | | | | 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
* VPATH setting for PowerPCXavier Leroy2015-09-131-1/+9
|
* PowerPC 64 bits: alternate, more efficient implementations of int64 operations.Xavier Leroy2015-09-121-2/+4
|
* Provide and use compiler-dependent standard headers.Xavier Leroy2015-04-251-5/+14
| | | | | | | | | | | | 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).
* C reference implementation of the int64 helper functions.Xavier Leroy2015-02-141-1/+1
| | | | 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-291-1/+1
| | | | | | | | 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
* Experimental support for <stdarg.h>, the GCC way. Works on IA32. To be ↵xleroy2014-01-011-1/+2
| | | | | | tested on PowerPC and ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2394 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
* Support for in64 -> float conversions w/ correct rounding.xleroy2013-05-061-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2235 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Expand 64-bit integer comparisons into 32-bit integer comparisons.xleroy2013-04-291-2/+2
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2218 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Make ia32/ code more portable across systems.xleroy2013-04-231-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2214 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Split arch/int64.s into one file per function.xleroy2013-04-201-1/+6
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2206 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Configuring the assembler used for the runtime libxleroy2013-04-201-1/+1
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2205 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Big merge of the newregalloc-int64 branch. Lots of changes in two directions:xleroy2013-04-201-10/+18
| | | | | | | | | 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Support for indirect symbols under MacOS X (final).xleroy2012-07-141-4/+4
| | | | | | | Remove stdio hack in runtime/ git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1979 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Simplified stdlib wrapper; use it only under MacOS Xxleroy2010-09-041-3/+11
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1502 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Compilo C, preprocesseur, assembleur sont determines par configure et mis ↵xleroy2008-04-191-2/+1
| | | | | | dans Makefile.config git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@622 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
* Ajout et utilisation de caml/Driver.ml. Ajout ./configure. Revu Makefilesxleroy2007-08-061-0/+7
| | | | git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@387 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
generated by cgit (git 2.34.1) at 2024-05-20 10:27:28 +0000