RTLpathSE_impl.v 60.3 KB
Newer Older
1
(** Implementation and refinement of the symbolic execution *)
2
3
4
5
6

Require Import Coqlib Maps Floats.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import RTL RTLpath.
7
Require Import Errors.
8
Require Import RTLpathSE_theory RTLpathLivegenproof.
9
Require Import Axioms RTLpathSE_simu_specs.
Léo Gourdin's avatar
Léo Gourdin committed
10
Require Import RTLpathSE_simplify.
11
12

Local Open Scope error_monad_scope.
Cyril SIX's avatar
Cyril SIX committed
13
Local Open Scope option_monad_scope.
14

15
16
17
Require Import Impure.ImpHCons.
Import Notations.
Import HConsing.
18

19
20
Local Open Scope impure.
Local Open Scope hse.
21

22
23
Import ListNotations.
Local Open Scope list_scope.
24

25
Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := RET tt. (* TO REMOVE DEBUG INFO *)
26
(*Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := DO s <~ k x;; println ("DEBUG simu_check:" +; s). (* TO INSERT DEBUG INFO *)*)
27

28
Definition DEBUG (s: pstring): ?? unit := XDEBUG tt (fun _ => RET s).
29

30
31
32
33
34
(** * Implementation of Data-structure use in Hash-consing *)

Definition hsval_get_hid (hsv: hsval): hashcode :=
  match hsv with
  | HSinput _ hid => hid
35
  | HSop _ _ hid => hid
36
37
38
39
40
41
42
43
  | HSload _ _ _ _ _ hid => hid
  end.

Definition list_hsval_get_hid (lhsv: list_hsval): hashcode :=
  match lhsv with
  | HSnil hid => hid
  | HScons _ _ hid => hid
  end.
44

45
46
47
48
49
50
51
52
53
Definition hsmem_get_hid (hsm: hsmem): hashcode :=
  match hsm with
  | HSinit hid => hid
  | HSstore _ _ _ _ _ hid => hid
  end.

Definition hsval_set_hid (hsv: hsval) (hid: hashcode): hsval :=
  match hsv with
  | HSinput r _ => HSinput r hid
54
  | HSop o lhsv _ => HSop o lhsv hid
55
56
57
58
59
60
61
62
63
64
65
66
67
68
  | HSload hsm trap chunk addr lhsv _ => HSload hsm trap chunk addr lhsv hid
  end.

Definition list_hsval_set_hid (lhsv: list_hsval) (hid: hashcode): list_hsval :=
  match lhsv with
  | HSnil _ => HSnil hid
  | HScons hsv lhsv _ => HScons hsv lhsv hid
  end.

Definition hsmem_set_hid (hsm: hsmem) (hid: hashcode): hsmem :=
  match hsm with
  | HSinit _ => HSinit hid
  | HSstore hsm chunk addr lhsv srce _ => HSstore hsm chunk addr lhsv srce hid
  end.
Cyril SIX's avatar
Cyril SIX committed
69

70

71
72
73
Lemma hsval_set_hid_correct x y ge sp rs0 m0:
  hsval_set_hid x unknown_hid = hsval_set_hid y unknown_hid ->
  seval_hsval ge sp x rs0 m0 = seval_hsval ge sp y rs0 m0.
74
Proof.
75
  destruct x, y; intro H; inversion H; subst; simpl; auto.
76
Qed.
77
Local Hint Resolve hsval_set_hid_correct: core.
78

79
80
81
Lemma list_hsval_set_hid_correct x y ge sp rs0 m0:
  list_hsval_set_hid x unknown_hid = list_hsval_set_hid y unknown_hid ->
  seval_list_hsval ge sp x rs0 m0 = seval_list_hsval ge sp y rs0 m0.
82
Proof.
83
  destruct x, y; intro H; inversion H; subst; simpl; auto.
84
Qed.
85
Local Hint Resolve list_hsval_set_hid_correct: core.
86

87
88
89
90
91
92
93
Lemma hsmem_set_hid_correct x y ge sp rs0 m0:
  hsmem_set_hid x unknown_hid = hsmem_set_hid y unknown_hid ->
  seval_hsmem ge sp x rs0 m0 = seval_hsmem ge sp y rs0 m0.
Proof.
  destruct x, y; intro H; inversion H; subst; simpl; auto.
Qed.
Local Hint Resolve hsmem_set_hid_correct: core.
94

95
(** Now, we build the hash-Cons value from a "hash_eq".
96

97
98
99
100
101
  Informal specification: 
    [hash_eq] must be consistent with the "hashed" constructors defined above.

  We expect that hashinfo values in the code of these "hashed" constructors verify:
    (hash_eq (hdata x) (hdata y) ~> true) <-> (hcodes x)=(hcodes y)
102
*)
103
104
105
106
107


Definition hsval_hash_eq (sv1 sv2: hsval): ?? bool :=
  match sv1, sv2 with
  | HSinput r1 _, HSinput r2 _ => struct_eq r1 r2 (* NB: really need a struct_eq here ? *)
108
  | HSop op1 lsv1 _, HSop op2 lsv2 _  =>
109
     DO b1 <~ phys_eq lsv1 lsv2;;
110
     if b1
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
     then struct_eq op1 op2 (* NB: really need a struct_eq here ? *)
     else RET false
  | HSload sm1 trap1 chk1 addr1 lsv1 _, HSload sm2 trap2 chk2 addr2 lsv2 _ =>
     DO b1 <~ phys_eq lsv1 lsv2;;
     DO b2 <~ phys_eq sm1 sm2;;
     DO b3 <~ struct_eq trap1 trap2;;
     DO b4 <~ struct_eq chk1 chk2;;
     if b1 && b2 && b3 && b4
     then struct_eq addr1 addr2
     else RET false
  | _,_ => RET false
  end.


Lemma and_true_split a b: a && b = true <-> a = true /\ b = true.
Cyril SIX's avatar
Cyril SIX committed
126
Proof.
127
  destruct a; simpl; intuition.
Cyril SIX's avatar
Cyril SIX committed
128
129
Qed.

130
131
132
133
134
135
136
137
Lemma hsval_hash_eq_correct x y:
  WHEN hsval_hash_eq x y ~> b THEN 
   b = true -> hsval_set_hid x unknown_hid = hsval_set_hid y unknown_hid.
Proof.
  destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence.
Qed.
Global Opaque hsval_hash_eq.
Local Hint Resolve hsval_hash_eq_correct: wlp.
Cyril SIX's avatar
Cyril SIX committed
138

139
140
141
142
143
144
145
146
147
Definition list_hsval_hash_eq (lsv1 lsv2: list_hsval): ?? bool :=
  match lsv1, lsv2 with
  | HSnil _, HSnil _ => RET true
  | HScons sv1 lsv1' _, HScons sv2 lsv2' _  =>
     DO b <~ phys_eq lsv1' lsv2';;
     if b 
     then phys_eq sv1 sv2
     else RET false
  | _,_ => RET false
Cyril SIX's avatar
Cyril SIX committed
148
149
  end.

150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
Lemma list_hsval_hash_eq_correct x y:
  WHEN list_hsval_hash_eq x y ~> b THEN 
   b = true -> list_hsval_set_hid x unknown_hid = list_hsval_set_hid y unknown_hid.
Proof.
  destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence.
Qed.
Global Opaque list_hsval_hash_eq.
Local Hint Resolve list_hsval_hash_eq_correct: wlp.

Definition hsmem_hash_eq (sm1 sm2: hsmem): ?? bool :=
  match sm1, sm2 with
  | HSinit _, HSinit _ => RET true
  | HSstore sm1 chk1 addr1 lsv1 sv1 _, HSstore sm2 chk2 addr2 lsv2 sv2 _ =>
     DO b1 <~ phys_eq lsv1 lsv2;;
     DO b2 <~ phys_eq sm1 sm2;;
     DO b3 <~ phys_eq sv1 sv2;;
     DO b4 <~ struct_eq chk1 chk2;;
     if b1 && b2 && b3 && b4
     then struct_eq addr1 addr2
     else RET false
  | _,_ => RET false
Cyril SIX's avatar
Cyril SIX committed
171
172
  end.

173
174
175
Lemma hsmem_hash_eq_correct x y:
  WHEN hsmem_hash_eq x y ~> b THEN 
   b = true -> hsmem_set_hid x unknown_hid = hsmem_set_hid y unknown_hid.
Cyril SIX's avatar
Cyril SIX committed
176
Proof.
177
  destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence.
Cyril SIX's avatar
Cyril SIX committed
178
Qed.
179
180
Global Opaque hsmem_hash_eq.
Local Hint Resolve hsmem_hash_eq_correct: wlp.
Cyril SIX's avatar
Cyril SIX committed
181
182


183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
Definition hSVAL: hashP hsval := {| hash_eq := hsval_hash_eq; get_hid:=hsval_get_hid; set_hid:=hsval_set_hid |}. 
Definition hLSVAL: hashP list_hsval := {| hash_eq := list_hsval_hash_eq; get_hid:= list_hsval_get_hid; set_hid:= list_hsval_set_hid |}.
Definition hSMEM: hashP hsmem := {| hash_eq := hsmem_hash_eq; get_hid:= hsmem_get_hid; set_hid:= hsmem_set_hid |}.

Program Definition mk_hash_params: Dict.hash_params hsval :=
 {|
    Dict.test_eq := phys_eq;
    Dict.hashing := fun (ht: hsval) => RET (hsval_get_hid ht);
    Dict.log := fun hv =>
         DO hv_name <~ string_of_hashcode (hsval_get_hid hv);;
         println ("unexpected undef behavior of hashcode:" +; (CamlStr hv_name)) |}.
Obligation 1.
  wlp_simplify.
Qed.

(** ** various auxiliary (trivial lemmas) *)
Lemma hsilocal_refines_sreg ge sp rs0 m0 hst st:
  hsilocal_refines ge sp rs0 m0 hst st -> hsok_local ge sp rs0 m0 hst -> forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0.
Cyril SIX's avatar
Cyril SIX committed
201
Proof.
202
  unfold hsilocal_refines; intuition.
Cyril SIX's avatar
Cyril SIX committed
203
Qed.
204
Local Hint Resolve hsilocal_refines_sreg: core.
Cyril SIX's avatar
Cyril SIX committed
205

206
207
Lemma hsilocal_refines_valid_pointer ge sp rs0 m0 hst st:
  hsilocal_refines ge sp rs0 m0 hst st -> forall m b ofs, seval_smem ge sp st.(si_smem) rs0 m0 = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs.
Cyril SIX's avatar
Cyril SIX committed
208
Proof.
209
  unfold hsilocal_refines; intuition.
Cyril SIX's avatar
Cyril SIX committed
210
Qed.
211
Local Hint Resolve hsilocal_refines_valid_pointer: core.
Cyril SIX's avatar
Cyril SIX committed
212

213
214
215
216
217
218
Lemma hsilocal_refines_smem_refines ge sp rs0 m0 hst st:
  hsilocal_refines ge sp rs0 m0 hst st -> hsok_local ge sp rs0 m0 hst -> smem_refines ge sp rs0 m0 (hsi_smem hst) (st.(si_smem)).
Proof.
  unfold hsilocal_refines; intuition.
Qed.
Local Hint Resolve hsilocal_refines_smem_refines: core.
Cyril SIX's avatar
Cyril SIX committed
219

220
221
Lemma hsistate_refines_dyn_exits ge sp rs0 m0 hst st:
  hsistate_refines_dyn ge sp rs0 m0 hst st -> hsiexits_refines_dyn ge sp rs0 m0 (hsi_exits hst) (si_exits st).
Cyril SIX's avatar
Cyril SIX committed
222
Proof.
223
  unfold hsistate_refines_dyn; intuition.
Cyril SIX's avatar
Cyril SIX committed
224
Qed.
225
Local Hint Resolve hsistate_refines_dyn_exits: core.
Cyril SIX's avatar
Cyril SIX committed
226

227
228
229
230
231
232
Lemma hsistate_refines_dyn_local ge sp rs0 m0 hst st:
  hsistate_refines_dyn ge sp rs0 m0 hst st -> hsilocal_refines ge sp rs0 m0 (hsi_local hst) (si_local st).
Proof.
  unfold hsistate_refines_dyn; intuition.
Qed.
Local Hint Resolve hsistate_refines_dyn_local: core.
Cyril SIX's avatar
Cyril SIX committed
233

234
235
Lemma hsistate_refines_dyn_nested ge sp rs0 m0 hst st:
  hsistate_refines_dyn ge sp rs0 m0 hst st -> nested_sok ge sp rs0 m0 (si_local st) (si_exits st).
Cyril SIX's avatar
Cyril SIX committed
236
Proof.
237
238
239
  unfold hsistate_refines_dyn; intuition.
Qed.
Local Hint Resolve hsistate_refines_dyn_nested: core.
Cyril SIX's avatar
Cyril SIX committed
240

241
242
(** * Implementation of symbolic execution *)
Section CanonBuilding.
Cyril SIX's avatar
Cyril SIX committed
243

244
Variable hC_hsval: hashinfo hsval -> ?? hsval.
245

246
247
248
Hypothesis hC_hsval_correct: forall hs,
  WHEN hC_hsval hs ~> hs' THEN forall ge sp rs0 m0,
    seval_hsval ge sp (hdata hs) rs0 m0 = seval_hsval ge sp hs' rs0 m0.
249

250
251
252
253
Variable hC_list_hsval: hashinfo list_hsval -> ?? list_hsval.
Hypothesis hC_list_hsval_correct: forall lh,
  WHEN hC_list_hsval lh ~> lh' THEN forall ge sp rs0 m0,
    seval_list_hsval ge sp (hdata lh) rs0 m0 = seval_list_hsval ge sp lh' rs0 m0.
Cyril SIX's avatar
Cyril SIX committed
254

255
256
257
258
Variable hC_hsmem: hashinfo hsmem -> ?? hsmem.
Hypothesis hC_hsmem_correct: forall hm,
  WHEN hC_hsmem hm ~> hm' THEN forall ge sp rs0 m0,
    seval_hsmem ge sp (hdata hm) rs0 m0 = seval_hsmem ge sp hm' rs0 m0.
Cyril SIX's avatar
Cyril SIX committed
259

260
(* First, we wrap constructors for hashed values !*)
Cyril SIX's avatar
Cyril SIX committed
261

262
263
264
Definition reg_hcode := 1.
Definition op_hcode := 2.
Definition load_hcode := 3.
Cyril SIX's avatar
Cyril SIX committed
265

266
267
268
269
270
Definition hSinput_hcodes (r: reg) :=
   DO hc <~ hash reg_hcode;;
   DO hv <~ hash r;;
   RET [hc;hv].
Extraction Inline hSinput_hcodes.
Cyril SIX's avatar
Cyril SIX committed
271

272
273
274
275
276
277
278
Definition hSinput (r:reg): ?? hsval :=
   DO hv <~ hSinput_hcodes r;;
   hC_hsval {| hdata:=HSinput r unknown_hid; hcodes :=hv; |}.

Lemma hSinput_correct r:
  WHEN hSinput r ~> hv THEN forall ge sp rs0 m0,
    sval_refines ge sp rs0 m0 hv (Sinput r).
Cyril SIX's avatar
Cyril SIX committed
279
Proof.
280
281
282
283
  wlp_simplify.
Qed.
Global Opaque hSinput.
Local Hint Resolve hSinput_correct: wlp.
Cyril SIX's avatar
Cyril SIX committed
284

285
Definition hSop_hcodes (op:operation) (lhsv: list_hsval) :=
286
287
   DO hc <~ hash op_hcode;;
   DO hv <~ hash op;;
288
   RET [hc;hv;list_hsval_get_hid lhsv].
289
Extraction Inline hSop_hcodes.
Cyril SIX's avatar
Cyril SIX committed
290

291
292
293
Definition hSop (op:operation) (lhsv: list_hsval): ?? hsval :=
   DO hv <~ hSop_hcodes op lhsv;;
   hC_hsval {| hdata:=HSop op lhsv unknown_hid; hcodes :=hv |}.
294

Sylvain Boulmé's avatar
Sylvain Boulmé committed
295
296
297
298
299
300
301
302
303
Lemma hSop_fSop_correct op lhsv:
  WHEN hSop op lhsv ~> hv THEN forall ge sp rs0 m0,
    seval_hsval ge sp hv rs0 m0 = seval_hsval ge sp (fSop op lhsv) rs0 m0.
Proof.
  wlp_simplify.
Qed.
Global Opaque hSop.
Local Hint Resolve hSop_fSop_correct: wlp_raw.

304
305
306
307
308
309
Lemma hSop_correct op lhsv:
  WHEN hSop op lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm m
   (MEM: seval_smem ge sp sm rs0 m0 = Some m)
   (MVALID: forall b ofs, Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
   (LR: list_sval_refines ge sp rs0 m0 lhsv lsv),
   sval_refines ge sp rs0 m0 hv (Sop op lsv sm).
Cyril SIX's avatar
Cyril SIX committed
310
Proof.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
311
312
313
314
  generalize fSop_correct; simpl.
  intros X.
  wlp_xsimplify ltac:(intuition eauto with wlp wlp_raw).
  erewrite H, X; eauto.
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
Qed.
Local Hint Resolve hSop_correct: wlp.

Definition hSload_hcodes (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval):=
   DO hc <~ hash load_hcode;;
   DO hv1 <~ hash trap;;
   DO hv2 <~ hash chunk;;
   DO hv3 <~ hash addr;;
   RET [hc; hsmem_get_hid hsm; hv1; hv2; hv3; list_hsval_get_hid lhsv].
Extraction Inline hSload_hcodes.

Definition hSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval): ?? hsval :=
   DO hv <~ hSload_hcodes hsm trap chunk addr lhsv;;
   hC_hsval {| hdata := HSload hsm trap chunk addr lhsv unknown_hid; hcodes := hv |}.

Lemma hSload_correct hsm trap chunk addr lhsv:
  WHEN hSload hsm trap chunk addr lhsv ~> hv THEN forall ge sp rs0 m0 lsv sm
    (LR: list_sval_refines ge sp rs0 m0 lhsv lsv)
    (MR: smem_refines ge sp rs0 m0 hsm sm),
    sval_refines ge sp rs0 m0 hv (Sload sm trap chunk addr lsv).
Proof.
  wlp_simplify.
  rewrite <- LR, <- MR.
  auto.
Qed.
Global Opaque hSload.
Local Hint Resolve hSload_correct: wlp.
Cyril SIX's avatar
Cyril SIX committed
342

343
344
Definition hSnil (_: unit): ?? list_hsval :=
   hC_list_hsval {| hdata := HSnil unknown_hid; hcodes := nil |}.
345

346
347
348
Lemma hSnil_correct:
  WHEN hSnil() ~> hv THEN forall ge sp rs0 m0,
    list_sval_refines ge sp rs0 m0 hv Snil.
349
Proof.
350
351
352
353
  wlp_simplify.
Qed.
Global Opaque hSnil.
Local Hint Resolve hSnil_correct: wlp.
354

355
356
357
358
359
360
361
362
Definition hScons (hsv: hsval) (lhsv: list_hsval): ?? list_hsval :=
   hC_list_hsval {| hdata := HScons hsv lhsv unknown_hid; hcodes := [hsval_get_hid hsv; list_hsval_get_hid lhsv] |}.

Lemma hScons_correct hsv lhsv:
  WHEN hScons hsv lhsv ~> lhsv' THEN forall ge sp rs0 m0 sv lsv
    (VR: sval_refines ge sp rs0 m0 hsv sv)
    (LR: list_sval_refines ge sp rs0 m0 lhsv lsv),
    list_sval_refines ge sp rs0 m0 lhsv' (Scons sv lsv).
Cyril SIX's avatar
Cyril SIX committed
363
Proof.
364
365
366
  wlp_simplify.
  rewrite <- VR, <- LR.
  auto.
367
Qed.
368
369
Global Opaque hScons.
Local Hint Resolve hScons_correct: wlp.
370

371
372
373
374
375
376
Definition hSinit (_: unit): ?? hsmem :=
   hC_hsmem {| hdata := HSinit unknown_hid; hcodes := nil |}.

Lemma hSinit_correct:
  WHEN hSinit() ~> hm THEN forall ge sp rs0 m0,
    smem_refines ge sp rs0 m0 hm Sinit.
377
Proof.
378
  wlp_simplify.
379
Qed.
380
381
Global Opaque hSinit.
Local Hint Resolve hSinit_correct: wlp.
Cyril SIX's avatar
Cyril SIX committed
382

383
384
385
386
387
Definition hSstore_hcodes (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval):=
   DO hv1 <~ hash chunk;;
   DO hv2 <~ hash addr;;
   RET [hsmem_get_hid hsm; hv1; hv2; list_hsval_get_hid lhsv; hsval_get_hid srce].
Extraction Inline hSstore_hcodes.
Cyril SIX's avatar
Cyril SIX committed
388

389
390
391
Definition hSstore (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval): ?? hsmem :=
   DO hv <~ hSstore_hcodes hsm chunk addr lhsv srce;;
   hC_hsmem {| hdata := HSstore hsm chunk addr lhsv srce unknown_hid; hcodes := hv |}.
Cyril SIX's avatar
Cyril SIX committed
392

393
394
395
396
397
398
399
400
401
402
403
404
405
Lemma hSstore_correct hsm chunk addr lhsv hsv:
  WHEN hSstore hsm chunk addr lhsv hsv ~> hsm' THEN forall ge sp rs0 m0 lsv sm sv
    (LR: list_sval_refines ge sp rs0 m0 lhsv lsv)
    (MR: smem_refines ge sp rs0 m0 hsm sm)
    (VR: sval_refines ge sp rs0 m0 hsv sv),
    smem_refines ge sp rs0 m0 hsm' (Sstore sm chunk addr lsv sv).
Proof.
  wlp_simplify.
  rewrite <- LR, <- MR, <- VR.
  auto.
Qed.
Global Opaque hSstore.
Local Hint Resolve hSstore_correct: wlp.
406

407
408
409
410
411
Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval :=
   match PTree.get r hst with 
   | None => hSinput r
   | Some sv => RET sv
   end.
Cyril SIX's avatar
Cyril SIX committed
412

413
414
415
416
417
418
419
420
421
Lemma hsi_sreg_get_correct hst r:
  WHEN hsi_sreg_get hst r ~> hsv THEN forall ge sp rs0 m0 (f: reg -> sval)
    (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
    sval_refines ge sp rs0 m0 hsv (f r).
Proof.
  unfold hsi_sreg_eval, hsi_sreg_proj; wlp_simplify; rewrite <- RR; try_simplify_someHyps.
Qed.
Global Opaque hsi_sreg_get.
Local Hint Resolve hsi_sreg_get_correct: wlp.
Cyril SIX's avatar
Cyril SIX committed
422

423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
Fixpoint hlist_args (hst: PTree.t hsval) (l: list reg): ?? list_hsval :=
  match l with
  | nil => hSnil()
  | r::l =>
    DO v <~ hsi_sreg_get hst r;;
    DO lhsv <~ hlist_args hst l;;
    hScons v lhsv
  end.

Lemma hlist_args_correct hst l:
  WHEN hlist_args hst l ~> lhsv THEN forall ge sp rs0 m0 (f: reg -> sval)
    (RR: forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (f r) rs0 m0),
    list_sval_refines ge sp rs0 m0 lhsv (list_sval_inj (List.map f l)).
Proof.
  induction l; wlp_simplify.
Qed.
Global Opaque hlist_args.
Local Hint Resolve hlist_args_correct: wlp.
441

Sylvain Boulmé's avatar
Sylvain Boulmé committed
442
443
(** Convert a "fake" hash-consed term into a "real" hash-consed term *)

444
445
446
447
448
449
450
451
452
453
454
455
Fixpoint fsval_proj hsv: ?? hsval :=
  match hsv with
  | HSinput r hc => 
    DO b <~ phys_eq hc unknown_hid;;
    if b 
    then hSinput r (* was not yet really hash-consed *)
    else RET hsv (* already hash-consed *)
  | HSop op hl hc => 
    DO b <~ phys_eq hc unknown_hid;;
    if b 
    then (* was not yet really hash-consed *) 
      DO hl' <~ fsval_list_proj hl;;
Léo Gourdin's avatar
Léo Gourdin committed
456
      hSop op hl'
457
458
459
    else RET hsv (* already hash-consed *)
  | HSload hm t chk addr hl _ => RET hsv (* FIXME ? *)
  end
Sylvain Boulmé's avatar
Sylvain Boulmé committed
460
461
with fsval_list_proj hsl: ?? list_hsval :=
  match hsl with
462
463
464
465
  | HSnil hc => 
    DO b <~ phys_eq hc unknown_hid;;
    if b 
    then hSnil() (* was not yet really hash-consed *)
Sylvain Boulmé's avatar
Sylvain Boulmé committed
466
    else RET hsl (* already hash-consed *)
467
468
469
470
471
472
473
  | HScons hv hl hc => 
    DO b <~ phys_eq hc unknown_hid;;
    if b 
    then (* was not yet really hash-consed *)
      DO hv' <~ fsval_proj hv;;
      DO hl' <~ fsval_list_proj hl;;
      hScons hv' hl' 
Sylvain Boulmé's avatar
Sylvain Boulmé committed
474
    else RET hsl (* already hash-consed *)
475
476
477
478
479
  end.

Lemma fsval_proj_correct hsv:
  WHEN fsval_proj hsv ~> hsv' THEN forall ge sp rs0 m0,
  seval_hsval ge sp hsv rs0 m0 = seval_hsval ge sp hsv' rs0 m0.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
480
481
482
483
484
485
486
487
488
489
Proof.
 induction hsv using hsval_mut 
 with (P0 := fun lhsv => 
       WHEN fsval_list_proj lhsv ~> lhsv' THEN forall ge sp rs0 m0,
         seval_list_hsval ge sp lhsv rs0 m0 = seval_list_hsval ge sp lhsv' rs0 m0)
       (P1 := fun sm => True); try (wlp_simplify; tauto).
 - wlp_xsimplify ltac:(intuition eauto with wlp_raw wlp).
   rewrite H, H0; auto.
 - wlp_simplify; erewrite H0, H1; eauto.
Qed.
490
491
492
Global Opaque fsval_proj.
Local Hint Resolve fsval_proj_correct: wlp.

Sylvain Boulmé's avatar
Sylvain Boulmé committed
493
494
495
Lemma fsval_list_proj_correct lhsv:
  WHEN fsval_list_proj lhsv ~> lhsv' THEN forall ge sp rs0 m0,
  seval_list_hsval ge sp lhsv rs0 m0 = seval_list_hsval ge sp lhsv' rs0 m0.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
496
497
498
499
Proof.
  induction lhsv; wlp_simplify.
  erewrite H0, H1; eauto.
Qed.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
500
501
502
503
Global Opaque fsval_list_proj.
Local Hint Resolve fsval_list_proj_correct: wlp.


504
(** ** Assignment of memory *)
505
506
Definition hslocal_set_smem (hst:hsistate_local) hm :=
  {| hsi_smem := hm;
Cyril SIX's avatar
Cyril SIX committed
507
508
     hsi_ok_lsval := hsi_ok_lsval hst;
     hsi_sreg:= hsi_sreg hst
509
510
  |}.

511
Lemma sok_local_set_mem ge sp rs0 m0 st sm:
512
  sok_local ge sp rs0 m0 (slocal_set_smem st sm)
513
  <-> (sok_local ge sp rs0 m0 st /\ seval_smem ge sp sm rs0 m0 <> None).
Sylvain Boulmé's avatar
Sylvain Boulmé committed
514
515
516
Proof.
  unfold slocal_set_smem, sok_local; simpl; intuition (subst; eauto).
Qed.
517

518
519
520
521
Lemma hsok_local_set_mem ge sp rs0 m0 hst hsm:
  (seval_hsmem ge sp (hsi_smem hst) rs0 m0 = None -> seval_hsmem ge sp hsm rs0 m0 = None) ->
  hsok_local ge sp rs0 m0 (hslocal_set_smem hst hsm)
  <-> (hsok_local ge sp rs0 m0 hst /\ seval_hsmem ge sp hsm rs0 m0 <> None).
522
Proof.
523
  unfold hslocal_set_smem, hsok_local; simpl; intuition.
524
525
Qed.

Sylvain Boulmé's avatar
Sylvain Boulmé committed
526
Lemma hslocal_set_mem_correct ge sp rs0 m0 hst st hsm sm:
527
  (seval_hsmem ge sp (hsi_smem hst) rs0 m0 = None -> seval_hsmem ge sp hsm rs0 m0 = None) ->
528
  (forall m b ofs, seval_smem ge sp sm rs0 m0 = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) ->
Cyril SIX's avatar
Cyril SIX committed
529
  hsilocal_refines ge sp rs0 m0 hst st ->
530
  (hsok_local ge sp rs0 m0 hst -> smem_refines ge sp rs0 m0 hsm sm) ->
Cyril SIX's avatar
Cyril SIX committed
531
  hsilocal_refines ge sp rs0 m0 (hslocal_set_smem hst hsm) (slocal_set_smem st sm).
Sylvain Boulmé's avatar
Sylvain Boulmé committed
532
Proof.
533
534
  intros PRESERV SMVALID (OKEQ & SMEMEQ' & REGEQ & MVALID) SMEMEQ.
  split; rewrite! hsok_local_set_mem; simpl; eauto; try tauto.
535
536
  rewrite sok_local_set_mem.
  intuition congruence.
537
Qed.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
538

539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
Definition hslocal_store (hst: hsistate_local) chunk addr args src: ?? hsistate_local :=
   let pt := hst.(hsi_sreg) in
   DO hargs <~ hlist_args pt args;;
   DO hsrc <~ hsi_sreg_get pt src;;
   DO hm <~ hSstore hst chunk addr hargs hsrc;;
   RET (hslocal_set_smem hst hm).

Lemma hslocal_store_correct hst chunk addr args src:
  WHEN hslocal_store hst chunk addr args src ~> hst' THEN forall ge sp rs0 m0 st
    (REF: hsilocal_refines ge sp rs0 m0 hst st),
    hsilocal_refines ge sp rs0 m0 hst' (slocal_store st chunk addr args src).
Proof.
  wlp_simplify.
  eapply hslocal_set_mem_correct; simpl; eauto.
  + intros X; erewrite H1; eauto.
    rewrite X. simplify_SOME z.
  + unfold hsilocal_refines in *; 
    simplify_SOME z; intuition. 
    erewrite <- Mem.storev_preserv_valid; [| eauto].
    eauto.
  + unfold hsilocal_refines in *; intuition eauto.
Qed.
Global Opaque hslocal_store.
Local Hint Resolve hslocal_store_correct: wlp.

564
565
566
567
568
(** ** Assignment of local state *)

Definition hsist_set_local (hst: hsistate) (pc: node) (hnxt: hsistate_local): hsistate :=
   {| hsi_pc := pc; hsi_exits := hst.(hsi_exits); hsi_local:= hnxt |}.

569
570
571
572
573
574
575
576
577
Lemma hsist_set_local_correct_stat hst st pc hnxt nxt:
  hsistate_refines_stat hst st ->
  hsistate_refines_stat (hsist_set_local hst pc hnxt) (sist_set_local st pc nxt).
Proof.
  unfold hsistate_refines_stat; simpl; intuition.
Qed.

Lemma hsist_set_local_correct_dyn ge sp rs0 m0 hst st pc hnxt nxt:
  hsistate_refines_dyn ge sp rs0 m0 hst st ->
Cyril SIX's avatar
Cyril SIX committed
578
  hsilocal_refines ge sp rs0 m0 hnxt nxt ->
579
  (sok_local ge sp rs0 m0 nxt -> sok_local ge sp rs0 m0 (si_local st)) ->
580
  hsistate_refines_dyn ge sp rs0 m0 (hsist_set_local hst pc hnxt) (sist_set_local st pc nxt).
581
Proof.
582
583
584
  unfold hsistate_refines_dyn; simpl.
  intros (EREF & LREF & NESTED) LREFN SOK; intuition.
  destruct NESTED as [|st0 se lse TOP NEST]; econstructor; simpl; auto.
585
586
587
588
Qed.

(** ** Assignment of registers *)

589
(** locally new symbolic values during symbolic execution *)
Sylvain Boulmé's avatar
Sylvain Boulmé committed
590
Inductive root_sval: Type :=
591
592
| Rop (op: operation)
| Rload (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing)
Sylvain Boulmé's avatar
Sylvain Boulmé committed
593
594
.

595
596
597
Definition root_apply (rsv: root_sval) (lr: list reg) (st: sistate_local): sval :=
  let lsv := list_sval_inj (List.map (si_sreg st) lr) in
  let sm := si_smem st in
Sylvain Boulmé's avatar
Sylvain Boulmé committed
598
  match rsv with
599
600
  | Rop op => Sop op lsv sm
  | Rload trap chunk addr => Sload sm trap chunk addr lsv
601
  end.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
602
Coercion root_apply: root_sval >-> Funclass.
603

604
605
Definition root_happly (rsv: root_sval) (lr: list reg) (hst: hsistate_local) : ?? hsval :=
  DO lhsv <~ hlist_args hst lr;;
606
  match rsv with
607
  | Rop op => hSop op lhsv
608
  | Rload trap chunk addr => hSload hst trap chunk addr lhsv
609
610
  end.

611
612
613
614
615
Lemma root_happly_correct (rsv: root_sval) lr hst:
  WHEN root_happly rsv lr hst ~> hv' THEN forall ge sp rs0 m0 st
    (REF:hsilocal_refines ge sp rs0 m0 hst st)
    (OK:hsok_local ge sp rs0 m0 hst),
    sval_refines ge sp rs0 m0 hv' (rsv lr st).
616
Proof.
617
618
619
620
621
   unfold hsilocal_refines, root_apply, root_happly; destruct rsv; wlp_simplify.
   unfold sok_local in *.
   generalize (H0 ge sp rs0 m0 (list_sval_inj (map (si_sreg st) lr)) (si_smem st)); clear H0.
   destruct (seval_smem ge sp (si_smem st) rs0 m0) as [m|] eqn:X; eauto.
   intuition congruence.
622
Qed.
623
624
Global Opaque root_happly.
Hint Resolve root_happly_correct: wlp.
625

Sylvain Boulmé's avatar
Sylvain Boulmé committed
626
627
628
Local Open Scope lazy_bool_scope.

(* NB: return [false] if the rsv cannot fail *)
629
Definition may_trap (rsv: root_sval) (lr: list reg): bool :=
Sylvain Boulmé's avatar
Sylvain Boulmé committed
630
  match rsv with 
631
  | Rop op => is_trapping_op op ||| negb (Nat.eqb (length lr) (args_of_operation op))  (* cf. lemma is_trapping_op_sound *)
Sylvain Boulmé's avatar
Sylvain Boulmé committed
632
633
  | Rload TRAP _ _  => true
  | _ => false
634
635
636
637
638
639
640
641
  end.

Lemma lazy_orb_negb_false (b1 b2:bool):
  (b1 ||| negb b2) = false <-> (b1 = false /\ b2 = true).
Proof.
  unfold negb; explore; simpl; intuition (try congruence).
Qed.

642
643
Lemma seval_list_sval_length ge sp rs0 m0 (f: reg -> sval) (l:list reg):
  forall l', seval_list_sval ge sp (list_sval_inj (List.map f l)) rs0 m0 = Some l' ->
Cyril SIX's avatar
Cyril SIX committed
644
645
646
647
648
649
650
651
652
  Datatypes.length l = Datatypes.length l'.
Proof.
  induction l.
  - simpl. intros. inv H. reflexivity.
  - simpl. intros. destruct (seval_sval _ _ _ _ _); [|discriminate].
    destruct (seval_list_sval _ _ _ _ _) eqn:SLS; [|discriminate]. inv H. simpl.
    erewrite IHl; eauto.
Qed.

653
654
655
656
657
Lemma may_trap_correct (ge: RTL.genv) (sp:val) (rsv: root_sval) (rs0: regset) (m0: mem) (lr: list reg) st:
  may_trap rsv lr = false -> 
  seval_list_sval ge sp (list_sval_inj (List.map (si_sreg st) lr)) rs0 m0 <> None ->
  seval_smem ge sp (si_smem st) rs0 m0 <> None ->
  seval_sval ge sp (rsv lr st) rs0 m0 <> None.
658
Proof.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
659
660
  destruct rsv; simpl; try congruence.
  - rewrite lazy_orb_negb_false. intros (TRAP1 & TRAP2) OK1 OK2.
661
662
    explore; try congruence.
    eapply is_trapping_op_sound; eauto.
Cyril SIX's avatar
Cyril SIX committed
663
664
665
    erewrite <- seval_list_sval_length; eauto.
    apply Nat.eqb_eq in TRAP2.
    assumption.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
666
  - intros X OK1 OK2.
667
    explore; try congruence.
Cyril SIX's avatar
Cyril SIX committed
668
Qed.
669

670
671
(** simplify a symbolic value before assignment to a register *)
Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval :=
Sylvain Boulmé's avatar
Sylvain Boulmé committed
672
  match rsv with
673
  | Rop op =>
674
675
676
     match is_move_operation op lr with
     | Some arg => hsi_sreg_get hst arg (* optimization of Omove *)
     | None =>
677
678
679
680
681
682
       match target_op_simplify op lr hst with
       | Some fhv => fsval_proj fhv
       | None =>
         DO lhsv <~ hlist_args hst lr;;
         hSop op lhsv
       end
683
     end
684
685
686
  | Rload _ chunk addr => 
       DO lhsv <~ hlist_args hst lr;;
       hSload hst NOTRAP chunk addr lhsv
687
  end.
688

689
690
691
692
693
694
Lemma simplify_correct rsv lr hst:
  WHEN simplify rsv lr hst ~> hv THEN forall ge sp rs0 m0 st
    (REF: hsilocal_refines ge sp rs0 m0 hst st)
    (OK0: hsok_local ge sp rs0 m0 hst)
    (OK1: seval_sval ge sp (rsv lr st) rs0 m0 <> None),
    sval_refines ge sp rs0 m0 hv (rsv lr st).
695
Proof.
696
  destruct rsv; simpl; auto.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
697
  - (* Rop *)
698
699
    destruct (is_move_operation _ _) eqn: Hmove.
    { wlp_simplify; exploit is_move_operation_correct; eauto.
700
      intros (Hop & Hlsv); subst; simpl in *.
701
702
703
      simplify_SOME z.
      * erewrite H; eauto.
      * try_simplify_someHyps; congruence.
704
705
706
707
708
709
710
711
712
      * congruence. }
    destruct (target_op_simplify _ _ _) eqn: Htarget_op_simp; wlp_simplify.
    { destruct (seval_list_sval _ _ _) eqn: OKlist; try congruence.
      destruct (seval_smem _ _ _ _ _) eqn: OKmem; try congruence.
      rewrite <- H; exploit target_op_simplify_correct; eauto. }
    clear Htarget_op_simp.
    generalize (H0 ge sp rs0 m0 (list_sval_inj (map (si_sreg st) lr)) (si_smem st)); clear H0.
    destruct (seval_smem ge sp (si_smem st) rs0 m0) as [m|] eqn:X; eauto.
    intro H0; clear H0; simplify_SOME z; congruence. (* absurd case *)
Sylvain Boulmé's avatar
Sylvain Boulmé committed
713
  - (* Rload *)
714
715
716
717
    destruct trap; wlp_simplify.
    erewrite H0; eauto.
    erewrite H; eauto.
    erewrite hsilocal_refines_smem_refines; eauto.
718
719
720
    destruct (seval_list_sval _ _ _ _) as [args|] eqn: Hargs; try congruence.
    destruct (eval_addressing _ _ _ _) as [a|] eqn: Ha; try congruence.
    destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
721
    destruct (Mem.loadv _ _ _); try congruence.
Léo Gourdin's avatar
Léo Gourdin committed
722
Qed.
723
724
Global Opaque simplify.
Local Hint Resolve simplify_correct: wlp.
725

726
727
728
Definition red_PTree_set (r: reg) (hsv: hsval) (hst: PTree.t hsval): PTree.t hsval :=
  match hsv with
  | HSinput r' _ =>
729
730
     if Pos.eq_dec r r' 
     then PTree.remove r' hst
731
732
     else PTree.set r hsv hst
  | _ => PTree.set r hsv hst
733
734
  end.

735
736
Lemma red_PTree_set_correct (r r0:reg) hsv hst ge sp rs0 m0:
  hsi_sreg_eval ge sp (red_PTree_set r hsv hst) r0 rs0 m0 = hsi_sreg_eval ge sp (PTree.set r hsv hst) r0 rs0 m0.
737
Proof.
738
  destruct hsv; simpl; auto.
739
  destruct (Pos.eq_dec r r1); auto.
740
  subst; unfold hsi_sreg_eval, hsi_sreg_proj.
741
742
743
  destruct (Pos.eq_dec r0 r1); auto.
  - subst; rewrite PTree.grs, PTree.gss; simpl; auto.
  - rewrite PTree.gro, PTree.gso; simpl; auto.
744
745
Qed.

746
747
748
749
750
751
752
753
754
755
756
757
758
Lemma red_PTree_set_refines (r r0:reg) hsv hst sv st ge sp rs0 m0:
 hsilocal_refines ge sp rs0 m0 hst st ->
 sval_refines ge sp rs0 m0 hsv sv ->
 hsok_local ge sp rs0 m0 hst ->
 hsi_sreg_eval ge sp (red_PTree_set r hsv hst) r0 rs0 m0 = seval_sval ge sp (if Pos.eq_dec r r0 then sv else si_sreg st r0) rs0 m0.
Proof.
  intros; rewrite red_PTree_set_correct.
  exploit hsilocal_refines_sreg; eauto.
  unfold hsi_sreg_eval, hsi_sreg_proj.
  destruct (Pos.eq_dec r r0); auto.
  - subst. rewrite PTree.gss; simpl; auto.
  - rewrite PTree.gso; simpl; eauto.
Qed.
759

760
761
762
Lemma sok_local_set_sreg (rsv:root_sval) ge sp rs0 m0 st r lr:
  sok_local ge sp rs0 m0 (slocal_set_sreg st r (rsv lr st))
  <-> (sok_local ge sp rs0 m0 st /\ seval_sval ge sp (rsv lr st) rs0 m0 <> None).
763
Proof.
764
  unfold slocal_set_sreg, sok_local; simpl; split.
765
766
767
768
769
770
771
772
773
  + intros ((SVAL0 & PRE) & SMEM & SVAL).
    repeat (split; try tauto).
    - intros r0; generalize (SVAL r0); clear SVAL; destruct (Pos.eq_dec r r0); try congruence.
    - generalize (SVAL r); clear SVAL; destruct (Pos.eq_dec r r); try congruence.
  + intros ((PRE & SMEM & SVAL0) & SVAL).
    repeat (split; try tauto; eauto).
    intros r0;  destruct (Pos.eq_dec r r0); try congruence.
Qed.

774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
Definition hslocal_set_sreg (hst: hsistate_local) (r: reg) (rsv: root_sval) (lr: list reg): ?? hsistate_local :=
  DO ok_lhsv <~
   (if may_trap rsv lr
    then DO hv <~ root_happly rsv lr hst;;
         XDEBUG hv (fun hv => DO hv_name <~ string_of_hashcode (hsval_get_hid hv);; RET ("-- insert undef behavior of hashcode:" +; (CamlStr hv_name))%string);;
         RET (hv::(hsi_ok_lsval hst))
    else RET (hsi_ok_lsval hst));;
  DO simp <~ simplify rsv lr hst;;
  RET {| hsi_smem := hst;
         hsi_ok_lsval := ok_lhsv;
         hsi_sreg := red_PTree_set r simp (hsi_sreg hst) |}.

Lemma hslocal_set_sreg_correct hst r rsv lr:
  WHEN hslocal_set_sreg hst r rsv lr ~> hst' THEN forall ge sp rs0 m0 st
    (REF: hsilocal_refines ge sp rs0 m0 hst st),
    hsilocal_refines ge sp rs0 m0 hst' (slocal_set_sreg st r (rsv lr st)).
790
Proof.
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
  wlp_simplify.
  + (* may_trap ~> true *)
    assert (X: sok_local ge sp rs0 m0 (slocal_set_sreg st r (rsv lr st)) <->
               hsok_local ge sp rs0 m0 {| hsi_smem := hst; hsi_ok_lsval := exta :: hsi_ok_lsval hst; hsi_sreg := red_PTree_set r exta0 hst |}).
    { rewrite sok_local_set_sreg; generalize REF.
      intros (OKeq & MEM & REG & MVALID); rewrite OKeq; clear OKeq.
      unfold hsok_local; simpl; intuition (subst; eauto);
      erewrite <- H0 in *; eauto; unfold hsok_local; simpl; intuition eauto.
    }
    unfold hsilocal_refines; simpl; split; auto.
    rewrite <- X, sok_local_set_sreg. intuition eauto.
    - destruct REF; intuition eauto.
    - generalize REF; intros (OKEQ & _). rewrite OKEQ in * |-; erewrite red_PTree_set_refines; eauto.
  + (* may_trap ~> false *)
    assert (X: sok_local ge sp rs0 m0 (slocal_set_sreg st r (rsv lr st)) <->
               hsok_local ge sp rs0 m0 {| hsi_smem := hst; hsi_ok_lsval := hsi_ok_lsval hst; hsi_sreg := red_PTree_set r exta hst |}).
    { 
      rewrite sok_local_set_sreg; generalize REF.
      intros (OKeq & MEM & REG & MVALID); rewrite OKeq.
      unfold hsok_local; simpl; intuition (subst; eauto).
      assert (X0:hsok_local ge sp rs0 m0 hst). { unfold hsok_local; intuition. }
      exploit may_trap_correct; eauto.
      * intro X1; eapply seval_list_sval_inj_not_none; eauto.
        assert (X2: sok_local ge sp rs0 m0 st). { intuition. }
        unfold sok_local in X2; intuition eauto.
      * rewrite <- MEM; eauto.
    }
    unfold hsilocal_refines; simpl; split; auto.
    rewrite <- X, sok_local_set_sreg. intuition eauto.
    - destruct REF; intuition eauto.
    - generalize REF; intros (OKEQ & _). rewrite OKEQ in * |-; erewrite red_PTree_set_refines; eauto.
Léo Gourdin's avatar
Léo Gourdin committed
822
                    Qed.
823
824
Global Opaque hslocal_set_sreg.
Local Hint Resolve hslocal_set_sreg_correct: wlp.
825

826
(* TODO gourdinl MOVE ELSEWHERE Branch expansion *)
827

828
(* TODO gourdinl NOT SURE IF THIS DEF IS NEEDED
829
830
831
832
833
 * SHOULD WE TAKE THE PREV STATE INTO ACCOUNT HERE?
Definition make_lr_prev_cmp (is_inv: bool) (a1 a2: reg) (prev: hsistate_local) : ?? list_hsval :=
  if is_inv then
   hlist_args prev*)

834
(*
835
836


Léo Gourdin's avatar
Léo Gourdin committed
837

838
  
839
Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : ?? (condition * list_hsval) :=
Léo Gourdin's avatar
Léo Gourdin committed
840
 *)
841

842
(** ** Execution of one instruction *)
843

Léo Gourdin's avatar
Léo Gourdin committed
844
845
846
847
848
849
850
851
852
853
854
855
856
857
(* TODO gourdinl
 * This is just useful for debugging fake values hashcode projection *)
Fixpoint check_no_uhid lhsv :=
  match lhsv with
  | HSnil hc =>
      DO b <~ phys_eq hc unknown_hid;;
      assert_b (negb b) "fail no uhid";;
      RET tt
  | HScons hsv lhsv' hc =>
      DO b <~ phys_eq hc unknown_hid;;
      assert_b (negb b) "fail no uhid";;
      check_no_uhid lhsv'
  end.

Sylvain Boulmé's avatar
Sylvain Boulmé committed
858
Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg): ?? (condition * list_hsval) :=
Léo Gourdin's avatar
Léo Gourdin committed
859
    match target_cbranch_expanse prev cond args with
Sylvain Boulmé's avatar
Sylvain Boulmé committed
860
861
    | Some (cond', vargs) => 
      DO vargs' <~ fsval_list_proj vargs;;
Léo Gourdin's avatar
Léo Gourdin committed
862
      RET (cond', vargs')
Sylvain Boulmé's avatar
Sylvain Boulmé committed
863
864
865
866
867
868
869
870
871
872
873
    | None =>
      DO vargs <~ hlist_args prev args ;;
      RET (cond, vargs)
    end.

Lemma cbranch_expanse_correct hst c l:
 WHEN cbranch_expanse hst c l ~> r THEN forall ge sp rs0 m0 st
  (LREF : hsilocal_refines ge sp rs0 m0 hst st)
  (OK: hsok_local ge sp rs0 m0 hst),
  seval_condition ge sp (fst r) (hsval_list_proj (snd r)) (si_smem st) rs0 m0 =
  seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
Léo Gourdin's avatar
Léo Gourdin committed
874
Proof. Admitted. (*
Sylvain Boulmé's avatar
Sylvain Boulmé committed
875
876
877
878
879
  unfold cbranch_expanse.
  destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify.
  + destruct p as [c' l']; simpl.
    exploit target_cbranch_expanse_correct; eauto.
  + unfold seval_condition; erewrite H; eauto.
Léo Gourdin's avatar
Léo Gourdin committed
880
                    Qed.*)
Sylvain Boulmé's avatar
Sylvain Boulmé committed
881
882
883
Local Hint Resolve cbranch_expanse_correct: wlp.
Global Opaque cbranch_expanse.

884
Definition hsiexec_inst (i: instruction) (hst: hsistate): ?? (option hsistate) := 
885
886
  match i with
  | Inop pc' => 
887
      RET (Some (hsist_set_local hst pc' hst.(hsi_local)))
888
  | Iop op args dst pc' =>
889
890
      DO next <~ hslocal_set_sreg hst.(hsi_local) dst (Rop op) args;;
      RET (Some (hsist_set_local hst pc' next))
Sylvain Boulmé's avatar
Sylvain Boulmé committed
891
  | Iload trap chunk addr args dst pc' =>
892
893
      DO next <~ hslocal_set_sreg hst.(hsi_local) dst (Rload trap chunk addr) args;;
      RET (Some (hsist_set_local hst pc' next))
Sylvain Boulmé's avatar
Sylvain Boulmé committed
894
  | Istore chunk addr args src pc' =>
895
896
897
      DO next <~ hslocal_store hst.(hsi_local) chunk addr args src;;
      RET (Some (hsist_set_local hst pc' next))
  | Icond cond args ifso ifnot _ =>
898
      let prev := hst.(hsi_local) in
899
      DO res <~ cbranch_expanse prev cond args;;
900
      let (cond, vargs) := res in
901
      let ex := {| hsi_cond:=cond; hsi_scondargs:=vargs; hsi_elocal := prev; hsi_ifso := ifso |} in
902
      RET (Some {| hsi_pc := ifnot; hsi_exits := ex::hst.(hsi_exits); hsi_local := prev |})
Sylvain Boulmé's avatar
Sylvain Boulmé committed
903
  | _ => RET None
904
905
  end.

906
907
Remark hsiexec_inst_None_correct i hst:
  WHEN hsiexec_inst i hst ~> o THEN forall st, o = None -> siexec_inst i st = None.
Cyril SIX's avatar
Cyril SIX committed
908
Proof.
909
  destruct i; wlp_simplify; congruence.
910
911
Qed.

912
Lemma seval_condition_refines hst st ge sp cond hargs args rs m:
913
  hsok_local ge sp rs m hst -> 
Cyril SIX's avatar
Cyril SIX committed
914
  hsilocal_refines ge sp rs m hst st ->
915
916
  list_sval_refines ge sp rs m hargs args ->
  hseval_condition ge sp cond hargs (hsi_smem hst) rs m
Cyril SIX's avatar
Cyril SIX committed
917
  = seval_condition ge sp cond args (si_smem st) rs m.
918
 Proof.
919
920
  intros HOK (_ & MEMEQ & _) LR. unfold hseval_condition, seval_condition.
  rewrite LR, <- MEMEQ; auto.
921
922
Qed.

923
924
925
Lemma sok_local_set_sreg_simp (rsv:root_sval) ge sp rs0 m0 st r lr:
  sok_local ge sp rs0 m0 (slocal_set_sreg st r (rsv lr st))
  -> sok_local ge sp rs0 m0 st.
926
Proof.
927
  rewrite sok_local_set_sreg; intuition.
928
Qed.
929

930
Local Hint Resolve hsist_set_local_correct_stat: core.
931

932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
Lemma hsiexec_cond_noexp (hst: hsistate): forall l c0 n n0,
  WHEN DO res <~
       (DO vargs <~ hlist_args (hsi_local hst) l;; RET ((c0, vargs)));;
       (let (cond, vargs) := res in
        RET (Some
               {|
               hsi_pc := n0;
               hsi_exits := {|
                            hsi_cond := cond;
                            hsi_scondargs := vargs;
                            hsi_elocal := hsi_local hst;
                            hsi_ifso := n |} :: hsi_exits hst;
               hsi_local := hsi_local hst |})) ~> o0
  THEN (forall (hst' : hsistate) (st : sistate),
        o0 = Some hst' ->
        exists st' : sistate,
          Some
            {|
            si_pc := n0;
            si_exits := {|
                        si_cond := c0;
                        si_scondargs := list_sval_inj
                                          (map (si_sreg (si_local st)) l);
                        si_elocal := si_local st;
                        si_ifso := n |} :: si_exits st;
            si_local := si_local st |} = Some st' /\
          (hsistate_refines_stat hst st -> hsistate_refines_stat hst' st') /\
          (forall (ge : RTL.genv) (sp : val) (rs0 : regset) (m0 : mem),
           hsistate_refines_dyn ge sp rs0 m0 hst st ->
           hsistate_refines_dyn ge sp rs0 m0 hst' st')).
Proof.
  intros.
  wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
  - unfold hsistate_refines_stat, hsiexits_refines_stat in *; simpl; intuition.
    constructor; simpl; eauto.
    constructor.
  - destruct H0 as (EXREF & LREF & NEST).
    split.
    + constructor; simpl; auto.
      constructor; simpl; auto.
      intros; erewrite seval_condition_refines; eauto.
    + split; simpl; auto.
      destruct NEST as [|st0 se lse TOP NEST];
      econstructor; simpl; auto; constructor; auto.
Qed.

978
979
980
981
982
983
Lemma hsiexec_inst_correct i hst:
  WHEN hsiexec_inst i hst ~> o THEN forall hst' st,
   o = Some hst' ->
   exists st', siexec_inst i st = Some st'
    /\ (forall (REF:hsistate_refines_stat hst st), hsistate_refines_stat hst' st')
    /\ (forall ge sp rs0 m0 (REF:hsistate_refines_dyn ge sp rs0 m0 hst st), hsistate_refines_dyn ge sp rs0 m0 hst' st').
Léo Gourdin's avatar
Léo Gourdin committed
984
Proof.
985
  destruct i; simpl;
986
  try (wlp_simplify; try_simplify_someHyps; eexists; intuition eauto; fail).
987
  - (* refines_dyn Iop *)
988
    wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
989
    eapply hsist_set_local_correct_dyn; eauto.
990
991
    generalize (sok_local_set_sreg_simp (Rop o)); simpl; eauto.
  - (* refines_dyn Iload *)
992
    wlp_simplify; try_simplify_someHyps; eexists; intuition eauto.
993
    eapply hsist_set_local_correct_dyn; eauto.
994
995
    generalize (sok_local_set_sreg_simp (Rload t0 m a)); simpl; eauto.
  - (* refines_dyn Istore *)