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