blob: 743b4681c2d807483b3963737e5948f84be47099 (
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
104
105
106
107
108
109
|
(* *********************************************************************)
(* *)
(* 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 UnionFind.
Require Import AST.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Op.
Require Import Locations.
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.
|
