diff options
-rw-r--r-- | driver/Clflags.ml | 2 | ||||
-rw-r--r-- | driver/Driver.ml | 6 | ||||
-rw-r--r-- | mppa_k1c/SelectOp.vp | 12 | ||||
-rw-r--r-- | mppa_k1c/SelectOpproof.v | 18 | ||||
-rw-r--r-- | mppa_k1c/TargetPrinter.ml | 54 | ||||
-rw-r--r-- | runtime/Makefile | 6 | ||||
-rw-r--r-- | runtime/mppa_k1c/i32_divmod.s | 120 | ||||
-rw-r--r-- | runtime/mppa_k1c/i64_sdiv.c | 5 | ||||
-rw-r--r-- | runtime/mppa_k1c/i64_smod.c | 35 | ||||
-rw-r--r-- | runtime/mppa_k1c/i64_udiv.c | 6 | ||||
-rw-r--r-- | runtime/mppa_k1c/i64_udivmod.c | 2 | ||||
-rw-r--r-- | runtime/mppa_k1c/i64_udivmod_stsud.s | 214 | ||||
-rw-r--r-- | runtime/mppa_k1c/i64_umod.c | 6 | ||||
-rw-r--r-- | test/monniaux/division/sum_div.c | 18 |
14 files changed, 427 insertions, 77 deletions
diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 6986fb96..c20758b3 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -77,6 +77,8 @@ let use_standard_headers = ref Configuration.has_standard_headers let option_fglobaladdrtmp = ref false let option_fglobaladdroffset = ref false let option_fxsaddr = ref true +let option_div_i32 = ref "stsud" +let option_div_i64 = ref "stsud" let option_faddx = ref false let option_fcoalesce_mem = ref true let option_fforward_moves = ref true diff --git a/driver/Driver.ml b/driver/Driver.ml index 388482a0..ba48f29a 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -289,6 +289,10 @@ let cmdline_actions = [Exact("-f" ^ name ^ "="), String (fun s -> (strref := (if s == "" then "list" 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 let check_align n = if n <= 0 || ((n land (n - 1)) <> 0) then error no_loc "requested alignment %d is not a power of 2" n @@ -408,6 +412,8 @@ let cmdline_actions = @ f_opt "globaladdrtmp" option_fglobaladdrtmp @ f_opt "globaladdroffset" option_fglobaladdroffset @ f_opt "xsaddr" option_fxsaddr + @ f_str "div-i32" option_div_i32 "stsud" + @ f_str "div-i64" option_div_i64 "stsud" @ f_opt "addx" option_faddx @ f_opt "coalesce-mem" option_fcoalesce_mem @ f_opt "all-loads-nontrap" option_all_loads_nontrap diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index ec3985c5..1cac2257 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -452,18 +452,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 d3eb1dde..6dd00ad5 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -929,6 +929,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. @@ -948,7 +954,8 @@ Proof. } congruence. Qed. - + *) + Theorem eval_modu_base: forall le a b x y z, eval_expr ge sp e m le a x -> @@ -956,6 +963,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. @@ -975,7 +988,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/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 930b1c51..63a0bd24 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -34,11 +34,57 @@ module Target (*: TARGET*) = let comment = "#" + type idiv_function_kind = + | Idiv_system + | Idiv_stsud + | Idiv_fp;; + + 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" -> "__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_smod_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 3b1cabc4..a689f3ea 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -23,9 +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 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 \ + 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 ifeq ($(ARCH),aarch64) diff --git a/runtime/mppa_k1c/i32_divmod.s b/runtime/mppa_k1c/i32_divmod.s new file mode 100644 index 00000000..d2b4e8d5 --- /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_fp +__compcert_i32_sdiv_fp: + 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_fp + ;; + + .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_fp + ;; + + .globl __compcert_i32_umod_fp +__compcert_i32_umod_fp: + make $r2 = 0 + make $r3 = 1 + goto __compcert_i32_divmod_fp + ;; + + .globl __compcert_i32_udiv_fp +__compcert_i32_udiv_fp: + make $r2 = 0 + make $r3 = 0 + ;; + +/* +r0 : a +r1 : b +r2 : negate result? +r3 : return mod? +*/ + + .globl __compcert_i32_divmod_fp +__compcert_i32_divmod_fp: + 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.s $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.s $r11 = $r5 +# cb.wnez $r8, .RET1 # if b=1 + ;; +# b (single) in r11 + floatud.rn.s $r10 = $r1, 0 + finvw.rn.s $r11 = $r11 + ;; + fwidenlwd.s $r11 = $r11 + ;; +# invb0 in r11 + copyd $r9 = $r11 + ffmsd.rn.s $r6 = $r11, $r5 +# alpha in r6 + ;; + ffmad.rn.s $r9 = $r11, $r6 +# 1/b in r9 + ;; + fmuld.rn.s $r0 = $r10, $r9 +# a/b in r1 + ;; + fixedud.rn.s $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 60269cae..b98d9316 100644 --- a/runtime/mppa_k1c/i64_sdiv.c +++ b/runtime/mppa_k1c/i64_sdiv.c @@ -1,10 +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); diff --git a/runtime/mppa_k1c/i64_smod.c b/runtime/mppa_k1c/i64_smod.c index 26ffb39b..3371eecf 100644 --- a/runtime/mppa_k1c/i64_smod.c +++ b/runtime/mppa_k1c/i64_smod.c @@ -1,40 +1,5 @@ -#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 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_udivmod_stsud.s b/runtime/mppa_k1c/i64_udivmod_stsud.s new file mode 100644 index 00000000..b1d10326 --- /dev/null +++ b/runtime/mppa_k1c/i64_udivmod_stsud.s @@ -0,0 +1,214 @@ +/* +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_umod_stsud +__compcert_i64_umod_stsud: + make $r2 = 0 + make $r3 = 1 + goto __compcert_i64_divmod_stsud + ;; + + .globl __compcert_i64_udiv_stsud +__compcert_i64_udiv_stsud: + make $r2 = 0 + make $r3 = 0 + goto __compcert_i64_divmod_stsud + ;; + + .globl __compcert_i64_sdiv_stsud +__compcert_i64_sdiv_stsud: + compd.lt $r2 = $r0, 0 + compd.lt $r3 = $r1, 0 + ;; + xord $r2 = $r2, $r3 + make $r3 = 0 + goto __compcert_i64_divmod_stsud + ;; + + .globl __compcert_i64_smod_stsud +__compcert_i64_smod_stsud: + compd.lt $r2 = $r0, 0 + make $r3 = 1 + 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 + ;; 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/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; -} |