progress in simulation test

1 files changed, 250 insertions, 57 deletions

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index 8f7881a5..94d7375d 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -166,6 +166,17 @@ Definition hSVAL: hashP sval := {| hash_eq := sval_hash_eq; get_hid:=sval_get_hi
 Definition hLSVAL: hashP list_sval := {| hash_eq := list_sval_hash_eq; get_hid:= list_sval_get_hid; set_hid:= list_sval_set_hid |}.
 Definition hSMEM: hashP smem := {| hash_eq := smem_hash_eq; get_hid:= smem_get_hid; set_hid:= smem_set_hid |}.
 
+Program Definition mk_hash_params: Dict.hash_params sval :=
+ {|
+    Dict.test_eq := phys_eq;
+    Dict.hashing := fun (sv: sval) => RET (sval_get_hid sv);
+    Dict.log := fun sv =>
+         DO sv_name <~ string_of_hashcode (sval_get_hid sv);;
+         println ("unexpected undef behavior of hashcode:" +; (CamlStr sv_name)) |}.
+Obligation 1.
+  wlp_simplify.
+Qed.
+
 (** * Implementation of symbolic execution *)
 Section CanonBuilding.
 
@@ -194,17 +205,17 @@ Definition undef_code := 4.
 
 Definition hSinput_hcodes (r: reg) :=
    DO hc <~ hash reg_hcode;;
-   DO hv <~ hash r;;
-   RET [hc;hv].
+   DO sv <~ hash r;;
+   RET [hc;sv].
 Extraction Inline hSinput_hcodes.
 
 Definition hSinput (r:reg): ?? sval :=
-   DO hv <~ hSinput_hcodes r;;
-   hC_sval {| hdata:=Sinput r unknown_hid; hcodes :=hv; |}.
+   DO sv <~ hSinput_hcodes r;;
+   hC_sval {| hdata:=Sinput r unknown_hid; hcodes :=sv; |}.
 
 Lemma hSinput_correct r:
-  WHEN hSinput r ~> hv THEN forall ctx,
-    sval_refines ctx hv (Sinput r unknown_hid).
+  WHEN hSinput r ~> sv THEN forall ctx,
+    sval_refines ctx sv (Sinput r unknown_hid).
 Proof.
   wlp_simplify.
 Qed.
@@ -213,17 +224,17 @@ Local Hint Resolve hSinput_correct: wlp.
 
 Definition hSop_hcodes (op:operation) (lsv: list_sval) :=
    DO hc <~ hash op_hcode;;
-   DO hv <~ hash op;;
-   RET [hc;hv;list_sval_get_hid lsv].
+   DO sv <~ hash op;;
+   RET [hc;sv;list_sval_get_hid lsv].
 Extraction Inline hSop_hcodes.
 
 Definition hSop (op:operation) (lsv: list_sval): ?? sval :=
-   DO hv <~ hSop_hcodes op lsv;;
-   hC_sval {| hdata:=Sop op lsv unknown_hid; hcodes :=hv |}.
+   DO sv <~ hSop_hcodes op lsv;;
+   hC_sval {| hdata:=Sop op lsv unknown_hid; hcodes :=sv |}.
 
 Lemma hSop_fSop_correct op lsv:
-  WHEN hSop op lsv ~> hv THEN forall ctx,
-    sval_refines ctx hv (fSop op lsv).
+  WHEN hSop op lsv ~> sv THEN forall ctx,
+    sval_refines ctx sv (fSop op lsv).
 Proof.
   wlp_simplify.
 Qed.
@@ -231,9 +242,9 @@ Global Opaque hSop.
 Local Hint Resolve hSop_fSop_correct: wlp_raw.
 
 Lemma hSop_correct op lsv1:
-  WHEN hSop op lsv1 ~> hv THEN forall ctx lsv2
+  WHEN hSop op lsv1 ~> sv THEN forall ctx lsv2
    (LR: list_sval_refines ctx lsv1 lsv2),
-   sval_refines ctx hv (Sop op lsv2 unknown_hid).
+   sval_refines ctx sv (Sop op lsv2 unknown_hid).
 Proof.
   wlp_xsimplify ltac:(intuition eauto with wlp wlp_raw).
   rewrite <- LR. erewrite H; eauto.
@@ -242,21 +253,21 @@ Local Hint Resolve hSop_correct: wlp.
 
 Definition hSload_hcodes (sm: smem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval):=
    DO hc <~ hash load_hcode;;
-   DO hv1 <~ hash trap;;
-   DO hv2 <~ hash chunk;;
-   DO hv3 <~ hash addr;;
-   RET [hc; smem_get_hid sm; hv1; hv2; hv3; list_sval_get_hid lsv].
+   DO sv1 <~ hash trap;;
+   DO sv2 <~ hash chunk;;
+   DO sv3 <~ hash addr;;
+   RET [hc; smem_get_hid sm; sv1; sv2; sv3; list_sval_get_hid lsv].
 Extraction Inline hSload_hcodes.
 
 Definition hSload (sm: smem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval): ?? sval :=
-   DO hv <~ hSload_hcodes sm trap chunk addr lsv;;
-   hC_sval {| hdata := Sload sm trap chunk addr lsv unknown_hid; hcodes := hv |}.
+   DO sv <~ hSload_hcodes sm trap chunk addr lsv;;
+   hC_sval {| hdata := Sload sm trap chunk addr lsv unknown_hid; hcodes := sv |}.
 
 Lemma hSload_correct sm1 trap chunk addr lsv1:
-  WHEN hSload sm1 trap chunk addr lsv1 ~> hv THEN forall ctx lsv2 sm2
+  WHEN hSload sm1 trap chunk addr lsv1 ~> sv THEN forall ctx lsv2 sm2
     (LR: list_sval_refines ctx lsv1 lsv2)
     (MR: smem_refines ctx sm1 sm2),
-    sval_refines ctx hv (Sload sm2 trap chunk addr lsv2 unknown_hid).
+    sval_refines ctx sv (Sload sm2 trap chunk addr lsv2 unknown_hid).
 Proof.
   wlp_simplify.
   rewrite <- LR, <- MR.
@@ -271,12 +282,12 @@ Definition hSundef_hcodes :=
 Extraction Inline hSundef_hcodes.
 
 Definition hSundef : ?? sval :=
-   DO hv <~ hSundef_hcodes;;
-   hC_sval {| hdata:=Sundef unknown_hid; hcodes :=hv; |}.
+   DO sv <~ hSundef_hcodes;;
+   hC_sval {| hdata:=Sundef unknown_hid; hcodes :=sv; |}.
 
 Lemma hSundef_correct:
-  WHEN hSundef ~> hv THEN forall ctx,
-    sval_refines ctx hv (Sundef unknown_hid).
+  WHEN hSundef ~> sv THEN forall ctx,
+    sval_refines ctx sv (Sundef unknown_hid).
 Proof.
   wlp_simplify.
 Qed.
@@ -287,8 +298,8 @@ Definition hSnil (_: unit): ?? list_sval :=
    hC_list_sval {| hdata := Snil unknown_hid; hcodes := nil |}.
 
 Lemma hSnil_correct:
-  WHEN hSnil() ~> hv THEN forall ctx,
-    list_sval_refines ctx hv (Snil unknown_hid).
+  WHEN hSnil() ~> sv THEN forall ctx,
+    list_sval_refines ctx sv (Snil unknown_hid).
 Proof.
   wlp_simplify.
 Qed.
@@ -324,14 +335,14 @@ Global Opaque hSinit.
 Local Hint Resolve hSinit_correct: wlp.
 
 Definition hSstore_hcodes (sm: smem) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) (srce: sval):=
-   DO hv1 <~ hash chunk;;
-   DO hv2 <~ hash addr;;
-   RET [smem_get_hid sm; hv1; hv2; list_sval_get_hid lsv; sval_get_hid srce].
+   DO sv1 <~ hash chunk;;
+   DO sv2 <~ hash addr;;
+   RET [smem_get_hid sm; sv1; sv2; list_sval_get_hid lsv; sval_get_hid srce].
 Extraction Inline hSstore_hcodes.
 
 Definition hSstore (sm: smem) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) (srce: sval): ?? smem :=
-   DO hv <~ hSstore_hcodes sm chunk addr lsv srce;;
-   hC_smem {| hdata := Sstore sm chunk addr lsv srce unknown_hid; hcodes := hv |}.
+   DO sv <~ hSstore_hcodes sm chunk addr lsv srce;;
+   hC_smem {| hdata := Sstore sm chunk addr lsv srce unknown_hid; hcodes := sv |}.
 
 Lemma hSstore_correct sm1 chunk addr lsv1 sv1:
   WHEN hSstore sm1 chunk addr lsv1 sv1 ~> sm1' THEN forall ctx lsv2 sm2 sv2
@@ -408,12 +419,12 @@ with fsval_list_proj sl: ?? list_sval :=
       DO b <~ phys_eq hc unknown_hid;;
       if b then hSnil() (* was not yet really hash-consed *)
       else RET sl (* already hash-consed *)
-  | Scons hv hl hc => 
+  | Scons sv hl hc => 
       DO b <~ phys_eq hc unknown_hid;;
       if b then (* was not yet really hash-consed *)
-        DO hv' <~ fsval_proj hv;;
+        DO sv' <~ fsval_proj sv;;
         DO hl' <~ fsval_list_proj hl;;
-        hScons hv' hl' 
+        hScons sv' hl' 
       else RET sl (* already hash-consed *)
   end.
 
@@ -555,7 +566,7 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval :=
          hSop op lsv
         (* TODO gourdinl
        match target_op_simplify op lr hrs with
-       | Some fhv => fsval_proj fhv
+       | Some fsv => fsval_proj fsv
        | None =>
          hSop op lhsv
            end*)
@@ -566,11 +577,11 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval :=
   end.
 
 Lemma simplify_correct rsv lr hrs:
-  WHEN simplify rsv lr hrs ~> hv THEN forall ctx sis
+  WHEN simplify rsv lr hrs ~> sv THEN forall ctx sis
     (REF: ris_refines ctx hrs sis)
     (OK0: ris_ok ctx hrs)
     (OK1: eval_sval ctx (rsv lr sis) <> None),
-    sval_refines ctx hv (rsv lr sis).
+    sval_refines ctx sv (rsv lr sis).
 Proof.
   destruct rsv; simpl; auto.
   - (* Rop *)
@@ -678,9 +689,9 @@ Qed.
 Definition hrset_sreg r lr rsv (hrs: ristate): ?? ristate :=
   DO ok_lsv <~
     (if may_trap rsv lr
-     then DO hv <~ root_happly rsv lr hrs;;
-          XDEBUG hv (fun hv => DO hv_name <~ string_of_hashcode (sval_get_hid hv);; RET ("-- insert undef behavior of hashcode:" +; (CamlStr hv_name))%string);;
-          RET (hv::(ok_rsval hrs))
+     then DO sv <~ root_happly rsv lr hrs;;
+          XDEBUG sv (fun sv => DO sv_name <~ string_of_hashcode (sval_get_hid sv);; RET ("-- insert undef behavior of hashcode:" +; (CamlStr sv_name))%string);;
+          RET (sv::(ok_rsval hrs))
      else RET (ok_rsval hrs));;
   DO simp <~ simplify rsv lr hrs;;
   RET {| ris_smem := hrs.(ris_smem);
@@ -878,11 +889,186 @@ Proof. wlp_simplify. Qed.
 Global Opaque struct_check.
 Hint Resolve struct_check_correct: wlp.
 
-Definition sfval_simu_check (sfv1 sfv2: sfval) := RET tt.
+Definition option_eq_check {A} (o1 o2: option A): ?? unit :=
+  match o1, o2 with
+  | Some x1, Some x2 => phys_check x1 x2 "option_eq_check: data physically differ"
+  | None, None => RET tt
+  | _, _ => FAILWITH "option_eq_check: structure differs"
+  end.
 
-Fixpoint rst_simu_check (rst1 rst2: rstate) :=
+Lemma option_eq_check_correct A (o1 o2: option A): WHEN option_eq_check o1 o2 ~> _ THEN o1=o2.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque option_eq_check.
+Hint Resolve option_eq_check_correct:wlp.
+
+Import PTree.
+
+Fixpoint PTree_eq_check {A} (d1 d2: PTree.t A): ?? unit :=
+  match d1, d2 with
+  | Leaf, Leaf => RET tt
+  | Node l1 o1 r1, Node l2 o2 r2 =>
+      option_eq_check o1 o2;;
+      PTree_eq_check l1 l2;;
+      PTree_eq_check r1 r2
+  | _, _ => FAILWITH "PTree_eq_check: some key is absent"
+  end.
+
+Lemma PTree_eq_check_correct A d1: forall (d2: t A),
+ WHEN PTree_eq_check d1 d2 ~> _ THEN forall x, PTree.get x d1 = PTree.get x d2.
+Proof.
+  induction d1 as [|l1 Hl1 o1 r1 Hr1]; destruct d2 as [|l2 o2 r2]; simpl; 
+  wlp_simplify. destruct x; simpl; auto.
+Qed.
+Global Opaque PTree_eq_check.
+Local Hint Resolve PTree_eq_check_correct: wlp.
+
+Definition hrs_simu_check (hrs1 hrs2: ristate) : ?? unit :=
+  DEBUG("? hrs_simu_check");;
+  phys_check (ris_smem hrs1) (ris_smem hrs2) "hrs_simu_check: ris_smem sets aren't equiv";;
+  phys_check (ris_input_init hrs1) (ris_input_init hrs2) "hrs_simu_check: ris_input_init bools aren't equiv";;
+  PTree_eq_check (ris_sreg hrs1) (ris_sreg hrs2);;
+  Sets.assert_list_incl mk_hash_params (ok_rsval hrs2) (ok_rsval hrs1);;
+  DEBUG("=> hrs_simu_check: OK").
+
+Lemma setoid_in {A: Type} (a: A): forall l,
+  SetoidList.InA (fun x y => x = y) a l ->
+  In a l.
+Proof.
+  induction l; intros; inv H.
+  - constructor. reflexivity.
+  - right. auto.
+Qed.
+
+Lemma regset_elements_in r rs:
+  Regset.In r rs ->
+  In r (Regset.elements rs).
+Proof.
+  intros. exploit Regset.elements_1; eauto. intro SIN.
+  apply setoid_in. assumption.
+Qed.
+Local Hint Resolve regset_elements_in: core.
+
+Lemma hrs_simu_check_correct hrs1 hrs2:
+  WHEN hrs_simu_check hrs1 hrs2 ~> _ THEN
+  ris_simu hrs1 hrs2.
+Proof.
+  wlp_simplify; constructor; auto.
+  unfold ris_sreg_get; intros r; rewrite H, H1; reflexivity.
+Qed.
+Hint Resolve hrs_simu_check_correct: wlp.
+Global Opaque hrs_simu_check.
+
+Definition svos_simu_check (svos1 svos2: sval + ident) :=
+  match svos1, svos2 with
+  | inl sv1, inl sv2 => phys_check sv1 sv2 "svos_simu_check: sval mismatch"
+  | inr id1, inr id2 => phys_check id1 id2 "svos_simu_check: symbol mismatch"
+  | _, _ => FAILWITH "svos_simu_check: type mismatch"
+  end.
+
+Lemma svos_simu_check_correct svos1 svos2:
+  WHEN svos_simu_check svos1 svos2 ~> _ THEN
+  svos1 = svos2.
+Proof.
+  destruct svos1; destruct svos2; wlp_simplify.
+Qed.
+Global Opaque svos_simu_check.
+Hint Resolve svos_simu_check_correct: wlp.
+
+Fixpoint builtin_arg_simu_check (bs bs': builtin_arg sval) :=
+  match bs with
+  | BA sv =>
+    match bs' with
+    | BA sv' => phys_check sv sv' "builtin_arg_simu_check: sval mismatch"
+    | _ => FAILWITH "builtin_arg_simu_check: BA mismatch"
+    end
+  | BA_splitlong lo hi =>
+    match bs' with
+    | BA_splitlong lo' hi' =>
+        builtin_arg_simu_check lo lo';;
+        builtin_arg_simu_check hi hi'
+    | _ => FAILWITH "builtin_arg_simu_check: BA_splitlong mismatch"
+    end
+  | BA_addptr b1 b2 =>
+    match bs' with
+    | BA_addptr b1' b2' =>
+        builtin_arg_simu_check b1 b1';;
+        builtin_arg_simu_check b2 b2'
+    | _ => FAILWITH "builtin_arg_simu_check: BA_addptr mismatch"
+    end
+  | bs => struct_check bs bs' "builtin_arg_simu_check: basic mismatch"
+  end.
+
+Lemma builtin_arg_simu_check_correct: forall bs1 bs2,
+  WHEN builtin_arg_simu_check bs1 bs2 ~> _ THEN
+  bs1 = bs2.
+Proof.
+  induction bs1.
+  all: try (wlp_simplify; subst; reflexivity).
+  all: destruct bs2; wlp_simplify; congruence.
+Qed.
+Global Opaque builtin_arg_simu_check.
+Hint Resolve builtin_arg_simu_check_correct: wlp.
+
+Fixpoint list_builtin_arg_simu_check lbs1 lbs2 :=
+  match lbs1, lbs2 with
+  | nil, nil => RET tt
+  | bs1::lbs1, bs2::lbs2 =>
+    builtin_arg_simu_check bs1 bs2;;
+    list_builtin_arg_simu_check lbs1 lbs2
+  | _, _ => FAILWITH "list_builtin_arg_simu_check: length mismatch"
+  end.
+
+Lemma list_builtin_arg_simu_check_correct: forall lbs1 lbs2,
+  WHEN list_builtin_arg_simu_check lbs1 lbs2 ~> _ THEN
+  lbs1 = lbs2.
+Proof.
+  induction lbs1; destruct lbs2; wlp_simplify. congruence.
+Qed.
+Global Opaque list_builtin_arg_simu_check.
+Hint Resolve list_builtin_arg_simu_check_correct: wlp.
+
+Definition sfval_simu_check (sfv1 sfv2: sfval): ?? unit :=
+  match sfv1, sfv2 with
+  | Sgoto e1, Sgoto e2 =>
+      phys_check e1 e2 "sfval_simu_check: Sgoto successors do not match"
+  | Scall sig1 svos1 lsv1 res1 e1, Scall sig2 svos2 lsv2 res2 e2 =>
+      phys_check e1 e2 "sfval_simu_check: Scall successors do not match";;
+      phys_check sig1 sig2 "sfval_simu_check: Scall different signatures";;
+      phys_check res1 res2 "sfval_simu_check: Scall res do not match";;
+      svos_simu_check svos1 svos2;;
+      phys_check lsv1 lsv2 "sfval_simu_check: Scall args do not match"
+  | Stailcall sig1 svos1 lsv1, Stailcall sig2 svos2 lsv2 =>
+      phys_check sig1 sig2 "sfval_simu_check: Stailcall different signatures";;
+      svos_simu_check svos1 svos2;;
+      phys_check lsv1 lsv2 "sfval_simu_check: Stailcall args do not match"
+  | Sbuiltin ef1 lbs1 br1 e1, Sbuiltin ef2 lbs2 br2 e2 =>
+      phys_check e1 e2 "sfval_simu_check: Sbuiltin successors do not match";;
+      phys_check ef1 ef2 "sfval_simu_check: Sbuiltin ef do not match";;
+      phys_check br1 br2 "sfval_simu_check: Sbuiltin br do not match";;
+      list_builtin_arg_simu_check lbs1 lbs2
+  | Sjumptable sv1 le1, Sjumptable sv2 le2 =>
+      phys_check le1 le2 "sfval_simu_check: Sjumptable successors do not match";;
+      phys_check sv1 sv2 "sfval_simu_check: Sjumptable sval do not match"
+  | Sreturn osv1, Sreturn osv2 =>
+      option_eq_check osv1 osv2
+  | _, _ => FAILWITH "sfval_simu_check: structure mismatch"
+  end.
+
+Lemma sfval_simu_check_correct sfv1 sfv2:
+  WHEN sfval_simu_check sfv1 sfv2 ~> _ THEN
+  rfv_simu sfv1 sfv2.
+Proof.
+  destruct sfv1; destruct sfv2; simpl; wlp_simplify; try congruence.
+Qed.
+Hint Resolve sfval_simu_check_correct: wlp.
+Global Opaque sfval_simu_check.
+
+Fixpoint rst_simu_check (rst1 rst2: rstate) {struct rst1} :=
   match rst1, rst2 with
-  | Rfinal ris1 sfv1, Rfinal ris2 sfv2 =>
+  | Rfinal hrs1 sfv1, Rfinal hrs2 sfv2 =>
+      hrs_simu_check hrs1 hrs2;;
       sfval_simu_check sfv1 sfv2
   | Rcond cond1 lsv1 rsL1 rsR1, Rcond cond2 lsv2 rsL2 rsR2 =>
       struct_check cond1 cond2 "hsstate_simu_check: conditions do not match";;
@@ -892,17 +1078,18 @@ Fixpoint rst_simu_check (rst1 rst2: rstate) :=
   | _, _ => FAILWITH "hsstate_simu_check: simu_check failed"
   end.
 
-Lemma rst_simu_check_correct rst1 rst2:
+Lemma rst_simu_check_correct rst1: forall rst2,
   WHEN rst_simu_check rst1 rst2 ~> _ THEN
   rst_simu rst1 rst2.
 Proof.
-  induction rst1, rst2;
-  wlp_simplify.
-Admitted.
+  induction rst1; destruct rst2;
+  wlp_simplify; constructor; auto.
+Qed.
 Hint Resolve rst_simu_check_correct: wlp.
 Global Opaque rst_simu_check.
 
-Definition simu_check_single (f1 f2: function) (ib1 ib2: iblock): ?? (option (node * node)) :=
+(* TODO do we really need both functions *)
+Definition simu_check_single (f1 f2: function) (ib1 ib2: iblock): ?? unit :=
   (* creating the hash-consing tables *)
   DO hC_sval <~ hCons hSVAL;;
   DO hC_list_hsval <~ hCons hLSVAL;;
@@ -918,18 +1105,24 @@ Lemma simu_check_single_correct (f1 f2: function) (ib1 ib2: iblock):
   WHEN simu_check_single f1 f2 ib1 ib2 ~> _ THEN
   symbolic_simu f1 f2 ib1 ib2.
 Proof.
+  unfold symbolic_simu; wlp_simplify.
 Admitted.
 Global Opaque simu_check_single.
 Global Hint Resolve simu_check_single_correct: wlp.
 
-Fixpoint simu_check_rec (f1 f2: function) (ibf1 ibf2: iblock_info): ?? unit :=
-  DO res <~ simu_check_single f1 f2 ibf1.(entry) ibf2.(entry);;
-  let (pc1', pc2') := res in
-  simu_check_rec pc1' pc2'.
+Fixpoint simu_check_rec (f1 f2: function) (blks: list node): ?? unit :=
+  match blks with
+  | nil => RET tt
+  | pc :: blk' =>
+      DO ibf1 <~ some_or_fail (fn_code f1)!pc "simu_check_rec: incorrect PTree for f1";;
+      DO ibf2 <~ some_or_fail (fn_code f2)!pc "simu_check_rec: incorrect PTree for f2";;
+      DO res <~ simu_check_single f1 f2 ibf1.(entry) ibf2.(entry);;
+      simu_check_rec f1 f2 blk'
+  end.
 
-Lemma simu_check_rec_correct dm f tf lm:
-  WHEN simu_check_rec dm f tf lm ~> _ THEN
-  forall pc1 pc2, In (pc2, pc1) lm -> sexec_simu dm f tf pc1 pc2.
+Lemma simu_check_rec_correct f1 f2:
+  WHEN simu_check_rec f1 f2 (PTree.elements (fn_code f1)) ~> _ THEN
+  symbolic_simu f1 f2 .
 Proof.
   induction lm; wlp_simplify.
   match goal with