diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-02-19 09:55:45 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-02-19 09:55:45 +0000 |
commit | 3ec022950ec233a2af418aacd1755fce4d701724 (patch) | |
tree | 154256c5c73fda06e874fb05695e14e610ba8ad4 /backend/SelectDivproof.v | |
parent | 9aeba45962e8ba5cde5d81fb701a4c9a3963f4a5 (diff) | |
download | compcert-kvx-3ec022950ec233a2af418aacd1755fce4d701724.tar.gz compcert-kvx-3ec022950ec233a2af418aacd1755fce4d701724.zip |
Add option -Os to optimize for code size rather than for execution speed.
Refactored compilation flags that affect the Coq part (module Compopts).
Added support for C99 for loops with declarations.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2410 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/SelectDivproof.v')
-rw-r--r-- | backend/SelectDivproof.v | 42 |
1 files changed, 25 insertions, 17 deletions
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 0719a5ed..9228cde4 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -369,10 +369,12 @@ Proof. replace (Vint (Int.shru i l)) with (Val.shru (Vint i) (Vint l)). apply eval_shruimm; auto. simpl. erewrite Int.is_power2_range; eauto. -- destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS. - + exists (Vint (Int.divu i n2)); split; auto. - econstructor; eauto. eapply eval_divu_mul; eauto. +- destruct (Compopts.optim_for_size tt). + eapply eval_divu_base; eauto. EvalOp. + + destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS. + * exists (Vint (Int.divu i n2)); split; auto. + econstructor; eauto. eapply eval_divu_mul; eauto. + * eapply eval_divu_base; eauto. EvalOp. Qed. Theorem eval_divu: @@ -412,13 +414,15 @@ Proof. change (Vint (Int.and i (Int.sub n2 Int.one))) with (Val.and (Vint i) (Vint (Int.sub n2 Int.one))). apply eval_andimm. auto. -- destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS. - + econstructor; split. - econstructor; eauto. eapply eval_mod_from_div. - eapply eval_divu_mul; eauto. simpl; eauto. simpl; eauto. - rewrite Int.modu_divu. auto. - red; intros; subst n2; discriminate. +- destruct (Compopts.optim_for_size tt). + eapply eval_modu_base; eauto. EvalOp. + + destruct (divu_mul_params (Int.unsigned n2)) as [[p M] | ] eqn:PARAMS. + * econstructor; split. + econstructor; eauto. eapply eval_mod_from_div. + eapply eval_divu_mul; eauto. simpl; eauto. simpl; eauto. + rewrite Int.modu_divu. auto. + red; intros; subst n2; discriminate. + * eapply eval_modu_base; eauto. EvalOp. Qed. Theorem eval_modu: @@ -485,10 +489,12 @@ Proof. - destruct (Int.ltu l (Int.repr 31)) eqn:LT31. + eapply eval_shrximm; eauto. eapply Val.divs_pow2; eauto. + eapply eval_divs_base; eauto. EvalOp. -- destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. - + exists (Vint (Int.divs i n2)); split; auto. - econstructor; eauto. eapply eval_divs_mul; eauto. +- destruct (Compopts.optim_for_size tt). + eapply eval_divs_base; eauto. EvalOp. + + destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. + * exists (Vint (Int.divs i n2)); split; auto. + econstructor; eauto. eapply eval_divs_mul; eauto. + * eapply eval_divs_base; eauto. EvalOp. Qed. Theorem eval_divs: @@ -524,12 +530,14 @@ Proof. apply eval_mod_from_div. eexact X. simpl; eauto. simpl. auto. + eapply eval_mods_base; eauto. EvalOp. -- destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. - + econstructor; split. - econstructor. eauto. apply eval_mod_from_div with (x := i); auto. - eapply eval_divs_mul with (x := i); eauto. - simpl. auto. +- destruct (Compopts.optim_for_size tt). + eapply eval_mods_base; eauto. EvalOp. + + destruct (divs_mul_params (Int.signed n2)) as [[p M] | ] eqn:PARAMS. + * econstructor; split. + econstructor. eauto. apply eval_mod_from_div with (x := i); auto. + eapply eval_divs_mul with (x := i); eauto. + simpl. auto. + * eapply eval_mods_base; eauto. EvalOp. Qed. Theorem eval_mods: |