first draft of simu_check

1 files changed, 83 insertions, 19 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index f08998b4..e46dddba 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -637,35 +637,99 @@ Definition hsstate_simu_check (dm: PTree.t node) (f: RTLpath.function) (hst1 hst
   hsistate_simu_check dm f (hinternal hst1) (hinternal hst2);;
   sfval_simu_check dm f (hsi_pc hst1) (hsi_pc hst2) (hfinal hst1) (hfinal hst2).
 
-(*
-Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node) :=
+Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node): ?? unit :=
   let (pc2, pc1) := m in
-  match (hsexec f pc1) with
-  | None => Error (msg "simu_check_single: hsexec f pc1 failed")
-  | Some hst1 =>
-      match (hsexec tf pc2) with
-      | None => Error (msg "simu_check_single: hsexec tf pc2 failed")
-      | Some hst2 => hsstate_simu_check dm f hst1 hst2
-      end
-  end.
+  (* creating the hash-consing tables *)
+  DO hC_sval <~ hCons hSVAL;;
+  DO hC_hlist_sval <~ hCons hLSVAL;;
+  DO hC_hsmem <~ hCons hSMEM;;
+  let hsexec := hsexec hC_sval.(hC) hC_hlist_sval.(hC) hC_hsmem.(hC) in
+  (* performing the hash-consed executions *)
+  DO hst1 <~ hsexec f pc1;;
+  DO hst2 <~ hsexec tf pc2;;
+  (* comparing the executions *)
+  hsstate_simu_check dm f hst1 hst2.
+
+Lemma simu_check_single_correct dm tf f pc1 pc2:
+  WHEN simu_check_single dm f tf (pc2, pc1) ~> _ THEN
+  sexec_simu dm f tf pc1 pc2.
+Admitted.
+Global Opaque simu_check_single.
+Global Hint Resolve simu_check_single_correct: wlp.
 
-Fixpoint simu_check_rec (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) lm :=
+Fixpoint simu_check_rec (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) lm : ?? unit :=
   match lm with
-  | nil => OK tt
-  | m :: lm => do u1 <- simu_check_single dm f tf m;
-               do u2 <- simu_check_rec dm f tf lm;
-               OK tt
+  | nil => RET tt
+  | m :: lm => 
+    simu_check_single dm f tf m;;
+    simu_check_rec dm f tf lm
+  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.
+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 simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) := 
+Definition imp_simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function): ?? unit := 
    simu_check_rec dm f tf (PTree.elements dm).
-*)
 
+Local Hint Resolve PTree.elements_correct: core.
+Lemma imp_simu_check_correct dm f tf:
+  WHEN imp_simu_check dm f tf ~> _ THEN
+  forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2.
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque imp_simu_check.
+Global Hint Resolve imp_simu_check_correct: wlp.
+
+Program Definition aux_simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function): ?? bool :=
+   DO r <~ 
+     (TRY 
+       imp_simu_check dm f tf;; 
+       RET true
+      CATCH_FAIL s, _ =>
+       println ("simu_check_failure:" +; s);;
+       RET false
+      ENSURE (fun b => b=true -> forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2));;
+   RET (`r).
+Obligation 1.
+  split; wlp_simplify. discriminate.
+Qed.
+
+Lemma aux_simu_check_correct dm f tf:
+  WHEN aux_simu_check dm f tf ~> b THEN
+  b=true -> forall pc1 pc2, dm ! pc2 = Some pc1 -> sexec_simu dm f tf pc1 pc2.
+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). *)
 
-Definition simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) := OK tt.
+Import UnsafeImpure.
+
+Definition simu_check (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) : res unit := 
+  match unsafe_coerce (aux_simu_check dm f tf) with
+  | Some true => OK tt
+  | _ => Error (msg "simu_check has failed")
+  end.
 
 Lemma simu_check_correct dm f tf:
   simu_check dm f tf = OK tt ->
   forall pc1 pc2, dm ! pc2 = Some pc1 ->
   sexec_simu dm f tf pc1 pc2.
-Admitted.
\ No newline at end of file
+Proof.
+  unfold simu_check.
+  destruct (unsafe_coerce (aux_simu_check dm f tf)) as [[|]|] eqn:Hres; simpl; try discriminate.
+  intros; eapply aux_simu_check_correct; eauto.
+  eapply unsafe_coerce_not_really_correct; eauto.
+Qed.
\ No newline at end of file