blob: 2501c7f0c00b2acefe1b6557f21d0184af6ab302 (
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. *)
(* *)
(* *********************************************************************)
(** Proof of type preservation for the [RRE] pass. *)
Require Import Coqlib.
Require Import AST.
Require Import Locations.
Require Import Linear.
Require Import Lineartyping.
Require Import Conventions.
Require Import RRE.
Require Import RREproof.
Remark wt_cons:
forall f c i, wt_instr f i -> wt_code f c -> wt_code f (i::c).
Proof.
intros; red; intros. simpl in H1; destruct H1. congruence. auto.
Qed.
Hint Constructors wt_instr : linearty.
Hint Resolve wt_cons: linearty.
Definition wt_eqs (eqs: equations) :=
forall e, In e eqs -> slot_type (e_slot e) = mreg_type (e_reg e).
Lemma wt_eqs_nil:
wt_eqs nil.
Proof. red; simpl; tauto. Qed.
Lemma wt_eqs_cons:
forall r s eqs,
slot_type s = mreg_type r -> wt_eqs eqs -> wt_eqs (mkeq r s :: eqs).
Proof.
intros; red; simpl; intros. destruct H1. subst; simpl; auto. auto.
Qed.
Lemma wt_kill_loc:
forall l eqs,
wt_eqs eqs -> wt_eqs (kill_loc l eqs).
Proof.
intros; red; intros. exploit In_kill_loc; eauto. intros [A B]. auto.
Qed.
Lemma wt_kill_locs:
forall ll eqs,
wt_eqs eqs -> wt_eqs (kill_locs ll eqs).
Proof.
intros; red; intros. exploit In_kill_locs; eauto. intros [A B]. auto.
Qed.
Lemma wt_kill_temps:
forall eqs, wt_eqs eqs -> wt_eqs (kill_temps eqs).
Proof.
exact (wt_kill_locs temporaries).
Qed.
Lemma wt_kill_at_move:
forall eqs, wt_eqs eqs -> wt_eqs (kill_at_move eqs).
Proof.
exact (wt_kill_locs destroyed_at_move).
Qed.
Hint Resolve wt_eqs_nil wt_eqs_cons wt_kill_loc wt_kill_locs
wt_kill_temps wt_kill_at_move: linearty.
Lemma wt_kill_op:
forall op eqs, wt_eqs eqs -> wt_eqs (kill_op op eqs).
Proof.
intros; destruct op; simpl; apply wt_kill_locs; auto.
Qed.
Hint Resolve wt_kill_op: linearty.
Lemma wt_transf_code:
forall f c eqs, wt_code f c -> wt_eqs eqs ->
wt_code (transf_function f) (transf_code eqs c).
Proof.
induction c; intros; simpl.
red; simpl; tauto.
assert (WI: wt_instr f a) by auto with coqlib.
assert (WC: wt_code f c) by (red; auto with coqlib).
clear H.
inv WI; auto 10 with linearty.
destruct (is_incoming s) as []_eqn. auto with linearty.
destruct (contains_equation s r eqs). auto with linearty.
destruct (find_reg_containing s eqs) as [r'|]_eqn; auto with linearty.
assert (mreg_type r' = mreg_type r).
exploit H0. eapply find_reg_containing_sound; eauto. simpl. congruence.
destruct (safe_move_insertion c); auto 10 with linearty.
Qed.
Lemma program_typing_preserved:
forall p, wt_program p -> wt_program (transf_program p).
Proof.
intros. red; intros. exploit transform_program_function; eauto.
intros [f0 [A B]]. subst f. exploit H; eauto. intros WTFD.
inv WTFD; simpl; constructor. red; simpl.
apply wt_transf_code; auto with linearty.
Qed.
|
