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.

1 files changed, 59 insertions, 6 deletions

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. *)