RTLpathSchedulerproof.v 19.1 KB
Newer Older
Sylvain Boulmé's avatar
Sylvain Boulmé committed
1
Require Import AST Linking Values Maps Globalenvs Smallstep Registers.
2
Require Import Coqlib Maps Events Errors Op.
3
4
Require Import RTL RTLpath RTLpathLivegen RTLpathLivegenproof RTLpathSE_theory.
Require Import RTLpathScheduler.
5

6
7
8
9
10
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.
11
Proof.
12
13
  intros. eapply match_transform_partial_program_contextual; eauto.
Qed.
14

15
Section PRESERVATION.
16

17
18
Variable prog: program.
Variable tprog: program.
19

20
Hypothesis TRANSL: match_prog prog tprog.
21

22
23
Let pge := Genv.globalenv prog.
Let tpge := Genv.globalenv tprog.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
24

25
Hypothesis all_fundef_liveness_ok: forall b fd, Genv.find_funct_ptr pge b = Some fd -> liveness_ok_fundef fd.
26

Sylvain Boulmé's avatar
Sylvain Boulmé committed
27
Lemma symbols_preserved s: Genv.find_symbol tpge s = Genv.find_symbol pge s.
28
29
30
Proof.
  rewrite <- (Genv.find_symbol_match TRANSL). reflexivity.
Qed.
31

Sylvain Boulmé's avatar
Sylvain Boulmé committed
32
Lemma senv_preserved:
33
  Senv.equiv pge tpge.
34
Proof.
35
  eapply (Genv.senv_match TRANSL).
36
Qed.
37

38
Lemma functions_preserved:
39
40
41
42
43
44
45
46
47
48
  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.
49

50
Lemma function_ptr_preserved:
51
52
53
54
55
56
57
58
59
  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.

60
Lemma function_sig_preserved:
61
62
63
  forall f tf, transf_fundef f = OK tf -> funsig tf = funsig f.
Proof.
  intros. destruct f.
64
65
66
67
68
69
70
  - simpl in H. monadInv H.
    destruct (transf_function f) as [res H]; simpl in * |- *; auto.
    destruct (H _ EQ).
    intuition subst; auto.
    symmetry.
    eapply match_function_preserves.
    eassumption.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
71
  - simpl in H. monadInv H. reflexivity.
72
73
74
75
76
77
78
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.
79
  exploit function_ptr_preserved; eauto. intros (tf & FIND &  TRANSF).
Sylvain Boulmé's avatar
Sylvain Boulmé committed
80
81
  exists (Callstate nil tf nil m0).
  split.
82
  - econstructor; eauto.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
83
    + intros; apply (Genv.init_mem_match TRANSL); assumption.
84
85
86
    + replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto.
      symmetry. eapply match_program_main. eauto.
    + destruct f.
87
88
89
90
91
      * monadInv TRANSF. rewrite <- H3.
        destruct (transf_function f) as [res H]; simpl in * |- *; auto.
        destruct (H _ EQ).
        intuition subst; auto.
        symmetry; eapply match_function_preserves. eassumption.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
92
      * monadInv TRANSF. assumption.
93
94
95
  - constructor; eauto.
    + constructor.
    + apply transf_fundef_correct; auto.
96
(*     + eapply all_fundef_liveness_ok; eauto. *)
97
98
Qed.

Sylvain Boulmé's avatar
Sylvain Boulmé committed
99
100
Theorem transf_final_states s1 s2 r:
  final_state s1 r -> match_states s1 s2 -> final_state s2 r.
101
Proof.
102
  unfold final_state.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
103
104
105
106
107
  intros H; inv H.
  intros H; inv H; simpl in * |- *; try congruence.
  inv H1.
  destruct st; simpl in * |- *; try congruence.
  inv STACKS. constructor.
108
109
Qed.

110

111
112
Let ge := Genv.globalenv (RTLpath.transf_program prog).
Let tge := Genv.globalenv (RTLpath.transf_program tprog).
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131

Lemma senv_sym x y: Senv.equiv x y -> Senv.equiv y x.
Proof.
  unfold Senv.equiv. intuition congruence.
Qed.

Lemma senv_transitivity x y z: Senv.equiv x y -> Senv.equiv y z -> Senv.equiv x z.
Proof.
  unfold Senv.equiv. intuition congruence.
Qed.

Lemma senv_preserved_RTL:
  Senv.equiv ge tge.
Proof.
  eapply senv_transitivity. { eapply senv_sym; eapply RTLpath.senv_preserved. }
  eapply senv_transitivity. { eapply senv_preserved. }
  eapply RTLpath.senv_preserved.
Qed.

132
Lemma symbols_preserved_RTL s: Genv.find_symbol tge s = Genv.find_symbol ge s.
133
Proof.
134
135
136
  unfold tge, ge. erewrite RTLpath.symbols_preserved; eauto.
  rewrite symbols_preserved.
  erewrite RTLpath.symbols_preserved; eauto.
137
138
Qed.

Sylvain Boulmé's avatar
Sylvain Boulmé committed
139
140
141
142
Program Definition mkctx sp rs0 m0 {f1: RTLpath.function} (hyp: liveness_ok_function f1)
   :  simu_proof_context f1
   := {| the_ge1:= ge; the_ge2 := tge; the_sp:=sp; the_rs0:=rs0; the_m0:=m0 |}.
Obligation 2.
143
  erewrite symbols_preserved_RTL. eauto.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
144
145
Qed.

Sylvain Boulmé's avatar
Sylvain Boulmé committed
146
147
148
149
150
151
152
153
154
155
156
157
158
Lemma s_find_function_fundef f sp svos rs0 m0 fd
  (LIVE: liveness_ok_function f):
  sfind_function pge ge sp svos rs0 m0 = Some fd ->
  liveness_ok_fundef fd.
Proof.
  unfold sfind_function. destruct svos; simpl.
  + destruct (seval_sval _ _ _ _); try congruence.
    eapply find_funct_liveness_ok; eauto.
  + destruct (Genv.find_symbol _ _); try congruence.
    intros. eapply all_fundef_liveness_ok; eauto.
Qed.
Local Hint Resolve s_find_function_fundef: core.

Sylvain Boulmé's avatar
Sylvain Boulmé committed
159
160
161
162
163
Lemma s_find_function_preserved f sp svos1 svos2 rs0 m0 fd
  (LIVE: liveness_ok_function f):
  (svident_simu f (mkctx sp rs0 m0 LIVE) svos1 svos2) ->
  sfind_function pge ge sp svos1 rs0 m0 = Some fd ->
  exists fd', sfind_function tpge tge sp svos2 rs0 m0 = Some fd'
Sylvain Boulmé's avatar
Sylvain Boulmé committed
164
              /\ transf_fundef fd = OK fd'.
165
Proof.
Cyril SIX's avatar
Cyril SIX committed
166
  Local Hint Resolve symbols_preserved_RTL: core.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
167
168
  unfold sfind_function. intros [sv1 sv2 SIMU|]; simpl in *.
  + rewrite !(seval_preserved ge tge) in *; eauto.
Cyril SIX's avatar
Cyril SIX committed
169
    destruct (seval_sval _ _ _ _); try congruence.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
170
    erewrite <- SIMU; try congruence. clear SIMU.
171
    intros; exploit functions_preserved; eauto.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
172
173
174
    intros (fd' & cunit & (X1 & X2 & X3)). eexists.
    repeat split; eauto.
  + subst. rewrite symbols_preserved. destruct (Genv.find_symbol _ _); try congruence.
175
    intros; exploit function_ptr_preserved; eauto.
176
177
Qed.

178
Lemma sistate_simu f dupmap outframe sp st st' rs m is 
Sylvain Boulmé's avatar
Sylvain Boulmé committed
179
  (LIVE: liveness_ok_function f):
Cyril SIX's avatar
Cyril SIX committed
180
  ssem_internal ge sp st rs m is ->
181
  sistate_simu dupmap f outframe st st' (mkctx sp rs m LIVE)->
Sylvain Boulmé's avatar
Sylvain Boulmé committed
182
  exists is',
183
    ssem_internal tge sp st' rs m is' /\ istate_simu f dupmap outframe is is'.
184
Proof.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
185
  intros SEM X; eapply X; eauto.
186
Qed.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
187

188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
Lemma seval_builtin_sval_preserved sp rs m:
  forall bs, seval_builtin_sval ge sp bs rs m = seval_builtin_sval tge sp bs rs m.
Proof.
  induction bs.
  all: try (simpl; try reflexivity; erewrite seval_preserved by eapply symbols_preserved_RTL; reflexivity).
  all: simpl; rewrite IHbs1; rewrite IHbs2; reflexivity.
Qed.

Lemma seval_list_builtin_sval_preserved sp rs m:
  forall lbs,
  seval_list_builtin_sval ge sp lbs rs m = seval_list_builtin_sval tge sp lbs rs m.
Proof.
  induction lbs; [simpl; reflexivity|].
  simpl. rewrite seval_builtin_sval_preserved. rewrite IHlbs.
  reflexivity.
Qed.

Sylvain Boulmé's avatar
Sylvain Boulmé committed
205
206
Lemma ssem_final_simu dm f f' stk stk' sp st st' rs0 m0 sv sv' rs m t s
  (LIVE: liveness_ok_function f):
207
  match_function dm f f' ->
208
  list_forall2 match_stackframes stk stk' ->
Sylvain Boulmé's avatar
Sylvain Boulmé committed
209
  sfval_simu dm f st.(si_pc) st'.(si_pc) (mkctx sp rs0 m0 LIVE) sv sv' ->
Cyril SIX's avatar
Cyril SIX committed
210
211
  ssem_final pge ge sp st.(si_pc) stk f rs0 m0 sv rs m t s ->
  exists s', ssem_final tpge tge sp st'.(si_pc) stk' f' rs0 m0 sv' rs m t s' /\ match_states s s'.
212
Proof.
Cyril SIX's avatar
Cyril SIX committed
213
  Local Hint Resolve transf_fundef_correct: core.
214
  intros FUN STK SFV. destruct SFV; intros SEM; inv SEM; simpl in *.
215
  - (* Snone *)
216
    exploit initialize_path. { eapply dupmap_path_entry1; eauto. }
217
    intros (path & PATH).
218
    eexists; split; econstructor; eauto.
219
220
    eapply eqlive_reg_refl.
  - (* Scall *)
221
    exploit s_find_function_preserved; eauto.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
222
    intros (fd' & FIND & TRANSF).
223
    erewrite <- function_sig_preserved; eauto.
224
    exploit initialize_path. { eapply dupmap_path_entry1; eauto. }
225
    intros (path & PATH).
226
    eexists; split; econstructor; eauto.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
227
    + eapply eq_trans; try eassumption; auto.
228
    + simpl. repeat (econstructor; eauto).
229
230
  - (* Stailcall *)
    exploit s_find_function_preserved; eauto.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
231
    intros (fd' & FIND & TRANSF).
232
233
234
    erewrite <- function_sig_preserved; eauto.
    eexists; split; econstructor; eauto.
    + erewrite <- preserv_fnstacksize; eauto.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
235
    + eapply eq_trans; try eassumption; auto.
Cyril SIX's avatar
Cyril SIX committed
236
237
238
239
240
241
  - (* Sbuiltin *)
    pose senv_preserved_RTL as SRTL.
    exploit initialize_path. { eapply dupmap_path_entry1; eauto. }
    intros (path & PATH).
    eexists; split; econstructor; eauto.
    + eapply seval_builtin_args_preserved; eauto.
Cyril SIX's avatar
Cyril SIX committed
242
      eapply seval_list_builtin_sval_correct; eauto.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
243
      rewrite H0.
244
      erewrite seval_list_builtin_sval_preserved; eauto.
Cyril SIX's avatar
Cyril SIX committed
245
246
    + eapply external_call_symbols_preserved; eauto.
    + eapply eqlive_reg_refl.
247
248
249
250
251
  - (* Sjumptable *)
    exploit ptree_get_list_nth_rev; eauto. intros (p2 & LNZ & DM).
    exploit initialize_path. { eapply dupmap_path_entry1; eauto. }
    intros (path & PATH).
    eexists; split; econstructor; eauto.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
252
    + eapply eq_trans; try eassumption; auto.
253
    + eapply eqlive_reg_refl.
254
  - (* Sreturn *)
255
    eexists; split; econstructor; eauto.
Cyril SIX's avatar
Cyril SIX committed
256
    erewrite <- preserv_fnstacksize; eauto.
257
258
259
  - (* Sreturn bis *)
    eexists; split; econstructor; eauto.
    + erewrite <- preserv_fnstacksize; eauto.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
260
    + rewrite <- H. erewrite <- seval_preserved; eauto.
261
Qed.
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
(* TODO: deux lemmes à deplacer dans RTLpathLivegen ou RTLpathLivegenproof ? *)
Lemma iinst_checker_default_succ f alive i res:
  iinst_checker (fn_path f) alive i = Some res -> default_succ i = Some (snd res).
Proof.
  destruct i; simpl; try_simplify_someHyps.
  + destruct (list_mem _ _); try_simplify_someHyps.
  + destruct (list_mem _ _); try_simplify_someHyps.
  + destruct (Regset.mem _ _); try_simplify_someHyps.
    destruct (list_mem _ _); try_simplify_someHyps.
  + destruct (list_mem _ _); try_simplify_someHyps.
    unfold exit_checker.
    inversion_SOME path.
    destruct (Regset.subset _ _); try_simplify_someHyps.
Qed.

Lemma ipath_checker_default_succ (f: RTLpath.function) path: forall alive pc res,
  ipath_checker path f (fn_path f) alive pc = Some res
  -> nth_default_succ (fn_code f) path pc = Some (snd res).
Proof.
  induction path; simpl.
  + try_simplify_someHyps.
  + intros alive pc res.
    inversion_SOME i; intros INST.
    inversion_SOME res0; intros ICHK IPCHK.
    rewrite INST.
    erewrite iinst_checker_default_succ; eauto.
Qed.

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
Lemma siexec_snone_por_correct rs' is t s alive path0 i sp s0 st0 stk stk' f rs0 m0: forall
  (SSEM2 : ssem_final pge ge sp (si_pc s0) stk f rs0 m0 Snone
          (irs is) (imem is) t s)
  (SIEXEC : siexec_inst i st0 = Some s0)
  (ICHK : inst_checker (fn_path f) alive (pre_output_regs path0) i = Some tt),
  (liveness_ok_function f) ->
  list_forall2 match_stackframes stk stk' ->
  eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) (irs is) rs' ->
  exists s' : state,
    ssem_final pge ge sp (si_pc s0) stk f rs0 m0 Snone rs' (imem is) t s' /\
    eqlive_states s s'.
Proof.
  Local Hint Resolve eqlive_stacks_refl: core.
  intros ? ? ? LIVE STK EQLIVE.
  inversion SSEM2; subst; clear SSEM2.
  eexists; split.
  * econstructor.
  * generalize ICHK.
    unfold inst_checker. destruct i; simpl in *;
    unfold exit_checker; try discriminate.
    all:
      try destruct (list_mem _ _); simpl;
      try (destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence; fail).
    4,5:
      destruct (Regset.mem _ _); destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
    1,2,3,4: assert (NPC: n=(si_pc s0)).
    all: try (inv SIEXEC; simpl; auto; fail).
    1,2,3,4:
      try (destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence);
      simpl; inversion_SOME p;
      destruct (Regset.subset (input_regs p) (pre_output_regs path0)) eqn:SUB_PATH; try congruence;
      intros NPATH _; econstructor; eauto;
      try (instantiate (1:=p); rewrite <- NPC; auto; fail).
    1,2,3,4:
      eapply eqlive_reg_monotonic; eauto; simpl;
      intros; apply Regset.subset_2 in SUB_PATH;
      unfold Regset.Subset in SUB_PATH;
      apply SUB_PATH in H; auto.
    assert (NPC: n0=(si_pc s0)). { inv SIEXEC; simpl; auto. }
    inversion_SOME p.
    2: { destruct (Regset.subset _ _) eqn:?; try congruence. }
    destruct (Regset.subset _ _) eqn:SUB_ALIVE; try congruence.
    2: { destruct (Regset.subset (pre_output_regs path0) alive) eqn:?; try congruence. }
    simpl.
    destruct (Regset.subset (pre_output_regs path0) alive) eqn:SUB_ALIVE'; try congruence.
    inversion_SOME p'.
    destruct (Regset.subset (input_regs p') (pre_output_regs path0)) eqn:SUB_PATH; try congruence.
    intros NPATH NPATH' _. econstructor; eauto.
    instantiate (1:=p'). rewrite <- NPC; auto.
    eapply eqlive_reg_monotonic; eauto; simpl.
    intros. apply Regset.subset_2 in SUB_PATH.
    unfold Regset.Subset in SUB_PATH.
    apply SUB_PATH in H; auto.
Qed.

Sylvain Boulmé's avatar
Sylvain Boulmé committed
346
Lemma pre_output_regs_correct f pc0 path0 stk stk' sp (st:sstate) rs0 m0 t s is rs':
347
348
  (liveness_ok_function f) ->
  (fn_path f) ! pc0 = Some path0 ->
349
  (* path_step ge pge path0.(psize) stk f sp rs0 m0 pc0 t s -> *)  (* NB: should be useless *)
Sylvain Boulmé's avatar
Sylvain Boulmé committed
350
  sexec f pc0 = Some st -> 
351
  (* icontinue is = true -> *)
Sylvain Boulmé's avatar
Sylvain Boulmé committed
352
  list_forall2 match_stackframes stk stk' ->
353
  (* ssem_internal ge sp st rs0 m0 is -> *)
Sylvain Boulmé's avatar
Sylvain Boulmé committed
354
355
356
357
358
  ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) (irs is) (imem is) t s ->
  eqlive_reg (fun r : Regset.elt => Regset.In r (pre_output_regs path0)) (irs is) rs' ->
  exists s', ssem_final pge ge sp (si_pc st) stk f rs0 m0 (final st) rs' (imem is) t s' /\ eqlive_states s s'.
Proof.
  Local Hint Resolve eqlive_stacks_refl: core.
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
  intros LIVE PATH0 (*PSTEP*) SEXEC (*CONT*) STK (*SSEM1*) SSEM2 EQLIVE.
  (* start decomposing path_checker *)
  generalize (LIVE pc0 path0 PATH0).
  unfold path_checker.
  inversion_SOME res; intros IPCHK.
  inversion_SOME i; intros INST ICHK.
  exploit ipath_checker_default_succ; eauto. intros DEFSUCC.
  (* start decomposing SEXEC *)
  generalize SEXEC; clear SEXEC.
  unfold sexec; rewrite PATH0.
  inversion_SOME st0; intros SEXEC_PATH.
  exploit siexec_path_default_succ; eauto.
  simpl. rewrite DEFSUCC.
  clear DEFSUCC. destruct res as [alive pc1]. simpl in *.
  try_simplify_someHyps.
  destruct (siexec_inst i st0) eqn: SIEXEC; try_simplify_someHyps; intros.
375
376
377
378
  (* Snone *)
  eapply siexec_snone_por_correct; eauto.
  destruct i; try_simplify_someHyps; try congruence;
  inversion SSEM2; subst; clear SSEM2; simpl in *.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
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
 + (* Scall *)
    eexists; split.
    * econstructor; eauto.
    * econstructor; eauto.
      econstructor; eauto.
      econstructor; eauto.
      - admit. (* wf *)
      - intros; eapply eqlive_reg_update.
        (* TODO: condition sur pre_output_regs a revoir *)
        eapply eqlive_reg_monotonic; eauto; simpl.
        admit.
 + (* Stailcall *)
    eexists; split.
    * econstructor; eauto.
    * econstructor; eauto.
 + (* Sbuiltin *)
    eexists; split.
    * econstructor; eauto.
    * econstructor; eauto.
      - admit. (* wf *)
      - (* TODO: condition sur pre_output_regs a voir *)
        (* NB: cas du [regmap_setres] à traiter *)
        admit.
 + (* Sjumptable *)
    eexists; split.
    * econstructor; eauto.
    * econstructor; eauto.
      - admit. (* wf *)
      - (* TODO: condition sur pre_output_regs a revoir *)
        eapply eqlive_reg_monotonic; eauto; simpl.
        admit.
 + (* Sreturn *)
    eexists; split.
    * econstructor; eauto.
    * econstructor; eauto.
414
415
Admitted.

416

417
(* The main theorem on simulation of symbolic states ! *)
418
419
Theorem ssem_sstate_simu dm f f' pc0 path0 stk stk' sp st st' rs m t s:
  (fn_path f) ! pc0 = Some path0 ->
Sylvain Boulmé's avatar
Sylvain Boulmé committed
420
421
  (* path_step ge pge (psize path0) stk f sp rs m pc0 t s -> *)
  sexec f pc0 = Some st -> 
422
  match_function dm f f' ->
423
  liveness_ok_function f ->
424
  list_forall2 match_stackframes stk stk' ->
425
  ssem pge ge sp st stk f rs m t s ->
426
  (forall ctx: simu_proof_context f, sstate_simu dm f (pre_output_regs path0) st st' ctx) ->
427
  exists s', ssem tpge tge sp st' stk' f' rs m t s' /\ match_states s s'.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
428
Proof.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
429
  intros PATH0 (*STEP*) SEXEC MFUNC LIVE STACKS SEM SIMU.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
430
  destruct (SIMU (mkctx sp rs m LIVE)) as (SIMU1 & SIMU2); clear SIMU.
431
  destruct SEM as [is CONT SEM|is t s' CONT SEM1 SEM2]; simpl in *.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
432
  - (* sem_early *)
Cyril SIX's avatar
Cyril SIX committed
433
    exploit sistate_simu; eauto.
434
    unfold istate_simu; rewrite CONT.
435
    intros (is' & SEM' & (path & PATH & (CONT' & RS' & M') & PC')).
Cyril SIX's avatar
Cyril SIX committed
436
    exists (State stk' f' sp (ipc is') (irs is') (imem is')).
Sylvain Boulmé's avatar
Sylvain Boulmé committed
437
    split.
438
    + eapply ssem_early; auto. congruence.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
439
440
    + rewrite M'. econstructor; eauto.
  - (* sem_normal *)
Cyril SIX's avatar
Cyril SIX committed
441
    exploit sistate_simu; eauto.
442
    unfold istate_simu; rewrite CONT.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
443
444
445
    intros (is' & SEM' & (CONT' & RS' & M')).
    exploit pre_output_regs_correct; eauto.
    clear SEM2; intros (s0 & SEM2 & EQLIVE).
Cyril SIX's avatar
Cyril SIX committed
446
    exploit ssem_final_simu; eauto.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
447
    clear SEM2; intros (s1 & SEM2 & MATCH0).
Cyril SIX's avatar
Cyril SIX committed
448
    exploit ssem_final_equiv; eauto.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
449
450
    clear SEM2; rewrite M'; rewrite CONT' in CONT; intros (s2 & EQ & SEM2).
    exists s2; split.
451
    + eapply ssem_normal; eauto.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
452
453
    + eapply eqlive_match_states; eauto.
      eapply match_states_equiv; eauto.
454
Qed.
455
456
457

Lemma exec_path_simulation dupmap path stk stk' f f' sp rs m pc pc' t s:
  (fn_path f)!pc = Some path ->
458
  path_step ge pge path.(psize) stk f sp rs m pc t s ->
459
460
461
  list_forall2 match_stackframes stk stk' ->
  dupmap ! pc' = Some pc ->
  match_function dupmap f f' ->
462
  liveness_ok_function f ->
463
  exists path' s', (fn_path f')!pc' = Some path' /\ path_step tge tpge path'.(psize) stk' f' sp rs m pc' t s' /\ match_states s s'.
464
Proof.
465
466
467
  intros PATH STEP STACKS DUPPC MATCHF LIVE.
  exploit initialize_path. { eapply dupmap_path_entry2; eauto. }
  intros (path' & PATH').
468
  exists path'.
469
  exploit (sexec_correct f pc pge ge sp path stk rs m t s); eauto.
470
  intros (st & SYMB & SEM).
471
  exploit dupmap_correct; eauto.
Sylvain Boulmé's avatar
Sylvain Boulmé committed
472
  intros (path0 & st' & PATH0 & SYMB' & SIMU).
473
  rewrite PATH0 in PATH; inversion PATH; subst.
474
  exploit ssem_sstate_simu; eauto.
475
  intros (s0 & SEM0 & MATCH). 
476
  exploit (sexec_exact f'); eauto.
477
478
479
480
481
  intros (s' & STEP' & EQ).
  exists s'; intuition.
  eapply match_states_equiv; eauto.
Qed.

482
483
484
Lemma step_simulation s1 t s1' s2:
  step ge pge s1 t s1' ->
  match_states s1 s2 ->
485
  exists s2',
486
     step tge tpge s2 t s2'
487
488
  /\ match_states s1' s2'.
Proof.
Cyril SIX's avatar
Cyril SIX committed
489
  Local Hint Resolve eqlive_stacks_refl transf_fundef_correct: core.
490
  destruct 1 as [path stack f sp rs m pc t s PATH STEP | | | ]; intros MS; inv MS.
491
(* exec_path *)
492
  - try_simplify_someHyps. intros.
493
    exploit path_step_eqlive; eauto. (* { intros. eapply all_fundef_liveness_ok; eauto. } *)
494
    clear STEP EQUIV rs; intros (s2 & STEP & EQLIVE).
495
    exploit exec_path_simulation; eauto.
496
497
    clear STEP; intros (path' & s' & PATH' & STEP' & MATCH').
    exists s'; split.
498
    + eapply exec_path; eauto.
499
    + eapply eqlive_match_states; eauto.
500
(* exec_function_internal *)
501
502
503
504
  - inv LIVE.
    exploit initialize_path. { eapply (fn_entry_point_wf f). }
    destruct 1 as (path & PATH).
    inversion TRANSF as [f0 xf tf MATCHF|]; subst. eexists. split.
505
506
    + eapply exec_function_internal. erewrite <- preserv_fnstacksize; eauto.
    + erewrite preserv_fnparams; eauto.
507
508
509
      econstructor; eauto. 
      { apply preserv_entrypoint; auto. }
      { apply eqlive_reg_refl. }
510
511
(* exec_function_external *)
  - inversion TRANSF as [|]; subst. eexists. split.
512
    + econstructor. eapply external_call_symbols_preserved; eauto. apply senv_preserved_RTL.
513
514
515
516
    + constructor. assumption.
(* exec_return *)
  - inv STACKS. destruct b1 as [res' f' sp' pc' rs']. eexists. split.
    + constructor.
517
    + inv H1. econstructor; eauto.
518
Qed.
519
520
521
522
523
524
525

Theorem transf_program_correct:
  forward_simulation (semantics prog) (semantics tprog).
Proof.
  eapply forward_simulation_step with match_states.
  - eapply senv_preserved.
  - eapply transf_initial_states.
526
  - intros; eapply transf_final_states; eauto.
527
  - intros; eapply step_simulation; eauto.
528
529
530
Qed.

End PRESERVATION.