From 9833210392b7bddf740e6b555ce931efb46cf387 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 5 Mar 2019 11:02:51 +0100 Subject: remove cumbersome dependency on genv in bblock_eq_test --- mppa_k1c/abstractbb/AbstractBasicBlocksDef.v | 5 ++++ mppa_k1c/abstractbb/DepTreeTheory.v | 10 +++---- mppa_k1c/abstractbb/ImpDep.v | 39 +++++++++++++--------------- 3 files changed, 27 insertions(+), 27 deletions(-) (limited to 'mppa_k1c/abstractbb') diff --git a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v index 21e7bd98..904fb72c 100644 --- a/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v +++ b/mppa_k1c/abstractbb/AbstractBasicBlocksDef.v @@ -29,6 +29,11 @@ Parameter genv: Type. (* environment to be used for evaluating an op *) *) Parameter op_eval: genv -> op -> list value -> option value. +Parameter is_constant: op -> bool. + +Parameter is_constant_correct: + forall ge o, is_constant o = true -> op_eval ge o nil <> None. + End LangParam. diff --git a/mppa_k1c/abstractbb/DepTreeTheory.v b/mppa_k1c/abstractbb/DepTreeTheory.v index 6f017378..353e9160 100644 --- a/mppa_k1c/abstractbb/DepTreeTheory.v +++ b/mppa_k1c/abstractbb/DepTreeTheory.v @@ -129,19 +129,17 @@ with list_exp_tree (le: list_exp) (d old: deps): list_tree := Definition failsafe (t: tree): bool := match t with | Tname x => true - | Top o Tnil => - match op_eval ge o nil with - | Some _ => true - | None => false - end + | Top o Tnil => is_constant o | _ => false end. +Local Hint Resolve is_constant_correct. + Lemma failsafe_correct (t: tree) m: failsafe t = true -> tree_eval t m <> None. Proof. destruct t; simpl; try congruence. destruct l; simpl; try congruence. - destruct (op_eval ge o nil); try congruence. + eauto. Qed. Fixpoint macro_deps (i: macro) (d old: deps): deps := diff --git a/mppa_k1c/abstractbb/ImpDep.v b/mppa_k1c/abstractbb/ImpDep.v index 994c8e34..0cce7ce3 100644 --- a/mppa_k1c/abstractbb/ImpDep.v +++ b/mppa_k1c/abstractbb/ImpDep.v @@ -215,7 +215,7 @@ Fixpoint hmacro_deps (i: macro) (d od: hdeps): ?? hdeps := | (x, e)::i' => DO dbg <~ debug_assign x;; DO t0 <~ hdeps_get d x None;; - DO v' <~ (if failsafe ge (data t0) + DO v' <~ (if failsafe (data t0) then hexp_tree e d od dbg else @@ -248,16 +248,16 @@ Lemma hmacro_deps_correct i: forall d1 od1, WHEN hmacro_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 (macro_deps ge i d2 od2) x. + forall x, pdeps_get d1' x = deps_get (macro_deps i d2 od2) x. Proof. induction i; simpl; wlp_simplify. - + cutrewrite (failsafe ge (deps_get d2 a0) = failsafe ge (data exta0)). + + 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 ge (deps_get d2 a0) = failsafe ge (data exta0)). + + 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. @@ -282,7 +282,7 @@ Fixpoint hbblock_deps_rec (p: bblock) (d: hdeps): ?? hdeps := 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 ge p d2) x. + 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. Proof. induction p; simpl; wlp_simplify. Qed. @@ -294,7 +294,7 @@ Definition hbblock_deps: bblock -> ?? hdeps := fun p => hbblock_deps_rec p Dict.empty. Lemma hbblock_deps_correct p: - WHEN hbblock_deps p ~> d1 THEN forall x, pdeps_get d1 x = deps_get (bblock_deps ge p) x. + WHEN hbblock_deps p ~> d1 THEN forall x, pdeps_get d1 x = deps_get (bblock_deps p) x. Proof. unfold bblock_deps; wlp_simplify. erewrite H; eauto. intros; autorewrite with dict_rw; auto. rewrite empty_spec. reflexivity. @@ -375,7 +375,6 @@ Variable dbg1: R.t -> ?? option pstring. (* debugging of p1 macros *) Variable dbg2: R.t -> ?? option pstring. (* log of p2 macros *) Variable log1: unit -> ?? unit. (* log of p1 macros *) Variable log2: unit -> ?? unit. (* log of p2 macros *) -Variable ge: genv. Variable hco_tree: hashConsing tree. @@ -388,8 +387,8 @@ Variable print_error: pstring -> ?? unit. Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool := DO r <~ (TRY - DO d1 <~ hbblock_deps (hC hco_tree) (hC hco_list) ge dbg1 log1 p1 ;; - DO d2 <~ hbblock_deps (hC_known hco_tree) (hC_known hco_list) ge dbg2 log2 p2 ;; + 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 ( @@ -399,7 +398,7 @@ Program Definition g_bblock_eq_test (p1 p2: bblock): ?? bool := CATCH_FAIL s, _ => print_error s;; RET false - ENSURE (fun b => b=true -> bblock_equiv ge p1 p2));; + ENSURE (fun b => b=true -> forall ge, bblock_equiv ge p1 p2));; RET (`r). Obligation 1. destruct hco_tree_correct as [X1 X2], hco_list_correct as [Y1 Y2]. @@ -410,7 +409,7 @@ Obligation 1. Qed. Theorem g_bblock_eq_test_correct p1 p2: - WHEN g_bblock_eq_test p1 p2 ~> b THEN b=true -> bblock_equiv ge p1 p2. + WHEN g_bblock_eq_test p1 p2 ~> b THEN b=true -> forall ge, bblock_equiv ge p1 p2. Proof. wlp_simplify. destruct exta; simpl in * |- *; auto. @@ -439,11 +438,11 @@ Definition print_error (log: logger unit) (s:pstring): ?? unit println (msg_prefix +; msg_number +; n +; " -- " +; s). -Program Definition bblock_eq_test (ge: genv) (p1 p2: bblock): ?? bool := +Program Definition bblock_eq_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) ge hco_tree _ hco_list _ print_error_end (print_error log) p1 p2. + g_bblock_eq_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. @@ -455,8 +454,8 @@ Qed. Local Hint Resolve g_bblock_eq_test_correct. -Theorem bblock_eq_test_correct ge p1 p2: - WHEN bblock_eq_test ge p1 p2 ~> b THEN b=true -> bblock_equiv ge p1 p2. +Theorem bblock_eq_test_correct p1 p2: + WHEN bblock_eq_test p1 p2 ~> b THEN b=true -> forall ge, bblock_equiv ge p1 p2. Proof. wlp_simplify. Qed. @@ -690,7 +689,7 @@ Definition hlog (log: logger unit) (hct: hashConsing tree) (hcl: hashConsing lis next_log hcl s ). -Program Definition verb_bblock_eq_test (ge: genv) (p1 p2: bblock): ?? bool := +Program Definition verb_bblock_eq_test (p1 p2: bblock): ?? bool := DO log1 <~ count_logger ();; DO log2 <~ count_logger ();; DO cr <~ make_cref Nothing;; @@ -701,7 +700,6 @@ Program Definition verb_bblock_eq_test (ge: genv) (p1 p2: bblock): ?? bool := simple_debug (hlog log1 hco_tree hco_list) (log_insert log2) - ge hco_tree _ hco_list _ (print_error_end1 hco_tree hco_list) @@ -719,8 +717,7 @@ Program Definition verb_bblock_eq_test (ge: genv) (p1 p2: bblock): ?? bool := (log_debug log1) simple_debug (hlog log1 hco_tree hco_list) - (log_insert log2) - ge + (log_insert log2) hco_tree _ hco_list _ (print_error_end2 hco_tree hco_list) @@ -749,8 +746,8 @@ Obligation 4. constructor 1; wlp_simplify. Qed. -Theorem verb_bblock_eq_test_correct ge p1 p2: - WHEN verb_bblock_eq_test ge p1 p2 ~> b THEN b=true -> bblock_equiv ge p1 p2. +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. Proof. wlp_simplify. Qed. -- cgit