diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-05-26 22:04:20 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-05-26 22:04:20 +0200 |
commit | b4a08d0815342b6238d307864f0823d0f07bb691 (patch) | |
tree | 85f48254ca79a6e2bc9d7359017a5731f98f897f /runtime | |
parent | 490a6caea1a95cfdbddf7aca244fa6a1c83aa9a2 (diff) | |
download | compcert-kvx-b4a08d0815342b6238d307864f0823d0f07bb691.tar.gz compcert-kvx-b4a08d0815342b6238d307864f0823d0f07bb691.zip |
k1c -> kvx changes
Diffstat (limited to 'runtime')
-rw-r--r-- | runtime/Makefile | 8 | ||||
l--------- | runtime/c/ccomp_kvx_fixes.h | 1 | ||||
-rw-r--r-- | runtime/include/ccomp_kvx_fixes.h (renamed from runtime/include/ccomp_k1c_fixes.h) | 16 | ||||
-rw-r--r-- | runtime/include/math.h | 2 | ||||
-rw-r--r-- | runtime/kvx/Makefile (renamed from runtime/mppa_k1c/Makefile) | 0 | ||||
l--------- | runtime/kvx/ccomp_k1c_fixes.h (renamed from runtime/c/ccomp_k1c_fixes.h) | 0 | ||||
-rw-r--r-- | runtime/kvx/i32_divmod.s (renamed from runtime/mppa_k1c/i32_divmod.s) | 2 | ||||
-rw-r--r-- | runtime/kvx/i64_sdiv.c (renamed from runtime/mppa_k1c/i64_sdiv.c) | 4 | ||||
-rw-r--r-- | runtime/kvx/i64_smod.c (renamed from runtime/mppa_k1c/i64_smod.c) | 0 | ||||
-rw-r--r-- | runtime/kvx/i64_udiv.c (renamed from runtime/mppa_k1c/i64_udiv.c) | 0 | ||||
-rw-r--r-- | runtime/kvx/i64_udivmod.c (renamed from runtime/mppa_k1c/i64_udivmod.c) | 2 | ||||
-rw-r--r-- | runtime/kvx/i64_udivmod_stsud.s (renamed from runtime/mppa_k1c/i64_udivmod_stsud.s) | 2 | ||||
-rw-r--r-- | runtime/kvx/i64_umod.c (renamed from runtime/mppa_k1c/i64_umod.c) | 0 | ||||
-rw-r--r-- | runtime/kvx/vararg.s (renamed from runtime/mppa_k1c/vararg.s) | 0 | ||||
l--------- | runtime/mppa_k1c/ccomp_k1c_fixes.h | 1 |
15 files changed, 19 insertions, 19 deletions
diff --git a/runtime/Makefile b/runtime/Makefile index ebce458b..ea3c914f 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -22,12 +22,12 @@ ifeq ($(ARCH),x86_64) OBJS=i64_dtou.o i64_utod.o i64_utof.o vararg.o else ifeq ($(ARCH),powerpc64) OBJS=i64_dtou.o i64_stof.o i64_utod.o i64_utof.o vararg.o -else ifeq ($(ARCH),mppa_k1c) +else ifeq ($(ARCH),kvx) OBJS=i64_umod.o i64_udiv.o i64_udivmod.o i64_sdiv.o i64_smod.o \ i64_udivmod_stsud.o i32_divmod.o \ i64_utod.o i64_utof.o i64_stod.o i64_stof.o \ vararg.o -DOMAKE:=$(shell (cd mppa_k1c && make)) +DOMAKE:=$(shell (cd kvx && make)) else ifeq ($(ARCH),aarch64) OBJS=vararg.o else @@ -45,8 +45,8 @@ LIB=libcompcert.a INCLUDES=include/float.h include/stdarg.h include/stdbool.h \ include/stddef.h include/varargs.h include/stdalign.h \ include/stdnoreturn.h -ifeq ($(ARCH),mppa_k1c) -INCLUDES += include/ccomp_k1c_fixes.h include/math.h +ifeq ($(ARCH),kvx) +INCLUDES += include/ccomp_kvx_fixes.h include/math.h endif VPATH=$(ARCH) diff --git a/runtime/c/ccomp_kvx_fixes.h b/runtime/c/ccomp_kvx_fixes.h new file mode 120000 index 00000000..726d0f72 --- /dev/null +++ b/runtime/c/ccomp_kvx_fixes.h @@ -0,0 +1 @@ +../include/ccomp_kvx_fixes.h
\ No newline at end of file diff --git a/runtime/include/ccomp_k1c_fixes.h b/runtime/include/ccomp_kvx_fixes.h index c884ae23..65d65e7b 100644 --- a/runtime/include/ccomp_k1c_fixes.h +++ b/runtime/include/ccomp_kvx_fixes.h @@ -16,8 +16,8 @@ #ifndef __CCOMP_KIC_FIXES_H #define __CCOMP_KIC_FIXES_H -#if ! (defined(__COMPCERT__) && defined (__K1C__)) -#error This header is solely for CompCert on K1C +#if ! (defined(__COMPCERT__) && defined (__KVX__)) +#error This header is solely for CompCert on KVX #endif #undef __GNUC__ @@ -27,19 +27,19 @@ struct __int128_ccomp { long __int128_ccomp_low; long __int128_ccomp_high; }; #define __int128 struct __int128_ccomp -#define __builtin_k1_acswapd __compcert_acswapd +#define __builtin_kvx_acswapd __compcert_acswapd extern __int128 __compcert_acswapd(void *address, unsigned long long new_value, unsigned long long old_value); -#define __builtin_k1_acswapw __compcert_acswapw +#define __builtin_kvx_acswapw __compcert_acswapw extern __int128 __compcert_acswapw(void *address, unsigned long long new_value, unsigned long long old_value); -#define __builtin_k1_afaddd __compcert_afaddd +#define __builtin_kvx_afaddd __compcert_afaddd extern long long __compcert_afaddd(void *address, unsigned long long incr); -#define __builtin_k1_afaddw __compcert_afaddw +#define __builtin_kvx_afaddw __compcert_afaddw extern int __compcert_afaddw(void *address, unsigned int incr); #endif /* #define __builtin_expect(x, y) (x) */ -#define __builtin_ctz(x) __builtin_k1_ctzw(x) -#define __builtin_clz(x) __builtin_k1_clzw(x) +#define __builtin_ctz(x) __builtin_kvx_ctzw(x) +#define __builtin_clz(x) __builtin_kvx_clzw(x) diff --git a/runtime/include/math.h b/runtime/include/math.h index 422787e1..e7c9e475 100644 --- a/runtime/include/math.h +++ b/runtime/include/math.h @@ -15,7 +15,7 @@ #ifndef _COMPCERT_MATH_H #define _COMPCERT_MATH_H -#ifdef __K1C__ +#ifdef __KVX__ #define isfinite(__y) (fpclassify((__y)) >= FP_ZERO) diff --git a/runtime/mppa_k1c/Makefile b/runtime/kvx/Makefile index 4e47f567..4e47f567 100644 --- a/runtime/mppa_k1c/Makefile +++ b/runtime/kvx/Makefile diff --git a/runtime/c/ccomp_k1c_fixes.h b/runtime/kvx/ccomp_k1c_fixes.h index b640c96e..b640c96e 120000 --- a/runtime/c/ccomp_k1c_fixes.h +++ b/runtime/kvx/ccomp_k1c_fixes.h diff --git a/runtime/mppa_k1c/i32_divmod.s b/runtime/kvx/i32_divmod.s index d2b4e8d5..9a6f0bce 100644 --- a/runtime/mppa_k1c/i32_divmod.s +++ b/runtime/kvx/i32_divmod.s @@ -1,4 +1,4 @@ -/* K1C +/* KVX 32-bit unsigned/signed integer division/modulo (udiv5) D. Monniaux, CNRS, VERIMAG */ diff --git a/runtime/mppa_k1c/i64_sdiv.c b/runtime/kvx/i64_sdiv.c index b98d9316..a42164cc 100644 --- a/runtime/mppa_k1c/i64_sdiv.c +++ b/runtime/kvx/i64_sdiv.c @@ -11,13 +11,13 @@ int i32_sdiv (int a, int b) /* DM FIXME this is for floating point */ int fetestexcept(int excepts) { int mask = (COS_SFR_CS_IO_MASK | COS_SFR_CS_DZ_MASK | COS_SFR_CS_OV_MASK | COS_SFR_CS_UN_MASK | COS_SFR_CS_IN_MASK) & excepts; - unsigned long long cs = __builtin_k1_get(COS_SFR_CS); + unsigned long long cs = __builtin_kvx_get(COS_SFR_CS); return cs & mask; } int feclearexcept(int excepts) { int mask = (COS_SFR_CS_IO_MASK | COS_SFR_CS_DZ_MASK | COS_SFR_CS_OV_MASK | COS_SFR_CS_UN_MASK | COS_SFR_CS_IN_MASK) & excepts; - __builtin_k1_wfxl(COS_SFR_CS, mask); + __builtin_kvx_wfxl(COS_SFR_CS, mask); return 0; } #endif diff --git a/runtime/mppa_k1c/i64_smod.c b/runtime/kvx/i64_smod.c index 3371eecf..3371eecf 100644 --- a/runtime/mppa_k1c/i64_smod.c +++ b/runtime/kvx/i64_smod.c diff --git a/runtime/mppa_k1c/i64_udiv.c b/runtime/kvx/i64_udiv.c index 75f4bbf5..75f4bbf5 100644 --- a/runtime/mppa_k1c/i64_udiv.c +++ b/runtime/kvx/i64_udiv.c diff --git a/runtime/mppa_k1c/i64_udivmod.c b/runtime/kvx/i64_udivmod.c index ca48cd87..952e47e5 100644 --- a/runtime/mppa_k1c/i64_udivmod.c +++ b/runtime/kvx/i64_udivmod.c @@ -16,7 +16,7 @@ udivmoddi4(unsigned long long num, unsigned long long den, int modwanted) unsigned i = k; den = den >> 1; do { - r = __builtin_k1_stsud (den, r); + r = __builtin_kvx_stsud (den, r); i--; } while (i!= 0); q = q + r; diff --git a/runtime/mppa_k1c/i64_udivmod_stsud.s b/runtime/kvx/i64_udivmod_stsud.s index 50d0a767..2dd73d66 100644 --- a/runtime/mppa_k1c/i64_udivmod_stsud.s +++ b/runtime/kvx/i64_udivmod_stsud.s @@ -1,5 +1,5 @@ /* -Integer division for K1c +Integer division for KVX David Monniaux, CNRS / Verimag */ diff --git a/runtime/mppa_k1c/i64_umod.c b/runtime/kvx/i64_umod.c index 59e35960..59e35960 100644 --- a/runtime/mppa_k1c/i64_umod.c +++ b/runtime/kvx/i64_umod.c diff --git a/runtime/mppa_k1c/vararg.s b/runtime/kvx/vararg.s index 65c1eab8..65c1eab8 100644 --- a/runtime/mppa_k1c/vararg.s +++ b/runtime/kvx/vararg.s diff --git a/runtime/mppa_k1c/ccomp_k1c_fixes.h b/runtime/mppa_k1c/ccomp_k1c_fixes.h deleted file mode 120000 index b640c96e..00000000 --- a/runtime/mppa_k1c/ccomp_k1c_fixes.h +++ /dev/null @@ -1 +0,0 @@ -../include/ccomp_k1c_fixes.h
\ No newline at end of file |