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

9 files changed, 78 insertions, 16 deletions

diff --git a/ia32/Asm.v b/ia32/Asm.v
index d86ff19..78c4c3b 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -145,6 +145,8 @@ Inductive instruction: Type :=
   | Psub_rr (rd: ireg) (r1: ireg)
   | Pimul_rr (rd: ireg) (r1: ireg)
   | Pimul_ri (rd: ireg) (n: int)
+  | Pimul_r (r1: ireg)
+  | Pmul_r (r1: ireg)
   | Pdiv (r1: ireg)
   | Pidiv (r1: ireg)
   | Pand_rr (rd: ireg) (r1: ireg)
@@ -540,6 +542,12 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       Next (nextinstr_nf (rs#rd <- (Val.mul rs#rd rs#r1))) m
   | Pimul_ri rd n =>
       Next (nextinstr_nf (rs#rd <- (Val.mul rs#rd (Vint n)))) m
+  | Pimul_r r1 =>
+      Next (nextinstr_nf (rs#EAX <- (Val.mul rs#EAX rs#r1)
+                            #EDX <- (Val.mulhs rs#EAX rs#r1))) m
+  | Pmul_r r1 =>
+      Next (nextinstr_nf (rs#EAX <- (Val.mul rs#EAX rs#r1)
+                            #EDX <- (Val.mulhu rs#EAX rs#r1))) m
   | Pdiv r1 =>
       let vn := rs#EAX in let vd := (rs#EDX <- Vundef)#r1 in
       match Val.divu vn vd, Val.modu vn vd with
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index 4543ac9..0410057 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -311,6 +311,14 @@ Definition transl_op
   | Omulimm n, a1 :: nil =>
       assertion (mreg_eq a1 res);
       do r <- ireg_of res; OK (Pimul_ri r n :: k)
+  | Omulhs, a1 :: a2 :: nil =>
+      assertion (mreg_eq a1 AX);
+      assertion (mreg_eq res DX);
+      do r2 <- ireg_of a2; OK (Pimul_r r2 :: k)
+  | Omulhu, a1 :: a2 :: nil =>
+      assertion (mreg_eq a1 AX);
+      assertion (mreg_eq res DX);
+      do r2 <- ireg_of a2; OK (Pmul_r r2 :: k)
   | Odiv, a1 :: a2 :: nil =>
       assertion (mreg_eq a1 AX);
       assertion (mreg_eq a2 CX);
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 728617e..9ddc463 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -922,6 +922,10 @@ Transparent destroyed_by_op.
   apply SAME. eapply mk_intconv_correct; eauto.
 (* cast16unsigned *)
   apply SAME. eapply mk_intconv_correct; eauto.
+(* mulhs *)
+  apply SAME. TranslOp. destruct H1. Simplifs. 
+(* mulhu *)
+  apply SAME. TranslOp. destruct H1. Simplifs. 
 (* div *)
   apply SAME.
   specialize (divs_mods_exist (rs EAX) (rs ECX)). rewrite H0. 
diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index fea0afd..a29b450 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/ConstpropOp.vp
@@ -107,6 +107,8 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | Osub, G s1 n1 :: I n2 :: nil => G s1 (Int.sub n1 n2)
   | 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/ia32/Machregs.v b/ia32/Machregs.v
index 528e9ed..826dadf 100644
--- a/ia32/Machregs.v
+++ b/ia32/Machregs.v
@@ -75,6 +75,8 @@ Definition destroyed_by_op (op: operation): list mreg :=
   match op with
   | Omove => FP0 :: nil
   | Ocast8signed | Ocast8unsigned | Ocast16signed | Ocast16unsigned => AX :: nil
+  | Omulhs => AX :: DX :: nil
+  | Omulhu => AX :: DX :: nil
   | Odiv => AX :: DX :: nil
   | Odivu => AX :: DX :: nil
   | Omod => AX :: DX :: nil
@@ -136,6 +138,8 @@ Definition temp_for_parent_frame: mreg :=
 
 Definition mregs_for_operation (op: operation): list (option mreg) * option mreg :=
   match op with
+  | Omulhs => (Some AX :: None :: nil, Some DX)
+  | Omulhu => (Some AX :: None :: nil, Some DX)
   | Odiv => (Some AX :: Some CX :: nil, Some AX)
   | Odivu => (Some AX :: Some CX :: nil, Some AX)
   | Omod => (Some AX :: Some CX :: nil, Some DX)
@@ -192,6 +196,8 @@ Definition two_address_op (op: operation) : bool :=
   | Osub => true
   | Omul => true
   | Omulimm _ => true
+  | Omulhs => false
+  | Omulhu => false
   | Odiv => false
   | Odivu => false
   | Omod => false
diff --git a/ia32/Op.v b/ia32/Op.v
index 509938e..f2e6b13 100644
--- a/ia32/Op.v
+++ b/ia32/Op.v
@@ -78,6 +78,8 @@ Inductive operation : Type :=
   | Osub: operation                     (**r [rd = r1 - r2] *)
   | 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) *)
   | Omod: operation                     (**r [rd = r1 % r2] (signed) *)
@@ -216,6 +218,8 @@ Definition eval_operation
   | Osub, v1::v2::nil => Some (Val.sub v1 v2)
   | 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
   | Omod, v1::v2::nil => Val.mods v1 v2
@@ -305,6 +309,8 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osub => (Tint :: 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)
   | Omod => (Tint :: Tint :: nil, Tint)
@@ -387,6 +393,8 @@ Proof with (try exact I).
   destruct v0; destruct v1... simpl. destruct (eq_block b b0)...
   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...
   destruct v0; destruct v1; simpl in *; inv H0. destruct (Int.eq i0 Int.zero); inv H2...
@@ -796,6 +804,8 @@ Proof.
     rewrite Int.sub_shifted. 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.
   inv H4; inv H3; simpl in H1; inv H1. simpl. 
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 9c8f963..5fb2568 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -606,6 +606,10 @@ let print_instruction oc = function
       fprintf oc "	imull	%a, %a\n" ireg r1 ireg rd
   | Pimul_ri(rd, n) ->
       fprintf oc "	imull	$%a, %a\n" coqint n ireg rd
+  | Pimul_r(r1) ->
+      fprintf oc "	imull	%a\n" ireg r1
+  | Pmul_r(r1) ->
+      fprintf oc "	mull	%a\n" ireg r1
   | Pdiv(r1) ->
       fprintf oc "	xorl	%%edx, %%edx\n";
       fprintf oc "	divl	%a\n" ireg r1
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index 2d1ab48..209147e 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -299,10 +299,13 @@ Nondetfunction xor (e1: expr) (e2: expr) :=
 
 (** ** Integer division and modulus *)
 
-Definition divu (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
-Definition modu (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil).
-Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
-Definition mods (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil).
+Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil).
+Definition modu_base (e1: expr) (e2: expr) := Eop Omodu (e1:::e2:::Enil).
+Definition divs_base (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
+Definition mods_base (e1: expr) (e2: expr) := Eop Omod (e1:::e2:::Enil).
+
+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/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 8c9c7e6..85802b6 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -471,44 +471,61 @@ 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.
 
-Theorem eval_divu:
+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. unfold divu. exists z; split. EvalOp. auto.
+  intros. unfold divu_base. exists z; split. EvalOp. auto.
 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. exists z; split. EvalOp. auto.
+  intros. unfold mods_base. exists z; split. EvalOp. auto.
 Qed.
 
-Theorem eval_modu:
+Theorem eval_modu_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.modu x y = Some z ->
-  exists v, eval_expr ge sp e m le (modu a b) v /\ Val.lessdef z v.
+  exists v, eval_expr ge sp e m le (modu_base a b) v /\ Val.lessdef z v.
 Proof.
-  intros. unfold modu. exists z; split. EvalOp. auto.
+  intros. unfold modu_base. exists z; split. EvalOp. auto.
+Qed.
+
+Theorem eval_shrximm:
+  forall le a n x z,
+  eval_expr ge sp e m le a x ->
+  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. 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.