From ca92d5ab93f2ee63ff416a096fdbfa569a64c717 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 16 May 2019 14:27:06 +0200
Subject: sdiv seems to work, udiv/umod/smod BOGUS

---
 mppa_k1c/SelectOp.vp             | 12 ++--------
 mppa_k1c/SelectOpproof.v         | 18 ++++++++++++--
 runtime/mppa_k1c/i64_sdiv.c      | 10 --------
 runtime/mppa_k1c/i64_smod.c      | 40 -------------------------------
 runtime/mppa_k1c/vararg.S        | 51 ++++++++++++++++++++++++++++++++++++++++
 test/monniaux/division/sum_div.c | 18 --------------
 6 files changed, 69 insertions(+), 80 deletions(-)
 delete mode 100644 test/monniaux/division/sum_div.c

diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp
index aac3010e..6adcebe5 100644
--- a/mppa_k1c/SelectOp.vp
+++ b/mppa_k1c/SelectOp.vp
@@ -423,18 +423,10 @@ Definition mods_base (e1: expr) (e2: expr) :=
   Eexternal i32_smod sig_ii_i (e1 ::: e2 ::: Enil).
 
 Definition divu_base (e1: expr) (e2: expr) :=
-  Eop Olowlong
-     ((Eexternal i64_udiv sig_ll_l
-       ((Eop Ocast32unsigned (e1 ::: Enil)):::
-       (Eop Ocast32unsigned (e2 ::: Enil))::: Enil))
-      :::Enil).
+  Eexternal i32_udiv sig_ii_i (e1 ::: e2 ::: Enil).
   
 Definition modu_base (e1: expr) (e2: expr) :=
-  Eop Olowlong
-     ((Eexternal i64_umod sig_ll_l
-       ((Eop Ocast32unsigned (e1 ::: Enil)):::
-       (Eop Ocast32unsigned (e2 ::: Enil))::: Enil))
-      :::Enil).
+  Eexternal i32_umod sig_ii_i (e1 ::: e2 ::: Enil).
 
 Definition shrximm (e1: expr) (n2: int) :=
   if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil).
diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v
index d22725d5..22eecfad 100644
--- a/mppa_k1c/SelectOpproof.v
+++ b/mppa_k1c/SelectOpproof.v
@@ -872,6 +872,12 @@ Theorem eval_divu_base:
     Val.divu x y = Some z ->
     exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v.
 Proof.
+  intros; unfold divu_base.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+Qed.
+
+(* For using 64-bit unsigned division for 32-bit
+
   intros until z.
   intros Hax Hby Hdiv. unfold divu_base.
   pose proof (divu_is_divlu x y) as DIVU.
@@ -891,7 +897,8 @@ Proof.
   }
   congruence.
 Qed.
-
+ *)
+  
 Theorem eval_modu_base:
   forall le a b x y z,
     eval_expr ge sp e m le a x ->
@@ -899,6 +906,12 @@ Theorem eval_modu_base:
     Val.modu x y = Some z ->
     exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v.
 Proof.
+  intros; unfold modu_base.
+  econstructor; split. eapply eval_helper_2; eauto. DeclHelper. UseHelper. auto.
+Qed.
+
+(* for using 64-bit unsigned modulo for 32-bit
+
   intros until z.
   intros Hax Hby Hmod. unfold modu_base.
   pose proof (modu_is_modlu x y) as MODU.
@@ -918,7 +931,8 @@ Proof.
   }
   congruence.
 Qed.
-
+ *)
+  
 Theorem eval_shrximm:
   forall le a n x z,
     eval_expr ge sp e m le a x ->
diff --git a/runtime/mppa_k1c/i64_sdiv.c b/runtime/mppa_k1c/i64_sdiv.c
index 9feab791..809f2b1c 100644
--- a/runtime/mppa_k1c/i64_sdiv.c
+++ b/runtime/mppa_k1c/i64_sdiv.c
@@ -1,15 +1,5 @@
 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);
-}
-
 #include <mppa_bare_runtime/k1c/registers.h>
 
 /* DM FIXME this is for floating point */
diff --git a/runtime/mppa_k1c/i64_smod.c b/runtime/mppa_k1c/i64_smod.c
index 26ffb39b..e69de29b 100644
--- a/runtime/mppa_k1c/i64_smod.c
+++ b/runtime/mppa_k1c/i64_smod.c
@@ -1,40 +0,0 @@
-#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/vararg.S b/runtime/mppa_k1c/vararg.S
index 9e23e0b3..2050c9aa 100644
--- a/runtime/mppa_k1c/vararg.S
+++ b/runtime/mppa_k1c/vararg.S
@@ -52,3 +52,54 @@ __compcert_acswapw:
 	sq	0[$r0] = $r2r3
 	ret
 	;;
+
+	.globl __compcert_i32_sdiv
+	.globl __compcert_i32_smod
+	.globl __compcert_i32_udiv
+	.globl __compcert_i32_umod
+__compcert_i32_sdiv:
+__compcert_i32_smod:
+__compcert_i32_udiv:
+__compcert_i32_umod:
+	sxwd $r0 = $r0
+	;; /* Can't issue next in the same bundle */
+	sxwd $r1 = $r1
+	;; /* Can't issue next in the same bundle */
+	make $r2 = 0x3ff0000000000000
+	addd $r12 = $r12, -16
+	;;
+	floatd.rn.s $r0 = $r0, 0
+	;;
+	floatd.rn.s $r3 = $r1, 0
+	;;
+	floatw.rn.s $r1 = $r1, 0
+	;;
+	;;
+#APP
+# 16 "clock_int_div2.c" 1
+	finvw $r1=$r1
+# 0 "" 2
+	;;
+
+	;;
+#NO_APP
+	fwidenlwd $r1 = $r1
+	;;
+	fmuld $r0 = $r0, $r1
+	;;
+	ffmsd $r2 = $r1, $r3
+	;;
+	sd 8[$r12] = $r0
+	;;
+	ld $r1 = 8[$r12]
+	;;
+	ffmad $r1 = $r2, $r0
+	;;
+	ffmad $r0 = $r2, $r1
+	;;
+	sd 8[$r12] = $r1
+	addd $r12 = $r12, 16
+	;;
+	fixedd.rz $r0 = $r0, 0
+	ret
+	;;
diff --git a/test/monniaux/division/sum_div.c b/test/monniaux/division/sum_div.c
deleted file mode 100644
index 87256922..00000000
--- a/test/monniaux/division/sum_div.c
+++ /dev/null
@@ -1,18 +0,0 @@
-#include <stdio.h>
-#include <stdlib.h>
-#include "../clock.h"
- 
-int main(int argc, char **argv) {
-  unsigned modulus = argc < 2 ? 3371 : atoi(argv[1]);
-  clock_prepare();
-  clock_start();
-  unsigned total=0, total_mod=0;
-  for(int i=0; i<1000; i++) {
-    total += i;
-    total_mod = (total_mod + i)%modulus;
-  }
-  clock_stop();
-  print_total_clock();
-  printf("%u %u %d\n", total, total_mod, total%modulus == total_mod);
-  return 0;
-}
-- 
cgit 


From acc7b444ba2ccdf7273bb0da128a6cdfe392dc5d Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 16 May 2019 14:29:15 +0200
Subject: simplify sdiv code

---
 runtime/mppa_k1c/vararg.S | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/runtime/mppa_k1c/vararg.S b/runtime/mppa_k1c/vararg.S
index 2050c9aa..e0b73811 100644
--- a/runtime/mppa_k1c/vararg.S
+++ b/runtime/mppa_k1c/vararg.S
@@ -62,7 +62,6 @@ __compcert_i32_smod:
 __compcert_i32_udiv:
 __compcert_i32_umod:
 	sxwd $r0 = $r0
-	;; /* Can't issue next in the same bundle */
 	sxwd $r1 = $r1
 	;; /* Can't issue next in the same bundle */
 	make $r2 = 0x3ff0000000000000
@@ -74,15 +73,8 @@ __compcert_i32_umod:
 	;;
 	floatw.rn.s $r1 = $r1, 0
 	;;
-	;;
-#APP
-# 16 "clock_int_div2.c" 1
 	finvw $r1=$r1
-# 0 "" 2
-	;;
-
 	;;
-#NO_APP
 	fwidenlwd $r1 = $r1
 	;;
 	fmuld $r0 = $r0, $r1
-- 
cgit 


From a36a8c77b67ad1e054cb7aabae53817e98c00088 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 16 May 2019 14:31:17 +0200
Subject: simplify sdiv code

---
 runtime/mppa_k1c/vararg.S | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/runtime/mppa_k1c/vararg.S b/runtime/mppa_k1c/vararg.S
index e0b73811..d3626c25 100644
--- a/runtime/mppa_k1c/vararg.S
+++ b/runtime/mppa_k1c/vararg.S
@@ -80,10 +80,7 @@ __compcert_i32_umod:
 	fmuld $r0 = $r0, $r1
 	;;
 	ffmsd $r2 = $r1, $r3
-	;;
-	sd 8[$r12] = $r0
-	;;
-	ld $r1 = 8[$r12]
+	copyd $r1 = $r0
 	;;
 	ffmad $r1 = $r2, $r0
 	;;
-- 
cgit 


From aecc44ba24c68b03f5cd978ce193ac9b7bc9bb42 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 16 May 2019 14:32:51 +0200
Subject: simplify sdiv

---
 runtime/mppa_k1c/vararg.S | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/runtime/mppa_k1c/vararg.S b/runtime/mppa_k1c/vararg.S
index d3626c25..e7b05893 100644
--- a/runtime/mppa_k1c/vararg.S
+++ b/runtime/mppa_k1c/vararg.S
@@ -63,9 +63,7 @@ __compcert_i32_udiv:
 __compcert_i32_umod:
 	sxwd $r0 = $r0
 	sxwd $r1 = $r1
-	;; /* Can't issue next in the same bundle */
 	make $r2 = 0x3ff0000000000000
-	addd $r12 = $r12, -16
 	;;
 	floatd.rn.s $r0 = $r0, 0
 	;;
@@ -86,9 +84,6 @@ __compcert_i32_umod:
 	;;
 	ffmad $r0 = $r2, $r1
 	;;
-	sd 8[$r12] = $r1
-	addd $r12 = $r12, 16
-	;;
 	fixedd.rz $r0 = $r0, 0
 	ret
 	;;
-- 
cgit 


From be0b9e66ce1fd71830d9316a13afc64d9a71552e Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 16 May 2019 14:47:28 +0200
Subject: udiv

---
 runtime/mppa_k1c/vararg.S | 29 ++++++++++++++++++++++++++++-
 1 file changed, 28 insertions(+), 1 deletion(-)

diff --git a/runtime/mppa_k1c/vararg.S b/runtime/mppa_k1c/vararg.S
index e7b05893..9869eb0b 100644
--- a/runtime/mppa_k1c/vararg.S
+++ b/runtime/mppa_k1c/vararg.S
@@ -59,7 +59,6 @@ __compcert_acswapw:
 	.globl __compcert_i32_umod
 __compcert_i32_sdiv:
 __compcert_i32_smod:
-__compcert_i32_udiv:
 __compcert_i32_umod:
 	sxwd $r0 = $r0
 	sxwd $r1 = $r1
@@ -87,3 +86,31 @@ __compcert_i32_umod:
 	fixedd.rz $r0 = $r0, 0
 	ret
 	;;
+
+__compcert_i32_udiv:
+	zxwd $r0 = $r0
+	zxwd $r1 = $r1
+	make $r2 = 0x3ff0000000000000
+	;;
+	floatud.rn.s $r0 = $r0, 0
+	;;
+	floatud.rn.s $r3 = $r1, 0
+	;;
+	floatuw.rn.s $r1 = $r1, 0
+	;;
+	finvw $r1=$r1
+	;;
+	fwidenlwd $r1 = $r1
+	;;
+	fmuld $r0 = $r0, $r1
+	;;
+	ffmsd $r2 = $r1, $r3
+	copyd $r1 = $r0
+	;;
+	ffmad $r1 = $r2, $r0
+	;;
+	ffmad $r0 = $r2, $r1
+	;;
+	fixedud.rz $r0 = $r0, 0
+	ret
+	;;
-- 
cgit 


From 7d59276032275776e1f37dfb99ad2f60bc6ab639 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 16 May 2019 14:52:35 +0200
Subject: umod

---
 runtime/mppa_k1c/vararg.S | 34 +++++++++++++++++++++++++++++++++-
 1 file changed, 33 insertions(+), 1 deletion(-)

diff --git a/runtime/mppa_k1c/vararg.S b/runtime/mppa_k1c/vararg.S
index 9869eb0b..184bd3f8 100644
--- a/runtime/mppa_k1c/vararg.S
+++ b/runtime/mppa_k1c/vararg.S
@@ -58,7 +58,6 @@ __compcert_acswapw:
 	.globl __compcert_i32_udiv
 	.globl __compcert_i32_umod
 __compcert_i32_sdiv:
-__compcert_i32_smod:
 __compcert_i32_umod:
 	sxwd $r0 = $r0
 	sxwd $r1 = $r1
@@ -87,6 +86,38 @@ __compcert_i32_umod:
 	ret
 	;;
 
+__compcert_i32_smod:
+	sxwd $r4 = $r0
+	sxwd $r5 = $r1
+	make $r2 = 0x3ff0000000000000
+	;;
+	copyd $r0 = $r4
+	copyd $r1 = $r5
+	floatd.rn.s $r4 = $r4, 0
+	;;
+	floatd.rn.s $r3 = $r5, 0
+	;;
+	floatw.rn.s $r5 = $r5, 0
+	;;
+	finvw $r5=$r5
+	;;
+	fwidenlwd $r5 = $r5
+	;;
+	fmuld $r4 = $r4, $r5
+	;;
+	ffmsd $r2 = $r5, $r3
+	copyd $r5 = $r4
+	;;
+	ffmad $r5 = $r2, $r4
+	;;
+	ffmad $r4 = $r2, $r5
+	;;
+	fixedd.rz $r4 = $r4, 0
+	;;
+	msbfd $r0 = $r1, $r4
+	ret
+	;;
+
 __compcert_i32_udiv:
 	zxwd $r0 = $r0
 	zxwd $r1 = $r1
@@ -112,5 +143,6 @@ __compcert_i32_udiv:
 	ffmad $r0 = $r2, $r1
 	;;
 	fixedud.rz $r0 = $r0, 0
+	;; 
 	ret
 	;;
-- 
cgit 


From 742cd4505a6646247bf0740ea4e6ab779972a554 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 16 May 2019 14:54:17 +0200
Subject: sdiv, smod, udiv, umod through fast routines

---
 runtime/mppa_k1c/vararg.S | 33 ++++++++++++++++++++++++++++++++-
 1 file changed, 32 insertions(+), 1 deletion(-)

diff --git a/runtime/mppa_k1c/vararg.S b/runtime/mppa_k1c/vararg.S
index 184bd3f8..5804c707 100644
--- a/runtime/mppa_k1c/vararg.S
+++ b/runtime/mppa_k1c/vararg.S
@@ -58,7 +58,6 @@ __compcert_acswapw:
 	.globl __compcert_i32_udiv
 	.globl __compcert_i32_umod
 __compcert_i32_sdiv:
-__compcert_i32_umod:
 	sxwd $r0 = $r0
 	sxwd $r1 = $r1
 	make $r2 = 0x3ff0000000000000
@@ -146,3 +145,35 @@ __compcert_i32_udiv:
 	;; 
 	ret
 	;;
+
+__compcert_i32_umod:
+	zxwd $r4 = $r0
+	zxwd $r5 = $r1
+	make $r2 = 0x3ff0000000000000
+	;;
+	copyd $r0 = $r4
+	copyd $r1 = $r5
+	floatud.rn.s $r4 = $r4, 0
+	;;
+	floatud.rn.s $r3 = $r5, 0
+	;;
+	floatuw.rn.s $r5 = $r5, 0
+	;;
+	finvw $r5=$r5
+	;;
+	fwidenlwd $r5 = $r5
+	;;
+	fmuld $r4 = $r4, $r5
+	;;
+	ffmsd $r2 = $r5, $r3
+	copyd $r5 = $r4
+	;;
+	ffmad $r5 = $r2, $r4
+	;;
+	ffmad $r4 = $r2, $r5
+	;;
+	fixedud.rz $r4 = $r4, 0
+	;;
+	msbfd $r0 = $r1, $r4
+	ret
+	;;
-- 
cgit 


From b0ec7472890babc8c439984d75c14f2b4486416a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Tue, 21 May 2019 15:32:45 +0200
Subject: new routines for 32-bit division

---
 runtime/Makefile              |   5 +-
 runtime/mppa_k1c/i32_divmod.S | 120 ++++++++++++++++++++++++++++++++++++++++++
 runtime/mppa_k1c/i64_sdiv.c   |   2 -
 3 files changed, 122 insertions(+), 5 deletions(-)
 create mode 100644 runtime/mppa_k1c/i32_divmod.S

diff --git a/runtime/Makefile b/runtime/Makefile
index 1258d941..2448279e 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -23,9 +23,8 @@ 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
+OBJS=i64_umod.o i64_udiv.o i64_udivmod.o i64_sdiv.o i64_smod.o i32_divmod.o \
+                 vararg.o
 # Missing: i64_utod.o i64_utof.o i64_stod.o i64_stof.o
 DOMAKE:=$(shell (cd mppa_k1c && make))
 else
diff --git a/runtime/mppa_k1c/i32_divmod.S b/runtime/mppa_k1c/i32_divmod.S
new file mode 100644
index 00000000..d5a4c2ca
--- /dev/null
+++ b/runtime/mppa_k1c/i32_divmod.S
@@ -0,0 +1,120 @@
+/* K1C
+32-bit unsigned/signed integer division/modulo (udiv5)
+
+D. Monniaux, CNRS, VERIMAG */
+
+	
+	.globl __compcert_i32_sdiv
+__compcert_i32_sdiv:
+	compw.lt $r2 = $r0, 0
+	compw.lt $r3 = $r1, 0
+	absw $r0 = $r0
+	absw $r1 = $r1
+	;;
+	xord $r2 = $r2, $r3
+	make $r3 = 0
+	goto __compcert_i32_divmod
+	;;
+	
+	.globl __compcert_i32_smod
+__compcert_i32_smod:
+	compw.lt $r2 = $r0, 0
+	absw $r0 = $r0
+	absw $r1 = $r1
+	make $r3 = 1
+	goto __compcert_i32_divmod
+	;;
+	
+	.globl __compcert_i32_umod
+__compcert_i32_umod:
+	make $r2 = 0
+	make $r3 = 1
+	goto __compcert_i32_divmod
+	;;
+
+	.globl __compcert_i32_udiv
+__compcert_i32_udiv:
+	make $r2 = 0
+	make $r3 = 0
+	;;
+
+/*
+r0 : a
+r1 : b
+r2 : negate result?
+r3 : return mod?
+*/
+
+	.globl __compcert_i32_divmod
+__compcert_i32_divmod:
+	zxwd $r7 = $r1
+	zxwd $r1 = $r0
+#ifndef NO_SHORTCUT
+	compw.ltu $r8 = $r0, $r1
+	cb.weqz $r1? .ERR # return 0 if divide by 0
+#endif
+	;;
+# a in r1, b in r7
+	floatud.rn $r5 = $r7, 0
+#ifndef NO_SHORTCUT
+	compd.eq $r8 = $r7, 1
+	cb.wnez $r8? .LESS # shortcut if a < b
+#endif
+	;;
+# b (double) in r5
+	make $r6 = 0x3ff0000000000000 # 1.0
+	fnarrowdw.rn $r11 = $r5
+#	cb.wnez $r8, .RET1 # if b=1
+	;;
+# b (single) in r11
+	floatud.rn $r10 = $r1, 0
+	finvw.rn $r11 = $r11
+	;;
+	fwidenlwd $r11 = $r11
+	;;
+# invb0 in r11
+	copyd $r9 = $r11
+	ffmsd.rn $r6 = $r11, $r5
+# alpha in r6
+	;;
+	ffmad.rn $r9 = $r11, $r6
+# 1/b in r9
+	;;
+	fmuld.rn $r0 = $r10, $r9
+# a/b in r1
+	;;
+	fixedud.rn $r0 = $r0, 0
+	;;
+	msbfd $r1 = $r0, $r7
+	;;
+	addd $r6 = $r0, -1
+	addd $r8 = $r1, $r7
+	;;
+	cmoved.dltz $r1? $r0 = $r6
+	cmoved.dltz $r1? $r1 = $r8
+	;;
+	negw $r4 = $r0
+	negw $r5 = $r1
+	;;
+	cmoved.wnez $r2? $r0 = $r4
+	cmoved.wnez $r2? $r1 = $r5
+	;;
+.END:
+	cmoved.wnez $r3? $r0 = $r1
+	ret
+	;;
+#ifndef NO_SHORTCUT
+
+.LESS:
+	make $r0 = 0
+	negw $r5 = $r1
+	;;
+	cmoved.wnez $r2? $r1 = $r5
+	goto .END
+	;;
+	
+.ERR:
+	make $r0 = 0
+	ret
+	;;
+#endif
diff --git a/runtime/mppa_k1c/i64_sdiv.c b/runtime/mppa_k1c/i64_sdiv.c
index 809f2b1c..18a2c46c 100644
--- a/runtime/mppa_k1c/i64_sdiv.c
+++ b/runtime/mppa_k1c/i64_sdiv.c
@@ -1,5 +1,3 @@
-extern long __divdi3 (long a, long b);
-
 #include <mppa_bare_runtime/k1c/registers.h>
 
 /* DM FIXME this is for floating point */
-- 
cgit 


From 6141d184274db971f553130703554f0b1b66ef1b Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 29 May 2019 10:20:24 +0200
Subject: various fixes

---
 configure                   | 2 +-
 runtime/mppa_k1c/i64_sdiv.c | 2 ++
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/configure b/configure
index 43c90b47..52fffa63 100755
--- a/configure
+++ b/configure
@@ -461,7 +461,7 @@ if test "$arch" = "mppa_k1c"; then
   libdir="$HOME/.usr/lib"
   clinker_options="$model_options -L$libdir -Wl,-rpath=$libdir"
   cprepro="$k1base-gcc"
-  cprepro_options="$model_options -D __K1C_$osupper__ -std=c99 -E -include ccomp_k1c_fixes.h"
+  cprepro_options="$model_options -D __K1C_${osupper}__ -std=c99 -E -include ccomp_k1c_fixes.h"
   libmath="-lm"
   system="linux"
 fi
diff --git a/runtime/mppa_k1c/i64_sdiv.c b/runtime/mppa_k1c/i64_sdiv.c
index d1d268c4..b53294ec 100644
--- a/runtime/mppa_k1c/i64_sdiv.c
+++ b/runtime/mppa_k1c/i64_sdiv.c
@@ -10,6 +10,7 @@
 #include <mppa_bare_runtime/k1c/registers.h>
 #endif
 
+#ifdef COMPCERT_FE_EXCEPT
 /* DM FIXME this is for floating point */
 int fetestexcept(int excepts) {
   int mask = (K1_SFR_CS_IO_MASK | K1_SFR_CS_DZ_MASK | K1_SFR_CS_OV_MASK | K1_SFR_CS_UN_MASK | K1_SFR_CS_IN_MASK) & excepts;
@@ -22,3 +23,4 @@ int feclearexcept(int excepts) {
   __builtin_k1_wfxl(K1_SFR_CS, mask);
   return 0;
 }
+#endif
-- 
cgit 


From aa3ff942fb4944242c7a2398592b7e3d33f6c9dc Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 29 May 2019 10:35:01 +0200
Subject: fixes

---
 runtime/mppa_k1c/i64_sdiv.c | 1 +
 1 file changed, 1 insertion(+)

diff --git a/runtime/mppa_k1c/i64_sdiv.c b/runtime/mppa_k1c/i64_sdiv.c
index b53294ec..9fac8ff9 100644
--- a/runtime/mppa_k1c/i64_sdiv.c
+++ b/runtime/mppa_k1c/i64_sdiv.c
@@ -10,6 +10,7 @@
 #include <mppa_bare_runtime/k1c/registers.h>
 #endif
 
+/* #define COMPCERT_FE_EXCEPT */
 #ifdef COMPCERT_FE_EXCEPT
 /* DM FIXME this is for floating point */
 int fetestexcept(int excepts) {
-- 
cgit 


From 11cd0ace897752ef7ca33609aa1250ca1597185b Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 29 May 2019 11:14:46 +0200
Subject: arranging for selection of divisor as option

---
 mppa_k1c/TargetPrinter.ml      |  48 ++++++++++++++--
 runtime/Makefile               |   5 +-
 runtime/mppa_k1c/i32_divmod.S  |  26 ++++-----
 runtime/mppa_k1c/i64_sdiv.c    |  12 +++-
 runtime/mppa_k1c/i64_smod.c    |   5 ++
 runtime/mppa_k1c/i64_udiv.c    |   6 ++
 runtime/mppa_k1c/i64_udivmod.c |   2 +
 runtime/mppa_k1c/i64_umod.c    |   6 ++
 runtime/mppa_k1c/vararg.S      | 125 -----------------------------------------
 9 files changed, 89 insertions(+), 146 deletions(-)

diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 96779517..4dc4b7c2 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -34,11 +34,51 @@ module Target (*: TARGET*) =
 
     let comment = "#"
 
+    type idiv_function_kind =
+      | Idiv_system
+      | Idiv_stsud
+      | Idiv_fp;;
+
+    let idiv_function_kind_32bit () = Idiv_fp;;
+    let idiv_function_kind_64bit () = Idiv_stsud;;
+    
     let subst_symbol = function
-        "__compcert_i64_udiv" -> "__udivdi3"
-      | "__compcert_i64_sdiv" -> "__divdi3"
-      | "__compcert_i64_umod" -> "__umoddi3"
-      | "__compcert_i64_smod" -> "__moddi3"
+        "__compcert_i64_udiv" ->
+        (match idiv_function_kind_64bit () with
+         | Idiv_system | Idiv_fp -> "__udivdi3"
+         | Idiv_stsud -> "__compcert_i64_udiv_stsud")
+      | "__compcert_i64_sdiv" ->
+        (match idiv_function_kind_64bit() with
+         | Idiv_system | Idiv_fp -> "__divdi3"
+         | Idiv_stsud -> "__compcert_i64_sdiv_stsud")
+      | "__compcert_i64_umod" ->
+        (match idiv_function_kind_64bit() with
+         | Idiv_system | Idiv_fp -> "__umoddi3"
+         | Idiv_stsud -> "__compcert_i64_umod_stsud")
+      | "__compcert_i64_smod" ->
+        (match idiv_function_kind_64bit() with
+         | Idiv_system | Idiv_fp -> "__moddi3"
+         | Idiv_stsud -> "__compcert_i64_stsud")
+      | "__compcert_i32_sdiv" as s ->
+        (match idiv_function_kind_32bit() with
+         | Idiv_system -> s
+         | Idiv_fp -> "__compcert_i32_sdiv_fp"
+         | Idiv_stsud -> "__compcert_i32_sdiv_stsud")
+      | "__compcert_i32_udiv" as s ->
+        (match idiv_function_kind_32bit() with
+         | Idiv_system -> s
+         | Idiv_fp -> "__compcert_i32_udiv_fp"
+         | Idiv_stsud -> "__compcert_i32_udiv_stsud")
+      | "__compcert_i32_smod" as s ->
+        (match idiv_function_kind_32bit() with
+         | Idiv_system -> s
+         | Idiv_fp -> "__compcert_i32_smod_fp"
+         | Idiv_stsud -> "__compcert_i32_smod_stsud")
+      | "__compcert_i32_umod" as s ->
+        (match idiv_function_kind_32bit() with
+         | Idiv_system -> s
+         | Idiv_fp -> "__compcert_i32_umod_fp"
+         | Idiv_stsud -> "__compcert_i32_umod_stsud")
       | "__compcert_f64_div" -> "__divdf3"
       | "__compcert_f32_div" -> "__divsf3"
       | x -> x;;
diff --git a/runtime/Makefile b/runtime/Makefile
index 2448279e..6bc3e7ea 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -23,8 +23,9 @@ 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 i32_divmod.o \
-                 vararg.o
+OBJS=i64_umod.o i64_udiv.o i64_udivmod.o i64_sdiv.o i64_smod.o \
+     i64_udivmod_stsud.o i32_divmod.o \
+     vararg.o
 # Missing: i64_utod.o i64_utof.o i64_stod.o i64_stof.o
 DOMAKE:=$(shell (cd mppa_k1c && make))
 else
diff --git a/runtime/mppa_k1c/i32_divmod.S b/runtime/mppa_k1c/i32_divmod.S
index d5a4c2ca..8dd9481c 100644
--- a/runtime/mppa_k1c/i32_divmod.S
+++ b/runtime/mppa_k1c/i32_divmod.S
@@ -4,8 +4,8 @@
 D. Monniaux, CNRS, VERIMAG */
 
 	
-	.globl __compcert_i32_sdiv
-__compcert_i32_sdiv:
+	.globl __compcert_i32_sdiv_fp
+__compcert_i32_sdiv_fp:
 	compw.lt $r2 = $r0, 0
 	compw.lt $r3 = $r1, 0
 	absw $r0 = $r0
@@ -13,27 +13,27 @@ __compcert_i32_sdiv:
 	;;
 	xord $r2 = $r2, $r3
 	make $r3 = 0
-	goto __compcert_i32_divmod
+	goto __compcert_i32_divmod_fp
 	;;
 	
-	.globl __compcert_i32_smod
-__compcert_i32_smod:
+	.globl __compcert_i32_smod_fp
+__compcert_i32_smod_fp:
 	compw.lt $r2 = $r0, 0
 	absw $r0 = $r0
 	absw $r1 = $r1
 	make $r3 = 1
-	goto __compcert_i32_divmod
+	goto __compcert_i32_divmod_fp
 	;;
 	
-	.globl __compcert_i32_umod
-__compcert_i32_umod:
+	.globl __compcert_i32_umod_fp
+__compcert_i32_umod_fp:
 	make $r2 = 0
 	make $r3 = 1
-	goto __compcert_i32_divmod
+	goto __compcert_i32_divmod_fp
 	;;
 
-	.globl __compcert_i32_udiv
-__compcert_i32_udiv:
+	.globl __compcert_i32_udiv_fp
+__compcert_i32_udiv_fp:
 	make $r2 = 0
 	make $r3 = 0
 	;;
@@ -45,8 +45,8 @@ r2 : negate result?
 r3 : return mod?
 */
 
-	.globl __compcert_i32_divmod
-__compcert_i32_divmod:
+	.globl __compcert_i32_divmod_fp
+__compcert_i32_divmod_fp:
 	zxwd $r7 = $r1
 	zxwd $r1 = $r0
 #ifndef NO_SHORTCUT
diff --git a/runtime/mppa_k1c/i64_sdiv.c b/runtime/mppa_k1c/i64_sdiv.c
index 9fac8ff9..df308736 100644
--- a/runtime/mppa_k1c/i64_sdiv.c
+++ b/runtime/mppa_k1c/i64_sdiv.c
@@ -1,4 +1,14 @@
+extern long __divdi3 (long a, long b);
+
+int i32_sdiv (int a, int b)
+{
+  return __divdi3 (a, b);
+}
+
+/* #define COMPCERT_FE_EXCEPT */
+#ifdef COMPCERT_FE_EXCEPT
 #ifdef __K1C_COS__
+
 #include <hal/cos_registers.h>
 #define K1_SFR_CS_IO_MASK COS_SFR_CS_IO_MASK
 #define K1_SFR_CS_DZ_MASK COS_SFR_CS_DZ_MASK
@@ -10,8 +20,6 @@
 #include <mppa_bare_runtime/k1c/registers.h>
 #endif
 
-/* #define COMPCERT_FE_EXCEPT */
-#ifdef COMPCERT_FE_EXCEPT
 /* DM FIXME this is for floating point */
 int fetestexcept(int excepts) {
   int mask = (K1_SFR_CS_IO_MASK | K1_SFR_CS_DZ_MASK | K1_SFR_CS_OV_MASK | K1_SFR_CS_UN_MASK | K1_SFR_CS_IN_MASK) & excepts;
diff --git a/runtime/mppa_k1c/i64_smod.c b/runtime/mppa_k1c/i64_smod.c
index e69de29b..3371eecf 100644
--- a/runtime/mppa_k1c/i64_smod.c
+++ b/runtime/mppa_k1c/i64_smod.c
@@ -0,0 +1,5 @@
+extern long __moddi3 (long a, long b);
+int i32_smod (int a, int b)
+{
+  return __moddi3 (a, b);
+}
diff --git a/runtime/mppa_k1c/i64_udiv.c b/runtime/mppa_k1c/i64_udiv.c
index e69de29b..75f4bbf5 100644
--- a/runtime/mppa_k1c/i64_udiv.c
+++ b/runtime/mppa_k1c/i64_udiv.c
@@ -0,0 +1,6 @@
+extern unsigned long __udivdi3 (unsigned long a, unsigned long b);
+
+unsigned i32_udiv (unsigned a, unsigned b)
+{
+  return __udivdi3 (a, b);
+}
diff --git a/runtime/mppa_k1c/i64_udivmod.c b/runtime/mppa_k1c/i64_udivmod.c
index 74b39874..ca48cd87 100644
--- a/runtime/mppa_k1c/i64_udivmod.c
+++ b/runtime/mppa_k1c/i64_udivmod.c
@@ -1,3 +1,4 @@
+#if 0
 /* THIS IS THE PREVIOUS VERSION, USED ON BOSTAN AND ANDEY */
 unsigned long long
 udivmoddi4(unsigned long long num, unsigned long long den, int modwanted)
@@ -26,3 +27,4 @@ udivmoddi4(unsigned long long num, unsigned long long den, int modwanted)
 
     return modwanted ? r : q;
 }
+#endif
diff --git a/runtime/mppa_k1c/i64_umod.c b/runtime/mppa_k1c/i64_umod.c
index e69de29b..59e35960 100644
--- a/runtime/mppa_k1c/i64_umod.c
+++ b/runtime/mppa_k1c/i64_umod.c
@@ -0,0 +1,6 @@
+extern unsigned long __umoddi3 (unsigned long a, unsigned long b);
+
+unsigned i32_umod (unsigned a, unsigned b)
+{
+  return __umoddi3 (a, b);
+}
diff --git a/runtime/mppa_k1c/vararg.S b/runtime/mppa_k1c/vararg.S
index 5804c707..9e23e0b3 100644
--- a/runtime/mppa_k1c/vararg.S
+++ b/runtime/mppa_k1c/vararg.S
@@ -52,128 +52,3 @@ __compcert_acswapw:
 	sq	0[$r0] = $r2r3
 	ret
 	;;
-
-	.globl __compcert_i32_sdiv
-	.globl __compcert_i32_smod
-	.globl __compcert_i32_udiv
-	.globl __compcert_i32_umod
-__compcert_i32_sdiv:
-	sxwd $r0 = $r0
-	sxwd $r1 = $r1
-	make $r2 = 0x3ff0000000000000
-	;;
-	floatd.rn.s $r0 = $r0, 0
-	;;
-	floatd.rn.s $r3 = $r1, 0
-	;;
-	floatw.rn.s $r1 = $r1, 0
-	;;
-	finvw $r1=$r1
-	;;
-	fwidenlwd $r1 = $r1
-	;;
-	fmuld $r0 = $r0, $r1
-	;;
-	ffmsd $r2 = $r1, $r3
-	copyd $r1 = $r0
-	;;
-	ffmad $r1 = $r2, $r0
-	;;
-	ffmad $r0 = $r2, $r1
-	;;
-	fixedd.rz $r0 = $r0, 0
-	ret
-	;;
-
-__compcert_i32_smod:
-	sxwd $r4 = $r0
-	sxwd $r5 = $r1
-	make $r2 = 0x3ff0000000000000
-	;;
-	copyd $r0 = $r4
-	copyd $r1 = $r5
-	floatd.rn.s $r4 = $r4, 0
-	;;
-	floatd.rn.s $r3 = $r5, 0
-	;;
-	floatw.rn.s $r5 = $r5, 0
-	;;
-	finvw $r5=$r5
-	;;
-	fwidenlwd $r5 = $r5
-	;;
-	fmuld $r4 = $r4, $r5
-	;;
-	ffmsd $r2 = $r5, $r3
-	copyd $r5 = $r4
-	;;
-	ffmad $r5 = $r2, $r4
-	;;
-	ffmad $r4 = $r2, $r5
-	;;
-	fixedd.rz $r4 = $r4, 0
-	;;
-	msbfd $r0 = $r1, $r4
-	ret
-	;;
-
-__compcert_i32_udiv:
-	zxwd $r0 = $r0
-	zxwd $r1 = $r1
-	make $r2 = 0x3ff0000000000000
-	;;
-	floatud.rn.s $r0 = $r0, 0
-	;;
-	floatud.rn.s $r3 = $r1, 0
-	;;
-	floatuw.rn.s $r1 = $r1, 0
-	;;
-	finvw $r1=$r1
-	;;
-	fwidenlwd $r1 = $r1
-	;;
-	fmuld $r0 = $r0, $r1
-	;;
-	ffmsd $r2 = $r1, $r3
-	copyd $r1 = $r0
-	;;
-	ffmad $r1 = $r2, $r0
-	;;
-	ffmad $r0 = $r2, $r1
-	;;
-	fixedud.rz $r0 = $r0, 0
-	;; 
-	ret
-	;;
-
-__compcert_i32_umod:
-	zxwd $r4 = $r0
-	zxwd $r5 = $r1
-	make $r2 = 0x3ff0000000000000
-	;;
-	copyd $r0 = $r4
-	copyd $r1 = $r5
-	floatud.rn.s $r4 = $r4, 0
-	;;
-	floatud.rn.s $r3 = $r5, 0
-	;;
-	floatuw.rn.s $r5 = $r5, 0
-	;;
-	finvw $r5=$r5
-	;;
-	fwidenlwd $r5 = $r5
-	;;
-	fmuld $r4 = $r4, $r5
-	;;
-	ffmsd $r2 = $r5, $r3
-	copyd $r5 = $r4
-	;;
-	ffmad $r5 = $r2, $r4
-	;;
-	ffmad $r4 = $r2, $r5
-	;;
-	fixedud.rz $r4 = $r4, 0
-	;;
-	msbfd $r0 = $r1, $r4
-	ret
-	;;
-- 
cgit 


From d075968e1e516ab80460afce57c9bcc15d206c19 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 29 May 2019 11:43:29 +0200
Subject: added -fdiv-i32 and -fdiv-i64 options

---
 driver/Clflags.ml         |  3 +++
 driver/Driver.ml          | 12 +++++++++---
 mppa_k1c/TargetPrinter.ml | 10 ++++++++--
 3 files changed, 20 insertions(+), 5 deletions(-)

diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index b1afab6f..fd5f0e68 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -71,3 +71,6 @@ let option_fglobaladdrtmp = ref false
 let option_fglobaladdroffset = ref false
 let option_fxsaddr = ref true  
 let option_coalesce_mem = ref true  
+
+let option_div_i32 = ref "stsud"
+let option_div_i64 = ref "stsud" 
diff --git a/driver/Driver.ml b/driver/Driver.ml
index cfafcaa3..314cf31c 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -265,9 +265,13 @@ let num_input_files = ref 0
 let cmdline_actions =
   let f_opt name ref =
     [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in
-  let f_opt_str name ref strref =
+  let f_opt_str name ref strref default =
     [Exact("-f" ^ name ^ "="), String 
-      (fun s -> (strref := (if s == "" then "list" else s)); ref := true)
+      (fun s -> (strref := (if s == "" then default else s)); ref := true)
+     ] in
+  let f_str name strref default =
+    [Exact("-f" ^ name ^ "="), String 
+      (fun s -> (strref := (if s == "" then default else s)))
      ] in
   [
 (* Getting help *)
@@ -369,13 +373,15 @@ let cmdline_actions =
   @ f_opt "cse" option_fcse
   @ f_opt "redundancy" option_fredundancy
   @ f_opt "postpass" option_fpostpass
-  @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched
+  @ f_opt_str "postpass" option_fpostpass option_fpostpass_sched "list"
   @ f_opt "inline" option_finline
   @ f_opt "inline-functions-called-once" option_finline_functions_called_once
   @ f_opt "globaladdrtmp" option_fglobaladdrtmp
   @ f_opt "globaladdroffset" option_fglobaladdroffset
   @ f_opt "xsaddr" option_fxsaddr
   @ f_opt "coalesce-mem" option_coalesce_mem
+  @ f_str "div-i32" option_div_i32 "stsud"
+  @ f_str "div-i64" option_div_i64 "stsud"
 (* Code generation options *)
   @ f_opt "fpu" option_ffpu
   @ f_opt "sse" option_ffpu (* backward compatibility *)
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 4dc4b7c2..2bdd0978 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -39,8 +39,14 @@ module Target (*: TARGET*) =
       | Idiv_stsud
       | Idiv_fp;;
 
-    let idiv_function_kind_32bit () = Idiv_fp;;
-    let idiv_function_kind_64bit () = Idiv_stsud;;
+    let idiv_function_kind = function
+        "stsud" -> Idiv_stsud
+      | "system" -> Idiv_system
+      | "fp" -> Idiv_fp
+      | _ -> failwith "unknown integer division kind";;
+    
+    let idiv_function_kind_32bit () = idiv_function_kind !Clflags.option_div_i32;;
+    let idiv_function_kind_64bit () = idiv_function_kind !Clflags.option_div_i64;;
     
     let subst_symbol = function
         "__compcert_i64_udiv" ->
-- 
cgit 


From 6b874a7d5867fc8da503b6658f2fb179c5a12a6b Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 29 May 2019 12:08:24 +0200
Subject: use silent FP

---
 runtime/mppa_k1c/i32_divmod.S | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/runtime/mppa_k1c/i32_divmod.S b/runtime/mppa_k1c/i32_divmod.S
index 8dd9481c..d2b4e8d5 100644
--- a/runtime/mppa_k1c/i32_divmod.S
+++ b/runtime/mppa_k1c/i32_divmod.S
@@ -55,7 +55,7 @@ __compcert_i32_divmod_fp:
 #endif
 	;;
 # a in r1, b in r7
-	floatud.rn $r5 = $r7, 0
+	floatud.rn.s $r5 = $r7, 0
 #ifndef NO_SHORTCUT
 	compd.eq $r8 = $r7, 1
 	cb.wnez $r8? .LESS # shortcut if a < b
@@ -63,27 +63,27 @@ __compcert_i32_divmod_fp:
 	;;
 # b (double) in r5
 	make $r6 = 0x3ff0000000000000 # 1.0
-	fnarrowdw.rn $r11 = $r5
+	fnarrowdw.rn.s $r11 = $r5
 #	cb.wnez $r8, .RET1 # if b=1
 	;;
 # b (single) in r11
-	floatud.rn $r10 = $r1, 0
-	finvw.rn $r11 = $r11
+	floatud.rn.s $r10 = $r1, 0
+	finvw.rn.s $r11 = $r11
 	;;
-	fwidenlwd $r11 = $r11
+	fwidenlwd.s $r11 = $r11
 	;;
 # invb0 in r11
 	copyd $r9 = $r11
-	ffmsd.rn $r6 = $r11, $r5
+	ffmsd.rn.s $r6 = $r11, $r5
 # alpha in r6
 	;;
-	ffmad.rn $r9 = $r11, $r6
+	ffmad.rn.s $r9 = $r11, $r6
 # 1/b in r9
 	;;
-	fmuld.rn $r0 = $r10, $r9
+	fmuld.rn.s $r0 = $r10, $r9
 # a/b in r1
 	;;
-	fixedud.rn $r0 = $r0, 0
+	fixedud.rn.s $r0 = $r0, 0
 	;;
 	msbfd $r1 = $r0, $r7
 	;;
-- 
cgit 


From 633b72565b022f159526338b5bbb9fcac86dfd2b Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Wed, 29 May 2019 21:22:55 +0200
Subject: copyright block

---
 runtime/mppa_k1c/i64_udivmod_stsud.S | 183 +++++++++++++++++++++++++++++++++++
 1 file changed, 183 insertions(+)
 create mode 100644 runtime/mppa_k1c/i64_udivmod_stsud.S

diff --git a/runtime/mppa_k1c/i64_udivmod_stsud.S b/runtime/mppa_k1c/i64_udivmod_stsud.S
new file mode 100644
index 00000000..ac84ca47
--- /dev/null
+++ b/runtime/mppa_k1c/i64_udivmod_stsud.S
@@ -0,0 +1,183 @@
+/*
+Integer division for K1c
+
+David Monniaux, CNRS / Verimag
+	*/
+	
+	.globl dm_udivmoddi4
+dm_udivmoddi4:
+	sxwd $r2 = $r2
+	make $r5 = 0
+	compd.ltu $r3 = $r0, $r1
+	;;
+
+	clzd $r3 = $r1
+	clzd $r4 = $r0
+	cb.dnez $r3? .L74
+	;;
+
+	sbfw $r4 = $r4, $r3
+	;;
+
+	zxwd $r3 = $r4
+	slld $r1 = $r1, $r4
+	;;
+
+	compd.ltu $r6 = $r0, $r1
+	;;
+
+	cb.dnez $r6? .L4C
+	;;
+
+	make $r5 = 1
+	sbfd $r0 = $r1, $r0
+	;;
+
+	slld $r5 = $r5, $r4
+	;;
+
+.L4C:
+	cb.deqz $r3? .L74
+	;;
+
+	srld $r1 = $r1, 1
+	zxwd $r3 = $r4
+	;;
+
+	loopdo $r3, .LOOP
+	;;
+
+	stsud $r0 = $r1, $r0
+	;;
+
+.LOOP:
+	addd $r5 = $r0, $r5
+	srld $r0 = $r0, $r4
+	;;
+
+	slld $r4 = $r0, $r4
+	;;
+
+	sbfd $r5 = $r4, $r5
+	;;
+
+.L74:
+	cmoved.deqz $r2? $r0 = $r5
+	ret
+	;;
+
+/*
+r0 : a
+r1 : b
+r2 : negate result?
+r3 : return mod?
+*/
+
+	.globl __compcert_i32_sdiv_stsud
+__compcert_i32_sdiv_stsud:
+	compw.lt $r2 = $r0, 0
+	compw.lt $r3 = $r1, 0
+	absw $r0 = $r0
+	absw $r1 = $r1
+	;;
+	zxwd $r0 = $r0
+	zxwd $r1 = $r1
+	xord $r2 = $r2, $r3
+	make $r3 = 0
+	goto __compcert_i64_divmod_stsud
+	;;
+	
+	.globl __compcert_i32_smod_stsud
+__compcert_i32_smod_stsud:
+	compw.lt $r2 = $r0, 0
+	absw $r0 = $r0
+	absw $r1 = $r1
+	make $r3 = 1
+	;;
+	zxwd $r0 = $r0
+	zxwd $r1 = $r1
+	goto __compcert_i64_divmod_stsud
+	;;
+	
+	.globl __compcert_i32_umod_stsud
+__compcert_i32_umod_stsud:
+	make $r2 = 0
+	make $r3 = 1
+	zxwd $r0 = $r0
+	zxwd $r1 = $r1
+	goto __compcert_i64_divmod_stsud
+	;;
+
+	.globl __compcert_i32_udiv_stsud
+__compcert_i32_udiv_stsud:
+	make $r2 = 0
+	make $r3 = 0
+	zxwd $r0 = $r0
+	zxwd $r1 = $r1
+	goto __compcert_i64_divmod_stsud
+	;;
+
+	.globl __compcert_i64_divmod_stsud
+ __compcert_i64_divmod_stsud:
+	make $r5 = 0
+	compd.ltu $r7 = $r0, $r1
+	;;
+
+	clzd $r7 = $r1
+	clzd $r4 = $r0
+	cb.dnez $r7? .ZL74
+	;;
+
+	sbfw $r4 = $r4, $r7
+	;;
+
+	zxwd $r7 = $r4
+	slld $r1 = $r1, $r4
+	;;
+
+	compd.ltu $r6 = $r0, $r1
+	;;
+
+	cb.dnez $r6? .ZL4C
+	;;
+
+	make $r5 = 1
+	sbfd $r0 = $r1, $r0
+	;;
+
+	slld $r5 = $r5, $r4
+	;;
+
+.ZL4C:
+	cb.deqz $r7? .ZL74
+	;;
+
+	srld $r1 = $r1, 1
+	zxwd $r7 = $r4
+	;;
+
+	loopdo $r7, .ZLOOP
+	;;
+
+	stsud $r0 = $r1, $r0
+	;;
+
+.ZLOOP:
+	addd $r5 = $r0, $r5
+	srld $r0 = $r0, $r4
+	;;
+
+	slld $r4 = $r0, $r4
+	;;
+
+	sbfd $r5 = $r4, $r5
+	;;
+
+.ZL74:
+	cmoved.weqz $r3? $r0 = $r5
+	;;
+	negd $r5 = $r0
+	;;
+	cmoved.wnez $r2? $r0 = $r5
+	ret
+	;;
-- 
cgit 


From a529539e958f358cad0911cb668723749e565f58 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 20 Apr 2020 14:12:21 +0200
Subject: seems like fixed linking tests?!

---
 runtime/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/runtime/Makefile b/runtime/Makefile
index a689f3ea..5b8f8fdf 100644
--- a/runtime/Makefile
+++ b/runtime/Makefile
@@ -25,8 +25,8 @@ 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 \
      i64_udivmod_stsud.o i32_divmod.o \
+     i64_utod.o i64_utof.o i64_stod.o i64_stof.o \
      vararg.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
-- 
cgit 


From 09184b1ab9be700d0cb5125c113b4fb8d6be06c8 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 20 Apr 2020 15:16:34 +0200
Subject: fix int64

---
 runtime/mppa_k1c/i64_udivmod_stsud.s | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/runtime/mppa_k1c/i64_udivmod_stsud.s b/runtime/mppa_k1c/i64_udivmod_stsud.s
index b1d10326..50d0a767 100644
--- a/runtime/mppa_k1c/i64_udivmod_stsud.s
+++ b/runtime/mppa_k1c/i64_udivmod_stsud.s
@@ -135,6 +135,8 @@ __compcert_i64_udiv_stsud:
 __compcert_i64_sdiv_stsud:
 	compd.lt $r2 = $r0, 0
 	compd.lt $r3 = $r1, 0
+	absd $r0 = $r0
+	absd $r1 = $r1
 	;;
 	xord $r2 = $r2, $r3
 	make $r3 = 0
@@ -144,6 +146,8 @@ __compcert_i64_sdiv_stsud:
 	.globl __compcert_i64_smod_stsud
 __compcert_i64_smod_stsud:
 	compd.lt $r2 = $r0, 0
+	absd $r0 = $r0
+	absd $r1 = $r1
 	make $r3 = 1
 	goto __compcert_i64_divmod_stsud
 	;;
-- 
cgit