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
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
|
Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Memory Registers Op RTL Maps.
Require Import Globalenvs Values.
Require Import Linking Values Memory Globalenvs Events Smallstep.
Require Import Registers Op RTL.
Require Import CSE3analysis CSE2deps CSE2depsproof HashedSet.
Require Import Lia.
Lemma subst_args_notin :
forall (rs : regset) dst v args,
~ In dst args ->
(rs # dst <- v) ## args = rs ## args.
Proof.
induction args; simpl; trivial.
intro NOTIN.
destruct (peq a dst).
{
subst a.
intuition congruence.
}
rewrite Regmap.gso by congruence.
f_equal.
apply IHargs.
intuition congruence.
Qed.
Lemma add_i_j_adds : forall i j m,
PSet.contains (Regmap.get i (add_i_j i j m)) j = true.
Proof.
intros.
unfold add_i_j.
rewrite Regmap.gss.
auto with pset.
Qed.
Hint Resolve add_i_j_adds: cse3.
Lemma add_i_j_monotone : forall i j i' j' m,
PSet.contains (Regmap.get i' m) j' = true ->
PSet.contains (Regmap.get i' (add_i_j i j m)) j' = true.
Proof.
intros.
unfold add_i_j.
destruct (peq i i').
- subst i'.
rewrite Regmap.gss.
destruct (peq j j').
+ subst j'.
apply PSet.gadds.
+ eauto with pset.
- rewrite Regmap.gso.
assumption.
congruence.
Qed.
Hint Resolve add_i_j_monotone: cse3.
Lemma add_ilist_j_monotone : forall ilist j i' j' m,
PSet.contains (Regmap.get i' m) j' = true ->
PSet.contains (Regmap.get i' (add_ilist_j ilist j m)) j' = true.
Proof.
induction ilist; simpl; intros until m; intro CONTAINS; auto with cse3.
Qed.
Hint Resolve add_ilist_j_monotone: cse3.
Lemma add_ilist_j_adds : forall ilist j m,
forall i, In i ilist ->
PSet.contains (Regmap.get i (add_ilist_j ilist j m)) j = true.
Proof.
induction ilist; simpl; intros until i; intro IN.
contradiction.
destruct IN as [HEAD | TAIL]; subst; auto with cse3.
Qed.
Hint Resolve add_ilist_j_adds: cse3.
Definition xlget_kills (eqs : list (eq_id * equation)) (m : Regmap.t PSet.t) :
Regmap.t PSet.t :=
List.fold_left (fun already (item : eq_id * equation) =>
add_i_j (eq_lhs (snd item)) (fst item)
(add_ilist_j (eq_args (snd item)) (fst item) already)) eqs m.
Lemma xlget_kills_monotone :
forall eqs m i j,
PSet.contains (Regmap.get i m) j = true ->
PSet.contains (Regmap.get i (xlget_kills eqs m)) j = true.
Proof.
induction eqs; simpl; trivial.
intros.
auto with cse3.
Qed.
Hint Resolve xlget_kills_monotone : cse3.
Lemma xlget_kills_has_lhs :
forall eqs m lhs sop args j,
In (j, {| eq_lhs := lhs;
eq_op := sop;
eq_args:= args |}) eqs ->
PSet.contains (Regmap.get lhs (xlget_kills eqs m)) j = true.
Proof.
induction eqs; simpl.
contradiction.
intros until j.
intro HEAD_TAIL.
destruct HEAD_TAIL as [HEAD | TAIL]; subst; simpl.
- auto with cse3.
- eapply IHeqs. eassumption.
Qed.
Hint Resolve xlget_kills_has_lhs : cse3.
Lemma xlget_kills_has_arg :
forall eqs m lhs sop arg args j,
In (j, {| eq_lhs := lhs;
eq_op := sop;
eq_args:= args |}) eqs ->
In arg args ->
PSet.contains (Regmap.get arg (xlget_kills eqs m)) j = true.
Proof.
induction eqs; simpl.
contradiction.
intros until j.
intros HEAD_TAIL ARG.
destruct HEAD_TAIL as [HEAD | TAIL]; subst; simpl.
- auto with cse3.
- eapply IHeqs; eassumption.
Qed.
Hint Resolve xlget_kills_has_arg : cse3.
Lemma get_kills_has_lhs :
forall eqs lhs sop args j,
PTree.get j eqs = Some {| eq_lhs := lhs;
eq_op := sop;
eq_args:= args |} ->
PSet.contains (Regmap.get lhs (get_kills eqs)) j = true.
Proof.
unfold get_kills.
intros.
rewrite PTree.fold_spec.
change (fold_left
(fun (a : Regmap.t PSet.t) (p : positive * equation) =>
add_i_j (eq_lhs (snd p)) (fst p)
(add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills.
eapply xlget_kills_has_lhs.
apply PTree.elements_correct.
eassumption.
Qed.
Lemma get_kills_has_arg :
forall eqs lhs sop arg args j,
PTree.get j eqs = Some {| eq_lhs := lhs;
eq_op := sop;
eq_args:= args |} ->
In arg args ->
PSet.contains (Regmap.get arg (get_kills eqs)) j = true.
Proof.
unfold get_kills.
intros.
rewrite PTree.fold_spec.
change (fold_left
(fun (a : Regmap.t PSet.t) (p : positive * equation) =>
add_i_j (eq_lhs (snd p)) (fst p)
(add_ilist_j (eq_args (snd p)) (fst p) a))) with xlget_kills.
eapply xlget_kills_has_arg.
- apply PTree.elements_correct.
eassumption.
- assumption.
Qed.
Definition eq_involves (eq : equation) (i : reg) :=
i = (eq_lhs eq) \/ In i (eq_args eq).
Section SOUNDNESS.
Variable F V : Type.
Variable genv: Genv.t F V.
Variable sp : val.
Context {ctx : eq_context}.
Definition sem_eq (eq : equation) (rs : regset) (m : mem) :=
match eq_op eq with
| SOp op =>
match eval_operation genv sp op (rs ## (eq_args eq)) m with
| Some v => rs # (eq_lhs eq) = v
| None => False
end
| SLoad chunk addr =>
match
match eval_addressing genv sp addr rs##(eq_args eq) with
| Some a => Mem.loadv chunk m a
| None => None
end
with
| Some dat => rs # (eq_lhs eq) = dat
| None => rs # (eq_lhs eq) = default_notrap_load_value chunk
end
end.
Definition sem_rel (rel : RELATION.t) (rs : regset) (m : mem) :=
forall i eq,
PSet.contains rel i = true ->
eq_catalog ctx i = Some eq ->
sem_eq eq rs m.
Hypothesis ctx_kills_has_lhs :
forall lhs sop args j,
eq_catalog ctx j = Some {| eq_lhs := lhs;
eq_op := sop;
eq_args:= args |} ->
PSet.contains (eq_kills ctx lhs) j = true.
Hypothesis ctx_kills_has_arg :
forall lhs sop args j,
eq_catalog ctx j = Some {| eq_lhs := lhs;
eq_op := sop;
eq_args:= args |} ->
forall arg,
In arg args ->
PSet.contains (eq_kills ctx arg) j = true.
Theorem kill_reg_sound :
forall rel rs m dst v,
(sem_rel rel rs m) ->
(sem_rel (kill_reg (ctx:=ctx) dst rel) (rs#dst <- v) m).
Proof.
unfold sem_rel, sem_eq, kill_reg.
intros until v.
intros REL i eq.
specialize REL with (i := i) (eq0 := eq).
destruct eq as [lhs sop args]; simpl.
specialize ctx_kills_has_lhs with (lhs := lhs) (sop := sop) (args := args) (j := i).
specialize ctx_kills_has_arg with (lhs := lhs) (sop := sop) (args := args) (j := i) (arg := dst).
intuition.
rewrite PSet.gsubtract in H.
rewrite andb_true_iff in H.
rewrite negb_true_iff in H.
intuition.
simpl in *.
assert ({In dst args} + {~In dst args}) as IN_ARGS.
{
apply List.in_dec.
apply peq.
}
destruct IN_ARGS as [IN_ARGS | NOTIN_ARGS].
{ intuition.
congruence.
}
destruct (peq dst lhs).
{
congruence.
}
rewrite subst_args_notin by assumption.
destruct sop.
- destruct (eval_operation genv sp o rs ## args m) as [ev | ]; trivial.
rewrite Regmap.gso by congruence.
assumption.
- rewrite Regmap.gso by congruence.
assumption.
Qed.
End SOUNDNESS.
|
