diff options
Diffstat (limited to 'scheduling/RTLpathLivegen.v')
| -rw-r--r-- | scheduling/RTLpathLivegen.v | 290 |
1 files changed, 290 insertions, 0 deletions
diff --git a/scheduling/RTLpathLivegen.v b/scheduling/RTLpathLivegen.v new file mode 100644 index 00000000..1f0ebe3c --- /dev/null +++ b/scheduling/RTLpathLivegen.v @@ -0,0 +1,290 @@ +(** 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. + +(* FIXME - what about trap? *) +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 (* TODO jumptable ? *) + 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. + +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 inst_checker (pm: path_map) (alive: 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 alive) 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 alive) pc' tt + | Ijumptable arg tbl => + ASSERT Regset.mem arg alive IN + ASSERT exit_list_checker pm alive tbl IN + Some tt + | Ireturn optarg => + ASSERT (reg_option_mem optarg) alive IN + Some tt + | _ => + SOME res <- iinst_checker pm alive i IN + exit_checker pm (fst res) (snd res) tt + end. + +Lemma inst_checker_wellformed (c:code) pc (pm: path_map) (alive: Regset.t) (i: instruction): + inst_checker pm alive 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). + intros X; exploit exit_checker_res; eauto. + clear X. intros; subst; eauto. +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) 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. + |