From e637d041c5c2ee3a3ed395a7dab6c9101e8eb16c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 1 Oct 2016 17:25:18 +0200 Subject: Support for 64-bit architectures: generic support - Introduce Archi.ptr64 parameter. - Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise). - Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated. - Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers. - Update the memory model accordingly. - Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly. - Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers. - Update the compiler front-end and back-end accordingly. --- backend/SelectDiv.vp | 36 +++++++++++++++++++++++++++++++++++- 1 file changed, 35 insertions(+), 1 deletion(-) (limited to 'backend/SelectDiv.vp') diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index a275a850..d708afb7 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -36,7 +36,7 @@ Fixpoint find_div_mul_params (fuel: nat) (nc: Z) (d: Z) (p: Z) : option (Z * Z) | S fuel' => let twp := two_p p in if zlt (nc * (d - twp mod d)) twp - then Some(p - 32, (twp + d - twp mod d) / d) + then Some(p, (twp + d - twp mod d) / d) else find_div_mul_params fuel' nc d (p + 1) end. @@ -47,6 +47,7 @@ Definition divs_mul_params (d: Z) : option (Z * Z) := d 32 with | None => None | Some(p, m) => + let p := p - 32 in if zlt 0 d && zlt (two_p (32 + p)) (m * d) && zle (m * d) (two_p (32 + p) + two_p (p + 1)) @@ -62,6 +63,7 @@ Definition divu_mul_params (d: Z) : option (Z * Z) := d 32 with | None => None | Some(p, m) => + let p := p - 32 in if zlt 0 d && zle (two_p (32 + p)) (m * d) && zle (m * d) (two_p (32 + p) + two_p p) @@ -70,6 +72,38 @@ Definition divu_mul_params (d: Z) : option (Z * Z) := then Some(p, m) else None end. +Definition divls_mul_params (d: Z) : option (Z * Z) := + match find_div_mul_params + Int64.wordsize + (Int64.half_modulus - Int64.half_modulus mod d - 1) + d 64 with + | None => None + | Some(p, m) => + let p := p - 64 in + if zlt 0 d + && zlt (two_p (64 + p)) (m * d) + && zle (m * d) (two_p (64 + p) + two_p (p + 1)) + && zle 0 m && zlt m Int64.modulus + && zle 0 p && zlt p 64 + then Some(p, m) else None + end. + +Definition divlu_mul_params (d: Z) : option (Z * Z) := + match find_div_mul_params + Int64.wordsize + (Int64.modulus - Int64.modulus mod d - 1) + d 64 with + | None => None + | Some(p, m) => + let p := p - 64 in + if zlt 0 d + && zle (two_p (64 + p)) (m * d) + && zle (m * d) (two_p (64 + p) + two_p p) + && zle 0 m && zlt m Int64.modulus + && zle 0 p && zlt p 64 + then Some(p, m) else None + end. + Definition divu_mul (p: Z) (m: Z) := shruimm (Eop Omulhu (Eletvar O ::: Eop (Ointconst (Int.repr m)) Enil ::: Enil)) (Int.repr p). -- cgit From f21a6b181dded86ef0e5c7ab94f74e5b960fd510 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 2 Oct 2016 16:17:51 +0200 Subject: Improve code generation for 64-bit signed integer division Implement the 'shift right extended' trick, both in the generic implementation (backend/SplitLong) and in the IA32 port. Note that now SelectDiv depends on SelectLong, and that some work was moved from SelectLong to SelectDiv. --- backend/SelectDiv.vp | 65 +++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 59 insertions(+), 6 deletions(-) (limited to 'backend/SelectDiv.vp') diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index d708afb7..1fc0b689 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -14,12 +14,8 @@ Require Import Coqlib. Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Import CminorSel. -Require Import SelectOp. +Require Import AST Integers Floats. +Require Import Op CminorSel SelectOp SplitLong SelectLong. Open Local Scope cminorsel_scope. @@ -201,6 +197,63 @@ Nondetfunction mods (e1: expr) (e2: expr) := | _ => mods_base e1 e2 end. +(** 64-bit integer divisions *) + +Section SELECT. + +Context {hf: helper_functions}. + +Definition modl_from_divl (equo: expr) (n: int64) := + subl (Eletvar O) (mullimm n equo). + +Definition divlu (e1 e2: expr) := + match is_longconst e2, is_longconst e1 with + | Some n2, Some n1 => longconst (Int64.divu n1 n2) + | Some n2, _ => + match Int64.is_power2' n2 with + | Some l => shrluimm e1 l + | None => divlu_base e1 e2 + end (* TODO: multiply-high *) + | _, _ => divlu_base e1 e2 + end. + +Definition modlu (e1 e2: expr) := + match is_longconst e2, is_longconst e1 with + | Some n2, Some n1 => longconst (Int64.modu n1 n2) + | Some n2, _ => + match Int64.is_power2 n2 with + | Some l => andl e1 (longconst (Int64.sub n2 Int64.one)) + | None => modlu_base e1 e2 + end + | _, _ => modlu_base e1 e2 + end. + +Definition divls (e1 e2: expr) := + match is_longconst e2, is_longconst e1 with + | Some n2, Some n1 => longconst (Int64.divs n1 n2) + | Some n2, _ => + match Int64.is_power2' n2 with + | Some l => if Int.ltu l (Int.repr 63) then shrxlimm e1 l else divls_base e1 e2 + | None => divls_base e1 e2 + end (* TODO: multiply-high *) + | _, _ => divls_base e1 e2 + end. + +Definition modls (e1 e2: expr) := + match is_longconst e2, is_longconst e1 with + | Some n2, Some n1 => longconst (Int64.mods n1 n2) + | Some n2, _ => + match Int64.is_power2' n2 with + | Some l => if Int.ltu l (Int.repr 63) + then Elet e1 (modl_from_divl (shrxlimm (Eletvar O) l) n2) + else modls_base e1 e2 + | None => modls_base e1 e2 + end + | _, _ => modls_base e1 e2 + end. + +End SELECT. + (** Floating-point division by a constant can also be turned into a FP multiplication by the inverse constant, but only for powers of 2. *) -- cgit 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/SelectDiv.vp | 51 ++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 44 insertions(+), 7 deletions(-) (limited to 'backend/SelectDiv.vp') diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index 1fc0b689..5cc66322 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -206,14 +206,23 @@ Context {hf: helper_functions}. Definition modl_from_divl (equo: expr) (n: int64) := subl (Eletvar O) (mullimm n equo). +Definition divlu_mull (p: Z) (m: Z) := + shrluimm (mullhu (Eletvar O) (Int64.repr m)) (Int.repr p). + Definition divlu (e1 e2: expr) := match is_longconst e2, is_longconst e1 with | Some n2, Some n1 => longconst (Int64.divu n1 n2) | Some n2, _ => match Int64.is_power2' n2 with | Some l => shrluimm e1 l - | None => divlu_base e1 e2 - end (* TODO: multiply-high *) + | None => if optim_for_size tt then + divlu_base e1 e2 + else + match divlu_mul_params (Int64.unsigned n2) with + | None => divlu_base e1 e2 + | Some(p, m) => Elet e1 (divlu_mull p m) + end + end | _, _ => divlu_base e1 e2 end. @@ -223,19 +232,41 @@ Definition modlu (e1 e2: expr) := | Some n2, _ => match Int64.is_power2 n2 with | Some l => andl e1 (longconst (Int64.sub n2 Int64.one)) - | None => modlu_base e1 e2 + | None => if optim_for_size tt then + modlu_base e1 e2 + else + match divlu_mul_params (Int64.unsigned n2) with + | None => modlu_base e1 e2 + | Some(p, m) => Elet e1 (modl_from_divl (divlu_mull p m) n2) + end end | _, _ => modlu_base e1 e2 end. +Definition divls_mull (p: Z) (m: Z) := + let e2 := + mullhs (Eletvar O) (Int64.repr m) in + let e3 := + if zlt m Int64.half_modulus then e2 else addl e2 (Eletvar O) in + addl (shrlimm e3 (Int.repr p)) + (shrluimm (Eletvar O) (Int.repr (Int64.zwordsize - 1))). + Definition divls (e1 e2: expr) := match is_longconst e2, is_longconst e1 with | Some n2, Some n1 => longconst (Int64.divs n1 n2) | Some n2, _ => match Int64.is_power2' n2 with - | Some l => if Int.ltu l (Int.repr 63) then shrxlimm e1 l else divls_base e1 e2 - | None => divls_base e1 e2 - end (* TODO: multiply-high *) + | Some l => if Int.ltu l (Int.repr 63) + then shrxlimm e1 l + else divls_base e1 e2 + | None => if optim_for_size tt then + divls_base e1 e2 + else + match divls_mul_params (Int64.signed n2) with + | None => divls_base e1 e2 + | Some(p, m) => Elet e1 (divls_mull p m) + end + end | _, _ => divls_base e1 e2 end. @@ -247,7 +278,13 @@ Definition modls (e1 e2: expr) := | Some l => if Int.ltu l (Int.repr 63) then Elet e1 (modl_from_divl (shrxlimm (Eletvar O) l) n2) else modls_base e1 e2 - | None => modls_base e1 e2 + | None => if optim_for_size tt then + modls_base e1 e2 + else + match divls_mul_params (Int64.signed n2) with + | None => modls_base e1 e2 + | Some(p, m) => Elet e1 (modl_from_divl (divls_mull p m) n2) + end end | _, _ => modls_base e1 e2 end. -- cgit