diff options
Diffstat (limited to 'scheduling/RTLpathLivegenproof.v')
| -rw-r--r-- | scheduling/RTLpathLivegenproof.v | 760 |
1 files changed, 760 insertions, 0 deletions
diff --git a/scheduling/RTLpathLivegenproof.v b/scheduling/RTLpathLivegenproof.v new file mode 100644 index 00000000..b02400bf --- /dev/null +++ b/scheduling/RTLpathLivegenproof.v @@ -0,0 +1,760 @@ +(** Proofs of the liveness properties from the liveness checker of RTLpathLivengen. +*) + + +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. +Require Import Bool Errors Linking Values Events. +Require Import Program. + +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. + all: erewrite eval_addressing_preserved; eauto. + + (* Iload notrap1 *) eapply exec_Iload_notrap1; eauto. + all: erewrite eval_addressing_preserved; eauto. + + (* Iload notrap2 *) eapply exec_Iload_notrap2; eauto. + all: erewrite eval_addressing_preserved; eauto. + + (* Istore *) eapply exec_Istore; eauto. + all: 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. + +Local Open Scope lazy_bool_scope. +Local Open Scope option_monad_scope. + +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. + +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. + +Local Hint Resolve Regset.mem_2 Regset.subset_2: core. + +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. + +Record eqlive_istate alive (st1 st2: istate): Prop := + { 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) }. + +Lemma iinst_checker_eqlive ge sp pm alive i res rs1 rs2 m st1: + eqlive_reg (ext alive) rs1 rs2 -> + iinst_checker pm alive i = Some res -> + istep ge i sp rs1 m = Some st1 -> + exists st2, istep ge i sp rs2 m = Some st2 /\ eqlive_istate (ext (fst res)) st1 st2. +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. + destruct t. + inversion_SOME a0. intros EVAL. + erewrite <- eqlive_reg_listmem; eauto. + try_simplify_someHyps. + inversion_SOME v; try_simplify_someHyps. + repeat (econstructor; simpl; eauto). + 2: + erewrite <- (eqlive_reg_listmem _ _ rs1 rs2); eauto; + destruct (eval_addressing _ _ _ _); + try destruct (Memory.Mem.loadv _ _ _); + try (intros; inv H1; repeat (econstructor; simpl; eauto)). + all: + eapply eqlive_reg_update; + eapply eqlive_reg_monotonic; eauto; + intros r0; rewrite regset_add_spec; + intuition. + - (* 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: + iinst_checker pm alive i = Some res -> + istep ge i sp rs m = Some st -> + icontinue st = true -> + (snd res)=(ipc st). +Proof. + intros; exploit iinst_checker_default_succ; eauto. + erewrite istep_normal_exit; eauto. + congruence. +Qed. + +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 -> + eqlive_reg (ext alive) rs1 rs2 -> + 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 -> + 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. +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. + 1-3: explore_destruct; simpl; try_simplify_someHyps; repeat (inversion_ASSERT || inversion_SOME b); try_simplify_someHyps; try congruence. + (* 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 -> + icontinue st1 = true -> + exists st2, isteps ge ps f sp rs2 m pc = Some st2 /\ eqlive_istate (ext (fst res)) st1 st2. +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. + destruct 1 as (st2 & ISTEP & [CONT PC RS MEM]). + try_simplify_someHyps. + rewrite <- CONT, <- MEM, <- PC. + destruct (icontinue st0) eqn:CONT'. + * intros; exploit iinst_checker_istep_continue; eauto. + rewrite <- PC; intros X; rewrite X in * |-. eauto. + * try_simplify_someHyps. + congruence. +Qed. + +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 -> + icontinue st = true -> + (snd res)=(ipc st). +Proof. + induction ps as [|ps]; simpl; try_simplify_someHyps. + inversion_SOME i; try_simplify_someHyps. + inversion_SOME res0. + inversion_SOME st0. + destruct (icontinue st0) eqn:CONT'. + - 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 -> + 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. +Proof. + induction ps as [|ps]; simpl; try_simplify_someHyps; try congruence. + inversion_SOME i; try_simplify_someHyps. + inversion_SOME res0. + inversion_SOME st0. + intros. + destruct (icontinue st0) eqn:CONT'; try_simplify_someHyps; intros. + * 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. + +Inductive eqlive_stackframes: stackframe -> stackframe -> Prop := + | eqlive_stackframes_intro path res f sp pc rs1 rs2 + (LIVE: liveness_ok_function f) + (PATH: f.(fn_path)!pc = Some path) + (EQUIV: forall v, eqlive_reg (ext path.(input_regs)) (rs1 # res <- v) (rs2 # res <- v)): + eqlive_stackframes (Stackframe res f sp pc rs1) (Stackframe res f sp pc rs2). + +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) + (LIVE: liveness_ok_function f) + (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 + (LIVE: liveness_ok_fundef f) + (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). + + +Section LivenessProperties. + +Variable prog: program. + +Let pge := Genv.globalenv prog. +Let ge := Genv.globalenv (RTLpath.transf_program prog). + +Hypothesis all_fundef_liveness_ok: forall b f, + Genv.find_funct_ptr pge b = Some f -> + liveness_ok_fundef f. + +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: + find_function pge ros rs = Some f -> liveness_ok_fundef f. +Proof. + destruct ros as [r|i]; simpl. + - intros; eapply find_funct_liveness_ok; eauto. + - destruct (Genv.find_symbol pge i); try congruence. + eapply all_fundef_liveness_ok; eauto. +Qed. + +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. + +Lemma final_inst_checker_from_iinst_checker i sp rs m st pm alive por: + istep ge i sp rs m = Some st -> + final_inst_checker pm alive por i = None. +Proof. + destruct i; simpl; try congruence. +Qed. + +(* is it useful ? +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. + unfold inst_checker. + destruct (iinst_checker pm alive i); simpl; auto. + 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. + +Local Hint Resolve in_or_app: local. +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 -> + (forall r, List.In r (params_of_builtin_args args) -> alive r) -> + Events.eval_builtin_args ge (fun r => rs2 # r) sp m args vargs. +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. + +Lemma exit_checker_eqlive_builtin_res (pm: path_map) (alive: Regset.t) (pc: node) rs1 rs2 (res:builtin_res reg): + exit_checker pm (reg_builtin_res res alive) pc tt = Some tt -> + 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)). +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. + +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. + +Lemma final_inst_checker_eqlive (f: function) sp alive por pc i rs1 rs2 m stk1 stk2 t s1: + list_forall2 eqlive_stackframes stk1 stk2 -> + eqlive_reg (ext alive) rs1 rs2 -> + Regset.Subset por alive -> + liveness_ok_function f -> + (fn_code f) ! pc = Some i -> + path_last_step ge pge stk1 f sp pc rs1 m t s1 -> + final_inst_checker (fn_path f) alive por 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 SUB LIVENESS PC; + destruct 1 as [i' sp pc rs1 m st1| + sp pc rs1 m sig ros args res pc' fd| + st1 pc rs1 m sig ros args fd m'| + sp pc rs1 m ef args res pc' vargs t vres m'| + sp pc rs1 m arg tbl n pc' | + st1 pc rs1 m optr m']; + try_simplify_someHyps. + + (* istate *) + intros PC ISTEP. erewrite final_inst_checker_from_iinst_checker; eauto. + congruence. + + (* Icall *) + repeat inversion_ASSERT. intros. + exploit exit_checker_eqlive_ext1; eauto. + eapply eqlive_reg_monotonic; 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. + eapply find_function_liveness_ok; eauto. + repeat (econstructor; eauto). + + (* Itailcall *) + 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. + eapply find_function_liveness_ok; eauto. + + (* Ibuiltin *) + repeat inversion_ASSERT. intros. + exploit exit_checker_eqlive_builtin_res; eauto. + eapply eqlive_reg_monotonic; 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). + + (* Ijumptable *) + repeat inversion_ASSERT. intros. + exploit exit_list_checker_eqlive; eauto. + eapply eqlive_reg_monotonic; eauto. + intros (path & PATH & EQLIVE2). + eexists; split. + - eapply exec_Ijumptable; eauto. + erewrite <- EQLIVE; eauto. + - repeat (econstructor; simpl; eauto). + + (* 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. +Qed. + +Lemma inst_checker_eqlive (f: function) sp alive por pc i rs1 rs2 m stk1 stk2 t s1: + 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 por i = Some tt -> + 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. + intros IICHECKER PC ISTEP. inversion_ASSERT. + 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. + apply Regset.subset_2 in H. + exploit exit_checker_eqlive; eauto. + eapply eqlive_reg_monotonic; 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. + + inversion_ASSERT. + intros; exploit final_inst_checker_eqlive; eauto. +Qed. + +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 -> + eqlive_reg (ext (input_regs path)) rs1 rs2 -> + liveness_ok_function f -> + (fn_path f) ! pc = Some path -> + exists s2, path_step ge pge (psize path) stk2 f sp rs2 m pc t s2 /\ eqlive_states s1 s2. +Proof. + intros STEP STACKS EQLIVE LIVE PC. + unfold liveness_ok_function in LIVE. + exploit LIVE; eauto. + unfold path_checker. + inversion_SOME res; (* destruct res as [alive pc']. *) intros ICHECK. (* simpl. *) + inversion_SOME i; intros PC'. + destruct STEP as [st ISTEPS CONT|]. + - (* 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. + +Theorem step_eqlive t s1 s1' s2: + step ge pge s1 t s1' -> + eqlive_states s1 s2 -> + exists s2', step ge pge s2 t s2' /\ eqlive_states s1' s2'. +Proof. + destruct 1 as [path stack f sp rs m pc t s PATH STEP | | | ]. + - intros EQLIVE; inv EQLIVE; simplify_someHyps. + intro PATH. + 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). + eexists; split. + * eapply exec_function_internal; eauto. + * eapply eqlive_states_intro; eauto. + 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. +Qed. + +End LivenessProperties. |