From 41b7ecb127b93b1aecc29a298ec21dc94603e6fa Mon Sep 17 00:00:00 2001 From: xleroy 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 --- ia32/Asm.v | 8 ++++++++ ia32/Asmgen.v | 8 ++++++++ ia32/Asmgenproof1.v | 4 ++++ ia32/ConstpropOp.vp | 2 ++ ia32/Machregs.v | 6 ++++++ ia32/Op.v | 10 ++++++++++ ia32/PrintAsm.ml | 4 ++++ ia32/SelectOp.vp | 11 +++++++---- ia32/SelectOpproof.v | 41 +++++++++++++++++++++++++++++------------ 9 files changed, 78 insertions(+), 16 deletions(-) (limited to 'ia32') 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. -- cgit v1.2.3