hrexec_correct1

1 files changed, 48 insertions, 25 deletions

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
index 25819ffa..b04c17fb 100644
--- a/scheduling/BTL_SEimpl.v
+++ b/scheduling/BTL_SEimpl.v
@@ -657,7 +657,8 @@ Lemma cbranch_expanse_correct hrs c l:
   (REF : ris_refines ctx hrs sis)
   (OK: ris_ok ctx hrs),
   eval_scondition ctx (fst r) (snd r) =
-  eval_scondition ctx c (list_sval_inj (map (si_sreg sis) l)).
+  eval_scondition ctx c (list_sval_inj (map (si_sreg sis) l))
+  /\ (fst r) = c.
 Proof.
   unfold cbranch_expanse.
   wlp_simplify; inv REF.
@@ -687,6 +688,8 @@ Proof.
   + destruct 1; simpl in *. unfold ris_sreg_get; simpl.
     intros; rewrite PTree.gempty; eauto.
 Qed.
+Local Hint Resolve hrs_init_correct: wlp.
+Global Opaque hrs_init.
 
 Definition hrs_sreg_set r lr rsv (hrs: ristate): ?? ristate :=
   DO ok_lsv <~
@@ -935,26 +938,26 @@ Lemma hrexec_rec_correct1 ctx ib:
   rst_refines ctx rst st.
 Proof.
   induction ib; try (wlp_simplify; fail).
-  - wlp_simplify; eapply CONT; eauto.
-  - destruct trap; wlp_simplify.
-  - (* seq *)
+  - (* Bnop *) wlp_simplify; eapply CONT; eauto.
+  - (* Bload *) destruct trap; wlp_simplify.
+  - (* Bseq *)
     wlp_simplify.
     eapply IHib1. 3-7: eauto.
     + simpl. eapply sexec_rec_okpreserv; eauto.
     + intros; subst. eapply IHib2; eauto.
-  - (* cond *)
+  - (* Bcond *)
     simpl; intros; wlp_simplify.
     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.
+    exploit (Refcond ctx cond (snd exta) (list_sval_inj (map sis args)) exta0 exta1
+              (sexec_rec (cf ctx) ib1 sis k) (sexec_rec (cf ctx) ib2 sis k));
+    exploit H; eauto; intros (SEVAL & EQC); subst; auto.
+    all: simpl in SOUT; generalize SOUT; inversion_SOME b0; try_simplify_someHyps.
+    * intros; eapply IHib1; eauto.
+    * intros; eapply IHib2; eauto.
+Qed.
 
 Lemma hrexec_correct1 ctx ib sis sfv:
   get_soutcome ctx (sexec (cf ctx) ib) = Some (sout sis sfv) ->
@@ -963,14 +966,7 @@ Lemma hrexec_correct1 ctx ib sis sfv:
   rst_refines ctx rst (sexec (cf ctx) ib).
 Proof.
   unfold sexec; intros; wlp_simplify.
-  eapply hrexec_rec_correct1; eauto; simpl; try congruence; split.
-  - intuition eauto.
-    + inv H2; constructor; auto; simpl; congruence.
-    + inv H2; split; simpl in *; try congruence; trivial.
-  - intros X; simpl in *; auto.
-  - intros X r; inv X; simpl in *.
-    unfold ris_sreg_get; simpl; rewrite PTree.gempty; simpl.
-    reflexivity.
+  eapply hrexec_rec_correct1; eauto; simpl; congruence.
 Qed.
 
 (*Lemma hrexec_rec_correct2 ctx ib: 
@@ -999,7 +995,7 @@ Lemma hrexec_correct2 ctx ib hrs rfv:
 Proof.
 Admitted.
 
-Lemma hrexec_simu_correct ctx ib:
+Lemma hrexec_correct_aux ctx ib:
   WHEN hrexec (cf ctx) ib ~> rst THEN
   exists st, sexec (cf ctx) ib = st /\ rst_refines ctx rst st.
 Proof.
@@ -1007,8 +1003,34 @@ Proof.
   repeat eexists.
 Admitted.
 
+Global Opaque hrexec.
+
 End CanonBuilding.
 
+(** Correction of concrete symbolic execution wrt abstract symbolic execution *)
+Theorem hrexec_correct
+  (hC_hsval : hashinfo sval -> ?? sval)
+  (hC_list_hsval : hashinfo list_sval -> ?? list_sval)
+  (hC_hsmem : hashinfo smem -> ?? smem)
+  (ctx: iblock_exec_context) 
+  (ib: iblock):
+       WHEN hrexec hC_hsval hC_list_hsval hC_hsmem (cf ctx) ib ~> hrs THEN forall
+        (hC_hsval_correct: forall hs,
+            WHEN hC_hsval hs ~> hs' THEN forall ctx,
+                sval_refines ctx (hdata hs) hs')
+        (hC_list_hsval_correct: forall lh,
+            WHEN hC_list_hsval lh ~> lh' THEN forall ctx,
+              list_sval_refines ctx (hdata lh) lh')
+         (hC_hsmem_correct: forall hm,
+            WHEN hC_hsmem hm ~> hm' THEN forall ctx,
+              smem_refines ctx (hdata hm) hm'),
+         exists st : sstate, sexec (cf ctx) ib = st /\ rst_refines ctx hrs st.
+Proof.
+  wlp_simplify.
+  eapply hrexec_correct_aux; eauto.
+Qed.
+Local Hint Resolve hrexec_correct: wlp.
+
 (** * Implementing the simulation test with concrete hash-consed symbolic execution *)
 
 Definition phys_check {A} (x y:A) (msg: pstring): ?? unit :=
@@ -1233,10 +1255,10 @@ Definition simu_check_single (f1 f2: function) (ib1 ib2: iblock): ?? unit :=
   DO hC_sval <~ hCons hSVAL;;
   DO hC_list_hsval <~ hCons hLSVAL;;
   DO hC_hsmem <~ hCons hSMEM;;
-  let hsexec := hrexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in
+  let hrexec := hrexec 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;;
+  DO hst1 <~ hrexec f1 ib1;;
+  DO hst2 <~ hrexec f2 ib2;;
   (* comparing the executions *)
   rst_simu_check hst1 hst2.
 
@@ -1245,9 +1267,10 @@ Lemma simu_check_single_correct (f1 f2: function) (ib1 ib2: iblock):
   symbolic_simu f1 f2 ib1 ib2.
 Proof. (* TODO *)
   unfold symbolic_simu; wlp_simplify.
+    exploit hrexec_correct; eauto.
   eapply rst_simu_correct; eauto.
   + intros; eapply hrexec_correct1; eauto.
-    1-3: wlp_simplify. unfold hrexec.
+    1-3: wlp_simplify. intuition eauto.
     simpl. eauto.
     intuition eauto.
     admit.