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
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Sylvain Boulmé Grenoble-INP, VERIMAG *)
(* *)
(* Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
(** A theory for checking/proving simulation by symbolic execution.
*)
Require Coq.Logic.FunctionalExtensionality. (* not really necessary -- see lemma at the end *)
Require Setoid. (* in order to rewrite <-> *)
Require Export AbstractBasicBlocksDef.
Require Import List.
Require Import ImpPrelude.
Import HConsingDefs.
Module SimuTheory (L: SeqLanguage).
Export L.
Export LP.
Inductive term :=
| Input (x:R.t)
| App (o: op) (l: list_term)
with list_term :=
| LTnil
| LTcons (t:term) (l:list_term)
.
Fixpoint term_eval (ge: genv) (t: term) (m: mem): option value :=
match t with
| Input x => Some (m x)
| App o l =>
match list_term_eval ge l m with
| Some v => op_eval ge o v
| _ => None
end
end
with list_term_eval ge (l: list_term) (m: mem) {struct l}: option (list value) :=
match l with
| LTnil => Some nil
| LTcons t l' =>
match term_eval ge t m, list_term_eval ge l' m with
| Some v, Some lv => Some (v::lv)
| _, _ => None
end
end.
(** The (abstract) symbolic memory state *)
Record smem :=
{
pre: genv -> mem -> Prop; (**r pre-condition expressing that the computation has not yet abort on a None. *)
post:> R.t -> term (**r the output term computed on each pseudo-register *)
}.
(** Initial symbolic memory state *)
Definition smem_empty := {| pre:=fun _ _ => True; post:=(fun x => Input x) |}.
Fixpoint exp_term (e: exp) (d old: smem) : term :=
match e with
| PReg x => d x
| Op o le => App o (list_exp_term le d old)
| Old e => exp_term e old old
end
with list_exp_term (le: list_exp) (d old: smem) : list_term :=
match le with
| Enil => LTnil
| Econs e le' => LTcons (exp_term e d old) (list_exp_term le' d old)
| LOld le => list_exp_term le old old
end.
(** assignment of the symbolic memory state *)
Definition smem_set (d:smem) x (t:term) :=
{| pre:=(fun ge m => (term_eval ge (d x) m) <> None /\ (d.(pre) ge m));
post:=fun y => if R.eq_dec x y then t else d y |}.
(** Simulation theory: the theorem [bblock_smem_simu] ensures that the simulation between two abstract basic blocks is implied by the simulation between their symbolic execution. *)
Section SIMU_THEORY.
Variable ge: genv.
Lemma set_spec_eq d x t m:
term_eval ge (smem_set d x t x) m = term_eval ge t m.
Proof.
unfold smem_set; cbn; case (R.eq_dec x x); try congruence.
Qed.
Lemma set_spec_diff d x y t m:
x <> y -> term_eval ge (smem_set d x t y) m = term_eval ge (d y) m.
Proof.
unfold smem_set; cbn; case (R.eq_dec x y); try congruence.
Qed.
Fixpoint inst_smem (i: inst) (d old: smem): smem :=
match i with
| nil => d
| (x, e)::i' =>
let t:=exp_term e d old in
inst_smem i' (smem_set d x t) old
end.
Fixpoint bblock_smem_rec (p: bblock) (d: smem): smem :=
match p with
| nil => d
| i::p' =>
let d':=inst_smem i d d in
bblock_smem_rec p' d'
end.
Definition bblock_smem: bblock -> smem
:= fun p => bblock_smem_rec p smem_empty.
Lemma inst_smem_pre_monotonic i old: forall d m,
(pre (inst_smem i d old) ge m) -> (pre d ge m).
Proof.
induction i as [|[y e] i IHi]; cbn; auto.
intros d a H; generalize (IHi _ _ H); clear H IHi.
unfold smem_set; cbn; intuition.
Qed.
Lemma bblock_smem_pre_monotonic p: forall d m,
(pre (bblock_smem_rec p d) ge m) -> (pre d ge m).
Proof.
induction p as [|i p' IHp']; cbn; eauto.
intros d a H; eapply inst_smem_pre_monotonic; eauto.
Qed.
Local Hint Resolve inst_smem_pre_monotonic bblock_smem_pre_monotonic: core.
Lemma term_eval_exp e (od:smem) m0 old:
(forall x, term_eval ge (od x) m0 = Some (old x)) ->
forall (d:smem) m1,
(forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
term_eval ge (exp_term e d od) m0 = exp_eval ge e m1 old.
Proof.
intro H.
induction e using exp_mut with
(P0:=fun l => forall (d:smem) m1, (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> list_term_eval ge (list_exp_term l d od) m0 = list_exp_eval ge l m1 old);
cbn; auto.
- intros; erewrite IHe; eauto.
- intros. erewrite IHe, IHe0; eauto.
Qed.
Lemma inst_smem_abort i m0 x old: forall (d:smem),
pre (inst_smem i d old) ge m0 ->
term_eval ge (d x) m0 = None ->
term_eval ge (inst_smem i d old x) m0 = None.
Proof.
induction i as [|[y e] i IHi]; cbn; auto.
intros d VALID H; erewrite IHi; eauto. clear IHi.
unfold smem_set; cbn; destruct (R.eq_dec y x); auto.
subst;
generalize (inst_smem_pre_monotonic _ _ _ _ VALID); clear VALID.
unfold smem_set; cbn. intuition congruence.
Qed.
Lemma block_smem_rec_abort p m0 x: forall d,
pre (bblock_smem_rec p d) ge m0 ->
term_eval ge (d x) m0 = None ->
term_eval ge (bblock_smem_rec p d x) m0 = None.
Proof.
induction p; cbn; auto.
intros d VALID H; erewrite IHp; eauto. clear IHp.
eapply inst_smem_abort; eauto.
Qed.
Lemma inst_smem_Some_correct1 i m0 old (od:smem):
(forall x, term_eval ge (od x) m0 = Some (old x)) ->
forall (m1 m2: mem) (d: smem),
inst_run ge i m1 old = Some m2 ->
(forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
forall x, term_eval ge (inst_smem i d od x) m0 = Some (m2 x).
Proof.
intro X; induction i as [|[x e] i IHi]; cbn; intros m1 m2 d H.
- inversion_clear H; eauto.
- intros H0 x0.
destruct (exp_eval ge e m1 old) eqn:Heqov; try congruence.
refine (IHi _ _ _ _ _ _); eauto.
clear x0; intros x0.
unfold assign, smem_set; cbn. destruct (R.eq_dec x x0); auto.
subst; erewrite term_eval_exp; eauto.
Qed.
Lemma bblocks_smem_rec_Some_correct1 p m0: forall (m1 m2: mem) (d: smem),
run ge p m1 = Some m2 ->
(forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
forall x, term_eval ge (bblock_smem_rec p d x) m0 = Some (m2 x).
Proof.
Local Hint Resolve inst_smem_Some_correct1: core.
induction p as [ | i p]; cbn; intros m1 m2 d H.
- inversion_clear H; eauto.
- intros H0 x0.
destruct (inst_run ge i m1 m1) eqn: Heqov.
+ refine (IHp _ _ _ _ _ _); eauto.
+ inversion H.
Qed.
Lemma bblock_smem_Some_correct1 p m0 m1:
run ge p m0 = Some m1
-> forall x, term_eval ge (bblock_smem p x) m0 = Some (m1 x).
Proof.
intros; eapply bblocks_smem_rec_Some_correct1; eauto.
Qed.
Lemma inst_smem_None_correct i m0 old (od: smem):
(forall x, term_eval ge (od x) m0 = Some (old x)) ->
forall m1 d, pre (inst_smem i d od) ge m0 ->
(forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
inst_run ge i m1 old = None -> exists x, term_eval ge (inst_smem i d od x) m0 = None.
Proof.
intro X; induction i as [|[x e] i IHi]; cbn; intros m1 d.
- discriminate.
- intros VALID H0.
destruct (exp_eval ge e m1 old) eqn: Heqov.
+ refine (IHi _ _ _ _); eauto.
intros x0; unfold assign, smem_set; cbn. destruct (R.eq_dec x x0); auto.
subst; erewrite term_eval_exp; eauto.
+ intuition.
constructor 1 with (x:=x); cbn.
apply inst_smem_abort; auto.
rewrite set_spec_eq.
erewrite term_eval_exp; eauto.
Qed.
Lemma inst_smem_Some_correct2 i m0 old (od: smem):
(forall x, term_eval ge (od x) m0 = Some (old x)) ->
forall (m1 m2: mem) d,
pre (inst_smem i d od) ge m0 ->
(forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
(forall x, term_eval ge (inst_smem i d od x) m0 = Some (m2 x)) ->
res_eq (Some m2) (inst_run ge i m1 old).
Proof.
intro X.
induction i as [|[x e] i IHi]; cbn; intros m1 m2 d VALID H0.
- intros H; eapply ex_intro; intuition eauto.
generalize (H0 x); rewrite H.
congruence.
- intros H.
destruct (exp_eval ge e m1 old) eqn: Heqov.
+ refine (IHi _ _ _ _ _ _); eauto.
intros x0; unfold assign, smem_set; cbn; destruct (R.eq_dec x x0); auto.
subst; erewrite term_eval_exp; eauto.
+ generalize (H x).
rewrite inst_smem_abort; discriminate || auto.
rewrite set_spec_eq.
erewrite term_eval_exp; eauto.
Qed.
Lemma bblocks_smem_rec_Some_correct2 p m0: forall (m1 m2: mem) d,
pre (bblock_smem_rec p d) ge m0 ->
(forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
(forall x, term_eval ge (bblock_smem_rec p d x) m0 = Some (m2 x)) ->
res_eq (Some m2) (run ge p m1).
Proof.
induction p as [|i p]; cbn; intros m1 m2 d VALID H0.
- intros H; eapply ex_intro; intuition eauto.
generalize (H0 x); rewrite H.
congruence.
- intros H.
destruct (inst_run ge i m1 m1) eqn: Heqom.
+ refine (IHp _ _ _ _ _ _); eauto.
+ assert (X: exists x, term_eval ge (inst_smem i d d x) m0 = None).
{ eapply inst_smem_None_correct; eauto. }
destruct X as [x H1].
generalize (H x).
erewrite block_smem_rec_abort; eauto.
congruence.
Qed.
Lemma bblock_smem_Some_correct2 p m0 m1:
pre (bblock_smem p) ge m0 ->
(forall x, term_eval ge (bblock_smem p x) m0 = Some (m1 x))
-> res_eq (Some m1) (run ge p m0).
Proof.
intros; eapply bblocks_smem_rec_Some_correct2; eauto.
Qed.
Lemma inst_valid i m0 old (od:smem):
(forall x, term_eval ge (od x) m0 = Some (old x)) ->
forall (m1 m2: mem) (d: smem),
pre d ge m0 ->
inst_run ge i m1 old = Some m2 ->
(forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
pre (inst_smem i d od) ge m0.
Proof.
induction i as [|[x e] i IHi]; cbn; auto.
intros Hold m1 m2 d VALID0 H Hm1.
destruct (exp_eval ge e m1 old) eqn: Heq; cbn; try congruence.
eapply IHi; eauto.
+ unfold smem_set in * |- *; cbn.
rewrite Hm1; intuition congruence.
+ intros x0. unfold assign, smem_set; cbn; destruct (R.eq_dec x x0); auto.
subst; erewrite term_eval_exp; eauto.
Qed.
Lemma block_smem_rec_valid p m0: forall (m1 m2: mem) (d:smem),
pre d ge m0 ->
run ge p m1 = Some m2 ->
(forall x, term_eval ge (d x) m0 = Some (m1 x)) ->
pre (bblock_smem_rec p d) ge m0.
Proof.
Local Hint Resolve inst_valid: core.
induction p as [ | i p]; cbn; intros m1 d H; auto.
intros H0 H1.
destruct (inst_run ge i m1 m1) eqn: Heqov; eauto.
congruence.
Qed.
Lemma bblock_smem_valid p m0 m1:
run ge p m0 = Some m1 ->
pre (bblock_smem p) ge m0.
Proof.
intros; eapply block_smem_rec_valid; eauto.
unfold smem_empty; cbn. auto.
Qed.
Definition smem_valid ge d m := pre d ge m /\ forall x, term_eval ge (d x) m <> None.
Definition smem_simu (d1 d2: smem): Prop :=
(forall m, smem_valid ge d1 m -> smem_valid ge d2 m)
/\ (forall m0 x, smem_valid ge d1 m0 ->
term_eval ge (d1 x) m0 = term_eval ge (d2 x) m0).
Theorem bblock_smem_simu p1 p2:
smem_simu (bblock_smem p1) (bblock_smem p2) ->
bblock_simu ge p1 p2.
Proof.
Local Hint Resolve bblock_smem_valid bblock_smem_Some_correct1: core.
intros (INCL & EQUIV) m DONTFAIL; unfold smem_valid in * |-.
destruct (run ge p1 m) as [m1|] eqn: RUN1; cbn; try congruence.
assert (X: forall x, term_eval ge (bblock_smem p1 x) m = Some (m1 x)); eauto.
eapply bblock_smem_Some_correct2; eauto.
+ destruct (INCL m); intuition eauto.
congruence.
+ intro x; erewrite <- EQUIV; intuition eauto.
congruence.
Qed.
Lemma smem_valid_set_decompose_1 d t x m:
smem_valid ge (smem_set d x t) m -> smem_valid ge d m.
Proof.
unfold smem_valid; intros ((PRE1 & PRE2) & VALID); split.
+ intuition.
+ intros x0 H. case (R.eq_dec x x0).
* intuition congruence.
* intros DIFF; eapply VALID. erewrite set_spec_diff; eauto.
Qed.
Lemma smem_valid_set_decompose_2 d t x m:
smem_valid ge (smem_set d x t) m -> term_eval ge t m <> None.
Proof.
unfold smem_valid; intros ((PRE1 & PRE2) & VALID) H.
generalize (VALID x); rewrite set_spec_eq.
tauto.
Qed.
Lemma smem_valid_set_proof d x t m:
smem_valid ge d m -> term_eval ge t m <> None -> smem_valid ge (smem_set d x t) m.
Proof.
unfold smem_valid; intros (PRE & VALID) PREt. split.
+ split; auto.
+ intros x0; unfold smem_set; cbn; case (R.eq_dec x x0); intros; subst; auto.
Qed.
End SIMU_THEORY.
(** REMARK: this theorem reformulates the lemma above in a more abstract way (but relies on functional_extensionality axiom).
*)
Definition smem_correct ge (d: smem) (m: mem) (om: option mem): Prop:=
forall m', om=Some m' <-> (d.(pre) ge m /\ forall x, term_eval ge (d x) m = Some (m' x)).
Lemma bblock_smem_correct ge p m: smem_correct ge (bblock_smem p) m (run ge p m).
Proof.
unfold smem_correct; cbn; intros m'; split.
+ intros; split.
* eapply bblock_smem_valid; eauto.
* eapply bblock_smem_Some_correct1; eauto.
+ intros (H1 & H2).
destruct (bblock_smem_Some_correct2 ge p m m') as (m2 & X & Y); eauto.
rewrite X. f_equal.
apply FunctionalExtensionality.functional_extensionality; auto.
Qed.
End SimuTheory.
|
