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
|
Require Import AST Maps.
Require Import Op Registers.
Require Import RTL BTL.
Require Import BTL_SEsimuref BTL_SEtheory OptionMonad.
Require Import Impure.ImpHCons.
Import Notations.
Import HConsing.
Local Open Scope option_monad_scope.
Local Open Scope impure.
Import ListNotations.
Local Open Scope list_scope.
(** Notations to make lemmas more readable *)
Notation "'sval_refines' ctx sv1 sv2" := (eval_sval ctx sv1 = eval_sval ctx sv2)
(only parsing, at level 0, ctx at next level, sv1 at next level, sv2 at next level): hse.
Local Open Scope hse.
Notation "'list_sval_refines' ctx lsv1 lsv2" := (eval_list_sval ctx lsv1 = eval_list_sval ctx lsv2)
(only parsing, at level 0, ctx at next level, lsv1 at next level, lsv2 at next level): hse.
Notation "'smem_refines' ctx sm1 sm2" := (eval_smem ctx sm1 = eval_smem ctx sm2)
(only parsing, at level 0, ctx at next level, sm1 at next level, sm2 at next level): hse.
(** Debug printer *)
Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := RET tt. (* TO REMOVE DEBUG INFO *)
(*Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := DO s <~ k x;; println ("DEBUG simu_check:" +; s). (* TO INSERT DEBUG INFO *)*)
Definition DEBUG (s: pstring): ?? unit := XDEBUG tt (fun _ => RET s).
(** * Implementation of Data-structure use in Hash-consing *)
Definition sval_get_hid (sv: sval): hashcode :=
match sv with
| Sundef hid => hid
| Sinput _ hid => hid
| Sop _ _ hid => hid
| Sload _ _ _ _ _ hid => hid
end.
Definition list_sval_get_hid (lsv: list_sval): hashcode :=
match lsv with
| Snil hid => hid
| Scons _ _ hid => hid
end.
Definition smem_get_hid (sm: smem): hashcode :=
match sm with
| Sinit hid => hid
| Sstore _ _ _ _ _ hid => hid
end.
Definition sval_set_hid (sv: sval) (hid: hashcode): sval :=
match sv with
| Sundef _ => Sundef hid
| Sinput r _ => Sinput r hid
| Sop o lsv _ => Sop o lsv hid
| Sload sm trap chunk addr lsv _ => Sload sm trap chunk addr lsv hid
end.
Definition list_sval_set_hid (lsv: list_sval) (hid: hashcode): list_sval :=
match lsv with
| Snil _ => Snil hid
| Scons sv lsv _ => Scons sv lsv hid
end.
Definition smem_set_hid (sm: smem) (hid: hashcode): smem :=
match sm with
| Sinit _ => Sinit hid
| Sstore sm chunk addr lsv srce _ => Sstore sm chunk addr lsv srce hid
end.
(** * Implementation of symbolic execution *)
Section CanonBuilding.
Variable hC_sval: hashinfo sval -> ?? sval.
Hypothesis hC_sval_correct: forall s,
WHEN hC_sval s ~> s' THEN forall ctx,
sval_refines ctx (hdata s) s'.
Variable hC_list_sval: hashinfo list_sval -> ?? list_sval.
Hypothesis hC_list_sval_correct: forall lh,
WHEN hC_list_sval lh ~> lh' THEN forall ctx,
list_sval_refines ctx (hdata lh) lh'.
Variable hC_smem: hashinfo smem -> ?? smem.
Hypothesis hC_smem_correct: forall hm,
WHEN hC_smem hm ~> hm' THEN forall ctx,
smem_refines ctx (hdata hm) hm'.
(* First, we wrap constructors for hashed values !*)
Definition reg_hcode := 1.
Definition op_hcode := 2.
Definition load_hcode := 3.
Definition undef_code := 4.
Definition hSinput_hcodes (r: reg) :=
DO hc <~ hash reg_hcode;;
DO hv <~ hash r;;
RET [hc;hv].
Extraction Inline hSinput_hcodes.
Definition hSinput (r:reg): ?? sval :=
DO hv <~ hSinput_hcodes r;;
hC_sval {| hdata:=Sinput r unknown_hid; hcodes :=hv; |}.
Lemma hSinput_correct r:
WHEN hSinput r ~> hv THEN forall ctx,
sval_refines ctx hv (Sinput r unknown_hid).
Proof.
wlp_simplify.
Qed.
Global Opaque hSinput.
Local Hint Resolve hSinput_correct: wlp.
Definition hSop_hcodes (op:operation) (lsv: list_sval) :=
DO hc <~ hash op_hcode;;
DO hv <~ hash op;;
RET [hc;hv;list_sval_get_hid lsv].
Extraction Inline hSop_hcodes.
Definition hSop (op:operation) (lsv: list_sval): ?? sval :=
DO hv <~ hSop_hcodes op lsv;;
hC_sval {| hdata:=Sop op lsv unknown_hid; hcodes :=hv |}.
Lemma hSop_fSop_correct op lsv:
WHEN hSop op lsv ~> hv THEN forall ctx,
sval_refines ctx hv (fSop op lsv).
Proof.
wlp_simplify.
Qed.
Global Opaque hSop.
Local Hint Resolve hSop_fSop_correct: wlp_raw.
Lemma hSop_correct op lsv1:
WHEN hSop op lsv1 ~> hv THEN forall ctx lsv2
(LR: list_sval_refines ctx lsv1 lsv2),
sval_refines ctx hv (Sop op lsv2 unknown_hid).
Proof.
wlp_xsimplify ltac:(intuition eauto with wlp wlp_raw).
rewrite <- LR. erewrite H; eauto.
Qed.
Local Hint Resolve hSop_correct: wlp.
Definition hSload_hcodes (sm: smem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval):=
DO hc <~ hash load_hcode;;
DO hv1 <~ hash trap;;
DO hv2 <~ hash chunk;;
DO hv3 <~ hash addr;;
RET [hc; smem_get_hid sm; hv1; hv2; hv3; list_sval_get_hid lsv].
Extraction Inline hSload_hcodes.
Definition hSload (sm: smem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval): ?? sval :=
DO hv <~ hSload_hcodes sm trap chunk addr lsv;;
hC_sval {| hdata := Sload sm trap chunk addr lsv unknown_hid; hcodes := hv |}.
Lemma hSload_correct sm1 trap chunk addr lsv1:
WHEN hSload sm1 trap chunk addr lsv1 ~> hv THEN forall ctx lsv2 sm2 hid
(LR: list_sval_refines ctx lsv1 lsv2)
(MR: smem_refines ctx sm1 sm2),
sval_refines ctx hv (Sload sm2 trap chunk addr lsv2 hid).
Proof.
wlp_simplify.
rewrite <- LR, <- MR.
auto.
Qed.
Global Opaque hSload.
Local Hint Resolve hSload_correct: wlp.
Definition hSundef_hcodes :=
DO hc <~ hash undef_code;;
RET [hc].
Extraction Inline hSundef_hcodes.
Definition hSundef : ?? sval :=
DO hv <~ hSundef_hcodes;;
hC_sval {| hdata:=Sundef unknown_hid; hcodes :=hv; |}.
Lemma hSundef_correct:
WHEN hSundef ~> hv THEN forall ctx,
sval_refines ctx hv (Sundef unknown_hid).
Proof.
wlp_simplify.
Qed.
Global Opaque hSundef.
Local Hint Resolve hSundef_correct: wlp.
Definition hSnil (_: unit): ?? list_sval :=
hC_list_sval {| hdata := Snil unknown_hid; hcodes := nil |}.
Lemma hSnil_correct:
WHEN hSnil() ~> hv THEN forall ctx,
list_sval_refines ctx hv (Snil unknown_hid).
Proof.
wlp_simplify.
Qed.
Global Opaque hSnil.
Local Hint Resolve hSnil_correct: wlp.
Definition hScons (sv: sval) (lsv: list_sval): ?? list_sval :=
hC_list_sval {| hdata := Scons sv lsv unknown_hid; hcodes := [sval_get_hid sv; list_sval_get_hid lsv] |}.
Lemma hScons_correct sv1 lsv1:
WHEN hScons sv1 lsv1 ~> lsv1' THEN forall ctx sv2 lsv2
(VR: sval_refines ctx sv1 sv2)
(LR: list_sval_refines ctx lsv1 lsv2),
list_sval_refines ctx lsv1' (Scons sv2 lsv2 unknown_hid).
Proof.
wlp_simplify.
rewrite <- VR, <- LR.
auto.
Qed.
Global Opaque hScons.
Local Hint Resolve hScons_correct: wlp.
Definition hSinit (_: unit): ?? smem :=
hC_smem {| hdata := Sinit unknown_hid; hcodes := nil |}.
Lemma hSinit_correct:
WHEN hSinit() ~> hm THEN forall ctx,
smem_refines ctx hm (Sinit unknown_hid).
Proof.
wlp_simplify.
Qed.
Global Opaque hSinit.
Local Hint Resolve hSinit_correct: wlp.
Definition hSstore_hcodes (sm: smem) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) (srce: sval):=
DO hv1 <~ hash chunk;;
DO hv2 <~ hash addr;;
RET [smem_get_hid sm; hv1; hv2; list_sval_get_hid lsv; sval_get_hid srce].
Extraction Inline hSstore_hcodes.
Definition hSstore (sm: smem) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) (srce: sval): ?? smem :=
DO hv <~ hSstore_hcodes sm chunk addr lsv srce;;
hC_smem {| hdata := Sstore sm chunk addr lsv srce unknown_hid; hcodes := hv |}.
Lemma hSstore_correct sm1 chunk addr lsv1 sv1:
WHEN hSstore sm1 chunk addr lsv1 sv1 ~> sm1' THEN forall ctx lsv2 sm2 sv2
(LR: list_sval_refines ctx lsv1 lsv2)
(MR: smem_refines ctx sm1 sm2)
(VR: sval_refines ctx sv1 sv2),
smem_refines ctx sm1' (Sstore sm2 chunk addr lsv2 sv2 unknown_hid).
Proof.
wlp_simplify.
rewrite <- LR, <- MR, <- VR.
auto.
Qed.
Global Opaque hSstore.
Local Hint Resolve hSstore_correct: wlp.
Definition hris_sreg_eval ctx hris r := eval_sval ctx (ris_sreg_get hris r).
Definition hris_sreg_get (hris: ristate) r: ?? sval :=
match PTree.get r hris with
| None => if ris_input_init hris then hSinput r else hSundef
| Some sv => RET sv
end.
Coercion hris_sreg_get: ristate >-> Funclass.
Lemma hris_sreg_get_correct hris r:
WHEN hris_sreg_get hris r ~> sv THEN forall ctx (f: reg -> sval)
(RR: forall r, hris_sreg_eval ctx hris r = eval_sval ctx (f r)),
sval_refines ctx sv (f r).
Proof.
unfold hris_sreg_eval, ris_sreg_get. wlp_simplify; rewrite <- RR; rewrite H; auto;
rewrite H0, H1; simpl; auto.
Qed.
Global Opaque hris_sreg_get.
Local Hint Resolve hris_sreg_get_correct: wlp.
Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A :=
match o with
| Some x => RET x
| None => FAILWITH msg
end.
Definition hris_init: ?? ristate
:= DO hm <~ hSinit ();;
RET {| ris_smem := hm; ris_input_init := true; ok_rsval := nil; ris_sreg := PTree.empty _ |}.
Lemma ris_init_correct:
WHEN hris_init ~> hris THEN
forall ctx, ris_refines ctx hris sis_init.
Proof.
unfold hris_init, sis_init; wlp_simplify.
econstructor; simpl in *; eauto.
+ split; destruct 1; econstructor; simpl in *;
try rewrite H; try congruence; trivial.
+ destruct 1; simpl in *. unfold ris_sreg_get; simpl.
intros; rewrite PTree.gempty; eauto.
Qed.
(*
Definition hrexec f ib := hrexec_rec f ib hris_init (fun _ => Rabort).
Definition hsexec (f: function) (pc:node): ?? ristate :=
DO path <~ some_or_fail ((fn_code f)!pc) "hsexec.internal_error.1";;
DO hinit <~ init_ristate;;
DO hst <~ hsiexec_path path.(psize) f hinit;;
DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsexec.internal_error.2";;
DO ohst <~ hsiexec_inst i hst;;
match ohst with
| Some hst' => RET {| hinternal := hst'; hfinal := HSnone |}
| None => DO hsvf <~ hsexec_final i hst.(hsi_local);;
RET {| hinternal := hst; hfinal := hsvf |}
end.*)
End CanonBuilding.
|
