diff options
Diffstat (limited to 'scheduling/RTLpathLivegenproof.v')
| -rw-r--r-- | scheduling/RTLpathLivegenproof.v | 760 |
1 files changed, 0 insertions, 760 deletions
diff --git a/scheduling/RTLpathLivegenproof.v b/scheduling/RTLpathLivegenproof.v deleted file mode 100644 index b02400bf..00000000 --- a/scheduling/RTLpathLivegenproof.v +++ /dev/null @@ -1,760 +0,0 @@ -(** 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. |