diff options
Diffstat (limited to 'scheduling/BTL_Livecheck.v')
| -rw-r--r-- | scheduling/BTL_Livecheck.v | 690 |
1 files changed, 690 insertions, 0 deletions
diff --git a/scheduling/BTL_Livecheck.v b/scheduling/BTL_Livecheck.v new file mode 100644 index 00000000..d200b9bd --- /dev/null +++ b/scheduling/BTL_Livecheck.v @@ -0,0 +1,690 @@ +Require Import Coqlib Maps. +Require Import AST Integers Values Events Memory Globalenvs Smallstep Op Registers OptionMonad. +Require Import Errors RTL BTL BTLmatchRTL. + + +Local Open Scope lazy_bool_scope. + +Local Open Scope option_monad_scope. + +Fixpoint list_mem (rl: list reg) (alive: Regset.t) {struct rl}: bool := + match rl with + | nil => true + | r1 :: rs => Regset.mem r1 alive &&& list_mem rs alive + end. + +Definition reg_option_mem (or: option reg) (alive: Regset.t) := + match or with None => true | Some r => Regset.mem r alive end. + +Definition reg_sum_mem (ros: reg + ident) (alive: Regset.t) := + match ros with inl r => Regset.mem r alive | inr s => true end. + +(* NB: definition following [regmap_setres] in [RTL.step] semantics *) +Definition reg_builtin_res (res: builtin_res reg) (alive: Regset.t): Regset.t := + match res with + | BR r => Regset.add r alive + | _ => alive + end. + +Definition exit_checker (btl: code) (alive: Regset.t) (s: node): option unit := + SOME next <- btl!s IN + ASSERT Regset.subset next.(input_regs) alive IN + Some tt. + +Fixpoint exit_list_checker (btl: code) (alive: Regset.t) (l: list node): bool := + match l with + | nil => true + | s :: l' => exit_checker btl alive s &&& exit_list_checker btl alive l' + end. + +Definition final_inst_checker (btl: code) (alive: Regset.t) (fin: final): option unit := + match fin with + | Bgoto s => + exit_checker btl alive s + | Breturn oreg => + ASSERT reg_option_mem oreg alive IN Some tt + | Bcall _ ros args res s => + ASSERT list_mem args alive IN + ASSERT reg_sum_mem ros alive IN + exit_checker btl (Regset.add res alive) s + | Btailcall _ ros args => + ASSERT list_mem args alive IN + ASSERT reg_sum_mem ros alive IN Some tt + | Bbuiltin _ args res s => + ASSERT list_mem (params_of_builtin_args args) alive IN + exit_checker btl (reg_builtin_res res alive) s + | Bjumptable arg tbl => + ASSERT Regset.mem arg alive IN + ASSERT exit_list_checker btl alive tbl IN Some tt + end. + +(* This definition is the meet (infimum) subset of alive registers, + used for conditions by the below checker. + A None argument represents the neutral element for intersection. *) +Definition meet (o1 o2: option Regset.t): option Regset.t := + match o1, o2 with + | None, _ => o2 + | _, None => o1 + | Some alive1, Some alive2 => Some (Regset.inter alive1 alive2) + end. + +Fixpoint body_checker (btl: code) (ib: iblock) (alive: Regset.t): option (option Regset.t) := + match ib with + | Bseq ib1 ib2 => + SOME oalive1 <- body_checker btl ib1 alive IN + SOME alive1 <- oalive1 IN + body_checker btl ib2 alive1 + | Bnop _ => Some (Some alive) + | Bop _ args dest _ => + ASSERT list_mem args alive IN + Some (Some (Regset.add dest alive)) + | Bload _ _ _ args dest _ => + ASSERT list_mem args alive IN + Some (Some (Regset.add dest alive)) + | Bstore _ _ args src _ => + ASSERT Regset.mem src alive IN + ASSERT list_mem args alive IN + Some (Some alive) + | Bcond _ args ib1 ib2 _ => + ASSERT list_mem args alive IN + SOME oalive1 <- body_checker btl ib1 alive IN + SOME oalive2 <- body_checker btl ib2 alive IN + Some (meet oalive1 oalive2) + | BF fin _ => + SOME _ <- final_inst_checker btl alive fin IN + Some None + end. + +(* This definition simply convert the result in an option unit *) +Definition iblock_checker (btl: code) (ib: iblock) (alive: Regset.t): option unit := + SOME _ <- body_checker btl ib alive IN Some tt. + +Fixpoint list_iblock_checker (btl: code) (l: list (node*iblock_info)): bool := + match l with + | nil => true + | (_, ibf) :: l' => iblock_checker btl ibf.(entry) ibf.(input_regs) &&& list_iblock_checker btl l' + end. + +Lemma lazy_and_Some_true A (o: option A) (b: bool): o &&& b = true <-> (exists v, o = Some v) /\ b = true. +Proof. + destruct o; simpl; intuition. + - eauto. + - firstorder. try_simplify_someHyps. +Qed. + +Lemma lazy_and_Some_tt_true (o: option unit) (b: bool): o &&& b = true <-> o = Some tt /\ b = true. +Proof. + intros; rewrite lazy_and_Some_true; firstorder. + destruct x; auto. +Qed. + +Lemma list_iblock_checker_correct btl l: + list_iblock_checker btl l = true -> + forall e, List.In e l -> iblock_checker btl (snd e).(entry) (snd e).(input_regs) = Some tt. +Proof. + intros CHECKER e H; induction l as [|(n & ibf) l]; intuition. + simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto). +Qed. + +Definition liveness_checker_bool (f: BTL.function): bool := + f.(fn_code)!(f.(fn_entrypoint)) &&& list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)). + +Definition liveness_checker (f: BTL.function): res unit := + match liveness_checker_bool f with + | true => OK tt + | false => Error (msg "BTL_Livecheck: liveness_checker failed") + end. + +Lemma decomp_liveness_checker f: + liveness_checker f = OK tt -> + exists ibf, f.(fn_code)!(f.(fn_entrypoint)) = Some ibf /\ + list_iblock_checker f.(fn_code) (PTree.elements f.(fn_code)) = true. +Proof. + intros LIVE; unfold liveness_checker in LIVE. + destruct liveness_checker_bool eqn:EQL; try congruence. + clear LIVE. unfold liveness_checker_bool in EQL. + rewrite lazy_and_Some_true in EQL; destruct EQL as [[ibf ENTRY] LIST]. + eexists; split; eauto. +Qed. + +Lemma liveness_checker_correct f n ibf: + liveness_checker f = OK tt -> + f.(fn_code)!n = Some ibf -> + iblock_checker f.(fn_code) ibf.(entry) ibf.(input_regs) = Some tt. +Proof. + intros LIVE PC. + apply decomp_liveness_checker in LIVE; destruct LIVE as [ibf' [ENTRY LIST]]. + exploit list_iblock_checker_correct; eauto. + - eapply PTree.elements_correct; eauto. + - simpl; auto. +Qed. + +Lemma liveness_checker_entrypoint f: + liveness_checker f = OK tt -> + f.(fn_code)!(f.(fn_entrypoint)) <> None. +Proof. + intros LIVE; apply decomp_liveness_checker in LIVE; destruct LIVE as [ibf' [ENTRY LIST]]. + unfold not; intros CONTRA. congruence. +Qed. + +Definition liveness_ok_function (f: BTL.function): Prop := liveness_checker f = OK tt. + +Inductive liveness_ok_fundef: fundef -> Prop := + | liveness_ok_Internal f: liveness_ok_function f -> liveness_ok_fundef (Internal f) + | liveness_ok_External ef: liveness_ok_fundef (External ef). + + +Local Notation ext alive := (fun r => Regset.In r alive). + +Definition ext_opt (oalive: option Regset.t): Regset.elt -> Prop := + match oalive with + | Some alive => ext alive + | None => fun _ => True + end. + +Lemma ext_opt_meet: forall r oalive1 oalive2, + ext_opt (meet oalive1 oalive2) r -> + ext_opt oalive1 r /\ ext_opt oalive2 r. +Proof. + intros. destruct oalive1, oalive2; + simpl in *; intuition. + eapply Regset.inter_1; eauto. + eapply Regset.inter_2; eauto. +Qed. + +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. + +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. + +Definition eqlive_reg (alive: Regset.elt -> Prop) (rs1 rs2: regset): Prop := + forall r, (alive r) -> rs1#r = rs2#r. + +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_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. + +Inductive eqlive_stackframes: stackframe -> stackframe -> Prop := + | eqlive_stackframes_intro ibf res f sp pc rs1 rs2 + (LIVE: liveness_ok_function f) + (ENTRY: f.(fn_code)!pc = Some ibf) + (EQUIV: forall v, eqlive_reg (ext ibf.(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 + ibf st1 st2 f sp pc rs1 rs2 m + (STACKS: list_forall2 eqlive_stackframes st1 st2) + (LIVE: liveness_ok_function f) + (PATH: f.(fn_code)!pc = Some ibf) + (EQUIV: eqlive_reg (ext ibf.(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 FSEM_SIMULATES_CFGSEM. + +Variable prog: BTL.program. + +Let ge := Genv.globalenv prog. + +Hypothesis all_fundef_liveness_ok: forall b f, Genv.find_funct_ptr ge b = Some f -> liveness_ok_fundef f. + +Local Hint Constructors eqlive_stackframes eqlive_states final_step list_forall2 step: core. + +Lemma eqlive_reg_update_gso alive rs1 rs2 res r: forall v : val, + eqlive_reg (ext alive) rs1 # res <- v rs2 # res <- v -> + res <> r -> Regset.In r alive -> + rs1 # r = rs2 # r. +Proof. + intros v REGS NRES INR. unfold eqlive_reg in REGS. + specialize REGS with r. apply REGS in INR. + rewrite !Regmap.gso in INR; auto. +Qed. + +Lemma find_funct_liveness_ok v fd: + Genv.find_funct ge 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 ge 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 ge 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 ge ros rs1 = find_function ge ros rs2. +Proof. + intros EQLIVE. + destruct ros; simpl; auto. + intros H; erewrite (EQLIVE r); eauto. +Qed. + +Lemma exit_checker_eqlive (btl: code) (alive: Regset.t) (pc: node) rs1 rs2: + exit_checker btl alive pc = Some tt -> + eqlive_reg (ext alive) rs1 rs2 -> + exists ibf, btl!pc = Some ibf /\ eqlive_reg (ext ibf.(input_regs)) rs1 rs2. +Proof. + unfold exit_checker. + inversion_SOME next. + inversion_ASSERT. try_simplify_someHyps. + repeat (econstructor; eauto). + intros; eapply eqlive_reg_monotonic; eauto. + intros; exploit Regset.subset_2; eauto. +Qed. + +Lemma exit_list_checker_eqlive (btl: code) (alive: Regset.t) (tbl: list node) rs1 rs2 pc: forall n, + exit_list_checker btl alive tbl = true -> + eqlive_reg (ext alive) rs1 rs2 -> + list_nth_z tbl n = Some pc -> + exists ibf, btl!pc = Some ibf /\ eqlive_reg (ext ibf.(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 exit_checker_eqlive_update (btl: code) (alive: Regset.t) (pc: node) r rs1 rs2: + exit_checker btl (Regset.add r alive) pc = Some tt -> + eqlive_reg (ext alive) rs1 rs2 -> + exists ibf, btl!pc = Some ibf /\ (forall v, eqlive_reg (ext ibf.(input_regs)) (rs1 # r <- v) (rs2 # r <- v)). +Proof. + unfold exit_checker. + inversion_SOME next. + 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. + +Lemma exit_checker_eqlive_builtin_res (btl: code) (alive: Regset.t) (pc: node) rs1 rs2 (res:builtin_res reg): + exit_checker btl (reg_builtin_res res alive) pc = Some tt -> + eqlive_reg (ext alive) rs1 rs2 -> + exists ibf, btl!pc = Some ibf /\ (forall vres, eqlive_reg (ext ibf.(input_regs)) (regmap_setres res vres rs1) (regmap_setres res vres rs2)). +Proof. + destruct res; simpl. + - intros; exploit exit_checker_eqlive_update; eauto. + - intros; exploit exit_checker_eqlive; eauto. + intros (ibf & PC & REGS). + eexists; intuition eauto. + - intros; exploit exit_checker_eqlive; eauto. + intros (ibf & PC & REGS). + eexists; intuition eauto. +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 tr_inputs_eqlive_None f pc tbl ibf rs1 rs2 + (PC: (fn_code f) ! pc = Some ibf) + (REGS: eqlive_reg (ext (input_regs ibf)) rs1 rs2) + :eqlive_reg (ext (input_regs ibf)) (tid f (pc :: tbl) None rs1) + (tr_inputs f (pc :: tbl) None rs2). +Proof. + unfold eqlive_reg. intros r INR. + unfold tid. rewrite tr_inputs_get. + simpl. rewrite PC. + exploit Regset.union_3. eapply INR. + intros INRU. eapply Regset.mem_1 in INRU. + erewrite INRU; eauto. +Qed. + +Lemma tr_inputs_eqlive_list_None tbl: forall f pc n alive ibf rs1 rs2 + (REGS1: eqlive_reg (ext alive) rs1 rs2) + (EXIT_LIST: exit_list_checker (fn_code f) alive tbl = true) + (LIST: list_nth_z tbl n = Some pc) + (PC: (fn_code f) ! pc = Some ibf) + (REGS2: eqlive_reg (ext (input_regs ibf)) rs1 rs2), + eqlive_reg (ext (input_regs ibf)) (tid f tbl None rs1) + (tr_inputs f tbl None rs2). +Proof. + induction tbl as [| pc' tbl IHtbl]; try_simplify_someHyps. + autodestruct; try_simplify_someHyps. + - intros; eapply tr_inputs_eqlive_None; eauto. + - rewrite lazy_and_Some_tt_true in EXIT_LIST. + destruct EXIT_LIST as [EXIT EXIT_REM]. + intros. unfold eqlive_reg. intros r INR. + exploit (IHtbl f pc (Z.pred n) alive ibf rs1 rs2); eauto. + unfold tid. rewrite !tr_inputs_get. + exploit exit_checker_eqlive; eauto. + intros (ibf' & PC' & REGS3). + simpl; rewrite PC'. autodestruct. + + intro INRU. apply Regset.mem_2 in INRU. + intros EQR. eapply Regset.union_2 in INRU. + eapply Regset.mem_1 in INRU. erewrite INRU; auto. + + intros. autodestruct. + rewrite (REGS2 r); auto. +Qed. + +Lemma tr_inputs_eqlive_update f pc ibf rs1 rs2 res + (PC: (fn_code f) ! pc = Some ibf) + :forall (v: val) + (REGS: eqlive_reg (ext (input_regs ibf)) rs1 # res <- v rs2 # res <- v), + eqlive_reg (ext (input_regs ibf)) + (tid f (pc :: nil) (Some res) rs1) # res <- v + (tr_inputs f (pc :: nil) (Some res) rs2) # res <- v. +Proof. + intros. apply eqlive_reg_update. + unfold eqlive_reg. intros r (NRES & INR). + unfold tid. rewrite tr_inputs_get. + simpl. rewrite PC. assert (NRES': res <> r) by auto. + clear NRES. exploit Regset.union_3. eapply INR. + intros INRU. exploit Regset.remove_2; eauto. + intros INRU_RES. eapply Regset.mem_1 in INRU_RES. + erewrite INRU_RES. eapply eqlive_reg_update_gso; eauto. +Qed. + +Local Hint Resolve tr_inputs_eqlive_None tr_inputs_eqlive_update: core. +Lemma cfgsem2fsem_finalstep_simu sp f stk1 stk2 s t fin alive rs1 m rs2 + (FSTEP: final_step tid ge stk1 f sp rs1 m fin t s) + (LIVE: liveness_ok_function f) + (REGS: eqlive_reg (ext alive) rs1 rs2) + (FCHK: final_inst_checker (fn_code f) alive fin = Some tt) + (STACKS: list_forall2 eqlive_stackframes stk1 stk2) + :exists s', + final_step tr_inputs ge stk2 f sp rs2 m fin t s' + /\ eqlive_states s s'. +Proof. + destruct FSTEP; try_simplify_someHyps; repeat inversion_ASSERT; intros. + - (* Bgoto *) + eexists; split. + + econstructor; eauto. + + exploit exit_checker_eqlive; eauto. + intros (ibf & PC & REGS'). + econstructor; eauto. + - (* Breturn *) + eexists; split. econstructor; eauto. + destruct or; simpl in *; + try erewrite (REGS r); eauto. + - (* Bcall *) + exploit exit_checker_eqlive_update; eauto. + intros (ibf & PC & REGS'). + eexists; split. + + econstructor; eauto. + erewrite <- find_function_eqlive; eauto. + + erewrite eqlive_reg_listmem; eauto. + eapply eqlive_states_call; eauto. + eapply find_function_liveness_ok; eauto. + - (* Btailcall *) + eexists; split. + + econstructor; eauto. + erewrite <- find_function_eqlive; eauto. + + erewrite eqlive_reg_listmem; eauto. + eapply eqlive_states_call; eauto. + eapply find_function_liveness_ok; eauto. + - (* Bbuiltin *) + exploit exit_checker_eqlive_builtin_res; eauto. + intros (ibf & PC & REGS'). + eexists; split. + + econstructor; eauto. + eapply eqlive_eval_builtin_args; eauto. + intros; eapply list_mem_correct; eauto. + + repeat (econstructor; simpl; eauto). + unfold regmap_setres. destruct res; simpl in *; eauto. + - (* Bjumptable *) + exploit exit_list_checker_eqlive; eauto. + intros (ibf & PC & REGS'). + eexists; split. + + econstructor; eauto. + erewrite <- REGS; eauto. + + repeat (econstructor; simpl; eauto). + apply (tr_inputs_eqlive_list_None tbl f pc' (Int.unsigned n) alive ibf rs1 rs2); + auto. +Qed. + +Lemma cfgsem2fsem_ibistep_simu_None sp f ib: forall rs1 m rs1' m' + (ISTEP: iblock_istep ge sp rs1 m ib rs1' m' None) + alive1 oalive2 rs2 (REGS: eqlive_reg (ext alive1) rs1 rs2) + (BDY: body_checker (fn_code f) ib alive1 = Some (oalive2)), + exists rs2', + iblock_istep_run ge sp ib rs2 m = Some (out rs2' m' None) + /\ eqlive_reg (ext_opt oalive2) rs1' rs2'. +Proof. + induction ib; intros; try_simplify_someHyps; + repeat inversion_ASSERT; intros; inv ISTEP. + - (* Bnop *) + inv BDY; eauto. + - (* Bop *) + erewrite <- eqlive_reg_listmem; eauto. + try_simplify_someHyps; intros. + repeat econstructor. + apply eqlive_reg_update. + eapply eqlive_reg_monotonic; eauto. + intros r0; rewrite regset_add_spec. + intuition. + - (* Bload *) + erewrite <- eqlive_reg_listmem; eauto. + try_simplify_someHyps; intros. + destruct trap; inv LOAD; + rewrite EVAL, LOAD0 || (autodestruct; try rewrite LOAD0; auto). + all: + repeat econstructor; + apply eqlive_reg_update; + eapply eqlive_reg_monotonic; eauto; + intros r0; rewrite regset_add_spec; + intuition. + - (* Bstore *) + erewrite <- eqlive_reg_listmem; eauto. + rewrite <- (REGS src); auto. + try_simplify_someHyps; intros. + rewrite STORE; eauto. + - (* Bseq continue *) + destruct (body_checker _ _ _) eqn:BDY1 in BDY; try discriminate. + generalize BDY; clear BDY. + inversion_SOME aliveMid; intros OALIVE BDY2. inv OALIVE. + exploit IHib1; eauto. + intros (rs2' & ISTEP1 & REGS1). rewrite ISTEP1; simpl. + eapply IHib2; eauto. + - (* Bcond *) + generalize BDY; clear BDY. + inversion_SOME oaliveSo; inversion_SOME oaliveNot; intros BDY1 BDY2 JOIN. + erewrite <- eqlive_reg_listmem; eauto. + rewrite EVAL. + destruct b; [ exploit IHib1; eauto | exploit IHib2; eauto]. + all: + intros (rs2' & ISTEP1 & REGS1); + econstructor; split; eauto; inv JOIN; + eapply eqlive_reg_monotonic; eauto; + intros r EXTM; apply ext_opt_meet in EXTM; intuition. +Qed. + +Lemma cfgsem2fsem_ibistep_simu_Some sp f stk1 stk2 ib: forall s t rs1 m rs1' m' fin + (ISTEP: iblock_istep ge sp rs1 m ib rs1' m' (Some fin)) + (FSTEP: final_step tid ge stk1 f sp rs1' m' fin t s) + alive1 oalive2 rs2 (REGS: eqlive_reg (ext alive1) rs1 rs2) + (BDY: body_checker (fn_code f) ib alive1 = Some (oalive2)) + (LIVE: liveness_ok_function f) + (STACKS: list_forall2 eqlive_stackframes stk1 stk2), + exists rs2' s', + iblock_istep_run ge sp ib rs2 m = Some (out rs2' m' (Some fin)) + /\ final_step tr_inputs ge stk2 f sp rs2' m' fin t s' + /\ eqlive_states s s'. +Proof. + induction ib; simpl; try_simplify_someHyps; + repeat inversion_ASSERT; intros; inv ISTEP. + - (* BF *) + generalize BDY; clear BDY. + inversion_SOME x; try_simplify_someHyps; intros FCHK. + destruct x; exploit cfgsem2fsem_finalstep_simu; eauto. + intros (s2 & FSTEP' & STATES); eauto. + - (* Bseq stop *) + destruct (body_checker _ _ _) eqn:BDY1 in BDY; try discriminate. + generalize BDY; clear BDY. + inversion_SOME aliveMid. intros OALIVE BDY2. inv OALIVE. + exploit IHib1; eauto. intros (rs2' & s' & ISTEP1 & FSTEP1 & STATES). + rewrite ISTEP1; simpl. + do 2 eexists; intuition eauto. + - (* Bseq continue *) + destruct (body_checker _ _ _) eqn:BDY1 in BDY; try discriminate. + generalize BDY; clear BDY. + inversion_SOME aliveMid; intros OALIVE BDY2. inv OALIVE. + exploit cfgsem2fsem_ibistep_simu_None; eauto. + intros (rs2' & ISTEP1 & REGS'). rewrite ISTEP1; simpl; eauto. + - (* Bcond *) + generalize BDY; clear BDY. + inversion_SOME oaliveSo; inversion_SOME oaliveNot; intros BDY1 BDY2 JOIN. + erewrite <- eqlive_reg_listmem; eauto. rewrite EVAL. + destruct b; eauto. +Qed. + +Lemma cfgsem2fsem_ibstep_simu stk1 stk2 f sp rs1 m rs2 ibf pc s1 t: + iblock_step tid (Genv.globalenv prog) stk1 f sp rs1 m ibf.(entry) t s1 -> + list_forall2 eqlive_stackframes stk1 stk2 -> + eqlive_reg (ext (input_regs ibf)) rs1 rs2 -> + liveness_ok_function f -> + (fn_code f) ! pc = Some ibf -> + exists s2 : state, + iblock_step tr_inputs (Genv.globalenv prog) stk2 f sp rs2 m ibf.(entry) t s2 /\ + eqlive_states s1 s2. +Proof. + intros STEP STACKS EQLIVE LIVE PC. + assert (CHECKER: liveness_ok_function f) by auto. + unfold liveness_ok_function in CHECKER. + apply decomp_liveness_checker in CHECKER; destruct CHECKER as [ibf' [ENTRY LIST]]. + eapply PTree.elements_correct in PC as PCIN. + eapply list_iblock_checker_correct in LIST as IBC; eauto. + unfold iblock_checker in IBC. generalize IBC; clear IBC. + inversion_SOME alive; intros BODY _. + destruct STEP as (rs1' & m1' & fin' & ISTEP & FSTEP). + exploit cfgsem2fsem_ibistep_simu_Some; eauto. + intros (rs2' & s' & ISTEP' & FSTEP' & REGS). + rewrite <- iblock_istep_run_equiv in ISTEP'. clear ISTEP. + unfold iblock_step. repeat eexists; eauto. +Qed. + +Local Hint Constructors step: core. + +Lemma cfgsem2fsem_step_simu s1 s1' t s2: + step tid (Genv.globalenv prog) s1 t s1' -> + eqlive_states s1 s2 -> + exists s2' : state, + step tr_inputs (Genv.globalenv prog) s2 t s2' /\ + eqlive_states s1' s2'. +Proof. + destruct 1 as [stack ibf f sp n rs m t s ENTRY STEP | | | ]; intros STATES. + - (* iblock *) + inv STATES; simplify_someHyps. + intros. + exploit cfgsem2fsem_ibstep_simu; eauto. + intros (s2 & STEP2 & EQUIV2). + eexists; split; eauto. + - (* function internal *) + inv STATES; inv LIVE. + apply liveness_checker_entrypoint in H0 as ENTRY. + destruct ((fn_code f) ! (fn_entrypoint f)) eqn:EQENTRY; try congruence; eauto. + eexists; split; repeat econstructor; eauto. + - (* function external *) + inv STATES; inv LIVE; eexists; split; econstructor; eauto. + - (* return *) + inv STATES. + 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. + +Theorem cfgsem2fsem: forward_simulation (cfgsem prog) (fsem prog). +Proof. + eapply forward_simulation_step with eqlive_states; simpl; eauto. + - destruct 1, f; intros; eexists; intuition eauto; + repeat (econstructor; eauto). + - intros s1 s2 r STATES FINAL; destruct FINAL. + inv STATES; inv STACKS; constructor. + - intros. eapply cfgsem2fsem_step_simu; eauto. +Qed. + +End FSEM_SIMULATES_CFGSEM. + + |