From fd7a801bef1e9fe6e47b62c5c1b0905a4dde7ae8 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Sun, 26 May 2019 08:50:44 +0200 Subject: extending bblock_simu_test with rewriting --- mppa_k1c/Asmblockdeps.v | 63 +- mppa_k1c/abstractbb/AbstractBasicBlocksDef.v | 130 ++- mppa_k1c/abstractbb/DepTreeTheory.v | 456 -------- mppa_k1c/abstractbb/ImpDep.v | 960 ----------------- mppa_k1c/abstractbb/ImpSimuTest.v | 1108 ++++++++++++++++++++ mppa_k1c/abstractbb/Impure/ImpCore.v | 2 +- mppa_k1c/abstractbb/Impure/ImpHCons.v | 104 +- mppa_k1c/abstractbb/Impure/ImpLoops.v | 8 +- mppa_k1c/abstractbb/Impure/ImpPrelude.v | 51 +- .../abstractbb/Impure/ocaml/ImpHConsOracles.ml | 37 +- .../abstractbb/Impure/ocaml/ImpHConsOracles.mli | 5 +- mppa_k1c/abstractbb/Parallelizability.v | 4 +- mppa_k1c/abstractbb/SeqSimuTheory.v | 428 ++++++++ 13 files changed, 1825 insertions(+), 1531 deletions(-) delete mode 100644 mppa_k1c/abstractbb/DepTreeTheory.v delete mode 100644 mppa_k1c/abstractbb/ImpDep.v create mode 100644 mppa_k1c/abstractbb/ImpSimuTest.v create mode 100644 mppa_k1c/abstractbb/SeqSimuTheory.v (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index eb3900d5..e0aaee58 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -9,7 +9,7 @@ Require Import Integers. Require Import Floats. Require Import ZArith. Require Import Coqlib. -Require Import ImpDep. +Require Import ImpSimuTest. Require Import Axioms. Require Import Parallelizability. Require Import Asmvliw Permutation. @@ -302,30 +302,6 @@ Definition op_eval (o: op) (l: list value) := end. - (** Function [is_constant] is used for a small optimization inside the scheduling verifier. - It is good that it answers [true] as much as possible while satisfying [is_constant_correct] below. - - BE CAREFUL that, [is_constant] must not depend on [ge]. - Otherwise, we would have an easy implementation: [match op_eval o nil with Some _ => true | _ => false end] - - => REM: when [is_constant] is not complete w.r.t [is_constant_correct], this should have only a very little impact - on the performance of the scheduling verifier... - *) - -Definition is_constant (o: op): bool := - match o with - | Constant _ | OArithR _ | OArithRI32 _ _ | OArithRI64 _ _ | OArithRF32 _ _ | OArithRF64 _ _ => true - | _ => false - end. - -Lemma is_constant_correct o: is_constant o = true -> op_eval o nil <> None. -Proof. - destruct o; simpl; try congruence. - destruct ao; simpl; try congruence; - destruct n; simpl; try congruence; - unfold arith_eval; destruct Ge; simpl; try congruence. -Qed. - Definition arith_op_eq (o1 o2: arith_op): ?? bool := match o1 with | OArithR n1 => @@ -507,7 +483,7 @@ Include MkSeqLanguage P. End L. -Module IDT := ImpDepTree L ImpPosDict. +Module IST := ImpSimu L ImpPosDict. Import L. Import P. @@ -1593,16 +1569,35 @@ Definition string_of_op (op: P.op): ?? pstring := | Fail => RET (Str "Fail") end. +End SECT_BBLOCK_EQUIV. + +(** REWRITE RULES *) + +Definition is_constant (o: op): bool := + match o with + | Constant _ | OArithR _ | OArithRI32 _ _ | OArithRI64 _ _ | OArithRF32 _ _ | OArithRF64 _ _ => true + | _ => false + end. + +Program Definition failsafe_reduce := Terms.failsafe_reduce is_constant. +Obligation 1. + destruct o; simpl in * |- *; try congruence. + destruct ao; simpl in * |- *; try congruence; + destruct n; simpl in * |- *; try congruence; + unfold arith_eval; destruct ge; simpl in * |- *; try congruence. +Qed. + + Definition bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool := if verb then - IDT.verb_bblock_simu_test string_of_name string_of_op (trans_block p1) (trans_block p2) + IST.verb_bblock_simu_test failsafe_reduce string_of_name string_of_op (trans_block p1) (trans_block p2) else - IDT.bblock_simu_test (trans_block p1) (trans_block p2). + IST.bblock_simu_test failsafe_reduce (trans_block p1) (trans_block p2). -Local Hint Resolve IDT.bblock_simu_test_correct bblock_simu_reduce IDT.verb_bblock_simu_test_correct: wlp. +Local Hint Resolve IST.bblock_simu_test_correct bblock_simu_reduce IST.verb_bblock_simu_test_correct: wlp. Theorem bblock_simu_test_correct verb p1 p2 : - WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Ge = Genv ge fn -> Asmblockgenproof0.bblock_simu ge fn p1 p2. + WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Asmblockgenproof0.bblock_simu ge fn p1 p2. Proof. wlp_simplify. Qed. @@ -1614,7 +1609,7 @@ Import UnsafeImpure. Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := unsafe_coerce (bblock_simu_test verb p1 p2). -Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: Ge = Genv ge fn -> pure_bblock_simu_test verb p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2. +Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2. Proof. intros; unfold pure_bblock_simu_test. intros; eapply bblock_simu_test_correct; eauto. apply unsafe_coerce_not_really_correct; eauto. @@ -1622,9 +1617,7 @@ Qed. Definition bblock_simub: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bblock_simu_test true. -Lemma bblock_simub_correct p1 p2 ge fn: Ge = Genv ge fn -> bblock_simub p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2. +Lemma bblock_simub_correct p1 p2 ge fn: bblock_simub p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2. Proof. eapply (pure_bblock_simu_test_correct true). -Qed. - -End SECT_BBLOCK_EQUIV. +Qed. \ No newline at end of file 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 -- cgit From e9e83f59ed2b1087ea974e7112abf71d8eb4195b Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Sun, 26 May 2019 15:00:35 +0200 Subject: slightly more efficient version --- mppa_k1c/abstractbb/AbstractBasicBlocksDef.v | 10 ++-- mppa_k1c/abstractbb/ImpSimuTest.v | 89 +++++++++++++++++++++------- mppa_k1c/abstractbb/SeqSimuTheory.v | 26 ++++---- 3 files changed, 85 insertions(+), 40 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v index f381c810..8ee04f44 100644 --- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v +++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v @@ -306,12 +306,12 @@ Definition list_term_get_hid (l: list_term): hashcode := 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; + mayfail: 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 m, term_eval ge t m <> None <-> allvalid ge pt.(mayfail) m) /\ (forall ge m0 m1, term_eval ge t m0 = Some m1 -> term_eval ge pt.(effect) m0 = Some m1). Import ImpCore.Notations. @@ -323,7 +323,7 @@ Record reduction (t:term):= { }. Hint Resolve result_correct: wlp. -Program Definition identity_reduce (t: term): reduction t := {| result := RET {| valid := [t]; effect := t |} |}. +Program Definition identity_reduce (t: term): reduction t := {| result := RET {| mayfail := [t]; effect := t |} |}. Obligation 1. unfold match_pseudo_term, allvalid; wlp_simplify; congruence. Qed. @@ -331,9 +331,9 @@ 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 |} |} + | Input x _ => {| result := RET {| mayfail := []; effect := t |} |} | o @ [] => match is_constant o with - | true => {| result := RET {| valid := []; effect := t |} |} + | true => {| result := RET {| mayfail := []; effect := t |} |} | false => identity_reduce t end | _ => identity_reduce t diff --git a/mppa_k1c/abstractbb/ImpSimuTest.v b/mppa_k1c/abstractbb/ImpSimuTest.v index 8c9c820f..13af4289 100644 --- a/mppa_k1c/abstractbb/ImpSimuTest.v +++ b/mppa_k1c/abstractbb/ImpSimuTest.v @@ -231,20 +231,20 @@ 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)). + (forall m, allvalid ge hd.(hpre) m <-> smem_valid ge d m) + /\ (forall m x, smem_valid 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. +Lemma smem_model_smem_valid_alt ge d hd: smem_model ge d hd -> + forall m x, smem_valid 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. + unfold smem_valid 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. + intros (H1 & H2) m x H. eapply smem_model_smem_valid_alt. - split; eauto. - rewrite <- H1; auto. Qed. @@ -254,24 +254,24 @@ Definition naive_set (hd:hsmem) x (t:term) := 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) -> + (forall m, smem_valid 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. } + assert (VALID1: allvalid ge hd.(hpre) m -> pre d ge m). { unfold smem_valid in PRE; tauto. } + assert (VALID2: allvalid ge hd.(hpre) m -> forall x : Dict.R.t, smem_eval ge d x m <> None). { unfold smem_valid in PRE; tauto. } unfold allvalid in * |- *; simpl. intuition (subst; eauto). - + eapply svalid_set_proof; eauto. + + eapply smem_valid_set_proof; eauto. erewrite <- EQT; eauto. - + exploit svalid_set_decompose_1; eauto. - intros X1; exploit svalid_set_decompose_2; eauto. + + exploit smem_valid_set_decompose_1; eauto. + intros X1; exploit smem_valid_set_decompose_2; eauto. rewrite <- EQT; eauto. - + exploit svalid_set_decompose_1; eauto. + + exploit smem_valid_set_decompose_1; eauto. - clear DM0. unfold smem_eval, smem_eval, smem_get in * |- *; simpl. - Local Hint Resolve svalid_set_decompose_1. + Local Hint Resolve smem_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. @@ -387,7 +387,7 @@ 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 lht <~ hterm_append pt.(mayfail) hd.(hpre);; DO ht <~ hterm_lift pt.(effect);; log_new_hterm ht;; DO nd <~ smart_set hd x ht;; @@ -396,7 +396,7 @@ Definition hsmem_set (hd:hsmem) x (t:term) := 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) -> + (forall m, smem_valid 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. @@ -418,34 +418,79 @@ Qed. Local Hint Resolve hsmem_set_correct: wlp. Global Opaque hsmem_set. +(* VARIANTE: we do not hash-cons the term from the expression 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. + forall m, smem_valid ge d m -> smem_valid 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); + smem_model ge d hd -> forall m, smem_valid ge d m -> smem_valid 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 hexp_term (e: exp) (d od: hsmem): ?? term := + match e with + | PReg x => hsmem_get d x + | Op o le => + DO lt <~ hlist_exp_term le d od;; + hApp o lt + | Old e => hexp_term e od od + end +with hlist_exp_term (le: list_exp) (d od: hsmem): ?? list_term := + match le with + | Enil => hLTnil tt + | Econs e le' => + DO t <~ hexp_term e d od;; + DO lt <~ hlist_exp_term le' d od;; + hLTcons t lt + | LOld le => hlist_exp_term le od od + end. + +Lemma hexp_term_correct_x ge e hod od: + smem_model ge od hod -> + forall hd d, + smem_model ge d hd -> + WHEN hexp_term e hd hod ~> t THEN forall m, smem_valid ge d m -> smem_valid ge od m -> term_eval ge t 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 -> + WHEN hlist_exp_term le hd hod ~> lt THEN forall m, smem_valid ge d m -> smem_valid ge od m -> list_term_eval ge lt m = list_term_eval ge (list_exp_term le d od) m); + unfold smem_model, smem_eval in * |- * ; simpl; wlp_simplify. + - rewrite H1, <- H4; auto. + - rewrite H4, <- H0; simpl; auto. + - rewrite H5, <- H0, <- H4; simpl; auto. +Qed. +Global Opaque hexp_term. + +Lemma hexp_term_correct e hd hod: + WHEN hexp_term e hd hod ~> t THEN forall ge od d m, smem_model ge od hod -> smem_model ge d hd -> smem_valid ge d m -> smem_valid ge od m -> term_eval ge t m = term_eval ge (exp_term e d od) m. +Proof. + unfold wlp; intros; eapply hexp_term_correct_x; eauto. +Qed. +Hint Resolve hexp_term_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);; + DO ht <~ hexp_term e hd hod;; + DO nd <~ hsmem_set hd x ht;; 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'. + forall ge od d, smem_model ge od hod -> smem_model ge d hd -> (forall m, smem_valid ge d m -> smem_valid ge od m) -> smem_model ge (inst_smem i d od) hd'. Proof. - Local Hint Resolve svalid_set_proof. + Local Hint Resolve smem_valid_set_proof. induction i; simpl; wlp_simplify; eauto 15 with wlp. Qed. Global Opaque hinst_smem. @@ -479,7 +524,7 @@ 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; + unfold smem_model, smem_valid, smem_eval, allvalid, smem_eval, smem_get; simpl; intuition; rewrite !Dict.empty_spec in * |- *; simpl in * |- *; try congruence. Qed. Global Opaque hbblock_smem. diff --git a/mppa_k1c/abstractbb/SeqSimuTheory.v b/mppa_k1c/abstractbb/SeqSimuTheory.v index 45afd830..8b6a372a 100644 --- a/mppa_k1c/abstractbb/SeqSimuTheory.v +++ b/mppa_k1c/abstractbb/SeqSimuTheory.v @@ -337,16 +337,16 @@ Proof. unfold smem_empty; simpl. auto. Qed. -Definition svalid ge d m := pre d ge m /\ forall x, smem_eval ge d x m <> None. +Definition smem_valid 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 -> + (forall m, smem_valid ge (bblock_smem p1) m -> smem_valid ge (bblock_smem p2) m) -> + (forall m0 x m1, smem_valid 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. + unfold smem_valid; 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. @@ -356,28 +356,28 @@ Proof. congruence. Qed. -Lemma svalid_set_decompose_1 d t x m: - svalid ge (smem_set d x t) m -> svalid ge d m. +Lemma smem_valid_set_decompose_1 d t x m: + smem_valid ge (smem_set d x t) m -> smem_valid ge d m. Proof. - unfold svalid; intros ((PRE1 & PRE2) & VALID); split. + unfold smem_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 svalid_set_decompose_2 d t x m: - svalid ge (smem_set d x t) m -> term_eval ge t m <> None. +Lemma smem_valid_set_decompose_2 d t x m: + smem_valid ge (smem_set d x t) m -> term_eval ge t m <> None. Proof. - unfold svalid; intros ((PRE1 & PRE2) & VALID) H. + unfold smem_valid; 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. +Lemma smem_valid_set_proof d x t m: + smem_valid ge d m -> term_eval ge t m <> None -> smem_valid ge (smem_set d x t) m. Proof. - unfold svalid; intros (PRE & VALID) PREt. split. + unfold smem_valid; intros (PRE & VALID) PREt. split. + split; auto. + intros x0; case (R.eq_dec x x0). - intros; subst; autorewrite with dict_rw. auto. -- cgit From 0bd3d3c9cb1445a588ed4f254c5e036a213801c1 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 28 May 2019 07:13:39 +0200 Subject: simpler definition of reduce --- mppa_k1c/Asmblockdeps.v | 19 ++++- mppa_k1c/abstractbb/AbstractBasicBlocksDef.v | 123 ++++++++++++++++++++------- mppa_k1c/abstractbb/ImpSimuTest.v | 39 +++++---- 3 files changed, 133 insertions(+), 48 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index e0aaee58..55a02633 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1579,20 +1579,31 @@ Definition is_constant (o: op): bool := | _ => false end. -Program Definition failsafe_reduce := Terms.failsafe_reduce is_constant. -Obligation 1. +Lemma is_constant_correct ge o: is_constant o = true -> op_eval ge o [] <> None. +Proof. destruct o; simpl in * |- *; try congruence. destruct ao; simpl in * |- *; try congruence; destruct n; simpl in * |- *; try congruence; unfold arith_eval; destruct ge; simpl in * |- *; try congruence. Qed. +Definition main_reduce (t: Terms.term):= RET (Terms.nofail is_constant t). + +Local Hint Resolve is_constant_correct: wlp. + +Lemma main_reduce_correct t: + WHEN main_reduce t ~> pt THEN Terms.match_pt t pt. +Proof. + wlp_simplify. +Qed. + +Definition reduce := {| Terms.result := main_reduce; Terms.result_correct := main_reduce_correct |}. Definition bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool := if verb then - IST.verb_bblock_simu_test failsafe_reduce string_of_name string_of_op (trans_block p1) (trans_block p2) + IST.verb_bblock_simu_test reduce string_of_name string_of_op (trans_block p1) (trans_block p2) else - IST.bblock_simu_test failsafe_reduce (trans_block p1) (trans_block p2). + IST.bblock_simu_test reduce (trans_block p1) (trans_block p2). Local Hint Resolve IST.bblock_simu_test_correct bblock_simu_reduce IST.verb_bblock_simu_test_correct: wlp. diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v index 8ee04f44..43c70ae5 100644 --- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v +++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v @@ -1,5 +1,6 @@ (** Syntax and Sequential Semantics of Abstract Basic Blocks. *) +Require Import Setoid. Require Import ImpPrelude. Module Type PseudoRegisters. @@ -303,50 +304,114 @@ Definition list_term_get_hid (l: list_term): hashcode := end. -Definition allvalid ge (l: list term) m := forall t, List.In t l -> term_eval ge t m <> None. +Fixpoint allvalid ge (l: list term) m : Prop := + match l with + | nil => True + | t::nil => term_eval ge t m <> None + | t::l' => term_eval ge t m <> None /\ allvalid ge l' m + end. + +Lemma allvalid_extensionality ge (l: list term) m: + allvalid ge l m <-> (forall t, List.In t l -> term_eval ge t m <> None). +Proof. + induction l as [|t l]; simpl; try (tauto). + destruct l. + - intuition (congruence || eauto). + - rewrite IHl; clear IHl. intuition (congruence || eauto). +Qed. -Record pseudo_term: Type := { +Record pseudo_term: Type := intro_fail { mayfail: list term; effect: term }. -Definition match_pseudo_term (t: term) (pt: pseudo_term) := +Definition match_pt (t: term) (pt: pseudo_term) := (forall ge m, term_eval ge t m <> None <-> allvalid ge pt.(mayfail) 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. +Lemma intro_fail_correct (l: list term) (t: term) : + (forall ge m, term_eval ge t m <> None <-> allvalid ge l m) -> match_pt t (intro_fail l t). +Proof. + unfold match_pt; simpl; intros; intuition congruence. +Qed. +Hint Resolve intro_fail_correct: wlp. -Record reduction (t:term):= { - result:> ?? pseudo_term; - result_correct: WHEN result ~> pt THEN match_pseudo_term t pt; -}. -Hint Resolve result_correct: wlp. +Definition identity_fail (t: term):= intro_fail [t] t. -Program Definition identity_reduce (t: term): reduction t := {| result := RET {| mayfail := [t]; effect := t |} |}. -Obligation 1. - unfold match_pseudo_term, allvalid; wlp_simplify; congruence. +Lemma identity_fail_correct (t: term): match_pt t (identity_fail t). +Proof. + eapply intro_fail_correct; simpl; tauto. Qed. -Global Opaque identity_reduce. +Global Opaque identity_fail. +Hint Resolve identity_fail_correct: wlp. + +Definition nofail (is_constant: op -> bool) (t: term):= + match t with + | Input x _ => intro_fail ([])%list t + | o @ [] => if is_constant o then (intro_fail ([])%list t) else (identity_fail t) + | _ => identity_fail t + end. + +Lemma nofail_correct (is_constant: op -> bool) t: + (forall ge o, is_constant o = true -> op_eval ge o nil <> None) -> match_pt t (nofail is_constant t). +Proof. + destruct t; simpl. + + intros; eapply intro_fail_correct; simpl; intuition congruence. + + intros; destruct l; simpl; auto with wlp. + destruct (is_constant o) eqn:Heqo; simpl; intuition eauto with wlp. + eapply intro_fail_correct; simpl; intuition eauto with wlp. +Qed. +Global Opaque nofail. +Hint Resolve nofail_correct: wlp. -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 {| mayfail := []; effect := t |} |} - | o @ [] => match is_constant o with - | true => {| result := RET {| mayfail := []; effect := t |} |} - | false => identity_reduce t - end - | _ => identity_reduce t - end. -Obligation 1. - unfold match_pseudo_term, allvalid; simpl; wlp_simplify; congruence. +Definition term_equiv t1 t2:= forall ge m, term_eval ge t1 m = term_eval ge t2 m. + +Global Instance term_equiv_Equivalence : Equivalence term_equiv. +Proof. + split; intro x; unfold term_equiv; intros; eauto. + eapply eq_trans; eauto. Qed. -Obligation 2. - unfold match_pseudo_term, allvalid; simpl; wlp_simplify. + +Lemma match_pt_term_equiv t1 t2 pt: term_equiv t1 t2 -> match_pt t1 pt -> match_pt t2 pt. +Proof. + unfold match_pt, term_equiv. + intros H. intuition; try (erewrite <- H1 in * |- *; congruence). + erewrite <- H2; eauto; congruence. Qed. -Obligation 3. - intuition congruence. +Hint Resolve match_pt_term_equiv: wlp. + +Definition app_fail (l: list term) (pt: pseudo_term): pseudo_term := + {| mayfail := List.rev_append l pt.(mayfail); effect := pt.(effect) |}. + +Lemma app_fail_correct l pt t1 t2: + match_pt t1 pt -> + match_pt t2 {| mayfail:=t1::l; effect:=t1 |} -> + match_pt t2 (app_fail l pt). +Proof. + unfold match_pt in * |- *. + intros (XV & XE) (YV & YE). + split; intros ge m; try (simpl; auto; fail). + generalize (XV ge m) (YV ge m); rewrite !allvalid_extensionality; simpl. clear XV XE YV YE. + intuition subst. + + rewrite rev_append_rev, in_app_iff, <- in_rev in H3. destruct H3; eauto. + + eapply H3; eauto. + intros. intuition subst. + * eapply H2; eauto. intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff; auto. + * intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff, <- in_rev; auto. Qed. +Hint Resolve app_fail_correct: wlp. +Extraction Inline app_fail. +Global Opaque app_fail. + + +Import ImpCore.Notations. +Local Open Scope impure_scope. + +Record reduction:= { + result:> term -> ?? pseudo_term; + result_correct: forall t, WHEN result t ~> pt THEN match_pt t pt; +}. +Hint Resolve result_correct: wlp. End Terms. diff --git a/mppa_k1c/abstractbb/ImpSimuTest.v b/mppa_k1c/abstractbb/ImpSimuTest.v index 13af4289..8f6b05b7 100644 --- a/mppa_k1c/abstractbb/ImpSimuTest.v +++ b/mppa_k1c/abstractbb/ImpSimuTest.v @@ -67,20 +67,20 @@ Declare Module CoreL: ISeqLanguage. Import CoreL. Import Terms. -Parameter bblock_simu_test: (forall t : term, reduction t) -> bblock -> bblock -> ?? bool. +Parameter bblock_simu_test: reduction -> bblock -> bblock -> ?? bool. -Parameter bblock_simu_test_correct: forall (reduce: forall t, reduction t) (p1 p2 : bblock), +Parameter bblock_simu_test_correct: forall reduce (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) -> + : reduction -> (R.t -> ?? pstring) -> (op -> ?? pstring) -> bblock -> bblock -> ?? bool. Parameter verb_bblock_simu_test_correct: - forall (reduce: forall t, reduction t) + forall reduce (string_of_name : R.t -> ?? pstring) (string_of_op : op -> ?? pstring) (p1 p2 : bblock), @@ -128,7 +128,7 @@ Module D:=ImpPrelude.Dict. Section SimuWithReduce. -Variable reduce: forall t, reduction t. +Variable reduce: reduction. Section CanonBuilding. @@ -230,6 +230,8 @@ Qed. Global Opaque hsmem_get. Hint Resolve hsmem_get_correct: wlp. +Local Opaque allvalid. + Definition smem_model ge (d: smem) (hd:hsmem): Prop := (forall m, allvalid ge hd.(hpre) m <-> smem_valid ge d m) /\ (forall m x, smem_valid ge d m -> smem_eval ge hd x m = (smem_eval ge d x m)). @@ -262,7 +264,7 @@ Proof. destruct (DM0 m) as (PRE & VALID0); clear DM0. assert (VALID1: allvalid ge hd.(hpre) m -> pre d ge m). { unfold smem_valid in PRE; tauto. } assert (VALID2: allvalid ge hd.(hpre) m -> forall x : Dict.R.t, smem_eval ge d x m <> None). { unfold smem_valid in PRE; tauto. } - unfold allvalid in * |- *; simpl. + rewrite !allvalid_extensionality in * |- *; simpl. intuition (subst; eauto). + eapply smem_valid_set_proof; eauto. erewrite <- EQT; eauto. @@ -351,8 +353,10 @@ 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). + induction l as [|t l']; simpl; wlp_xsimplify ltac:(eauto with wlp). + - intros; rewrite! allvalid_extensionality; intuition eauto. + - intros REC ge m; rewrite REC; clear IHl' REC. rewrite !allvalid_extensionality. + simpl; intuition (subst; eauto with wlp localhint). Qed. (*Local Hint Resolve hterm_append_correct: wlp.*) Global Opaque hterm_append. @@ -406,14 +410,14 @@ Proof. 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). + rewrite !allvalid_extensionality in * |- *; 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. + * rewrite allvalid_extensionality in ALLVALID; destruct (ALLVALID ht); simpl; auto. Qed. Local Hint Resolve hsmem_set_correct: wlp. Global Opaque hsmem_set. @@ -520,11 +524,13 @@ Local Hint Resolve hbblock_smem_rec_correct: wlp. Definition hbblock_smem: bblock -> ?? hsmem := fun p => hbblock_smem_rec p {| hpre:= nil ; hpost := Dict.empty |}. +Transparent allvalid. + 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, smem_valid, smem_eval, allvalid, smem_eval, smem_get; simpl; intuition; + unfold smem_model, smem_valid, smem_eval, smem_get; simpl; intuition; rewrite !Dict.empty_spec in * |- *; simpl in * |- *; try congruence. Qed. Global Opaque hbblock_smem. @@ -649,12 +655,14 @@ Obligation 1. 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. + rewrite ! allvalid_extensionality. + unfold incl 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. + rewrite ! allvalid_extensionality in * |- *. + unfold incl in * |- *; intuition eauto. Qed. Theorem g_bblock_simu_test_correct p1 p2: @@ -1011,9 +1019,10 @@ Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool := 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 + DO result2 <~ g_bblock_simu_test (log_assign dict_info log1) - (log_new_term (msg_term cr)) + (*fun _ _ => RET no_log_new_term*) (* REM: too weak !! *) + (log_new_term (msg_term cr)) (* REM: too strong ?? *) (hlog log1 hco_term hco_list) (log_insert log2) hco_term _ -- cgit From 9f111987bb820d2a2b92441752c0d5c0c5df8033 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 28 May 2019 17:35:03 +0200 Subject: minor change in auxiliary lemma --- mppa_k1c/abstractbb/AbstractBasicBlocksDef.v | 32 ++++++++++++++++++---------- 1 file changed, 21 insertions(+), 11 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v index 43c70ae5..5c94d435 100644 --- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v +++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v @@ -325,6 +325,13 @@ Record pseudo_term: Type := intro_fail { effect: term }. +Lemma inf_option_equivalence (A:Type) (o1 o2: option A): + (o1 <> None -> o1 = o2) <-> (forall m1, o1 = Some m1 -> o2 = Some m1). +Proof. + destruct o1; intuition (congruence || eauto). + symmetry; eauto. +Qed. + Definition match_pt (t: term) (pt: pseudo_term) := (forall ge m, term_eval ge t m <> None <-> allvalid ge pt.(mayfail) m) /\ (forall ge m0 m1, term_eval ge t m0 = Some m1 -> term_eval ge pt.(effect) m0 = Some m1). @@ -383,15 +390,12 @@ Hint Resolve match_pt_term_equiv: wlp. Definition app_fail (l: list term) (pt: pseudo_term): pseudo_term := {| mayfail := List.rev_append l pt.(mayfail); effect := pt.(effect) |}. -Lemma app_fail_correct l pt t1 t2: - match_pt t1 pt -> - match_pt t2 {| mayfail:=t1::l; effect:=t1 |} -> - match_pt t2 (app_fail l pt). +Lemma app_fail_allvalid_correct l pt t1 t2: forall + (V1: forall (ge : genv) (m : mem), term_eval ge t1 m <> None <-> allvalid ge (mayfail pt) m) + (V2: forall (ge : genv) (m : mem), term_eval ge t2 m <> None <-> allvalid ge (mayfail {| mayfail := t1 :: l; effect := t1 |}) m) + (ge : genv) (m : mem), term_eval ge t2 m <> None <-> allvalid ge (mayfail (app_fail l pt)) m. Proof. - unfold match_pt in * |- *. - intros (XV & XE) (YV & YE). - split; intros ge m; try (simpl; auto; fail). - generalize (XV ge m) (YV ge m); rewrite !allvalid_extensionality; simpl. clear XV XE YV YE. + intros; generalize (V1 ge m) (V2 ge m); rewrite !allvalid_extensionality; simpl. clear V1 V2. intuition subst. + rewrite rev_append_rev, in_app_iff, <- in_rev in H3. destruct H3; eauto. + eapply H3; eauto. @@ -399,10 +403,16 @@ Proof. * eapply H2; eauto. intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff; auto. * intros; eapply H0; eauto. rewrite rev_append_rev, in_app_iff, <- in_rev; auto. Qed. -Hint Resolve app_fail_correct: wlp. -Extraction Inline app_fail. -Global Opaque app_fail. +Local Hint Resolve app_fail_allvalid_correct. +Lemma app_fail_correct l pt t1 t2: + match_pt t1 pt -> + match_pt t2 {| mayfail:=t1::l; effect:=t1 |} -> + match_pt t2 (app_fail l pt). +Proof. + unfold match_pt in * |- *; intros (V1 & E1) (V2 & E2); split; intros ge m; try (eauto; fail). +Qed. +Extraction Inline app_fail. Import ImpCore.Notations. Local Open Scope impure_scope. -- cgit From 8f88967df89f625d1a15f4c36f49450fe42e97db Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Sat, 8 Jun 2019 22:09:55 +0200 Subject: abstract_bb: few improvements while writing the paper --- mppa_k1c/abstractbb/ImpSimuTest.v | 236 ++++++++++++------ mppa_k1c/abstractbb/Impure/ImpHCons.v | 18 +- mppa_k1c/abstractbb/Impure/ImpPrelude.v | 6 +- .../abstractbb/Impure/ocaml/ImpHConsOracles.ml | 8 +- .../abstractbb/Impure/ocaml/ImpHConsOracles.mli | 2 +- mppa_k1c/abstractbb/SeqSimuTheory.v | 275 +++++++++------------ 6 files changed, 294 insertions(+), 251 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/abstractbb/ImpSimuTest.v b/mppa_k1c/abstractbb/ImpSimuTest.v index 8f6b05b7..ea55b735 100644 --- a/mppa_k1c/abstractbb/ImpSimuTest.v +++ b/mppa_k1c/abstractbb/ImpSimuTest.v @@ -44,7 +44,32 @@ End ISeqLanguage. Module Type ImpDict. -Include 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 rem: forall {A}, t A -> R.t -> t A. + +Parameter rem_spec_eq: forall A (d: t A) x, + get (rem d x) x = None. + +Parameter rem_spec_diff: forall A (d: t A) x y, + x <> y -> get (rem d x) y = get d y. + +Parameter empty: forall {A}, t A. + +Parameter empty_spec: forall A x, + get (empty (A:=A)) x = None. Parameter eq_test: forall {A}, t A -> t A -> ?? bool. @@ -95,9 +120,10 @@ Module ImpSimu (L: ISeqLanguage) (Dict: ImpDict with Module R:=L.LP.R): ImpSimuI Module CoreL:=L. -Module ST := SimuTheory L Dict. +Module ST := SimuTheory L. Import ST. +Import Terms. Definition term_set_hid (t: term) (hid: hashcode): term := match t with @@ -212,9 +238,14 @@ Hint Resolve hLTcons_correct: wlp. (* Second, we use these hashed constructors ! *) -Record hsmem:= {hpre: list term; hpost: Dict.t term}. +Record hsmem:= {hpre: list term; hpost:> Dict.t term}. -Coercion hpost: hsmem >-> Dict.t. +(** evaluation of the post-condition *) +Definition hsmem_post_eval ge (hd: Dict.t term) x (m:mem) := + match Dict.get hd x with + | None => Some (m x) + | Some ht => term_eval ge ht m + end. Definition hsmem_get (d:hsmem) x: ?? term := match Dict.get d x with @@ -223,9 +254,9 @@ Definition hsmem_get (d:hsmem) x: ?? term := 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. + WHEN hsmem_get d x ~> t THEN forall ge m, term_eval ge t m = hsmem_post_eval ge d x m. Proof. - unfold hsmem_get, smem_eval, smem_get; destruct (Dict.get d x); wlp_simplify. + unfold hsmem_get, hsmem_post_eval; destruct (Dict.get d x); wlp_simplify. Qed. Global Opaque hsmem_get. Hint Resolve hsmem_get_correct: wlp. @@ -234,17 +265,17 @@ Local Opaque allvalid. Definition smem_model ge (d: smem) (hd:hsmem): Prop := (forall m, allvalid ge hd.(hpre) m <-> smem_valid ge d m) - /\ (forall m x, smem_valid ge d m -> smem_eval ge hd x m = (smem_eval ge d x m)). + /\ (forall m x, smem_valid ge d m -> hsmem_post_eval ge hd x m = (ST.term_eval ge (d x) m)). Lemma smem_model_smem_valid_alt ge d hd: smem_model ge d hd -> - forall m x, smem_valid ge d m -> smem_eval ge hd x m <> None. + forall m x, smem_valid ge d m -> hsmem_post_eval ge hd x m <> None. Proof. intros (H1 & H2) m x H. rewrite H2; auto. unfold smem_valid 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. + forall m x, allvalid ge hd.(hpre) m -> hsmem_post_eval ge hd x m <> None. Proof. intros (H1 & H2) m x H. eapply smem_model_smem_valid_alt. - split; eauto. @@ -256,14 +287,14 @@ Definition naive_set (hd:hsmem) x (t:term) := Lemma naive_set_correct hd x ht ge d t: smem_model ge d hd -> - (forall m, smem_valid ge d m -> term_eval ge ht m = term_eval ge t m) -> + (forall m, smem_valid ge d m -> term_eval ge ht m = ST.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 smem_valid in PRE; tauto. } - assert (VALID2: allvalid ge hd.(hpre) m -> forall x : Dict.R.t, smem_eval ge d x m <> None). { unfold smem_valid in PRE; tauto. } + assert (VALID2: allvalid ge hd.(hpre) m -> forall x : Dict.R.t, ST.term_eval ge (d x) m <> None). { unfold smem_valid in PRE; tauto. } rewrite !allvalid_extensionality in * |- *; simpl. intuition (subst; eauto). + eapply smem_valid_set_proof; eauto. @@ -272,7 +303,7 @@ Proof. intros X1; exploit smem_valid_set_decompose_2; eauto. rewrite <- EQT; eauto. + exploit smem_valid_set_decompose_1; eauto. - - clear DM0. unfold smem_eval, smem_eval, smem_get in * |- *; simpl. + - clear DM0. unfold hsmem_post_eval, hsmem_post_eval in * |- *; simpl. Local Hint Resolve smem_valid_set_decompose_1. intros; case (R.eq_dec x x0). + intros; subst; rewrite !Dict.set_spec_eq; simpl; eauto. @@ -282,7 +313,7 @@ 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). + /\ (forall m x, allvalid ge hd1.(hpre) m -> hsmem_post_eval ge hd1 x m = hsmem_post_eval ge hd2 x m). Lemma equiv_smem_symmetry ge hd1 hd2: equiv_hsmem ge hd1 hd2 -> equiv_hsmem ge hd2 hd1. @@ -363,11 +394,9 @@ 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)) + | Input y _ => + if R.eq_dec x y then + RET (Dict.rem hd x) else ( log_assign x ht;; RET (Dict.set hd x ht) @@ -379,12 +408,12 @@ Definition smart_set (hd:hsmem) x (ht:term) := 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. + forall ge m y, hsmem_post_eval ge d y m = hsmem_post_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. + unfold hsmem_post_eval; simpl. case (R.eq_dec x0 y). + - intros; subst. rewrite Dict.set_spec_eq, Dict.rem_spec_eq. simpl; congruence. + - intros; rewrite Dict.set_spec_diff, Dict.rem_spec_diff; auto. Qed. (*Local Hint Resolve smart_set_correct: wlp.*) Global Opaque smart_set. @@ -400,7 +429,7 @@ Definition hsmem_set (hd:hsmem) x (t:term) := 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, smem_valid ge d m -> term_eval ge ht m = term_eval ge t m) -> + (forall m, smem_valid ge d m -> term_eval ge ht m = ST.term_eval ge t m) -> smem_model ge (smem_set d x t) nhd. Proof. intros; wlp_simplify. @@ -414,9 +443,9 @@ Proof. - 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. + + intros; subst. unfold hsmem_post_eval; simpl. rewrite !Dict.set_spec_eq. erewrite LIFT, EFFECT; eauto. - + intros; unfold smem_eval; unfold smem_get; simpl. rewrite !Dict.set_spec_diff; auto. + + intros; unfold hsmem_post_eval; simpl. rewrite !Dict.set_spec_diff; auto. * rewrite allvalid_extensionality in ALLVALID; destruct (ALLVALID ht); simpl; auto. Qed. Local Hint Resolve hsmem_set_correct: wlp. @@ -439,53 +468,53 @@ Qed. Local Hint Resolve exp_hterm_correct: wlp. *) -Fixpoint hexp_term (e: exp) (d od: hsmem): ?? term := +Fixpoint exp_hterm (e: exp) (hd hod: hsmem): ?? term := match e with - | PReg x => hsmem_get d x + | PReg x => hsmem_get hd x | Op o le => - DO lt <~ hlist_exp_term le d od;; + DO lt <~ list_exp_hterm le hd hod;; hApp o lt - | Old e => hexp_term e od od + | Old e => exp_hterm e hod hod end -with hlist_exp_term (le: list_exp) (d od: hsmem): ?? list_term := +with list_exp_hterm (le: list_exp) (hd hod: hsmem): ?? list_term := match le with | Enil => hLTnil tt | Econs e le' => - DO t <~ hexp_term e d od;; - DO lt <~ hlist_exp_term le' d od;; + DO t <~ exp_hterm e hd hod;; + DO lt <~ list_exp_hterm le' hd hod;; hLTcons t lt - | LOld le => hlist_exp_term le od od + | LOld le => list_exp_hterm le hod hod end. -Lemma hexp_term_correct_x ge e hod od: +Lemma exp_hterm_correct_x ge e hod od: smem_model ge od hod -> forall hd d, smem_model ge d hd -> - WHEN hexp_term e hd hod ~> t THEN forall m, smem_valid ge d m -> smem_valid ge od m -> term_eval ge t m = term_eval ge (exp_term e d od) m. + WHEN exp_hterm e hd hod ~> t THEN forall m, smem_valid ge d m -> smem_valid ge od m -> term_eval ge t m = ST.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 -> - WHEN hlist_exp_term le hd hod ~> lt THEN forall m, smem_valid ge d m -> smem_valid ge od m -> list_term_eval ge lt m = list_term_eval ge (list_exp_term le d od) m); - unfold smem_model, smem_eval in * |- * ; simpl; wlp_simplify. + WHEN list_exp_hterm le hd hod ~> lt THEN forall m, smem_valid ge d m -> smem_valid ge od m -> list_term_eval ge lt m = ST.list_term_eval ge (list_exp_term le d od) m); + unfold smem_model, hsmem_post_eval in * |- * ; simpl; wlp_simplify. - rewrite H1, <- H4; auto. - rewrite H4, <- H0; simpl; auto. - rewrite H5, <- H0, <- H4; simpl; auto. Qed. -Global Opaque hexp_term. +Global Opaque exp_hterm. -Lemma hexp_term_correct e hd hod: - WHEN hexp_term e hd hod ~> t THEN forall ge od d m, smem_model ge od hod -> smem_model ge d hd -> smem_valid ge d m -> smem_valid ge od m -> term_eval ge t m = term_eval ge (exp_term e d od) m. +Lemma exp_hterm_correct e hd hod: + WHEN exp_hterm e hd hod ~> t THEN forall ge od d m, smem_model ge od hod -> smem_model ge d hd -> smem_valid ge d m -> smem_valid ge od m -> term_eval ge t m = ST.term_eval ge (exp_term e d od) m. Proof. - unfold wlp; intros; eapply hexp_term_correct_x; eauto. + unfold wlp; intros; eapply exp_hterm_correct_x; eauto. Qed. -Hint Resolve hexp_term_correct: wlp. +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 ht <~ hexp_term e hd hod;; + DO ht <~ exp_hterm e hd hod;; DO nd <~ hsmem_set hd x ht;; hinst_smem i' nd hod end. @@ -503,37 +532,41 @@ 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 := +Fixpoint bblock_hsmem_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' + bblock_hsmem_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'. +Lemma bblock_hsmem_rec_correct p: forall hd, + WHEN bblock_hsmem_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. +Global Opaque bblock_hsmem_rec. +Local Hint Resolve bblock_hsmem_rec_correct: wlp. +Definition hsmem_empty: hsmem := {| hpre:= nil ; hpost := Dict.empty |}. -Definition hbblock_smem: bblock -> ?? hsmem - := fun p => hbblock_smem_rec p {| hpre:= nil ; hpost := Dict.empty |}. +Lemma hsmem_empty_correct ge: smem_model ge smem_empty hsmem_empty. +Proof. + unfold smem_model, smem_valid, hsmem_post_eval; simpl; intuition try congruence. + rewrite !Dict.empty_spec; simpl; auto. +Qed. -Transparent allvalid. +Definition bblock_hsmem: bblock -> ?? hsmem + := fun p => bblock_hsmem_rec p hsmem_empty. -Lemma hbblock_smem_correct p: - WHEN hbblock_smem p ~> hd THEN forall ge, smem_model ge (bblock_smem p) hd. +Lemma bblock_hsmem_correct p: + WHEN bblock_hsmem 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, smem_valid, smem_eval, smem_get; simpl; intuition; - rewrite !Dict.empty_spec in * |- *; simpl in * |- *; try congruence. + Local Hint Resolve hsmem_empty_correct. + wlp_simplify. Qed. -Global Opaque hbblock_smem. +Global Opaque bblock_hsmem. End CanonBuilding. @@ -586,13 +619,13 @@ 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). +Lemma hsmem_post_eval_intro (d1 d2: hsmem): + (forall x, Dict.get d1 x = Dict.get d2 x) -> (forall ge x m, hsmem_post_eval ge d1 x m = hsmem_post_eval ge d2 x m). Proof. - unfold smem_eval, smem_get; intros H ge x m; rewrite H. destruct (Dict.get d2 x); auto. + unfold hsmem_post_eval; 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. +Local Hint Resolve bblock_hsmem_correct Dict.eq_test_correct: wlp. Program Definition mk_hash_params (log: term -> ?? unit): Dict.hash_params term := {| @@ -629,9 +662,9 @@ Variable dbg_failpreserv: term -> ?? unit. (* info of additional failure of the 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 d1 <~ bblock_hsmem 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 d2 <~ bblock_hsmem 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 ( @@ -653,12 +686,12 @@ Program Definition g_bblock_simu_test (p1 p2: bblock): ?? bool := 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. + apply bblock_smem_simu; auto. split. + intros m; rewrite <- EQPRE1, <- EQPRE2. rewrite ! allvalid_extensionality. unfold incl in * |- *; intuition eauto. - + intros m0 x m1 VALID; rewrite <- EQPOST1, <- EQPOST2; auto. - erewrite smem_eval_intro; eauto. + + intros m0 x VALID; rewrite <- EQPOST1, <- EQPOST2; auto. + erewrite hsmem_post_eval_intro; eauto. erewrite <- EQPRE2; auto. erewrite <- EQPRE1 in VALID. rewrite ! allvalid_extensionality in * |- *. @@ -677,8 +710,8 @@ 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 hpt: hashP term := {| hash_eq := term_hash_eq; get_hid:=term_get_hid; set_hid:=term_set_hid |}. +Definition hplt: hashP 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 @@ -746,8 +779,8 @@ 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);; + DO hco_term <~ mk_annot (hCons hpt);; + DO hco_list <~ mk_annot (hCons hplt);; g_bblock_simu_test no_log_assign (log_new_term (fun _ => RET msg_unknow_term)) @@ -996,8 +1029,8 @@ Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool := 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 hco_term <~ mk_annot (hCons hpt);; + DO hco_list <~ mk_annot (hCons hplt);; DO result1 <~ g_bblock_simu_test (log_assign dict_info log1) (log_new_term (msg_term cr)) @@ -1017,8 +1050,8 @@ Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool := 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 hco_term <~ mk_annot (hCons hpt);; + DO hco_list <~ mk_annot (hCons hplt);; DO result2 <~ g_bblock_simu_test (log_assign dict_info log1) (*fun _ _ => RET no_log_new_term*) (* REM: too weak !! *) @@ -1074,9 +1107,60 @@ End ImpSimu. Require Import FMapPositive. + +Require Import PArith. +Require Import FMapPositive. + Module ImpPosDict <: ImpDict with Module R:=Pos. -Include PosDict. +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 rem {A} (d:t A) (x:R.t): t A + := PositiveMap.remove x d. + +Lemma rem_spec_eq A (d: t A) x: + get (rem d x) x = None. +Proof. + unfold get, rem; apply PositiveMap.grs; auto. +Qed. + +Lemma rem_spec_diff A (d: t A) x y: + x <> y -> get (rem d x) y = get d y. +Proof. + unfold get, rem; intros; apply PositiveMap.gro; 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. + Import PositiveMap. Fixpoint eq_test {A} (d1 d2: t A): ?? bool := diff --git a/mppa_k1c/abstractbb/Impure/ImpHCons.v b/mppa_k1c/abstractbb/Impure/ImpHCons.v index 637e8296..d8002375 100644 --- a/mppa_k1c/abstractbb/Impure/ImpHCons.v +++ b/mppa_k1c/abstractbb/Impure/ImpHCons.v @@ -110,17 +110,17 @@ Module HConsing. 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. +Axiom xhCons: forall {A}, (hashP A) -> ?? hashConsing A. Extract Constant xhCons => "ImpHConsOracles.xhCons". Definition hCons_eq_msg: pstring := "xhCons: hash eq differs". -Definition hCons {A} (hh: hashH A): ?? (hashConsing A) := - DO hco <~ xhCons hh ;; +Definition hCons {A} (hp: hashP A): ?? (hashConsing A) := + DO hco <~ xhCons hp ;; RET {| hC := (fun x => DO x' <~ hC hco x ;; - DO b0 <~ hash_eq hh x.(hdata) x' ;; + DO b0 <~ hash_eq hp x.(hdata) x' ;; assert_b b0 hCons_eq_msg;; RET x'); next_hid := hco.(next_hid); @@ -130,10 +130,10 @@ Definition hCons {A} (hh: hashH A): ?? (hashConsing A) := |}. -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'. +Lemma hCons_correct A (hp: hashP A): + WHEN hCons hp ~> hco THEN + (forall x y, WHEN hp.(hash_eq) x y ~> b THEN b=true -> (ignore_hid hp x)=(ignore_hid hp y)) -> + forall x, WHEN hco.(hC) x ~> x' THEN ignore_hid hp x.(hdata)=ignore_hid hp x'. Proof. wlp_simplify. Qed. @@ -149,7 +149,7 @@ Record hashV {A:Type}:= { }. Arguments hashV: clear implicits. -Definition hashV_C {A} (test_eq: A -> A -> ?? bool) : hashH (hashV A) := {| +Definition hashV_C {A} (test_eq: A -> A -> ?? bool) : hashP (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 |} diff --git a/mppa_k1c/abstractbb/Impure/ImpPrelude.v b/mppa_k1c/abstractbb/Impure/ImpPrelude.v index 477be65c..de4c7973 100644 --- a/mppa_k1c/abstractbb/Impure/ImpPrelude.v +++ b/mppa_k1c/abstractbb/Impure/ImpPrelude.v @@ -130,17 +130,17 @@ Record hashinfo {A: Type} := { Arguments hashinfo: clear implicits. (* for inductive types with intrinsic hash-consing *) -Record hashH {A:Type}:= { +Record hashP {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 hashH: clear implicits. +Arguments hashP: 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. +Definition ignore_hid {A} (hp: hashP A) (hv:A) := set_hid hp hv unknown_hid. Record hashExport {A:Type}:= { get_info: hashcode -> ?? hashinfo A; diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml index 3994cae6..2b66899b 100644 --- a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml +++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml @@ -17,13 +17,13 @@ let make_dict (type key) (p: key Dict.hash_params) = exception Stop;; -let xhCons (type a) (hh:a hashH) = +let xhCons (type a) (hp:a hashP) = (* 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 hashinfo - let equal x y = hh.hash_eq x.hdata y.hdata + let equal x y = hp.hash_eq x.hdata y.hdata let hash x = Hashtbl.hash x.hcodes end in let module MyHashtbl = Hashtbl.Make(MyHashedType) in @@ -42,7 +42,7 @@ let xhCons (type a) (hh:a hashH) = match MyHashtbl.find_opt t k with | Some d -> d | None -> (*print_string "+";*) - let d = hh.set_hid k.hdata (MyHashtbl.length t) in + let d = hp.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); @@ -58,7 +58,7 @@ let xhCons (type a) (hh:a hashH) = | (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.(hh.get_hid d) <- k) t; + MyHashtbl.iter (fun k d -> a.(hp.get_hid d) <- k) t; { 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 9f5eca89..5075d176 100644 --- a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli +++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli @@ -2,4 +2,4 @@ open ImpPrelude open HConsingDefs val make_dict : 'a Dict.hash_params -> ('a, 'b) Dict.t -val xhCons: 'a hashH -> 'a hashConsing +val xhCons: 'a hashP -> 'a hashConsing diff --git a/mppa_k1c/abstractbb/SeqSimuTheory.v b/mppa_k1c/abstractbb/SeqSimuTheory.v index 8b6a372a..649dd083 100644 --- a/mppa_k1c/abstractbb/SeqSimuTheory.v +++ b/mppa_k1c/abstractbb/SeqSimuTheory.v @@ -3,104 +3,90 @@ *) +Require Coq.Logic.FunctionalExtensionality. (* not really necessary -- see lemma at the end *) 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). +Module SimuTheory (L: SeqLanguage). Export L. Export LP. -Export Terms. + +Inductive term := + | Input (x:R.t) + | App (o: op) (l: list_term) +with list_term := + | LTnil + | LTcons (t:term) (l:list_term) + . + +Fixpoint term_eval (ge: genv) (t: term) (m: mem): option value := + match t with + | Input x => Some (m x) + | App 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 + | LTnil => 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. (* 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. +Record smem:= {pre: genv -> mem -> Prop; post:> R.t -> term}. (** initial symbolic memory *) -Definition smem_empty := {| pre:=fun _ _ => True; post:=Dict.empty |}. +Definition smem_empty := {| pre:=fun _ _ => True; post:=(fun x => Input x) |}. -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 := +Fixpoint exp_term (e: exp) (d old: smem) : term := match e with - | PReg x => smem_get d x - | Op o le => App o (list_exp_term le d old) unknown_hid + | PReg x => d x + | Op o le => App o (list_exp_term le d old) | Old e => exp_term e old old end -with list_exp_term (le: list_exp) (d old: Dict.t term) : list_term := +with list_exp_term (le: list_exp) (d old: smem) : 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 + | Enil => LTnil + | Econs e le' => LTcons (exp_term e d old) (list_exp_term le' d old) | 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 |}. + {| pre:=(fun ge m => (term_eval ge (d x) m) <> None /\ (d.(pre) ge m)); + post:=fun y => if R.eq_dec x y then t else d y |}. 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. + term_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. + unfold smem_set; simpl; case (R.eq_dec x x); try congruence. 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. + x <> y -> term_eval ge (smem_set d x t y) m = term_eval ge (d y) m. Proof. - intros; unfold smem_eval, smem_set, smem_get; simpl; rewrite Dict.set_spec_diff; simpl; auto. + unfold smem_set; simpl; case (R.eq_dec x y); try congruence. 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 @@ -116,8 +102,9 @@ Fixpoint bblock_smem_rec (p: bblock) (d: smem): smem := 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. @@ -140,37 +127,36 @@ 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)) -> + (forall x, term_eval ge (od x) m0 = Some (old x)) -> + forall (d:smem) m1, + (forall x, term_eval ge (d 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. + 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); + (P0:=fun l => forall (d:smem) m1, (forall x, term_eval ge (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, +Lemma inst_smem_abort i m0 x old: forall (d:smem), 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. + term_eval ge (d x) m0 = None -> + term_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. + unfold smem_set; simpl; destruct (R.eq_dec y x); auto. + subst; + generalize (inst_smem_pre_monotonic _ _ _ _ VALID); clear VALID. + unfold smem_set; simpl. intuition congruence. 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. + term_eval ge (d x) m0 = None -> + term_eval ge (bblock_smem_rec p d x) m0 = None. Proof. induction p; simpl; auto. intros d VALID H; erewrite IHp; eauto. clear IHp. @@ -178,11 +164,11 @@ Proof. Qed. Lemma inst_smem_Some_correct1 i m0 old (od:smem): - (forall x, smem_eval ge od x m0 = Some (old x)) -> + (forall x, term_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). + (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> + forall x, term_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. @@ -190,16 +176,14 @@ Proof. 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. + unfold assign, smem_set; simpl. destruct (R.eq_dec x x0); auto. + subst; erewrite term_eval_exp; eauto. 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). + (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> + forall x, term_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. @@ -212,39 +196,37 @@ 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). + -> forall x, term_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 x, term_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. + (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> + inst_run ge i m1 old = None -> exists x, term_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. + intros x0; unfold assign, smem_set; simpl. destruct (R.eq_dec x x0); auto. + subst; erewrite term_eval_exp; eauto. + intuition. constructor 1 with (x:=x); simpl. apply inst_smem_abort; auto. - autorewrite with dict_rw. + rewrite set_spec_eq. 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 x, term_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)) -> + (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> + (forall x, term_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. @@ -255,20 +237,18 @@ Proof. - 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. + intros x0; unfold assign, smem_set; simpl; destruct (R.eq_dec x x0); auto. + subst; erewrite term_eval_exp; eauto. + generalize (H x). rewrite inst_smem_abort; discriminate || auto. - autorewrite with dict_rw. + rewrite set_spec_eq. 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)) -> + (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> + (forall x, term_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. @@ -278,7 +258,7 @@ Proof. - 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). + + assert (X: exists x, term_eval ge (inst_smem i d d x) m0 = None). { eapply inst_smem_None_correct; eauto. } destruct X as [x H1]. generalize (H x). @@ -286,21 +266,20 @@ Proof. 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)) + (forall x, term_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 x, term_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)) -> + (forall x, term_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. @@ -309,17 +288,15 @@ Proof. 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. + + intros x0. unfold assign, smem_set; simpl; destruct (R.eq_dec x x0); auto. + subst; erewrite term_eval_exp; eauto. 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)) -> + (forall x, term_eval ge (d x) m0 = Some (m1 x)) -> pre (bblock_smem_rec p d) ge m0. Proof. Local Hint Resolve inst_valid. @@ -337,22 +314,26 @@ Proof. unfold smem_empty; simpl. auto. Qed. -Definition smem_valid ge d m := pre d ge m /\ forall x, smem_eval ge d x m <> None. +Definition smem_valid ge d m := pre d ge m /\ forall x, term_eval ge (d x) m <> None. + +Definition smem_simu (d1 d2: smem): Prop := + (forall m, smem_valid ge d1 m -> smem_valid ge d2 m) + /\ (forall m0 x, smem_valid ge d1 m0 -> + term_eval ge (d1 x) m0 = term_eval ge (d2 x) m0). + Theorem bblock_smem_simu p1 p2: - (forall m, smem_valid ge (bblock_smem p1) m -> smem_valid ge (bblock_smem p2) m) -> - (forall m0 x m1, smem_valid 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) -> + smem_simu (bblock_smem p1) (bblock_smem p2) -> bblock_simu ge p1 p2. Proof. Local Hint Resolve bblock_smem_valid bblock_smem_Some_correct1. - unfold smem_valid; intros INCL EQUIV m DONTFAIL. + intros (INCL & EQUIV) m DONTFAIL; unfold smem_valid in * |-. 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. + assert (X: forall x, term_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. + + intro x; erewrite <- EQUIV; intuition eauto. congruence. Qed. @@ -370,7 +351,7 @@ Lemma smem_valid_set_decompose_2 d t x m: smem_valid ge (smem_set d x t) m -> term_eval ge t m <> None. Proof. unfold smem_valid; intros ((PRE1 & PRE2) & VALID) H. - generalize (VALID x); autorewrite with dict_rw. + generalize (VALID x); rewrite set_spec_eq. tauto. Qed. @@ -379,50 +360,28 @@ Lemma smem_valid_set_proof d x t m: Proof. unfold smem_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. + + intros x0; unfold smem_set; simpl; case (R.eq_dec x x0); intros; subst; 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. +End SIMU_THEORY. -Definition empty {A}: t A := PositiveMap.empty A. +(** REMARKS: more abstract formulation of the proof... + but relying on functional_extensionality. +*) +Definition smem_correct ge (d: smem) (m: mem) (om: option mem): Prop:= + forall m', om=Some m' <-> (d.(pre) ge m /\ forall x, term_eval ge (d x) m = Some (m' x)). -Lemma empty_spec A x: - get (empty (A:=A)) x = None. +Lemma bblock_smem_correct ge p m: smem_correct ge (bblock_smem p) m (run ge p m). Proof. - unfold get, empty; apply PositiveMap.gempty; auto. + unfold smem_correct; simpl; intros m'; split. + + intros; split. + * eapply bblock_smem_valid; eauto. + * eapply bblock_smem_Some_correct1; eauto. + + intros (H1 & H2). + destruct (bblock_smem_Some_correct2 ge p m m') as (m2 & X & Y); eauto. + rewrite X. f_equal. + apply FunctionalExtensionality.functional_extensionality; auto. Qed. -End PosDict. \ No newline at end of file +End SimuTheory. -- cgit From 69f4580c239548082d899b3719b5de2d686252c3 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Wed, 12 Jun 2019 17:05:55 +0200 Subject: Removing the Admitted warning when running "make check-admitted" --- mppa_k1c/ExtValues.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/ExtValues.v b/mppa_k1c/ExtValues.v index 8e6aa028..3370fae3 100644 --- a/mppa_k1c/ExtValues.v +++ b/mppa_k1c/ExtValues.v @@ -424,7 +424,7 @@ Qed. (* Lemma signed_0_eqb : forall x, (Z.eqb (Int.signed x) 0) = Int.eq x Int.zero. -Admitted. +Qed. *) Lemma Z_quot_le: forall a b, -- cgit From 60f5b79492144740338e5d77653c4dc3e61606e7 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 14 Jun 2019 17:46:11 +0200 Subject: [BROKEN] Replaced the accesses lists by Maps, does not compile --- mppa_k1c/PostpassSchedulingOracle.ml | 66 +++++++++++++++++++++++++++++++----- 1 file changed, 58 insertions(+), 8 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 2fc561ee..c153576b 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -699,20 +699,56 @@ let instruction_usages bb = * Latency constraints building *) -type access = { inst: int; loc: location } +(* type access = { inst: int; loc: location } *) -let rec get_accesses llocs laccs = - let accesses loc laccs = List.filter (fun acc -> acc.loc = loc) laccs - in match llocs with - | [] -> [] - | loc :: llocs -> (accesses loc laccs) @ (get_accesses llocs laccs) +let preg2int pr = Camlcoq.P.to_int @@ Asmblockdeps.ppos pr + +let loc2int = function + | Mem -> 1 + | Reg pr -> preg2int pr + +module OrderedLoc : Map.OrderedType = struct + type t = location + let compare l l' = compare (loc2int l) (loc2int l') +end + +module LocMap = Map.Make(OrderedLoc) let rec intlist n = if n < 0 then failwith "intlist: n < 0" else if n = 0 then [] else (n-1) :: (intlist (n-1)) -let latency_constraints bb = (* failwith "latency_constraints: not implemented" *) +let rec list2locmap v = function + | [] -> LocMap.empty + | loc :: l -> LocMap.add loc v (list2locmap v l) + +let get_accesses locs locmap = List.map (fun l _ -> List.mem l locs) locmap + +let latency_constraints bb = + let written = ref LocMap.empty + and read = ref LocMap.empty + and count = ref 0 + and constraints = ref [] + and instr_infos = instruction_infos bb + in let step (i: inst_info) = + let write_accesses = list2locmap !count i.write_locs + and read_accesses = list2locmap !count i.read_locs + in let raw = get_accesses i.read_locs !written + and waw = get_accesses i.write_locs !written + and war = get_accesses i.write_locs !read + in begin + Map.iter (fun l i -> constraints := {instr_from = i; instr_to = !count; latency = (List.nth instr_infos i).latency} :: !constraints) raw; + Map.iter (fun l i -> constraints := {instr_from = i; instr_to = !count; latency = (List.nth instr_infos i).latency} :: !constraints) waw; + Map.iter (fun l i -> constraints := {instr_from = i; instr_to = !count; latency = 0} :: !constraints) war; + if i.is_control then List.iter (fun n -> constraints := {instr_from = n; instr_to = !count; latency = 0} :: !constraints) (intlist !count); + written := Map.union (fun _ i1 i2 -> if i1 < i2 then Some i2 else Some i1) !written write_accesses; + read := Map.union (fun _ i1 i2 -> if i1 < i2 then Some i2 else Some i1) !read read_accesses; + count := !count + 1 + end + in (List.iter step instr_infos; !constraints) + +(* let latency_constraints bb = (* failwith "latency_constraints: not implemented" *) let written = ref [] and read = ref [] and count = ref 0 @@ -734,6 +770,7 @@ let latency_constraints bb = (* failwith "latency_constraints: not implemented" count := !count + 1 end in (List.iter step instr_infos; !constraints) +*) (** * Using the InstructionScheduler @@ -829,7 +866,7 @@ let print_bb oc bb = let asm_instructions = Asm.unfold_bblock bb in List.iter (print_inst oc) asm_instructions -let do_schedule bb = +let real_do_schedule bb = let problem = build_problem bb in let solution = (if !Clflags.option_fpostpass_sched = "ilp" then validated_scheduler cascaded_scheduler @@ -850,6 +887,19 @@ let do_schedule bb = end; bundles) +let do_schedule bb = + let nb_instructions = Camlcoq.Z.to_int64 @@ Asmvliw.size bb + in let start_time = (Gc.major(); (Unix.times ()).Unix.tms_utime) + in let sched = real_do_schedule bb + in let refer = ref sched + in begin + for i = 1 to 100-1 do + refer := (if i > 0 then real_do_schedule bb else real_do_schedule bb); + done; + Printf.printf "%Ld: %f\n" nb_instructions ((Unix.times ()).Unix.tms_utime -. start_time); + sched + end + (** * Dumb schedule if the above doesn't work *) -- cgit From 8697837760ad3b0002ed94ff3e83a60a15c259a1 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 17 Jun 2019 14:31:37 +0200 Subject: [NOT TESTED] ça compile MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- mppa_k1c/PostpassSchedulingOracle.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index c153576b..9912fbcb 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -707,7 +707,7 @@ let loc2int = function | Mem -> 1 | Reg pr -> preg2int pr -module OrderedLoc : Map.OrderedType = struct +module OrderedLoc = struct type t = location let compare l l' = compare (loc2int l) (loc2int l') end @@ -723,7 +723,7 @@ let rec list2locmap v = function | [] -> LocMap.empty | loc :: l -> LocMap.add loc v (list2locmap v l) -let get_accesses locs locmap = List.map (fun l _ -> List.mem l locs) locmap +let get_accesses locs locmap = LocMap.filter (fun l _ -> List.mem l locs) locmap let latency_constraints bb = let written = ref LocMap.empty @@ -738,12 +738,12 @@ let latency_constraints bb = and waw = get_accesses i.write_locs !written and war = get_accesses i.write_locs !read in begin - Map.iter (fun l i -> constraints := {instr_from = i; instr_to = !count; latency = (List.nth instr_infos i).latency} :: !constraints) raw; - Map.iter (fun l i -> constraints := {instr_from = i; instr_to = !count; latency = (List.nth instr_infos i).latency} :: !constraints) waw; - Map.iter (fun l i -> constraints := {instr_from = i; instr_to = !count; latency = 0} :: !constraints) war; + LocMap.iter (fun l i -> constraints := {instr_from = i; instr_to = !count; latency = (List.nth instr_infos i).latency} :: !constraints) raw; + LocMap.iter (fun l i -> constraints := {instr_from = i; instr_to = !count; latency = (List.nth instr_infos i).latency} :: !constraints) waw; + LocMap.iter (fun l i -> constraints := {instr_from = i; instr_to = !count; latency = 0} :: !constraints) war; if i.is_control then List.iter (fun n -> constraints := {instr_from = n; instr_to = !count; latency = 0} :: !constraints) (intlist !count); - written := Map.union (fun _ i1 i2 -> if i1 < i2 then Some i2 else Some i1) !written write_accesses; - read := Map.union (fun _ i1 i2 -> if i1 < i2 then Some i2 else Some i1) !read read_accesses; + written := LocMap.union (fun _ i1 i2 -> if i1 < i2 then Some i2 else Some i1) !written write_accesses; + read := LocMap.union (fun _ i1 i2 -> if i1 < i2 then Some i2 else Some i1) !read read_accesses; count := !count + 1 end in (List.iter step instr_infos; !constraints) -- cgit From 45e8a0997169b0b081f3cea500debc237e4a8c76 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 17 Jun 2019 18:43:14 +0200 Subject: [BROKEN] Fixed the dependency oracle, does not compile I was removing too many dependencies --- mppa_k1c/PostpassSchedulingOracle.ml | 50 ++++++++++++++++++++++++++++++------ 1 file changed, 42 insertions(+), 8 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 9912fbcb..75dc2495 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -707,26 +707,59 @@ let loc2int = function | Mem -> 1 | Reg pr -> preg2int pr -module OrderedLoc = struct - type t = location - let compare l l' = compare (loc2int l) (loc2int l') +module HashedLoc = struct + type t = { loc: location; key: int } + let equal l1 l2 = (l1.key = l2.key) + let hash l = l.key + let create (l:location) : t = { loc=l; key = loc2int l } end -module LocMap = Map.Make(OrderedLoc) +module LocHash = Hashtbl.Make(HashedLoc) + +(* Hash table : location => list of instruction ids *) let rec intlist n = if n < 0 then failwith "intlist: n < 0" else if n = 0 then [] else (n-1) :: (intlist (n-1)) +(* Returns a list of instruction ids *) +let rec get_accesses hashloc = function + | [] -> [] + | loc :: llocs -> (LocHash.find hashloc loc) @ (get_accesses hashloc llocs) + +let latency_constraints bb = + let written = LocHash.create 0 + and read = LocHash.create 0 + and count = ref 0 + and constraints = ref [] + and instr_infos = instruction_infos bb + in let step (i: inst_info) = + let raw = get_accesses i.read_locs written + and waw = get_accesses i.write_locs written + and war = get_accesses i.write_locs read + in begin + List.iter (fun i -> constraints := {instr_from = i; instr_to = !count; latency = (List.nth instr_infos i).latency} :: !constraints) raw; + List.iter (fun i -> constraints := {instr_from = i; instr_to = !count; latency = (List.nth instr_infos i).latency} :: !constraints) waw; + List.iter (fun i -> constraints := {instr_from = i; instr_to = !count; latency = 0} :: !constraints) war; + if i.is_control then List.iter (fun n -> constraints := {instr_from = n; instr_to = !count; latency = 0} :: !constraints) (intlist !count); + (* Updating "read" and "written" hashmaps *) + List.iter (fun loc -> + begin + LocHash.replace written loc [!count]; + LocHash.replace read loc []; (* Clearing all the entries of "read" hashmap when a register is written *) + end) i.write_locs; + List.iter (fun loc -> LocHash.replace read loc (LocHash.find read loc)) i.read_locs; + count := !count + 1 + end + in (List.iter step instr_infos; !constraints) + +(* let rec list2locmap v = function | [] -> LocMap.empty | loc :: l -> LocMap.add loc v (list2locmap v l) -let get_accesses locs locmap = LocMap.filter (fun l _ -> List.mem l locs) locmap - -let latency_constraints bb = - let written = ref LocMap.empty + let written = ref (LocHash.create 0) and read = ref LocMap.empty and count = ref 0 and constraints = ref [] @@ -747,6 +780,7 @@ let latency_constraints bb = count := !count + 1 end in (List.iter step instr_infos; !constraints) + *) (* let latency_constraints bb = (* failwith "latency_constraints: not implemented" *) let written = ref [] -- cgit From 99cf129352db347291e893d1102df9804fd04472 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Mon, 17 Jun 2019 18:53:12 +0200 Subject: [BROKEN] still broken, just fixing a logical detail --- mppa_k1c/PostpassSchedulingOracle.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 75dc2495..09d5e15b 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -749,7 +749,7 @@ let latency_constraints bb = LocHash.replace written loc [!count]; LocHash.replace read loc []; (* Clearing all the entries of "read" hashmap when a register is written *) end) i.write_locs; - List.iter (fun loc -> LocHash.replace read loc (LocHash.find read loc)) i.read_locs; + List.iter (fun loc -> LocHash.replace read loc ((!count) :: (LocHash.find read loc))) i.read_locs; count := !count + 1 end in (List.iter step instr_infos; !constraints) -- cgit From b480d21954b63abb93411e7691e4cafc9d658f3f Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 18 Jun 2019 16:02:40 +0200 Subject: [NOT TESTED] Compiles and should work ? --- mppa_k1c/PostpassSchedulingOracle.ml | 28 +++++++++++++++++----------- 1 file changed, 17 insertions(+), 11 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 09d5e15b..b54dfeda 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -707,14 +707,15 @@ let loc2int = function | Mem -> 1 | Reg pr -> preg2int pr -module HashedLoc = struct +(* module HashedLoc = struct type t = { loc: location; key: int } let equal l1 l2 = (l1.key = l2.key) let hash l = l.key let create (l:location) : t = { loc=l; key = loc2int l } -end +end *) -module LocHash = Hashtbl.Make(HashedLoc) +(* module LocHash = Hashtbl.Make(HashedLoc) *) +module LocHash = Hashtbl (* Hash table : location => list of instruction ids *) @@ -723,21 +724,26 @@ let rec intlist n = else if n = 0 then [] else (n-1) :: (intlist (n-1)) +let find_in_hash hashloc loc = + match LocHash.find_opt hashloc loc with + | Some idl -> idl + | None -> [] + (* Returns a list of instruction ids *) -let rec get_accesses hashloc = function +let rec get_accesses hashloc (ll: location list) = match ll with | [] -> [] - | loc :: llocs -> (LocHash.find hashloc loc) @ (get_accesses hashloc llocs) + | loc :: llocs -> (find_in_hash hashloc loc) @ (get_accesses hashloc llocs) let latency_constraints bb = - let written = LocHash.create 0 - and read = LocHash.create 0 + let written = LocHash.create 70 + and read = LocHash.create 70 and count = ref 0 and constraints = ref [] and instr_infos = instruction_infos bb in let step (i: inst_info) = - let raw = get_accesses i.read_locs written - and waw = get_accesses i.write_locs written - and war = get_accesses i.write_locs read + let raw = get_accesses written i.read_locs + and waw = get_accesses written i.write_locs + and war = get_accesses read i.write_locs in begin List.iter (fun i -> constraints := {instr_from = i; instr_to = !count; latency = (List.nth instr_infos i).latency} :: !constraints) raw; List.iter (fun i -> constraints := {instr_from = i; instr_to = !count; latency = (List.nth instr_infos i).latency} :: !constraints) waw; @@ -749,7 +755,7 @@ let latency_constraints bb = LocHash.replace written loc [!count]; LocHash.replace read loc []; (* Clearing all the entries of "read" hashmap when a register is written *) end) i.write_locs; - List.iter (fun loc -> LocHash.replace read loc ((!count) :: (LocHash.find read loc))) i.read_locs; + List.iter (fun loc -> LocHash.replace read loc ((!count) :: (find_in_hash read loc))) i.read_locs; count := !count + 1 end in (List.iter step instr_infos; !constraints) -- cgit From 82db72dbd06eced8f72ca4a41e08892b908b5036 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 18 Jun 2019 16:08:25 +0200 Subject: Reverting the unwanted time measurement from the other branch --- mppa_k1c/PostpassSchedulingOracle.ml | 15 +-------------- 1 file changed, 1 insertion(+), 14 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index b54dfeda..462e9cd0 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -906,7 +906,7 @@ let print_bb oc bb = let asm_instructions = Asm.unfold_bblock bb in List.iter (print_inst oc) asm_instructions -let real_do_schedule bb = +let do_schedule bb = let problem = build_problem bb in let solution = (if !Clflags.option_fpostpass_sched = "ilp" then validated_scheduler cascaded_scheduler @@ -927,19 +927,6 @@ let real_do_schedule bb = end; bundles) -let do_schedule bb = - let nb_instructions = Camlcoq.Z.to_int64 @@ Asmvliw.size bb - in let start_time = (Gc.major(); (Unix.times ()).Unix.tms_utime) - in let sched = real_do_schedule bb - in let refer = ref sched - in begin - for i = 1 to 100-1 do - refer := (if i > 0 then real_do_schedule bb else real_do_schedule bb); - done; - Printf.printf "%Ld: %f\n" nb_instructions ((Unix.times ()).Unix.tms_utime -. start_time); - sched - end - (** * Dumb schedule if the above doesn't work *) -- cgit