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
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
|
Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
Require Import AST Linking.
Require Import Memory Registers Op RTL Maps CSE2deps.
Require Import HashedSet.
Module RELATION <: SEMILATTICE_WITHOUT_BOTTOM.
Definition t := PSet.t.
Definition eq (x : t) (y : t) := x = y.
Lemma eq_refl: forall x, eq x x.
Proof.
unfold eq. trivial.
Qed.
Lemma eq_sym: forall x y, eq x y -> eq y x.
Proof.
unfold eq. congruence.
Qed.
Lemma eq_trans: forall x y z, eq x y -> eq y z -> eq x z.
Proof.
unfold eq. congruence.
Qed.
Definition beq (x y : t) := if PSet.eq x y then true else false.
Lemma beq_correct: forall x y, beq x y = true -> eq x y.
Proof.
unfold beq.
intros.
destruct PSet.eq; congruence.
Qed.
Definition ge (x y : t) := (PSet.is_subset x y) = true.
Lemma ge_refl: forall x y, eq x y -> ge x y.
Proof.
unfold eq, ge.
intros.
subst y.
apply PSet.is_subset_spec.
trivial.
Qed.
Lemma ge_trans: forall x y z, ge x y -> ge y z -> ge x z.
Proof.
unfold ge.
intros.
rewrite PSet.is_subset_spec in *.
intuition.
Qed.
Definition lub := PSet.inter.
Lemma ge_lub_left: forall x y, ge (lub x y) x.
Proof.
unfold ge, lub.
intros.
apply PSet.is_subset_spec.
intro.
rewrite PSet.ginter.
rewrite andb_true_iff.
intuition.
Qed.
Lemma ge_lub_right: forall x y, ge (lub x y) y.
Proof.
unfold ge, lub.
intros.
apply PSet.is_subset_spec.
intro.
rewrite PSet.ginter.
rewrite andb_true_iff.
intuition.
Qed.
End RELATION.
Module RB := ADD_BOTTOM(RELATION).
Module DS := Dataflow_Solver(RB)(NodeSetForward).
Inductive sym_op : Type :=
| SOp : operation -> sym_op
| SLoad : memory_chunk -> addressing -> sym_op.
Record equation :=
mkequation
{ eq_lhs : reg;
eq_op : sym_op;
eq_args : list reg }.
Definition eq_id := positive.
Definition add_i_j (i : reg) (j : eq_id) (m : Regmap.t PSet.t) :=
Regmap.set i (PSet.add j (Regmap.get i m)) m.
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.
Definition add_ilist_j (ilist : list reg) (j : eq_id) (m : Regmap.t PSet.t) :=
List.fold_left (fun already i => add_i_j i j already) ilist m.
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 get_kills (eqs : PTree.t equation) :
Regmap.t PSet.t :=
PTree.fold (fun already (eqno : eq_id) (eq : equation) =>
add_i_j (eq_lhs eq) eqno
(add_ilist_j (eq_args eq) eqno already)) eqs
(PMap.init PSet.empty).
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.
(*
Lemma xget_kills_monotone :
forall eqs m i j,
PSet.contains (Regmap.get i m) j = true ->
PSet.contains (Regmap.get i (xget_kills eqs m)) j = true.
Proof.
unfold xget_kills.
intros eqs m.
rewrite PTree.fold_spec.
generalize (PTree.elements eqs).
intro.
generalize m.
clear m.
induction l; simpl; trivial.
intros.
apply IHl.
apply add_i_j_monotone.
apply add_ilist_j_monotone.
assumption.
Qed.
*)
Lemma xget_kills_has_lhs :
forall eqs m lhs sop args j,
PTree.get j eqs = Some {| eq_lhs := lhs;
eq_op := sop;
eq_args:= args |} ->
PSet.contains (Regmap.get lhs (xget_kills eqs m)) j = true.
Definition eq_involves (eq : equation) (i : reg) :=
i = (eq_lhs eq) \/ In i (eq_args eq).
Definition totoro := RELATION.lub.
|
