diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-17 09:00:42 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-03-17 09:00:42 +0000 |
| commit | 7d4128f2e6d73b8f105472f12157488d38898eff (patch) | |
| tree | c76f90730ded3a2581f74977abe394b39d6cfc2d /backend/CSEproof.v | |
| parent | 707b6a1ae9660b13cf6f68c7c0ce74017f5981c5 (diff) | |
More aggressive CSE across Ibuiltin.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2152 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/CSEproof.v')
| -rw-r--r-- | backend/CSEproof.v | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 44d23c8..8fc9407 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -307,7 +307,8 @@ Proof. apply wf_add_store; auto. apply wf_empty_numbering. apply wf_empty_numbering. - apply wf_add_unknown. apply wf_kill_equations; auto. + destruct e; (apply wf_empty_numbering || + apply wf_add_unknown; auto; apply wf_kill_equations; auto). Qed. (** As a consequence, the numberings computed by the static analysis @@ -1088,9 +1089,17 @@ Proof. apply wt_regset_assign; auto. rewrite H6. eapply external_call_well_typed; eauto. eapply analysis_correct_1; eauto. simpl; auto. - unfold transfer; rewrite H. - apply add_unknown_satisfiable. apply wf_kill_equations. eapply wf_analyze; eauto. - eapply kill_loads_satisfiable; eauto. + unfold transfer; rewrite H. + assert (CASE1: numbering_satisfiable ge sp (rs#res <- v) m' empty_numbering). + { apply empty_numbering_satisfiable. } + assert (CASE2: m' = m -> numbering_satisfiable ge sp (rs#res <- v) m' (add_unknown approx#pc res)). + { intros. rewrite H1. apply add_unknown_satisfiable. + eapply wf_analyze; eauto. auto. } + assert (CASE3: numbering_satisfiable ge sp (rs#res <- v) m' + (add_unknown (kill_loads approx#pc) res)). + { apply add_unknown_satisfiable. apply wf_kill_equations. eapply wf_analyze; eauto. + eapply kill_loads_satisfiable; eauto. } + destruct ef; auto; apply CASE2; inv H0; auto. (* Icond *) destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?. |