aboutsummaryrefslogtreecommitdiffstats
path: root/runtime
diff options
context:
space:
mode:
Diffstat (limited to 'runtime')
-rw-r--r--runtime/Makefile11
l---------runtime/c/ccomp_k1c_fixes.h1
-rw-r--r--runtime/include/ccomp_k1c_fixes.h30
-rw-r--r--runtime/include/math.h26
-rw-r--r--runtime/mppa_k1c/Makefile15
l---------runtime/mppa_k1c/ccomp_k1c_fixes.h1
-rw-r--r--runtime/mppa_k1c/i64_sdiv.c28
-rw-r--r--runtime/mppa_k1c/i64_smod.c40
-rw-r--r--runtime/mppa_k1c/i64_udiv.c0
-rw-r--r--runtime/mppa_k1c/i64_udivmod.c28
-rw-r--r--runtime/mppa_k1c/i64_umod.c0
-rw-r--r--runtime/mppa_k1c/vararg.s54
12 files changed, 233 insertions, 1 deletions
diff --git a/runtime/Makefile b/runtime/Makefile
index 6777995d..3b1cabc4 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -22,6 +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)
+OBJS=i64_umod.o i64_udiv.o i64_udivmod.o i64_sdiv.o i64_smod.o vararg.o\
+ i64_dtos.o i64_dtou.o i64_utod.o i64_utof.o i64_stod.o i64_stof.o\
+ i64_shl.o i64_shr.o
+# Missing: i64_utod.o i64_utof.o i64_stod.o i64_stof.o
+DOMAKE:=$(shell (cd mppa_k1c && make))
else ifeq ($(ARCH),aarch64)
OBJS=vararg.o
else
@@ -37,6 +43,9 @@ 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
+endif
VPATH=$(ARCH)
@@ -65,7 +74,7 @@ $(LIB): $(OBJS)
../ccomp -O2 -S -o $*.s -I./c c/$*.c
sed -i -e 's/i64_/__compcert_i64_/g' $*.s
$(CASMRUNTIME) -o $*.o $*.s
- @rm -f $*.s
+ @rm $*.s
clean::
rm -f *.o $(LIB) *.tmp?.s
diff --git a/runtime/c/ccomp_k1c_fixes.h b/runtime/c/ccomp_k1c_fixes.h
new file mode 120000
index 00000000..b640c96e
--- /dev/null
+++ b/runtime/c/ccomp_k1c_fixes.h
@@ -0,0 +1 @@
+../include/ccomp_k1c_fixes.h \ No newline at end of file
diff --git a/runtime/include/ccomp_k1c_fixes.h b/runtime/include/ccomp_k1c_fixes.h
new file mode 100644
index 00000000..718ac3e5
--- /dev/null
+++ b/runtime/include/ccomp_k1c_fixes.h
@@ -0,0 +1,30 @@
+#ifndef __CCOMP_KIC_FIXES_H
+#define __CCOMP_KIC_FIXES_H
+
+#if ! (defined(__COMPCERT__) && defined (__K1C__))
+#error This header is solely for CompCert on K1C
+#endif
+
+#undef __GNUC__
+#define __thread
+
+struct __int128_ccomp { long __int128_ccomp_low; long __int128_ccomp_high; };
+
+#define __int128 struct __int128_ccomp
+
+#define __builtin_k1_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
+extern __int128 __compcert_acswapw(void *address, unsigned long long new_value, unsigned long long old_value);
+
+#define __builtin_k1_afaddd __compcert_afaddd
+extern long long __compcert_afaddd(void *address, unsigned long long incr);
+
+#define __builtin_k1_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)
diff --git a/runtime/include/math.h b/runtime/include/math.h
new file mode 100644
index 00000000..01b8d8d8
--- /dev/null
+++ b/runtime/include/math.h
@@ -0,0 +1,26 @@
+#ifndef _COMPCERT_MATH_H
+#define _COMPCERT_MATH_H
+
+#ifdef __K1C__
+
+#define isfinite(__y) (fpclassify((__y)) >= FP_ZERO)
+
+#include_next <math.h>
+
+#ifndef COMPCERT_NO_FP_MACROS
+#define fmin(x, y) __builtin_fmin((x),(y))
+#define fmax(x, y) __builtin_fmax((x),(y))
+#define fminf(x, y) __builtin_fminf((x),(y))
+#define fmaxf(x, y) __builtin_fmaxf((x),(y))
+#define fabs(x) __builtin_fabs((x))
+#define fabsf(x) __builtin_fabsf((x))
+#define fma(x, y, z) __builtin_fma((x),(y),(z))
+#define fmaf(x, y, z) __builtin_fmaf((x),(y),(z))
+#endif
+
+#else
+
+#include_next <math.h>
+
+#endif
+#endif
diff --git a/runtime/mppa_k1c/Makefile b/runtime/mppa_k1c/Makefile
new file mode 100644
index 00000000..4e47f567
--- /dev/null
+++ b/runtime/mppa_k1c/Makefile
@@ -0,0 +1,15 @@
+CCOMP ?= ../../ccomp
+CFLAGS ?= -O2 -D__K1_TINYK1__
+
+CFILES=$(wildcard *.c)
+SFILES=$(subst .c,.s,$(CFILES))
+
+CCOMPPATH=$(shell which $(CCOMP))
+
+all: $(SFILES)
+
+.SECONDARY:
+%.s: %.c $(CCOMPPATH)
+ $(CCOMP) $(CFLAGS) -S $< -o $@
+ sed -i -e 's/i64_/__compcert_i64_/g' -e 's/i32_/__compcert_i32_/g' \
+ -e 's/f64_/__compcert_f64_/g' -e 's/f32_/__compcert_f32_/g' $@
diff --git a/runtime/mppa_k1c/ccomp_k1c_fixes.h b/runtime/mppa_k1c/ccomp_k1c_fixes.h
new file mode 120000
index 00000000..b640c96e
--- /dev/null
+++ b/runtime/mppa_k1c/ccomp_k1c_fixes.h
@@ -0,0 +1 @@
+../include/ccomp_k1c_fixes.h \ No newline at end of file
diff --git a/runtime/mppa_k1c/i64_sdiv.c b/runtime/mppa_k1c/i64_sdiv.c
new file mode 100644
index 00000000..60269cae
--- /dev/null
+++ b/runtime/mppa_k1c/i64_sdiv.c
@@ -0,0 +1,28 @@
+extern long __divdi3 (long a, long b);
+
+long i64_sdiv (long a, long b)
+{
+ return __divdi3 (a, b);
+}
+
+int i32_sdiv (int a, int b)
+{
+ return __divdi3 (a, b);
+}
+
+#ifdef OUR_OWN_FE_EXCEPT
+#include <../../k1-cos/include/hal/cos_registers.h>
+
+/* 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);
+ 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);
+ return 0;
+}
+#endif
diff --git a/runtime/mppa_k1c/i64_smod.c b/runtime/mppa_k1c/i64_smod.c
new file mode 100644
index 00000000..26ffb39b
--- /dev/null
+++ b/runtime/mppa_k1c/i64_smod.c
@@ -0,0 +1,40 @@
+#if COMPLIQUE
+unsigned long long
+udivmoddi4(unsigned long long num, unsigned long long den, int modwanted);
+
+long long
+i64_smod (long long a, long long b)
+{
+ int neg = 0;
+ long long res;
+
+ if (a < 0)
+ {
+ a = -a;
+ neg = 1;
+ }
+
+ if (b < 0)
+ b = -b;
+
+ res = udivmoddi4 (a, b, 1);
+
+ if (neg)
+ res = -res;
+
+ return res;
+}
+
+#else
+extern long __moddi3 (long a, long b);
+
+long i64_smod (long a, long b)
+{
+ return __moddi3 (a, b);
+}
+
+int i32_smod (int a, int b)
+{
+ return __moddi3 (a, b);
+}
+#endif
diff --git a/runtime/mppa_k1c/i64_udiv.c b/runtime/mppa_k1c/i64_udiv.c
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/runtime/mppa_k1c/i64_udiv.c
diff --git a/runtime/mppa_k1c/i64_udivmod.c b/runtime/mppa_k1c/i64_udivmod.c
new file mode 100644
index 00000000..74b39874
--- /dev/null
+++ b/runtime/mppa_k1c/i64_udivmod.c
@@ -0,0 +1,28 @@
+/* THIS IS THE PREVIOUS VERSION, USED ON BOSTAN AND ANDEY */
+unsigned long long
+udivmoddi4(unsigned long long num, unsigned long long den, int modwanted)
+{
+ unsigned long long r = num, q = 0;
+
+ if(den <= r) {
+ unsigned k = __builtin_clzll (den) - __builtin_clzll (r);
+ den = den << k;
+ if(r >= den) {
+ r = r - den;
+ q = 1LL << k;
+ }
+ if(k != 0) {
+ unsigned i = k;
+ den = den >> 1;
+ do {
+ r = __builtin_k1_stsud (den, r);
+ i--;
+ } while (i!= 0);
+ q = q + r;
+ r = r >> k;
+ q = q - (r << k);
+ }
+ }
+
+ return modwanted ? r : q;
+}
diff --git a/runtime/mppa_k1c/i64_umod.c b/runtime/mppa_k1c/i64_umod.c
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/runtime/mppa_k1c/i64_umod.c
diff --git a/runtime/mppa_k1c/vararg.s b/runtime/mppa_k1c/vararg.s
new file mode 100644
index 00000000..65c1eab8
--- /dev/null
+++ b/runtime/mppa_k1c/vararg.s
@@ -0,0 +1,54 @@
+
+# typedef void * va_list;
+# unsigned int __compcert_va_int32(va_list * ap);
+# unsigned long long __compcert_va_int64(va_list * ap);
+
+ .text
+ .balign 2
+ .globl __compcert_va_int32
+__compcert_va_int32:
+ ld $r32 = 0[$r0] # $r32 <- *ap
+;;
+ addd $r32 = $r32, 8 # $r32 <- $r32 + WORDSIZE
+;;
+ sd 0[$r0] = $r32 # *ap <- $r32
+;;
+ lws $r0 = -8[$r32] # retvalue <- 32-bits at *ap - WORDSIZE
+ ret
+;;
+
+ .text
+ .balign 2
+ .globl __compcert_va_int64
+ .globl __compcert_va_float64
+ .globl __compcert_va_composite
+__compcert_va_int64:
+__compcert_va_float64:
+# FIXME this assumes pass-by-reference
+__compcert_va_composite:
+# Prologue
+ ld $r32 = 0[$r0] # $r32 <- *ap
+;;
+ addd $r32 = $r32, 8 # $r32 <- $r32 + WORDSIZE
+;;
+ sd 0[$r0] = $r32 # *ap <- $r32
+;;
+ ld $r0 = -8[$r32] # retvalue <- 64-bits at *ap - WORDSIZE
+ ret
+;;
+
+# FIXME this assumes pass-by-reference
+ .globl __compcert_acswapd
+__compcert_acswapd:
+ acswapd 0[$r1] = $r2r3
+ ;;
+ sq 0[$r0] = $r2r3
+ ret
+ ;;
+ .globl __compcert_acswapw
+__compcert_acswapw:
+ acswapw 0[$r1] = $r2r3
+ ;;
+ sq 0[$r0] = $r2r3
+ ret
+ ;;
generated by cgit (git 2.34.1) at 2024-05-20 08:58:17 +0000