generalize bblock_equiv into bblock_simu (abstract_bb)

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.