1 files changed, 131 insertions, 7 deletions
diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp
index a275a850..5cc66322 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.
 
@@ -36,7 +32,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 +43,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 +59,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 +68,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).
@@ -167,6 +197,100 @@ 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_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   => 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.
+
+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   => 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   => 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.
+
+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   => 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.
+
+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. *)