diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:27:50 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2007-08-04 07:27:50 +0000 |
commit | 355b4abcee015c3fae9ac5653c25259e104a886c (patch) | |
tree | cfdb5b17f36b815bb358699cf420f64eba9dfe25 /backend/Tunnelingtyping.v | |
parent | 22ff08b38616ceef336f5f974d4edc4d37d955e8 (diff) |
Fusion des modifications faites sur les branches "tailcalls" et "smallstep".
En particulier:
- Semantiques small-step depuis RTL jusqu'a PPC
- Cminor independant du processeur
- Ajout passes Selection et Reload
- Ajout des langages intermediaires CminorSel et LTLin correspondants
- Ajout des tailcalls depuis Cminor jusqu'a PPC
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Tunnelingtyping.v')
-rw-r--r-- | backend/Tunnelingtyping.v | 61 |
1 files changed, 50 insertions, 11 deletions
diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v index 6281afa..c611067 100644 --- a/backend/Tunnelingtyping.v +++ b/backend/Tunnelingtyping.v @@ -11,26 +11,65 @@ Require Import Locations. Require Import LTL. Require Import LTLtyping. Require Import Tunneling. +Require Import Tunnelingproof. (** Tunneling preserves typing. *) -Lemma wt_tunnel_block: - forall f b, - wt_block f b -> - wt_block (tunnel_function f) (tunnel_block f b). +Lemma branch_target_rec_valid: + forall f, wt_function f -> + forall count pc pc', + branch_target_rec f pc count = Some pc' -> + valid_successor f pc -> + valid_successor f pc'. Proof. - induction 1; simpl; econstructor; eauto. + induction count; simpl. + intros; discriminate. + intros until pc'. caseEq (is_goto_instr (fn_code f)!pc); intros. + generalize (is_goto_instr_correct _ _ H0). intro. + eapply IHcount; eauto. + generalize (wt_instrs _ H _ _ H3); intro WTI; inv WTI. auto. + inv H1; auto. +Qed. + +Lemma tunnel_valid_successor: + forall f pc, + valid_successor f pc -> valid_successor (tunnel_function f) pc. +Proof. + intros. destruct H as [i AT]. + unfold valid_successor; simpl. rewrite PTree.gmap. rewrite AT. + simpl. exists (tunnel_instr f i); auto. +Qed. + +Lemma branch_target_valid: + forall f pc, + wt_function f -> + valid_successor f pc -> + valid_successor (tunnel_function f) (branch_target f pc). +Proof. + intros. apply tunnel_valid_successor. + unfold branch_target. caseEq (branch_target_rec f pc 10); intros. + eapply branch_target_rec_valid; eauto. + auto. +Qed. + +Lemma wt_tunnel_instr: + forall f i, + wt_function f -> + wt_instr f i -> wt_instr (tunnel_function f) (tunnel_instr f i). +Proof. + intros; inv H0; simpl; econstructor; eauto; + eapply branch_target_valid; eauto. Qed. Lemma wt_tunnel_function: forall f, wt_function f -> wt_function (tunnel_function f). Proof. - unfold wt_function; intros until b. - simpl. rewrite PTree.gmap. unfold option_map. - caseEq (fn_code f)!pc. intros b0 AT EQ. - injection EQ; intros; subst b. - apply wt_tunnel_block. eauto. - intros; discriminate. + intros. inversion H. constructor; simpl; auto. + intros until instr. rewrite PTree.gmap. unfold option_map. + caseEq (fn_code f)!pc. intros b0 AT EQ. inv EQ. + apply wt_tunnel_instr; eauto. + congruence. + eapply branch_target_valid; eauto. Qed. Lemma wt_tunnel_fundef: |