Merge branch 'mppa-RTLpathSE-verif_Op_mem-irrel' into mppa-RTLpathSE-xverif

1 files changed, 29 insertions, 30 deletions

diff --git a/kvx/lib/RTLpathSE_impl.v b/kvx/lib/RTLpathSE_impl.v
index bf854c97..a2939cba 100644
--- a/kvx/lib/RTLpathSE_impl.v
+++ b/kvx/lib/RTLpathSE_impl.v
@@ -57,7 +57,9 @@ Definition hsok_local ge sp rs0 m0 (hst: hsistate_local) : Prop :=
 Definition hsilocal_refines ge sp rs0 m0 (hst: hsistate_local) (st: sistate_local) :=
       (sok_local ge sp rs0 m0 st <-> hsok_local ge sp rs0 m0 hst) 
   /\  (hsok_local ge sp rs0 m0 hst -> seval_smem ge sp hst.(hsi_smem) rs0 m0 = seval_smem ge sp st.(si_smem) rs0 m0)
-  /\  (hsok_local ge sp rs0 m0 hst -> forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0).
+  /\  (hsok_local ge sp rs0 m0 hst -> forall r, hsi_sreg_eval ge sp hst r rs0 m0 = seval_sval ge sp (si_sreg st r) rs0 m0)
+  /\  (forall m b ofs, seval_smem ge sp st.(si_smem) rs0 m0 = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs)
+  .
 
 Lemma ssem_local_refines_hok ge sp rs0 m0 hst st rs m:
   ssem_local ge sp st rs0 m0 rs m -> hsilocal_refines ge sp rs0 m0 hst st -> hsok_local ge sp rs0 m0 hst.
@@ -143,7 +145,7 @@ Proof.
   destruct of as [alive |].
   - constructor.
     + constructor; [assumption | constructor; [assumption|]].
-      destruct HREF2 as (B & _ & A).
+      destruct HREF2 as (B & _ & A & _).
       (** B is used for the auto below. *)
       assert (forall r : positive, hsi_sreg_eval ge2 sp hst2 r rs0 m0 = seval_sval ge2 sp (si_sreg st2 r) rs0 m0) by auto.
       intro r. rewrite <- H. clear H. 
@@ -154,7 +156,7 @@ Proof.
       unfold seval_sval_partial. generalize HOK2; rewrite <- B; intros (_ & _ & C) D.
       assert (seval_sval ge2 sp s rs0 m0 <> None) by congruence.
       destruct (seval_sval ge2 sp s rs0 m0); [reflexivity | contradiction].
-    + intros r ALIVE. destruct HREF2 as (_ & _ & A). destruct HREF1 as (_ & _ & B).
+    + intros r ALIVE. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _).
       destruct CORE as (_ & C & _). rewrite seval_partial_regset_get.
       assert (OPT: forall (x y: val), Some x = Some y -> x = y) by congruence.
       destruct (hst2 ! r) eqn:HST2; apply OPT; clear OPT.
@@ -174,7 +176,7 @@ Proof.
       rewrite <- MEMEQ2; auto. rewrite <- MEMEQ3.
       erewrite smem_eval_preserved; [| eapply GFS].
       rewrite MEMEQ1; auto.
-    + intro r. destruct HREF2 as (_ & _ & A). destruct HREF1 as (_ & _ & B).
+    + intro r. destruct HREF2 as (_ & _ & A & _). destruct HREF1 as (_ & _ & B & _).
       destruct CORE as (_ & C & _). rewrite <- A; auto. rewrite hsi_sreg_eval_correct.
       rewrite C; [|auto]. erewrite seval_preserved; [| eapply GFS]. rewrite <- hsi_sreg_eval_correct.
       rewrite B; auto.
@@ -910,12 +912,13 @@ Qed.
 
 Lemma hslocal_set_mem_correct ge sp rs0 m0 hst st hsm sm:
   (seval_smem ge sp (hsi_smem hst) rs0 m0 = None -> seval_smem ge sp hsm rs0 m0 = None) ->
+  (forall m b ofs, seval_smem ge sp sm rs0 m0 = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) ->
   hsilocal_refines ge sp rs0 m0 hst st ->
   (hsok_local ge sp rs0 m0 hst -> seval_smem ge sp hsm rs0 m0 = seval_smem ge sp sm rs0 m0) ->
   hsilocal_refines ge sp rs0 m0 (hslocal_set_smem hst hsm) (slocal_set_smem st sm).
 Proof.
-  intros PRESERV (OKEQ & SMEMEQ' & REGEQ) SMEMEQ.
-  split; rewrite! hsok_local_set_mem; eauto; try tauto.
+  intros PRESERV SMVALID (OKEQ & SMEMEQ' & REGEQ & MVALID) SMEMEQ.
+  split; rewrite! hsok_local_set_mem; simpl; eauto; try tauto.
   rewrite sok_local_set_mem.
   intuition congruence.
 Qed.
@@ -1009,20 +1012,17 @@ Definition simplify (rsv: root_sval) lsv sm: sval :=
   | Rop op =>
      match is_move_operation op lsv with
      | Some arg => arg  (* optimization of Omove *)
-     | None => 
-       if op_depends_on_memory op then
-          rsv lsv sm
-       else
-          Sop op (list_sval_inj lsv) Sinit (* magically remove the dependency on sm ! *)
+     | None => Sop op (list_sval_inj lsv) Sinit (* magically remove the dependency on sm ! *)
      end
   | _ => rsv lsv sm
   end.
 
 Lemma simplify_correct (rsv: root_sval) lsv sm (ge: RTL.genv) (sp:val) (rs0: regset) (m0: mem) v:
+  (forall m b ofs, seval_smem ge sp sm rs0 m0 = Some m -> Mem.valid_pointer m b ofs = Mem.valid_pointer m0 b ofs) ->
   seval_sval ge sp (rsv lsv sm) rs0 m0 = Some v ->
   seval_sval ge sp (simplify rsv lsv sm) rs0 m0 = Some v.
 Proof.
-  destruct rsv; simpl; auto.
+  intros MVALID; destruct rsv; simpl; auto.
   - (* Rop *)
     destruct (seval_list_sval _ _ _ _) as [args|] eqn: Hargs; try congruence.
     destruct (seval_smem _ _ _ _) as [m|] eqn: Hm; try congruence.
@@ -1031,9 +1031,9 @@ Proof.
     + exploit is_move_operation_correct; eauto.
       intros (Hop & Hlsv); subst; simpl in *.
       explore. auto.
-    + clear Hmove; destruct (op_depends_on_memory op) eqn: Hop; simpl; explore; try congruence.
+    + clear Hmove; simpl; explore; try congruence.
       inversion Hargs; subst.
-      erewrite op_depends_on_memory_correct; eauto.
+      erewrite <- op_valid_pointer_eq; eauto.
   - (* Rload *)
     destruct trap; simpl; auto.
     destruct (seval_list_sval _ _ _ _) as [args|] eqn: Hargs; try congruence.
@@ -1062,16 +1062,6 @@ Proof.
   - rewrite PTree.gro, PTree.gso; simpl; auto.
 Qed.
 
-(* naive version:
-@Cyril: éventuellement, tu peux utiliser la version naive dans un premier temps pour simplifier les preuves...
-
-Definition naive_hslocal_set_sreg (hst:hsistate_local) (r:reg) (rsv:root_sval) lsv sm :=
-  let sv := rsv lsv sm in
-  {| hsi_lsmem := hsi_lsmem hst;
-     hsi_ok_lsval := sv::(hsi_ok_lsval hst);
-     hsi_sreg:= PTree.set r sv (hsi_sreg hst) |}.
-*)
-
 Definition hslocal_set_sreg (hst:hsistate_local) (r:reg) (rsv:root_sval) lsv :=
   {| hsi_smem := hsi_smem hst;
      hsi_ok_lsval := if may_trap rsv lsv (hsi_smem hst) then (rsv lsv (hsi_smem hst))::(hsi_ok_lsval hst) else hsi_ok_lsval hst;
@@ -1112,11 +1102,12 @@ Lemma hslocal_set_sreg_correct ge sp rs0 m0 hst st r (rsv:root_sval) lsv sv':
   (hsok_local ge sp rs0 m0 hst -> seval_sval ge sp sv' rs0 m0 = seval_sval ge sp (rsv lsv (hsi_smem hst)) rs0 m0) ->
   hsilocal_refines ge sp rs0 m0 (hslocal_set_sreg hst r rsv lsv) (slocal_set_sreg st r sv').
 Proof.
-  intros (ROK & RMEM & RVAL) OKA RSV.
+  intros (ROK & RMEM & RVAL & MVALID) OKA RSV.
   unfold hsilocal_refines; simpl. rewrite! hsok_local_set_sreg; eauto. split.
   + rewrite <- ROK in RSV; rewrite sok_local_set_sreg; eauto.
     intuition congruence.
-  + split; try tauto.
+  + split. { try tauto. }
+    split. 2: { try tauto. }
     intros (HOKL & RSV2) r0.
     rewrite red_PTree_set_correct.
     rewrite hsi_sreg_eval_correct. unfold hsi_sreg_get.
@@ -1124,6 +1115,7 @@ Proof.
     * subst. rewrite PTree.gss, RSV; auto.
       destruct (seval_sval ge sp (rsv lsv (hsi_smem hst))) eqn: RSV3; simpl; try congruence.
       eapply simplify_correct; eauto.
+      intros m b ofs; rewrite RMEM; eauto.
     * intros; rewrite PTree.gso; auto.
       rewrite <- RVAL, hsi_sreg_eval_correct; auto.
 Qed.
@@ -1165,7 +1157,7 @@ Lemma seval_sval_refines ge sp rs0 m0 hst st p:
   hsilocal_refines ge sp rs0 m0 hst st ->
   seval_sval ge sp (hsi_sreg_get hst p) rs0 m0 = seval_sval ge sp (si_sreg st p) rs0 m0.
 Proof.
-  intros OKL HREF. destruct HREF as (_ & _ & RSEQ).
+  intros OKL HREF. destruct HREF as (_ & _ & RSEQ & _).
   rewrite <- hsi_sreg_eval_correct; eauto.
 Qed.
 
@@ -1175,7 +1167,7 @@ Lemma seval_list_sval_refines ge sp rs0 m0 hst st l:
   seval_list_sval ge sp (list_sval_inj (map (hsi_sreg_get hst) l)) rs0 m0 =
   seval_list_sval ge sp (list_sval_inj (map (si_sreg st) l)) rs0 m0.
 Proof.
-  intros OKL HLREF. destruct HLREF as (_ & _ & RSEQ).
+  intros OKL HLREF. destruct HLREF as (_ & _ & RSEQ & _).
   induction l; simpl; auto.
   erewrite <- RSEQ; auto.
   rewrite IHl. 
@@ -1198,7 +1190,7 @@ Lemma seval_condition_refines hst st ge sp cond args rs m:
   seval_condition ge sp cond args (hsi_smem hst) rs m
   = seval_condition ge sp cond args (si_smem st) rs m.
  Proof.
-  intros HOK (OKEQ & MEMEQ & RSEQ). unfold seval_condition.
+  intros HOK (_ & MEMEQ & _). unfold seval_condition.
   rewrite <- MEMEQ; auto.
 Qed.
 
@@ -1267,6 +1259,12 @@ Proof.
     eapply hsist_set_local_correct_dyn; eauto.
     + eapply hslocal_set_mem_correct; eauto.
       * simpl. simplify_SOME x.
+      * simpl. intros m1; simplify_SOME x.
+        intros.
+        erewrite <- Mem.storev_preserv_valid; [| eauto].
+        destruct REF as (_ & LREF & _).
+        destruct LREF as (_ & _ & _ & MVALID).
+        eauto.
       * intros. simpl.
         erewrite seval_list_sval_refines; eauto.
         erewrite seval_smem_refines; eauto.
@@ -1407,7 +1405,8 @@ Proof.
   - intro. destruct H as (SVAL & SMEM). constructor; [simpl; auto|].
     constructor; simpl; discriminate.
   - intros; simpl; reflexivity.
-  - intros. unfold hsi_sreg_eval. rewrite PTree.gempty. reflexivity.
+  - split. { intros; unfold hsi_sreg_eval; rewrite PTree.gempty; reflexivity. }
+    congruence.
 Qed.
 
 Definition init_hsistate pc := {| hsi_pc := pc; hsi_exits := nil; hsi_local := init_hsistate_local |}.