diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-26 08:50:44 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-26 08:50:44 +0200 |
commit | fd7a801bef1e9fe6e47b62c5c1b0905a4dde7ae8 (patch) | |
tree | 0aa1815de9f96f536652fed44fc0bfc2819e0fee /mppa_k1c/abstractbb | |
parent | 11aa243fe776dc99001004a74b8ed0fc42c12fc9 (diff) | |
download | compcert-kvx-fd7a801bef1e9fe6e47b62c5c1b0905a4dde7ae8.tar.gz compcert-kvx-fd7a801bef1e9fe6e47b62c5c1b0905a4dde7ae8.zip |
extending bblock_simu_test with rewriting
Diffstat (limited to 'mppa_k1c/abstractbb')
-rw-r--r-- | mppa_k1c/abstractbb/AbstractBasicBlocksDef.v | 130 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/DepTreeTheory.v | 456 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/ImpDep.v | 960 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/ImpSimuTest.v | 1108 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpCore.v | 2 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpHCons.v | 104 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpLoops.v | 8 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpPrelude.v | 51 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml | 37 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli | 5 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Parallelizability.v | 4 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/SeqSimuTheory.v | 428 |
12 files changed, 1797 insertions, 1496 deletions
diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v index 618f3ebe..f381c810 100644 --- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v +++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v @@ -1,6 +1,6 @@ (** Syntax and Sequential Semantics of Abstract Basic Blocks. *) - +Require Import ImpPrelude. Module Type PseudoRegisters. @@ -24,16 +24,8 @@ Parameter op: Type. (* type of operations *) Parameter genv: Type. (* environment to be used for evaluating an op *) -(* NB: possible generalization - - relation after/before. -*) Parameter op_eval: genv -> op -> list value -> option value. -Parameter is_constant: op -> bool. - -Parameter is_constant_correct: - forall ge o, is_constant o = true -> op_eval ge o nil <> None. - End LangParam. @@ -54,6 +46,9 @@ Definition mem := R.t -> value. Definition assign (m: mem) (x:R.t) (v: value): mem := fun y => if R.eq_dec x y then v else m y. + +(** expressions *) + Inductive exp := | PReg (x:R.t) | Op (o:op) (le: list_exp) @@ -140,7 +135,7 @@ Proof. Qed. -(** A small theory of bblock equality *) +(** A small theory of bblock simulation *) (* equalities on bblock outputs *) Definition res_eq (om1 om2: option mem): Prop := @@ -240,6 +235,121 @@ Qed. End SEQLANG. +Module Terms. + +(** terms in the symbolic evaluation +NB: such a term represents the successive computations in one given pseudo-register +*) + +Inductive term := + | Input (x:R.t) (hid:hashcode) + | App (o: op) (l: list_term) (hid:hashcode) +with list_term := + | LTnil (hid:hashcode) + | LTcons (t:term) (l:list_term) (hid:hashcode) + . + +Scheme term_mut := Induction for term Sort Prop +with list_term_mut := Induction for list_term Sort Prop. + +Bind Scope pattern_scope with term. +Delimit Scope term_scope with term. +Delimit Scope pattern_scope with pattern. + +Notation "[ ]" := (LTnil _) (format "[ ]"): pattern_scope. +Notation "[ x ]" := (LTcons x [] _): pattern_scope. +Notation "[ x ; y ; .. ; z ]" := (LTcons x (LTcons y .. (LTcons z (LTnil _) _) .. _) _): pattern_scope. +Notation "o @ l" := (App o l _) (at level 50, no associativity): pattern_scope. + +Import HConsingDefs. + +Notation "[ ]" := (LTnil unknown_hid) (format "[ ]"): term_scope. +Notation "[ x ]" := (LTcons x [] unknown_hid): term_scope. +Notation "[ x ; y ; .. ; z ]" := (LTcons x (LTcons y .. (LTcons z (LTnil unknown_hid) unknown_hid) .. unknown_hid) unknown_hid): term_scope. +Notation "o @ l" := (App o l unknown_hid) (at level 50, no associativity): term_scope. + +Local Open Scope pattern_scope. + +Fixpoint term_eval (ge: genv) (t: term) (m: mem): option value := + match t with + | Input x _ => Some (m x) + | o @ l => + match list_term_eval ge l m with + | Some v => op_eval ge o v + | _ => None + end + end +with list_term_eval ge (l: list_term) (m: mem) {struct l}: option (list value) := + match l with + | [] => Some nil + | LTcons t l' _ => + match term_eval ge t m, list_term_eval ge l' m with + | Some v, Some lv => Some (v::lv) + | _, _ => None + end + end. + + +Definition term_get_hid (t: term): hashcode := + match t with + | Input _ hid => hid + | App _ _ hid => hid + end. + +Definition list_term_get_hid (l: list_term): hashcode := + match l with + | LTnil hid => hid + | LTcons _ _ hid => hid + end. + + +Definition allvalid ge (l: list term) m := forall t, List.In t l -> term_eval ge t m <> None. + +Record pseudo_term: Type := { + valid: list term; + effect: term +}. + +Definition match_pseudo_term (t: term) (pt: pseudo_term) := + (forall ge m, term_eval ge t m <> None <-> allvalid ge pt.(valid) m) + /\ (forall ge m0 m1, term_eval ge t m0 = Some m1 -> term_eval ge pt.(effect) m0 = Some m1). + +Import ImpCore.Notations. +Local Open Scope impure_scope. + +Record reduction (t:term):= { + result:> ?? pseudo_term; + result_correct: WHEN result ~> pt THEN match_pseudo_term t pt; +}. +Hint Resolve result_correct: wlp. + +Program Definition identity_reduce (t: term): reduction t := {| result := RET {| valid := [t]; effect := t |} |}. +Obligation 1. + unfold match_pseudo_term, allvalid; wlp_simplify; congruence. +Qed. +Global Opaque identity_reduce. + +Program Definition failsafe_reduce (is_constant: op -> bool | forall ge o, is_constant o = true -> op_eval ge o nil <> None) (t: term) := + match t with + | Input x _ => {| result := RET {| valid := []; effect := t |} |} + | o @ [] => match is_constant o with + | true => {| result := RET {| valid := []; effect := t |} |} + | false => identity_reduce t + end + | _ => identity_reduce t + end. +Obligation 1. + unfold match_pseudo_term, allvalid; simpl; wlp_simplify; congruence. +Qed. +Obligation 2. + unfold match_pseudo_term, allvalid; simpl; wlp_simplify. +Qed. +Obligation 3. + intuition congruence. +Qed. + +End Terms. + End MkSeqLanguage. diff --git a/mppa_k1c/abstractbb/DepTreeTheory.v b/mppa_k1c/abstractbb/DepTreeTheory.v deleted file mode 100644 index c7bed8bf..00000000 --- a/mppa_k1c/abstractbb/DepTreeTheory.v +++ /dev/null @@ -1,456 +0,0 @@ -(** Dependency Trees of Abstract Basic Blocks - -with a purely-functional-but-exponential test. - -*) - - -Require Setoid. (* in order to rewrite <-> *) -Require Export AbstractBasicBlocksDef. -Require Import List. - -Module Type PseudoRegDictionary. - -Declare Module R: PseudoRegisters. - -Parameter t: Type -> Type. - -Parameter get: forall {A}, t A -> R.t -> option A. - -Parameter set: forall {A}, t A -> R.t -> A -> t A. - -Parameter set_spec_eq: forall A d x (v: A), - get (set d x v) x = Some v. - -Parameter set_spec_diff: forall A d x y (v: A), - x <> y -> get (set d x v) y = get d y. - -Parameter empty: forall {A}, t A. - -Parameter empty_spec: forall A x, - get (empty (A:=A)) x = None. - -End PseudoRegDictionary. - - -(** * Computations of "bblock" Dependencies and application to the equality test *) - -Module DepTree (L: SeqLanguage) (Dict: PseudoRegDictionary with Module R:=L.LP.R). - -Export L. -Export LP. - -Section DEPTREE. - -(** Dependency Trees of these "bblocks" - -NB: each tree represents the successive computations in one given resource - -*) - -Inductive tree := - | Tname (x:R.t) - | Top (o: op) (l: list_tree) -with list_tree := - | Tnil: list_tree - | Tcons (t:tree) (l:list_tree): list_tree - . - - -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 ge l m with - | Some v => op_eval ge o v - | _ => None - end - end -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 ge t m), (list_tree_eval ge l' m) with - | Some v, Some lv => Some (v::lv) - | _, _ => None - end - end. - -Definition deps_get (d:Dict.t tree) x := - match Dict.get d x with - | None => Tname x - | Some t => t - end. - -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: 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. - -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. - -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 deps_eval_empty x m: deps_eval ge deps_empty x m = Some (m x). -Proof. - 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 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 := - match p with - | nil => d - | i::p' => - let d':=inst_deps i d d in - bblock_deps_rec p' d' - end. - -Local Hint Resolve deps_eval_empty. - -Definition bblock_deps: bblock -> deps - := 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. - -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, 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. - 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. -Qed. - -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 VALID H; erewrite IHi; eauto. clear IHi. - destruct (R.eq_dec x y). - * subst; autorewrite with dict_rw. - generalize (inst_deps_pre_monotonic _ _ _ _ VALID); clear VALID. - unfold deps_set; simpl; intuition congruence. - * rewrite set_spec_diff; auto. -Qed. - -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 VALID H; erewrite IHp; eauto. clear IHp. - eapply inst_deps_abort; eauto. -Qed. - -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, 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. - 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. - -Lemma bblocks_deps_rec_Some_correct1 p m0: forall (m1 m2: mem) d, - run ge p m1 = Some m2 -> - (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. - 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, deps_eval ge (bblock_deps p) x m0 = Some (m1 x). -Proof. - intros; eapply bblocks_deps_rec_Some_correct1; eauto. -Qed. - -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. - - 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. - erewrite tree_eval_exp; eauto. - * rewrite set_spec_diff; auto. - + intuition. - constructor 1 with (x:=x); simpl. - apply inst_deps_abort; auto. - autorewrite with dict_rw. - erewrite tree_eval_exp; eauto. -Qed. - -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, - 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 VALID H0. - - intros H; eapply ex_intro; intuition eauto. - generalize (H0 x); rewrite H. - congruence. - - intros H. - 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. - erewrite tree_eval_exp; eauto. - * rewrite set_spec_diff; auto. - + generalize (H x). - rewrite inst_deps_abort; discriminate || auto. - autorewrite with dict_rw. - erewrite tree_eval_exp; eauto. -Qed. - -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 VALID H0. - - intros H; eapply ex_intro; intuition eauto. - generalize (H0 x); rewrite H. - congruence. - - intros H. - 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). - erewrite block_deps_rec_abort; eauto. - congruence. -Qed. - - -Lemma bblock_deps_Some_correct2 p m0 m1: - 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 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. - -Definition valid ge d m := pre d ge m /\ forall x, deps_eval ge d x m <> None. - -Theorem bblock_deps_simu p1 p2: - (forall m, valid ge (bblock_deps p1) m -> valid ge (bblock_deps p2) m) -> - (forall m0 x m1, valid ge (bblock_deps p1) 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. - Local Hint Resolve bblock_deps_valid bblock_deps_Some_correct1. - unfold valid; intros INCL EQUIV m DONTFAIL. - destruct (run ge p1 m) as [m1|] eqn: RUN1; simpl; try congruence. - assert (X: forall x, deps_eval ge (bblock_deps p1) x m = Some (m1 x)); eauto. - eapply bblock_deps_Some_correct2; eauto. - + destruct (INCL m); intuition eauto. - congruence. - + intro x; apply EQUIV; intuition eauto. - congruence. -Qed. - -Lemma valid_set_decompose_1 d t x m: - valid ge (deps_set d x t) m -> valid ge d m. -Proof. - unfold valid; intros ((PRE1 & PRE2) & VALID); split. - + intuition. - + intros x0 H. case (R.eq_dec x x0). - * intuition congruence. - * intros DIFF; eapply VALID. erewrite set_spec_diff; eauto. -Qed. - -Lemma valid_set_decompose_2 d t x m: - valid ge (deps_set d x t) m -> tree_eval ge t m <> None. -Proof. - unfold valid; intros ((PRE1 & PRE2) & VALID) H. - generalize (VALID x); autorewrite with dict_rw. - tauto. -Qed. - -Lemma valid_set_proof d x t m: - valid ge d m -> tree_eval ge t m <> None -> valid ge (deps_set d x t) m. -Proof. - unfold valid; intros (PRE & VALID) PREt. split. - + split; auto. - + intros x0; case (R.eq_dec x x0). - - intros; subst; autorewrite with dict_rw. auto. - - intros. rewrite set_spec_diff; auto. -Qed. - -End DEPTREE. - -End DepTree. - -Require Import PArith. -Require Import FMapPositive. - -Module PosDict <: PseudoRegDictionary with Module R:=Pos. - -Module R:=Pos. - -Definition t:=PositiveMap.t. - -Definition get {A} (d:t A) (x:R.t): option A - := PositiveMap.find x d. - -Definition set {A} (d:t A) (x:R.t) (v:A): t A - := PositiveMap.add x v d. - -Local Hint Unfold PositiveMap.E.eq. - -Lemma set_spec_eq A d x (v: A): - get (set d x v) x = Some v. -Proof. - unfold get, set; apply PositiveMap.add_1; auto. -Qed. - -Lemma set_spec_diff A d x y (v: A): - x <> y -> get (set d x v) y = get d y. -Proof. - unfold get, set; intros; apply PositiveMap.gso; auto. -Qed. - -Definition empty {A}: t A := PositiveMap.empty A. - -Lemma empty_spec A x: - get (empty (A:=A)) x = None. -Proof. - unfold get, empty; apply PositiveMap.gempty; auto. -Qed. - -End PosDict.
\ No newline at end of file diff --git a/mppa_k1c/abstractbb/ImpDep.v b/mppa_k1c/abstractbb/ImpDep.v deleted file mode 100644 index eebf396d..00000000 --- a/mppa_k1c/abstractbb/ImpDep.v +++ /dev/null @@ -1,960 +0,0 @@ -(** Dependency Graph of Abstract Basic Blocks - -using imperative hash-consing technique in order to get a linear equivalence test. - -*) - -Require Export Impure.ImpHCons. -Export Notations. - -Require Export DepTreeTheory. - -Require Import PArith. - - -Local Open Scope impure. - -Import ListNotations. -Local Open Scope list_scope. - - -Module Type ImpParam. - -Include LangParam. - -Parameter op_eq: op -> op -> ?? bool. - -Parameter op_eq_correct: forall o1 o2, - WHEN op_eq o1 o2 ~> b THEN - b=true -> o1 = o2. - -End ImpParam. - - -Module Type ISeqLanguage. - -Declare Module LP: ImpParam. - -Include MkSeqLanguage LP. - -End ISeqLanguage. - - -Module Type ImpDict. - -Include PseudoRegDictionary. - -Parameter eq_test: forall {A}, t A -> t A -> ?? bool. - -Parameter eq_test_correct: forall A (d1 d2: t A), - WHEN eq_test d1 d2 ~> b THEN - b=true -> forall x, get d1 x = get d2 x. - -(* NB: we could also take an eq_test on R.t (but not really useful with "pure" dictionaries *) - - -(* only for debugging *) -Parameter not_eq_witness: forall {A}, t A -> t A -> ?? option R.t. - -End ImpDict. - -Module ImpDepTree (L: ISeqLanguage) (Dict: ImpDict with Module R:=L.LP.R). - -Module DT := DepTree L Dict. - -Import DT. - -Section CanonBuilding. - -Variable hC_tree: pre_hashV tree -> ?? hashV tree. -Hypothesis hC_tree_correct: forall t, WHEN hC_tree t ~> t' THEN pre_data t=data t'. - -Variable hC_list_tree: pre_hashV list_tree -> ?? hashV list_tree. -Hypothesis hC_list_tree_correct: forall t, WHEN hC_list_tree t ~> t' THEN pre_data t=data t'. - -(* First, we wrap constructors for hashed values !*) - -Local Open Scope positive. -Local Open Scope list_scope. - -Definition hTname (x:R.t) (debug: option pstring): ?? hashV tree := - DO hc <~ hash 1;; - DO hv <~ hash x;; - hC_tree {| pre_data:=Tname x; hcodes :=[hc;hv]; debug_info := debug |}. - -Lemma hTname_correct x dbg: - WHEN hTname x dbg ~> t THEN (data t)=(Tname x). -Proof. - wlp_simplify. -Qed. -Global Opaque hTname. -Hint Resolve hTname_correct: wlp. - -Definition hTop (o:op) (l: hashV list_tree) (debug: option pstring) : ?? hashV tree := - DO hc <~ hash 2;; - DO hv <~ hash o;; - hC_tree {| pre_data:=Top o (data l); - hcodes:=[hc;hv;hid l]; - debug_info := debug |}. - -Lemma hTop_correct o l dbg : - WHEN hTop o l dbg ~> t THEN (data t)=(Top o (data l)). -Proof. - wlp_simplify. -Qed. -Global Opaque hTop. -Hint Resolve hTop_correct: wlp. - -Definition hTnil (_: unit): ?? hashV list_tree := - hC_list_tree {| pre_data:=Tnil; hcodes := nil; debug_info := None |} . - -Lemma hTnil_correct x: - WHEN hTnil x ~> l THEN (data l)=Tnil. -Proof. - wlp_simplify. -Qed. -Global Opaque hTnil. -Hint Resolve hTnil_correct: wlp. - - -Definition hTcons (t: hashV tree) (l: hashV list_tree): ?? hashV list_tree := - hC_list_tree {| pre_data:=Tcons (data t) (data l); hcodes := [hid t; hid l]; debug_info := None |}. - -Lemma hTcons_correct t l: - WHEN hTcons t l ~> l' THEN (data l')=Tcons (data t) (data l). -Proof. - wlp_simplify. -Qed. -Global Opaque hTcons. -Hint Resolve hTcons_correct: wlp. - -(* Second, we use these hashed constructors ! *) - - -Record hdeps:= {hpre: list (hashV tree); hpost: Dict.t (hashV tree)}. - -Coercion hpost: hdeps >-> Dict.t. - -(* pseudo deps_get *) -Definition pdeps_get (d:Dict.t (hashV tree)) x : tree := - match Dict.get d x with - | None => Tname x - | Some t => (data t) - end. - -Definition hdeps_get (d:hdeps) x dbg : ?? hashV tree := - match Dict.get d x with - | None => hTname x dbg - | Some t => RET t - end. - -Lemma hdeps_get_correct (d:hdeps) x dbg: - WHEN hdeps_get d x dbg ~> t THEN (data t) = pdeps_get d x. -Proof. - unfold hdeps_get, pdeps_get; destruct (Dict.get d x); wlp_simplify. -Qed. -Global Opaque hdeps_get. -Hint Resolve hdeps_get_correct: wlp. - -Definition hdeps_valid ge (hd:hdeps) m := forall ht, List.In ht hd.(hpre) -> tree_eval ge (data ht) m <> None. - - -Definition deps_model ge (d: deps) (hd:hdeps): Prop := - (forall m, hdeps_valid ge hd m <-> valid ge d m) - /\ (forall m x, valid ge d m -> tree_eval ge (pdeps_get hd x) m = (deps_eval ge d x m)). - -Lemma deps_model_valid_alt ge d hd: deps_model ge d hd -> - forall m x, valid ge d m -> tree_eval ge (pdeps_get hd x) m <> None. -Proof. - intros (H1 & H2) m x H. rewrite H2; auto. - unfold valid in H. intuition eauto. -Qed. - -Lemma deps_model_hdeps_valid_alt ge d hd: deps_model ge d hd -> - forall m x, hdeps_valid ge hd m -> tree_eval ge (pdeps_get hd x) m <> None. -Proof. - intros (H1 & H2) m x H. eapply deps_model_valid_alt. - - split; eauto. - - rewrite <- H1; auto. -Qed. - -Fixpoint hexp_tree (e: exp) (d od: hdeps) (dbg: option pstring) : ?? hashV tree := - match e with - | PReg x => hdeps_get d x dbg - | Op o le => - DO lt <~ hlist_exp_tree le d od;; - hTop o lt dbg - | Old e => hexp_tree e od od dbg - end -with hlist_exp_tree (le: list_exp) (d od: hdeps): ?? hashV list_tree := - match le with - | Enil => hTnil tt - | Econs e le' => - DO t <~ hexp_tree e d od None;; - DO lt <~ hlist_exp_tree le' d od;; - hTcons t lt - | LOld le => hlist_exp_tree le od od - end. - -Lemma hexp_tree_correct_x ge e hod od: - deps_model ge od hod -> - forall hd d dbg, - deps_model ge d hd -> - WHEN hexp_tree e hd hod dbg ~> t THEN forall m, valid ge d m -> valid ge od m -> tree_eval ge (data t) m = tree_eval ge (exp_tree e d od) m. -Proof. - intro H. - induction e using exp_mut with (P0:=fun le => forall d hd, - deps_model ge d hd -> - WHEN hlist_exp_tree le hd hod ~> lt THEN forall m, valid ge d m -> valid ge od m -> list_tree_eval ge (data lt) m = list_tree_eval ge (list_exp_tree le d od) m); - unfold deps_model, deps_eval in * |- * ; simpl; wlp_simplify. - - rewrite H1, H4; auto. - - rewrite H4, <- H0; simpl; auto. - - rewrite H1; simpl; auto. - - rewrite H5, <- H0, <- H4; simpl; auto. -Qed. -Global Opaque hexp_tree. - -Lemma hexp_tree_correct e hd hod dbg: - WHEN hexp_tree e hd hod dbg ~> t THEN forall ge od d m, deps_model ge od hod -> deps_model ge d hd -> valid ge d m -> valid ge od m -> tree_eval ge (data t) m = tree_eval ge (exp_tree e d od) m. -Proof. - unfold wlp; intros; eapply hexp_tree_correct_x; eauto. -Qed. -Hint Resolve hexp_tree_correct: wlp. - -Definition failsafe (t: tree): bool := - match t with - | Tname x => true - | Top o Tnil => is_constant o - | _ => false - end. - -Local Hint Resolve is_constant_correct. - -Lemma failsafe_correct ge (t: tree) m: failsafe t = true -> tree_eval ge t m <> None. -Proof. - destruct t; simpl; try congruence. - destruct l; simpl; try congruence. - eauto. -Qed. -Local Hint Resolve failsafe_correct. - -Definition naive_set (hd:hdeps) x (t:hashV tree) := - {| hpre:= t::hd.(hpre); hpost:=Dict.set hd x t |}. - -Lemma naive_set_correct hd x ht ge d t: - deps_model ge d hd -> - (forall m, valid ge d m -> tree_eval ge (data ht) m = tree_eval ge t m) -> - deps_model ge (deps_set d x t) (naive_set hd x ht). -Proof. - unfold naive_set; intros (DM0 & DM1) EQT; split. - - intros m. - destruct (DM0 m) as (PRE & VALID0); clear DM0. - assert (VALID1: hdeps_valid ge hd m -> pre d ge m). { unfold valid in PRE; tauto. } - assert (VALID2: hdeps_valid ge hd m -> forall x : Dict.R.t, deps_eval ge d x m <> None). { unfold valid in PRE; tauto. } - unfold hdeps_valid in * |- *; simpl. - intuition (subst; eauto). - + eapply valid_set_proof; eauto. - erewrite <- EQT; eauto. - + exploit valid_set_decompose_1; eauto. - intros X1; exploit valid_set_decompose_2; eauto. - rewrite <- EQT; eauto. - + exploit valid_set_decompose_1; eauto. - - clear DM0. unfold deps_eval, pdeps_get, deps_get in * |- *; simpl. - Local Hint Resolve valid_set_decompose_1. - intros; case (R.eq_dec x x0). - + intros; subst; rewrite !Dict.set_spec_eq; simpl; eauto. - + intros; rewrite !Dict.set_spec_diff; simpl; eauto. -Qed. -Local Hint Resolve naive_set_correct. - -Definition equiv_hdeps ge (hd1 hd2: hdeps) := - (forall m, hdeps_valid ge hd1 m <-> hdeps_valid ge hd2 m) - /\ (forall m x, hdeps_valid ge hd1 m -> tree_eval ge (pdeps_get hd1 x) m = tree_eval ge (pdeps_get hd2 x) m). - -Lemma equiv_deps_symmetry ge hd1 hd2: - equiv_hdeps ge hd1 hd2 -> equiv_hdeps ge hd2 hd1. -Proof. - intros (V1 & P1); split. - - intros; symmetry; auto. - - intros; symmetry; eapply P1. rewrite V1; auto. -Qed. - -Lemma equiv_hdeps_models ge hd1 hd2 d: - deps_model ge d hd1 -> equiv_hdeps ge hd1 hd2 -> deps_model ge d hd2. -Proof. - intros (VALID & EQUIV) (HEQUIV & PEQUIV); split. - - intros m; rewrite <- VALID; auto. symmetry; auto. - - intros m x H. rewrite <- EQUIV; auto. - rewrite PEQUIV; auto. - rewrite VALID; auto. -Qed. - -Definition hdeps_set (hd:hdeps) x (t:hashV tree) := - DO ot <~ hdeps_get hd x None;; - DO b <~ phys_eq ot t;; - if b then - RET hd - else - RET {| hpre:= if failsafe (data t) then hd.(hpre) else t::hd.(hpre); - hpost:=Dict.set hd x t |}. - -Lemma hdeps_set_correct hd x ht: - WHEN hdeps_set hd x ht ~> nhd THEN - forall ge d t, deps_model ge d hd -> - (forall m, valid ge d m -> tree_eval ge (data ht) m = tree_eval ge t m) -> - deps_model ge (deps_set d x t) nhd. -Proof. - intros; wlp_simplify; eapply equiv_hdeps_models; eauto; unfold equiv_hdeps, hdeps_valid; simpl. - + split; eauto. - * intros m; split. - - intros X1 ht0 X2; apply X1; auto. - - intros X1 ht0 [Y1 | Y1]. subst. - rewrite H; eapply deps_model_hdeps_valid_alt; eauto. - eauto. - * intros m x0 X1. case (R.eq_dec x x0). - - intros; subst. unfold pdeps_get at 1. rewrite Dict.set_spec_eq. congruence. - - intros; unfold pdeps_get; rewrite Dict.set_spec_diff; auto. - + split; eauto. intros m. - generalize (failsafe_correct ge (data ht) m); intros FAILSAFE. - destruct (failsafe _); simpl; intuition (subst; eauto). -Qed. -Local Hint Resolve hdeps_set_correct: wlp. -Global Opaque hdeps_set. - -Variable debug_assign: R.t -> ?? option pstring. - -Fixpoint hinst_deps (i: inst) (d od: hdeps): ?? hdeps := - match i with - | nil => RET d - | (x, e)::i' => - DO dbg <~ debug_assign x;; - DO ht <~ hexp_tree e d od dbg;; - DO nd <~ hdeps_set d x ht;; - hinst_deps i' nd od - end. - - -Lemma hinst_deps_correct i: forall hd hod, - WHEN hinst_deps i hd hod ~> hd' THEN - forall ge od d, deps_model ge od hod -> deps_model ge d hd -> (forall m, valid ge d m -> valid ge od m) -> deps_model ge (inst_deps i d od) hd'. -Proof. - Local Hint Resolve valid_set_proof. - induction i; simpl; wlp_simplify; eauto 20. -Qed. -Global Opaque hinst_deps. -Local Hint Resolve hinst_deps_correct: wlp. - -(* logging info: we log the number of inst-instructions passed ! *) -Variable log: unit -> ?? unit. - -Fixpoint hbblock_deps_rec (p: bblock) (d: hdeps): ?? hdeps := - match p with - | nil => RET d - | i::p' => - log tt;; - DO d' <~ hinst_deps i d d;; - hbblock_deps_rec p' d' - end. - -Lemma hbblock_deps_rec_correct p: forall hd, - WHEN hbblock_deps_rec p hd ~> hd' THEN forall ge d, deps_model ge d hd -> deps_model ge (bblock_deps_rec p d) hd'. -Proof. - induction p; simpl; wlp_simplify. -Qed. -Global Opaque hbblock_deps_rec. -Local Hint Resolve hbblock_deps_rec_correct: wlp. - - -Definition hbblock_deps: bblock -> ?? hdeps - := fun p => hbblock_deps_rec p {| hpre:= nil ; hpost := Dict.empty |}. - -Lemma hbblock_deps_correct p: - WHEN hbblock_deps p ~> hd THEN forall ge, deps_model ge (bblock_deps p) hd. -Proof. - unfold bblock_deps; wlp_simplify. eapply H. clear H. - unfold deps_model, valid, pdeps_get, hdeps_valid, deps_eval, deps_get; simpl; intuition; - rewrite !Dict.empty_spec in * |- *; simpl in * |- *; try congruence. -Qed. -Global Opaque hbblock_deps. - -End CanonBuilding. - -(* Now, we build the hash-Cons value from a "hash_eq". - -Informal specification: - [hash_eq] must be consistent with the "hashed" constructors defined above. - -We expect that pre_hashV values in the code of these "hashed" constructors verify: - - (hash_eq (pre_data x) (pre_data y) ~> true) <-> (hcodes x)=(hcodes y) - -*) - -Definition tree_hash_eq (ta tb: tree): ?? bool := - match ta, tb with - | Tname xa, Tname xb => - if R.eq_dec xa xb (* Inefficient in some cases ? *) - then RET true - else RET false - | Top oa lta, Top ob ltb => - DO b <~ op_eq oa ob ;; - if b then phys_eq lta ltb - else RET false - | _,_ => RET false - end. - -Local Hint Resolve op_eq_correct: wlp. - -Lemma tree_hash_eq_correct: forall ta tb, WHEN tree_hash_eq ta tb ~> b THEN b=true -> ta=tb. -Proof. - destruct ta, tb; wlp_simplify; (discriminate || (subst; auto)). -Qed. -Global Opaque tree_hash_eq. -Hint Resolve tree_hash_eq_correct: wlp. - -Definition list_tree_hash_eq (lta ltb: list_tree): ?? bool := - match lta, ltb with - | Tnil, Tnil => RET true - | Tcons ta lta, Tcons tb ltb => - DO b <~ phys_eq ta tb ;; - if b then phys_eq lta ltb - else RET false - | _,_ => RET false - end. - -Lemma list_tree_hash_eq_correct: forall lta ltb, WHEN list_tree_hash_eq lta ltb ~> b THEN b=true -> lta=ltb. -Proof. - destruct lta, ltb; wlp_simplify; (discriminate || (subst; auto)). -Qed. -Global Opaque list_tree_hash_eq. -Hint Resolve list_tree_hash_eq_correct: wlp. - -Lemma pdeps_get_intro (d1 d2: hdeps): - (forall x, Dict.get d1 x = Dict.get d2 x) -> (forall x, pdeps_get d1 x = pdeps_get d2 x). -Proof. - unfold pdeps_get; intros H x; rewrite H. destruct (Dict.get d2 x); auto. -Qed. - -Local Hint Resolve hbblock_deps_correct Dict.eq_test_correct: wlp. - -(* TODO: - A REVOIR pour que Dict.test_eq qui soit insensible aux infos de debug ! - (cf. definition ci-dessous). - Il faut pour généraliser hash_params sur des Setoid (et les Dict aussi, avec ListSetoid, etc)... - *) -Program Definition mk_hash_params (log: hashV tree -> ?? unit): Dict.hash_params (hashV tree) := - {| (* Dict.test_eq := fun (ht1 ht2: hashV tree) => phys_eq (data ht1) (data ht2); *) - Dict.test_eq := phys_eq; - Dict.hashing := fun (ht: hashV tree) => RET (hid ht); - Dict.log := log |}. -Obligation 1. - eauto with wlp. -Qed. - -(*** A GENERIC EQ_TEST: IN ORDER TO SUPPORT SEVERAL DEBUGGING MODE !!! ***) - -Section Prog_Eq_Gen. - -Variable dbg1: R.t -> ?? option pstring. (* debugging of p1 insts *) -Variable dbg2: R.t -> ?? option pstring. (* log of p2 insts *) -Variable log1: unit -> ?? unit. (* log of p1 insts *) -Variable log2: unit -> ?? unit. (* log of p2 insts *) - -Variable hco_tree: hashConsing tree. -Hypothesis hco_tree_correct: hCons_spec hco_tree. -Variable hco_list: hashConsing list_tree. -Hypothesis hco_list_correct: hCons_spec hco_list. - -Variable print_error_end: hdeps -> hdeps -> ?? unit. -Variable print_error: pstring -> ?? unit. - -Variable check_failpreserv: bool. -Variable dbg_failpreserv: hashV tree -> ?? unit. (* info of additional failure of the output bbloc p2 wrt the input bbloc p1 *) - -Program Definition g_bblock_simu_test (p1 p2: bblock): ?? bool := - DO failure_in_failpreserv <~ make_cref false;; - DO r <~ (TRY - DO d1 <~ hbblock_deps (hC hco_tree) (hC hco_list) dbg1 log1 p1 ;; - DO d2 <~ hbblock_deps (hC_known hco_tree) (hC_known hco_list) dbg2 log2 p2 ;; - DO b <~ Dict.eq_test d1 d2 ;; - if b then ( - if check_failpreserv then ( - let hp := mk_hash_params dbg_failpreserv in - failure_in_failpreserv.(set)(true);; - Sets.assert_list_incl hp d2.(hpre) d1.(hpre);; - RET true - ) else RET false - ) else ( - print_error_end d1 d2 ;; - RET false - ) - CATCH_FAIL s, _ => - DO b <~ failure_in_failpreserv.(get)();; - if b then RET false - else print_error s;; RET false - ENSURE (fun b => b=true -> forall ge, bblock_simu ge p1 p2));; - RET (`r). -Obligation 1. - destruct hco_tree_correct as [TEQ1 TEQ2], hco_list_correct as [LEQ1 LEQ2]. - constructor 1; wlp_simplify; try congruence. - destruct (H ge) as (EQPRE1&EQPOST1); destruct (H0 ge) as (EQPRE2&EQPOST2); clear H H0. - apply bblock_deps_simu; auto. - + intros m; rewrite <- EQPRE1, <- EQPRE2. - unfold incl, hdeps_valid in * |- *; intuition eauto. - + intros m0 x m1 VALID; rewrite <- EQPOST1, <- EQPOST2; auto. - erewrite pdeps_get_intro; auto. - auto. - erewrite <- EQPRE2; auto. - erewrite <- EQPRE1 in VALID. - unfold incl, hdeps_valid in * |- *; intuition eauto. -Qed. - -Theorem g_bblock_simu_test_correct p1 p2: - WHEN g_bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2. -Proof. - wlp_simplify. - destruct exta0; simpl in * |- *; auto. -Qed. -Global Opaque g_bblock_simu_test. - -End Prog_Eq_Gen. - - - -Definition skip (_:unit): ?? unit := RET tt. -Definition no_dbg (_:R.t): ?? option pstring := RET None. - - -Definition msg_prefix: pstring := "*** ERROR INFO from bblock_simu_test: ". -Definition msg_error_on_end: pstring := "mismatch in final assignments !". -Definition msg_unknow_tree: pstring := "unknown tree node". -Definition msg_unknow_list_tree: pstring := "unknown list node". -Definition msg_number: pstring := "on 2nd bblock -- on inst num ". -Definition msg_notfailpreserv: pstring := "a possible failure of 2nd bblock is absent in 1st bblock". - -Definition print_error_end (_ _: hdeps): ?? unit - := println (msg_prefix +; msg_error_on_end). - -Definition print_error (log: logger unit) (s:pstring): ?? unit - := DO n <~ log_info log ();; - println (msg_prefix +; msg_number +; n +; " -- " +; s). - -Definition failpreserv_error (_: hashV tree): ?? unit - := println (msg_prefix +; msg_notfailpreserv). - -Program Definition bblock_simu_test (p1 p2: bblock): ?? bool := - DO log <~ count_logger ();; - DO hco_tree <~ mk_annot (hCons tree_hash_eq (fun _ => RET msg_unknow_tree));; - DO hco_list <~ mk_annot (hCons list_tree_hash_eq (fun _ => RET msg_unknow_list_tree));; - g_bblock_simu_test - no_dbg - no_dbg - skip - (log_insert log) - hco_tree _ - hco_list _ - print_error_end - (print_error log) - true (* check_failpreserv *) - failpreserv_error - p1 p2. -Obligation 1. - generalize (hCons_correct _ _ _ _ H0); clear H0. - constructor 1; wlp_simplify. -Qed. -Obligation 2. - generalize (hCons_correct _ _ _ _ H); clear H. - constructor 1; wlp_simplify. -Qed. - -Local Hint Resolve g_bblock_simu_test_correct. - -Theorem bblock_simu_test_correct p1 p2: - WHEN bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2. -Proof. - wlp_simplify. -Qed. -Global Opaque bblock_simu_test. - - - -(** This is only to print info on each bblock_simu_test run **) -Section Verbose_version. - -Variable string_of_name: R.t -> ?? pstring. -Variable string_of_op: op -> ?? pstring. - -Definition tree_id (id: caml_string): pstring := "E" +; (CamlStr id). -Definition list_id (id: caml_string): pstring := "L" +; (CamlStr id). - -Local Open Scope string_scope. - -Definition print_raw_htree (td: pre_hashV tree): ?? unit := - match pre_data td, hcodes td with - | (Tname x), _ => - DO s <~ string_of_name x;; - println( "init_access " +; s) - | (Top o Tnil), _ => - DO so <~ string_of_op o;; - println so - | (Top o _), [ _; _; lid ] => - DO so <~ string_of_op o;; - DO sl <~ string_of_hashcode lid;; - println (so +; " " +; (list_id sl)) - | _, _ => FAILWITH "unexpected hcodes" - end. - -Definition print_raw_hlist(ld: pre_hashV list_tree): ?? unit := - match pre_data ld, hcodes ld with - | Tnil, _ => println "" - | (Tcons _ _), [ t ; l ] => - DO st <~ string_of_hashcode t ;; - DO sl <~ string_of_hashcode l ;; - println((tree_id st) +; " " +; (list_id sl)) - | _, _ => FAILWITH "unexpected hcodes" - end. - -Section PrettryPrint. - -Variable get_htree: hashcode -> ?? pre_hashV tree. -Variable get_hlist: hashcode -> ?? pre_hashV list_tree. - -(* NB: requires [t = pre_data pt] *) -Fixpoint string_of_tree (t: tree) (pt: pre_hashV tree) : ?? pstring := - match debug_info pt with - | Some x => RET x - | None => - match t, hcodes pt with - | Tname x, _ => string_of_name x - | Top o Tnil, _ => string_of_op o - | Top o (_ as l), [ _; _; lid ] => - DO so <~ string_of_op o;; - DO pl <~ get_hlist lid;; - DO sl <~ string_of_list_tree l pl;; - RET (so +; "(" +; sl +; ")") - | _, _ => FAILWITH "unexpected hcodes" - end - end -(* NB: requires [l = pre_data pl] *) -with string_of_list_tree (l: list_tree) (lt: pre_hashV list_tree): ?? pstring := - match l, hcodes lt with - | Tnil, _ => RET (Str "") - | Tcons t Tnil, [ tid ; l ] => - DO pt <~ get_htree tid;; - string_of_tree t pt - | Tcons t l', [ tid ; lid' ] => - DO pt <~ get_htree tid;; - DO st <~ string_of_tree t pt;; - DO pl' <~ get_hlist lid';; - DO sl <~ string_of_list_tree l' pl';; - RET (st +; "," +; sl) - | _, _ => FAILWITH "unexpected hcodes" - end. - - -End PrettryPrint. - - -Definition pretty_tree ext exl pt := - DO r <~ string_of_tree (get_hashV ext) (get_hashV exl) (pre_data pt) pt;; - println(r). - -Fixpoint print_head (head: list pstring): ?? unit := - match head with - | i::head' => println ("--- inst " +; i);; print_head head' - | _ => RET tt - end. - -Definition print_htree ext exl (head: list pstring) (hid: hashcode) (td: pre_hashV tree): ?? unit := - print_head head;; - DO s <~ string_of_hashcode hid ;; - print ((tree_id s) +; ": ");; - print_raw_htree td;; - match debug_info td with - | Some x => - print("// " +; x +; " <- ");; - pretty_tree ext exl {| pre_data:=(pre_data td); hcodes:=(hcodes td); debug_info:=None |} - | None => RET tt - end. - -Definition print_hlist (head: list pstring) (hid: hashcode) (ld: pre_hashV list_tree): ?? unit := - print_head head;; - DO s <~ string_of_hashcode hid ;; - print ((list_id s) +; ": ");; - print_raw_hlist ld. - -Definition print_tables ext exl: ?? unit := - println "-- tree table --" ;; - iterall ext (print_htree ext exl);; - println "-- list table --" ;; - iterall exl print_hlist;; - println "----------------". - -Definition print_final_debug ext exl (d1 d2: hdeps): ?? unit - := DO b <~ Dict.not_eq_witness d1 d2 ;; - match b with - | Some x => - DO s <~ string_of_name x;; - println("mismatch on: " +; s);; - match Dict.get d1 x with - | None => println("=> unassigned in 1st bblock") - | Some ht1 => - print("=> node expected from 1st bblock: ");; - DO pt1 <~ get_hashV ext (hid ht1);; - pretty_tree ext exl pt1 - end;; - match Dict.get d2 x with - | None => println("=> unassigned in 2nd bblock") - | Some ht2 => - print("=> node found from 2nd bblock: ");; - DO pt2 <~ get_hashV ext (hid ht2);; - pretty_tree ext exl pt2 - end - | None => FAILWITH "bug in Dict.not_eq_witness ?" - end. - -Inductive witness:= - | Htree (pt: pre_hashV tree) - | Hlist (pl: pre_hashV list_tree) - | Nothing - . - -Definition msg_tree (cr: cref witness) td := - set cr (Htree td);; - RET msg_unknow_tree. - -Definition msg_list (cr: cref witness) tl := - set cr (Hlist tl);; - RET msg_unknow_list_tree. - -Definition print_witness ext exl cr msg := - DO wit <~ get cr ();; - match wit with - | Htree pt => - println("=> unknown tree node: ");; - pretty_tree ext exl {| pre_data:=(pre_data pt); hcodes:=(hcodes pt); debug_info:=None |};; - println("=> encoded on " +; msg +; " graph as: ");; - print_raw_htree pt - | Hlist pl => - println("=> unknown list node: ");; - DO r <~ string_of_list_tree (get_hashV ext) (get_hashV exl) (pre_data pl) pl;; - println(r);; - println("=> encoded on " +; msg +; " graph as: ");; - print_raw_hlist pl - | _ => println "Unexpected failure: no witness info (hint: hash-consing bug ?)" - end. - - -Definition print_error_end1 hct hcl (d1 d2:hdeps): ?? unit - := println "- GRAPH of 1st bblock";; - DO ext <~ export hct ();; - DO exl <~ export hcl ();; - print_tables ext exl;; - print_error_end d1 d2;; - print_final_debug ext exl d1 d2. - -Definition print_error1 hct hcl cr log s : ?? unit - := println "- GRAPH of 1st bblock";; - DO ext <~ export hct ();; - DO exl <~ export hcl ();; - print_tables ext exl;; - print_error log s;; - print_witness ext exl cr "1st". - - -Definition xmsg_number: pstring := "on 1st bblock -- on inst num ". - -Definition print_error_end2 hct hcl (d1 d2:hdeps): ?? unit - := println (msg_prefix +; msg_error_on_end);; - println "- GRAPH of 2nd bblock";; - DO ext <~ export hct ();; - DO exl <~ export hcl ();; - print_tables ext exl. - -Definition print_error2 hct hcl cr (log: logger unit) (s:pstring): ?? unit - := DO n <~ log_info log ();; - DO ext <~ export hct ();; - DO exl <~ export hcl ();; - println (msg_prefix +; xmsg_number +; n +; " -- " +; s);; - print_witness ext exl cr "2nd";; - println "- GRAPH of 2nd bblock";; - print_tables ext exl. - -Definition simple_debug (x: R.t): ?? option pstring := - DO s <~ string_of_name x;; - RET (Some s). - -Definition log_debug (log: logger unit) (x: R.t): ?? option pstring := - DO i <~ log_info log ();; - DO sx <~ string_of_name x;; - RET (Some (sx +; "@" +; i)). - -Definition hlog (log: logger unit) (hct: hashConsing tree) (hcl: hashConsing list_tree): unit -> ?? unit := - (fun _ => - log_insert log tt ;; - DO s <~ log_info log tt;; - next_log hct s;; - next_log hcl s - ). - -Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool := - DO log1 <~ count_logger ();; - DO log2 <~ count_logger ();; - DO cr <~ make_cref Nothing;; - DO hco_tree <~ mk_annot (hCons tree_hash_eq (msg_tree cr));; - DO hco_list <~ mk_annot (hCons list_tree_hash_eq (msg_list cr));; - DO result1 <~ g_bblock_simu_test - (log_debug log1) - simple_debug - (hlog log1 hco_tree hco_list) - (log_insert log2) - hco_tree _ - hco_list _ - (print_error_end1 hco_tree hco_list) - (print_error1 hco_tree hco_list cr log2) - true - failpreserv_error (* TODO: debug info *) - p1 p2;; - if result1 - then RET true - else - DO log1 <~ count_logger ();; - DO log2 <~ count_logger ();; - DO cr <~ make_cref Nothing;; - DO hco_tree <~ mk_annot (hCons tree_hash_eq (msg_tree cr));; - DO hco_list <~ mk_annot (hCons list_tree_hash_eq (msg_list cr));; - DO result2 <~ g_bblock_simu_test - (log_debug log1) - simple_debug - (hlog log1 hco_tree hco_list) - (log_insert log2) - hco_tree _ - hco_list _ - (print_error_end2 hco_tree hco_list) - (print_error2 hco_tree hco_list cr log2) - false - (fun _ => RET tt) - p2 p1;; - if result2 - then ( - println (msg_prefix +; " OOops - symmetry violation in bblock_simu_test => this is a bug of bblock_simu_test ??");; - RET false - ) else RET false - . -Obligation 1. - generalize (hCons_correct _ _ _ _ H0); clear H0. - constructor 1; wlp_simplify. -Qed. -Obligation 2. - generalize (hCons_correct _ _ _ _ H); clear H. - constructor 1; wlp_simplify. -Qed. -Obligation 3. - generalize (hCons_correct _ _ _ _ H0); clear H0. - constructor 1; wlp_simplify. -Qed. -Obligation 4. - generalize (hCons_correct _ _ _ _ H); clear H. - constructor 1; wlp_simplify. -Qed. - -Theorem verb_bblock_simu_test_correct p1 p2: - WHEN verb_bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2. -Proof. - wlp_simplify. -Qed. -Global Opaque verb_bblock_simu_test. - -End Verbose_version. - - -End ImpDepTree. - -Require Import FMapPositive. - -Module ImpPosDict <: ImpDict with Module R:=Pos. - -Include PosDict. -Import PositiveMap. - -Fixpoint eq_test {A} (d1 d2: t A): ?? bool := - match d1, d2 with - | Leaf _, Leaf _ => RET true - | Node l1 (Some x1) r1, Node l2 (Some x2) r2 => - DO b0 <~ phys_eq x1 x2 ;; - if b0 then - DO b1 <~ eq_test l1 l2 ;; - if b1 then - eq_test r1 r2 - else - RET false - else - RET false - | Node l1 None r1, Node l2 None r2 => - DO b1 <~ eq_test l1 l2 ;; - if b1 then - eq_test r1 r2 - else - RET false - | _, _ => RET false - end. - -Lemma eq_test_correct A d1: forall (d2: t A), - WHEN eq_test d1 d2 ~> b THEN - b=true -> forall x, get d1 x = get d2 x. -Proof. - unfold get; induction d1 as [|l1 Hl1 [x1|] r1 Hr1]; destruct d2 as [|l2 [x2|] r2]; simpl; - wlp_simplify; (discriminate || (subst; destruct x; simpl; auto)). -Qed. -Global Opaque eq_test. - -(* ONLY FOR DEBUGGING INFO: get some key of a non-empty d *) -Fixpoint pick {A} (d: t A): ?? R.t := - match d with - | Leaf _ => FAILWITH "unexpected empty dictionary" - | Node _ (Some _) _ => RET xH - | Node (Leaf _) None r => - DO p <~ pick r;; - RET (xI p) - | Node l None _ => - DO p <~ pick l;; - RET (xO p) - end. - -(* ONLY FOR DEBUGGING INFO: find one variable on which d1 and d2 differs *) -Fixpoint not_eq_witness {A} (d1 d2: t A): ?? option R.t := - match d1, d2 with - | Leaf _, Leaf _ => RET None - | Node l1 (Some x1) r1, Node l2 (Some x2) r2 => - DO b0 <~ phys_eq x1 x2 ;; - if b0 then - DO b1 <~ not_eq_witness l1 l2;; - match b1 with - | None => - DO b2 <~ not_eq_witness r1 r2;; - match b2 with - | None => RET None - | Some p => RET (Some (xI p)) - end - | Some p => RET (Some (xO p)) - end - else - RET (Some xH) - | Node l1 None r1, Node l2 None r2 => - DO b1 <~ not_eq_witness l1 l2;; - match b1 with - | None => - DO b2 <~ not_eq_witness r1 r2;; - match b2 with - | None => RET None - | Some p => RET (Some (xI p)) - end - | Some p => RET (Some (xO p)) - end - | l, Leaf _ => DO p <~ pick l;; RET (Some p) - | Leaf _, r => DO p <~ pick r;; RET (Some p) - | _, _ => RET (Some xH) - end. - -End ImpPosDict. - diff --git a/mppa_k1c/abstractbb/ImpSimuTest.v b/mppa_k1c/abstractbb/ImpSimuTest.v new file mode 100644 index 00000000..8c9c820f --- /dev/null +++ b/mppa_k1c/abstractbb/ImpSimuTest.v @@ -0,0 +1,1108 @@ +(** Implementation of a symbolic execution of sequential semantics of Abstract Basic Blocks + +with imperative hash-consing, and rewriting. + +*) + +Require Export Impure.ImpHCons. +Export Notations. +Import HConsing. + + +Require Export SeqSimuTheory. + +Require Import PArith. + + +Local Open Scope impure. + +Import ListNotations. +Local Open Scope list_scope. + + +Module Type ImpParam. + +Include LangParam. + +Parameter op_eq: op -> op -> ?? bool. + +Parameter op_eq_correct: forall o1 o2, + WHEN op_eq o1 o2 ~> b THEN + b=true -> o1 = o2. + +End ImpParam. + + +Module Type ISeqLanguage. + +Declare Module LP: ImpParam. + +Include MkSeqLanguage LP. + +End ISeqLanguage. + + +Module Type ImpDict. + +Include PseudoRegDictionary. + +Parameter eq_test: forall {A}, t A -> t A -> ?? bool. + +Parameter eq_test_correct: forall A (d1 d2: t A), + WHEN eq_test d1 d2 ~> b THEN + b=true -> forall x, get d1 x = get d2 x. + +(* NB: we could also take an eq_test on R.t (but not really useful with "pure" dictionaries *) + + +(* only for debugging *) +Parameter not_eq_witness: forall {A}, t A -> t A -> ?? option R.t. + +End ImpDict. + + +Module Type ImpSimuInterface. + +Declare Module CoreL: ISeqLanguage. +Import CoreL. +Import Terms. + +Parameter bblock_simu_test: (forall t : term, reduction t) -> bblock -> bblock -> ?? bool. + +Parameter bblock_simu_test_correct: forall (reduce: forall t, reduction t) (p1 p2 : bblock), + WHEN bblock_simu_test reduce p1 p2 ~> b + THEN b = true -> forall ge : genv, bblock_simu ge p1 p2. + + +Parameter verb_bblock_simu_test + : (forall t : term, reduction t) -> + (R.t -> ?? pstring) -> + (op -> ?? pstring) -> bblock -> bblock -> ?? bool. + +Parameter verb_bblock_simu_test_correct: + forall (reduce: forall t, reduction t) + (string_of_name : R.t -> ?? pstring) + (string_of_op : op -> ?? pstring) + (p1 p2 : bblock), + WHEN verb_bblock_simu_test reduce string_of_name string_of_op p1 p2 ~> b + THEN b = true -> forall ge : genv, bblock_simu ge p1 p2. + +End ImpSimuInterface. + + + +Module ImpSimu (L: ISeqLanguage) (Dict: ImpDict with Module R:=L.LP.R): ImpSimuInterface with Module CoreL := L. + +Module CoreL:=L. + +Module ST := SimuTheory L Dict. + +Import ST. + +Definition term_set_hid (t: term) (hid: hashcode): term := + match t with + | Input x _ => Input x hid + | App op l _ => App op l hid + end. + +Definition list_term_set_hid (l: list_term) (hid: hashcode): list_term := + match l with + | LTnil _ => LTnil hid + | LTcons t l' _ => LTcons t l' hid + end. + +Lemma term_eval_set_hid ge t hid m: + term_eval ge (term_set_hid t hid) m = term_eval ge t m. +Proof. + destruct t; simpl; auto. +Qed. + +Lemma list_term_eval_set_hid ge l hid m: + list_term_eval ge (list_term_set_hid l hid) m = list_term_eval ge l m. +Proof. + destruct l; simpl; auto. +Qed. + +(* Local nickname *) +Module D:=ImpPrelude.Dict. + +Section SimuWithReduce. + +Variable reduce: forall t, reduction t. + +Section CanonBuilding. + +Variable hC_term: hashinfo term -> ?? term. +Hypothesis hC_term_correct: forall t, WHEN hC_term t ~> t' THEN forall ge m, term_eval ge (hdata t) m = term_eval ge t' m. + +Variable hC_list_term: hashinfo list_term -> ?? list_term. +Hypothesis hC_list_term_correct: forall t, WHEN hC_list_term t ~> t' THEN forall ge m, list_term_eval ge (hdata t) m = list_term_eval ge t' m. + +(* First, we wrap constructors for hashed values !*) + +Local Open Scope positive. +Local Open Scope list_scope. + +Definition hInput_hcodes (x:R.t) := + DO hc <~ hash 1;; + DO hv <~ hash x;; + RET [hc;hv]. +Extraction Inline hInput_hcodes. + +Definition hInput (x:R.t): ?? term := + DO hv <~ hInput_hcodes x;; + hC_term {| hdata:=Input x unknown_hid; hcodes :=hv; |}. + +Lemma hInput_correct x: + WHEN hInput x ~> t THEN forall ge m, term_eval ge t m = Some (m x). +Proof. + wlp_simplify. +Qed. +Global Opaque hInput. +Hint Resolve hInput_correct: wlp. + +Definition hApp_hcodes (o:op) (l: list_term) := + DO hc <~ hash 2;; + DO hv <~ hash o;; + RET [hc;hv;list_term_get_hid l]. +Extraction Inline hApp_hcodes. + +Definition hApp (o:op) (l: list_term) : ?? term := + DO hv <~ hApp_hcodes o l;; + hC_term {| hdata:=App o l unknown_hid; hcodes:=hv |}. + +Lemma hApp_correct o l: + WHEN hApp o l ~> t THEN forall ge m, + term_eval ge t m = match list_term_eval ge l m with + | Some v => op_eval ge o v + | None => None + end. +Proof. + wlp_simplify. +Qed. +Global Opaque hApp. +Hint Resolve hApp_correct: wlp. + +Definition hLTnil (_: unit): ?? list_term := + hC_list_term {| hdata:=LTnil unknown_hid; hcodes := nil; |} . + +Lemma hLTnil_correct x: + WHEN hLTnil x ~> l THEN forall ge m, list_term_eval ge l m = Some nil. +Proof. + wlp_simplify. +Qed. +Global Opaque hLTnil. +Hint Resolve hLTnil_correct: wlp. + + +Definition hLTcons (t: term) (l: list_term): ?? list_term := + hC_list_term {| hdata:=LTcons t l unknown_hid; hcodes := [term_get_hid t; list_term_get_hid l]; |}. + +Lemma hLTcons_correct t l: + WHEN hLTcons t l ~> l' THEN forall ge m, + list_term_eval ge l' m = match term_eval ge t m, list_term_eval ge l m with + | Some v, Some lv => Some (v::lv) + | _, _ => None + end. +Proof. + wlp_simplify. +Qed. +Global Opaque hLTcons. +Hint Resolve hLTcons_correct: wlp. + +(* Second, we use these hashed constructors ! *) + +Record hsmem:= {hpre: list term; hpost: Dict.t term}. + +Coercion hpost: hsmem >-> Dict.t. + +Definition hsmem_get (d:hsmem) x: ?? term := + match Dict.get d x with + | None => hInput x + | Some t => RET t + end. + +Lemma hsmem_get_correct (d:hsmem) x: + WHEN hsmem_get d x ~> t THEN forall ge m, term_eval ge t m = smem_eval ge d x m. +Proof. + unfold hsmem_get, smem_eval, smem_get; destruct (Dict.get d x); wlp_simplify. +Qed. +Global Opaque hsmem_get. +Hint Resolve hsmem_get_correct: wlp. + +Definition smem_model ge (d: smem) (hd:hsmem): Prop := + (forall m, allvalid ge hd.(hpre) m <-> svalid ge d m) + /\ (forall m x, svalid ge d m -> smem_eval ge hd x m = (smem_eval ge d x m)). + +Lemma smem_model_svalid_alt ge d hd: smem_model ge d hd -> + forall m x, svalid ge d m -> smem_eval ge hd x m <> None. +Proof. + intros (H1 & H2) m x H. rewrite H2; auto. + unfold svalid in H. intuition eauto. +Qed. + +Lemma smem_model_allvalid_alt ge d hd: smem_model ge d hd -> + forall m x, allvalid ge hd.(hpre) m -> smem_eval ge hd x m <> None. +Proof. + intros (H1 & H2) m x H. eapply smem_model_svalid_alt. + - split; eauto. + - rewrite <- H1; auto. +Qed. + +Definition naive_set (hd:hsmem) x (t:term) := + {| hpre:= t::hd.(hpre); hpost:=Dict.set hd x t |}. + +Lemma naive_set_correct hd x ht ge d t: + smem_model ge d hd -> + (forall m, svalid ge d m -> term_eval ge ht m = term_eval ge t m) -> + smem_model ge (smem_set d x t) (naive_set hd x ht). +Proof. + unfold naive_set; intros (DM0 & DM1) EQT; split. + - intros m. + destruct (DM0 m) as (PRE & VALID0); clear DM0. + assert (VALID1: allvalid ge hd.(hpre) m -> pre d ge m). { unfold svalid in PRE; tauto. } + assert (VALID2: allvalid ge hd.(hpre) m -> forall x : Dict.R.t, smem_eval ge d x m <> None). { unfold svalid in PRE; tauto. } + unfold allvalid in * |- *; simpl. + intuition (subst; eauto). + + eapply svalid_set_proof; eauto. + erewrite <- EQT; eauto. + + exploit svalid_set_decompose_1; eauto. + intros X1; exploit svalid_set_decompose_2; eauto. + rewrite <- EQT; eauto. + + exploit svalid_set_decompose_1; eauto. + - clear DM0. unfold smem_eval, smem_eval, smem_get in * |- *; simpl. + Local Hint Resolve svalid_set_decompose_1. + intros; case (R.eq_dec x x0). + + intros; subst; rewrite !Dict.set_spec_eq; simpl; eauto. + + intros; rewrite !Dict.set_spec_diff; simpl; eauto. +Qed. +Local Hint Resolve naive_set_correct. + +Definition equiv_hsmem ge (hd1 hd2: hsmem) := + (forall m, allvalid ge hd1.(hpre) m <-> allvalid ge hd2.(hpre) m) + /\ (forall m x, allvalid ge hd1.(hpre) m -> smem_eval ge hd1 x m = smem_eval ge hd2 x m). + +Lemma equiv_smem_symmetry ge hd1 hd2: + equiv_hsmem ge hd1 hd2 -> equiv_hsmem ge hd2 hd1. +Proof. + intros (V1 & P1); split. + - intros; symmetry; auto. + - intros; symmetry; eapply P1. rewrite V1; auto. +Qed. + +Lemma equiv_hsmem_models ge hd1 hd2 d: + smem_model ge d hd1 -> equiv_hsmem ge hd1 hd2 -> smem_model ge d hd2. +Proof. + intros (VALID & EQUIV) (HEQUIV & PEQUIV); split. + - intros m; rewrite <- VALID; auto. symmetry; auto. + - intros m x H. rewrite <- EQUIV; auto. + rewrite PEQUIV; auto. + rewrite VALID; auto. +Qed. + +Variable log_assign: R.t -> term -> ?? unit. + +Definition lift {A B} hid (x:A) (k: B -> ?? A) (y:B): ?? A := + DO b <~ phys_eq hid unknown_hid;; + if b then k y else RET x. + +Fixpoint hterm_lift (t: term): ?? term := + match t with + | Input x hid => lift hid t hInput x + | App o l hid => + lift hid t + (fun l => DO lt <~ hlist_term_lift l;; + hApp o lt) l + end +with hlist_term_lift (l: list_term) {struct l}: ?? list_term := + match l with + | LTnil hid => lift hid l hLTnil () + | LTcons t l' hid => + lift hid l + (fun t => DO t <~ hterm_lift t;; + DO lt <~ hlist_term_lift l';; + hLTcons t lt) t + end. + +Lemma hterm_lift_correct t: + WHEN hterm_lift t ~> ht THEN forall ge m, term_eval ge ht m = term_eval ge t m. +Proof. + induction t using term_mut with (P0:=fun lt => + WHEN hlist_term_lift lt ~> hlt THEN forall ge m, list_term_eval ge hlt m = list_term_eval ge lt m); + wlp_simplify. + - rewrite H0, H; auto. + - rewrite H1, H0, H; auto. +Qed. +Local Hint Resolve hterm_lift_correct: wlp. +Global Opaque hterm_lift. + +Variable log_new_hterm: term -> ?? unit. + +Fixpoint hterm_append (l: list term) (lh: list term): ?? list term := + match l with + | nil => RET lh + | t::l' => + DO ht <~ hterm_lift t;; + log_new_hterm ht;; + hterm_append l' (ht::lh) + end. + +Lemma hterm_append_correct l: forall lh, + WHEN hterm_append l lh ~> lh' THEN (forall ge m, allvalid ge lh' m <-> (allvalid ge l m /\ allvalid ge lh m)). +Proof. + Local Hint Resolve eq_trans: localhint. + unfold allvalid; induction l as [|t l']; simpl; wlp_xsimplify ltac:(eauto with wlp). + intros REC ge m; rewrite REC; clear IHl' REC. intuition (subst; eauto with wlp localhint). +Qed. +(*Local Hint Resolve hterm_append_correct: wlp.*) +Global Opaque hterm_append. + +Definition smart_set (hd:hsmem) x (ht:term) := + match ht with + | Input _ _ => + DO ot <~ hsmem_get hd x;; + DO b <~ phys_eq ot ht;; + if b then + RET (hd.(hpost)) + else ( + log_assign x ht;; + RET (Dict.set hd x ht) + ) + | _ => + log_assign x ht;; + RET (Dict.set hd x ht) + end. + +Lemma smart_set_correct hd x ht: + WHEN smart_set hd x ht ~> d THEN + forall ge m y, smem_eval ge d y m = smem_eval ge (Dict.set hd x ht) y m. +Proof. + destruct ht; wlp_simplify. + unfold smem_eval at 2; unfold smem_get; simpl; case (R.eq_dec x y). + - intros; subst. rewrite Dict.set_spec_eq. congruence. + - intros; rewrite Dict.set_spec_diff; auto. +Qed. +(*Local Hint Resolve smart_set_correct: wlp.*) +Global Opaque smart_set. + +Definition hsmem_set (hd:hsmem) x (t:term) := + DO pt <~ reduce t;; + DO lht <~ hterm_append pt.(valid) hd.(hpre);; + DO ht <~ hterm_lift pt.(effect);; + log_new_hterm ht;; + DO nd <~ smart_set hd x ht;; + RET {| hpre := lht; hpost := nd |}. + +Lemma hsmem_set_correct hd x ht: + WHEN hsmem_set hd x ht ~> nhd THEN + forall ge d t, smem_model ge d hd -> + (forall m, svalid ge d m -> term_eval ge ht m = term_eval ge t m) -> + smem_model ge (smem_set d x t) nhd. +Proof. + intros; wlp_simplify. + generalize (hterm_append_correct _ _ _ Hexta0); intro APPEND. + generalize (hterm_lift_correct _ _ Hexta1); intro LIFT. + generalize (smart_set_correct _ _ _ _ Hexta3); intro SMART. + eapply equiv_hsmem_models; eauto; unfold equiv_hsmem; simpl. + destruct H as (VALID & EFFECT); split. + - intros; rewrite APPEND, <- VALID. + unfold allvalid; simpl; intuition (subst; eauto). + - intros m x0 ALLVALID; rewrite SMART. + destruct (term_eval ge ht m) eqn: Hht. + * case (R.eq_dec x x0). + + intros; subst. unfold smem_eval; unfold smem_get; simpl. rewrite !Dict.set_spec_eq. + erewrite LIFT, EFFECT; eauto. + + intros; unfold smem_eval; unfold smem_get; simpl. rewrite !Dict.set_spec_diff; auto. + * destruct (ALLVALID ht); simpl; auto. +Qed. +Local Hint Resolve hsmem_set_correct: wlp. +Global Opaque hsmem_set. + +Lemma exp_hterm_correct ge e hod od: + smem_model ge od hod -> + forall hd d, + smem_model ge d hd -> + forall m, svalid ge d m -> svalid ge od m -> term_eval ge (exp_term e hd hod) m = term_eval ge (exp_term e d od) m. +Proof. + intro H. + induction e using exp_mut with (P0:=fun le => forall d hd, + smem_model ge d hd -> forall m, svalid ge d m -> svalid ge od m -> list_term_eval ge (list_exp_term le hd hod) m = list_term_eval ge (list_exp_term le d od) m); + unfold smem_model in * |- * ; simpl; intuition eauto. + - erewrite IHe; eauto. + - erewrite IHe0, IHe; eauto. +Qed. +Local Hint Resolve exp_hterm_correct: wlp. + +Fixpoint hinst_smem (i: inst) (hd hod: hsmem): ?? hsmem := + match i with + | nil => RET hd + | (x, e)::i' => + DO nd <~ hsmem_set hd x (exp_term e hd hod);; + hinst_smem i' nd hod + end. + +Lemma hinst_smem_correct i: forall hd hod, + WHEN hinst_smem i hd hod ~> hd' THEN + forall ge od d, smem_model ge od hod -> smem_model ge d hd -> (forall m, svalid ge d m -> svalid ge od m) -> smem_model ge (inst_smem i d od) hd'. +Proof. + Local Hint Resolve svalid_set_proof. + induction i; simpl; wlp_simplify; eauto 15 with wlp. +Qed. +Global Opaque hinst_smem. +Local Hint Resolve hinst_smem_correct: wlp. + +(* logging info: we log the number of inst-instructions passed ! *) +Variable log_new_inst: unit -> ?? unit. + +Fixpoint hbblock_smem_rec (p: bblock) (d: hsmem): ?? hsmem := + match p with + | nil => RET d + | i::p' => + log_new_inst tt;; + DO d' <~ hinst_smem i d d;; + hbblock_smem_rec p' d' + end. + +Lemma hbblock_smem_rec_correct p: forall hd, + WHEN hbblock_smem_rec p hd ~> hd' THEN forall ge d, smem_model ge d hd -> smem_model ge (bblock_smem_rec p d) hd'. +Proof. + induction p; simpl; wlp_simplify. +Qed. +Global Opaque hbblock_smem_rec. +Local Hint Resolve hbblock_smem_rec_correct: wlp. + + +Definition hbblock_smem: bblock -> ?? hsmem + := fun p => hbblock_smem_rec p {| hpre:= nil ; hpost := Dict.empty |}. + +Lemma hbblock_smem_correct p: + WHEN hbblock_smem p ~> hd THEN forall ge, smem_model ge (bblock_smem p) hd. +Proof. + unfold bblock_smem; wlp_simplify. eapply H. clear H. + unfold smem_model, svalid, smem_eval, allvalid, smem_eval, smem_get; simpl; intuition; + rewrite !Dict.empty_spec in * |- *; simpl in * |- *; try congruence. +Qed. +Global Opaque hbblock_smem. + +End CanonBuilding. + +(* Now, we build the hash-Cons value from a "hash_eq". + +Informal specification: + [hash_eq] must be consistent with the "hashed" constructors defined above. + +We expect that hashinfo values in the code of these "hashed" constructors verify: + + (hash_eq (hdata x) (hdata y) ~> true) <-> (hcodes x)=(hcodes y) + +*) + +Definition term_hash_eq (ta tb: term): ?? bool := + match ta, tb with + | Input xa _, Input xb _ => + if R.eq_dec xa xb (* Inefficient in some cases ? *) + then RET true + else RET false + | App oa lta _, App ob ltb _ => + DO b <~ op_eq oa ob ;; + if b then phys_eq lta ltb + else RET false + | _,_ => RET false + end. + +Lemma term_hash_eq_correct: forall ta tb, WHEN term_hash_eq ta tb ~> b THEN b=true -> term_set_hid ta unknown_hid=term_set_hid tb unknown_hid. +Proof. + Local Hint Resolve op_eq_correct: wlp. + destruct ta, tb; wlp_simplify; (discriminate || (subst; auto)). +Qed. +Global Opaque term_hash_eq. +Hint Resolve term_hash_eq_correct: wlp. + +Definition list_term_hash_eq (lta ltb: list_term): ?? bool := + match lta, ltb with + | LTnil _, LTnil _ => RET true + | LTcons ta lta _, LTcons tb ltb _ => + DO b <~ phys_eq ta tb ;; + if b then phys_eq lta ltb + else RET false + | _,_ => RET false + end. + +Lemma list_term_hash_eq_correct: forall lta ltb, WHEN list_term_hash_eq lta ltb ~> b THEN b=true -> list_term_set_hid lta unknown_hid=list_term_set_hid ltb unknown_hid. +Proof. + destruct lta, ltb; wlp_simplify; (discriminate || (subst; auto)). +Qed. +Global Opaque list_term_hash_eq. +Hint Resolve list_term_hash_eq_correct: wlp. + +Lemma smem_eval_intro (d1 d2: hsmem): + (forall x, Dict.get d1 x = Dict.get d2 x) -> (forall ge x m, smem_eval ge d1 x m = smem_eval ge d2 x m). +Proof. + unfold smem_eval, smem_get; intros H ge x m; rewrite H. destruct (Dict.get d2 x); auto. +Qed. + +Local Hint Resolve hbblock_smem_correct Dict.eq_test_correct: wlp. + +Program Definition mk_hash_params (log: term -> ?? unit): Dict.hash_params term := + {| + Dict.test_eq := phys_eq; + Dict.hashing := fun (ht: term) => RET (term_get_hid ht); + Dict.log := log |}. +Obligation 1. + eauto with wlp. +Qed. + +(*** A GENERIC EQ_TEST: IN ORDER TO SUPPORT SEVERAL DEBUGGING MODE !!! ***) +Definition no_log_assign (x:R.t) (t:term): ?? unit := RET tt. +Definition no_log_new_term (t:term): ?? unit := RET tt. + +Section Prog_Eq_Gen. + +Variable log_assign: R.t -> term -> ?? unit. +Variable log_new_term: hashConsing term -> hashConsing list_term -> ??(term -> ?? unit). +Variable log_inst1: unit -> ?? unit. (* log of p1 insts *) +Variable log_inst2: unit -> ?? unit. (* log of p2 insts *) + +Variable hco_term: hashConsing term. +Hypothesis hco_term_correct: forall t, WHEN hco_term.(hC) t ~> t' THEN forall ge m, term_eval ge (hdata t) m = term_eval ge t' m. + +Variable hco_list: hashConsing list_term. +Hypothesis hco_list_correct: forall t, WHEN hco_list.(hC) t ~> t' THEN forall ge m, list_term_eval ge (hdata t) m = list_term_eval ge t' m. + +Variable print_error_end: hsmem -> hsmem -> ?? unit. +Variable print_error: pstring -> ?? unit. + +Variable check_failpreserv: bool. +Variable dbg_failpreserv: term -> ?? unit. (* info of additional failure of the output bbloc p2 wrt the input bbloc p1 *) + +Program Definition g_bblock_simu_test (p1 p2: bblock): ?? bool := + DO failure_in_failpreserv <~ make_cref false;; + DO r <~ (TRY + DO d1 <~ hbblock_smem hco_term.(hC) hco_list.(hC) log_assign no_log_new_term log_inst1 p1;; + DO log_new_term <~ log_new_term hco_term hco_list;; + DO d2 <~ hbblock_smem hco_term.(hC) hco_list.(hC) no_log_assign log_new_term log_inst2 p2;; + DO b <~ Dict.eq_test d1 d2 ;; + if b then ( + if check_failpreserv then ( + let hp := mk_hash_params dbg_failpreserv in + failure_in_failpreserv.(set)(true);; + Sets.assert_list_incl hp d2.(hpre) d1.(hpre);; + RET true + ) else RET false + ) else ( + print_error_end d1 d2 ;; + RET false + ) + CATCH_FAIL s, _ => + DO b <~ failure_in_failpreserv.(get)();; + if b then RET false + else print_error s;; RET false + ENSURE (fun b => b=true -> forall ge, bblock_simu ge p1 p2));; + RET (`r). +Obligation 1. + constructor 1; wlp_simplify; try congruence. + destruct (H ge) as (EQPRE1&EQPOST1); destruct (H0 ge) as (EQPRE2&EQPOST2); clear H H0. + apply bblock_smem_simu; auto. + + intros m; rewrite <- EQPRE1, <- EQPRE2. + unfold incl, allvalid in * |- *; intuition eauto. + + intros m0 x m1 VALID; rewrite <- EQPOST1, <- EQPOST2; auto. + erewrite smem_eval_intro; eauto. + erewrite <- EQPRE2; auto. + erewrite <- EQPRE1 in VALID. + unfold incl, allvalid in * |- *; intuition eauto. +Qed. + +Theorem g_bblock_simu_test_correct p1 p2: + WHEN g_bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2. +Proof. + wlp_simplify. + destruct exta0; simpl in * |- *; auto. +Qed. +Global Opaque g_bblock_simu_test. + +End Prog_Eq_Gen. + + + +Definition hht: hashH term := {| hash_eq := term_hash_eq; get_hid:=term_get_hid; set_hid:=term_set_hid |}. +Definition hlht: hashH list_term := {| hash_eq := list_term_hash_eq; get_hid:=list_term_get_hid; set_hid:=list_term_set_hid |}. + +Definition recover_hcodes (t:term): ??(hashinfo term) := + match t with + | Input x _ => + DO hv <~ hInput_hcodes x ;; + RET {| hdata := t; hcodes := hv |} + | App o l _ => + DO hv <~ hApp_hcodes o l ;; + RET {| hdata := t; hcodes := hv |} + end. + + +Definition msg_end_of_bblock: pstring :="--- unknown subterms in the graph". + +Definition log_new_term + (unknownHash_msg: term -> ?? pstring) + (hct:hashConsing term) + (hcl:hashConsing list_term) + : ?? (term -> ?? unit) := + DO clock <~ hct.(next_hid)();; + hct.(next_log) msg_end_of_bblock;; + hcl.(next_log) msg_end_of_bblock;; + RET (fun t => + DO ok <~ hash_older (term_get_hid t) clock;; + if ok + then + RET tt + else + DO ht <~ recover_hcodes t;; + hct.(remove) ht;; + DO msg <~ unknownHash_msg t;; + FAILWITH msg). + +Definition skip (_:unit): ?? unit := RET tt. + +Definition msg_prefix: pstring := "*** ERROR INFO from bblock_simu_test: ". +Definition msg_error_on_end: pstring := "mismatch in final assignments !". +Definition msg_unknow_term: pstring := "unknown term". +Definition msg_number: pstring := "on 2nd bblock -- on inst num ". +Definition msg_notfailpreserv: pstring := "a possible failure of 2nd bblock is absent in 1st bblock (INTERNAL ERROR: this error is expected to be detected before!!!)". + +Definition print_error_end (_ _: hsmem): ?? unit + := println (msg_prefix +; msg_error_on_end). + +Definition print_error (log: logger unit) (s:pstring): ?? unit + := DO n <~ log_info log ();; + println (msg_prefix +; msg_number +; n +; " -- " +; s). + +Definition failpreserv_error (_: term): ?? unit + := println (msg_prefix +; msg_notfailpreserv). + +Lemma term_eval_set_hid_equiv ge t1 t2 hid1 hid2 m: + term_set_hid t1 hid1 = term_set_hid t2 hid2 -> term_eval ge t1 m = term_eval ge t2 m. +Proof. + intro H; erewrite <- term_eval_set_hid; rewrite H. apply term_eval_set_hid. +Qed. + +Lemma list_term_eval_set_hid_equiv ge t1 t2 hid1 hid2 m: + list_term_set_hid t1 hid1 = list_term_set_hid t2 hid2 -> list_term_eval ge t1 m = list_term_eval ge t2 m. +Proof. + intro H; erewrite <- list_term_eval_set_hid; rewrite H. apply list_term_eval_set_hid. +Qed. + +Local Hint Resolve term_eval_set_hid_equiv list_term_eval_set_hid_equiv. + +Program Definition bblock_simu_test (p1 p2: bblock): ?? bool := + DO log <~ count_logger ();; + DO hco_term <~ mk_annot (hCons hht);; + DO hco_list <~ mk_annot (hCons hlht);; + g_bblock_simu_test + no_log_assign + (log_new_term (fun _ => RET msg_unknow_term)) + skip + (log_insert log) + hco_term _ + hco_list _ + print_error_end + (print_error log) + true (* check_failpreserv *) + failpreserv_error + p1 p2. +Obligation 1. + generalize (hCons_correct _ _ _ H0); clear H0. + wlp_simplify. +Qed. +Obligation 2. + generalize (hCons_correct _ _ _ H); clear H. + wlp_simplify. +Qed. + +Local Hint Resolve g_bblock_simu_test_correct. + +Theorem bblock_simu_test_correct p1 p2: + WHEN bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2. +Proof. + wlp_simplify. +Qed. +Global Opaque bblock_simu_test. + +(** This is only to print info on each bblock_simu_test run **) +Section Verbose_version. + +Variable string_of_name: R.t -> ?? pstring. +Variable string_of_op: op -> ?? pstring. + + +Local Open Scope string_scope. + +Definition string_term_hid (t: term): ?? pstring := + DO id <~ string_of_hashcode (term_get_hid t);; + RET ("E" +; (CamlStr id)). + +Definition string_list_hid (lt: list_term): ?? pstring := + DO id <~ string_of_hashcode (list_term_get_hid lt);; + RET ("L" +; (CamlStr id)). + +Definition print_raw_term (t: term): ?? unit := + match t with + | Input x _ => + DO s <~ string_of_name x;; + println( "init_access " +; s) + | App o (LTnil _) _ => + DO so <~ string_of_op o;; + println so + | App o l _ => + DO so <~ string_of_op o;; + DO sl <~ string_list_hid l;; + println (so +; " " +; sl) + end. + +(* +Definition print_raw_list(lt: list_term): ?? unit := + match lt with + | LTnil _=> println "" + | LTcons t l _ => + DO st <~ string_term_hid t;; + DO sl <~ string_list_hid l;; + println(st +; " " +; sl) + end. +*) + +Section PrettryPrint. + +Variable get_debug_info: term -> ?? option pstring. + +Fixpoint string_of_term (t: term): ?? pstring := + match t with + | Input x _ => string_of_name x + | App o (LTnil _) _ => string_of_op o + | App o l _ => + DO so <~ string_of_op o;; + DO sl <~ string_of_list_term l;; + RET (so +; "[" +; sl +; "]") + end +with string_of_list_term (l: list_term): ?? pstring := + match l with + | LTnil _ => RET (Str "") + | LTcons t (LTnil _) _ => + DO dbg <~ get_debug_info t;; + match dbg with + | Some x => RET x + | None => string_of_term t + end + | LTcons t l' _ => + DO st <~ (DO dbg <~ get_debug_info t;; + match dbg with + | Some x => RET x + | None => string_of_term t + end);; + DO sl <~ string_of_list_term l';; + RET (st +; ";" +; sl) + end. + + +End PrettryPrint. + + +Definition pretty_term gdi t := + DO r <~ string_of_term gdi t;; + println(r). + +Fixpoint print_head (head: list pstring): ?? unit := + match head with + | i::head' => println (i);; print_head head' + | _ => RET tt + end. + +Definition print_term gdi (head: list pstring) (t: term): ?? unit := + print_head head;; + DO s <~ string_term_hid t;; + print (s +; ": ");; + print_raw_term t;; + DO dbg <~ gdi t;; + match dbg with + | Some x => + print("// " +; x +; " <- ");; + pretty_term gdi t + | None => RET tt + end. + +Definition print_list gdi (head: list pstring) (lt: list_term): ?? unit := + print_head head;; + DO s <~ string_list_hid lt ;; + print (s +; ": ");; + (* print_raw_list lt;; *) + DO ps <~ string_of_list_term gdi lt;; + println("[" +; ps +; "]"). + + +Definition print_tables gdi ext exl: ?? unit := + println "-- term table --" ;; + iterall ext (fun head _ pt => print_term gdi head pt.(hdata));; + println "-- list table --" ;; + iterall exl (fun head _ pl => print_list gdi head pl.(hdata));; + println "----------------". + +Definition print_final_debug gdi (d1 d2: hsmem): ?? unit + := DO b <~ Dict.not_eq_witness d1 d2 ;; + match b with + | Some x => + DO s <~ string_of_name x;; + println("mismatch on: " +; s);; + match Dict.get d1 x with + | None => println("=> unassigned in 1st bblock") + | Some t1 => + print("=> node expected from 1st bblock: ");; + pretty_term gdi t1 + end;; + match Dict.get d2 x with + | None => println("=> unassigned in 2nd bblock") + | Some t2 => + print("=> node found from 2nd bblock: ");; + pretty_term gdi t2 + end + | None => FAILWITH "bug in Dict.not_eq_witness ?" + end. + +Definition witness:= option term. + +Definition msg_term (cr: cref witness) t := + set cr (Some t);; + RET msg_unknow_term. + +Definition print_witness gdi cr (*msg*) := + DO wit <~ get cr ();; + match wit with + | Some t => + println("=> unknown term node: ");; + pretty_term gdi t (*;; + println("=> encoded on " +; msg +; " graph as: ");; + print_raw_term t *) + | None => println "Unexpected failure: no witness info (hint: hash-consing bug ?)" + end. + + +Definition print_error_end1 gdi hct hcl (d1 d2:hsmem): ?? unit + := println "- GRAPH of 1st bblock";; + DO ext <~ export hct ();; + DO exl <~ export hcl ();; + print_tables gdi ext exl;; + print_error_end d1 d2;; + print_final_debug gdi d1 d2. + +Definition print_error1 gdi hct hcl cr log s : ?? unit + := println "- GRAPH of 1st bblock";; + DO ext <~ export hct ();; + DO exl <~ export hcl ();; + print_tables gdi ext exl;; + print_error log s;; + print_witness gdi cr (*"1st"*). + + +Definition xmsg_number: pstring := "on 1st bblock -- on inst num ". + +Definition print_error_end2 gdi hct hcl (d1 d2:hsmem): ?? unit + := println (msg_prefix +; msg_error_on_end);; + println "- GRAPH of 2nd bblock";; + DO ext <~ export hct ();; + DO exl <~ export hcl ();; + print_tables gdi ext exl. + +Definition print_error2 gdi hct hcl cr (log: logger unit) (s:pstring): ?? unit + := DO n <~ log_info log ();; + DO ext <~ export hct ();; + DO exl <~ export hcl ();; + println (msg_prefix +; xmsg_number +; n +; " -- " +; s);; + print_witness gdi cr (*"2nd"*);; + println "- GRAPH of 2nd bblock";; + print_tables gdi ext exl. + +(* USELESS +Definition simple_log_assign (d: D.t term pstring) (x: R.t) (t: term): ?? unit := + DO s <~ string_of_name x;; + d.(D.set) (t,s). +*) + +Definition log_assign (d: D.t term pstring) (log: logger unit) (x: R.t) (t: term): ?? unit := + DO i <~ log_info log ();; + DO sx <~ string_of_name x;; + d.(D.set) (t,(sx +; "@" +; i)). + +Definition msg_new_inst : pstring := "--- inst ". + +Definition hlog (log: logger unit) (hct: hashConsing term) (hcl: hashConsing list_term): unit -> ?? unit := + (fun _ => + log_insert log tt ;; + DO s <~ log_info log tt;; + let s:= msg_new_inst +; s in + next_log hct s;; + next_log hcl s + ). + +Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool := + DO dict_info <~ make_dict (mk_hash_params (fun _ => RET tt));; + DO log1 <~ count_logger ();; + DO log2 <~ count_logger ();; + DO cr <~ make_cref None;; + DO hco_term <~ mk_annot (hCons hht);; + DO hco_list <~ mk_annot (hCons hlht);; + DO result1 <~ g_bblock_simu_test + (log_assign dict_info log1) + (log_new_term (msg_term cr)) + (hlog log1 hco_term hco_list) + (log_insert log2) + hco_term _ + hco_list _ + (print_error_end1 dict_info.(D.get) hco_term hco_list) + (print_error1 dict_info.(D.get) hco_term hco_list cr log2) + true + failpreserv_error + p1 p2;; + if result1 + then RET true + else + DO dict_info <~ make_dict (mk_hash_params (fun _ => RET tt));; + DO log1 <~ count_logger ();; + DO log2 <~ count_logger ();; + DO cr <~ make_cref None;; + DO hco_term <~ mk_annot (hCons hht);; + DO hco_list <~ mk_annot (hCons hlht);; + DO result2 <~ g_bblock_simu_test + (log_assign dict_info log1) + (log_new_term (msg_term cr)) + (hlog log1 hco_term hco_list) + (log_insert log2) + hco_term _ + hco_list _ + (print_error_end2 dict_info.(D.get) hco_term hco_list) + (print_error2 dict_info.(D.get) hco_term hco_list cr log2) + false + (fun _ => RET tt) + p2 p1;; + if result2 + then ( + println (msg_prefix +; " OOops - symmetry violation in bblock_simu_test => this is a bug of bblock_simu_test ??");; + RET false + ) else RET false + . +Obligation 1. + generalize (hCons_correct _ _ _ H0); clear H0. + wlp_simplify. +Qed. +Obligation 2. + generalize (hCons_correct _ _ _ H); clear H. + wlp_simplify. +Qed. +Obligation 3. + generalize (hCons_correct _ _ _ H0); clear H0. + wlp_simplify. +Qed. +Obligation 4. + generalize (hCons_correct _ _ _ H); clear H. + wlp_simplify. +Qed. + +Theorem verb_bblock_simu_test_correct p1 p2: + WHEN verb_bblock_simu_test p1 p2 ~> b THEN b=true -> forall ge, bblock_simu ge p1 p2. +Proof. + wlp_simplify. +Qed. +Global Opaque verb_bblock_simu_test. + +End Verbose_version. + +End SimuWithReduce. + +(* TODO: why inlining fails here ? *) +Transparent hterm_lift. +Extraction Inline lift. + +End ImpSimu. + +Require Import FMapPositive. + +Module ImpPosDict <: ImpDict with Module R:=Pos. + +Include PosDict. +Import PositiveMap. + +Fixpoint eq_test {A} (d1 d2: t A): ?? bool := + match d1, d2 with + | Leaf _, Leaf _ => RET true + | Node l1 (Some x1) r1, Node l2 (Some x2) r2 => + DO b0 <~ phys_eq x1 x2 ;; + if b0 then + DO b1 <~ eq_test l1 l2 ;; + if b1 then + eq_test r1 r2 + else + RET false + else + RET false + | Node l1 None r1, Node l2 None r2 => + DO b1 <~ eq_test l1 l2 ;; + if b1 then + eq_test r1 r2 + else + RET false + | _, _ => RET false + end. + +Lemma eq_test_correct A d1: forall (d2: t A), + WHEN eq_test d1 d2 ~> b THEN + b=true -> forall x, get d1 x = get d2 x. +Proof. + unfold get; induction d1 as [|l1 Hl1 [x1|] r1 Hr1]; destruct d2 as [|l2 [x2|] r2]; simpl; + wlp_simplify; (discriminate || (subst; destruct x; simpl; auto)). +Qed. +Global Opaque eq_test. + +(* ONLY FOR DEBUGGING INFO: get some key of a non-empty d *) +Fixpoint pick {A} (d: t A): ?? R.t := + match d with + | Leaf _ => FAILWITH "unexpected empty dictionary" + | Node _ (Some _) _ => RET xH + | Node (Leaf _) None r => + DO p <~ pick r;; + RET (xI p) + | Node l None _ => + DO p <~ pick l;; + RET (xO p) + end. + +(* ONLY FOR DEBUGGING INFO: find one variable on which d1 and d2 differs *) +Fixpoint not_eq_witness {A} (d1 d2: t A): ?? option R.t := + match d1, d2 with + | Leaf _, Leaf _ => RET None + | Node l1 (Some x1) r1, Node l2 (Some x2) r2 => + DO b0 <~ phys_eq x1 x2 ;; + if b0 then + DO b1 <~ not_eq_witness l1 l2;; + match b1 with + | None => + DO b2 <~ not_eq_witness r1 r2;; + match b2 with + | None => RET None + | Some p => RET (Some (xI p)) + end + | Some p => RET (Some (xO p)) + end + else + RET (Some xH) + | Node l1 None r1, Node l2 None r2 => + DO b1 <~ not_eq_witness l1 l2;; + match b1 with + | None => + DO b2 <~ not_eq_witness r1 r2;; + match b2 with + | None => RET None + | Some p => RET (Some (xI p)) + end + | Some p => RET (Some (xO p)) + end + | l, Leaf _ => DO p <~ pick l;; RET (Some p) + | Leaf _, r => DO p <~ pick r;; RET (Some p) + | _, _ => RET (Some xH) + end. + +End ImpPosDict. + diff --git a/mppa_k1c/abstractbb/Impure/ImpCore.v b/mppa_k1c/abstractbb/Impure/ImpCore.v index 7925f62d..f1abaf7a 100644 --- a/mppa_k1c/abstractbb/Impure/ImpCore.v +++ b/mppa_k1c/abstractbb/Impure/ImpCore.v @@ -193,4 +193,4 @@ Ltac wlp_xsimplify hint := Create HintDb wlp discriminated. -Ltac wlp_simplify := wlp_xsimplify ltac:(intuition (eauto with wlp)).
\ No newline at end of file +Ltac wlp_simplify := wlp_xsimplify ltac:(intuition eauto with wlp).
\ No newline at end of file diff --git a/mppa_k1c/abstractbb/Impure/ImpHCons.v b/mppa_k1c/abstractbb/Impure/ImpHCons.v index dd615628..637e8296 100644 --- a/mppa_k1c/abstractbb/Impure/ImpHCons.v +++ b/mppa_k1c/abstractbb/Impure/ImpHCons.v @@ -99,41 +99,101 @@ Hint Resolve assert_list_incl_correct. End Sets. + + + (********************************) (* (Weak) HConsing *) +Module HConsing. -Axiom xhCons: forall {A}, ((A -> A -> ?? bool) * (pre_hashV A -> ?? hashV A)) -> ?? hashConsing A. +Export HConsingDefs. + +(* NB: this axiom is NOT intended to be called directly, but only through [hCons...] functions below. *) +Axiom xhCons: forall {A}, (hashH A) -> ?? hashConsing A. Extract Constant xhCons => "ImpHConsOracles.xhCons". -Definition hCons_eq_msg: pstring := "xhCons: hash_eq differs". +Definition hCons_eq_msg: pstring := "xhCons: hash eq differs". -Definition hCons {A} (hash_eq: A -> A -> ?? bool) (unknownHash_msg: pre_hashV A -> ?? pstring): ?? (hashConsing A) := - DO hco <~ xhCons (hash_eq, fun v => DO s <~ unknownHash_msg v ;; FAILWITH s) ;; +Definition hCons {A} (hh: hashH A): ?? (hashConsing A) := + DO hco <~ xhCons hh ;; RET {| - hC := fun x => - DO x' <~ hC hco x ;; - DO b0 <~ hash_eq (pre_data x) (data x') ;; - assert_b b0 hCons_eq_msg;; - RET x'; - hC_known := fun x => - DO x' <~ hC_known hco x ;; - DO b0 <~ hash_eq (pre_data x) (data x') ;; - assert_b b0 hCons_eq_msg;; - RET x'; - next_log := next_log hco; - export := export hco; + hC := (fun x => + DO x' <~ hC hco x ;; + DO b0 <~ hash_eq hh x.(hdata) x' ;; + assert_b b0 hCons_eq_msg;; + RET x'); + next_hid := hco.(next_hid); + next_log := hco.(next_log); + export := hco.(export); + remove := hco.(remove) |}. -Lemma hCons_correct: forall A (hash_eq: A -> A -> ?? bool) msg, - WHEN hCons hash_eq msg ~> hco THEN - ((forall x y, WHEN hash_eq x y ~> b THEN b=true -> x=y) -> forall x, WHEN hC hco x ~> x' THEN (pre_data x)=(data x')) - /\ ((forall x y, WHEN hash_eq x y ~> b THEN b=true -> x=y) -> forall x, WHEN hC_known hco x ~> x' THEN (pre_data x)=(data x')). + +Lemma hCons_correct A (hh: hashH A): + WHEN hCons hh ~> hco THEN + (forall x y, WHEN hh.(hash_eq) x y ~> b THEN b=true -> (ignore_hid hh x)=(ignore_hid hh y)) -> + forall x, WHEN hco.(hC) x ~> x' THEN ignore_hid hh x.(hdata)=ignore_hid hh x'. Proof. wlp_simplify. Qed. Global Opaque hCons. Hint Resolve hCons_correct: wlp. -Definition hCons_spec {A} (hco: hashConsing A) := - (forall x, WHEN hC hco x ~> x' THEN (pre_data x)=(data x')) /\ (forall x, WHEN hC_known hco x ~> x' THEN (pre_data x)=(data x')). + + +(* hashV: extending a given type with hash-consing *) +Record hashV {A:Type}:= { + data: A; + hid: hashcode +}. +Arguments hashV: clear implicits. + +Definition hashV_C {A} (test_eq: A -> A -> ?? bool) : hashH (hashV A) := {| + hash_eq := fun v1 v2 => test_eq v1.(data) v2.(data); + get_hid := hid; + set_hid := fun v id => {| data := v.(data); hid := id |} +|}. + +Definition liftHV (x:nat) := {| data := x; hid := unknown_hid |}. + +Definition hConsV {A} (hasheq: A -> A -> ?? bool): ?? (hashConsing (hashV A)) := + hCons (hashV_C hasheq). + +Lemma hConsV_correct A (hasheq: A -> A -> ?? bool): + WHEN hConsV hasheq ~> hco THEN + (forall x y, WHEN hasheq x y ~> b THEN b=true -> x=y) -> + forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data). +Proof. + Local Hint Resolve f_equal2. + wlp_simplify. + exploit H; eauto. + + wlp_simplify. + + intros; congruence. +Qed. +Global Opaque hConsV. +Hint Resolve hConsV_correct: wlp. + +Definition hC_known {A} (hco:hashConsing (hashV A)) (unknownHash_msg: hashinfo (hashV A) -> ?? pstring) (x:hashinfo (hashV A)): ?? hashV A := + DO clock <~ hco.(next_hid)();; + DO x' <~ hco.(hC) x;; + DO ok <~ hash_older x'.(hid) clock;; + if ok + then RET x' + else + hco.(remove) x;; + DO msg <~ unknownHash_msg x;; + FAILWITH msg. + +Lemma hC_known_correct A (hco:hashConsing (hashV A)) msg x: + WHEN hC_known hco msg x ~> x' THEN + (forall x, WHEN hco.(hC) x ~> x' THEN x.(hdata).(data)=x'.(data)) -> + x.(hdata).(data)=x'.(data). +Proof. + wlp_simplify. + unfold wlp in * |- ; eauto. +Qed. +Global Opaque hC_known. +Hint Resolve hC_known_correct: wlp. + +End HConsing. diff --git a/mppa_k1c/abstractbb/Impure/ImpLoops.v b/mppa_k1c/abstractbb/Impure/ImpLoops.v index dc8b2627..33376c19 100644 --- a/mppa_k1c/abstractbb/Impure/ImpLoops.v +++ b/mppa_k1c/abstractbb/Impure/ImpLoops.v @@ -17,7 +17,7 @@ Section While_Loop. (** Local Definition of "while-loop-invariant" *) Let wli {S} cond body (I: S -> Prop) := forall s, I s -> cond s = true -> WHEN (body s) ~> s' THEN I s'. -Program Definition while {S} cond body (I: S -> Prop | wli cond body I) s0: ?? {s | I s0 -> I s /\ cond s = false} +Program Definition while {S} cond body (I: S -> Prop | wli cond body I) s0: ?? {s | (I s0 -> I s) /\ cond s = false} := loop (A:={s | I s0 -> I s}) (s0, fun s => @@ -26,7 +26,7 @@ Program Definition while {S} cond body (I: S -> Prop | wli cond body I) s0: ?? { DO s' <~ mk_annot (body s) ;; RET (inl (A:={s | I s0 -> I s }) s') | false => - RET (inr (B:={s | I s0 -> I s /\ cond s = false}) s) + RET (inr (B:={s | (I s0 -> I s) /\ cond s = false}) s) end). Obligation 2. unfold wli, wlp in * |-; eauto. @@ -83,7 +83,7 @@ Definition wapply {A B} {R: A -> B -> Prop} (beq: A -> A -> ?? bool) (k: A -> ?? assert_b b msg;; RET (output a). -Lemma wapply_correct A B (R: A -> B -> Prop) (beq: A -> A -> ?? bool)x (k: A -> ?? answ R): +Lemma wapply_correct A B (R: A -> B -> Prop) (beq: A -> A -> ?? bool) (k: A -> ?? answ R) x: beq_correct beq -> WHEN wapply beq k x ~> y THEN R x y. Proof. @@ -107,7 +107,7 @@ Definition rec_preserv {A B} (recF: (A -> ?? B) -> A -> ?? B) (R: A -> B -> Prop Program Definition rec {A B} beq recF (R: A -> B -> Prop) (H1: rec_preserv recF R) (H2: beq_correct beq): ?? (A -> ?? B) := DO f <~ xrec (B:=answ R) (fun f x => DO y <~ mk_annot (recF (wapply beq f) x) ;; - RET {| input := x; output := proj1_sig y |});; + RET {| input := x; output := `y |});; RET (wapply beq f). Obligation 1. eapply H1; eauto. clear H H1. diff --git a/mppa_k1c/abstractbb/Impure/ImpPrelude.v b/mppa_k1c/abstractbb/Impure/ImpPrelude.v index 1a84eb3b..477be65c 100644 --- a/mppa_k1c/abstractbb/Impure/ImpPrelude.v +++ b/mppa_k1c/abstractbb/Impure/ImpPrelude.v @@ -91,11 +91,17 @@ Extract Inlined Constant struct_eq => "(=)". Hint Resolve struct_eq_correct: wlp. -(** Data-structure for generic hash-consing, hash-set *) +(** Data-structure for generic hash-consing *) Axiom hashcode: Type. Extract Constant hashcode => "int". +(* NB: hashConsing is assumed to generate hash-code in ascending order. + This gives a way to check that a hash-consed value is older than an other one. +*) +Axiom hash_older: hashcode -> hashcode -> ?? bool. +Extract Inlined Constant hash_older => "(<)". + Module Dict. Record hash_params {A:Type} := { @@ -115,42 +121,45 @@ Arguments t: clear implicits. End Dict. +Module HConsingDefs. -(* NB: hashConsing is assumed to generate hash-code in ascending order. - This gives a way to check that a hash-consed value is older than an other one. -*) -Axiom hash_older: hashcode -> hashcode -> ?? bool. -Extract Inlined Constant hash_older => "(<=)". - -Record pre_hashV {A: Type} := { - pre_data: A; +Record hashinfo {A: Type} := { + hdata: A; hcodes: list hashcode; - debug_info: option pstring; }. -Arguments pre_hashV: clear implicits. +Arguments hashinfo: clear implicits. -Record hashV {A:Type}:= { - data: A; - hid: hashcode +(* for inductive types with intrinsic hash-consing *) +Record hashH {A:Type}:= { + hash_eq: A -> A -> ?? bool; + get_hid: A -> hashcode; + set_hid: A -> hashcode -> A; (* WARNING: should only be used by hash-consing machinery *) }. -Arguments hashV: clear implicits. +Arguments hashH: clear implicits. + +Axiom unknown_hid: hashcode. +Extract Constant unknown_hid => "-1". + +Definition ignore_hid {A} (hh: hashH A) (hv:A) := set_hid hh hv unknown_hid. Record hashExport {A:Type}:= { - get_hashV: hashcode -> ?? pre_hashV A; - iterall: ((list pstring) -> hashcode -> pre_hashV A -> ?? unit) -> ?? unit; (* iter on all elements in the hashtbl, by order of creation *) + get_info: hashcode -> ?? hashinfo A; + iterall: ((list pstring) -> hashcode -> hashinfo A -> ?? unit) -> ?? unit; (* iter on all elements in the hashtbl, by order of creation *) }. Arguments hashExport: clear implicits. Record hashConsing {A:Type}:= { - (* TODO next_hashcode: unit -> ?? hashcode *) - hC: pre_hashV A -> ?? hashV A; - hC_known: pre_hashV A -> ?? hashV A; (* fails on unknown inputs *) - (**** below: debugging functions ****) + hC: hashinfo A -> ?? A; + (**** below: debugging or internal functions ****) + next_hid: unit -> ?? hashcode; (* should be strictly less old than ignore_hid *) + remove: hashinfo A -> ??unit; (* SHOULD NOT BE USED ! *) next_log: pstring -> ?? unit; (* insert a log info (for the next introduced element) -- regiven by [iterall export] below *) export: unit -> ?? hashExport A ; }. Arguments hashConsing: clear implicits. +End HConsingDefs. + (** recMode: this is mainly for Tests ! *) Inductive recMode:= StdRec | MemoRec | BareRec | BuggyRec. diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml index b7a80679..3994cae6 100644 --- a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml +++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml @@ -1,6 +1,5 @@ open ImpPrelude - -exception Stop;; +open HConsingDefs let make_dict (type key) (p: key Dict.hash_params) = let module MyHashedType = struct @@ -16,10 +15,15 @@ let make_dict (type key) (p: key Dict.hash_params) = } -let xhCons (type a) (hash_eq, error: (a -> a -> bool)*(a pre_hashV -> a hashV)) = +exception Stop;; + +let xhCons (type a) (hh:a hashH) = + (* We use a hash-table, but a hash-set would be sufficient ! *) + (* Thus, we could use a weak hash-set, but prefer avoid it for easier debugging *) + (* Ideally, a parameter would allow to select between the weak or full version *) let module MyHashedType = struct - type t = a pre_hashV - let equal x y = hash_eq x.pre_data y.pre_data + type t = a hashinfo + let equal x y = hh.hash_eq x.hdata y.hdata let hash x = Hashtbl.hash x.hcodes end in let module MyHashtbl = Hashtbl.Make(MyHashedType) in @@ -34,21 +38,18 @@ let xhCons (type a) (hash_eq, error: (a -> a -> bool)*(a pre_hashV -> a hashV)) let t = MyHashtbl.create 1000 in let logs = ref [] in { - hC = (fun (x:a pre_hashV) -> - match MyHashtbl.find_opt t x with - | Some x' -> x' + hC = (fun (k:a hashinfo) -> + match MyHashtbl.find_opt t k with + | Some d -> d | None -> (*print_string "+";*) - let x' = { data = x.pre_data ; - hid = MyHashtbl.length t } - in MyHashtbl.add t x x'; x'); - hC_known = (fun (x:a pre_hashV) -> - match MyHashtbl.find_opt t x with - | Some x' -> x' - | None -> error x); + let d = hh.set_hid k.hdata (MyHashtbl.length t) in + MyHashtbl.add t {k with hdata = d } d; d); next_log = (fun info -> logs := (MyHashtbl.length t, info)::(!logs)); + next_hid = (fun () -> MyHashtbl.length t); + remove = (fun (x:a hashinfo) -> MyHashtbl.remove t x); export = fun () -> match pick t with - | None -> { get_hashV = (fun _ -> raise Not_found); iterall = (fun _ -> ()) } + | None -> { get_info = (fun _ -> raise Not_found); iterall = (fun _ -> ()) } | Some (k,_) -> (* the state is fully copied at export ! *) let logs = ref (List.rev_append (!logs) []) in @@ -57,9 +58,9 @@ let xhCons (type a) (hash_eq, error: (a -> a -> bool)*(a pre_hashV -> a hashV)) | (j, info)::l' when i>=j -> logs:=l'; info::(step_log i) | _ -> [] in let a = Array.make (MyHashtbl.length t) k in - MyHashtbl.iter (fun k d -> a.(d.hid) <- k) t; + MyHashtbl.iter (fun k d -> a.(hh.get_hid d) <- k) t; { - get_hashV = (fun i -> a.(i)); + get_info = (fun i -> a.(i)); iterall = (fun iter_node -> Array.iteri (fun i k -> iter_node (step_log i) i k) a) } } diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli index a74c721a..9f5eca89 100644 --- a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli +++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli @@ -1,4 +1,5 @@ open ImpPrelude +open HConsingDefs -val make_dict : 'a1 Dict.hash_params -> ('a1, 'a2) Dict.t -val xhCons: (('a -> 'a -> bool) * ('a pre_hashV -> 'a hashV)) -> 'a hashConsing +val make_dict : 'a Dict.hash_params -> ('a, 'b) Dict.t +val xhCons: 'a hashH -> 'a hashConsing diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v index d1971e57..22809095 100644 --- a/mppa_k1c/abstractbb/Parallelizability.v +++ b/mppa_k1c/abstractbb/Parallelizability.v @@ -1,4 +1,4 @@ -(** Parallel Semantics of Abstract Basic Blocks and parallelizability test.s +(** Parallel Semantics of Abstract Basic Blocks and parallelizability test. *) Require Setoid. (* in order to rewrite <-> *) @@ -32,7 +32,7 @@ Fixpoint inst_prun (i: inst) (m tmp old: mem): option mem := end end. -(* [inst_prun] is generalization of [inst_run] *) +(* [inst_prun] is generalization of [inst_run] *) Lemma inst_run_prun i: forall m old, inst_run ge i m old = inst_prun i m m old. Proof. diff --git a/mppa_k1c/abstractbb/SeqSimuTheory.v b/mppa_k1c/abstractbb/SeqSimuTheory.v new file mode 100644 index 00000000..45afd830 --- /dev/null +++ b/mppa_k1c/abstractbb/SeqSimuTheory.v @@ -0,0 +1,428 @@ +(** A theory for checking/proving simulation by symbolic execution. + +*) + + +Require Setoid. (* in order to rewrite <-> *) +Require Export AbstractBasicBlocksDef. +Require Import List. +Require Import ImpPrelude. +Import HConsingDefs. + +Module Type PseudoRegDictionary. + +Declare Module R: PseudoRegisters. + +Parameter t: Type -> Type. + +Parameter get: forall {A}, t A -> R.t -> option A. + +Parameter set: forall {A}, t A -> R.t -> A -> t A. + +Parameter set_spec_eq: forall A d x (v: A), + get (set d x v) x = Some v. + +Parameter set_spec_diff: forall A d x y (v: A), + x <> y -> get (set d x v) y = get d y. + +Parameter empty: forall {A}, t A. + +Parameter empty_spec: forall A x, + get (empty (A:=A)) x = None. + +End PseudoRegDictionary. + + +Module SimuTheory (L: SeqLanguage) (Dict: PseudoRegDictionary with Module R:=L.LP.R). + +Export L. +Export LP. +Export Terms. + +(* the symbolic memory: + - pre: pre-condition expressing that the computation has not yet abort on a None. + - post: the post-condition for each pseudo-register +*) +Record smem:= {pre: genv -> mem -> Prop; post: Dict.t term}. + +Coercion post: smem >-> Dict.t. + +(** initial symbolic memory *) +Definition smem_empty := {| pre:=fun _ _ => True; post:=Dict.empty |}. + +Definition smem_get (d:Dict.t term) x := + match Dict.get d x with + | None => Input x unknown_hid + | Some t => t + end. + +Fixpoint exp_term (e: exp) (d old: Dict.t term): term := + match e with + | PReg x => smem_get d x + | Op o le => App o (list_exp_term le d old) unknown_hid + | Old e => exp_term e old old + end +with list_exp_term (le: list_exp) (d old: Dict.t term) : list_term := + match le with + | Enil => LTnil unknown_hid + | Econs e le' => LTcons (exp_term e d old) (list_exp_term le' d old) unknown_hid + | LOld le => list_exp_term le old old + end. + +(** evaluation of the post-condition *) +Definition smem_eval ge (d: Dict.t term) x (m:mem) := + term_eval ge (smem_get d x) m. + +(** assignment of the symbolic memory *) +Definition smem_set (d:smem) x (t:term) := + {| pre:=(fun ge m => (smem_eval ge d x m) <> None /\ (d.(pre) ge m)); + post:=Dict.set d x t |}. + +Section SIMU_THEORY. + +Variable ge: genv. + +Lemma set_spec_eq d x t m: + smem_eval ge (smem_set d x t) x m = term_eval ge t m. +Proof. + unfold smem_eval, smem_set, smem_get; simpl; rewrite Dict.set_spec_eq; simpl; auto. +Qed. + +Lemma set_spec_diff d x y t m: + x <> y -> smem_eval ge (smem_set d x t) y m = smem_eval ge d y m. +Proof. + intros; unfold smem_eval, smem_set, smem_get; simpl; rewrite Dict.set_spec_diff; simpl; auto. +Qed. + +Lemma smem_eval_empty x m: smem_eval ge smem_empty x m = Some (m x). +Proof. + unfold smem_eval, smem_get; rewrite Dict.empty_spec; simpl; auto. +Qed. + +Hint Rewrite set_spec_eq smem_eval_empty: dict_rw. + +Fixpoint inst_smem (i: inst) (d old: smem): smem := + match i with + | nil => d + | (x, e)::i' => + let t:=exp_term e d old in + inst_smem i' (smem_set d x t) old + end. + +Fixpoint bblock_smem_rec (p: bblock) (d: smem): smem := + match p with + | nil => d + | i::p' => + let d':=inst_smem i d d in + bblock_smem_rec p' d' + end. + +Local Hint Resolve smem_eval_empty. + +Definition bblock_smem: bblock -> smem + := fun p => bblock_smem_rec p smem_empty. + +Lemma inst_smem_pre_monotonic i old: forall d m, + (pre (inst_smem 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 smem_set; simpl; intuition. +Qed. + +Lemma bblock_smem_pre_monotonic p: forall d m, + (pre (bblock_smem_rec p d) ge m) -> (pre d ge m). +Proof. + induction p as [|i p' IHp']; simpl; eauto. + intros d a H; eapply inst_smem_pre_monotonic; eauto. +Qed. + +Local Hint Resolve inst_smem_pre_monotonic bblock_smem_pre_monotonic. + +Lemma term_eval_exp e (od:smem) m0 old: + (forall x, smem_eval ge od x m0 = Some (old x)) -> + forall d m1, + (forall x, smem_eval ge (d:smem) x m0 = Some (m1 x)) -> + term_eval ge (exp_term e d od) m0 = exp_eval ge e m1 old. +Proof. + unfold smem_eval in * |- *; intro H. + induction e using exp_mut with + (P0:=fun l => forall (d:smem) m1, (forall x, term_eval ge (smem_get d x) m0 = Some (m1 x)) -> list_term_eval ge (list_exp_term l d od) m0 = list_exp_eval ge l m1 old); + simpl; auto. + - intros; erewrite IHe; eauto. + - intros. erewrite IHe, IHe0; eauto. +Qed. + +Lemma inst_smem_abort i m0 x old: forall d, + pre (inst_smem i d old) ge m0 -> + smem_eval ge d x m0 = None -> + smem_eval ge (inst_smem i d old) x m0 = None. +Proof. + induction i as [|[y e] i IHi]; simpl; auto. + intros d VALID H; erewrite IHi; eauto. clear IHi. + destruct (R.eq_dec x y). + * subst; autorewrite with dict_rw. + generalize (inst_smem_pre_monotonic _ _ _ _ VALID); clear VALID. + unfold smem_set; simpl; intuition congruence. + * rewrite set_spec_diff; auto. +Qed. + +Lemma block_smem_rec_abort p m0 x: forall d, + pre (bblock_smem_rec p d) ge m0 -> + smem_eval ge d x m0 = None -> + smem_eval ge (bblock_smem_rec p d) x m0 = None. +Proof. + induction p; simpl; auto. + intros d VALID H; erewrite IHp; eauto. clear IHp. + eapply inst_smem_abort; eauto. +Qed. + +Lemma inst_smem_Some_correct1 i m0 old (od:smem): + (forall x, smem_eval ge od x m0 = Some (old x)) -> + forall (m1 m2: mem) (d: smem), + inst_run ge i m1 old = Some m2 -> + (forall x, smem_eval ge d x m0 = Some (m1 x)) -> + forall x, smem_eval ge (inst_smem 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. + 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 term_eval_exp; eauto. + * rewrite set_spec_diff; auto. +Qed. + +Lemma bblocks_smem_rec_Some_correct1 p m0: forall (m1 m2: mem) (d: smem), + run ge p m1 = Some m2 -> + (forall x, smem_eval ge d x m0 = Some (m1 x)) -> + forall x, smem_eval ge (bblock_smem_rec p d) x m0 = Some (m2 x). +Proof. + Local Hint Resolve inst_smem_Some_correct1. + induction p as [ | i p]; simpl; intros m1 m2 d H. + - inversion_clear H; eauto. + - intros H0 x0. + destruct (inst_run ge i m1 m1) eqn: Heqov. + + refine (IHp _ _ _ _ _ _); eauto. + + inversion H. +Qed. + +Lemma bblock_smem_Some_correct1 p m0 m1: + run ge p m0 = Some m1 + -> forall x, smem_eval ge (bblock_smem p) x m0 = Some (m1 x). +Proof. + intros; eapply bblocks_smem_rec_Some_correct1; eauto. +Qed. + +Lemma inst_smem_None_correct i m0 old (od: smem): + (forall x, smem_eval ge od x m0 = Some (old x)) -> + forall m1 d, pre (inst_smem i d od) ge m0 -> + (forall x, smem_eval ge d x m0 = Some (m1 x)) -> + inst_run ge i m1 old = None -> exists x, smem_eval ge (inst_smem i d od) x m0 = None. +Proof. + intro X; induction i as [|[x e] i IHi]; simpl; intros m1 d. + - 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. + erewrite term_eval_exp; eauto. + * rewrite set_spec_diff; auto. + + intuition. + constructor 1 with (x:=x); simpl. + apply inst_smem_abort; auto. + autorewrite with dict_rw. + erewrite term_eval_exp; eauto. +Qed. + +Lemma inst_smem_Some_correct2 i m0 old (od: smem): + (forall x, smem_eval ge od x m0 = Some (old x)) -> + forall (m1 m2: mem) d, + pre (inst_smem i d od) ge m0 -> + (forall x, smem_eval ge d x m0 = Some (m1 x)) -> + (forall x, smem_eval ge (inst_smem 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 VALID H0. + - intros H; eapply ex_intro; intuition eauto. + generalize (H0 x); rewrite H. + congruence. + - intros H. + 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. + erewrite term_eval_exp; eauto. + * rewrite set_spec_diff; auto. + + generalize (H x). + rewrite inst_smem_abort; discriminate || auto. + autorewrite with dict_rw. + erewrite term_eval_exp; eauto. +Qed. + +Lemma bblocks_smem_rec_Some_correct2 p m0: forall (m1 m2: mem) d, + pre (bblock_smem_rec p d) ge m0 -> + (forall x, smem_eval ge d x m0 = Some (m1 x)) -> + (forall x, smem_eval ge (bblock_smem_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 VALID H0. + - intros H; eapply ex_intro; intuition eauto. + generalize (H0 x); rewrite H. + congruence. + - intros H. + destruct (inst_run ge i m1 m1) eqn: Heqom. + + refine (IHp _ _ _ _ _ _); eauto. + + assert (X: exists x, term_eval ge (smem_get (inst_smem i d d) x) m0 = None). + { eapply inst_smem_None_correct; eauto. } + destruct X as [x H1]. + generalize (H x). + erewrite block_smem_rec_abort; eauto. + congruence. +Qed. + + +Lemma bblock_smem_Some_correct2 p m0 m1: + pre (bblock_smem p) ge m0 -> + (forall x, smem_eval ge (bblock_smem p) x m0 = Some (m1 x)) + -> res_eq (Some m1) (run ge p m0). +Proof. + intros; eapply bblocks_smem_rec_Some_correct2; eauto. +Qed. + +Lemma inst_valid i m0 old (od:smem): + (forall x, smem_eval ge od x m0 = Some (old x)) -> + forall (m1 m2: mem) (d: smem), + pre d ge m0 -> + inst_run ge i m1 old = Some m2 -> + (forall x, smem_eval ge d x m0 = Some (m1 x)) -> + pre (inst_smem 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 smem_set in * |- *; simpl. + rewrite Hm1; intuition congruence. + + intros x0. unfold assign; destruct (R.eq_dec x x0). + * subst; autorewrite with dict_rw. + erewrite term_eval_exp; eauto. + * rewrite set_spec_diff; auto. +Qed. + + +Lemma block_smem_rec_valid p m0: forall (m1 m2: mem) (d:smem), + pre d ge m0 -> + run ge p m1 = Some m2 -> + (forall x, smem_eval ge d x m0 = Some (m1 x)) -> + pre (bblock_smem_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_smem_valid p m0 m1: + run ge p m0 = Some m1 -> + pre (bblock_smem p) ge m0. +Proof. + intros; eapply block_smem_rec_valid; eauto. + unfold smem_empty; simpl. auto. +Qed. + +Definition svalid ge d m := pre d ge m /\ forall x, smem_eval ge d x m <> None. + +Theorem bblock_smem_simu p1 p2: + (forall m, svalid ge (bblock_smem p1) m -> svalid ge (bblock_smem p2) m) -> + (forall m0 x m1, svalid ge (bblock_smem p1) m0 -> smem_eval ge (bblock_smem p1) x m0 = Some m1 -> + smem_eval ge (bblock_smem p2) x m0 = Some m1) -> + bblock_simu ge p1 p2. +Proof. + Local Hint Resolve bblock_smem_valid bblock_smem_Some_correct1. + unfold svalid; intros INCL EQUIV m DONTFAIL. + destruct (run ge p1 m) as [m1|] eqn: RUN1; simpl; try congruence. + assert (X: forall x, smem_eval ge (bblock_smem p1) x m = Some (m1 x)); eauto. + eapply bblock_smem_Some_correct2; eauto. + + destruct (INCL m); intuition eauto. + congruence. + + intro x; apply EQUIV; intuition eauto. + congruence. +Qed. + +Lemma svalid_set_decompose_1 d t x m: + svalid ge (smem_set d x t) m -> svalid ge d m. +Proof. + unfold svalid; intros ((PRE1 & PRE2) & VALID); split. + + intuition. + + intros x0 H. case (R.eq_dec x x0). + * intuition congruence. + * intros DIFF; eapply VALID. erewrite set_spec_diff; eauto. +Qed. + +Lemma svalid_set_decompose_2 d t x m: + svalid ge (smem_set d x t) m -> term_eval ge t m <> None. +Proof. + unfold svalid; intros ((PRE1 & PRE2) & VALID) H. + generalize (VALID x); autorewrite with dict_rw. + tauto. +Qed. + +Lemma svalid_set_proof d x t m: + svalid ge d m -> term_eval ge t m <> None -> svalid ge (smem_set d x t) m. +Proof. + unfold svalid; intros (PRE & VALID) PREt. split. + + split; auto. + + intros x0; case (R.eq_dec x x0). + - intros; subst; autorewrite with dict_rw. auto. + - intros. rewrite set_spec_diff; auto. +Qed. + +End SIMU_THEORY. + +End SimuTheory. + +Require Import PArith. +Require Import FMapPositive. + +Module PosDict <: PseudoRegDictionary with Module R:=Pos. + +Module R:=Pos. + +Definition t:=PositiveMap.t. + +Definition get {A} (d:t A) (x:R.t): option A + := PositiveMap.find x d. + +Definition set {A} (d:t A) (x:R.t) (v:A): t A + := PositiveMap.add x v d. + +Local Hint Unfold PositiveMap.E.eq. + +Lemma set_spec_eq A d x (v: A): + get (set d x v) x = Some v. +Proof. + unfold get, set; apply PositiveMap.add_1; auto. +Qed. + +Lemma set_spec_diff A d x y (v: A): + x <> y -> get (set d x v) y = get d y. +Proof. + unfold get, set; intros; apply PositiveMap.gso; auto. +Qed. + +Definition empty {A}: t A := PositiveMap.empty A. + +Lemma empty_spec A x: + get (empty (A:=A)) x = None. +Proof. + unfold get, empty; apply PositiveMap.gempty; auto. +Qed. + +End PosDict.
\ No newline at end of file |