diff options
Diffstat (limited to 'mppa_k1c/abstractbb/DepTreeTheory.v')
-rw-r--r-- | mppa_k1c/abstractbb/DepTreeTheory.v | 365 |
1 files changed, 186 insertions, 179 deletions
diff --git a/mppa_k1c/abstractbb/DepTreeTheory.v b/mppa_k1c/abstractbb/DepTreeTheory.v index bf45d11a..6646d4f5 100644 --- a/mppa_k1c/abstractbb/DepTreeTheory.v +++ b/mppa_k1c/abstractbb/DepTreeTheory.v @@ -1,13 +1,13 @@ (** Dependency Trees of Abstract Basic Blocks -with a purely-functional-but-exponential equivalence test. +with a purely-functional-but-exponential test. *) Require Setoid. (* in order to rewrite <-> *) Require Export AbstractBasicBlocksDef. - +Require Import List. Module Type PseudoRegDictionary. @@ -39,12 +39,9 @@ Module DepTree (L: SeqLanguage) (Dict: PseudoRegDictionary with Module R:=L.LP.R Export L. Export LP. -Local Open Scope list. Section DEPTREE. -Variable ge: genv. - (** Dependency Trees of these "bblocks" NB: each tree represents the successive computations in one given resource @@ -54,102 +51,90 @@ NB: each tree represents the successive computations in one given resource Inductive tree := | Tname (x:R.t) | Top (o: op) (l: list_tree) - | Terase (new old:tree) (* assignment in the resource: [new] replaces [old] *) with list_tree := | Tnil: list_tree | Tcons (t:tree) (l:list_tree): list_tree . -Fixpoint tree_eval (t: tree) (m: mem): option value := +Fixpoint tree_eval (ge: genv) (t: tree) (m: mem): option value := match t with | Tname x => Some (m x) | Top o l => - match list_tree_eval l m with + match list_tree_eval ge l m with | Some v => op_eval ge o v | _ => None end - | Terase new old => - (* NB: we simply check whether the old computations has aborted *) - match tree_eval old m with - | Some _ => tree_eval new m - | _ => None - end end -with list_tree_eval (l: list_tree) (m: mem) {struct l}: option (list value) := +with list_tree_eval ge (l: list_tree) (m: mem) {struct l}: option (list value) := match l with | Tnil => Some nil | Tcons t l' => - match (tree_eval t m), (list_tree_eval l' m) with + match (tree_eval ge t m), (list_tree_eval ge l' m) with | Some v, Some lv => Some (v::lv) | _, _ => None end end. -Definition deps:= Dict.t tree. - -Definition deps_get (d:deps) x := +Definition deps_get (d:Dict.t tree) x := match Dict.get d x with | None => Tname x | Some t => t end. -Lemma set_spec_eq d x t: - deps_get (Dict.set d x t) x = t. -Proof. - unfold deps_get; rewrite Dict.set_spec_eq; simpl; auto. -Qed. - -Lemma set_spec_diff d x y t: - x <> y -> deps_get (Dict.set d x t) y = deps_get d y. -Proof. - unfold deps_get; intros; rewrite Dict.set_spec_diff; simpl; auto. -Qed. - -Lemma empty_spec x: deps_get Dict.empty x = Tname x. -Proof. - unfold deps_get; rewrite Dict.empty_spec; simpl; auto. -Qed. - -Hint Rewrite set_spec_eq empty_spec: dict_rw. - -Fixpoint exp_tree (e: exp) (d old: deps): tree := +Fixpoint exp_tree (e: exp) d old: tree := match e with | PReg x => deps_get d x | Op o le => Top o (list_exp_tree le d old) | Old e => exp_tree e old old end -with list_exp_tree (le: list_exp) (d old: deps): list_tree := +with list_exp_tree (le: list_exp) d old: list_tree := match le with | Enil => Tnil | Econs e le' => Tcons (exp_tree e d old) (list_exp_tree le' d old) | LOld le => list_exp_tree le old old end. -Definition failsafe (t: tree): bool := - match t with - | Tname x => true - | Top o Tnil => is_constant o - | _ => false - end. +Record deps:= {pre: genv -> mem -> Prop; post: Dict.t tree}. + +Coercion post: deps >-> Dict.t. + +Definition deps_eval ge (d: deps) x (m:mem) := + tree_eval ge (deps_get d x) m. + +Definition deps_set (d:deps) x (t:tree) := + {| pre:=(fun ge m => (deps_eval ge d x m) <> None /\ (d.(pre) ge m)); + post:=Dict.set d x t |}. + +Definition deps_empty := {| pre:=fun _ _ => True; post:=Dict.empty |}. + +Variable ge: genv. + +Lemma set_spec_eq d x t m: + deps_eval ge (deps_set d x t) x m = tree_eval ge t m. +Proof. + unfold deps_eval, deps_set, deps_get; simpl; rewrite Dict.set_spec_eq; simpl; auto. +Qed. -Local Hint Resolve is_constant_correct. +Lemma set_spec_diff d x y t m: + x <> y -> deps_eval ge (deps_set d x t) y m = deps_eval ge d y m. +Proof. + intros; unfold deps_eval, deps_set, deps_get; simpl; rewrite Dict.set_spec_diff; simpl; auto. +Qed. -Lemma failsafe_correct (t: tree) m: failsafe t = true -> tree_eval t m <> None. +Lemma deps_eval_empty x m: deps_eval ge deps_empty x m = Some (m x). Proof. - destruct t; simpl; try congruence. - destruct l; simpl; try congruence. - eauto. + unfold deps_eval, deps_get; rewrite Dict.empty_spec; simpl; auto. Qed. +Hint Rewrite set_spec_eq deps_eval_empty: dict_rw. + Fixpoint inst_deps (i: inst) (d old: deps): deps := match i with | nil => d | (x, e)::i' => - let t0:=deps_get d x in - let t1:=exp_tree e d old in - let v':=if failsafe t0 then t1 else (Terase t1 t0) in - inst_deps i' (Dict.set d x v') old + let t:=exp_tree e d old in + inst_deps i' (deps_set d x t) old end. Fixpoint bblock_deps_rec (p: bblock) (d: deps): deps := @@ -160,214 +145,236 @@ Fixpoint bblock_deps_rec (p: bblock) (d: deps): deps := bblock_deps_rec p' d' end. +Local Hint Resolve deps_eval_empty. + Definition bblock_deps: bblock -> deps - := fun p => bblock_deps_rec p Dict.empty. + := fun p => bblock_deps_rec p deps_empty. + +Lemma inst_deps_pre_monotonic i old: forall d m, + (pre (inst_deps i d old) ge m) -> (pre d ge m). +Proof. + induction i as [|[y e] i IHi]; simpl; auto. + intros d a H; generalize (IHi _ _ H); clear H IHi. + unfold deps_set; simpl; intuition. +Qed. -(** Main Result: the [bblock_deps_equiv] theorem states that bblocks with the same dependencies are observationaly equals *) +Lemma bblock_deps_pre_monotonic p: forall d m, + (pre (bblock_deps_rec p d) ge m) -> (pre d ge m). +Proof. + induction p as [|i p' IHp']; simpl; eauto. + intros d a H; eapply inst_deps_pre_monotonic; eauto. +Qed. +Local Hint Resolve inst_deps_pre_monotonic bblock_deps_pre_monotonic. Lemma tree_eval_exp e od m0 old: - (forall x, tree_eval (deps_get od x) m0 = Some (old x)) -> - forall d m1, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - (tree_eval (exp_tree e d od) m0) = exp_eval ge e m1 old. + (forall x, deps_eval ge od x m0 = Some (old x)) -> + forall d m1, + (forall x, deps_eval ge d x m0 = Some (m1 x)) -> + tree_eval ge (exp_tree e d od) m0 = exp_eval ge e m1 old. Proof. - intro H. - induction e using exp_mut with (P0:=fun l => forall d m1, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> list_tree_eval (list_exp_tree l d od) m0 = list_exp_eval ge l m1 old); simpl; auto. + unfold deps_eval in * |- *; intro H. + induction e using exp_mut with + (P0:=fun l => forall (d:deps) m1, (forall x, tree_eval ge (deps_get d x) m0 = Some (m1 x)) -> list_tree_eval ge (list_exp_tree l d od) m0 = list_exp_eval ge l m1 old); + simpl; auto. - intros; erewrite IHe; eauto. - - intros; erewrite IHe, IHe0; eauto. + - intros. erewrite IHe, IHe0; eauto. Qed. -Lemma tree_eval_inst_abort i m0 x old: forall d, - tree_eval (deps_get d x) m0 = None -> - tree_eval (deps_get (inst_deps i d old) x) m0 = None. +Lemma inst_deps_abort i m0 x old: forall d, + pre (inst_deps i d old) ge m0 -> + deps_eval ge d x m0 = None -> + deps_eval ge (inst_deps i d old) x m0 = None. Proof. induction i as [|[y e] i IHi]; simpl; auto. - intros d H; erewrite IHi; eauto. clear IHi. + intros d VALID H; erewrite IHi; eauto. clear IHi. destruct (R.eq_dec x y). * subst; autorewrite with dict_rw. - generalize (failsafe_correct (deps_get d y) m0). - destruct (failsafe (deps_get d y)); simpl; intuition try congruence. - rewrite H; simpl. auto. - * rewrite! set_spec_diff; auto. + generalize (inst_deps_pre_monotonic _ _ _ _ VALID); clear VALID. + unfold deps_set; simpl; intuition congruence. + * rewrite set_spec_diff; auto. Qed. -Lemma tree_eval_abort p m0 x: forall d, - tree_eval (deps_get d x) m0 = None -> - tree_eval (deps_get (bblock_deps_rec p d) x) m0 = None. +Lemma block_deps_rec_abort p m0 x: forall d, + pre (bblock_deps_rec p d) ge m0 -> + deps_eval ge d x m0 = None -> + deps_eval ge (bblock_deps_rec p d) x m0 = None. Proof. induction p; simpl; auto. - intros d H; erewrite IHp; eauto. clear IHp. - eapply tree_eval_inst_abort; eauto. + intros d VALID H; erewrite IHp; eauto. clear IHp. + eapply inst_deps_abort; eauto. Qed. -Lemma tree_eval_inst_Some_correct1 i m0 old od: - (forall x, tree_eval (deps_get od x) m0 = Some (old x)) -> - forall (m1 m2: mem) d, +Lemma inst_deps_Some_correct1 i m0 old od: + (forall x, deps_eval ge od x m0 = Some (old x)) -> + forall (m1 m2: mem) (d: deps), inst_run ge i m1 old = Some m2 -> - (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - (forall x, tree_eval (deps_get (inst_deps i d od) x) m0 = Some (m2 x)). + (forall x, deps_eval ge d x m0 = Some (m1 x)) -> + forall x, deps_eval ge (inst_deps i d od) x m0 = Some (m2 x). Proof. intro X; induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H. - inversion_clear H; eauto. - intros H0 x0. - remember (exp_eval ge e m1 old) as ov. - destruct ov. - + refine (IHi _ _ _ _ _ _); eauto. - clear x0; intros x0. - unfold assign; destruct (R.eq_dec x x0). - * subst; autorewrite with dict_rw. - destruct (failsafe (deps_get d x0)); simpl; try rewrite H0; - erewrite tree_eval_exp; eauto. - * rewrite set_spec_diff; auto. - + inversion H. + destruct (exp_eval ge e m1 old) eqn:Heqov; try congruence. + refine (IHi _ _ _ _ _ _); eauto. + clear x0; intros x0. + unfold assign; destruct (R.eq_dec x x0). + * subst; autorewrite with dict_rw. + erewrite tree_eval_exp; eauto. + * rewrite set_spec_diff; auto. Qed. -Local Hint Resolve tree_eval_inst_Some_correct1 tree_eval_abort. - -Lemma tree_eval_Some_correct1 p m0: forall (m1 m2: mem) d, +Lemma bblocks_deps_rec_Some_correct1 p m0: forall (m1 m2: mem) d, run ge p m1 = Some m2 -> - (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - (forall x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = Some (m2 x)). + (forall x, deps_eval ge d x m0 = Some (m1 x)) -> + forall x, deps_eval ge (bblock_deps_rec p d) x m0 = Some (m2 x). Proof. + Local Hint Resolve inst_deps_Some_correct1. induction p as [ | i p]; simpl; intros m1 m2 d H. - inversion_clear H; eauto. - intros H0 x0. - remember (inst_run ge i m1 m1) as om. - destruct om. + destruct (inst_run ge i m1 m1) eqn: Heqov. + refine (IHp _ _ _ _ _ _); eauto. + inversion H. Qed. Lemma bblock_deps_Some_correct1 p m0 m1: - run ge p m0 = Some m1 - -> forall x, tree_eval (deps_get (bblock_deps p) x) m0 = Some (m1 x). + run ge p m0 = Some m1 + -> forall x, deps_eval ge (bblock_deps p) x m0 = Some (m1 x). Proof. - intros; eapply tree_eval_Some_correct1; - intros; autorewrite with dict_rw; simpl; eauto. + intros; eapply bblocks_deps_rec_Some_correct1; eauto. Qed. -Lemma tree_eval_inst_None_correct i m0 old od: - (forall x, tree_eval (deps_get od x) m0 = Some (old x)) -> - forall m1 d, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - inst_run ge i m1 old = None <-> exists x, tree_eval (deps_get (inst_deps i d od) x) m0 = None. +Lemma inst_deps_None_correct i m0 old od: + (forall x, deps_eval ge od x m0 = Some (old x)) -> + forall m1 d, pre (inst_deps i d od) ge m0 -> + (forall x, deps_eval ge d x m0 = Some (m1 x)) -> + inst_run ge i m1 old = None -> exists x, deps_eval ge (inst_deps i d od) x m0 = None. Proof. intro X; induction i as [|[x e] i IHi]; simpl; intros m1 d. - - constructor 1; [discriminate | intros [x H']; rewrite H in H'; discriminate]. - - intros H0. - remember (exp_eval ge e m1 old) as ov. - destruct ov. - + refine (IHi _ _ _); eauto. + - discriminate. + - intros VALID H0. + destruct (exp_eval ge e m1 old) eqn: Heqov. + + refine (IHi _ _ _ _); eauto. intros x0; unfold assign; destruct (R.eq_dec x x0). * subst; autorewrite with dict_rw. - destruct (failsafe (deps_get d x0)); simpl; try rewrite H0; erewrite tree_eval_exp; eauto. * rewrite set_spec_diff; auto. + intuition. constructor 1 with (x:=x); simpl. - apply tree_eval_inst_abort. + apply inst_deps_abort; auto. autorewrite with dict_rw. - destruct (failsafe (deps_get d x)); simpl; try rewrite H0; erewrite tree_eval_exp; eauto. Qed. - -Lemma tree_eval_None_correct p m0: forall m1 d, - (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - run ge p m1 = None <-> exists x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = None. -Proof. - induction p as [|i p IHp]; simpl; intros m1 d. - - constructor 1; [discriminate | intros [x H']; rewrite H in H'; discriminate]. - - intros H0. - remember (inst_run ge i m1 m1) as om. - destruct om. - + refine (IHp _ _ _); eauto. - + intuition. - assert (X: inst_run ge i m1 m1 = None); auto. - rewrite tree_eval_inst_None_correct in X; auto. - destruct X as [x H1]. - constructor 1 with (x:=x); simpl; auto. -Qed. - -Lemma bblock_deps_None_correct p m: - run ge p m = None <-> exists x, tree_eval (deps_get (bblock_deps p) x) m = None. -Proof. - intros; eapply tree_eval_None_correct. - intros; autorewrite with dict_rw; simpl; eauto. -Qed. - -Lemma tree_eval_inst_Some_correct2 i m0 old od: - (forall x, tree_eval (deps_get od x) m0 = Some (old x)) -> +Lemma inst_deps_Some_correct2 i m0 old od: + (forall x, deps_eval ge od x m0 = Some (old x)) -> forall (m1 m2: mem) d, - (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - (forall x, tree_eval (deps_get (inst_deps i d od) x) m0 = Some (m2 x)) -> - res_eq (Some m2) (inst_run ge i m1 old). + pre (inst_deps i d od) ge m0 -> + (forall x, deps_eval ge d x m0 = Some (m1 x)) -> + (forall x, deps_eval ge (inst_deps i d od) x m0 = Some (m2 x)) -> + res_eq (Some m2) (inst_run ge i m1 old). Proof. intro X. - induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H0. + induction i as [|[x e] i IHi]; simpl; intros m1 m2 d VALID H0. - intros H; eapply ex_intro; intuition eauto. generalize (H0 x); rewrite H. congruence. - intros H. - remember (exp_eval ge e m1 old) as ov. - destruct ov. - + refine (IHi _ _ _ _ _); eauto. + destruct (exp_eval ge e m1 old) eqn: Heqov. + + refine (IHi _ _ _ _ _ _); eauto. intros x0; unfold assign; destruct (R.eq_dec x x0). - * subst; autorewrite with dict_rw. - destruct (failsafe (deps_get d x0)); simpl; try rewrite H0; + * subst. autorewrite with dict_rw. erewrite tree_eval_exp; eauto. * rewrite set_spec_diff; auto. + generalize (H x). - rewrite tree_eval_inst_abort; try discriminate. + rewrite inst_deps_abort; discriminate || auto. autorewrite with dict_rw. - destruct (failsafe (deps_get d x)); simpl; try rewrite H0; erewrite tree_eval_exp; eauto. Qed. -Lemma tree_eval_Some_correct2 p m0: forall (m1 m2: mem) d, - (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - (forall x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = Some (m2 x)) -> +Lemma bblocks_deps_rec_Some_correct2 p m0: forall (m1 m2: mem) d, + pre (bblock_deps_rec p d) ge m0 -> + (forall x, deps_eval ge d x m0 = Some (m1 x)) -> + (forall x, deps_eval ge (bblock_deps_rec p d) x m0 = Some (m2 x)) -> res_eq (Some m2) (run ge p m1). Proof. - induction p as [|i p]; simpl; intros m1 m2 d H0. + induction p as [|i p]; simpl; intros m1 m2 d VALID H0. - intros H; eapply ex_intro; intuition eauto. generalize (H0 x); rewrite H. congruence. - intros H. - remember (inst_run ge i m1 m1) as om. - destruct om. - + refine (IHp _ _ _ _ _); eauto. - + assert (X: inst_run ge i m1 m1 = None); auto. - rewrite tree_eval_inst_None_correct in X; auto. + destruct (inst_run ge i m1 m1) eqn: Heqom. + + refine (IHp _ _ _ _ _ _); eauto. + + assert (X: exists x, tree_eval ge (deps_get (inst_deps i d d) x) m0 = None). + { eapply inst_deps_None_correct; eauto. } destruct X as [x H1]. generalize (H x). - rewrite tree_eval_abort; congruence. + erewrite block_deps_rec_abort; eauto. + congruence. Qed. + Lemma bblock_deps_Some_correct2 p m0 m1: - (forall x, tree_eval (deps_get (bblock_deps p) x) m0 = Some (m1 x)) + pre (bblock_deps p) ge m0 -> + (forall x, deps_eval ge (bblock_deps p) x m0 = Some (m1 x)) -> res_eq (Some m1) (run ge p m0). Proof. - intros; eapply tree_eval_Some_correct2; eauto. - intros; autorewrite with dict_rw; simpl; eauto. + intros; eapply bblocks_deps_rec_Some_correct2; eauto. +Qed. + +Lemma inst_valid i m0 old od: + (forall x, deps_eval ge od x m0 = Some (old x)) -> + forall (m1 m2: mem) (d: deps), + pre d ge m0 -> + inst_run ge i m1 old = Some m2 -> + (forall x, deps_eval ge d x m0 = Some (m1 x)) -> + pre (inst_deps i d od) ge m0. +Proof. + induction i as [|[x e] i IHi]; simpl; auto. + intros Hold m1 m2 d VALID0 H Hm1. + destruct (exp_eval ge e m1 old) eqn: Heq; simpl; try congruence. + eapply IHi; eauto. + + unfold deps_set in * |- *; simpl. + rewrite Hm1; intuition congruence. + + intros x0. unfold assign; destruct (R.eq_dec x x0). + * subst; autorewrite with dict_rw. + erewrite tree_eval_exp; eauto. + * rewrite set_spec_diff; auto. +Qed. + + +Lemma block_deps_rec_valid p m0: forall (m1 m2: mem) (d:deps), + pre d ge m0 -> + run ge p m1 = Some m2 -> + (forall x, deps_eval ge d x m0 = Some (m1 x)) -> + pre (bblock_deps_rec p d) ge m0. +Proof. + Local Hint Resolve inst_valid. + induction p as [ | i p]; simpl; intros m1 d H; auto. + intros H0 H1. + destruct (inst_run ge i m1 m1) eqn: Heqov; eauto. + congruence. Qed. +Lemma bblock_deps_valid p m0 m1: + run ge p m0 = Some m1 -> + pre (bblock_deps p) ge m0. +Proof. + intros; eapply block_deps_rec_valid; eauto. + unfold deps_empty; simpl. auto. +Qed. Theorem bblock_deps_simu p1 p2: - (forall x, deps_get (bblock_deps p1) x = deps_get (bblock_deps p2) x) - -> bblock_simu ge p1 p2. + (forall m, pre (bblock_deps p1) ge m -> pre (bblock_deps p2) ge m) -> + (forall m0 x m1, pre (bblock_deps p1) ge m0 -> deps_eval ge (bblock_deps p1) x m0 = Some m1 -> + deps_eval ge (bblock_deps p2) x m0 = Some m1) -> + bblock_simu ge p1 p2. Proof. - intros H m2 DONTFAIL. - remember (run ge p1 m2) as om1. - destruct om1; simpl. - + apply bblock_deps_Some_correct2. - intros; rewrite <- H. - apply bblock_deps_Some_correct1; auto. - + rewrite bblock_deps_None_correct. - assert (X: run ge p1 m2 = None); auto. - rewrite bblock_deps_None_correct in X. - destruct X as [x Hx]. - rewrite H in Hx. - eauto. + Local Hint Resolve bblock_deps_valid bblock_deps_Some_correct1. + intros INCL EQUIV m DONTFAIL. + destruct (run ge p1 m) as [m1|] eqn: RUN1; simpl; try congruence. + eapply bblock_deps_Some_correct2; eauto. Qed. End DEPTREE. |