Branching simu_coreb

1 files changed, 58 insertions, 211 deletions

diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v
index bfa66d8b..f25143fd 100644
--- a/kvx/lib/RTLpathSE_impl.v
+++ b/kvx/lib/RTLpathSE_impl.v
@@ -205,6 +205,14 @@ Definition hsiexit_simu dm f (ctx: simu_proof_context f) hse1 hse2: Prop := fora
   hsiexit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 ->
   siexit_simu dm f ctx se1 se2.
 
+(* Definition hsiexit_simub (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate_exit) :=
+  if (eq_condition (hsi_cond hse1) (hsi_cond hse2)) then
+    do _ <- list_sval_simub (hsi_scondargs hse1) (hsi_scondargs hse2);
+    do _ <- hsilocal_simub dm f (hsi_elocal hse1) (hsi_elocal hse2);
+    revmap_check_single dm (hsi_ifso hse1) (hsi_ifso hse2)
+  else Error (msg "siexit_simub: conditions do not match")
+. *)
+
 Lemma hsiexit_simu_core_nofail dm f hse1 hse2 ge1 ge2 sp rs m:
   hsiexit_simu_core dm f hse1 hse2 ->
   (forall s, Genv.find_symbol ge1 s = Genv.find_symbol ge2 s) ->
@@ -278,6 +286,38 @@ Definition hsiexits_simu dm f (ctx: simu_proof_context f) lhse1 lhse2: Prop :=
 Definition hsiexits_simu_core dm f lhse1 lhse2: Prop :=
   list_forall2 (hsiexit_simu_core dm f) lhse1 lhse2.
 
+(* Fixpoint hsiexits_simub (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) :=
+  match lhse1 with
+  | nil =>
+      match lhse2 with
+      | nil => OK tt
+      | _ => Error (msg "siexists_simub: sle1 and sle2 lengths do not match")
+      end
+  | hse1 :: lhse1 =>
+      match lhse2 with
+      | nil => Error (msg "siexits_simub: sle1 and sle2 lengths do not match")
+      | hse2 :: lhse2 =>
+          do _ <- hsiexit_simub dm f hse1 hse2;
+          do _ <- hsiexits_simub dm f lhse1 lhse2;
+          OK tt
+      end
+  end. *)
+
+(* Lemma hsiexits_simub_correct dm f ctx lhse1: forall lhse2,
+  hsiexits_simub dm f lhse1 lhse2 = OK tt ->
+  hsiexits_simu dm f ctx lhse1 lhse2.
+Proof.
+(*   induction lhse1.
+  - simpl. intros. destruct lhse2; try discriminate. intros se1 se2 HEREFS1 HEREFS2 _ _.
+    inv HEREFS1. inv HEREFS2. constructor.
+  - (* simpl. *) unfold hsiexits_simub. intros. destruct lhse2; try discriminate. explore.
+    fold hsiexits_simub in EQ1.
+    eapply hsiexit_simub_correct in EQ. apply IHlhse1 in EQ1.
+    intros se1 se2 HEREFS1 HEREFS2 HEREFD1 HEREFD2. inv HEREFS1. inv HEREFS2. inv HEREFD1. inv HEREFD2. constructor; auto.
+    apply EQ1; assumption. *)
+Admitted.
+ *)
+
 (* TODO *)
 Definition hsiexits_simu_coreb (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) := OK tt.
 
@@ -554,7 +594,15 @@ Definition hsstate_refines (hst: hsstate) (st:sstate): Prop :=
 
 Definition hsstate_simu_core (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
      hsistate_simu_core dm f (hinternal hst1) (hinternal hst2)
-  /\ hfinal hst1 = hfinal hst2.
+  /\ hfinal_simu_core dm f (hfinal hst1) (hfinal hst2).
+
+Definition hsstate_simu_coreb (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) := OK tt. (* TODO *)
+
+Theorem hsstate_simu_coreb_correct dm f hst1 hst2:
+  hsstate_simu_coreb dm f hst1 hst2 = OK tt ->
+  hsstate_simu_core dm f hst1 hst2.
+Proof.
+Admitted.
 
 Definition hok ge sp rs m hst := hsok ge sp rs m (hinternal hst).
 
@@ -563,15 +611,6 @@ Definition hsstate_simu dm f (hst1 hst2: hsstate) ctx: Prop :=
   hsstate_refines hst1 st1 ->
   hsstate_refines hst2 st2 -> sstate_simu dm f st1 st2 ctx.
 
-Remark sfval_simu_reflexive dm f ctx pc1 pc2 hf:
-  dm ! pc2 = Some pc1 ->
-  sfval_simu dm f pc1 pc2 ctx hf hf.
-Proof.
-  intro DMEQ. destruct hf.
-  - constructor; auto.
-  - constructor; auto.
-Abort. (* theorem not true !! *)
-
 Theorem hsstate_simu_core_correct dm f ctx hst1 hst2:
   hsstate_simu_core dm f hst1 hst2 ->
   hok (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 ->
@@ -581,11 +620,11 @@ Proof.
   destruct HREF1 as (SREF1 & DREF1 & FREF1). destruct HREF2 as (SREF2 & DREF2 & FREF2).
   assert (PCEQ: dm ! (hsi_pc hst2) = Some (hsi_pc hst1)) by apply SCORE.
   eapply hsistate_simu_core_correct in SCORE; [|eassumption].
+  eapply hfinal_simu_core_correct in FSIMU; eauto.
   constructor; [apply SCORE; auto|].
-(*   rewrite <- FREF1. rewrite <- FREF2. rewrite FSIMU. (* FIXME - not that simple *)
-  apply sfval_simu_reflexive.
-  destruct SREF1 as (PC1 & _). destruct SREF2 as (PC2 & _). congruence. *)
-Admitted.
+  destruct SREF1 as (PC1 & _). destruct SREF2 as (PC2 & _). rewrite <- PC1. rewrite <- PC2.
+  eapply FSIMU.
+Qed.
 
 Lemma hsistate_refines_stat_pceq st hst:
   hsistate_refines_stat hst st ->
@@ -1077,35 +1116,6 @@ Qed.
 
 (** * The simulation test of concrete symbolic execution *)
 
-(* TODO - generalize it with a list of registers to test ? *)
-Definition hsilocal_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate_local) := OK tt.
-
-(* (* TODO: voilà les conditions que hsilocal_simub doit garantir *)
-Definition hsilocal_simu_core (hst1 hst2: hsistate_local):=
-    forall sm, List.In sm (hsi_lsmem hst2) -> List.In sm (hsi_lsmem hst1)
- /\ forall sv, List.In sv (hsi_ok_lsval hst2) -> List.In sv (hsi_ok_lsval hst1)
- /\ forall r, hsi_sreg_get hst2 r = hsi_sreg_get hst1 r.
-
-*)
-
-Definition hsilocal_simu dm f (hst1 hst2: hsistate_local) (ctx: simu_proof_context f): Prop := forall st1 st2,
-  hsilocal_refines (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 st1 ->
-  hsilocal_refines (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst2 st2 ->
-  silocal_simu dm f st1 st2 ctx. 
-
-Lemma hsilocal_simub_correct dm f hst1 hst2:
-  hsilocal_simub dm f hst1 hst2 = OK tt ->
-  forall ctx, hsilocal_simu dm f hst1 hst2 ctx.
-Proof.
-Admitted.
-
-Lemma hsilocal_simub_eq dm f hsl1 hsl2:
-  hsilocal_simub dm f hsl1 hsl2 = OK tt ->
-     hsi_sreg_get (hsi_sreg hsl1) = hsi_sreg_get (hsi_sreg hsl2) (* FIXME: a bit too strong ? *)
-  /\ hsi_smem_get (hsi_lsmem hsl1) = hsi_smem_get (hsi_lsmem hsl2).
-Proof.
-Admitted.
-
 Definition revmap_check_single (dm: PTree.t node) (n tn: node) : res unit :=
   match dm ! tn with
   | None => Error (msg "revmap_check_single: no mapping for tn")
@@ -1234,154 +1244,8 @@ Proof.
     congruence.
 Qed.
 
-Definition hsiexit_simub (dm: PTree.t node) (f: RTLpath.function) (hse1 hse2: hsistate_exit) :=
-  if (eq_condition (hsi_cond hse1) (hsi_cond hse2)) then
-    do _ <- list_sval_simub (hsi_scondargs hse1) (hsi_scondargs hse2);
-    do _ <- hsilocal_simub dm f (hsi_elocal hse1) (hsi_elocal hse2);
-    revmap_check_single dm (hsi_ifso hse1) (hsi_ifso hse2)
-  else Error (msg "siexit_simub: conditions do not match")
-.
-
-(* Definition hsiexit_simu dm f hse1 hse2 (ctx: simu_proof_context f): Prop := forall se1 se2,
-  hsiexit_refines_stat hse1 se1 ->
-  hsiexit_refines_stat hse2 se2 ->
-  hsiexit_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse1 se1 ->
-  hsiexit_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hse2 se2 ->
-  siexit_simu dm f ctx se1 se2. *)
-
 Local Hint Resolve genv_match ssem_local_refines_hok: core.
 
-Lemma hsiexit_simub_correct dm f hse1 hse2:
-  hsiexit_simub dm f hse1 hse2 = OK tt ->
-  forall ctx, hsiexit_simu dm f ctx hse1 hse2.
-Proof.
-(*   unfold hsiexit_simub. intro. explore.
-  apply list_sval_simub_correct in EQ0. exploit hsilocal_simub_eq; eauto.
-  intros (SREGEQ & SMEMEQ) ctx.
-  eapply hsilocal_simub_correct in EQ2.
-  apply revmap_check_single_correct in EQ3.
-  intros se1 se2 HIFSO1 HIFSO2 (HLREF1 & HCOND1) (HLREF2 & HCOND2).
-  unfold hsiexit_refines_stat in *.
-  intros is1 (SCOND & SLOCAL & SIFSO).
-  constructor.
-  - rewrite <- HCOND1; eauto.
-    rewrite <- HCOND2; eauto.
-    rewrite SMEMEQ, EQ0, e. 
-    eapply seval_condition_preserved; eauto.
-    assert (X: hsok_local (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (hsi_elocal hse1) -> 
-                 hsok_local (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) (hsi_elocal hse2)).
-    + admit. (* TODO: on doit savoir ça du fait que l'état symbolique de hse2 simule celui de hse1 *)
-    + eauto.
-  - let H0 := fresh "SLOCAL" in assert (H0 := SLOCAL).
-    eapply EQ2 in SLOCAL0; eauto. destruct SLOCAL0 as (is2 & SLOCAL' & ISIMU).
-    destruct is2 as [icont ipc irs imem]. simpl in *.
-    exists (mk_istate icont (si_ifso se2) irs imem). simpl.
-    constructor; auto.
-    + repeat (constructor; auto).
-      rewrite <- HCOND2; eauto.
-      rewrite <- e, <- EQ0, <- SMEMEQ.
-      erewrite seval_condition_preserved; eauto.
-      rewrite HCOND1; eauto.
-    + unfold istate_simu in *. destruct (icontinue is1) eqn:ICONT.
-      * destruct ISIMU as (A & B & C). constructor; auto.
-      * destruct ISIMU as (path & PATHEQ & ISIMU & REVEQ). exists path.
-        repeat (constructor; auto). simpl in *. congruence. *)
-Admitted.
-
-Fixpoint hsiexits_simub (dm: PTree.t node) (f: RTLpath.function) (lhse1 lhse2: list hsistate_exit) :=
-  match lhse1 with
-  | nil =>
-      match lhse2 with
-      | nil => OK tt
-      | _ => Error (msg "siexists_simub: sle1 and sle2 lengths do not match")
-      end
-  | hse1 :: lhse1 =>
-      match lhse2 with
-      | nil => Error (msg "siexits_simub: sle1 and sle2 lengths do not match")
-      | hse2 :: lhse2 =>
-          do _ <- hsiexit_simub dm f hse1 hse2;
-          do _ <- hsiexits_simub dm f lhse1 lhse2;
-          OK tt
-      end
-  end.
-
-Lemma hsiexits_simub_correct dm f ctx lhse1: forall lhse2,
-  hsiexits_simub dm f lhse1 lhse2 = OK tt ->
-  hsiexits_simu dm f ctx lhse1 lhse2.
-Proof.
-(*   induction lhse1.
-  - simpl. intros. destruct lhse2; try discriminate. intros se1 se2 HEREFS1 HEREFS2 _ _.
-    inv HEREFS1. inv HEREFS2. constructor.
-  - (* simpl. *) unfold hsiexits_simub. intros. destruct lhse2; try discriminate. explore.
-    fold hsiexits_simub in EQ1.
-    eapply hsiexit_simub_correct in EQ. apply IHlhse1 in EQ1.
-    intros se1 se2 HEREFS1 HEREFS2 HEREFD1 HEREFD2. inv HEREFS1. inv HEREFS2. inv HEREFD1. inv HEREFD2. constructor; auto.
-    apply EQ1; assumption. *)
-Admitted.
-
-Definition hsistate_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsistate) :=
-  do _ <- hsilocal_simub dm f (hsi_local hst1) (hsi_local hst2);
-  do _ <- hsiexits_simub dm f (hsi_exits hst1) (hsi_exits hst2);
-  OK tt.
-
-(* Definition hsistate_simu dm f (hst1 hst2: hsistate) (ctx: simu_proof_context f): Prop := forall st1 st2,
-  hsistate_refines_stat hst1 st1 ->
-  hsistate_refines_stat hst2 st2 ->
-  hsistate_refines_dyn (the_ge1 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst1 st1 ->
-  hsistate_refines_dyn (the_ge2 ctx) (the_sp ctx) (the_rs0 ctx) (the_m0 ctx) hst2 st2 ->
-  sistate_simu dm f st1 st2 ctx. *)
-
-
-
-
-
-
-
-
-
-(* Very adapted from sistate_simub_correct ---> should delete sistate_simub_correct after *)
-Lemma hsistate_simub_correct dm f hst1 hst2:
-  hsistate_simub dm f hst1 hst2 = OK tt ->
-  forall ctx, hsistate_simu dm f hst1 hst2 ctx.
-Proof.
-(*   unfold hsistate_simub. intro. explore. unfold hsistate_simu.
-  intros ctx st1 st2 (PCEQ1 & HEREFD1) (PCEQ2 & HEREFD2) (HREF1 & HLREF1) (HREF2 & HLREF2) is1 SEMI.
-  exploit hsiexits_simub_correct; eauto. intro ESIMU.
-  unfold ssem_internal in SEMI. destruct (icontinue _) eqn:ICONT.
-  - destruct SEMI as (SSEML & PCEQ & ALLFU).
-    exploit hsilocal_simub_correct; eauto. intros (is2 & SSEML' & ISIMU).
-    destruct is2 as [icont2 ipc2 irs2 imem2]. simpl in *.
-    exists (mk_istate icont2 (si_pc st2) irs2 imem2). constructor; auto.
-    + unfold ssem_internal. simpl.
-      unfold istate_simu in ISIMU. rewrite ICONT in ISIMU.
-      destruct ISIMU as (CONTEQ & RSEQ & MEMEQ). simpl in *.
-      rewrite <- CONTEQ. rewrite ICONT.
-      constructor; [|constructor]; [eassumption | auto | eapply siexits_simu_all_fallthrough; eauto].
-    + unfold istate_simu in *; simpl in *. rewrite ICONT in ISIMU. rewrite ICONT.
-      destruct ISIMU as (A & B & C). simpl in *. constructor; auto.
-  - destruct SEMI as (ext & lx & SSEME & ALLFU).
-    exploit siexits_simu_all_fallthrough_upto; eauto. intros (ext2 & lx2 & ALLFU2 & LENEQ).
-    assert (EXTSIMU: siexit_simu dm f ctx ext ext2). {
-      eapply list_forall2_nth_error; eauto.
-      - destruct ALLFU as (ITAIL & _). eapply is_tail_nth_error; eauto.
-      - destruct ALLFU2 as (ITAIL & _). eapply is_tail_nth_error in ITAIL.
-        assert (LENEQ': length (si_exits st1) = length (si_exits st2)) by (eapply list_forall2_length; eauto).
-        congruence. } *)
-Admitted.
-(*
-    destruct EXTSIMU as (SEMSIMU & _). eapply SEMSIMU in SSEME; eauto.
-    destruct SSEME as (is2 & SSEME2 & ISIMU).
-    unfold istate_simu in ISIMU. rewrite ICONT in ISIMU. destruct ISIMU as (path & PATHEQ & SIMULIVE & REVBIND).
-    destruct SIMULIVE as (CONTEQ & REGLIVE & MEMEQ).
-    unfold ssem_internal. exists is2.
-    rewrite <- CONTEQ. rewrite ICONT. constructor; auto.
-    + eexists; eexists; constructor; eauto.
-    + unfold istate_simu. rewrite ICONT. eexists. repeat (constructor; eauto).
-Qed.
-*)
-
-
-
 Fixpoint revmap_check_list (dm: PTree.t node) (ln ln': list node): res unit :=
   match ln with
   | nil =>
@@ -1640,25 +1504,6 @@ Proof.
     + constructor; auto.
 Admitted.
 
-Definition hsstate_simub (dm: PTree.t node) (f: RTLpath.function) (hst1 hst2: hsstate) :=
-  do u1 <- hsistate_simub dm f (hinternal hst1) (hinternal hst2);
-  do u2 <- sfval_simub dm f (hsi_pc hst1) (hsi_pc hst2) (hfinal hst1) (hfinal hst2);
-  OK tt.
-
-Lemma hsstate_simub_correct dm f hst1 hst2 ctx:
-  hsstate_simub dm f hst1 hst2 = OK tt ->
-  hsstate_simu dm f hst1 hst2 ctx.
-Proof.
-  unfold hsstate_simub. intro. explore.
-  eapply sfval_simub_correct in EQ1. eapply hsistate_simub_correct in EQ.
-  intros st1 st2 (SREF1 & LREF1 & FREF1) (SREF2 & LREF2 & FREF2).
-  constructor; [eauto |].
-  destruct SREF1 as (PCEQ1 & _ ). destruct SREF2 as (PCEQ2 & _ ).
-  rewrite <- PCEQ1. rewrite <- PCEQ2. rewrite <- FREF1. rewrite <- FREF2.
-  eauto.
-  (* FIXME - that proof will have to be changed once hfinal_refines is more complex *)
-Qed.
-
 Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) (m: node * node) :=
   let (pc2, pc1) := m in
   match (hsexec f pc1) with
@@ -1666,7 +1511,7 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa
   | Some hst1 =>
       match (hsexec tf pc2) with
       | None => Error (msg "simu_check_single: hsexec tf pc2 failed")
-      | Some hst2 => hsstate_simub dm f hst1 hst2
+      | Some hst2 => hsstate_simu_coreb dm f hst1 hst2
       end
   end.
 
@@ -1685,8 +1530,10 @@ Proof.
   intros (st0 & SEXEC1 & REF1).
   rewrite SEXEC1 in SEXEC; inversion SEXEC; subst.
   eexists; split; eauto.
-  intros; eapply hsstate_simub_correct; eauto.
-Qed.
+  intros ctx. eapply hsstate_simu_coreb_correct in H.
+  eapply hsstate_simu_core_correct; eauto.
+  (* TODO - Needs a sok in _theory.v, and a sok -> hok lemma *)
+Admitted.
 
 Fixpoint simu_check_rec (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpath.function) lm :=
   match lm with