-
Notifications
You must be signed in to change notification settings - Fork 0
/
WellTyped.v
175 lines (165 loc) · 6.22 KB
/
WellTyped.v
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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
Require Import Common.
Require Import List.
Require Import sflib.
Require Import Value.
Require Import Lang.
Require Import State.
Module Ir.
Inductive inst_typechecked (md:Ir.IRModule.t) (st:Ir.Config.t)
:Prop :=
| tc_bop:
forall op1 op2 r opty bopc i1 i2 bsz
(HINST: Some (Ir.Inst.ibinop r opty bopc op1 op2) =
Ir.Config.cur_inst md st)
(HTY: Ir.ity bsz = opty)
(HOP1: Some (Ir.num i1) = Ir.Config.get_val st op1)
(HOP2: Some (Ir.num i2) = Ir.Config.get_val st op2),
inst_typechecked md st
| tc_psub:
forall op1 op2 r retty ptrty p1 p2 bsz pty
(HINST: Some (Ir.Inst.ipsub r retty ptrty op1 op2) =
Ir.Config.cur_inst md st)
(HRETTY: Ir.ity bsz = retty)
(HPTY: Ir.ptrty pty = ptrty)
(HOP1: Some (Ir.ptr p1) = Ir.Config.get_val st op1)
(HOP2: Some (Ir.ptr p2) = Ir.Config.get_val st op1),
inst_typechecked md st
| tc_gep:
forall op1 op2 r ptrty p i pty inb
(HINST: Some (Ir.Inst.igep r ptrty op1 op2 inb) =
Ir.Config.cur_inst md st)
(HPTY: Ir.ptrty pty = ptrty)
(HOP1: Some (Ir.ptr p) = Ir.Config.get_val st op1)
(HOP2: Some (Ir.num i) = Ir.Config.get_val st op2),
inst_typechecked md st
| tc_load:
forall retty opval opptr p
(HINST: Some (Ir.Inst.iload retty opval opptr) =
Ir.Config.cur_inst md st)
(HOPPTR: Some (Ir.ptr p) = Ir.Config.get_val st opptr),
inst_typechecked md st
| tc_store:
forall valty opval opptr p v
(HINST: Some (Ir.Inst.istore valty opptr opval) =
Ir.Config.cur_inst md st)
(HOPPTR: Some (Ir.ptr p) = Ir.Config.get_val st opptr)
(HOPVAL: Some v = Ir.Config.get_val st opval),
inst_typechecked md st
| tc_malloc:
forall opty opval i sz r
(HINST: Some (Ir.Inst.imalloc r opty opval) =
Ir.Config.cur_inst md st)
(HOPPTR: Some (Ir.num i) = Ir.Config.get_val st opval)
(HSZTY: Ir.ity sz = opty),
inst_typechecked md st
| tc_bitcast_int:
forall r opval retty bsz i1
(HINST: Some (Ir.Inst.ibitcast r opval retty) =
Ir.Config.cur_inst md st)
(HTY: Ir.ity bsz = retty)
(HOP1: Some (Ir.num i1) = Ir.Config.get_val st opval),
inst_typechecked md st
| tc_bitcast_ptr:
forall r opval retty pty p
(HINST: Some (Ir.Inst.ibitcast r opval retty) =
Ir.Config.cur_inst md st)
(HTY: Ir.ptrty pty = retty)
(HOP1: Some (Ir.ptr p) = Ir.Config.get_val st opval),
inst_typechecked md st
| tc_ptrtoint:
forall r opval retty bsz p
(HINST: Some (Ir.Inst.iptrtoint r opval retty) =
Ir.Config.cur_inst md st)
(HTY: Ir.ity bsz = retty)
(HOP1: Some (Ir.ptr p) = Ir.Config.get_val st opval),
inst_typechecked md st
| tc_inttoptr:
forall r opval retty pty i
(HINST: Some (Ir.Inst.iinttoptr r opval retty) =
Ir.Config.cur_inst md st)
(HTY: Ir.ptrty pty = retty)
(HOP1: Some (Ir.num i) = Ir.Config.get_val st opval),
inst_typechecked md st
| tc_event:
forall opval i
(HINST: Some (Ir.Inst.ievent opval) =
Ir.Config.cur_inst md st)
(HOP1: Some (Ir.num i) = Ir.Config.get_val st opval),
inst_typechecked md st
| tc_icmpeq_int:
forall op1 op2 r opty i1 i2 bsz
(HINST: Some (Ir.Inst.iicmp_eq r opty op1 op2) =
Ir.Config.cur_inst md st)
(HTY: Ir.ity bsz = opty)
(HOP1: Some (Ir.num i1) = Ir.Config.get_val st op1)
(HOP2: Some (Ir.num i2) = Ir.Config.get_val st op2),
inst_typechecked md st
| tc_icmpeq_ptr:
forall op1 op2 r opty p1 p2 pty
(HINST: Some (Ir.Inst.iicmp_eq r opty op1 op2) =
Ir.Config.cur_inst md st)
(HTY: Ir.ptrty pty = opty)
(HOP1: Some (Ir.ptr p1) = Ir.Config.get_val st op1)
(HOP2: Some (Ir.ptr p2) = Ir.Config.get_val st op2),
inst_typechecked md st
| tc_icmpule_int:
forall op1 op2 r opty i1 i2 bsz
(HINST: Some (Ir.Inst.iicmp_ule r opty op1 op2) =
Ir.Config.cur_inst md st)
(HTY: Ir.ity bsz = opty)
(HOP1: Some (Ir.num i1) = Ir.Config.get_val st op1)
(HOP2: Some (Ir.num i2) = Ir.Config.get_val st op2),
inst_typechecked md st
| tc_icmpule_ptr:
forall op1 op2 r opty p1 p2 pty
(HINST: Some (Ir.Inst.iicmp_ule r opty op1 op2) =
Ir.Config.cur_inst md st)
(HTY: Ir.ptrty pty = opty)
(HOP1: Some (Ir.ptr p1) = Ir.Config.get_val st op1)
(HOP2: Some (Ir.ptr p2) = Ir.Config.get_val st op2),
inst_typechecked md st
| tc_free:
forall opptr p
(HINST: Some (Ir.Inst.ifree opptr) =
Ir.Config.cur_inst md st)
(HOPPTR: Some (Ir.ptr p) = Ir.Config.get_val st opptr),
inst_typechecked md st.
(****************************************
Dominatedness relation.
***************************************)
Definition dominates (from to:Ir.IRFunction.pc) (f:Ir.IRFunction.t) :=
forall (exec:list Ir.IRFunction.pc)
(HLEN:List.length exec > 0)
(HBEGIN:List.hd from exec = Ir.IRFunction.get_begin_pc f)
(HEND:List.last exec to = to)
(HVALID: forall_adj
(fun pc pc_next => Ir.IRFunction.valid_next_pc pc pc_next f)
exec = true),
List.In from exec.
(* Theorem: reflexivity of dominatedness. *)
Theorem dominates_refl:
forall (pc:Ir.IRFunction.pc) (f:Ir.IRFunction.t),
dominates pc pc f.
Proof.
intros.
unfold dominates.
intros.
destruct exec.
simpl in HLEN. inversion HLEN.
simpl in HBEGIN.
apply last_head in HEND.
remember (rev (p::exec)) as l.
assert (List.length l = List.length (p::exec)).
{ rewrite Heql. rewrite rev_length. reflexivity. }
destruct l.
- simpl in H. inversion H.
- simpl in HEND.
assert (p :: exec = rev (p0::l)).
{ rewrite Heql. rewrite rev_involutive. reflexivity. }
rewrite H0.
apply in_rev. rewrite rev_involutive. rewrite HEND. constructor.
reflexivity.
- simpl.
apply Gt.gt_Sn_O.
Qed.
End Ir.