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
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
|
Require Import AST Linking Values Maps Globalenvs Smallstep Registers.
Require Import Coqlib Maps Events Errors Op OptionMonad.
Require Import RTL BTL BTL_SEtheory.
Require Import BTLmatchRTL BTL_Scheduler.
Definition match_prog (p tp: program) :=
match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
Lemma transf_program_match:
forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
Proof.
intros. eapply match_transform_partial_program_contextual; eauto.
Qed.
Section PRESERVATION.
Variable prog: program.
Variable tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Let pge := Genv.globalenv prog.
Let tpge := Genv.globalenv tprog.
Lemma symbols_preserved s: Genv.find_symbol tpge s = Genv.find_symbol pge s.
Proof.
rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
Qed.
Lemma senv_preserved:
Senv.equiv pge tpge.
Proof.
eapply (Genv.senv_match TRANSL).
Qed.
Lemma functions_preserved:
forall (v: val) (f: fundef),
Genv.find_funct pge v = Some f ->
exists tf cunit, transf_fundef f = OK tf /\ Genv.find_funct tpge v = Some tf /\ linkorder cunit prog.
Proof.
intros. exploit (Genv.find_funct_match TRANSL); eauto.
intros (cu & tf & A & B & C).
repeat eexists; intuition eauto.
+ unfold incl; auto.
+ eapply linkorder_refl.
Qed.
Lemma transf_function_correct f f':
transf_function f = OK f' -> match_function f f'.
Proof.
unfold transf_function. intros H.
assert (OH: transf_function f = OK f') by auto. monadInv H.
econstructor; eauto.
eapply check_symbolic_simu_input_equiv; eauto.
eapply check_symbolic_simu_correct; eauto.
Qed.
Lemma transf_fundef_correct f f':
transf_fundef f = OK f' -> match_fundef f f'.
Proof.
intros TRANSF; destruct f; simpl; inv TRANSF.
+ monadInv H0. exploit transf_function_correct; eauto.
constructor; auto.
+ eapply match_External.
Qed.
Lemma function_ptr_preserved:
forall v f,
Genv.find_funct_ptr pge v = Some f ->
exists tf,
Genv.find_funct_ptr tpge v = Some tf /\ transf_fundef f = OK tf.
Proof.
intros.
exploit (Genv.find_funct_ptr_transf_partial TRANSL); eauto.
Qed.
Lemma function_sig_translated f tf: transf_fundef f = OK tf -> funsig tf = funsig f.
Proof.
intros H; apply transf_fundef_correct in H; destruct H; simpl; eauto.
symmetry; erewrite preserv_fnsig; eauto.
Qed.
Theorem transf_initial_states:
forall s1, initial_state prog s1 ->
exists s2, initial_state tprog s2 /\ match_states s1 s2.
Proof.
intros. inv H.
exploit function_ptr_preserved; eauto. intros (tf & FIND & TRANSF).
eexists. split.
- econstructor; eauto.
+ intros; apply (Genv.init_mem_match TRANSL); eauto.
+ replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto.
symmetry. eapply match_program_main. eauto.
+ erewrite function_sig_translated; eauto.
- constructor; eauto.
+ constructor.
+ apply transf_fundef_correct; auto.
Qed.
Lemma transf_final_states s1 s2 r:
match_states s1 s2 -> final_state s1 r -> final_state s2 r.
Proof.
intros. inv H0. inv H. inv STACKS. constructor.
Qed.
Section SYMBOLIC_CTX.
Variables f1 f2: function.
Variable sp0: val.
Variable rs0: regset.
Variable m0: Memory.Mem.mem.
Lemma symbols_preserved_rev s: Genv.find_symbol pge s = Genv.find_symbol tpge s.
Proof.
symmetry; apply symbols_preserved.
Qed.
Let ctx := Sctx f1 f2 pge tpge symbols_preserved_rev sp0 rs0 m0.
Lemma str_regs_equiv sfv1 sfv2 rs:
sfv_simu ctx sfv1 sfv2 ->
match_function f1 f2 ->
str_regs (cf (bctx1 ctx)) sfv1 rs = str_regs (cf (bctx2 ctx)) sfv2 rs.
Proof.
intros SFV MF; inv MF.
inv SFV; simpl;
erewrite equiv_input_regs_tr_inputs; auto.
Qed.
Lemma sfind_function_preserved ros1 ros2 fd:
svident_simu ctx ros1 ros2 ->
sfind_function (bctx1 ctx) ros1 = Some fd ->
exists fd',
sfind_function (bctx2 ctx) ros2 = Some fd'
/\ transf_fundef fd = OK fd'.
Proof.
unfold sfind_function. intros [sv1 sv2 SIMU|]; simpl in *.
+ rewrite !SIMU. clear SIMU.
destruct (eval_sval _ _); try congruence.
intros; exploit functions_preserved; eauto.
intros (fd' & cunit & (X1 & X2 & X3)). eexists; eauto.
+ subst. rewrite symbols_preserved. destruct (Genv.find_symbol _ _); try congruence.
intros; exploit function_ptr_preserved; eauto.
Qed.
Theorem symbolic_simu_ssem stk1 stk2 st st' s t:
sstate_simu ctx st st' ->
sem_sstate (bctx1 ctx) stk1 t s st ->
list_forall2 match_stackframes stk1 stk2 ->
match_function f1 f2 ->
exists s',
sem_sstate (bctx2 ctx) stk2 t s' st'
/\ match_states s s'.
Proof.
intros SIMU SST1 STACKS MF. inversion MF.
exploit sem_sstate_run; eauto.
intros (sis1 & sfv1 & rs' & m' & SOUT1 & SIS1 & SF).
exploit sem_si_ok; eauto. intros SOK.
exploit SIMU; simpl; eauto.
intros (sis2 & sfv2 & SOUT2 & SSIMU & SFVSIM).
remember SIS1 as EQSFV. clear HeqEQSFV.
eapply SFVSIM in EQSFV.
exploit SSIMU; eauto. intros SIS2.
destruct SIS1 as (PRE1 & SMEM1 & SREGS1).
try_simplify_someHyps; intros.
set (EQSFV2:=sfv2).
inversion EQSFV; subst; inversion SF; subst.
- (* goto *)
exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto.
+ erewrite <- str_regs_equiv; simpl; eauto.
+ econstructor.
+ intros SST2. eexists; split; eauto.
econstructor; simpl; eauto.
erewrite equiv_input_regs_tr_inputs; eauto.
- (* call *)
exploit sfind_function_preserved; eauto. intros (fd' & SFIND & FUND).
exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto.
+ erewrite <- str_regs_equiv; eauto.
+ econstructor; eauto.
* apply function_sig_translated; auto.
* erewrite <- ARGS; eauto.
+ intros SST2. eexists; split; eauto.
econstructor; simpl; eauto.
* erewrite equiv_input_regs_tr_inputs; eauto.
repeat (econstructor; eauto).
* apply transf_fundef_correct; auto.
- (* tailcall *)
exploit sfind_function_preserved; eauto. intros (fd' & SFIND & FUND).
exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto.
+ econstructor; eauto.
* apply function_sig_translated; auto.
* simpl; erewrite <- preserv_fnstacksize; eauto.
* erewrite <- ARGS; eauto.
+ intros SST2. eexists; split; eauto.
econstructor; simpl; eauto.
apply transf_fundef_correct; auto.
- (* builtin *)
exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto.
+ erewrite <- str_regs_equiv; simpl; eauto.
+ econstructor.
* eapply eval_builtin_sargs_preserved.
eapply senv_preserved.
eapply eval_list_builtin_sval_correct; eauto.
inv BARGS.
erewrite <- eval_list_builtin_sval_preserved in H0; auto.
* simpl in *; eapply external_call_symbols_preserved; eauto.
eapply senv_preserved.
+ intros SST2. eexists; split; eauto.
econstructor; simpl; eauto.
erewrite equiv_input_regs_tr_inputs; eauto.
- (* jumptable *)
exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto.
+ erewrite <- str_regs_equiv; simpl; eauto.
+ econstructor; eauto.
rewrite <- VAL; auto.
+ intros SST2. eexists; split; eauto.
econstructor; simpl; eauto.
erewrite equiv_input_regs_tr_inputs; eauto.
- (* return *)
exploit (run_sem_sstate (bctx2 ctx) st' sis2 EQSFV2); eauto.
+ econstructor; eauto.
* simpl; erewrite <- preserv_fnstacksize; eauto.
* inv OPT; eauto.
rewrite <- SIMU0; auto.
+ intros SST2. eexists; split; eauto.
econstructor; simpl; eauto.
Unshelve. all: auto.
Qed.
Theorem symbolic_simu_correct stk1 stk2 ibf1 ibf2 s t:
sstate_simu ctx (sexec f1 ibf1.(entry)) (sexec f2 ibf2.(entry)) ->
iblock_step tr_inputs (sge1 ctx) stk1 f1 (ssp ctx) (srs0 ctx) (sm0 ctx) ibf1.(entry) t s ->
list_forall2 match_stackframes stk1 stk2 ->
match_function f1 f2 ->
exists s',
iblock_step tr_inputs (sge2 ctx) stk2 f2 (ssp ctx) (srs0 ctx) (sm0 ctx) ibf2.(entry) t s'
/\ match_states s s'.
Proof.
unfold sstate_simu.
intros SIMU STEP1 STACKS MF.
exploit (sexec_correct (bctx1 ctx)); simpl; eauto.
intros SST1. exploit symbolic_simu_ssem; eauto.
intros (s2 & SST2 & MS).
exploit (sexec_exact (bctx2 ctx)); simpl; eauto.
intros (s3 & STEP & EQUIV).
exists s3. intuition eauto.
eapply match_states_equiv; eauto.
Qed.
End SYMBOLIC_CTX.
Lemma tr_inputs_eqregs_list f tbl: forall rs rs' r' ores,
(forall r : positive, rs # r = rs' # r) ->
(tr_inputs f tbl ores rs) # r' =
(tr_inputs f tbl ores rs') # r'.
Proof.
induction tbl as [|pc tbl IHtbl];
intros; destruct ores; simpl;
rewrite !tr_inputs_get; autodestruct.
Qed.
Lemma find_function_eqregs rs rs' ros fd:
(forall r : positive, rs # r = rs' # r) ->
find_function tpge ros rs = Some fd ->
find_function tpge ros rs' = Some fd.
Proof.
intros EQREGS; destruct ros; simpl.
rewrite EQREGS; auto.
autodestruct.
Qed.
Lemma args_eqregs (args: list reg): forall (rs rs': regset),
(forall r : positive, rs # r = rs' # r) ->
rs ## args = rs' ## args.
Proof.
induction args; simpl; trivial.
intros rs rs' EQREGS; rewrite EQREGS.
apply f_equal; eauto.
Qed.
Lemma f_arg_eqregs (rs rs': regset):
(forall r : positive, rs # r = rs' # r) ->
(fun r : positive => rs # r) = (fun r : positive => rs' # r).
Proof.
intros EQREGS; apply functional_extensionality; eauto.
Qed.
Lemma eqregs_update (rs rs': regset) v dest:
(forall r, rs # r = rs' # r) ->
(forall r, (rs # dest <- v) # r = (rs' # dest <- v) # r).
Proof.
intros EQREGS r; destruct (Pos.eq_dec dest r); subst.
* rewrite !Regmap.gss; reflexivity.
* rewrite !Regmap.gso; auto.
Qed.
Local Hint Resolve equiv_stack_refl tr_inputs_eqregs_list find_function_eqregs eqregs_update: core.
Lemma iblock_istep_eqregs_None sp ib: forall rs m rs' rs1 m1
(EQREGS: forall r, rs # r = rs' # r)
(ISTEP: iblock_istep tpge sp rs m ib rs1 m1 None),
exists rs1',
iblock_istep tpge sp rs' m ib rs1' m1 None
/\ (forall r, rs1 # r = rs1' # r).
Proof.
induction ib; intros; inv ISTEP.
- repeat econstructor; eauto.
- repeat econstructor; eauto.
erewrite args_eqregs; eauto.
- inv LOAD; repeat econstructor; eauto;
erewrite args_eqregs; eauto.
- repeat econstructor; eauto.
erewrite args_eqregs; eauto.
rewrite <- EQREGS; eauto.
- exploit IHib1; eauto.
intros (rs1' & ISTEP1 & EQREGS1).
exploit IHib2; eauto.
intros (rs2' & ISTEP2 & EQREGS2).
eexists; split. econstructor; eauto.
eauto.
- destruct b.
1: exploit IHib1; eauto.
2: exploit IHib2; eauto.
all:
intros (rs1' & ISTEP & EQREGS');
eexists; split; try eapply exec_cond;
try erewrite args_eqregs; eauto.
Qed.
Lemma iblock_step_eqregs stk sp f ib: forall rs rs' m t s
(EQREGS: forall r, rs # r = rs' # r)
(STEP: iblock_step tr_inputs tpge stk f sp rs m ib t s),
exists s',
iblock_step tr_inputs tpge stk f sp rs' m ib t s'
/\ equiv_state s s'.
Proof.
induction ib; intros;
destruct STEP as (rs2 & m2 & fin & ISTEP & FSTEP); inv ISTEP.
- inv FSTEP;
eexists; split; repeat econstructor; eauto.
+ destruct (or); simpl; try rewrite EQREGS; constructor; eauto.
+ erewrite args_eqregs; eauto. repeat econstructor; eauto.
+ erewrite args_eqregs; eauto. econstructor; eauto.
+ erewrite f_arg_eqregs; eauto.
+ destruct res; simpl; eauto.
+ rewrite <- EQREGS; auto.
- exploit IHib1; eauto.
+ econstructor. do 2 eexists; split; eauto.
+ intros (s' & STEP & EQUIV). clear FSTEP.
destruct STEP as (rs3 & m3 & fin2 & ISTEP & FSTEP).
repeat (econstructor; eauto).
- exploit iblock_istep_eqregs_None; eauto.
intros (rs1' & ISTEP1 & EQREGS1).
exploit IHib2; eauto.
+ econstructor. do 2 eexists; split; eauto.
+ intros (s' & STEP & EQUIV). clear FSTEP.
destruct STEP as (rs3 & m3 & fin2 & ISTEP & FSTEP).
eexists; split; eauto.
econstructor; do 2 eexists; split; eauto.
eapply exec_seq_continue; eauto.
- destruct b.
1: exploit IHib1; eauto.
3: exploit IHib2; eauto.
1,3: econstructor; do 2 eexists; split; eauto.
all:
intros (s' & STEP & EQUIV); clear FSTEP;
destruct STEP as (rs3 & m3 & fin2 & ISTEP & FSTEP);
eexists; split; eauto; econstructor;
do 2 eexists; split; eauto;
eapply exec_cond; try erewrite args_eqregs; eauto.
Qed.
Lemma iblock_step_simulation stk1 stk2 f1 f2 sp rs rs' m ibf t s1 pc
(STEP: iblock_step tr_inputs pge stk1 f1 sp rs m ibf.(entry) t s1)
(PC: (fn_code f1) ! pc = Some ibf)
(EQREGS: forall r : positive, rs # r = rs' # r)
(STACKS: list_forall2 match_stackframes stk1 stk2)
(TRANSF: match_function f1 f2)
:exists ibf' s2,
(fn_code f2) ! pc = Some ibf'
/\ iblock_step tr_inputs tpge stk2 f2 sp rs' m ibf'.(entry) t s2
/\ match_states s1 s2.
Proof.
exploit symbolic_simu_ok; eauto. intros (ib2 & PC' & SYMBS).
exploit symbolic_simu_correct; repeat (eauto; simpl).
intros (s2 & STEP2 & MS).
exploit iblock_step_eqregs; eauto. intros (s3 & STEP3 & EQUIV).
clear STEP2. exists ib2; exists s3. repeat split; auto.
eapply match_states_equiv; eauto.
Qed.
Local Hint Constructors step: core.
Theorem step_simulation s1 s1' t s2
(STEP: step tr_inputs pge s1 t s1')
(MS: match_states s1 s2)
:exists s2',
step tr_inputs tpge s2 t s2'
/\ match_states s1' s2'.
Proof.
destruct STEP as [stack ibf f sp n rs m t s PC STEP | | | ]; inv MS.
- (* iblock *)
simplify_someHyps. intros PC.
exploit iblock_step_simulation; eauto.
intros (ibf' & s2 & PC2 & STEP2 & MS2).
eexists; split; eauto.
- (* function internal *)
inversion TRANSF as [xf tf MF |]; subst.
eexists; split.
+ econstructor. erewrite <- preserv_fnstacksize; eauto.
+ erewrite preserv_fnparams; eauto.
erewrite preserv_entrypoint; eauto.
econstructor; eauto.
- (* function external *)
inv TRANSF. eexists; split; econstructor; eauto.
eapply external_call_symbols_preserved; eauto. apply senv_preserved.
- (* return *)
inv STACKS. destruct b1 as [res' f' sp' pc' rs'].
eexists; split.
+ econstructor.
+ inv H1. econstructor; eauto.
Qed.
Theorem transf_program_correct:
forward_simulation (fsem prog) (fsem tprog).
Proof.
eapply forward_simulation_step with match_states; simpl; eauto. (* lock-step with respect to match_states *)
- eapply senv_preserved.
- eapply transf_initial_states.
- eapply transf_final_states.
- intros; eapply step_simulation; eauto.
Qed.
End PRESERVATION.
|
