diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-14 13:02:40 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-14 13:02:40 +0200 |
commit | b15c0109a6e6a6bbba1c09a0c5fbfdc6ecf51f0e (patch) | |
tree | e67b8143fbe3ee3ec60dc0923647a173c01eab3d /mppa_k1c/abstractbb | |
parent | 13ea0149e1994c5489d9aed00e7486e49d687889 (diff) | |
download | compcert-kvx-b15c0109a6e6a6bbba1c09a0c5fbfdc6ecf51f0e.tar.gz compcert-kvx-b15c0109a6e6a6bbba1c09a0c5fbfdc6ecf51f0e.zip |
abstractbb: support of removing useless computations
Diffstat (limited to 'mppa_k1c/abstractbb')
-rw-r--r-- | mppa_k1c/abstractbb/DepTreeTheory.v | 365 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/ImpDep.v | 264 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpCore.v | 10 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpHCons.v | 95 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Impure/ImpPrelude.v | 29 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml | 16 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli | 1 |
7 files changed, 481 insertions, 299 deletions
diff --git a/mppa_k1c/abstractbb/DepTreeTheory.v b/mppa_k1c/abstractbb/DepTreeTheory.v index bf45d11a..6646d4f5 100644 --- a/mppa_k1c/abstractbb/DepTreeTheory.v +++ b/mppa_k1c/abstractbb/DepTreeTheory.v @@ -1,13 +1,13 @@ (** Dependency Trees of Abstract Basic Blocks -with a purely-functional-but-exponential equivalence test. +with a purely-functional-but-exponential test. *) Require Setoid. (* in order to rewrite <-> *) Require Export AbstractBasicBlocksDef. - +Require Import List. Module Type PseudoRegDictionary. @@ -39,12 +39,9 @@ Module DepTree (L: SeqLanguage) (Dict: PseudoRegDictionary with Module R:=L.LP.R Export L. Export LP. -Local Open Scope list. Section DEPTREE. -Variable ge: genv. - (** Dependency Trees of these "bblocks" NB: each tree represents the successive computations in one given resource @@ -54,102 +51,90 @@ NB: each tree represents the successive computations in one given resource Inductive tree := | Tname (x:R.t) | Top (o: op) (l: list_tree) - | Terase (new old:tree) (* assignment in the resource: [new] replaces [old] *) with list_tree := | Tnil: list_tree | Tcons (t:tree) (l:list_tree): list_tree . -Fixpoint tree_eval (t: tree) (m: mem): option value := +Fixpoint tree_eval (ge: genv) (t: tree) (m: mem): option value := match t with | Tname x => Some (m x) | Top o l => - match list_tree_eval l m with + match list_tree_eval ge l m with | Some v => op_eval ge o v | _ => None end - | Terase new old => - (* NB: we simply check whether the old computations has aborted *) - match tree_eval old m with - | Some _ => tree_eval new m - | _ => None - end end -with list_tree_eval (l: list_tree) (m: mem) {struct l}: option (list value) := +with list_tree_eval ge (l: list_tree) (m: mem) {struct l}: option (list value) := match l with | Tnil => Some nil | Tcons t l' => - match (tree_eval t m), (list_tree_eval l' m) with + match (tree_eval ge t m), (list_tree_eval ge l' m) with | Some v, Some lv => Some (v::lv) | _, _ => None end end. -Definition deps:= Dict.t tree. - -Definition deps_get (d:deps) x := +Definition deps_get (d:Dict.t tree) x := match Dict.get d x with | None => Tname x | Some t => t end. -Lemma set_spec_eq d x t: - deps_get (Dict.set d x t) x = t. -Proof. - unfold deps_get; rewrite Dict.set_spec_eq; simpl; auto. -Qed. - -Lemma set_spec_diff d x y t: - x <> y -> deps_get (Dict.set d x t) y = deps_get d y. -Proof. - unfold deps_get; intros; rewrite Dict.set_spec_diff; simpl; auto. -Qed. - -Lemma empty_spec x: deps_get Dict.empty x = Tname x. -Proof. - unfold deps_get; rewrite Dict.empty_spec; simpl; auto. -Qed. - -Hint Rewrite set_spec_eq empty_spec: dict_rw. - -Fixpoint exp_tree (e: exp) (d old: deps): tree := +Fixpoint exp_tree (e: exp) d old: tree := match e with | PReg x => deps_get d x | Op o le => Top o (list_exp_tree le d old) | Old e => exp_tree e old old end -with list_exp_tree (le: list_exp) (d old: deps): list_tree := +with list_exp_tree (le: list_exp) d old: list_tree := match le with | Enil => Tnil | Econs e le' => Tcons (exp_tree e d old) (list_exp_tree le' d old) | LOld le => list_exp_tree le old old end. -Definition failsafe (t: tree): bool := - match t with - | Tname x => true - | Top o Tnil => is_constant o - | _ => false - end. +Record deps:= {pre: genv -> mem -> Prop; post: Dict.t tree}. + +Coercion post: deps >-> Dict.t. + +Definition deps_eval ge (d: deps) x (m:mem) := + tree_eval ge (deps_get d x) m. + +Definition deps_set (d:deps) x (t:tree) := + {| pre:=(fun ge m => (deps_eval ge d x m) <> None /\ (d.(pre) ge m)); + post:=Dict.set d x t |}. + +Definition deps_empty := {| pre:=fun _ _ => True; post:=Dict.empty |}. + +Variable ge: genv. + +Lemma set_spec_eq d x t m: + deps_eval ge (deps_set d x t) x m = tree_eval ge t m. +Proof. + unfold deps_eval, deps_set, deps_get; simpl; rewrite Dict.set_spec_eq; simpl; auto. +Qed. -Local Hint Resolve is_constant_correct. +Lemma set_spec_diff d x y t m: + x <> y -> deps_eval ge (deps_set d x t) y m = deps_eval ge d y m. +Proof. + intros; unfold deps_eval, deps_set, deps_get; simpl; rewrite Dict.set_spec_diff; simpl; auto. +Qed. -Lemma failsafe_correct (t: tree) m: failsafe t = true -> tree_eval t m <> None. +Lemma deps_eval_empty x m: deps_eval ge deps_empty x m = Some (m x). Proof. - destruct t; simpl; try congruence. - destruct l; simpl; try congruence. - eauto. + unfold deps_eval, deps_get; rewrite Dict.empty_spec; simpl; auto. Qed. +Hint Rewrite set_spec_eq deps_eval_empty: dict_rw. + Fixpoint inst_deps (i: inst) (d old: deps): deps := match i with | nil => d | (x, e)::i' => - let t0:=deps_get d x in - let t1:=exp_tree e d old in - let v':=if failsafe t0 then t1 else (Terase t1 t0) in - inst_deps i' (Dict.set d x v') old + let t:=exp_tree e d old in + inst_deps i' (deps_set d x t) old end. Fixpoint bblock_deps_rec (p: bblock) (d: deps): deps := @@ -160,214 +145,236 @@ Fixpoint bblock_deps_rec (p: bblock) (d: deps): deps := bblock_deps_rec p' d' end. +Local Hint Resolve deps_eval_empty. + Definition bblock_deps: bblock -> deps - := fun p => bblock_deps_rec p Dict.empty. + := fun p => bblock_deps_rec p deps_empty. + +Lemma inst_deps_pre_monotonic i old: forall d m, + (pre (inst_deps i d old) ge m) -> (pre d ge m). +Proof. + induction i as [|[y e] i IHi]; simpl; auto. + intros d a H; generalize (IHi _ _ H); clear H IHi. + unfold deps_set; simpl; intuition. +Qed. -(** Main Result: the [bblock_deps_equiv] theorem states that bblocks with the same dependencies are observationaly equals *) +Lemma bblock_deps_pre_monotonic p: forall d m, + (pre (bblock_deps_rec p d) ge m) -> (pre d ge m). +Proof. + induction p as [|i p' IHp']; simpl; eauto. + intros d a H; eapply inst_deps_pre_monotonic; eauto. +Qed. +Local Hint Resolve inst_deps_pre_monotonic bblock_deps_pre_monotonic. Lemma tree_eval_exp e od m0 old: - (forall x, tree_eval (deps_get od x) m0 = Some (old x)) -> - forall d m1, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - (tree_eval (exp_tree e d od) m0) = exp_eval ge e m1 old. + (forall x, deps_eval ge od x m0 = Some (old x)) -> + forall d m1, + (forall x, deps_eval ge d x m0 = Some (m1 x)) -> + tree_eval ge (exp_tree e d od) m0 = exp_eval ge e m1 old. Proof. - intro H. - induction e using exp_mut with (P0:=fun l => forall d m1, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> list_tree_eval (list_exp_tree l d od) m0 = list_exp_eval ge l m1 old); simpl; auto. + unfold deps_eval in * |- *; intro H. + induction e using exp_mut with + (P0:=fun l => forall (d:deps) m1, (forall x, tree_eval ge (deps_get d x) m0 = Some (m1 x)) -> list_tree_eval ge (list_exp_tree l d od) m0 = list_exp_eval ge l m1 old); + simpl; auto. - intros; erewrite IHe; eauto. - - intros; erewrite IHe, IHe0; eauto. + - intros. erewrite IHe, IHe0; eauto. Qed. -Lemma tree_eval_inst_abort i m0 x old: forall d, - tree_eval (deps_get d x) m0 = None -> - tree_eval (deps_get (inst_deps i d old) x) m0 = None. +Lemma inst_deps_abort i m0 x old: forall d, + pre (inst_deps i d old) ge m0 -> + deps_eval ge d x m0 = None -> + deps_eval ge (inst_deps i d old) x m0 = None. Proof. induction i as [|[y e] i IHi]; simpl; auto. - intros d H; erewrite IHi; eauto. clear IHi. + intros d VALID H; erewrite IHi; eauto. clear IHi. destruct (R.eq_dec x y). * subst; autorewrite with dict_rw. - generalize (failsafe_correct (deps_get d y) m0). - destruct (failsafe (deps_get d y)); simpl; intuition try congruence. - rewrite H; simpl. auto. - * rewrite! set_spec_diff; auto. + generalize (inst_deps_pre_monotonic _ _ _ _ VALID); clear VALID. + unfold deps_set; simpl; intuition congruence. + * rewrite set_spec_diff; auto. Qed. -Lemma tree_eval_abort p m0 x: forall d, - tree_eval (deps_get d x) m0 = None -> - tree_eval (deps_get (bblock_deps_rec p d) x) m0 = None. +Lemma block_deps_rec_abort p m0 x: forall d, + pre (bblock_deps_rec p d) ge m0 -> + deps_eval ge d x m0 = None -> + deps_eval ge (bblock_deps_rec p d) x m0 = None. Proof. induction p; simpl; auto. - intros d H; erewrite IHp; eauto. clear IHp. - eapply tree_eval_inst_abort; eauto. + intros d VALID H; erewrite IHp; eauto. clear IHp. + eapply inst_deps_abort; eauto. Qed. -Lemma tree_eval_inst_Some_correct1 i m0 old od: - (forall x, tree_eval (deps_get od x) m0 = Some (old x)) -> - forall (m1 m2: mem) d, +Lemma inst_deps_Some_correct1 i m0 old od: + (forall x, deps_eval ge od x m0 = Some (old x)) -> + forall (m1 m2: mem) (d: deps), inst_run ge i m1 old = Some m2 -> - (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - (forall x, tree_eval (deps_get (inst_deps i d od) x) m0 = Some (m2 x)). + (forall x, deps_eval ge d x m0 = Some (m1 x)) -> + forall x, deps_eval ge (inst_deps i d od) x m0 = Some (m2 x). Proof. intro X; induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H. - inversion_clear H; eauto. - intros H0 x0. - remember (exp_eval ge e m1 old) as ov. - destruct ov. - + refine (IHi _ _ _ _ _ _); eauto. - clear x0; intros x0. - unfold assign; destruct (R.eq_dec x x0). - * subst; autorewrite with dict_rw. - destruct (failsafe (deps_get d x0)); simpl; try rewrite H0; - erewrite tree_eval_exp; eauto. - * rewrite set_spec_diff; auto. - + inversion H. + destruct (exp_eval ge e m1 old) eqn:Heqov; try congruence. + refine (IHi _ _ _ _ _ _); eauto. + clear x0; intros x0. + unfold assign; destruct (R.eq_dec x x0). + * subst; autorewrite with dict_rw. + erewrite tree_eval_exp; eauto. + * rewrite set_spec_diff; auto. Qed. -Local Hint Resolve tree_eval_inst_Some_correct1 tree_eval_abort. - -Lemma tree_eval_Some_correct1 p m0: forall (m1 m2: mem) d, +Lemma bblocks_deps_rec_Some_correct1 p m0: forall (m1 m2: mem) d, run ge p m1 = Some m2 -> - (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - (forall x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = Some (m2 x)). + (forall x, deps_eval ge d x m0 = Some (m1 x)) -> + forall x, deps_eval ge (bblock_deps_rec p d) x m0 = Some (m2 x). Proof. + Local Hint Resolve inst_deps_Some_correct1. induction p as [ | i p]; simpl; intros m1 m2 d H. - inversion_clear H; eauto. - intros H0 x0. - remember (inst_run ge i m1 m1) as om. - destruct om. + destruct (inst_run ge i m1 m1) eqn: Heqov. + refine (IHp _ _ _ _ _ _); eauto. + inversion H. Qed. Lemma bblock_deps_Some_correct1 p m0 m1: - run ge p m0 = Some m1 - -> forall x, tree_eval (deps_get (bblock_deps p) x) m0 = Some (m1 x). + run ge p m0 = Some m1 + -> forall x, deps_eval ge (bblock_deps p) x m0 = Some (m1 x). Proof. - intros; eapply tree_eval_Some_correct1; - intros; autorewrite with dict_rw; simpl; eauto. + intros; eapply bblocks_deps_rec_Some_correct1; eauto. Qed. -Lemma tree_eval_inst_None_correct i m0 old od: - (forall x, tree_eval (deps_get od x) m0 = Some (old x)) -> - forall m1 d, (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - inst_run ge i m1 old = None <-> exists x, tree_eval (deps_get (inst_deps i d od) x) m0 = None. +Lemma inst_deps_None_correct i m0 old od: + (forall x, deps_eval ge od x m0 = Some (old x)) -> + forall m1 d, pre (inst_deps i d od) ge m0 -> + (forall x, deps_eval ge d x m0 = Some (m1 x)) -> + inst_run ge i m1 old = None -> exists x, deps_eval ge (inst_deps i d od) x m0 = None. Proof. intro X; induction i as [|[x e] i IHi]; simpl; intros m1 d. - - constructor 1; [discriminate | intros [x H']; rewrite H in H'; discriminate]. - - intros H0. - remember (exp_eval ge e m1 old) as ov. - destruct ov. - + refine (IHi _ _ _); eauto. + - discriminate. + - intros VALID H0. + destruct (exp_eval ge e m1 old) eqn: Heqov. + + refine (IHi _ _ _ _); eauto. intros x0; unfold assign; destruct (R.eq_dec x x0). * subst; autorewrite with dict_rw. - destruct (failsafe (deps_get d x0)); simpl; try rewrite H0; erewrite tree_eval_exp; eauto. * rewrite set_spec_diff; auto. + intuition. constructor 1 with (x:=x); simpl. - apply tree_eval_inst_abort. + apply inst_deps_abort; auto. autorewrite with dict_rw. - destruct (failsafe (deps_get d x)); simpl; try rewrite H0; erewrite tree_eval_exp; eauto. Qed. - -Lemma tree_eval_None_correct p m0: forall m1 d, - (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - run ge p m1 = None <-> exists x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = None. -Proof. - induction p as [|i p IHp]; simpl; intros m1 d. - - constructor 1; [discriminate | intros [x H']; rewrite H in H'; discriminate]. - - intros H0. - remember (inst_run ge i m1 m1) as om. - destruct om. - + refine (IHp _ _ _); eauto. - + intuition. - assert (X: inst_run ge i m1 m1 = None); auto. - rewrite tree_eval_inst_None_correct in X; auto. - destruct X as [x H1]. - constructor 1 with (x:=x); simpl; auto. -Qed. - -Lemma bblock_deps_None_correct p m: - run ge p m = None <-> exists x, tree_eval (deps_get (bblock_deps p) x) m = None. -Proof. - intros; eapply tree_eval_None_correct. - intros; autorewrite with dict_rw; simpl; eauto. -Qed. - -Lemma tree_eval_inst_Some_correct2 i m0 old od: - (forall x, tree_eval (deps_get od x) m0 = Some (old x)) -> +Lemma inst_deps_Some_correct2 i m0 old od: + (forall x, deps_eval ge od x m0 = Some (old x)) -> forall (m1 m2: mem) d, - (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - (forall x, tree_eval (deps_get (inst_deps i d od) x) m0 = Some (m2 x)) -> - res_eq (Some m2) (inst_run ge i m1 old). + pre (inst_deps i d od) ge m0 -> + (forall x, deps_eval ge d x m0 = Some (m1 x)) -> + (forall x, deps_eval ge (inst_deps i d od) x m0 = Some (m2 x)) -> + res_eq (Some m2) (inst_run ge i m1 old). Proof. intro X. - induction i as [|[x e] i IHi]; simpl; intros m1 m2 d H0. + induction i as [|[x e] i IHi]; simpl; intros m1 m2 d VALID H0. - intros H; eapply ex_intro; intuition eauto. generalize (H0 x); rewrite H. congruence. - intros H. - remember (exp_eval ge e m1 old) as ov. - destruct ov. - + refine (IHi _ _ _ _ _); eauto. + destruct (exp_eval ge e m1 old) eqn: Heqov. + + refine (IHi _ _ _ _ _ _); eauto. intros x0; unfold assign; destruct (R.eq_dec x x0). - * subst; autorewrite with dict_rw. - destruct (failsafe (deps_get d x0)); simpl; try rewrite H0; + * subst. autorewrite with dict_rw. erewrite tree_eval_exp; eauto. * rewrite set_spec_diff; auto. + generalize (H x). - rewrite tree_eval_inst_abort; try discriminate. + rewrite inst_deps_abort; discriminate || auto. autorewrite with dict_rw. - destruct (failsafe (deps_get d x)); simpl; try rewrite H0; erewrite tree_eval_exp; eauto. Qed. -Lemma tree_eval_Some_correct2 p m0: forall (m1 m2: mem) d, - (forall x, tree_eval (deps_get d x) m0 = Some (m1 x)) -> - (forall x, tree_eval (deps_get (bblock_deps_rec p d) x) m0 = Some (m2 x)) -> +Lemma bblocks_deps_rec_Some_correct2 p m0: forall (m1 m2: mem) d, + pre (bblock_deps_rec p d) ge m0 -> + (forall x, deps_eval ge d x m0 = Some (m1 x)) -> + (forall x, deps_eval ge (bblock_deps_rec p d) x m0 = Some (m2 x)) -> res_eq (Some m2) (run ge p m1). Proof. - induction p as [|i p]; simpl; intros m1 m2 d H0. + induction p as [|i p]; simpl; intros m1 m2 d VALID H0. - intros H; eapply ex_intro; intuition eauto. generalize (H0 x); rewrite H. congruence. - intros H. - remember (inst_run ge i m1 m1) as om. - destruct om. - + refine (IHp _ _ _ _ _); eauto. - + assert (X: inst_run ge i m1 m1 = None); auto. - rewrite tree_eval_inst_None_correct in X; auto. + destruct (inst_run ge i m1 m1) eqn: Heqom. + + refine (IHp _ _ _ _ _ _); eauto. + + assert (X: exists x, tree_eval ge (deps_get (inst_deps i d d) x) m0 = None). + { eapply inst_deps_None_correct; eauto. } destruct X as [x H1]. generalize (H x). - rewrite tree_eval_abort; congruence. + erewrite block_deps_rec_abort; eauto. + congruence. Qed. + Lemma bblock_deps_Some_correct2 p m0 m1: - (forall x, tree_eval (deps_get (bblock_deps p) x) m0 = Some (m1 x)) + pre (bblock_deps p) ge m0 -> + (forall x, deps_eval ge (bblock_deps p) x m0 = Some (m1 x)) -> res_eq (Some m1) (run ge p m0). Proof. - intros; eapply tree_eval_Some_correct2; eauto. - intros; autorewrite with dict_rw; simpl; eauto. + intros; eapply bblocks_deps_rec_Some_correct2; eauto. +Qed. + +Lemma inst_valid i m0 old od: + (forall x, deps_eval ge od x m0 = Some (old x)) -> + forall (m1 m2: mem) (d: deps), + pre d ge m0 -> + inst_run ge i m1 old = Some m2 -> + (forall x, deps_eval ge d x m0 = Some (m1 x)) -> + pre (inst_deps i d od) ge m0. +Proof. + induction i as [|[x e] i IHi]; simpl; auto. + intros Hold m1 m2 d VALID0 H Hm1. + destruct (exp_eval ge e m1 old) eqn: Heq; simpl; try congruence. + eapply IHi; eauto. + + unfold deps_set in * |- *; simpl. + rewrite Hm1; intuition congruence. + + intros x0. unfold assign; destruct (R.eq_dec x x0). + * subst; autorewrite with dict_rw. + erewrite tree_eval_exp; eauto. + * rewrite set_spec_diff; auto. +Qed. + + +Lemma block_deps_rec_valid p m0: forall (m1 m2: mem) (d:deps), + pre d ge m0 -> + run ge p m1 = Some m2 -> + (forall x, deps_eval ge d x m0 = Some (m1 x)) -> + pre (bblock_deps_rec p d) ge m0. +Proof. + Local Hint Resolve inst_valid. + induction p as [ | i p]; simpl; intros m1 d H; auto. + intros H0 H1. + destruct (inst_run ge i m1 m1) eqn: Heqov; eauto. + congruence. Qed. +Lemma bblock_deps_valid p m0 m1: + run ge p m0 = Some m1 -> + pre (bblock_deps p) ge m0. +Proof. + intros; eapply block_deps_rec_valid; eauto. + unfold deps_empty; simpl. auto. +Qed. Theorem bblock_deps_simu p1 p2: - (forall x, deps_get (bblock_deps p1) x = deps_get (bblock_deps p2) x) - -> bblock_simu ge p1 p2. + (forall m, pre (bblock_deps p1) ge m -> pre (bblock_deps p2) ge m) -> + (forall m0 x m1, pre (bblock_deps p1) ge m0 -> deps_eval ge (bblock_deps p1) x m0 = Some m1 -> + deps_eval ge (bblock_deps p2) x m0 = Some m1) -> + bblock_simu ge p1 p2. Proof. - intros H m2 DONTFAIL. - remember (run ge p1 m2) as om1. - destruct om1; simpl. - + apply bblock_deps_Some_correct2. - intros; rewrite <- H. - apply bblock_deps_Some_correct1; auto. - + rewrite bblock_deps_None_correct. - assert (X: run ge p1 m2 = None); auto. - rewrite bblock_deps_None_correct in X. - destruct X as [x Hx]. - rewrite H in Hx. - eauto. + Local Hint Resolve bblock_deps_valid bblock_deps_Some_correct1. + intros INCL EQUIV m DONTFAIL. + destruct (run ge p1 m) as [m1|] eqn: RUN1; simpl; try congruence. + eapply bblock_deps_Some_correct2; eauto. Qed. End DEPTREE. diff --git a/mppa_k1c/abstractbb/ImpDep.v b/mppa_k1c/abstractbb/ImpDep.v index 2e2ad40f..3efe6a36 100644 --- a/mppa_k1c/abstractbb/ImpDep.v +++ b/mppa_k1c/abstractbb/ImpDep.v @@ -72,8 +72,6 @@ Hypothesis hC_tree_correct: forall t, WHEN hC_tree t ~> t' THEN pre_data t=data 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'. -Variable ge: genv. - (* First, we wrap constructors for hashed values !*) Local Open Scope positive. @@ -107,19 +105,6 @@ Qed. Global Opaque hTop. Hint Resolve hTop_correct: wlp. -Definition hTerase (t1 t2: hashV tree) (debug: option pstring): ?? hashV tree := - DO hc <~ hash 3;; - hC_tree {| pre_data:=Terase (data t1) (data t2); - hcodes:=[hc;hid t1; hid t2]; debug_info := debug |}. - -Lemma hTerase_correct t1 t2 dbg: - WHEN hTerase t1 t2 dbg ~> t THEN (data t)=(Terase (data t1) (data t2)). -Proof. - wlp_simplify. -Qed. -Global Opaque hTerase. -Hint Resolve hTerase_correct: wlp. - Definition hTnil (_: unit): ?? hashV list_tree := hC_list_tree {| pre_data:=Tnil; hcodes := nil; debug_info := None |} . @@ -146,7 +131,9 @@ Hint Resolve hTcons_correct: wlp. (* Second, we use these hashed constructors ! *) -Definition hdeps:= Dict.t (hashV tree). +Record hdeps:= {hpre: list (hashV tree); hpost: Dict.t (hashV tree)}. + +Coercion hpost: hdeps >-> Dict.t. (* pseudo deps_get *) Definition pdeps_get (d:hdeps) x : tree := @@ -169,6 +156,12 @@ 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 <-> pre d ge m) + /\ (forall m x, tree_eval ge (pdeps_get hd x) m = deps_eval ge d x m). + Fixpoint hexp_tree (e: exp) (d od: hdeps) (dbg: option pstring) : ?? hashV tree := match e with | PReg x => hdeps_get d x dbg @@ -187,86 +180,95 @@ with hlist_exp_tree (le: list_exp) (d od: hdeps): ?? hashV list_tree := | LOld le => hlist_exp_tree le od od end. -Lemma hexp_tree_correct_x e od1 od2: - (forall x, pdeps_get od1 x = deps_get od2 x) -> - forall d1 d2 dbg, - (forall x, pdeps_get d1 x = deps_get d2 x) -> - WHEN hexp_tree e d1 od1 dbg ~> t THEN data t = exp_tree e d2 od2. +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, 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 d1 d2, - (forall x, pdeps_get d1 x = deps_get d2 x) -> - WHEN hlist_exp_tree le d1 od1 ~> lt THEN data lt = list_exp_tree le d2 od2); simpl; wlp_simplify; congruence. + 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, 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; try congruence. + - rewrite H4, <- H0; simpl; reflexivity. + - rewrite H1; simpl; reflexivity. + - rewrite H5, <- H0, <- H4; simpl; reflexivity. Qed. Global Opaque hexp_tree. -Lemma hexp_tree_correct e d1 od1 dbg: - WHEN hexp_tree e d1 od1 dbg ~> t THEN forall od2 d2, (forall x, pdeps_get od1 x = deps_get od2 x) -> (forall x, pdeps_get d1 x = deps_get d2 x) -> data t = exp_tree e d2 od2. +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 -> tree_eval ge (data t) m = tree_eval ge (exp_tree e d od) m. Proof. - intros t H od2 d2 H1 H2; apply (hexp_tree_correct_x e od1 od2 H1 d1 d2 dbg H2 t H). + unfold wlp; intros; eapply hexp_tree_correct_x; eauto. Qed. Hint Resolve hexp_tree_correct: wlp. -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 t0 <~ hdeps_get d x None;; - DO v' <~ (if failsafe (data t0) - then - hexp_tree e d od dbg - else - DO t1 <~ hexp_tree e d od None;; - hTerase t1 t0 dbg);; - hinst_deps i' (Dict.set d x v') od +Definition failsafe (t: tree): bool := + match t with + | Tname x => true + | Top o Tnil => is_constant o + | _ => false end. -Lemma pset_spec_eq d x t: - pdeps_get (Dict.set d x t) x = (data t). -Proof. - unfold pdeps_get; rewrite Dict.set_spec_eq; simpl; auto. -Qed. +Local Hint Resolve is_constant_correct. -Lemma pset_spec_diff d x y t: - x <> y -> pdeps_get (Dict.set d x t) y = pdeps_get d y. +Lemma failsafe_correct ge (t: tree) m: failsafe t = true -> tree_eval ge t m <> None. Proof. - unfold pdeps_get; intros; rewrite Dict.set_spec_diff; simpl; auto. + destruct t; simpl; try congruence. + destruct l; simpl; try congruence. + eauto. Qed. - -Lemma pempty_spec x: pdeps_get Dict.empty x = Tname x. +Local Hint Resolve failsafe_correct. + +Definition hdeps_set (d:hdeps) x (t:hashV tree) := + DO ot <~ hdeps_get d x None;; + RET {| hpre:=if failsafe (data ot) then d.(hpre) else ot::d.(hpre); + hpost:=Dict.set d 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, tree_eval ge (data ht) m = tree_eval ge t m) -> (* TODO: condition à revoir, on peut sans doute relâcher ici ! *) + deps_model ge (deps_set d x t) nhd. Proof. - unfold pdeps_get; rewrite Dict.empty_spec; simpl; auto. + intros; wlp_simplify. + unfold deps_model, deps_set; simpl. destruct H0 as (DM0 & DM1); split. + - intros m; unfold hdeps_valid in DM0 |- *; simpl. + generalize (failsafe_correct ge (data exta) m); intros FAILSAFE. + destruct (DM0 m) as (H2 & H3); clear DM0. unfold deps_eval in * |- *. + destruct (failsafe _); simpl. + * rewrite !H, !DM1 in * |- *; intuition (subst; eauto). + * clear FAILSAFE. rewrite <- DM1, <- H. intuition (subst; eauto). + - clear H DM0. unfold deps_eval, pdeps_get, deps_get in * |- *; simpl. + intros; case (R.eq_dec x x0). + + intros; subst; rewrite !Dict.set_spec_eq; simpl; auto. + + intros; rewrite !Dict.set_spec_diff; simpl; auto. Qed. +Local Hint Resolve hdeps_set_correct: wlp. +Global Opaque hdeps_set. -Hint Rewrite pset_spec_eq pempty_spec: dict_rw. +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 d1 od1, - WHEN hinst_deps i d1 od1 ~> d1' THEN - forall od2 d2, (forall x, pdeps_get od1 x = deps_get od2 x) -> - (forall x, pdeps_get d1 x = deps_get d2 x) -> - forall x, pdeps_get d1' x = deps_get (inst_deps i d2 od2) x. +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 -> deps_model ge (inst_deps i d od) hd'. Proof. induction i; simpl; wlp_simplify. - + cutrewrite (failsafe (deps_get d2 a0) = failsafe (data exta0)). - - erewrite H0, H2; simpl; eauto. clear exta2 Hexta2 H2; auto. - intros x0; destruct (R.eq_dec a0 x0). - * subst. autorewrite with dict_rw. rewrite set_spec_eq. erewrite H1; eauto. - * rewrite set_spec_diff, pset_spec_diff; auto. - - rewrite H, H4; auto. - + cutrewrite (failsafe (deps_get d2 a0) = failsafe (data exta0)). - - erewrite H0, H3; simpl; eauto. clear exta3 Hexta3 H3; auto. - intros x0; destruct (R.eq_dec a0 x0). - * subst; autorewrite with dict_rw. rewrite H2. - erewrite H, H1; eauto. rewrite set_spec_eq. congruence. - * rewrite set_spec_diff, pset_spec_diff; auto. - - rewrite H, H5; auto. Qed. Global Opaque hinst_deps. -Hint Resolve hinst_deps_correct: wlp. +Local Hint Resolve hinst_deps_correct: wlp. (* logging info: we log the number of inst-instructions passed ! *) Variable log: unit -> ?? unit. @@ -280,24 +282,24 @@ Fixpoint hbblock_deps_rec (p: bblock) (d: hdeps): ?? hdeps := hbblock_deps_rec p' d' end. -Lemma hbblock_deps_rec_correct p: forall d1, - WHEN hbblock_deps_rec p d1 ~> d1' THEN - forall d2, (forall x, pdeps_get d1 x = deps_get d2 x) -> forall x, pdeps_get d1' x = deps_get (bblock_deps_rec p d2) x. +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. -Hint Resolve hbblock_deps_rec_correct: wlp. +Local Hint Resolve hbblock_deps_rec_correct: wlp. Definition hbblock_deps: bblock -> ?? hdeps - := fun p => hbblock_deps_rec p Dict.empty. + := fun p => hbblock_deps_rec p {| hpre:= nil ; hpost := Dict.empty |}. Lemma hbblock_deps_correct p: - WHEN hbblock_deps p ~> d1 THEN forall x, pdeps_get d1 x = deps_get (bblock_deps p) x. + WHEN hbblock_deps p ~> hd THEN forall ge, deps_model ge (bblock_deps p) hd. Proof. - unfold bblock_deps; wlp_simplify. erewrite H; eauto. - intros; autorewrite with dict_rw; auto. rewrite empty_spec. reflexivity. + unfold bblock_deps; wlp_simplify. eapply H. clear H. + unfold deps_model, pdeps_get, hdeps_valid, deps_eval, deps_get; simpl. + intuition; rewrite !Dict.empty_spec; simpl; auto. Qed. Global Opaque hbblock_deps. @@ -324,11 +326,6 @@ Definition tree_hash_eq (ta tb: tree): ?? bool := DO b <~ op_eq oa ob ;; if b then phys_eq lta ltb else RET false - | Terase t1a t2a, Terase t1b t2b => - DO b <~ phys_eq t1a t1b ;; - if b - then phys_eq t2a t2b - else RET false | _,_ => RET false end. @@ -358,7 +355,7 @@ Qed. Global Opaque list_tree_hash_eq. Hint Resolve list_tree_hash_eq_correct: wlp. -Lemma pdeps_get_intro d1 d2: +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. @@ -366,6 +363,19 @@ 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 !!! ***) @@ -376,7 +386,6 @@ 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. @@ -385,34 +394,48 @@ 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 RET true - else ( + 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, _ => - print_error s;; - RET false + 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 [X1 X2], hco_list_correct as [Y1 Y2]. + 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; rewrite <- H, <- H0. - apply pdeps_get_intro. auto. + + intros m; rewrite <- EQPRE1, <- EQPRE2. + unfold incl, hdeps_valid in * |- *; intuition eauto. + + intros m0 x m1 VALID; rewrite <- EQPOST1, <- EQPOST2. + erewrite pdeps_get_intro; auto. auto. 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 exta; simpl in * |- *; auto. + destruct exta0; simpl in * |- *; auto. Qed. Global Opaque g_bblock_simu_test. @@ -429,6 +452,7 @@ 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). @@ -437,17 +461,30 @@ 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) p1 p2. -Obligation 1. + 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. +Obligation 2. generalize (hCons_correct _ _ _ _ H); clear H. constructor 1; wlp_simplify. Qed. @@ -486,10 +523,6 @@ Definition print_raw_htree (td: pre_hashV tree): ?? unit := DO so <~ string_of_op o;; DO sl <~ string_of_hashcode lid;; println (so +; " " +; (list_id sl)) - | (Terase _ _), [ _ ; t1; t2 ] => - DO st1 <~ string_of_hashcode t1 ;; - DO st2 <~ string_of_hashcode t2 ;; - println((tree_id st1) +; " erases " +; (tree_id st2)) | _, _ => FAILWITH "unexpected hcodes" end. @@ -521,9 +554,6 @@ Fixpoint string_of_tree (t: tree) (pt: pre_hashV tree) : ?? pstring := DO pl <~ get_hlist lid;; DO sl <~ string_of_list_tree l pl;; RET (so +; "(" +; sl +; ")") - | Terase t _, [ _ ; tid; _ ] => - DO pt <~ get_htree tid ;; - string_of_tree t pt | _, _ => FAILWITH "unexpected hcodes" end end @@ -699,11 +729,13 @@ Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool := (log_debug log1) simple_debug (hlog log1 hco_tree hco_list) - (log_insert log2) - 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) + (print_error1 hco_tree hco_list cr log2) + true + failpreserv_error (* TODO: debug info *) p1 p2;; if result1 then RET true @@ -718,10 +750,12 @@ Program Definition verb_bblock_simu_test (p1 p2: bblock): ?? bool := simple_debug (hlog log1 hco_tree hco_list) (log_insert log2) - hco_tree _ - hco_list _ + hco_tree _ + hco_list _ (print_error_end2 hco_tree hco_list) - (print_error2 hco_tree hco_list cr log2) + (print_error2 hco_tree hco_list cr log2) + false + (fun _ => RET tt) p2 p1;; if result2 then ( @@ -796,7 +830,7 @@ Proof. Qed. Global Opaque eq_test. -(* get some key of a non-empty d *) +(* 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" @@ -809,7 +843,7 @@ Fixpoint pick {A} (d: t A): ?? R.t := 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 diff --git a/mppa_k1c/abstractbb/Impure/ImpCore.v b/mppa_k1c/abstractbb/Impure/ImpCore.v index 55e67608..7925f62d 100644 --- a/mppa_k1c/abstractbb/Impure/ImpCore.v +++ b/mppa_k1c/abstractbb/Impure/ImpCore.v @@ -132,6 +132,13 @@ Proof. destruct x; simpl; auto. Qed. +Lemma wlp_option (A B: Type) (x: option A) (k1: A -> ??B) (k2: ??B) (P: B -> Prop): + (forall a, x=Some a -> wlp (k1 a) P) -> + (x=None -> wlp k2 P) -> + (wlp (match x with Some a => k1 a | None => k2 end) P). +Proof. + destruct x; simpl; auto. +Qed. (* Tactics @@ -156,6 +163,7 @@ Ltac wlp_decompose := || apply wlp_letprod || apply wlp_sum || apply wlp_sumbool + || apply wlp_option . (* this tactic simplifies the current "wlp" goal using any hint found via tactic "hint". *) @@ -185,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 307eb163..dd615628 100644 --- a/mppa_k1c/abstractbb/Impure/ImpHCons.v +++ b/mppa_k1c/abstractbb/Impure/ImpHCons.v @@ -3,8 +3,6 @@ Require Export ImpIO. Import Notations. Local Open Scope impure. -(********************************) -(* (Weak) HConsing *) Axiom string_of_hashcode: hashcode -> ?? caml_string. Extract Constant string_of_hashcode => "string_of_int". @@ -12,6 +10,99 @@ Extract Constant string_of_hashcode => "string_of_int". Axiom hash: forall {A}, A -> ?? hashcode. Extract Constant hash => "Hashtbl.hash". +(**************************) +(* (Weak) Sets *) + + +Import Dict. + +Axiom make_dict: forall {A B}, (hash_params A) -> ?? Dict.t A B. +Extract Constant make_dict => "ImpHConsOracles.make_dict". + + +Module Sets. + +Definition t {A} (mod: A -> Prop) := Dict.t A {x | mod x}. + +Definition empty {A} (hp: hash_params A) {mod:A -> Prop}: ?? t mod := + make_dict hp. + +Program Fixpoint add {A} (l: list A) {mod: A -> Prop} (d: t mod): forall {H:forall x, List.In x l -> mod x}, ?? unit := + match l with + | nil => fun H => RET () + | x::l' => fun H => + d.(set)(x,x);; + add l' d + end. + +Program Definition create {A} (hp: hash_params A) (l:list A): ?? t (fun x => List.In x l) := + DO d <~ empty hp (mod:=fun x => List.In x l);; + add l (mod:=fun x => List.In x l) d (H:=_);; + RET d. +Global Opaque create. + +Definition is_present {A} (hp: hash_params A) (x:A) {mod} (d:t mod): ?? bool := + DO oy <~ (d.(get)) x;; + match oy with + | Some y => hp.(test_eq) x (`y) + | None => RET false + end. + +Local Hint Resolve test_eq_correct: wlp. + +Lemma is_present_correct A (hp: hash_params A) x mod (d:t mod): + WHEN is_present hp x d ~> b THEN b=true -> mod x. +Proof. + wlp_simplify; subst; eauto. + - apply proj2_sig. + - discriminate. +Qed. +Hint Resolve is_present_correct: wlp. +Global Opaque is_present. + +Definition msg_assert_incl: pstring := "Sets.assert_incl". + +Fixpoint assert_incl {A} (hp: hash_params A) (l: list A) {mod} (d:t mod): ?? unit := + match l with + | nil => RET () + | x::l' => + DO b <~ is_present hp x d;; + if b then + assert_incl hp l' d + else ( + hp.(log) x;; + FAILWITH msg_assert_incl + ) + end. + +Lemma assert_incl_correct A (hp: hash_params A) l mod (d:t mod): + WHEN assert_incl hp l d ~> _ THEN forall x, List.In x l -> mod x. +Proof. + induction l; wlp_simplify; subst; eauto. +Qed. +Hint Resolve assert_incl_correct: wlp. +Global Opaque assert_incl. + +Definition assert_list_incl {A} (hp: hash_params A) (l1 l2: list A): ?? unit := + (* println "";;print("dict_create ");;*) + DO d <~ create hp l2;; + (*print("assert_incl ");;*) + assert_incl hp l1 d. + +Lemma assert_list_incl_correct A (hp: hash_params A) l1 l2: + WHEN assert_list_incl hp l1 l2 ~> _ THEN List.incl l1 l2. +Proof. + wlp_simplify. +Qed. +Global Opaque assert_list_incl. +Hint Resolve assert_list_incl_correct. + +End Sets. + +(********************************) +(* (Weak) HConsing *) + + Axiom xhCons: forall {A}, ((A -> A -> ?? bool) * (pre_hashV A -> ?? hashV A)) -> ?? hashConsing A. Extract Constant xhCons => "ImpHConsOracles.xhCons". diff --git a/mppa_k1c/abstractbb/Impure/ImpPrelude.v b/mppa_k1c/abstractbb/Impure/ImpPrelude.v index 0efa042c..1a84eb3b 100644 --- a/mppa_k1c/abstractbb/Impure/ImpPrelude.v +++ b/mppa_k1c/abstractbb/Impure/ImpPrelude.v @@ -91,11 +91,37 @@ Extract Inlined Constant struct_eq => "(=)". Hint Resolve struct_eq_correct: wlp. -(** Data-structure for generic hash-consing *) +(** Data-structure for generic hash-consing, hash-set *) Axiom hashcode: Type. Extract Constant hashcode => "int". +Module Dict. + +Record hash_params {A:Type} := { + test_eq: A -> A -> ??bool; + test_eq_correct: forall x y, WHEN test_eq x y ~> r THEN r=true -> x=y; + hashing: A -> ??hashcode; + log: A -> ??unit (* for debugging only *) +}. +Arguments hash_params: clear implicits. + + +Record t {A B:Type} := { + set: A * B -> ?? unit; + get: A -> ?? option B +}. +Arguments t: clear implicits. + +End Dict. + + +(* 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; hcodes: list hashcode; @@ -116,6 +142,7 @@ Record hashExport {A:Type}:= { 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 ****) diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml index c421ff87..b7a80679 100644 --- a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml +++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.ml @@ -1,7 +1,21 @@ open ImpPrelude exception Stop;; - + +let make_dict (type key) (p: key Dict.hash_params) = + let module MyHashedType = struct + type t = key + let equal = p.Dict.test_eq + let hash = p.Dict.hashing + end in + let module MyHashtbl = Hashtbl.Make(MyHashedType) in + let dict = MyHashtbl.create 1000 in + { + Dict.set = (fun (k,d) -> MyHashtbl.replace dict k d); + Dict.get = (fun k -> MyHashtbl.find_opt dict k) + } + + let xhCons (type a) (hash_eq, error: (a -> a -> bool)*(a pre_hashV -> a hashV)) = let module MyHashedType = struct type t = a pre_hashV diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli index e81681df..a74c721a 100644 --- a/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli +++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpHConsOracles.mli @@ -1,3 +1,4 @@ open ImpPrelude +val make_dict : 'a1 Dict.hash_params -> ('a1, 'a2) Dict.t val xhCons: (('a -> 'a -> bool) * ('a pre_hashV -> 'a hashV)) -> 'a hashConsing |