From 41b7ecb127b93b1aecc29a298ec21dc94603e6fa Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 29 Jul 2013 12:10:11 +0000
Subject: Optimize integer divisions by positive constants, turning them into
 multiply-high and shifts.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2300 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 powerpc/Asm.v           |  6 ++++
 powerpc/Asmgen.v        |  6 ++++
 powerpc/ConstpropOp.vp  |  2 ++
 powerpc/Op.v            | 10 +++++++
 powerpc/PrintAsm.ml     |  4 +++
 powerpc/SelectOp.vp     | 32 ++++-----------------
 powerpc/SelectOpproof.v | 74 +++++++++++++++++++------------------------------
 7 files changed, 63 insertions(+), 71 deletions(-)

(limited to 'powerpc')

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index bbe2d3e..e6e9d76 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -193,6 +193,8 @@ Inductive instruction : Type :=
   | Pmtlr: ireg -> instruction                                (**r move ireg to LR *)
   | Pmulli: ireg -> ireg -> constant -> instruction           (**r integer multiply immediate *)
   | Pmullw: ireg -> ireg -> ireg -> instruction               (**r integer multiply *)
+  | Pmulhw: ireg -> ireg -> ireg -> instruction               (**r multiply high signed *)
+  | Pmulhwu: ireg -> ireg -> ireg -> instruction               (**r multiply high signed *)
   | Pnand: ireg -> ireg -> ireg -> instruction                (**r bitwise not-and *)
   | Pnor: ireg -> ireg -> ireg -> instruction                 (**r bitwise not-or *)
   | Por: ireg -> ireg -> ireg -> instruction                  (**r bitwise or *)
@@ -702,6 +704,10 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       Next (nextinstr (rs#rd <- (Val.mul rs#r1 (const_low cst)))) m
   | Pmullw rd r1 r2 =>
       Next (nextinstr (rs#rd <- (Val.mul rs#r1 rs#r2))) m
+  | Pmulhw rd r1 r2 =>
+      Next (nextinstr (rs#rd <- (Val.mulhs rs#r1 rs#r2))) m
+  | Pmulhwu rd r1 r2 =>
+      Next (nextinstr (rs#rd <- (Val.mulhu rs#r1 rs#r2))) m
   | Pnand rd r1 r2 =>
       Next (nextinstr (rs#rd <- (Val.notint (Val.and rs#r1 rs#r2)))) m
   | Pnor rd r1 r2 =>
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 2b6d80d..cc9a51c 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -371,6 +371,12 @@ Definition transl_op
            Pmulli r r1 (Cint n) :: k
          else
            loadimm GPR0 n (Pmullw r r1 GPR0 :: k))
+  | Omulhs, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Pmulhw r r1 r2 :: k)
+  | Omulhu, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
+      OK (Pmulhwu r r1 r2 :: k)
   | Odiv, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res;
       OK (Pdivw r r1 r2 :: k)
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index e7e4095..d0322c1 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -95,6 +95,8 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | Osubimm n, I n1 :: nil => I (Int.sub n n1)
   | Omul, I n1 :: I n2 :: nil => I(Int.mul n1 n2)
   | Omulimm n, I n1 :: nil => I(Int.mul n1 n)
+  | Omulhs, I n1 :: I n2 :: nil => I(Int.mulhs n1 n2)
+  | Omulhu, I n1 :: I n2 :: nil => I(Int.mulhu n1 n2)
   | Odiv, I n1 :: I n2 :: nil =>
       if Int.eq n2 Int.zero then Unknown else
       if Int.eq n1 (Int.repr Int.min_signed) && Int.eq n2 Int.mone then Unknown
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 1952304..085a098 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -65,6 +65,8 @@ Inductive operation : Type :=
   | Osubimm: int -> operation           (**r [rd = n - r1] *)
   | Omul: operation                     (**r [rd = r1 * r2] *)
   | Omulimm: int -> operation           (**r [rd = r1 * n] *)
+  | Omulhs: operation                   (**r [rd = high part of r1 * r2, signed] *)
+  | Omulhu: operation                   (**r [rd = high part of r1 * r2, unsigned] *)
   | Odiv: operation                     (**r [rd = r1 / r2] (signed) *)
   | Odivu: operation                    (**r [rd = r1 / r2] (unsigned) *)
   | Oand: operation                     (**r [rd = r1 & r2] *)
@@ -185,6 +187,8 @@ Definition eval_operation
   | Osubimm n, v1::nil => Some (Val.sub (Vint n) v1)
   | Omul, v1::v2::nil => Some (Val.mul v1 v2)
   | Omulimm n, v1::nil => Some (Val.mul v1 (Vint n))
+  | Omulhs, v1::v2::nil => Some (Val.mulhs v1 v2)
+  | Omulhu, v1::v2::nil => Some (Val.mulhu v1 v2)
   | Odiv, v1::v2::nil => Val.divs v1 v2
   | Odivu, v1::v2::nil => Val.divu v1 v2
   | Oand, v1::v2::nil => Some(Val.and v1 v2)
@@ -276,6 +280,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osubimm _ => (Tint :: nil, Tint)
   | Omul => (Tint :: Tint :: nil, Tint)
   | Omulimm _ => (Tint :: nil, Tint)
+  | Omulhs => (Tint :: Tint :: nil, Tint)
+  | Omulhu => (Tint :: Tint :: nil, Tint)
   | Odiv => (Tint :: Tint :: nil, Tint)
   | Odivu => (Tint :: Tint :: nil, Tint)
   | Oand => (Tint :: Tint :: nil, Tint)
@@ -351,6 +357,8 @@ Proof with (try exact I).
   destruct v0...
   destruct v0; destruct v1...
   destruct v0...
+  destruct v0; destruct v1...
+  destruct v0; destruct v1...
   destruct v0; destruct v1; simpl in *; inv H0.
     destruct (Int.eq i0 Int.zero
          || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2...
@@ -759,6 +767,8 @@ Proof.
   inv H4; auto. 
   inv H4; inv H2; simpl; auto.
   inv H4; simpl; auto.
+  inv H4; inv H2; simpl; auto.
+  inv H4; inv H2; simpl; auto.
   inv H4; inv H3; simpl in H1; inv H1. simpl. 
     destruct (Int.eq i0 Int.zero
          || Int.eq i (Int.repr Int.min_signed) && Int.eq i0 Int.mone); inv H2. TrivialExists.
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 879d755..08438df 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -818,6 +818,10 @@ let print_instruction oc tbl pc fallthrough = function
       fprintf oc "	mulli	%a, %a, %a\n" ireg r1 ireg r2 constant c
   | Pmullw(r1, r2, r3) ->
       fprintf oc "	mullw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pmulhw(r1, r2, r3) ->
+      fprintf oc "	mulhw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+  | Pmulhwu(r1, r2, r3) ->
+      fprintf oc "	mulhwu	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pnand(r1, r2, r3) ->
       fprintf oc "	nand	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
   | Pnor(r1, r2, r3) ->
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 7b15ccc..bc9b677 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -290,8 +290,6 @@ Nondetfunction xor (e1: expr) (e2: expr) :=
 
 (** ** Integer division and modulus *)
 
-Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
-
 Definition mod_aux (divop: operation) (e1 e2: expr) :=
   Elet e1
     (Elet (lift e2)
@@ -301,31 +299,13 @@ Definition mod_aux (divop: operation) (e1 e2: expr) :=
                            Enil) :::
                  Enil))).
 
-Definition mods := mod_aux Odiv.
-
-Definition divuimm (e: expr) (n: int) :=
-  match Int.is_power2 n with
-  | Some l => shruimm e l
-  | None   => Eop Odivu (e ::: Eop (Ointconst n) Enil ::: Enil)
-  end.
-
-Nondetfunction divu (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ointconst n2) Enil => divuimm e1 n2
-  | _ => Eop Odivu (e1:::e2:::Enil)
-  end.
-
-Definition moduimm (e: expr) (n: int) :=
-  match Int.is_power2 n with
-  | Some l => andimm (Int.sub n Int.one) e
-  | None   => mod_aux Odivu e (Eop (Ointconst n) Enil)
-  end.
+Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
+Definition mods_base := mod_aux Odiv.
+Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
+Definition modu_base := mod_aux Odivu.
 
-Nondetfunction modu (e1: expr) (e2: expr) :=
-  match e2 with
-  | Eop (Ointconst n2) Enil => moduimm e1 n2
-  | _ => mod_aux Odivu e1 e2
-  end.
+Definition shrximm (e1: expr) (n2: int) :=
+  if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil).
 
 (** ** General shifts *)
 
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 5a0a903..177d64a 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -465,14 +465,14 @@ Proof.
   TrivialExists.
 Qed.
 
-Theorem eval_divs:
+Theorem eval_divs_base:
   forall le a b x y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.divs x y = Some z ->
-  exists v, eval_expr ge sp e m le (divs a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (divs_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold divs. exists z; split. EvalOp. auto.
+  intros. unfold divs_base. exists z; split. EvalOp. auto.
 Qed.
 
 Lemma eval_mod_aux:
@@ -501,73 +501,57 @@ Proof.
   reflexivity.
 Qed.
 
-Theorem eval_mods:
+Theorem eval_mods_base:
   forall le a b x y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.mods x y = Some z ->
-  exists v, eval_expr ge sp e m le (mods a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (mods_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros; unfold mods. 
+  intros; unfold mods_base. 
   exploit Val.mods_divs; eauto. intros [v [A B]].
   subst. econstructor; split; eauto.
   apply eval_mod_aux with (semdivop := Val.divs); auto.
 Qed.
 
-Theorem eval_divuimm:
-  forall le n a x z,
-  eval_expr ge sp e m le a x ->
-  Val.divu x (Vint n) = Some z ->
-  exists v, eval_expr ge sp e m le (divuimm a n) v /\ Val.lessdef z v.
-Proof.
-  intros; unfold divuimm. 
-  destruct (Int.is_power2 n) eqn:?. 
-  replace z with (Val.shru x (Vint i)). apply eval_shruimm; auto.
-  eapply Val.divu_pow2; eauto.
-  TrivialExists. 
-  econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto.
-Qed.
-
-Theorem eval_divu:
-  forall le a x b y z,
+Theorem eval_divu_base:
+  forall le a b x y z,
   eval_expr ge sp e m le a x ->
   eval_expr ge sp e m le b y ->
   Val.divu x y = Some z ->
-  exists v, eval_expr ge sp e m le (divu a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (divu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros until z. unfold divu; destruct (divu_match b); intros; InvEval.
-  eapply eval_divuimm; eauto.
-  TrivialExists. 
+  intros. unfold divu_base. exists z; split. EvalOp. auto.
 Qed.
 
-Theorem eval_moduimm:
-  forall le n a x z,
+Theorem eval_modu_base:
+  forall le a b x y z,
   eval_expr ge sp e m le a x ->
-  Val.modu x (Vint n) = Some z ->
-  exists v, eval_expr ge sp e m le (moduimm a n) v /\ Val.lessdef z v.
+  eval_expr ge sp e m le b y ->
+  Val.modu x y = Some z ->
+  exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros; unfold moduimm. 
-  destruct (Int.is_power2 n) eqn:?. 
-  replace z with (Val.and x (Vint (Int.sub n Int.one))). apply eval_andimm; auto.
-  eapply Val.modu_pow2; eauto.
+  intros; unfold modu_base. 
   exploit Val.modu_divu; eauto. intros [v [A B]].
   subst. econstructor; split; eauto.
   apply eval_mod_aux with (semdivop := Val.divu); auto.
-  EvalOp.
 Qed.
 
-Theorem eval_modu:
-  forall le a x b y z,
+Theorem eval_shrximm:
+  forall le a n x z,
   eval_expr ge sp e m le a x ->
-  eval_expr ge sp e m le b y ->
-  Val.modu x y = Some z ->
-  exists v, eval_expr ge sp e m le (modu a b) v /\ Val.lessdef z v.
+  Val.shrx x (Vint n) = Some z ->
+  exists v, eval_expr ge sp e m le (shrximm a n) v /\ Val.lessdef z v.
 Proof.
-  intros until y; unfold modu; case (modu_match b); intros; InvEval.
-  eapply eval_moduimm; eauto.
-  exploit Val.modu_divu; eauto. intros [v [A B]].
-  subst. econstructor; split; eauto.
-  apply eval_mod_aux with (semdivop := Val.divu); auto.
+  intros. unfold shrximm. 
+  predSpec Int.eq Int.eq_spec n Int.zero.
+  subst n. exists x; split; auto. 
+  destruct x; simpl in H0; try discriminate.
+  destruct (Int.ltu Int.zero (Int.repr 31)); inv H0.
+  replace (Int.shrx i Int.zero) with i. auto. 
+  unfold Int.shrx, Int.divs. rewrite Int.shl_zero. 
+  change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto.
+  econstructor; split. EvalOp. auto.
 Qed.
 
 Theorem eval_shl: binary_constructor_sound shl Val.shl.
-- 
cgit v1.2.3