diff options
Diffstat (limited to 'mppa_k1c/abstractbb/ImpDep.v')
| -rw-r--r-- | mppa_k1c/abstractbb/ImpDep.v | 960 |
1 files changed, 0 insertions, 960 deletions
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. - |