RTLpathLivegenproof.v 30.4 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
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. 
David Monniaux's avatar
David Monniaux committed
112
      all: erewrite eval_addressing_preserved; eauto.
113
    + (* Iload notrap1 *) eapply exec_Iload_notrap1; eauto.
David Monniaux's avatar
David Monniaux committed
114
      all: erewrite eval_addressing_preserved; eauto.
115
    + (* Iload notrap2 *) eapply exec_Iload_notrap2; eauto.
David Monniaux's avatar
David Monniaux committed
116
      all: erewrite eval_addressing_preserved; eauto.
117
    + (* Istore *) eapply exec_Istore; eauto.
David Monniaux's avatar
David Monniaux committed
118
      all: erewrite eval_addressing_preserved; eauto.
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
    + (* 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
Local Hint Resolve Regset.mem_2 Regset.subset_2: core.
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

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
Lemma final_inst_checker_from_iinst_checker i sp rs m st pm alive por:
505
  istep ge i sp rs m = Some st -> 
506
  final_inst_checker pm alive por i = None.
507
508
509
510
511
Proof.
  destruct i; simpl; try congruence.
Qed.

(* is it useful ?
512
513
514
515
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.
516
517
518
  unfold inst_checker.
  destruct (iinst_checker pm alive i); simpl; auto.
  destruct i; simpl; try congruence.
519
Qed.
520
*)
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536

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.

537
Local Hint Resolve in_or_app: local.
538
539
540
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 ->
541
  (forall r, List.In r (params_of_builtin_args args) -> alive r) ->
542
  Events.eval_builtin_args ge (fun r => rs2 # r) sp m args vargs.
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
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.
570
571

Lemma exit_checker_eqlive_builtin_res (pm: path_map) (alive: Regset.t) (pc: node) rs1 rs2 (res:builtin_res reg):
572
  exit_checker pm (reg_builtin_res res alive) pc tt = Some tt ->
573
574
  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)).
575
576
577
578
579
580
581
582
583
584
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.
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599

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.

600
Lemma final_inst_checker_eqlive (f: function) sp alive por pc i rs1 rs2 m stk1 stk2 t s1:
601
602
  list_forall2 eqlive_stackframes stk1 stk2 ->
  eqlive_reg (ext alive) rs1 rs2 -> 
603
  Regset.Subset por alive ->
604
605
606
  liveness_ok_function f ->
  (fn_code f) ! pc = Some i ->
  path_last_step ge pge stk1 f sp pc rs1 m t s1 ->
607
  final_inst_checker (fn_path f) alive por i = Some tt -> 
608
  exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
609
610
Proof.
  intros STACKS EQLIVE SUB LIVENESS PC; 
611
  destruct 1 as [i' sp pc rs1 m st1|
612
                 sp pc rs1 m sig ros args res pc' fd|
613
614
                 st1 pc rs1 m sig ros args fd m'|
                 sp pc rs1 m ef args res pc' vargs t vres m'|
615
                 sp pc rs1 m arg tbl n pc' |
616
617
618
                 st1 pc rs1 m optr m']; 
  try_simplify_someHyps.
  + (* istate *)
619
620
    intros PC ISTEP. erewrite final_inst_checker_from_iinst_checker; eauto.
    congruence.
621
  + (* Icall *)
622
623
    repeat inversion_ASSERT. intros.
    exploit exit_checker_eqlive_ext1; eauto.
624
    eapply eqlive_reg_monotonic; eauto.
625
626
627
628
629
630
    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.
631
      eapply find_function_liveness_ok; eauto.
632
      repeat (econstructor; eauto).
633
  + (* Itailcall *)
634
635
636
637
638
639
    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.
640
      eapply find_function_liveness_ok; eauto.
641
  + (* Ibuiltin *)
642
643
    repeat inversion_ASSERT. intros.
    exploit exit_checker_eqlive_builtin_res; eauto.
644
    eapply eqlive_reg_monotonic; eauto.
645
646
647
648
649
650
    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).
651
  + (* Ijumptable *)
652
653
    repeat inversion_ASSERT. intros.
    exploit exit_list_checker_eqlive; eauto.
654
    eapply eqlive_reg_monotonic; eauto.
655
656
657
658
659
    intros (path & PATH & EQLIVE2).
    eexists; split.
    - eapply exec_Ijumptable; eauto.
      erewrite <- EQLIVE; eauto.
    - repeat (econstructor; simpl; eauto).
660
661
662
663
664
665
666
667
  + (* 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.
668
Qed.
669

670
(* TODO useless?
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
Lemma subset_contra: forall por alive inputs,
  Regset.Subset por alive ->
  Regset.subset inputs alive = false ->
  Regset.subset inputs por = true ->
  False.
Proof.
  intros por alive inputs SUB CONTRA H.
  assert (INV: Regset.Subset inputs alive).
  { 
    apply Regset.subset_2 in H.
    unfold Regset.Subset in *; intros.
    auto. }
  apply Regset.subset_1 in INV. congruence.
Qed.

Lemma add_subset_contra: forall r por alive inputs,
  Regset.Subset por alive ->
  Regset.subset inputs (Regset.add r alive) = false ->
  Regset.subset inputs (Regset.add r por) = true ->
  False.
Proof.
  intros r por alive inputs SUB CONTRA H.
  assert (INV: Regset.Subset inputs (Regset.add r alive)).
  { 
    apply Regset.subset_2 in H.
    unfold Regset.Subset in *; intros.
    destruct (Pos.eq_dec r a); subst.
    * apply Regset.add_1; auto.
    * specialize H with a.
      apply Regset.add_2. 
      apply SUB. apply Regset.add_3 in H; auto. }
  apply Regset.subset_1 in INV. congruence.
Qed.

Lemma exit_list_checker_subset_contra: forall por alive f l,
  Regset.Subset por alive ->
  exit_list_checker (fn_path f) alive l = false ->
  exit_list_checker (fn_path f) por l = true ->
  False.
Proof.
  induction l.
  - simpl in *; intuition.
  - simpl in *. unfold exit_checker.
    simplify_SOME path. generalize H2, H3. 
    repeat inversion_ASSERT.
    + intuition.
    + intuition.
      exploit (subset_contra por alive (input_regs path0)); eauto;
      intros CONTRA; inv CONTRA.
Qed.

Lemma final_inst_checker_trans: forall alive por i f,
  Regset.subset por alive = true ->
  final_inst_checker (fn_path f) alive por i = Some () ->
  final_inst_checker (fn_path f) alive alive i = Some ().
Proof.
  intros.
  destruct i; simpl in *; try congruence;
  generalize H0; clear H0; unfold exit_checker;
  repeat inversion_ASSERT; simplify_SOME path;
  repeat inversion_ASSERT; intuition.
  - exploit (add_subset_contra r por alive (input_regs path0)); eauto;
    intros CONTRA; inv CONTRA.
  - destruct b; simpl in *.
    + exploit (add_subset_contra x por alive (input_regs path0)); eauto;
      intros CONTRA; inv CONTRA.
    + exploit (subset_contra por alive (input_regs path0)); eauto;
      intros CONTRA; inv CONTRA.
    + exploit (subset_contra por alive (input_regs path0)); eauto;
      intros CONTRA; inv CONTRA.
  - exploit (exit_list_checker_subset_contra por alive f l); eauto;
    intros CONTRA; inv CONTRA.
743
Qed.*)
744
745

Lemma inst_checker_eqlive (f: function) sp alive por pc i rs1 rs2 m stk1 stk2 t s1:
746
747
748
749
750
  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 ->
751
  inst_checker (fn_path f) alive por i = Some tt -> 
752
753
754
755
756
757
758
  exists s2, path_last_step ge pge stk2 f sp pc rs2 m t s2 /\ eqlive_states s1 s2.
Proof.
  unfold inst_checker;
  intros STACKS EQLIVE LIVENESS PC.
  destruct (iinst_checker (fn_path f) alive i) as [res|] eqn: IICHECKER.
  + destruct 1 as [i' sp pc rs1 m st1| | | | | ];
    try_simplify_someHyps.
759
    intros IICHECKER PC ISTEP. inversion_ASSERT.
760
761
762
763
764
765
766
    intros.
    destruct (icontinue st1) eqn: CONT.
    - (* CONT => true *)
      exploit iinst_checker_eqlive; eauto.
      destruct 1 as (st2 & ISTEP2 & [CONT' PC2 RS MEM]).
      repeat (econstructor; simpl; eauto).
      rewrite <- MEM, <- PC2.
767
      apply Regset.subset_2 in H.
768
      exploit exit_checker_eqlive; eauto.
769
      eapply eqlive_reg_monotonic; eauto.
770
771
772
773
774
775
776
777
778
      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.
779
780
  + inversion_ASSERT.
    intros; exploit final_inst_checker_eqlive; eauto.
781
782
Qed.

783
784
785
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 ->
786
787
788
  eqlive_reg (ext (input_regs path)) rs1 rs2 ->
  liveness_ok_function f ->
  (fn_path f) ! pc = Some path ->
789
   exists s2, path_step ge pge (psize path) stk2 f sp rs2 m pc t s2 /\ eqlive_states s1 s2.
790
791
792
793
Proof.
  intros STEP STACKS EQLIVE LIVE PC.
  unfold liveness_ok_function in LIVE.
  exploit LIVE; eauto.
794
  unfold path_checker.
795
796
797
  inversion_SOME res; (* destruct res as [alive pc']. *) intros ICHECK. (* simpl. *)
  inversion_SOME i; intros PC'.
  destruct STEP as [st ISTEPS CONT|].
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
  - (* 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.
815

816
817
Theorem step_eqlive t s1 s1' s2: 
  step ge pge s1 t s1' ->
818
819
  eqlive_states s1 s2 ->
  exists s2', step ge pge s2 t s2' /\ eqlive_states s1' s2'.
820
821
822
823
Proof.
  destruct 1 as [path stack f sp rs m pc t s PATH STEP | | | ].
  - intros EQLIVE; inv EQLIVE; simplify_someHyps. 
    intro PATH.
824
825
826
827
828
829
830
    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).
831
832
833
    eexists; split.
    * eapply exec_function_internal; eauto.
    * eapply eqlive_states_intro; eauto.
834
835
836
837
838
839
840
841
842
843
844
      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.
845
846
Qed.

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