diff options
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: |