From 0b99415251e56c64adb5caeec8f7c9c4f77ac926 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 7 May 2019 22:32:13 +0200 Subject: generalize bblock_equiv into bblock_simu (abstract_bb) --- mppa_k1c/Asmblockdeps.v | 39 ++++++++++------------ mppa_k1c/abstractbb/AbstractBasicBlocksDef.v | 22 ++++++------- mppa_k1c/abstractbb/DepTreeTheory.v | 6 ++-- mppa_k1c/abstractbb/ImpDep.v | 42 ++++++++++++------------ mppa_k1c/abstractbb/Impure/ocaml/ImpIOOracles.ml | 15 ++------- mppa_k1c/abstractbb/Parallelizability.v | 8 ++--- 6 files changed, 59 insertions(+), 73 deletions(-) diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index c6207627..eb3900d5 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -1300,7 +1300,7 @@ Local Hint Resolve trans_state_match. Lemma bblock_simu_reduce: forall p1 p2 ge fn, Ge = Genv ge fn -> - L.bblock_equiv Ge (trans_block p1) (trans_block p2) -> + L.bblock_simu Ge (trans_block p1) (trans_block p2) -> Asmblockgenproof0.bblock_simu ge fn p1 p2. Proof. unfold bblock_simu, res_eq; intros p1 p2 ge fn H1 H2 rs m DONTSTUCK. @@ -1308,21 +1308,16 @@ Proof. intro H2. exploit (forward_simu Ge rs m p1 ge fn (trans_state (State rs m))); eauto. exploit (forward_simu Ge rs m p2 ge fn (trans_state (State rs m))); eauto. - remember (exec_bblock ge fn p1 rs m) as exp1. - destruct exp1. - + (* Next *) - intros H3 (s2' & exp2 & MS'). unfold exec in exp2, H3. rewrite exp2 in H2. - destruct H2 as (m2' & H2 & H4). rewrite H2 in H3. - destruct (exec_bblock ge fn p2 rs m); simpl in H3. - * destruct H3 as (s' & H3 & H5 & H6). inv H3. inv MS'. - cutrewrite (rs0=rs1). - - cutrewrite (m0=m1); auto. congruence. - - apply functional_extensionality. intros r. - generalize (H0 r). intros Hr. congruence. - * discriminate. - + intros MO MO2. remember (trans_state (State rs m)) as s1. inversion MO2. clear MO2. unfold exec in *. - rewrite H0 in H2. clear H0. destruct (exec_bblock ge fn p2 rs m); auto. rewrite H2 in MO. unfold match_outcome in MO. - destruct MO as (? & ? & ?). discriminate. + destruct (exec_bblock ge fn p1 rs m); try congruence. + intros H3 (s2' & exp2 & MS'). unfold exec in exp2, H3. rewrite exp2 in H2. + destruct H2 as (m2' & H2 & H4). discriminate. rewrite H2 in H3. + destruct (exec_bblock ge fn p2 rs m); simpl in H3. + * destruct H3 as (s' & H3 & H5 & H6). inv H3. inv MS'. + cutrewrite (rs0=rs1). + - cutrewrite (m0=m1); auto. congruence. + - apply functional_extensionality. intros r. + generalize (H0 r). intros Hr. congruence. + * discriminate. Qed. Definition gpreg_name (gpr: gpreg) := @@ -1600,11 +1595,11 @@ Definition string_of_op (op: P.op): ?? pstring := Definition bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool := if verb then - IDT.verb_bblock_eq_test string_of_name string_of_op (trans_block p1) (trans_block p2) + IDT.verb_bblock_simu_test string_of_name string_of_op (trans_block p1) (trans_block p2) else - IDT.bblock_eq_test (trans_block p1) (trans_block p2). + IDT.bblock_simu_test (trans_block p1) (trans_block p2). -Local Hint Resolve IDT.bblock_eq_test_correct bblock_simu_reduce IDT.verb_bblock_eq_test_correct: wlp. +Local Hint Resolve IDT.bblock_simu_test_correct bblock_simu_reduce IDT.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. @@ -1613,13 +1608,13 @@ Proof. Qed. Hint Resolve bblock_simu_test_correct: wlp. -(* Coerce bblock_eq_test into a pure function (this is a little unsafe like all oracles in CompCert). *) +(* Coerce bblock_simu_test into a pure function (this is a little unsafe like all oracles in CompCert). *) 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 -> bblock_simu ge fn 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. Proof. intros; unfold pure_bblock_simu_test. intros; eapply bblock_simu_test_correct; eauto. apply unsafe_coerce_not_really_correct; eauto. @@ -1627,7 +1622,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 -> bblock_simu ge fn p1 p2. +Lemma bblock_simub_correct p1 p2 ge fn: Ge = Genv ge fn -> bblock_simub p1 p2 = true -> Asmblockgenproof0.bblock_simu ge fn p1 p2. Proof. eapply (pure_bblock_simu_test_correct true). Qed. 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. -- cgit