blob: 57e1271d1c9fd0bf95efb18bf21759ba1a68be66 (
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
|
(* *********************************************************************)
(* *)
(* 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 Values.
Require Import Mem.
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_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 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.
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.
|
