diff options
Diffstat (limited to 'scheduling/RTLpathLivegen.v')
| -rw-r--r-- | scheduling/RTLpathLivegen.v | 325 |
1 files changed, 0 insertions, 325 deletions
diff --git a/scheduling/RTLpathLivegen.v b/scheduling/RTLpathLivegen.v deleted file mode 100644 index 9f646ad0..00000000 --- a/scheduling/RTLpathLivegen.v +++ /dev/null @@ -1,325 +0,0 @@ -(** Building a RTLpath program with liveness annotation. -*) - - -Require Import Coqlib. -Require Import Maps. -Require Import Lattice. -Require Import AST. -Require Import Op. -Require Import Registers. -Require Import Globalenvs Smallstep RTL RTLpath. -Require Import Bool Errors. -Require Import Program. - -Local Open Scope lazy_bool_scope. - -Local Open Scope option_monad_scope. - -Axiom build_path_map: RTL.function -> path_map. - -Extract Constant build_path_map => "RTLpathLivegenaux.build_path_map". - -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 exit_checker {A} (pm: path_map) (alive: Regset.t) (pc: node) (v:A): option A := - SOME path <- pm!pc IN - ASSERT Regset.subset path.(input_regs) alive IN - Some v. - -Lemma exit_checker_path_entry A (pm: path_map) (alive: Regset.t) (pc: node) (v:A) res: - exit_checker pm alive pc v = Some res -> path_entry pm pc. -Proof. - unfold exit_checker, path_entry. - inversion_SOME path; simpl; congruence. -Qed. - -Lemma exit_checker_res A (pm: path_map) (alive: Regset.t) (pc: node) (v:A) res: - exit_checker pm alive pc v = Some res -> v=res. -Proof. - unfold exit_checker, path_entry. - inversion_SOME path; try_simplify_someHyps. - inversion_ASSERT; try_simplify_someHyps. -Qed. - -Definition iinst_checker (pm: path_map) (alive: Regset.t) (i: instruction): option (Regset.t * node) := - match i with - | Inop pc' => Some (alive, pc') - | Iop op args dst pc' => - ASSERT list_mem args alive IN - Some (Regset.add dst alive, pc') - | Iload _ chunk addr args dst pc' => - ASSERT list_mem args alive IN - Some (Regset.add dst alive, pc') - | Istore chunk addr args src pc' => - ASSERT Regset.mem src alive IN - ASSERT list_mem args alive IN - Some (alive, pc') - | Icond cond args ifso ifnot _ => - ASSERT list_mem args alive IN - exit_checker pm alive ifso (alive, ifnot) - | _ => None - end. - - -Local Hint Resolve exit_checker_path_entry: core. - -Lemma iinst_checker_path_entry (pm: path_map) (alive: Regset.t) (i: instruction) res pc: - iinst_checker pm alive i = Some res -> - early_exit i = Some pc -> path_entry pm pc. -Proof. - destruct i; simpl; try_simplify_someHyps; subst. - inversion_ASSERT; try_simplify_someHyps. -Qed. - -Lemma iinst_checker_default_succ (pm: path_map) (alive: Regset.t) (i: instruction) res pc: - iinst_checker pm alive i = Some res -> - pc = snd res -> - default_succ i = Some pc. -Proof. - destruct i; simpl; try_simplify_someHyps; subst; - repeat (inversion_ASSERT); try_simplify_someHyps. - intros; exploit exit_checker_res; eauto. - intros; subst. simpl; auto. -Qed. - -Fixpoint ipath_checker (ps:nat) (f: RTL.function) (pm: path_map) (alive: Regset.t) (pc:node): option (Regset.t * node) := - match ps with - | O => Some (alive, pc) - | S p => - SOME i <- f.(fn_code)!pc IN - SOME res <- iinst_checker pm alive i IN - ipath_checker p f pm (fst res) (snd res) - end. - -Lemma ipath_checker_wellformed f pm ps: forall alive pc res, - ipath_checker ps f pm alive pc = Some res -> - wellformed_path f.(fn_code) pm 0 (snd res) -> - wellformed_path f.(fn_code) pm ps pc. -Proof. - induction ps; simpl; try_simplify_someHyps. - inversion_SOME i; inversion_SOME res'. - intros. eapply wf_internal_node; eauto. - * eapply iinst_checker_default_succ; eauto. - * intros; eapply iinst_checker_path_entry; eauto. -Qed. - - -Lemma ipath_checker_default_succ (f: RTLpath.function) path: forall alive pc res, - ipath_checker path f (fn_path f) alive pc = Some res - -> nth_default_succ (fn_code f) path pc = Some (snd res). -Proof. - induction path; simpl. - + try_simplify_someHyps. - + intros alive pc res. - inversion_SOME i; intros INST. - inversion_SOME res0; intros ICHK IPCHK. - rewrite INST. - erewrite iinst_checker_default_succ; eauto. -Qed. - -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. - -Fixpoint exit_list_checker (pm: path_map) (alive: Regset.t) (l: list node): bool := - match l with - | nil => true - | pc::l' => exit_checker pm alive pc tt &&& exit_list_checker pm alive 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 exit_list_checker_correct pm alive l pc: - exit_list_checker pm alive l = true -> List.In pc l -> exit_checker pm alive pc tt = Some tt. -Proof. - intros EXIT PC; induction l; intuition. - simpl in * |-. rewrite lazy_and_Some_tt_true in EXIT. - firstorder (subst; eauto). -Qed. - -Local Hint Resolve exit_list_checker_correct: core. - -Definition final_inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit := - match i with - | Icall sig ros args res pc' => - ASSERT list_mem args alive IN - ASSERT reg_sum_mem ros alive IN - exit_checker pm (Regset.add res por) pc' tt - | Itailcall sig ros args => - ASSERT list_mem args alive IN - ASSERT reg_sum_mem ros alive IN - Some tt - | Ibuiltin ef args res pc' => - ASSERT list_mem (params_of_builtin_args args) alive IN - exit_checker pm (reg_builtin_res res por) pc' tt - | Ijumptable arg tbl => - ASSERT Regset.mem arg alive IN - ASSERT exit_list_checker pm por tbl IN - Some tt - | Ireturn optarg => - ASSERT (reg_option_mem optarg) alive IN - Some tt - | _ => None - end. - -Lemma final_inst_checker_wellformed (c:code) pc (pm: path_map) (alive por: Regset.t) (i: instruction): - final_inst_checker pm alive por i = Some tt -> - c!pc = Some i -> wellformed_path c pm 0 pc. -Proof. - intros CHECK PC. eapply wf_last_node; eauto. - clear c pc PC. intros pc PC. - destruct i; simpl in * |- *; intuition (subst; eauto); - try (generalize CHECK; clear CHECK; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps). -Qed. - -Definition inst_checker (pm: path_map) (alive por: Regset.t) (i: instruction): option unit := - match iinst_checker pm alive i with - | Some res => - ASSERT Regset.subset por (fst res) IN - exit_checker pm por (snd res) tt - | _ => - ASSERT Regset.subset por alive IN - final_inst_checker pm alive por i - end. - -Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive por: Regset.t) (i: instruction): - inst_checker pm alive por i = Some tt -> - c!pc = Some i -> wellformed_path c pm 0 pc. -Proof. - unfold inst_checker. - destruct (iinst_checker pm alive i) as [[alive0 pc0]|] eqn: CHECK1; simpl. - - simpl; intros CHECK2 PC. eapply wf_last_node; eauto. - destruct i; simpl in * |- *; intuition (subst; eauto); - try (generalize CHECK2 CHECK1; clear CHECK1 CHECK2; try (inversion_SOME path); repeat inversion_ASSERT; try_simplify_someHyps). - intros PC CHECK1 CHECK2. - intros; exploit exit_checker_res; eauto. - intros X; inversion X. intros; subst; eauto. - - simpl; intros CHECK2 PC. eapply final_inst_checker_wellformed; eauto. - generalize CHECK2. clear CHECK2. inversion_ASSERT. try_simplify_someHyps. -Qed. - -Definition path_checker (f: RTL.function) pm (pc: node) (path:path_info): option unit := - SOME res <- ipath_checker (path.(psize)) f pm (path.(input_regs)) pc IN - SOME i <- f.(fn_code)!(snd res) IN - inst_checker pm (fst res) (path.(pre_output_regs)) i. - -Lemma path_checker_wellformed f pm pc path: - path_checker f pm pc path = Some tt -> wellformed_path (f.(fn_code)) pm (path.(psize)) pc. -Proof. - unfold path_checker. - inversion_SOME res. - inversion_SOME i. - intros; eapply ipath_checker_wellformed; eauto. - eapply inst_checker_wellformed; eauto. -Qed. - -Fixpoint list_path_checker f pm (l:list (node*path_info)): bool := - match l with - | nil => true - | (pc, path)::l' => - path_checker f pm pc path &&& list_path_checker f pm l' - end. - -Lemma list_path_checker_correct f pm l: - list_path_checker f pm l = true -> forall e, List.In e l -> path_checker f pm (fst e) (snd e) = Some tt. -Proof. - intros CHECKER e H; induction l as [|(pc & path) l]; intuition. - simpl in * |- *. rewrite lazy_and_Some_tt_true in CHECKER. intuition (subst; auto). -Qed. - -Definition function_checker (f: RTL.function) pm: bool := - pm!(f.(fn_entrypoint)) &&& list_path_checker f pm (PTree.elements pm). - -Lemma function_checker_correct f pm pc path: - function_checker f pm = true -> - pm!pc = Some path -> - path_checker f pm pc path = Some tt. -Proof. - unfold function_checker; rewrite lazy_and_Some_true. - intros (ENTRY & PATH) PC. - exploit list_path_checker_correct; eauto. - - eapply PTree.elements_correct; eauto. - - simpl; auto. -Qed. - -Lemma function_checker_wellformed_path_map f pm: - function_checker f pm = true -> wellformed_path_map f.(fn_code) pm. -Proof. - unfold wellformed_path_map. - intros; eapply path_checker_wellformed; eauto. - intros; eapply function_checker_correct; eauto. -Qed. - -Lemma function_checker_path_entry f pm: - function_checker f pm = true -> path_entry pm (f.(fn_entrypoint)). -Proof. - unfold function_checker; rewrite lazy_and_Some_true; - unfold path_entry. firstorder congruence. -Qed. - -Definition liveness_ok_function (f: function): Prop := - forall pc path, f.(fn_path)!pc = Some path -> path_checker f f.(fn_path) pc path = Some tt. - -Program Definition transf_function (f: RTL.function): { r: res function | forall f', r = OK f' -> liveness_ok_function f' /\ f'.(fn_RTL) = f } := - let pm := build_path_map f in - match function_checker f pm with - | true => OK {| fn_RTL := f; fn_path := pm |} - | false => Error(msg "RTLpathGen: function_checker failed") - end. -Obligation 1. - apply function_checker_path_entry; auto. -Qed. -Obligation 2. - apply function_checker_wellformed_path_map; auto. -Qed. -Obligation 3. - unfold liveness_ok_function; simpl; intros; intuition. - apply function_checker_correct; auto. -Qed. - -Definition transf_fundef (f: RTL.fundef) : res fundef := - transf_partial_fundef (fun f => ` (transf_function f)) f. - -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). - -Lemma transf_fundef_correct f f': - transf_fundef f = OK f' -> (liveness_ok_fundef f') /\ fundef_RTL f' = f. -Proof. - intros TRANSF; destruct f; simpl; monadInv TRANSF. - - destruct (transf_function f) as [res H]; simpl in * |- *; auto. - destruct (H _ EQ). - intuition subst; auto. apply liveness_ok_Internal; auto. - - intuition. apply liveness_ok_External; auto. -Qed. - -Definition transf_program (p: RTL.program) : res program := - transform_partial_program transf_fundef p. - |