From d2af79a77ed2936ff0ed90cadf8e48637d774d4c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 4 Oct 2016 15:52:16 +0200 Subject: Turn 64-bit integer division and modulus by constants into multiply-high This trick was already implemented for 32-bit integer division and modulus. Here we extend it to the 64-bit case. For 32-bit target processors, the runtime library must implement 64-bit multiply-high (signed and unsigned). Tentative implementations are provided for IA32 and PowerPC, but need testing. --- backend/SplitLong.vp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'backend/SplitLong.vp') diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp index 5891adef..f7eeebd0 100644 --- a/backend/SplitLong.vp +++ b/backend/SplitLong.vp @@ -38,7 +38,9 @@ Class helper_functions := mk_helper_functions { i64_umod: ident; (**r unsigned remainder *) i64_shl: ident; (**r shift left *) i64_shr: ident; (**r shift right unsigned *) - i64_sar: ident (**r shift right signed *) + i64_sar: ident; (**r shift right signed *) + i64_umulh: ident; (**r unsigned multiply high *) + i64_smulh: ident; (**r signed multiply high *) }. Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default. @@ -255,6 +257,11 @@ Definition mull (e1 e2: expr) := | _, _ => mull_base e1 e2 end. +Definition mullhu (e1: expr) (n2: int64) := + Eexternal i64_umulh sig_ll_l (e1 ::: longconst n2 ::: Enil). +Definition mullhs (e1: expr) (n2: int64) := + Eexternal i64_smulh sig_ll_l (e1 ::: longconst n2 ::: Enil). + Definition shrxlimm (e: expr) (n: int) := if Int.eq n Int.zero then e else Elet e (shrlimm (addl (Eletvar O) -- cgit