-
Notifications
You must be signed in to change notification settings - Fork 0
/
GVN3.v
338 lines (314 loc) · 11.4 KB
/
GVN3.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
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
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
Require Import Bool.
Require Import Sorting.Permutation.
Require Import Omega.
Require Import sflib.
Require Import Lia.
Require Import Common.
Require Import Value.
Require Import Lang.
Require Import Memory.
Require Import State.
Require Import LoadStore.
Require Import SmallStep.
Require Import SmallStepAux.
Require Import SmallStepWf.
Require Import Refinement.
Require Import SmallStepRefinement.
Require Import Reordering.
Require Import GVN1.
Module Ir.
Module GVN3.
(* 3nd condition of replacing p with q:
If p and q are both computed by the gep inbounds with same
base pointer, it is valid to replace p with q. *)
Definition eqprop_valid3 (m:Ir.Memory.t) (p q:Ir.val) :=
exists p0 idx1 idx2 ty1 ty2,
p = Ir.SmallStep.gep p0 idx1 ty1 m true /\
q = Ir.SmallStep.gep p0 idx2 ty2 m true.
(*********************************************************
Important property of eqprop_valid3:
If eqprop_valid3 p q holds, and `icmp eq p, q` evaluates
to true, then p and q are exactly the same pointer.
*********************************************************)
Lemma twos_compl_twos_compl_add_PTRSZ:
forall n x,
Ir.SmallStep.twos_compl (Ir.SmallStep.twos_compl_add n x Ir.PTRSZ) Ir.PTRSZ =
Ir.SmallStep.twos_compl_add n x Ir.PTRSZ.
Proof.
intros.
rewrite Ir.PTRSZ_def.
unfold Ir.SmallStep.twos_compl_add.
unfold Ir.SmallStep.twos_compl.
rewrite Nat.mod_mod. reflexivity.
apply shiftl_2_nonzero.
Qed.
Theorem gep_never_returns_num:
forall v p idx ty m inb
(HGEP1:Ir.SmallStep.gep p idx ty m inb = v),
~exists n, v = Ir.num n.
Proof.
intros.
unfold Ir.SmallStep.gep in HGEP1.
intros HH.
inv HH.
des_ifs.
Qed.
(* I had to split the big theorem into lemmas due to
Coq bug - Coq does not terminate processing of 'Qed.', due to unknown reason :( *)
Lemma eqprop_valid3_after_icmpeq_true_log:
forall md st st' r ptrty op1 op2 p1 p2 e l0 o0 idx1 ty1 idx2 ty2
(HWF:Ir.Config.wf md st)
(HINST:Some (Ir.Inst.iicmp_eq r ptrty op1 op2) = Ir.Config.cur_inst md st)
(HOP1:Some (Ir.ptr p1) = Ir.Config.get_val st op1)
(HOP2:Some (Ir.ptr p2) = Ir.Config.get_val st op2)
(* geps *)
(HGEP1:(Ir.ptr p1) = Ir.SmallStep.gep (Ir.plog l0 o0) idx1 ty1 (Ir.Config.m st) true)
(HGEP2:(Ir.ptr p2) = Ir.SmallStep.gep (Ir.plog l0 o0) idx2 ty2 (Ir.Config.m st) true)
(* have a small step *)
(HSTEP:Ir.SmallStep.sstep md st (Ir.SmallStep.sr_success e st'))
(* p1 == p2 is true *)
(HTRUE:Some (Ir.num 1) = Ir.Config.get_val st' (Ir.opreg r)),
p1 = p2.
Proof.
intros.
assert (HS:Ir.Config.s st <> []).
{
unfold Ir.Config.cur_inst in HINST.
unfold Ir.Config.cur_fdef_pc in HINST.
des_ifs.
}
inv HSTEP.
{ inv HISTEP; try congruence.
{ unfold Ir.SmallStep.inst_det_step in HNEXT.
rewrite <- HINST in HNEXT.
rewrite <- HOP1, <- HOP2 in HNEXT.
unfold Ir.SmallStep.icmp_eq_ptr in HNEXT.
unfold Ir.SmallStep.gep in *.
des_ifs.
{
rewrite Ir.SmallStep.get_val_update_reg_and_incrpc in HTRUE.
unfold Ir.Config.get_val in HTRUE.
rewrite Ir.Config.get_rval_update_rval_id in HTRUE.
inv HTRUE.
des_ifs.
rewrite Nat.eqb_eq in Heq3. congruence. assumption.
}
{
rewrite Ir.SmallStep.get_val_update_reg_and_incrpc in HTRUE.
unfold Ir.Config.get_val in HTRUE.
rewrite Ir.Config.get_rval_update_rval_id in HTRUE.
inv HTRUE.
des_ifs.
}
}
{ rewrite <- HINST in HCUR.
inv HCUR.
rewrite <- HOP1 in HOP0. inv HOP0.
rewrite <- HOP2 in HOP3. inv HOP3.
unfold Ir.SmallStep.gep in *.
unfold Ir.SmallStep.icmp_eq_ptr_nondet_cond in *.
des_ifs; rewrite Nat.eqb_refl in HNONDET; inv HNONDET.
}
}
{ apply Ir.Config.cur_inst_not_cur_terminator in HINST.
unfold Ir.SmallStep.t_step in HTSTEP. rewrite <- HINST in HTSTEP.
congruence.
}
Qed.
(* due to Coq bug, I made a separated lemmax *)
Lemma gep_helper_small:
forall n l o x1 x3 st p0 n'1
(HVAL2 : Ir.SmallStep.gep (Ir.pphy n l o) x1 x3 (Ir.Config.m st) true =
Ir.ptr p0)
(Heqn'1: n'1 =
Ir.SmallStep.twos_compl_add n (x1 * Ir.ty_bytesz x3)
Ir.PTRSZ),
p0 = Ir.pphy n'1 (n::n'1::l) o.
Proof.
intros. unfold Ir.SmallStep.gep in HVAL2. des_ifs.
Qed.
Lemma gep_helper:
forall n l o x1 x3 x0 x2 st p0 p st' r e md
(HVAL2 : Ir.SmallStep.gep (Ir.pphy n l o) x1 x3 (Ir.Config.m st) true =
Ir.ptr p0)
(HVAL1 : Ir.SmallStep.gep (Ir.pphy n l o) x0 x2 (Ir.Config.m st) true =
Ir.ptr p)
(HTRUE : Some (Ir.num 1) = Ir.Config.get_val st' (Ir.opreg r))
(HNEXT : Some (Ir.SmallStep.sr_success e st') =
match Ir.SmallStep.icmp_eq_ptr p p0 (Ir.Config.m st) with
| Some b =>
Some
(Ir.SmallStep.sr_success Behaviors.Ir.e_none
(Ir.SmallStep.update_reg_and_incrpc md st r
(Ir.SmallStep.to_num b)))
| None => None
end)
(HS : Ir.Config.s st <> []),
Ir.ptr p = Ir.ptr p0.
Proof.
intros.
eapply gep_helper_small in HVAL2; try reflexivity.
eapply gep_helper_small in HVAL1; try reflexivity.
rewrite HVAL1, HVAL2 in HNEXT.
unfold Ir.SmallStep.icmp_eq_ptr in HNEXT.
unfold Ir.SmallStep.p2N in HNEXT.
rewrite Nat.min_id in HNEXT.
rewrite twos_compl_twos_compl_add_PTRSZ in HNEXT.
inversion HNEXT.
rewrite H1 in HTRUE.
rewrite Ir.SmallStep.get_val_update_reg_and_incrpc in HTRUE.
unfold Ir.Config.get_val in HTRUE.
rewrite Ir.Config.get_rval_update_rval_id in HTRUE.
inversion HTRUE.
destruct (Ir.SmallStep.twos_compl_add n (x0 * Ir.ty_bytesz x2) Ir.PTRSZ =?
Ir.SmallStep.twos_compl_add n (x1 * Ir.ty_bytesz x3) Ir.PTRSZ)
eqn:Heq; try congruence.
rewrite Nat.eqb_eq in Heq. rewrite HVAL1, HVAL2, Heq.
reflexivity.
assumption.
Qed. (* This is really strange.. Why Qed never ends? *)
Theorem eqprop_valid3_after_icmpeq_true:
forall md st st' r ptrty op1 op2 v1 v2 e
(HWF:Ir.Config.wf md st)
(HINST:Some (Ir.Inst.iicmp_eq r ptrty op1 op2) = Ir.Config.cur_inst md st)
(HOP1:Some v1 = Ir.Config.get_val st op1)
(HOP2:Some v2 = Ir.Config.get_val st op2)
(* eqprop_valid3 holds *)
(HEQPROP:eqprop_valid3 (Ir.Config.m st) v1 v2)
(* have a small step *)
(HSTEP:Ir.SmallStep.sstep md st (Ir.SmallStep.sr_success e st'))
(* p1 == p2 is true *)
(HTRUE:Some (Ir.num 1) = Ir.Config.get_val st' (Ir.opreg r)),
v1 = v2.
Proof.
intros.
assert (HS:Ir.Config.s st <> []).
{
unfold Ir.Config.cur_inst in HINST.
unfold Ir.Config.cur_fdef_pc in HINST.
des_ifs.
}
inv HSTEP.
{ inv HISTEP; try congruence.
{ inv HEQPROP.
inv H. inv H0. inv H. inv H0. inv H.
destruct x.
{ destruct (Ir.SmallStep.gep (Ir.plog b n) x0 x2 (Ir.Config.m st) true) eqn:HVAL1;
destruct (Ir.SmallStep.gep (Ir.plog b n) x1 x3 (Ir.Config.m st) true) eqn:HVAL2;
try (apply gep_never_returns_num in HVAL1;
exfalso; apply HVAL1; eexists; reflexivity);
try (apply gep_never_returns_num in HVAL2;
exfalso; apply HVAL2; eexists; reflexivity).
{ exploit eqprop_valid3_after_icmpeq_true_log.
{ eassumption. }
{ eassumption. }
{ eassumption. }
{ eassumption. }
{ rewrite HVAL1. reflexivity. }
{ rewrite HVAL2. reflexivity. }
{ eapply Ir.SmallStep.ss_inst.
eapply Ir.SmallStep.s_det.
eassumption. }
{ eassumption. }
intros HH. congruence.
}
{ unfold Ir.SmallStep.inst_det_step in HNEXT.
rewrite <- HINST in HNEXT.
rewrite <- HOP2 in HNEXT. des_ifs.
rewrite Ir.SmallStep.get_val_update_reg_and_incrpc in HTRUE.
unfold Ir.Config.get_val in HTRUE.
rewrite Ir.Config.get_rval_update_rval_id in HTRUE.
inv HTRUE. assumption.
}
{ unfold Ir.SmallStep.inst_det_step in HNEXT.
rewrite <- HINST in HNEXT.
rewrite <- HOP1 in HNEXT. des_ifs.
rewrite Ir.SmallStep.get_val_update_reg_and_incrpc in HTRUE.
unfold Ir.Config.get_val in HTRUE.
rewrite Ir.Config.get_rval_update_rval_id in HTRUE.
inv HTRUE. assumption.
}
{ unfold Ir.SmallStep.inst_det_step in HNEXT.
rewrite <- HINST in HNEXT.
rewrite <- HOP2 in HNEXT. des_ifs.
}
}
{ (* phy. *)
unfold Ir.SmallStep.inst_det_step in HNEXT.
rewrite <- HINST in HNEXT.
rewrite <- HOP1, <- HOP2 in HNEXT.
destruct (Ir.SmallStep.gep (Ir.pphy n l o) x0 x2 (Ir.Config.m st) true) eqn:HVAL1;
destruct (Ir.SmallStep.gep (Ir.pphy n l o) x1 x3 (Ir.Config.m st) true) eqn:HVAL2;
try (apply gep_never_returns_num in HVAL1;
exfalso; apply HVAL1; eexists; reflexivity);
try (apply gep_never_returns_num in HVAL2;
exfalso; apply HVAL2; eexists; reflexivity).
{ eapply gep_helper; try eassumption. }
{ inv HNEXT.
rewrite Ir.SmallStep.get_val_update_reg_and_incrpc in HTRUE.
unfold Ir.Config.get_val in HTRUE.
rewrite Ir.Config.get_rval_update_rval_id in HTRUE.
inv HTRUE. assumption. }
{ inv HNEXT.
rewrite Ir.SmallStep.get_val_update_reg_and_incrpc in HTRUE.
unfold Ir.Config.get_val in HTRUE.
rewrite Ir.Config.get_rval_update_rval_id in HTRUE.
inv HTRUE. assumption. }
{ reflexivity. }
}
}
{ (* well, cannot be nondet... *)
rewrite <- HINST in HCUR. inv HCUR.
rewrite <- HOP1 in HOP0. inv HOP0.
rewrite <- HOP2 in HOP3. inv HOP3.
inv HEQPROP.
inv H. inv H0. inv H. inv H0. destruct H.
destruct x.
{ assert (HOFS1:exists ofs1, p1 = (Ir.plog b ofs1)).
{ unfold Ir.SmallStep.gep in H.
unfold Ir.SmallStep.gep in H0.
unfold Ir.SmallStep.icmp_eq_ptr_nondet_cond in HNONDET.
des_ifs; eexists; reflexivity. }
assert (HOFS2:exists ofs2, p2 = (Ir.plog b ofs2)).
{ unfold Ir.SmallStep.gep in H.
unfold Ir.SmallStep.gep in H0.
unfold Ir.SmallStep.icmp_eq_ptr_nondet_cond in HNONDET.
des_ifs; eexists; reflexivity. }
inv HOFS1. inv HOFS2.
unfold Ir.SmallStep.icmp_eq_ptr_nondet_cond in HNONDET.
des_ifs;
rewrite Nat.eqb_refl in HNONDET; inv HNONDET.
}
{ assert (HOFS1:exists a1 b1 c1, p1 = (Ir.pphy a1 b1 c1)).
{ unfold Ir.SmallStep.gep in H.
unfold Ir.SmallStep.gep in H0.
unfold Ir.SmallStep.icmp_eq_ptr_nondet_cond in HNONDET.
des_ifs; eexists; reflexivity. }
assert (HOFS2:exists a2 b2 c2, p2 = (Ir.pphy a2 b2 c2)).
{ unfold Ir.SmallStep.gep in H.
unfold Ir.SmallStep.gep in H0.
unfold Ir.SmallStep.icmp_eq_ptr_nondet_cond in HNONDET.
des_ifs; eexists; reflexivity. }
inv HOFS1. inv H1. inv H2.
inv HOFS2. inv H1. inv H2.
unfold Ir.SmallStep.icmp_eq_ptr_nondet_cond in HNONDET.
des_ifs.
}
}
}
{ (* terminator! *)
apply Ir.Config.cur_inst_not_cur_terminator in HINST.
unfold Ir.SmallStep.t_step in HTSTEP.
rewrite <- HINST in HTSTEP.
congruence.
}
Qed.
(*********************************************************
Okay, from theorem `eqprop_valid3_after_icmpeq_true`,
we can say that two pointers have same value after
`p == q` check.
It is trivial to have same execution when same value
is given, hence not proved.
*********************************************************)
End GVN3.
End Ir.