diff options
author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-04-28 15:56:59 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-04-28 16:05:51 +0200 |
commit | f642817f0dc761e51c3bd362f75b0068a8d4b0c8 (patch) | |
tree | b5830bb772611d2271c4b7d26f162d5c200dd788 /runtime | |
parent | 2fbdb0c45f0913b9fd8e95606c525fc5bfb3bc6d (diff) | |
download | compcert-kvx-f642817f0dc761e51c3bd362f75b0068a8d4b0c8.tar.gz compcert-kvx-f642817f0dc761e51c3bd362f75b0068a8d4b0c8.zip |
RISC-V port and assorted changes
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.
Diffstat (limited to 'runtime')
-rw-r--r-- | runtime/Makefile | 13 | ||||
-rw-r--r-- | runtime/c/i64.h | 10 | ||||
-rw-r--r-- | runtime/c/i64_dtos.c | 6 | ||||
-rw-r--r-- | runtime/c/i64_dtou.c | 6 | ||||
-rw-r--r-- | runtime/c/i64_sar.c | 2 | ||||
-rw-r--r-- | runtime/c/i64_sdiv.c | 4 | ||||
-rw-r--r-- | runtime/c/i64_shl.c | 2 | ||||
-rw-r--r-- | runtime/c/i64_shr.c | 2 | ||||
-rw-r--r-- | runtime/c/i64_smod.c | 4 | ||||
-rw-r--r-- | runtime/c/i64_smulh.c | 4 | ||||
-rw-r--r-- | runtime/c/i64_stod.c | 2 | ||||
-rw-r--r-- | runtime/c/i64_stof.c | 2 | ||||
-rw-r--r-- | runtime/c/i64_udiv.c | 4 | ||||
-rw-r--r-- | runtime/c/i64_udivmod.c | 22 | ||||
-rw-r--r-- | runtime/c/i64_umod.c | 4 | ||||
-rw-r--r-- | runtime/c/i64_umulh.c | 2 | ||||
-rw-r--r-- | runtime/c/i64_utod.c | 2 | ||||
-rw-r--r-- | runtime/c/i64_utof.c | 2 | ||||
-rw-r--r-- | runtime/riscV/sysdeps.h | 63 | ||||
-rw-r--r-- | runtime/riscV/vararg.S | 90 |
20 files changed, 205 insertions, 41 deletions
diff --git a/runtime/Makefile b/runtime/Makefile index 641c9fdc..b819991d 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -52,8 +52,19 @@ $(LIB): $(OBJS) %.o: %.S $(CASMRUNTIME) -DMODEL_$(MODEL) -DABI_$(ABI) -DENDIANNESS_$(ENDIANNESS) -DSYS_$(SYSTEM) -o $@ $^ +# If no asm implementation available, compile the portable C implementation +# with CompCert. Since CompCert rejects the "__i64_" identifiers, the C +# implementation uses "i64_" identifiers, and we rename them in the +# generated assembly + +%.o: c/%.c c/i64.h ../ccomp + ../ccomp -O2 -S -o $*.s -I./c c/$*.c + sed -i -e 's/i64_/__i64_/g' $*.s + $(CASMRUNTIME) -o $*.o $*.s + @rm -f $*.s + clean:: - rm -f *.o $(LIB) + rm -f *.o $(LIB) *.tmp?.s ifeq ($(strip $(HAS_RUNTIME_LIB)),true) install:: diff --git a/runtime/c/i64.h b/runtime/c/i64.h index a75214fe..3f59164b 100644 --- a/runtime/c/i64.h +++ b/runtime/c/i64.h @@ -34,12 +34,12 @@ /* Helper functions for 64-bit integer arithmetic. Reference C implementation */ -extern unsigned long long __i64_shl(unsigned long long x, int amount); -extern unsigned long long __i64_shr(unsigned long long x, int amount); -extern signed long long __i64_sar(signed long long x, int amount); +extern unsigned long long i64_shl(unsigned long long x, int amount); +extern unsigned long long i64_shr(unsigned long long x, int amount); +extern signed long long i64_sar(signed long long x, int amount); -extern unsigned long long __i64_udivmod(unsigned long long n, +extern unsigned long long i64_udivmod(unsigned long long n, unsigned long long d, unsigned long long * rp); -extern unsigned long long __i64_umulh(unsigned long long u, +extern unsigned long long i64_umulh(unsigned long long u, unsigned long long v); diff --git a/runtime/c/i64_dtos.c b/runtime/c/i64_dtos.c index d428e744..5d12bf4b 100644 --- a/runtime/c/i64_dtos.c +++ b/runtime/c/i64_dtos.c @@ -38,7 +38,7 @@ /* Conversion float64 -> signed int64 */ -long long __i64_dtos(double d) +long long i64_dtos(double d) { /* Extract bits of d's representation */ union { double d; unsigned long long i; } buf; @@ -63,9 +63,9 @@ long long __i64_dtos(double d) (buf.i & ~0xFFF0000000000000LL) | 0x0010000000000000LL; /* Shift it appropriately */ if (e >= 0) - m = __i64_shl(m, e); + m = i64_shl(m, e); else - m = __i64_shr(m, -e); + m = i64_shr(m, -e); /* Apply sign to result */ if ((int) h < 0) return -m; diff --git a/runtime/c/i64_dtou.c b/runtime/c/i64_dtou.c index c5f9df4d..5f4901b2 100644 --- a/runtime/c/i64_dtou.c +++ b/runtime/c/i64_dtou.c @@ -38,7 +38,7 @@ /* Conversion float64 -> unsigned int64 */ -unsigned long long __i64_dtou(double d) +unsigned long long i64_dtou(double d) { /* Extract bits of d's representation */ union { double d; unsigned long long i; } buf; @@ -62,8 +62,8 @@ unsigned long long __i64_dtou(double d) (buf.i & ~0xFFF0000000000000LL) | 0x0010000000000000LL; /* Shift it appropriately */ if (e >= 0) - return __i64_shl(m, e); + return i64_shl(m, e); else - return __i64_shr(m, -e); + return i64_shr(m, -e); } diff --git a/runtime/c/i64_sar.c b/runtime/c/i64_sar.c index a5f3364a..611aa047 100644 --- a/runtime/c/i64_sar.c +++ b/runtime/c/i64_sar.c @@ -38,7 +38,7 @@ /* Shift right signed */ -signed long long __i64_sar(signed long long x, int amount) +signed long long i64_sar(signed long long x, int amount) { unsigned xl = x; int xh = x >> 32; diff --git a/runtime/c/i64_sdiv.c b/runtime/c/i64_sdiv.c index 3f21d9b7..20faf121 100644 --- a/runtime/c/i64_sdiv.c +++ b/runtime/c/i64_sdiv.c @@ -38,14 +38,14 @@ /* Signed division */ -signed long long __i64_sdiv(signed long long n, signed long long d) +signed long long i64_sdiv(signed long long n, signed long long d) { unsigned long long un, ud, uq, ur; int nh = n >> 32, dh = d >> 32; /* Take absolute values of n and d */ un = nh < 0 ? -n : n; ud = dh < 0 ? -d : d; - uq = __i64_udivmod(un, ud, &ur); + uq = i64_udivmod(un, ud, &ur); /* Apply sign to quotient */ return (nh ^ dh) < 0 ? -uq : uq; } diff --git a/runtime/c/i64_shl.c b/runtime/c/i64_shl.c index 9b9aae57..186d2d32 100644 --- a/runtime/c/i64_shl.c +++ b/runtime/c/i64_shl.c @@ -38,7 +38,7 @@ /* Shift left */ -unsigned long long __i64_shl(unsigned long long x, int amount) +unsigned long long i64_shl(unsigned long long x, int amount) { unsigned xl = x, xh = x >> 32; amount = amount & 63; diff --git a/runtime/c/i64_shr.c b/runtime/c/i64_shr.c index c1db2a5f..bb2facce 100644 --- a/runtime/c/i64_shr.c +++ b/runtime/c/i64_shr.c @@ -38,7 +38,7 @@ /* Shift right unsigned */ -unsigned long long __i64_shr(unsigned long long x, int amount) +unsigned long long i64_shr(unsigned long long x, int amount) { unsigned xl = x, xh = x >> 32; amount = amount & 63; diff --git a/runtime/c/i64_smod.c b/runtime/c/i64_smod.c index ab15b6e6..b0f2c3cd 100644 --- a/runtime/c/i64_smod.c +++ b/runtime/c/i64_smod.c @@ -38,14 +38,14 @@ /* Signed remainder */ -signed long long __i64_smod(signed long long n, signed long long d) +signed long long i64_smod(signed long long n, signed long long d) { unsigned long long un, ud, ur; int nh = n >> 32, dh = d >> 32; /* Take absolute values of n and d */ un = nh < 0 ? -n : n; ud = dh < 0 ? -d : d; - (void) __i64_udivmod(un, ud, &ur); + (void) i64_udivmod(un, ud, &ur); /* Apply sign to remainder */ return nh < 0 ? -ur : ur; } diff --git a/runtime/c/i64_smulh.c b/runtime/c/i64_smulh.c index b7a42474..3b33d375 100644 --- a/runtime/c/i64_smulh.c +++ b/runtime/c/i64_smulh.c @@ -47,9 +47,9 @@ typedef unsigned long long u64; * - subtract Y if X < 0 */ -s64 __i64_smulh(s64 x, s64 y) +s64 i64_smulh(s64 x, s64 y) { - s64 t = (s64) __i64_umulh(x, y); + s64 t = (s64) i64_umulh(x, y); if (y < 0) t = t - x; if (x < 0) t = t - y; return t; diff --git a/runtime/c/i64_stod.c b/runtime/c/i64_stod.c index 158b6892..b5b6a7bc 100644 --- a/runtime/c/i64_stod.c +++ b/runtime/c/i64_stod.c @@ -38,7 +38,7 @@ /* Conversion from signed int64 to float64 */ -double __i64_stod(signed long long x) +double i64_stod(signed long long x) { unsigned xl = x; signed xh = x >> 32; diff --git a/runtime/c/i64_stof.c b/runtime/c/i64_stof.c index 8410ba13..12406421 100644 --- a/runtime/c/i64_stof.c +++ b/runtime/c/i64_stof.c @@ -38,7 +38,7 @@ /* Conversion from signed int64 to float32 */ -float __i64_stof(signed long long x) +float i64_stof(signed long long x) { if (x < -(1LL << 53) || x >= (1LL << 53)) { /* x is large enough that double rounding can occur. diff --git a/runtime/c/i64_udiv.c b/runtime/c/i64_udiv.c index 91fbf6e4..19d9264d 100644 --- a/runtime/c/i64_udiv.c +++ b/runtime/c/i64_udiv.c @@ -38,8 +38,8 @@ /* Unsigned division */ -unsigned long long __i64_udiv(unsigned long long n, unsigned long long d) +unsigned long long i64_udiv(unsigned long long n, unsigned long long d) { unsigned long long r; - return __i64_udivmod(n, d, &r); + return i64_udivmod(n, d, &r); } diff --git a/runtime/c/i64_udivmod.c b/runtime/c/i64_udivmod.c index d8f5073a..03efbc9d 100644 --- a/runtime/c/i64_udivmod.c +++ b/runtime/c/i64_udivmod.c @@ -37,13 +37,13 @@ #include <stddef.h> #include "i64.h" -static unsigned __i64_udiv6432(unsigned u1, unsigned u0, +static unsigned i64_udiv6432(unsigned u1, unsigned u0, unsigned v, unsigned *r); -static int __i64_nlz(unsigned x); +static int i64_nlz(unsigned x); /* Unsigned division and remainder */ -unsigned long long __i64_udivmod(unsigned long long n, +unsigned long long i64_udivmod(unsigned long long n, unsigned long long d, unsigned long long * rp) { @@ -62,7 +62,7 @@ unsigned long long __i64_udivmod(unsigned long long n, unsigned dl = d; unsigned qh = nh / dl; unsigned rl; - unsigned ql = __i64_udiv6432(nh % dl, nl, dl, &rl); + unsigned ql = i64_udiv6432(nh % dl, nl, dl, &rl); *rp = (unsigned long long) rl; /* high word of remainder is 0 */ return ((unsigned long long) qh) << 32 | ql; } @@ -70,11 +70,11 @@ unsigned long long __i64_udivmod(unsigned long long n, /* General case 64 / 64 */ unsigned dl = d; /* Scale N and D down, giving N' and D' such that 2^31 <= D' < 2^32 */ - int s = 32 - __i64_nlz(dh); /* shift amount, between 1 and 32 */ - unsigned long long np = __i64_shr(n, s); - unsigned dp = (unsigned) __i64_shr(d, s); + int s = 32 - i64_nlz(dh); /* shift amount, between 1 and 32 */ + unsigned long long np = i64_shr(n, s); + unsigned dp = (unsigned) i64_shr(d, s); /* Divide N' by D' to get an approximate quotient Q */ - unsigned q = __i64_udiv6432(np >> 32, np, dp, NULL); + unsigned q = i64_udiv6432(np >> 32, np, dp, NULL); again: ; /* Tentative quotient Q is either correct or one too high */ /* Compute Q * D, checking for overflow */ @@ -99,7 +99,7 @@ unsigned long long __i64_udivmod(unsigned long long n, /* Unsigned division and remainder for 64 bits divided by 32 bits. */ /* This is algorithm "divlu" from _Hacker's Delight_, fig 9.3 */ -static unsigned __i64_udiv6432(unsigned u1, unsigned u0, +static unsigned i64_udiv6432(unsigned u1, unsigned u0, unsigned v, unsigned *r) { const unsigned b = 65536; // Number base (16 bits). @@ -114,7 +114,7 @@ static unsigned __i64_udiv6432(unsigned u1, unsigned u0, if (r != NULL) *r = 0xFFFFFFFFU; // set rem to an impossible value, return 0xFFFFFFFFU; // and return largest possible quotient. } - s = __i64_nlz(v); // 0 <= s <= 31. + s = i64_nlz(v); // 0 <= s <= 31. v = v << s; // Normalize divisor. vn1 = v >> 16; // Break divisor up into vn0 = v & 0xFFFF; // two 16-bit digits. @@ -145,7 +145,7 @@ again2: /* Number of leading zeroes */ -static int __i64_nlz(unsigned x) +static int i64_nlz(unsigned x) { if (x == 0) return 32; int n = 0; diff --git a/runtime/c/i64_umod.c b/runtime/c/i64_umod.c index d30e29c4..37640d5f 100644 --- a/runtime/c/i64_umod.c +++ b/runtime/c/i64_umod.c @@ -38,9 +38,9 @@ /* Unsigned remainder */ -unsigned long long __i64_umod(unsigned long long n, unsigned long long d) +unsigned long long i64_umod(unsigned long long n, unsigned long long d) { unsigned long long r; - (void) __i64_udivmod(n, d, &r); + (void) i64_udivmod(n, d, &r); return r; } diff --git a/runtime/c/i64_umulh.c b/runtime/c/i64_umulh.c index d2394d09..a2e33f5d 100644 --- a/runtime/c/i64_umulh.c +++ b/runtime/c/i64_umulh.c @@ -43,7 +43,7 @@ typedef unsigned int u32; /* Hacker's Delight, algorithm 8.1, specialized to two 32-bit words */ -u64 __i64_umulh(u64 u, u64 v) +u64 i64_umulh(u64 u, u64 v) { u32 u0 = u, u1 = u >> 32; u32 v0 = v, v1 = v >> 32; diff --git a/runtime/c/i64_utod.c b/runtime/c/i64_utod.c index e70820a9..7210c73c 100644 --- a/runtime/c/i64_utod.c +++ b/runtime/c/i64_utod.c @@ -38,7 +38,7 @@ /* Conversion from unsigned int64 to float64 */ -double __i64_utod(unsigned long long x) +double i64_utod(unsigned long long x) { unsigned xl = x, xh = x >> 32; return (double) xl + 0x1.0p32 * (double) xh; diff --git a/runtime/c/i64_utof.c b/runtime/c/i64_utof.c index 87b85bfc..77a23765 100644 --- a/runtime/c/i64_utof.c +++ b/runtime/c/i64_utof.c @@ -38,7 +38,7 @@ /* Conversion from unsigned int64 to float32 */ -float __i64_utof(unsigned long long x) +float i64_utof(unsigned long long x) { if (x >= 1ULL << 53) { /* x is large enough that double rounding can occur. diff --git a/runtime/riscV/sysdeps.h b/runtime/riscV/sysdeps.h new file mode 100644 index 00000000..b95ca1b1 --- /dev/null +++ b/runtime/riscV/sysdeps.h @@ -0,0 +1,63 @@ +// ***************************************************************** +// +// The Compcert verified compiler +// +// Xavier Leroy, INRIA Paris-Rocquencourt +// +// Copyright (c) 2013 Institut National de Recherche en Informatique et +// en Automatique. +// +// Redistribution and use in source and binary forms, with or without +// modification, are permitted provided that the following conditions are met: +// * Redistributions of source code must retain the above copyright +// notice, this list of conditions and the following disclaimer. +// * Redistributions in binary form must reproduce the above copyright +// notice, this list of conditions and the following disclaimer in the +// documentation and/or other materials provided with the distribution. +// * Neither the name of the <organization> nor the +// names of its contributors may be used to endorse or promote products +// derived from this software without specific prior written permission. +// +// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT +// HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +// +// ********************************************************************* + +// System dependencies + +#define FUNCTION(f) \ + .text; \ + .balign 16; \ + .globl f; \ +f: + +#define ENDFUNCTION(f) \ + .type f, @function; .size f, . - f + +#if defined(MODEL_64) + +#define WORDSIZE 8 +#define lptr ld +#define sptr sd + +#elif defined(MODEL_32) + +#define WORDSIZE 4 +#define lptr lw +#define sptr sw + +#else + +#error "Wrong MODEL" + +#endif + diff --git a/runtime/riscV/vararg.S b/runtime/riscV/vararg.S new file mode 100644 index 00000000..a9481077 --- /dev/null +++ b/runtime/riscV/vararg.S @@ -0,0 +1,90 @@ +// ***************************************************************** +// +// The Compcert verified compiler +// +// Xavier Leroy, INRIA Paris-Rocquencourt +// Prashanth Mundkur, SRI International +// +// Copyright (c) 2013 Institut National de Recherche en Informatique et +// en Automatique. +// +// The contributions by Prashanth Mundkur are reused and adapted +// under the terms of a Contributor License Agreement between +// SRI International and INRIA. +// +// Redistribution and use in source and binary forms, with or without +// modification, are permitted provided that the following conditions are met: +// * Redistributions of source code must retain the above copyright +// notice, this list of conditions and the following disclaimer. +// * Redistributions in binary form must reproduce the above copyright +// notice, this list of conditions and the following disclaimer in the +// documentation and/or other materials provided with the distribution. +// * Neither the name of the <organization> nor the +// names of its contributors may be used to endorse or promote products +// derived from this software without specific prior written permission. +// +// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT +// HOLDER> BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +// +// ********************************************************************* + +// Helper functions for variadic functions <stdarg.h>. RISC-V version. + +#include "sysdeps.h" + +// typedef void * va_list; +// unsigned int __compcert_va_int32(va_list * ap); +// unsigned long long __compcert_va_int64(va_list * ap); +// double __compcert_va_float64(va_list * ap); + +FUNCTION(__compcert_va_int32) + # a0 = ap parameter + lptr t5, 0(a0) # t5 = pointer to next argument + addi t5, t5, WORDSIZE # advance ap + sptr t5, 0(a0) # update ap + lw a0, -WORDSIZE(t5) # load it and return it in a0 + jr ra +ENDFUNCTION(__compcert_va_int32) + +FUNCTION(__compcert_va_int64) + # a0 = ap parameter + lptr t5, 0(a0) # t5 = pointer to next argument + addi t5, t5, 15 # 8-align and advance by 8 + and t5, t5, -8 + sptr t5, 0(a0) # update ap +#ifdef MODEL_64 + ld a0, -8(t5) # return it in a0 +#else + lw a0, -8(t5) # return it in [a0,a1] + lw a1, -4(t5) +#endif + jr ra +ENDFUNCTION(__compcert_va_int64) + +FUNCTION(__compcert_va_float64) + # a0 = ap parameter + lptr t5, 0(a0) # t5 = pointer to next argument + addi t5, t5, 15 # 8-align and advance by 8 + and t5, t5, -8 + sw t5, 0(a0) # update ap + fld fa0, -8(t5) # return it in fa0 + jr ra +ENDFUNCTION(__compcert_va_float64) + +// Right now we pass structs by reference. This is not ABI conformant. +FUNCTION(__compcert_va_composite) +#ifdef MODEL_64 + j __compcert_va_int64 +#else + j __compcert_va_int32 +#endif +ENDFUNCTION(__compcert_va_composite) |