Some advance, need to finish canonbuilding proofs

1 files changed, 270 insertions, 13 deletions

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index 6e86bebb..8f7881a5 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -1,6 +1,6 @@
 Require Import Coqlib AST Maps.
 Require Import Op Registers.
-Require Import RTL BTL.
+Require Import RTL BTL Errors.
 Require Import BTL_SEsimuref BTL_SEtheory OptionMonad.
 
 Require Import Impure.ImpHCons.
@@ -77,6 +77,95 @@ Definition smem_set_hid (sm: smem) (hid: hashcode): smem :=
   | Sstore sm chunk addr lsv srce _ => Sstore sm chunk addr lsv srce hid
   end.
 
+(** Now, we build the hash-Cons value from a "hash_eq".
+
+  Informal specification: 
+    [hash_eq] must be consistent with the "hashed" constructors defined above.
+
+  We expect that hashinfo values in the code of these "hashed" constructors verify:
+    (hash_eq (hdata x) (hdata y) ~> true) <-> (hcodes x)=(hcodes y)
+*)
+
+Definition sval_hash_eq (sv1 sv2: sval): ?? bool :=
+  match sv1, sv2 with
+  | Sinput r1 _, Sinput r2 _ => struct_eq r1 r2 (* NB: really need a struct_eq here ? *)
+  | Sop op1 lsv1 _, Sop op2 lsv2 _  =>
+     DO b1 <~ phys_eq lsv1 lsv2;;
+     if b1
+     then struct_eq op1 op2 (* NB: really need a struct_eq here ? *)
+     else RET false
+  | Sload sm1 trap1 chk1 addr1 lsv1 _, Sload sm2 trap2 chk2 addr2 lsv2 _ =>
+     DO b1 <~ phys_eq lsv1 lsv2;;
+     DO b2 <~ phys_eq sm1 sm2;;
+     DO b3 <~ struct_eq trap1 trap2;;
+     DO b4 <~ struct_eq chk1 chk2;;
+     if b1 && b2 && b3 && b4
+     then struct_eq addr1 addr2
+     else RET false
+  | _,_ => RET false
+  end.
+
+Lemma and_true_split a b: a && b = true <-> a = true /\ b = true.
+Proof.
+  destruct a; simpl; intuition.
+Qed.
+
+Lemma sval_hash_eq_correct x y:
+  WHEN sval_hash_eq x y ~> b THEN 
+   b = true -> sval_set_hid x unknown_hid = sval_set_hid y unknown_hid.
+Proof.
+  destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence.
+Qed.
+Global Opaque sval_hash_eq.
+Local Hint Resolve sval_hash_eq_correct: wlp.
+
+Definition list_sval_hash_eq (lsv1 lsv2: list_sval): ?? bool :=
+  match lsv1, lsv2 with
+  | Snil _, Snil _ => RET true
+  | Scons sv1 lsv1' _, Scons sv2 lsv2' _  =>
+     DO b <~ phys_eq lsv1' lsv2';;
+     if b 
+     then phys_eq sv1 sv2
+     else RET false
+  | _,_ => RET false
+  end.
+
+Lemma list_sval_hash_eq_correct x y:
+  WHEN list_sval_hash_eq x y ~> b THEN 
+   b = true -> list_sval_set_hid x unknown_hid = list_sval_set_hid y unknown_hid.
+Proof.
+  destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence.
+Qed.
+Global Opaque list_sval_hash_eq.
+Local Hint Resolve list_sval_hash_eq_correct: wlp.
+
+Definition smem_hash_eq (sm1 sm2: smem): ?? bool :=
+  match sm1, sm2 with
+  | Sinit _, Sinit _ => RET true
+  | Sstore sm1 chk1 addr1 lsv1 sv1 _, Sstore sm2 chk2 addr2 lsv2 sv2 _ =>
+     DO b1 <~ phys_eq lsv1 lsv2;;
+     DO b2 <~ phys_eq sm1 sm2;;
+     DO b3 <~ phys_eq sv1 sv2;;
+     DO b4 <~ struct_eq chk1 chk2;;
+     if b1 && b2 && b3 && b4
+     then struct_eq addr1 addr2
+     else RET false
+  | _,_ => RET false
+  end.
+
+Lemma smem_hash_eq_correct x y:
+  WHEN smem_hash_eq x y ~> b THEN 
+   b = true -> smem_set_hid x unknown_hid = smem_set_hid y unknown_hid.
+Proof.
+  destruct x, y; wlp_simplify; try (rewrite !and_true_split in *); intuition; subst; try congruence.
+Qed.
+Global Opaque smem_hash_eq.
+Local Hint Resolve smem_hash_eq_correct: wlp.
+
+Definition hSVAL: hashP sval := {| hash_eq := sval_hash_eq; get_hid:=sval_get_hid; set_hid:=sval_set_hid |}. 
+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 |}.
+
 (** * Implementation of symbolic execution *)
 Section CanonBuilding.
 
@@ -465,7 +554,7 @@ Definition simplify (rsv: root_sval) (lr: list reg) (hrs: ristate): ?? sval :=
          DO lsv <~ hlist_args hrs lr;;
          hSop op lsv
         (* TODO gourdinl
-       match target_op_simplify op lr hst with
+       match target_op_simplify op lr hrs with
        | Some fhv => fsval_proj fhv
        | None =>
          hSop op lhsv
@@ -715,16 +804,184 @@ Definition hrexec f ib :=
   DO init <~ hris_init;;
   hrexec_rec f ib init (fun _ => RET Rabort).
 
-Definition hsexec (f: function) (pc:node): ?? rstate :=
-  DO path <~ some_or_fail ((fn_code f)!pc) "hsexec.internal_error.1";;
-  (*DO hinit <~ init_ristate;;*)
-  DO hst <~ hrexec f f.(fn_entrypoint);;
-  DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsexec.internal_error.2";;
-  DO ohst <~ hsiexec_inst i hst;;
-  match ohst with
-  | Some hst' => RET {| hinternal := hst'; hfinal := HSnone |}
-  | None => DO hsvf <~ hsexec_final i hst.(hsi_local);;
-            RET {| hinternal := hst; hfinal := hsvf |}
-   end.
+Lemma hrexec_rec_correct1 ctx ib: 
+  forall rk k
+  (CONTh: forall sis lsis sfv, get_soutcome ctx (k sis) = Some (sout lsis sfv) ->  si_ok ctx lsis -> si_ok ctx sis)
+  (CONT: forall hrs sis lsis sfv st,
+    ris_refines ctx hrs sis ->
+    k sis = st ->
+    get_soutcome ctx (k sis) = Some (sout lsis sfv) ->
+    si_ok ctx lsis ->
+    WHEN rk hrs ~> ris' THEN
+    rst_refines ctx ris' (k sis))
+  hrs sis lsis sfv st
+  (REF: ris_refines ctx hrs sis)
+  (EXEC: sexec_rec (cf ctx) ib sis k = st)
+  (SOUT: get_soutcome ctx st = Some (sout lsis sfv))
+  (OK: si_ok ctx lsis),
+  WHEN hrexec_rec (cf ctx) ib hrs rk ~> hrs THEN
+  rst_refines ctx hrs st.
+Proof.
+  (*
+  induction ib; wlp_simplify.
+  - admit.
+  - eapply CONT; eauto.
+  - try_simplify_someHyps. intros OUT.
+    eapply CONT; eauto.
+    intuition eauto.
+    econstructor; intuition eauto.
+    inv REF. inv H2.
+    intuition eauto.
+
+
+  - (* load *) intros; subst; autodestruct; simpl in *; subst; eauto.
+  - (* seq *)
+    intros; subst.
+    eapply IHib1. 3-6: eauto.
+    + simpl. eapply sexec_rec_okpreserv; eauto.
+    + intros; subst. eapply IHib2; eauto.
+  - (* cond *)
+    intros rk k CONTh CONT hrs sis lsis sfv st REF EXEC OUT OK. subst.
+    assert (rOK: ris_ok ctx hrs). {
+      erewrite <- OK_EQUIV. 2: eauto.
+      eapply sexec_rec_okpreserv with (ib:=(Bcond cond args ib1 ib2 iinfo)); simpl; eauto.
+    }
+    generalize OUT; clear OUT; simpl.
+    autodestruct.
+    intros COND; generalize COND.
+    erewrite <- eval_scondition_refpreserv; eauto.
+    econstructor; try_simplify_someHyps.
+     Qed.*)
+Admitted.
+
+Definition hsexec (f: function) ib: ?? rstate :=
+  hrexec f ib.
 
 End CanonBuilding.
+
+(** * Implementing the simulation test with concrete hash-consed symbolic execution *)
+
+Definition phys_check {A} (x y:A) (msg: pstring): ?? unit :=
+  DO b <~ phys_eq x y;;
+  assert_b b msg;;
+  RET tt.
+
+Definition struct_check {A} (x y: A) (msg: pstring): ?? unit :=
+  DO b <~ struct_eq x y;;
+  assert_b b msg;;
+  RET tt.
+
+Lemma struct_check_correct {A} (a b: A) msg:
+  WHEN struct_check a b msg ~> _ THEN
+  a = b.
+Proof. wlp_simplify. Qed.
+Global Opaque struct_check.
+Hint Resolve struct_check_correct: wlp.
+
+Definition sfval_simu_check (sfv1 sfv2: sfval) := RET tt.
+
+Fixpoint rst_simu_check (rst1 rst2: rstate) :=
+  match rst1, rst2 with
+  | Rfinal ris1 sfv1, Rfinal ris2 sfv2 =>
+      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";;
+      phys_check lsv1 lsv2 "hsstate_simu_check: args do not match";;
+      rst_simu_check rsL1 rsL2;;
+      rst_simu_check rsR1 rsR2
+  | _, _ => FAILWITH "hsstate_simu_check: simu_check failed"
+  end.
+
+Lemma rst_simu_check_correct rst1 rst2:
+  WHEN rst_simu_check rst1 rst2 ~> _ THEN
+  rst_simu rst1 rst2.
+Proof.
+  induction rst1, rst2;
+  wlp_simplify.
+Admitted.
+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)) :=
+  (* creating the hash-consing tables *)
+  DO hC_sval <~ hCons hSVAL;;
+  DO hC_list_hsval <~ hCons hLSVAL;;
+  DO hC_hsmem <~ hCons hSMEM;;
+  let hsexec := hsexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in
+  (* performing the hash-consed executions *)
+  DO hst1 <~ hsexec f1 ib1;;
+  DO hst2 <~ hsexec f2 ib2;;
+  (* comparing the executions *)
+  rst_simu_check hst1 hst2.
+
+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.
+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'.
+
+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.
+Proof.
+  induction lm; wlp_simplify.
+  match goal with
+  | X: (_,_) = (_,_) |- _ => inversion X; subst
+  end.
+  subst; eauto.
+Qed.
+Global Opaque simu_check_rec.
+Global Hint Resolve simu_check_rec_correct: wlp.
+
+Definition imp_simu_check (f tf: function): ?? unit :=
+   simu_check_rec f tf ;;
+   DEBUG("simu_check OK!").
+
+Local Hint Resolve PTree.elements_correct: core.
+Lemma imp_simu_check_correct f tf:
+  WHEN imp_simu_check f tf ~> _ THEN
+  forall sexec_simu f tf.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque imp_simu_check.
+Global Hint Resolve imp_simu_check_correct: wlp.
+
+Program Definition aux_simu_check (f tf: function): ?? bool :=
+   DO r <~ 
+     (TRY 
+       imp_simu_check f tf;; 
+       RET true
+      CATCH_FAIL s, _ =>
+       println ("simu_check_failure:" +; s);;
+       RET false
+      ENSURE (sexec_simu f tf));;
+   RET (`r).
+Obligation 1.
+  split; wlp_simplify. discriminate.
+Qed.
+
+Lemma aux_simu_check_correct f tf:
+  WHEN aux_simu_check f tf ~> b THEN
+  sexec_simu f tf.
+Proof.
+  unfold aux_simu_check; wlp_simplify.
+  destruct exta; simpl; auto.
+Qed.
+
+(* Coerce aux_simu_check into a pure function (this is a little unsafe like all oracles in CompCert). *)
+
+Import UnsafeImpure.
+
+Definition simu_check (f tf: function) : res unit := 
+  match unsafe_coerce (aux_simu_check f tf) with
+  | Some true => OK tt
+  | _ => Error (msg "simu_check has failed")
+  end.