RTLpathLivegenproof.v 26.7 KB
Newer Older
1
(** Proofs of the liveness properties from the liveness checker of RTLpathLivengen.
2
3
4
5
6
7
8
9
10
11
*)


Require Import Coqlib.
Require Import Maps.
Require Import Lattice.
Require Import AST.
Require Import Op.
Require Import Registers.
Require Import Globalenvs Smallstep RTL RTLpath RTLpathLivegen.
12
Require Import Bool Errors Linking Values Events.
13
14
Require Import Program.

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
Definition match_prog (p: RTL.program) (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.

Variables prog: RTL.program.
Variables tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tpge := Genv.globalenv tprog.
Let tge := Genv.globalenv (RTLpath.transf_program tprog).

Lemma symbols_preserved s: Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof.
  rewrite <- (Genv.find_symbol_match TRANSL).
  apply (Genv.find_symbol_match (match_prog_RTL tprog)).
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: Senv.equiv ge tge.
Proof.
  eapply senv_transitivity. { eapply (Genv.senv_match TRANSL). }
  eapply RTLpath.senv_preserved.
Qed.

Lemma function_ptr_preserved v f: Genv.find_funct_ptr ge v = Some f -> 
  exists tf, Genv.find_funct_ptr tpge v = Some tf /\ transf_fundef f = OK tf.
Proof.
  intros; apply (Genv.find_funct_ptr_transf_partial TRANSL); eauto.
Qed.


Lemma function_ptr_RTL_preserved v f: Genv.find_funct_ptr ge v = Some f -> Genv.find_funct_ptr tge v = Some f.
Proof.
  intros; exploit function_ptr_preserved; eauto.
  intros (tf & Htf & TRANS).
  exploit (Genv.find_funct_ptr_match (match_prog_RTL tprog)); eauto.
  intros (cunit & tf0 & X & Y & DUM); subst.
  unfold tge. rewrite X. 
  exploit transf_fundef_correct; eauto. 
  intuition subst; auto.
Qed.

Lemma find_function_preserved ros rs fd:
  RTL.find_function ge ros rs = Some fd -> RTL.find_function tge ros rs = Some fd.
Proof.
  intros H; assert (X: exists tfd, find_function tpge ros rs = Some tfd /\ fd = fundef_RTL tfd). 
  * destruct ros; simpl in * |- *.
    + intros; exploit (Genv.find_funct_match TRANSL); eauto.
      intros (cuint & tf & H1 & H2 & H3); subst; repeat econstructor; eauto.
      exploit transf_fundef_correct; eauto. 
      intuition auto.
    + rewrite <- (Genv.find_symbol_match TRANSL) in H.
    unfold tpge. destruct (Genv.find_symbol _ i); simpl; try congruence.
    exploit function_ptr_preserved; eauto.
    intros (tf & H1 & H2); subst; repeat econstructor; eauto.
    exploit transf_fundef_correct; eauto. 
    intuition auto.
 * destruct X as (tf & X1 & X2); subst.
   eapply find_function_RTL_match; eauto.
Qed.


Local Hint Resolve symbols_preserved senv_preserved: core.

Lemma transf_program_RTL_correct: 
  forward_simulation (RTL.semantics prog) (RTL.semantics (RTLpath.transf_program tprog)).
Proof.
  eapply forward_simulation_step with (match_states:=fun (s1 s2:RTL.state) => s1=s2); simpl; eauto.
  - eapply senv_preserved.
  - (* initial states *)
    intros s1 INIT. destruct INIT as [b f m0 ge0 INIT SYMB PTR SIG]. eexists; intuition eauto.
    econstructor; eauto.
    + intros; eapply (Genv.init_mem_match (match_prog_RTL tprog)). apply (Genv.init_mem_match TRANSL); auto.
    + rewrite symbols_preserved. 
      replace (prog_main (RTLpath.transf_program tprog)) with (prog_main prog).
      * eapply SYMB.
      * erewrite (match_program_main (match_prog_RTL tprog)). erewrite (match_program_main TRANSL); auto.
    + exploit function_ptr_RTL_preserved; eauto.
  - intros; subst; auto.
  - intros s t s2 STEP s1 H; subst.
    eexists; intuition.
    destruct STEP. 
    + (* Inop *) eapply exec_Inop; eauto.
    + (* Iop *) eapply exec_Iop; eauto.
      erewrite eval_operation_preserved; eauto.
    + (* Iload *) eapply exec_Iload; eauto. 
     erewrite eval_addressing_preserved; eauto.
    + (* Iload notrap1 *) eapply exec_Iload_notrap1; eauto.
      erewrite eval_addressing_preserved; eauto.
    + (* Iload notrap2 *) eapply exec_Iload_notrap2; eauto.
      erewrite eval_addressing_preserved; eauto.
    + (* Istore *) eapply exec_Istore; eauto.
      erewrite eval_addressing_preserved; eauto.
    + (* Icall *)
        eapply RTL.exec_Icall; eauto.
        eapply find_function_preserved; eauto.
    + (* Itailcall *)
        eapply RTL.exec_Itailcall; eauto.
        eapply find_function_preserved; eauto.
    + (* Ibuiltin *)
      eapply RTL.exec_Ibuiltin; eauto.
      * eapply eval_builtin_args_preserved; eauto.
      * eapply external_call_symbols_preserved; eauto.
    + (* Icond *)
      eapply exec_Icond; eauto.
    + (* Ijumptable *)
      eapply RTL.exec_Ijumptable; eauto.
    + (* Ireturn *)
      eapply RTL.exec_Ireturn; eauto.
    + (* exec_function_internal *)
      eapply RTL.exec_function_internal; eauto.
    + (* exec_function_external *)
      eapply RTL.exec_function_external; eauto.
      eapply external_call_symbols_preserved; eauto.
    + (* exec_return *)
      eapply RTL.exec_return; eauto.
Qed.

Theorem transf_program_correct: 
  forward_simulation (RTL.semantics prog) (RTLpath.semantics tprog).
Proof.
  eapply compose_forward_simulations.
  + eapply transf_program_RTL_correct.
  + eapply RTLpath_complete.
Qed.


(* Properties used in hypothesis of [RTLpathLiveproofs.step_eqlive] theorem *)
Theorem all_fundef_liveness_ok b f:
  Genv.find_funct_ptr tpge b = Some f -> liveness_ok_fundef f.
Proof.
  unfold match_prog, match_program in TRANSL.
  unfold Genv.find_funct_ptr, tpge; simpl; intro X.
  destruct (Genv.find_def_match_2 TRANSL b) as [|f0 y H]; try congruence.
  destruct y as [tf0|]; try congruence.
  inversion X as [H1]. subst. clear X.
  remember (@Gfun fundef unit f) as f2.
  destruct H as [ctx' f1 f2 H0|]; try congruence.
  inversion Heqf2 as [H2]. subst; clear Heqf2.
  exploit transf_fundef_correct; eauto.
  intuition.
Qed.

End PRESERVATION.
170
171

Local Open Scope lazy_bool_scope.
172
Local Open Scope option_monad_scope.
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

Local Notation ext alive := (fun r => Regset.In r alive).

Lemma regset_add_spec live r1 r2: Regset.In r1 (Regset.add r2 live) <-> (r1 = r2 \/ Regset.In r1 live).
Proof.
  destruct (Pos.eq_dec r1 r2).
  - subst. intuition; eapply Regset.add_1; auto.
  - intuition. 
    * right. eapply Regset.add_3; eauto.
    * eapply Regset.add_2; auto.
Qed.

Definition eqlive_reg (alive: Regset.elt -> Prop) (rs1 rs2: regset): Prop :=
 forall r, (alive r) -> rs1#r = rs2#r. 

Lemma eqlive_reg_refl alive rs: eqlive_reg alive rs rs.
Proof.
  unfold eqlive_reg; auto.
Qed.

Lemma eqlive_reg_symmetry alive rs1 rs2: eqlive_reg alive rs1 rs2 -> eqlive_reg alive rs2 rs1.
Proof.
  unfold eqlive_reg; intros; symmetry; auto.
Qed.

Lemma eqlive_reg_trans alive rs1 rs2 rs3: eqlive_reg alive rs1 rs2 -> eqlive_reg alive rs2 rs3 -> eqlive_reg alive rs1 rs3.
Proof.
  unfold eqlive_reg; intros H0 H1 r H. rewrite H0; eauto.
Qed.

Lemma eqlive_reg_update (alive: Regset.elt -> Prop) rs1 rs2 r v: eqlive_reg (fun r1 => r1 <> r /\ alive r1) rs1 rs2 -> eqlive_reg alive (rs1 # r <- v) (rs2 # r <- v).
Proof.
  unfold eqlive_reg; intros EQLIVE r0 ALIVE.
  destruct (Pos.eq_dec r r0) as [H|H].
  - subst. rewrite! Regmap.gss. auto.
  - rewrite! Regmap.gso; auto.
Qed.

Lemma eqlive_reg_monotonic (alive1 alive2: Regset.elt -> Prop) rs1 rs2: eqlive_reg alive2 rs1 rs2 -> (forall r, alive1 r -> alive2 r) ->  eqlive_reg alive1 rs1 rs2.
Proof.
  unfold eqlive_reg; intuition.
Qed.

216
217
218
219
220
221
222
223
224
225
226
227
Lemma eqlive_reg_triv rs1 rs2: (forall r, rs1#r = rs2#r) <-> eqlive_reg (fun _ => True) rs1 rs2.
Proof.
  unfold eqlive_reg; intuition.
Qed.

Lemma eqlive_reg_triv_trans alive rs1 rs2 rs3: eqlive_reg alive rs1 rs2 -> (forall r, rs2#r = rs3#r) -> eqlive_reg alive rs1 rs3.
Proof.
  rewrite eqlive_reg_triv; intros; eapply eqlive_reg_trans; eauto.
  eapply eqlive_reg_monotonic; eauto.
  simpl; eauto.
Qed.

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
Local Hint Resolve Regset.mem_2 Regset.subset_2.

Lemma lazy_and_true (b1 b2: bool): b1 &&& b2 = true <-> b1 = true /\ b2 = true.
Proof.
  destruct b1; simpl; intuition.
Qed.

Lemma list_mem_correct (rl: list reg) (alive: Regset.t):
  list_mem rl alive = true -> forall r, List.In r rl -> ext alive r.
Proof.
  induction rl; simpl; try rewrite lazy_and_true; intuition subst; auto.
Qed.

Lemma eqlive_reg_list (alive: Regset.elt -> Prop) args rs1 rs2: eqlive_reg alive rs1 rs2 -> (forall r, List.In r args -> (alive r)) -> rs1##args = rs2##args.
Proof.
  induction args; simpl; auto.
  intros EQLIVE ALIVE; rewrite IHargs; auto.
  unfold eqlive_reg in EQLIVE.
  rewrite EQLIVE; auto.
Qed.

Lemma eqlive_reg_listmem (alive: Regset.t) args rs1 rs2: eqlive_reg (ext alive) rs1 rs2 -> list_mem args alive = true -> rs1##args = rs2##args.
Proof.
  intros; eapply eqlive_reg_list; eauto.
  intros; eapply list_mem_correct; eauto.
Qed.

255
Record eqlive_istate alive (st1 st2: istate): Prop :=
256
257
258
259
   { eqlive_continue: icontinue st1 = icontinue st2;
     eqlive_ipc: ipc st1 = ipc st2;
     eqlive_irs: eqlive_reg alive (irs st1) (irs st2);
     eqlive_imem: (imem st1) = (imem st2) }.
260

261
Lemma iinst_checker_eqlive ge sp pm alive i res rs1 rs2 m st1: 
262
263
264
  eqlive_reg (ext alive) rs1 rs2 -> 
  iinst_checker pm alive i = Some res -> 
  istep ge i sp rs1 m = Some st1 -> 
265
  exists st2, istep ge i sp rs2 m = Some st2 /\ eqlive_istate (ext (fst res)) st1 st2.
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
Proof.
  intros EQLIVE.
  destruct i; simpl; try_simplify_someHyps.
  - (* Inop *)
    repeat (econstructor; eauto).
  - (* Iop *)
    inversion_ASSERT; try_simplify_someHyps.
    inversion_SOME v. intros EVAL.
    erewrite <- eqlive_reg_listmem; eauto.
    try_simplify_someHyps.
    repeat (econstructor; simpl; eauto).
    eapply eqlive_reg_update.
    eapply eqlive_reg_monotonic; eauto.
    intros r0; rewrite regset_add_spec. 
    intuition.
  - (* Iload *)
    inversion_ASSERT; try_simplify_someHyps.
Cyril SIX's avatar
Cyril SIX committed
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
    destruct t. (* TODO - simplify that proof ? *)
    + inversion_SOME a0. intros EVAL.
      erewrite <- eqlive_reg_listmem; eauto.
      try_simplify_someHyps.
      inversion_SOME v; try_simplify_someHyps.
      repeat (econstructor; simpl; eauto).
      eapply eqlive_reg_update.
      eapply eqlive_reg_monotonic; eauto.
      intros r0; rewrite regset_add_spec.
      intuition.
    + erewrite <- (eqlive_reg_listmem _ _ rs1 rs2); eauto.
      destruct (eval_addressing _ _ _ _).
      * destruct (Memory.Mem.loadv _ _ _).
        ** intros. inv H1. repeat (econstructor; simpl; eauto).
           eapply eqlive_reg_update.
           eapply eqlive_reg_monotonic; eauto.
           intros r0; rewrite regset_add_spec.
           intuition.
        ** intros. inv H1. repeat (econstructor; simpl; eauto).
           eapply eqlive_reg_update.
           eapply eqlive_reg_monotonic; eauto.
           intros r0; rewrite regset_add_spec.
           intuition.
      * intros. inv H1. repeat (econstructor; simpl; eauto).
        eapply eqlive_reg_update.
        eapply eqlive_reg_monotonic; eauto.
        intros r0; rewrite regset_add_spec.
        intuition.
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
  - (* Istore *)
    (repeat inversion_ASSERT); try_simplify_someHyps.
    inversion_SOME a0. intros EVAL.
    erewrite <- eqlive_reg_listmem; eauto.
    rewrite <- (EQLIVE r); auto.
    inversion_SOME v; try_simplify_someHyps.
    try_simplify_someHyps.
    repeat (econstructor; simpl; eauto).
  - (* Icond *)
    inversion_ASSERT.
    inversion_SOME b. intros EVAL.
    intros ARGS; erewrite <- eqlive_reg_listmem; eauto.
    try_simplify_someHyps.
    repeat (econstructor; simpl; eauto).
    exploit exit_checker_res; eauto.
    intro; subst; simpl. auto.
Qed.

Lemma iinst_checker_istep_continue ge sp pm alive i res rs m st: 
330
331
  iinst_checker pm alive i = Some res ->
  istep ge i sp rs m = Some st ->
332
333
  icontinue st = true ->
  (snd res)=(ipc st).
334
335
336
337
338
339
Proof.
  intros; exploit iinst_checker_default_succ; eauto.
  erewrite istep_normal_exit; eauto.
  congruence.
Qed.

340
341
Lemma exit_checker_eqlive A (pm: path_map) (alive: Regset.t) (pc: node) (v:A) res rs1 rs2:
  exit_checker pm alive pc v = Some res ->  
342
  eqlive_reg (ext alive) rs1 rs2 -> 
343
344
345
346
347
348
349
350
351
352
353
354
355
356
  exists path, pm!pc = Some path /\ eqlive_reg (ext path.(input_regs)) rs1 rs2.
Proof.
  unfold exit_checker.
  inversion_SOME path.
  inversion_ASSERT. try_simplify_someHyps.
  repeat (econstructor; eauto).
  intros; eapply eqlive_reg_monotonic; eauto.
  intros; exploit Regset.subset_2; eauto.
Qed.

Lemma iinst_checker_eqlive_stopped ge sp pm alive i res rs1 rs2 m st1: 
  eqlive_reg (ext alive) rs1 rs2 -> 
  istep ge i sp rs1 m = Some st1 ->
  iinst_checker pm alive i = Some res -> 
357
358
  icontinue st1 = false ->
  exists path st2, pm!(ipc st1) = Some path /\ istep ge i sp rs2 m = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2.
359
360
361
362
Proof.
  intros EQLIVE.
  set (tmp := istep ge i sp rs2).
  destruct i; simpl; try_simplify_someHyps; repeat (inversion_ASSERT || inversion_SOME b);  try_simplify_someHyps; try congruence.
Cyril SIX's avatar
Cyril SIX committed
363
  1-3: explore_destruct; simpl; try_simplify_someHyps; repeat (inversion_ASSERT || inversion_SOME b);  try_simplify_someHyps; try congruence.
364
365
366
367
368
369
370
371
372
373
374
375
376
377
  (* Icond *)
  unfold tmp; clear tmp; simpl.
  intros EVAL; erewrite <- eqlive_reg_listmem; eauto.
  try_simplify_someHyps.
  destruct b eqn:EQb; simpl in * |-; try congruence.
  intros; exploit exit_checker_eqlive; eauto.
  intros (path & PATH & EQLIVE2).
  repeat (econstructor; simpl; eauto).
Qed.

Lemma ipath_checker_eqlive_normal ge ps (f:function) sp pm: forall alive pc res rs1 rs2 m st1, 
  eqlive_reg (ext alive) rs1 rs2 ->
  ipath_checker ps f pm alive pc = Some res ->
  isteps ge ps f sp rs1 m pc = Some st1 ->
378
  icontinue st1 = true ->
379
  exists st2, isteps ge ps f sp rs2 m pc = Some st2 /\ eqlive_istate (ext (fst res)) st1 st2.
380
381
382
383
384
385
386
387
Proof.
  induction ps as [|ps]; simpl; try_simplify_someHyps.
  - repeat (econstructor; simpl; eauto).
  - inversion_SOME i; try_simplify_someHyps.
    inversion_SOME res0.
    inversion_SOME st0.
    intros.
    exploit iinst_checker_eqlive; eauto.
388
389
390
    destruct 1 as (st2 & ISTEP & [CONT PC RS MEM]).
    try_simplify_someHyps.
    rewrite <- CONT, <- MEM, <- PC.
391
    destruct (icontinue st0) eqn:CONT'.
392
393
394
395
396
    * intros; exploit iinst_checker_istep_continue; eauto.
      rewrite <- PC; intros X; rewrite X in * |-. eauto.
    * try_simplify_someHyps.
      congruence.
Qed.
397

398
399
400
Lemma ipath_checker_isteps_continue ge ps (f:function) sp pm: forall alive pc res rs m st, 
  ipath_checker ps f pm alive pc = Some res ->
  isteps ge ps f sp rs m pc = Some st ->
401
402
  icontinue st = true ->
  (snd res)=(ipc st).
403
404
405
406
407
Proof.
  induction ps as [|ps]; simpl; try_simplify_someHyps.
  inversion_SOME i; try_simplify_someHyps.
  inversion_SOME res0.
  inversion_SOME st0.
408
  destruct (icontinue st0) eqn:CONT'.
409
410
411
412
413
414
415
416
417
  - intros; exploit iinst_checker_istep_continue; eauto.
    intros EQ; rewrite EQ in * |-; clear EQ; eauto.
  - try_simplify_someHyps; congruence.
Qed.

Lemma ipath_checker_eqlive_stopped ge ps (f:function) sp pm: forall alive pc res rs1 rs2 m st1, 
  eqlive_reg (ext alive) rs1 rs2 -> 
  ipath_checker ps f pm alive pc = Some res -> 
  isteps ge ps f sp rs1 m pc = Some st1 -> 
418
419
  icontinue st1 = false ->
  exists path st2, pm!(ipc st1) = Some path /\ isteps ge ps f sp rs2 m pc = Some st2 /\ eqlive_istate (ext path.(input_regs)) st1 st2.
420
421
422
423
424
425
Proof.
  induction ps as [|ps]; simpl; try_simplify_someHyps; try congruence.
  inversion_SOME i; try_simplify_someHyps.
  inversion_SOME res0.
  inversion_SOME st0.
  intros.
426
  destruct (icontinue st0) eqn:CONT'; try_simplify_someHyps; intros.
427
428
429
430
431
432
433
434
435
436
437
438
439
  * intros; exploit iinst_checker_eqlive; eauto.
    destruct 1 as (st2 & ISTEP & [CONT PC RS MEM]).
    exploit iinst_checker_istep_continue; eauto.
    intros PC'.
    try_simplify_someHyps.
    rewrite PC', <- CONT, <- MEM, <- PC, CONT'.
    eauto.
  * intros; exploit iinst_checker_eqlive_stopped; eauto.
    intros EQLIVE; generalize EQLIVE; destruct 1 as (path & st2 & PATH & ISTEP & [CONT PC RS MEM]).
    try_simplify_someHyps.
    rewrite <- CONT, <- MEM, <- PC, CONT'.
    try_simplify_someHyps.
Qed.
440
441

Inductive eqlive_stackframes: stackframe -> stackframe -> Prop :=
442
  | eqlive_stackframes_intro path res f sp pc rs1 rs2
443
      (LIVE: liveness_ok_function f)
444
      (PATH: f.(fn_path)!pc = Some path)
445
      (EQUIV: forall v, eqlive_reg (ext path.(input_regs)) (rs1 # res <- v) (rs2 # res <- v)):
446
       eqlive_stackframes (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2). 
447
448
449
450
451

Inductive eqlive_states: state -> state -> Prop :=
  | eqlive_states_intro 
      path st1 st2 f sp pc rs1 rs2 m
      (STACKS: list_forall2 eqlive_stackframes st1 st2)
452
      (LIVE: liveness_ok_function f)
453
454
455
456
      (PATH: f.(fn_path)!pc = Some path)
      (EQUIV: eqlive_reg (ext path.(input_regs)) rs1 rs2):
      eqlive_states (State st1 f sp pc rs1 m) (State st2 f sp pc rs2 m)
  | eqlive_states_call st1 st2 f args m
457
      (LIVE: liveness_ok_fundef f)
458
459
460
461
462
463
464
      (STACKS: list_forall2 eqlive_stackframes st1 st2):
      eqlive_states (Callstate st1 f args m) (Callstate st2 f args m)
  | eqlive_states_return st1 st2 v m
      (STACKS: list_forall2 eqlive_stackframes st1 st2):
      eqlive_states (Returnstate st1 v m) (Returnstate st2 v m).


465
Section LivenessProperties.
466
467
468
469

Variable prog: program.

Let pge := Genv.globalenv prog.
470
Let ge := Genv.globalenv (RTLpath.transf_program prog).
471

472
Hypothesis all_fundef_liveness_ok: forall b f,
473
474
475
  Genv.find_funct_ptr pge b = Some f -> 
  liveness_ok_fundef f.

476
477
478
479
480
481
482
483
484
485
Lemma find_funct_liveness_ok v fd:
  Genv.find_funct pge v = Some fd -> liveness_ok_fundef fd.
Proof.
  unfold Genv.find_funct.
  destruct v; try congruence.
  destruct (Integers.Ptrofs.eq_dec _ _); try congruence.
  eapply all_fundef_liveness_ok; eauto.
Qed.

Lemma find_function_liveness_ok ros rs f:
486
487
488
  find_function pge ros rs = Some f -> liveness_ok_fundef f.
Proof.
  destruct ros as [r|i]; simpl.
489
  - intros; eapply find_funct_liveness_ok; eauto.
490
  - destruct (Genv.find_symbol pge i); try congruence.
491
    eapply all_fundef_liveness_ok; eauto.
492
493
Qed.

494
495
496
497
498
499
500
501
502
503
Lemma find_function_eqlive alive ros rs1 rs2:
  eqlive_reg (ext alive) rs1 rs2 ->
  reg_sum_mem ros alive = true ->
  find_function pge ros rs1 = find_function pge ros rs2.
Proof.
  intros EQLIVE.
  destruct ros; simpl; auto.
  intros H; erewrite (EQLIVE r); eauto.
Qed.

504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
Lemma inst_checker_from_iinst_checker i sp rs m st pm alive:
  istep ge i sp rs m = Some st -> 
  inst_checker pm alive i = (SOME res <- iinst_checker pm alive i IN exit_checker pm (fst res) (snd res) tt).
Proof.
  destruct i; simpl; try congruence. 
Qed.

Lemma exit_checker_eqlive_ext1 (pm: path_map) (alive: Regset.t) (pc: node) r rs1 rs2:
  exit_checker pm (Regset.add r alive) pc tt = Some tt ->  
  eqlive_reg (ext alive) rs1 rs2 ->
  exists path, pm!pc = Some path /\ (forall v, eqlive_reg (ext path.(input_regs)) (rs1 # r <- v) (rs2 # r <- v)).
Proof.
  unfold exit_checker.
  inversion_SOME path.
  inversion_ASSERT. try_simplify_someHyps.
  repeat (econstructor; eauto).
  intros; eapply eqlive_reg_update; eauto.
  eapply eqlive_reg_monotonic; eauto.
  intros r0 [X1 X2]; exploit Regset.subset_2; eauto.
  rewrite regset_add_spec. intuition subst.
Qed.

526
Local Hint Resolve in_or_app: local.
527
528
529
Lemma eqlive_eval_builtin_args alive rs1 rs2 sp m args vargs:
  eqlive_reg alive rs1 rs2 ->
  Events.eval_builtin_args ge (fun r => rs1 # r) sp m args vargs ->
530
  (forall r, List.In r (params_of_builtin_args args) -> alive r) ->
531
  Events.eval_builtin_args ge (fun r => rs2 # r) sp m args vargs.
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
Proof.
  unfold Events.eval_builtin_args.
  intros EQLIVE; induction 1 as [|a1 al b1 bl EVAL1 EVALL]; simpl.
  { econstructor; eauto. }
  intro X. 
  assert (X1: eqlive_reg (fun r => In r (params_of_builtin_arg a1)) rs1 rs2).
  { eapply eqlive_reg_monotonic; eauto with local. }
  lapply IHEVALL; eauto with local.
  clear X IHEVALL; intro X. econstructor; eauto.
  generalize X1; clear EVALL X1 X.
  induction EVAL1; simpl; try (econstructor; eauto; fail).
  - intros X1; erewrite X1; [ econstructor; eauto | eauto ].
  - intros; econstructor.
    + eapply IHEVAL1_1; eauto.
      eapply eqlive_reg_monotonic; eauto.
      simpl; intros; eauto with local.
    + eapply IHEVAL1_2; eauto.
      eapply eqlive_reg_monotonic; eauto.
      simpl; intros; eauto with local.
  - intros; econstructor.
    + eapply IHEVAL1_1; eauto.
      eapply eqlive_reg_monotonic; eauto.
      simpl; intros; eauto with local.
    + eapply IHEVAL1_2; eauto.
      eapply eqlive_reg_monotonic; eauto.
      simpl; intros; eauto with local.
Qed.
559
560

Lemma exit_checker_eqlive_builtin_res (pm: path_map) (alive: Regset.t) (pc: node) rs1 rs2 (res:builtin_res reg):
561
  exit_checker pm (reg_builtin_res res alive) pc tt = Some tt ->
562
563
  eqlive_reg (ext alive) rs1 rs2 ->
  exists path, pm!pc = Some path /\ (forall vres, eqlive_reg (ext path.(input_regs)) (regmap_setres res vres rs1) (regmap_setres res vres rs2)).
564
565
566
567
568
569
570
571
572
573
Proof.
  destruct res; simpl.
  - intros; exploit exit_checker_eqlive_ext1; eauto.
  - intros; exploit exit_checker_eqlive; eauto.
    intros (path & PATH & EQLIVE).
    eexists; intuition eauto.
  - intros; exploit exit_checker_eqlive; eauto.
    intros (path & PATH & EQLIVE).
    eexists; intuition eauto.
Qed.
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588

Lemma exit_list_checker_eqlive (pm: path_map) (alive: Regset.t) (tbl: list node) rs1 rs2 pc: forall n,
  exit_list_checker pm alive tbl = true ->  
  eqlive_reg (ext alive) rs1 rs2 -> 
  list_nth_z tbl n = Some pc ->
  exists path, pm!pc = Some path /\ eqlive_reg (ext path.(input_regs)) rs1 rs2.
Proof.
  induction tbl; simpl.
  - intros; try congruence.
  - intros n; rewrite lazy_and_Some_tt_true; destruct (zeq n 0) eqn: Hn.
    * try_simplify_someHyps; intuition.
      exploit exit_checker_eqlive; eauto.
    * intuition. eapply IHtbl; eauto.
Qed.

589
Lemma inst_checker_eqlive (f: function) sp alive pc i rs1 rs2 m stk1 stk2 t s1:
590
591
592
593
594
595
596
597
598
599
  list_forall2 eqlive_stackframes stk1 stk2 ->
  eqlive_reg (ext alive) rs1 rs2 -> 
  liveness_ok_function f ->
  (fn_code f) ! pc = Some i ->
  path_last_step ge pge stk1 f sp pc rs1 m t s1 ->
  inst_checker (fn_path f) alive i = Some tt -> 
  exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
Proof.
  intros STACKS EQLIVE LIVENESS PC; 
  destruct 1 as [i' sp pc rs1 m st1|
600
                 sp pc rs1 m sig ros args res pc' fd|
601
602
                 st1 pc rs1 m sig ros args fd m'|
                 sp pc rs1 m ef args res pc' vargs t vres m'|
603
                 sp pc rs1 m arg tbl n pc' |
604
605
606
607
608
609
                 st1 pc rs1 m optr m']; 
  try_simplify_someHyps.
  + (* istate *)
    intros PC ISTEP. erewrite inst_checker_from_iinst_checker; eauto.
    inversion_SOME res.
    intros.
610
    destruct (icontinue st1) eqn: CONT.
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
    - (* CONT => true *)
      exploit iinst_checker_eqlive; eauto.
      destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]).
      repeat (econstructor; simpl; eauto).
      rewrite <- MEM, <- PC2.
      exploit exit_checker_eqlive; eauto.
      intros (path & PATH & EQLIVE2).
      eapply eqlive_states_intro; eauto.
      erewrite <- iinst_checker_istep_continue; eauto.
    - (* CONT => false *)
      intros; exploit iinst_checker_eqlive_stopped; eauto.
      destruct 1 as (path & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]).
      repeat (econstructor; simpl; eauto).
      rewrite <- MEM, <- PC2.
      eapply eqlive_states_intro; eauto.
  + (* Icall *)
627
628
629
630
631
632
633
634
    repeat inversion_ASSERT. intros.
    exploit exit_checker_eqlive_ext1; eauto.
    intros (path & PATH & EQLIVE2).
    eexists; split.
    - eapply exec_Icall; eauto.
      erewrite <- find_function_eqlive; eauto.
    - erewrite eqlive_reg_listmem; eauto.
      eapply eqlive_states_call; eauto.
635
      eapply find_function_liveness_ok; eauto.
636
      repeat (econstructor; eauto).
637
  + (* Itailcall *)
638
639
640
641
642
643
    repeat inversion_ASSERT. intros.
    eexists; split.
    - eapply exec_Itailcall; eauto.
      erewrite <- find_function_eqlive; eauto.
    - erewrite eqlive_reg_listmem; eauto.
      eapply eqlive_states_call; eauto.
644
      eapply find_function_liveness_ok; eauto.
645
  + (* Ibuiltin *)
646
647
648
649
650
651
652
653
    repeat inversion_ASSERT. intros.
    exploit exit_checker_eqlive_builtin_res; eauto.
    intros (path & PATH & EQLIVE2).
    eexists; split.
    - eapply exec_Ibuiltin; eauto.
      eapply eqlive_eval_builtin_args; eauto.
      intros; eapply list_mem_correct; eauto.
    - repeat (econstructor; simpl; eauto).
654
  + (* Ijumptable *)
655
656
657
658
659
660
661
    repeat inversion_ASSERT. intros.
    exploit exit_list_checker_eqlive; eauto.
    intros (path & PATH & EQLIVE2).
    eexists; split.
    - eapply exec_Ijumptable; eauto.
      erewrite <- EQLIVE; eauto.
    - repeat (econstructor; simpl; eauto).
662
663
664
665
666
667
668
669
  + (* Ireturn *)
    repeat inversion_ASSERT. intros.
    eexists; split.
    - eapply exec_Ireturn; eauto.
    - destruct optr; simpl in * |- *.
      * erewrite (EQLIVE r); eauto.
        eapply eqlive_states_return; eauto.
      * eapply eqlive_states_return; eauto.
670
Qed.
671
672
673
674

Lemma path_step_eqlive path stk1 f sp rs1 m pc t s1 stk2 rs2:
  path_step ge pge (psize path) stk1 f sp rs1 m pc t s1 ->
  list_forall2 eqlive_stackframes stk1 stk2 ->
675
676
677
  eqlive_reg (ext (input_regs path)) rs1 rs2 ->
  liveness_ok_function f ->
  (fn_path f) ! pc = Some path ->
678
   exists s2, path_step ge pge (psize path) stk2 f sp rs2 m pc t s2 /\ eqlive_states s1 s2.
679
680
681
682
Proof.
  intros STEP STACKS EQLIVE LIVE PC.
  unfold liveness_ok_function in LIVE.
  exploit LIVE; eauto.
683
  unfold path_checker.
684
685
686
  inversion_SOME res; (* destruct res as [alive pc']. *) intros ICHECK. (* simpl. *)
  inversion_SOME i; intros PC'.
  destruct STEP as [st ISTEPS CONT|].
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
  - (* early_exit *)
    intros; exploit ipath_checker_eqlive_stopped; eauto.
    destruct 1 as (path2 & st2 & PATH & ISTEP2 & [CONT2 PC2 RS MEM]).
    repeat (econstructor; simpl; eauto).
    rewrite <- MEM, <- PC2.
    eapply eqlive_states_intro; eauto.
  - (* normal_exit *)
    intros; exploit ipath_checker_eqlive_normal; eauto.
    destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]).
    exploit ipath_checker_isteps_continue; eauto.
    intros PC3; rewrite <- PC3, <- PC2 in * |-.
    exploit inst_checker_eqlive; eauto.
    intros (s2 & LAST_STEP & EQLIVE2).
     eexists; split; eauto.
     eapply exec_normal_exit; eauto.
     rewrite <- PC3, <- MEM; auto.
Qed.
704

705
706
Theorem step_eqlive t s1 s1' s2: 
  step ge pge s1 t s1' ->
707
708
  eqlive_states s1 s2 ->
  exists s2', step ge pge s2 t s2' /\ eqlive_states s1' s2'.
709
710
711
712
Proof.
  destruct 1 as [path stack f sp rs m pc t s PATH STEP | | | ].
  - intros EQLIVE; inv EQLIVE; simplify_someHyps. 
    intro PATH.
713
714
715
716
717
718
719
    exploit path_step_eqlive; eauto.
    intros (s2 & STEP2 & EQUIV2). 
    eexists; split; eauto.
    eapply exec_path; eauto.
  - intros EQLIVE; inv EQLIVE; inv LIVE.
    exploit initialize_path. { eapply fn_entry_point_wf. }
    intros (path & Hpath).
720
721
722
    eexists; split.
    * eapply exec_function_internal; eauto.
    * eapply eqlive_states_intro; eauto.
723
724
725
726
727
728
729
730
731
732
733
      eapply eqlive_reg_refl.
  - intros EQLIVE; inv EQLIVE.
    eexists; split.
    * eapply exec_function_external; eauto.
    * eapply eqlive_states_return; eauto.
  - intros EQLIVE; inv EQLIVE.
    inversion STACKS as [|s1 st1 s' s2 STACK STACKS']; subst; clear STACKS.
    inv STACK.
    exists (State s2 f sp pc (rs2 # res <- vres) m); split.
    * apply exec_return.
    * eapply eqlive_states_intro; eauto.
734
735
Qed.

Cyril SIX's avatar
Cyril SIX committed
736
End LivenessProperties.