diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-07-29 12:10:11 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-07-29 12:10:11 +0000 |
commit | 41b7ecb127b93b1aecc29a298ec21dc94603e6fa (patch) | |
tree | 287ce1cbf88caf973534715c7816d57b9089b265 /ia32/SelectOpproof.v | |
parent | 4bf8b331372388dc9cb39154c986c918df9e071c (diff) | |
download | compcert-41b7ecb127b93b1aecc29a298ec21dc94603e6fa.tar.gz compcert-41b7ecb127b93b1aecc29a298ec21dc94603e6fa.zip |
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
Diffstat (limited to 'ia32/SelectOpproof.v')
-rw-r--r-- | ia32/SelectOpproof.v | 41 |
1 files changed, 29 insertions, 12 deletions
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 8c9c7e64..85802b60 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. |