sdiv seems to work, udiv/umod/smod BOGUS

6 files changed, 69 insertions, 80 deletions

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;
-}