blob: dfc36b60f66a6a63cac25efce848826ca6e63b2d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
|
(* *********************************************************************)
(* *)
(* 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.
|
