8 files changed, 193 insertions, 1 deletions
diff --git a/runtime/Makefile b/runtime/Makefile
index 27ad6e8c..f58d4b6a 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -22,6 +22,11 @@ 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
+# Missing: i64_utod.o i64_utof.o i64_stod.o i64_stof.o
+DOMAKE:=$(shell (cd mppa_k1c && make))
 else
 OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_sdiv.o i64_shl.o \
   i64_shr.o i64_smod.o i64_stod.o i64_stof.o \
@@ -63,7 +68,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/mppa_k1c/Makefile b/runtime/mppa_k1c/Makefile
new file mode 100644
index 00000000..37e15e94
--- /dev/null
+++ b/runtime/mppa_k1c/Makefile
@@ -0,0 +1,14 @@
+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' $@
diff --git a/runtime/mppa_k1c/i64_sdiv.c b/runtime/mppa_k1c/i64_sdiv.c
new file mode 100644
index 00000000..9ef1a25c
--- /dev/null
+++ b/runtime/mppa_k1c/i64_sdiv.c
@@ -0,0 +1,29 @@
+unsigned long long
+udivmoddi4(unsigned long long num, unsigned long long den, int modwanted);
+
+long long
+i64_sdiv (long long a, long long b)
+{
+  int neg = 0;
+  long long res;
+
+  if (a < 0)
+    {
+      a = -a;
+      neg = !neg;
+    }
+
+  if (b < 0)
+    {
+      b = -b;
+      neg = !neg;
+    }
+
+  res = udivmoddi4 (a, b, 0);
+
+  if (neg)
+    res = -res;
+
+  return res;
+}
+
diff --git a/runtime/mppa_k1c/i64_smod.c b/runtime/mppa_k1c/i64_smod.c
new file mode 100644
index 00000000..010edd85
--- /dev/null
+++ b/runtime/mppa_k1c/i64_smod.c
@@ -0,0 +1,25 @@
+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;
+}
diff --git a/runtime/mppa_k1c/i64_udiv.c b/runtime/mppa_k1c/i64_udiv.c
new file mode 100644
index 00000000..2a8dcbf5
--- /dev/null
+++ b/runtime/mppa_k1c/i64_udiv.c
@@ -0,0 +1,8 @@
+unsigned long long
+udivmoddi4(unsigned long long num, unsigned long long den, int modwanted);
+
+unsigned long long i64_udiv (unsigned long long a, unsigned long long b)
+{
+  return udivmoddi4 (a, b, 0);
+}
+
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..fc0872bb
--- /dev/null
+++ b/runtime/mppa_k1c/i64_umod.c
@@ -0,0 +1,9 @@
+unsigned long long
+udivmoddi4(unsigned long long num, unsigned long long den, int modwanted);
+
+unsigned long long
+i64_umod (unsigned long long a, unsigned long long b)
+{
+  return udivmoddi4 (a, b, 1);
+}
+
diff --git a/runtime/mppa_k1c/vararg.S b/runtime/mppa_k1c/vararg.S
new file mode 100644
index 00000000..af6a0f9c
--- /dev/null
+++ b/runtime/mppa_k1c/vararg.S
@@ -0,0 +1,74 @@
+
+// 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:
+# Prologue
+	addd	$r14 = $r12, 0
+;;
+	addd	$r12 = $r12, -16
+;;
+	sd		0[$r12] = $r14
+;;
+	get		$r16 = $ra
+;;
+	sd		8[$r12] = $r16
+;;
+# Body
+	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
+;;
+# Prologue
+	ld		$r16 = 8[$r12]
+;;
+	set		$ra = $r16
+;;
+	addd	$r12 = $r12, 16
+;;
+	ret
+;;
+
+	.text
+	.balign 2
+	.globl __compcert_va_int64
+	.globl __compcert_va_float64
+__compcert_va_int64:
+__compcert_va_float64:
+# Prologue
+	addd	$r14 = $r12, 0
+;;
+	addd	$r12 = $r12, -16
+;;
+	sd		0[$r12] = $r14
+;;
+	get		$r16 = $ra
+;;
+	sd		8[$r12] = $r16
+;;
+# Body
+	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
+;;
+# Prologue
+	ld		$r16 = 8[$r12]
+;;
+	set		$ra = $r16
+;;
+	addd	$r12 = $r12, 16
+;;
+	ret
+;;