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 --- arm/SelectOpproof.v | 108 +++++++++++++++++++++++++++++++--------------------- 1 file changed, 64 insertions(+), 44 deletions(-) (limited to 'arm/SelectOpproof.v') diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index a71ead78..9beb1ad8 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -468,83 +468,103 @@ Proof. reflexivity. 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_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: +Theorem eval_divu_base: forall le a x b 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 x b 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))). TrivialExists. - 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. +- destruct x; simpl in H0; try discriminate. + destruct (Int.ltu n (Int.repr 31)) eqn:LT31; inv H0. + assert (A: eval_expr ge sp e m (Vint i :: le) (Eletvar 0) (Vint i)) + by (constructor; auto). + exploit (eval_shrimm (Int.repr 31)). eexact A. + intros [v [B LD]]. simpl in LD. + change (Int.ltu (Int.repr 31) Int.iwordsize) with true in LD. + simpl in LD; inv LD. + exploit (eval_shruimm (Int.sub Int.iwordsize n)). eexact B. + intros [v [C LD]]. simpl in LD. + assert (RANGE: Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize = true). + { + generalize (Int.ltu_inv _ _ LT31). intros. + unfold Int.sub, Int.ltu. rewrite Int.unsigned_repr_wordsize. + rewrite Int.unsigned_repr. apply zlt_true. + assert (Int.unsigned n <> 0). + { red; intros; elim H1. rewrite <- (Int.repr_unsigned n). rewrite H2; reflexivity. } + omega. + change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0. + generalize Int.wordsize_max_unsigned; omega. + } + rewrite RANGE in LD. inv LD. + exploit eval_add. eexact A. eexact C. intros [v [D LD]]. + simpl in LD. inv LD. + exploit (eval_shrimm n). eexact D. intros [v [E LD]]. + simpl in LD. + assert (RANGE2: Int.ltu n Int.iwordsize = true). + { + generalize (Int.ltu_inv _ _ LT31). intros. + unfold Int.ltu. rewrite Int.unsigned_repr_wordsize. apply zlt_true. + change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0. + omega. + } + rewrite RANGE2 in LD. inv LD. + econstructor; split. econstructor. eassumption. eexact E. + rewrite Int.shrx_shr_2 by auto. + auto. Qed. Theorem eval_shl: binary_constructor_sound shl Val.shl. -- cgit