diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-07 22:32:13 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-05-07 22:32:13 +0200 |
commit | 0b99415251e56c64adb5caeec8f7c9c4f77ac926 (patch) | |
tree | cfed8d56e859c4b1ebd51cecd0a257f9d4361704 /mppa_k1c/abstractbb | |
parent | e1ae915f648df0137d0f183f3b992583528184a7 (diff) | |
download | compcert-kvx-0b99415251e56c64adb5caeec8f7c9c4f77ac926.tar.gz compcert-kvx-0b99415251e56c64adb5caeec8f7c9c4f77ac926.zip |
generalize bblock_equiv into bblock_simu (abstract_bb)
Diffstat (limited to 'mppa_k1c/abstractbb')
-rw-r--r-- | mppa_k1c/abstractbb/AbstractBasicBlocksDef.v | 22 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/DepTreeTheory.v | 6 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/ImpDep.v | 42 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml | 15 | ||||
-rw-r--r-- | mppa_k1c/abstractbb/Parallelizability.v | 8 |
5 files changed, 42 insertions, 51 deletions
diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v index d1950209..618f3ebe 100644 --- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v +++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v @@ -140,9 +140,9 @@ Proof. Qed. -(** A small theory of bblockram equality *) +(** A small theory of bblock equality *) -(* equalities on bblockram outputs *) +(* equalities on bblock outputs *) Definition res_eq (om1 om2: option mem): Prop := match om1 with | Some m1 => exists m2, om2 = Some m2 /\ forall x, m1 x = m2 x @@ -163,10 +163,10 @@ Proof. - intros; erewrite IHe, IHe0; auto. Qed. -Definition bblock_equiv (p1 p2: bblock): Prop - := forall m, res_eq (run p1 m) (run p2 m). +Definition bblock_simu (p1 p2: bblock): Prop + := forall m, (run p1 m) <> None -> res_eq (run p1 m) (run p2 m). -Lemma alt_inst_equiv_refl i old1 old2: +Lemma inst_equiv_refl i old1 old2: (forall x, old1 x = old2 x) -> forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (inst_run i m1 old1) (inst_run i m2 old2). @@ -178,10 +178,10 @@ Proof. unfold assign; intro y. destruct (R.eq_dec x y); auto. Qed. -Lemma alt_bblock_equiv_refl p: forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (run p m1) (run p m2). +Lemma bblock_equiv_refl p: forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (run p m1) (run p m2). Proof. induction p as [ | i p']; simpl; eauto. - intros m1 m2 H; lapply (alt_inst_equiv_refl i m1 m2); auto. + intros m1 m2 H; lapply (inst_equiv_refl i m1 m2); auto. intros X; lapply (X m1 m2); auto; clear X. destruct (inst_run i m1 m1); simpl. - intros [m3 [H1 H2]]; rewrite H1; simpl; auto. @@ -205,11 +205,11 @@ Proof. - intro; subst; simpl; auto. Qed. -Lemma bblock_equiv_alt p1 p2: bblock_equiv p1 p2 <-> (forall m1 m2, (forall x, m1 x = m2 x) -> res_eq (run p1 m1) (run p2 m2)). +Lemma bblock_simu_alt p1 p2: bblock_simu p1 p2 <-> (forall m1 m2, (forall x, m1 x = m2 x) -> (run p1 m1)<>None -> res_eq (run p1 m1) (run p2 m2)). Proof. - unfold bblock_equiv; intuition. - intros; eapply res_eq_trans. eapply alt_bblock_equiv_refl; eauto. - eauto. + unfold bblock_simu; intuition. + intros; eapply res_eq_trans. eauto. + eapply bblock_equiv_refl; eauto. Qed. diff --git a/mppa_k1c/abstractbb/DepTreeTheory.v b/mppa_k1c/abstractbb/DepTreeTheory.v index bfe79d42..bf45d11a 100644 --- a/mppa_k1c/abstractbb/DepTreeTheory.v +++ b/mppa_k1c/abstractbb/DepTreeTheory.v @@ -352,11 +352,11 @@ Proof. Qed. -Theorem bblock_deps_equiv p1 p2: +Theorem bblock_deps_simu p1 p2: (forall x, deps_get (bblock_deps p1) x = deps_get (bblock_deps p2) x) - -> bblock_equiv ge p1 p2. + -> bblock_simu ge p1 p2. Proof. - intros H m2. + intros H m2 DONTFAIL. remember (run ge p1 m2) as om1. destruct om1; simpl. + apply bblock_deps_Some_correct2. diff --git a/mppa_k1c/abstractbb/ImpDep.v b/mppa_k1c/abstractbb/ImpDep.v index a4dd12eb..2e2ad40f 100644 --- a/mppa_k1c/abstractbb/ImpDep.v +++ b/mppa_k1c/abstractbb/ImpDep.v @@ -385,7 +385,7 @@ Hypothesis hco_list_correct: hCons_spec hco_list. Variable print_error_end: hdeps -> hdeps -> ?? unit. Variable print_error: pstring -> ?? unit. -Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool := +Program Definition g_bblock_simu_test (p1 p2: bblock): ?? bool := 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 ;; @@ -398,23 +398,23 @@ Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool := CATCH_FAIL s, _ => print_error s;; RET false - ENSURE (fun b => b=true -> forall ge, bblock_equiv ge p1 p2));; + 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]. constructor 1; wlp_simplify; try congruence. - apply bblock_deps_equiv; auto. + apply bblock_deps_simu; auto. intros; rewrite <- H, <- H0. apply pdeps_get_intro. auto. Qed. -Theorem g_bblock_eq_test_correct p1 p2: - WHEN g_bblock_eq_test p1 p2 ~> b THEN b=true -> forall ge, bblock_equiv ge p1 p2. +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. Qed. -Global Opaque g_bblock_eq_test. +Global Opaque g_bblock_simu_test. End Prog_Eq_Gen. @@ -424,7 +424,7 @@ Definition skip (_:unit): ?? unit := RET tt. Definition no_dbg (_:R.t): ?? option pstring := RET None. -Definition msg_prefix: pstring := "*** ERROR INFO from bblock_eq_test: ". +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". @@ -438,11 +438,11 @@ Definition print_error (log: logger unit) (s:pstring): ?? unit println (msg_prefix +; msg_number +; n +; " -- " +; s). -Program Definition bblock_eq_test (p1 p2: bblock): ?? bool := +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_eq_test no_dbg no_dbg skip (log_insert log) hco_tree _ hco_list _ print_error_end (print_error log) p1 p2. + 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. generalize (hCons_correct _ _ _ _ H0); clear H0. constructor 1; wlp_simplify. @@ -452,18 +452,18 @@ Obligation 2. constructor 1; wlp_simplify. Qed. -Local Hint Resolve g_bblock_eq_test_correct. +Local Hint Resolve g_bblock_simu_test_correct. -Theorem bblock_eq_test_correct p1 p2: - WHEN bblock_eq_test p1 p2 ~> b THEN b=true -> forall ge, bblock_equiv ge p1 p2. +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_eq_test. +Global Opaque bblock_simu_test. -(** This is only to print info on each bblock_eq_test run **) +(** This is only to print info on each bblock_simu_test run **) Section Verbose_version. Variable string_of_name: R.t -> ?? pstring. @@ -689,13 +689,13 @@ Definition hlog (log: logger unit) (hct: hashConsing tree) (hcl: hashConsing lis next_log hcl s ). -Program Definition verb_bblock_eq_test (p1 p2: bblock): ?? bool := +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_eq_test + DO result1 <~ g_bblock_simu_test (log_debug log1) simple_debug (hlog log1 hco_tree hco_list) @@ -713,7 +713,7 @@ Program Definition verb_bblock_eq_test (p1 p2: bblock): ?? bool := 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_eq_test + DO result2 <~ g_bblock_simu_test (log_debug log1) simple_debug (hlog log1 hco_tree hco_list) @@ -725,7 +725,7 @@ Program Definition verb_bblock_eq_test (p1 p2: bblock): ?? bool := p2 p1;; if result2 then ( - println (msg_prefix +; " OOops - symmetry violation in bblock_eq_test => this is a bug of bblock_eq_test ??");; + println (msg_prefix +; " OOops - symmetry violation in bblock_simu_test => this is a bug of bblock_simu_test ??");; RET false ) else RET false . @@ -746,12 +746,12 @@ Obligation 4. constructor 1; wlp_simplify. Qed. -Theorem verb_bblock_eq_test_correct p1 p2: - WHEN verb_bblock_eq_test p1 p2 ~> b THEN b=true -> forall ge, bblock_equiv ge p1 p2. +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_eq_test. +Global Opaque verb_bblock_simu_test. End Verbose_version. diff --git a/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml b/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml index 0e5cf434..33c3c842 100644 --- a/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml +++ b/mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml @@ -53,14 +53,6 @@ let memo_int2pos: int -> int -> BinNums.positive Hashtbl.add t i pi; pi in find;; - -(* -let string_coq2caml: char list -> string - = fun l -> - let buf = Buffer.create (List.length l) in - List.iter (fun c -> Buffer.add_char buf c) l; - Buffer.contents buf;; -*) let new_exit_observer: (unit -> unit) -> (unit -> unit) ref = fun f -> @@ -123,8 +115,8 @@ let zTr: BinNums.coq_Z -> int let ten = BinNums.Zpos (BinNums.Coq_xO (BinNums.Coq_xI (BinNums.Coq_xO BinNums.Coq_xH))) let rec string_of_pos (p:BinNums.positive) (acc: pstring): pstring -= let (q,r) = BinInt.Z.pos_div_eucl p ten in - let acc0 = Concat (CamlStr (string_of_int (zTr r)), acc) in += let (q,r) = BinInt.Z.pos_div_eucl p ten in + let acc0 = Concat (CamlStr (string_of_int (zTr r)), acc) in match q with | BinNums.Z0 -> acc0 | BinNums.Zpos p0 -> string_of_pos p0 acc0 @@ -134,7 +126,7 @@ let rec string_of_pos (p:BinNums.positive) (acc: pstring): pstring let string_of_Z_debug: BinNums.coq_Z -> pstring = fun p -> CamlStr (string_of_int (zTr p)) *) - + let string_of_Z: BinNums.coq_Z -> pstring = function | BinNums.Z0 -> CamlStr "0" @@ -148,4 +140,3 @@ let timer ((f:'a -> 'b), (x:'a)) : 'b = let rt = (Unix.times()).Unix.tms_utime -. itime in Printf.printf "time = %f\n" rt; r - diff --git a/mppa_k1c/abstractbb/Parallelizability.v b/mppa_k1c/abstractbb/Parallelizability.v index eae7b672..d1971e57 100644 --- a/mppa_k1c/abstractbb/Parallelizability.v +++ b/mppa_k1c/abstractbb/Parallelizability.v @@ -91,18 +91,18 @@ Proof. intros; destruct (inst_prun _ _ _); simpl; auto. Qed. -Lemma prun_iw_app_None p1 m1 old p2: +Lemma prun_iw_app_None p1: forall m1 old p2, prun_iw p1 m1 old = None -> prun_iw (p1++p2) m1 old = None. Proof. - intros H; rewrite prun_iw_app. rewrite H; auto. + intros m1 old p2 H; rewrite prun_iw_app. rewrite H; auto. Qed. -Lemma prun_iw_app_Some p1 m1 old m2 p2: +Lemma prun_iw_app_Some p1: forall m1 old m2 p2, prun_iw p1 m1 old = Some m2 -> prun_iw (p1++p2) m1 old = prun_iw p2 m2 old. Proof. - intros H; rewrite prun_iw_app. rewrite H; auto. + intros m1 old m2 p2 H; rewrite prun_iw_app. rewrite H; auto. Qed. End PARALLEL. |