diff options
Diffstat (limited to 'backend/Tunnelingtyping.v')
-rw-r--r-- | backend/Tunnelingtyping.v | 103 |
1 files changed, 0 insertions, 103 deletions
diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v deleted file mode 100644 index dfc36b60..00000000 --- a/backend/Tunnelingtyping.v +++ /dev/null @@ -1,103 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Type preservation for the Tunneling pass *) - -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import LTL. -Require Import LTLtyping. -Require Import Tunneling. -Require Import Tunnelingproof. - -(** Tunneling preserves typing. *) - -Lemma branch_target_valid_1: - forall f pc, wt_function f -> - valid_successor f pc -> - valid_successor f (branch_target f pc). -Proof. - intros. - assert (forall n p, - (count_gotos f p < n)%nat -> - valid_successor f p -> - valid_successor f (branch_target f p)). - induction n; intros. - omegaContradiction. - elim H2; intros i EQ. - generalize (record_gotos_correct f p). rewrite EQ. - destruct i; try congruence. - intros [A | [B C]]. congruence. - generalize (wt_instrs _ H _ _ EQ); intro WTI; inv WTI. - rewrite B. apply IHn. omega. auto. - - apply H1 with (Datatypes.S (count_gotos f pc)); 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 (record_gotos 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. apply branch_target_valid_1; auto. -Qed. - -Lemma wt_tunnel_instr: - forall f i, - wt_function f -> - wt_instr f i -> wt_instr (tunnel_function f) (tunnel_instr (record_gotos f) i). -Proof. - intros; inv H0; simpl; econstructor; eauto; - try (eapply branch_target_valid; eauto). - intros. exploit list_in_map_inv; eauto. intros [x [A B]]. subst lbl. - eapply branch_target_valid; eauto. - rewrite list_length_z_map. auto. -Qed. - -Lemma wt_tunnel_function: - forall f, wt_function f -> wt_function (tunnel_function f). -Proof. - 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: - forall f, wt_fundef f -> wt_fundef (tunnel_fundef f). -Proof. - intros. inversion H; simpl. constructor; auto. - constructor. apply wt_tunnel_function; auto. -Qed. - -Lemma program_typing_preserved: - forall (p: LTL.program), - wt_program p -> wt_program (tunnel_program p). -Proof. - intros; red; intros. - generalize (transform_program_function tunnel_fundef p i f H0). - intros [f0 [IN TRANSF]]. - subst f. apply wt_tunnel_fundef. eauto. -Qed. |