-
Notifications
You must be signed in to change notification settings - Fork 0
/
GVN2.v
191 lines (175 loc) · 6.35 KB
/
GVN2.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
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.
Module Ir.
Module GVN2.
(* 2nd condition of replacing p with q:
If p and q are both logical pointers, and
either they point to the same block or
they are both dereferenceable. *)
Definition eqprop_valid2 (m:Ir.Memory.t) (p q:Ir.val) :=
exists l1 o1 l2 o2,
p = Ir.ptr (Ir.plog l1 o1) /\ q = Ir.ptr (Ir.plog l2 o2) /\
(l1 = l2 \/ (* they are logical ptrs on the same block, or *)
(* they are dereferenceable (with minimal access size) *)
(Ir.deref m (Ir.plog l1 o1) 1 = true /\
Ir.deref m (Ir.plog l2 o2) 1 = true)).
(*********************************************************
Important property of eqprop_valid2:
If eqprop_valid2 p q holds, and `icmp eq p, q` evaluates
to true, then p and q are exactly the same pointer!
*********************************************************)
Theorem eqprop_valid2_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_valid2 holds *)
(HEQPROP:eqprop_valid2 (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.
{ unfold Ir.SmallStep.inst_det_step in HNEXT.
rewrite <- HINST in HNEXT.
rewrite <- HOP1, <- HOP2 in HNEXT.
inv HEQPROP.
inv H. inv H0. inv H. inv H0. inv H1.
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; try assumption.
unfold Ir.SmallStep.icmp_eq_ptr in Heq.
destruct H0.
{ (* same block id *)
subst x.
rewrite Nat.eqb_refl in Heq. inv Heq. inv HTRUE.
des_ifs. rewrite Nat.eqb_eq in Heq. congruence.
}
{ destruct H.
destruct (x =? x1) eqn:HEQ.
{ rewrite Nat.eqb_eq in HEQ. subst x.
inv Heq. inv HTRUE. des_ifs. rewrite Nat.eqb_eq in Heq.
subst x0. reflexivity. }
{ (* okay, when the blocks are different. *)
unfold Ir.deref in *.
des_ifs. }
}
}
{ rewrite <- HINST in HCUR. inv HCUR.
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; try assumption.
inv HTRUE.
inv HEQPROP.
inv H. inv H0. inv H. inv H0. inv H1.
rewrite <- HOP1 in HOP0. inv HOP0.
rewrite <- HOP2 in HOP3. inv HOP3.
(* let's get blkid difference from icmp eq nondet cond. *)
assert (HDIFFBLK:x =? x1 = false).
{
unfold Ir.SmallStep.icmp_eq_ptr_nondet_cond in HNONDET.
des_ifs;
destruct (x =? x1) eqn:TT; try simpl in HNONDET; try congruence.
}
rewrite Nat.eqb_neq in HDIFFBLK.
destruct H0; try congruence.
inv H.
unfold Ir.deref in *.
des_ifs.
destruct p0. destruct p0. destruct p. destruct p.
(* singleton-ize get_derefs. *)
(* preparing Memory.get s.. *)
inv HWF.
symmetry in HOP1. apply wf_ptr in HOP1. inv HOP1.
exploit H. ss. intros HH. inv HH. inv H4.
symmetry in HOP2. apply wf_ptr in HOP2. inv HOP2.
exploit H4. ss. intros HH. inv HH. inv H8.
(* Okay, start! op1 *)
dup Heq0.
eapply Ir.get_deref_log in Heq1; try eassumption.
destruct Heq1; try congruence. inv H8.
(* okay, next op2. *)
dup Heq.
eapply Ir.get_deref_log in Heq1; try eassumption.
destruct Heq1; try congruence. inv H8.
(* okay, time to get inbounds conditions. *)
eapply Ir.get_deref_inv in Heq0.
eapply Ir.get_deref_inv in Heq.
repeat (rewrite andb_true_iff in *).
destruct Heq0. destruct H8. destruct Heq. destruct H12.
unfold Ir.MemBlock.inbounds in H11, H10, H13, H14.
(* Now, go toward contradiction. *)
unfold Ir.SmallStep.icmp_eq_ptr_nondet_cond in HNONDET.
rewrite H5, H9 in HNONDET.
rewrite <- Nat.eqb_neq in HDIFFBLK. rewrite HDIFFBLK in HNONDET.
unfold Ir.MemBlock.alive in *.
destruct (Ir.MemBlock.r x3) as [beg1 end1].
simpl in H8. destruct end1; try congruence.
destruct (Ir.MemBlock.r x4) as [beg2 end2].
simpl in H12. destruct end2; try congruence.
rewrite orb_false_r in HNONDET.
simpl in HNONDET.
assert (Ir.MemBlock.n x3 <? x0 = false).
{ rewrite Nat.ltb_ge. rewrite Nat.leb_le in H11. omega. }
rewrite H15 in HNONDET.
assert (Ir.MemBlock.n x4 <? x2 = false).
{ rewrite Nat.ltb_ge. rewrite Nat.leb_le in H13. omega. }
rewrite H16 in HNONDET.
assert (x0 =? Ir.MemBlock.n x3 = false).
{ rewrite Nat.eqb_neq. rewrite Nat.leb_le in H10. omega. }
rewrite H17 in HNONDET.
assert (x2 =? Ir.MemBlock.n x4 = false).
{ rewrite Nat.eqb_neq. rewrite Nat.leb_le in H13. omega. }
rewrite H18 in HNONDET.
rewrite andb_false_r in HNONDET.
simpl in HNONDET. congruence.
omega.
assumption.
assumption.
omega.
assumption.
assumption.
}
}
{ (* 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_valid2_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 GVN2.
End Ir.