diff options
-rw-r--r-- | mppa_k1c/SelectOp.vp | 12 | ||||
-rw-r--r-- | mppa_k1c/SelectOpproof.v | 18 | ||||
-rw-r--r-- | runtime/mppa_k1c/i64_sdiv.c | 10 | ||||
-rw-r--r-- | runtime/mppa_k1c/i64_smod.c | 40 | ||||
-rw-r--r-- | runtime/mppa_k1c/vararg.S | 51 | ||||
-rw-r--r-- | test/monniaux/division/sum_div.c | 18 |
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; -} |