Merge pull request #6 from alxest/mlepriv

Add MLEPRIV in after_external case
snu-sf · Mar 26, 2020 · 1bf2113 · 1bf2113
2 parents 829f24a + 363b805
commit 1bf2113
Show file tree

Hide file tree

Showing 13 changed files with 31 additions and 11 deletions.
diff --git a/.travis.yml b/.travis.yml
@@ -4,7 +4,6 @@ cache:
   apt: true
   directories:
   - $HOME/.opam
-  - $TRAVIS_BUILD_DIR/CompCertR
 addons:
   apt:
     sources:
@@ -36,12 +35,10 @@ install:
   - opam install -y --verbose -j ${NJOBS} menhir.${MENHIR} && opam pin add menhir ${MENHIR} -y
   - opam repo add coq-released https://coq.inria.fr/opam/released
   - opam install -y --verbose -j ${NJOBS} coq-paco.${PACO} && opam pin add coq-paco ${PACO} -y
-  - if [ ! -d "./CompCertR" ];
-    then
-      git clone ${COMPCERTR} CompCertR;
-    fi
+  - rm -rf ./CompCertR
+  - git clone ${COMPCERTR} CompCertR;
   - cd CompCertR
-  - git reset --hard origin/${BRANCH}
+  - git checkout origin/${BRANCH}
   - ./configure ${ARCHI}
   - make -j ${NJOBS}
 
@@ -52,5 +49,6 @@ script:
   - rm -rf CompCertM
   - git clone https://github.com/$TRAVIS_REPO_SLUG.git CompCertM
   - cd CompCertM
-  - git checkout $TRAVIS_COMMIT
+  - git fetch origin +refs/pull/*/merge:refs/remotes/origin/pr/*
+  - git checkout -qf $TRAVIS_COMMIT
   - make -j ${NJOBS}
diff --git a/backend/StackingproofC.v b/backend/StackingproofC.v
@@ -945,6 +945,8 @@ Proof.
   - eapply wt_state_local_preservation; eauto.
     eapply wt_prog; eauto.
   - inv FOOT. inv MLEEXCL. rewrite RSP in *. clarify. des. clarify. eapply SimMemInjC.foot_excl; et.
+  - inv EXCL. inv MLEEXCL. econs; ss; eauto.
+    inv MWF. eapply frozen_shortened; eauto with xomega.
   - (* init bsim *)
     { inv INITTGT. inv STORE. folder. inv SIMARGS; ss.
       exploit functions_translated_inject; eauto.

diff --git a/demo/mutrec/IdSimAsmIdInv.v b/demo/mutrec/IdSimAsmIdInv.v
@@ -423,6 +423,7 @@ Proof.
       exists (SimMemInjInvC.unlift' sm_arg sm_ret).
       eexists. eexists (AsmC.mkstate _ (Asm.State _ _)). esplits; eauto.
       - etrans; eauto.
+      - clear - MLE0. inv MLE0. inv MLE. ss. econs; ss; eauto. eapply SimMemInj.frozen_refl.
       - i. esplits; eauto.
         + econs 2; eauto.
         + exploit SimMemInjInvC.unlift_wf; try apply MLE0; eauto. i. inv MLE2.

diff --git a/demo/mutrec/MutrecAproof.v b/demo/mutrec/MutrecAproof.v
@@ -717,6 +717,7 @@ Proof.
   { i. eapply SoundTop.sound_state_local_preservation. }
   { i. eapply Preservation.local_preservation_noguarantee_weak; eauto. eapply SoundTop.sound_state_local_preservation. }
   { ii; ss. r. etrans; eauto. }
+  { ii. eauto. }
   i. ss. esplits; eauto.
 
   - i. des. inv SAFESRC.

diff --git a/demo/mutrec/MutrecBproof.v b/demo/mutrec/MutrecBproof.v
@@ -1172,6 +1172,7 @@ Proof.
   { i. eapply SoundTop.sound_state_local_preservation. }
   { i. eapply Preservation.local_preservation_noguarantee_weak; eauto. eapply SoundTop.sound_state_local_preservation. }
   { ii; ss. r. etrans; eauto. }
+  { ii. eauto. }
   i. ss. esplits; eauto.
 
   - i. des. inv SAFESRC. instantiate (1:=unit).

diff --git a/demo/unreadglob/IdSimAsmDropInv.v b/demo/unreadglob/IdSimAsmDropInv.v
@@ -402,6 +402,7 @@ Proof.
       exists (SimMemInjInvC.unlift' sm_arg sm_ret).
       eexists. eexists (AsmC.mkstate _ (Asm.State _ _)). esplits; eauto.
       - etrans; eauto.
+      - clear - MLE0. inv MLE0. inv MLE. ss. econs; ss; eauto. eapply SimMemInj.frozen_refl.
       - i. esplits; eauto.
         + econs 2; eauto.
         + exploit SimMemInjInvC.unlift_wf; try apply MLE0; eauto. i. inv MLE2.

diff --git a/demo/unreadglob/IdSimInvExtra.v b/demo/unreadglob/IdSimInvExtra.v
@@ -163,7 +163,8 @@ Lemma Mem_unfree_parallel
                        (Ptrofs.unsigned ofs_tgt) (Ptrofs.unsigned ofs_tgt + sz)
                      = Some sm1.(SimMem.tgt)>>)
       /\ (<<MWF: SimMem.wf sm1>>)
-      /\ (<<MLE: SimMem.le sm0 sm1>>).
+      /\ (<<MLE: SimMem.le sm0 sm1>>)
+      /\ (<<MLEPRIV: SimMem.lepriv sm_ret sm1>>).
 Proof.
   ss.
   destruct sm0 as [sm0 mem_inv_src0 mem_inv_tgt0].
@@ -308,6 +309,7 @@ Proof.
         * ii. eapply MAXTGT0; eauto.
           unfold Mem.valid_block in *. erewrite Mem.nextblock_free; eauto.
         * eapply Mem.unchanged_on_nextblock; eauto.
+    - econs; ss; eauto; try by congruence. eapply SimMemInj.frozen_refl.
   }
   Unshelve. apply 0.
 Qed.

diff --git a/proof/MatchSimModSemExcl2.v b/proof/MatchSimModSemExcl2.v
@@ -103,7 +103,7 @@ Section MATCHSIMFORWARD.
       (MWFAFTR: SimMem.wf (SimMemLift.unlift sm_arg sm_ret))
       (MLEAFTR: SimMem.le sm_arg (SimMemLift.unlift sm_arg sm_ret)),
       exists sm_after idx1 st_tgt1,
-        (<<MLE: SimMem.le sm0 sm_after>>) /\
+        (<<MLE: SimMem.le sm0 sm_after>>) /\ (<<MLEPRIV: SimMem.lepriv sm_ret sm_after>>) /\
         forall (MLE: SimMem.le sm0 sm_after) (* helper *),
           ((<<AFTERTGT: ms_tgt.(ModSem.after_external) st_tgt0 retv_tgt st_tgt1>>) /\
            (<<MATCH: match_states idx1 st_src1 st_tgt1 sm_after>>)).
@@ -184,7 +184,7 @@ Section MATCHSIMFORWARD.
         { econs; eauto. }
         { eapply SimMemLift.unlift_wf; eauto. }
         { eapply SimMemLift.lift_spec; eauto. }
-        i; des. spc H1. des. esplits; eauto. right. eapply CIH; eauto.
+        i; des. spc H0. des. esplits; eauto. right. eapply CIH; eauto.
         { eapply ModSemPair.mfuture_preserves_sim_skenv; try apply SIMSKENV; eauto.
           apply rtc_once. left. et.
         }

diff --git a/proof/SimModSem.v b/proof/SimModSem.v
@@ -93,6 +93,7 @@ Section SIMMODSEM.
                 exists st_tgt1 sm_after i1,
                   (<<AFTERTGT: ms_tgt.(after_external) st_tgt0 retv_tgt st_tgt1>>) /\
                   (<<MLEPUB: SimMem.le sm0 sm_after>>) /\
+                  (<<MLEPRIV: SimMem.lepriv sm_ret sm_after>>) /\
                   (<<LXSIM: lxsim i1 st_src1 st_tgt1 sm_after>>)>>))>>)
 
   | lxsim_final

diff --git a/proof/SimModSemLift.v b/proof/SimModSemLift.v
@@ -190,6 +190,8 @@ Context {SMLIFT: SimMemLift.class SM}.
           (MLEEXCL: (mle_excl st_at_src st_at_tgt) sm1 sm2)
           (MLE: SimMem.le sm0 sm1),
           <<MLE: SimMem.le sm0 sm2>>)
+      (EXCLPRIV: forall st_init_src st_init_tgt sm0 sm1 (MWF: SimMem.wf sm0),
+          mle_excl st_init_src st_init_tgt sm0 sm1 -> SimMem.lepriv sm0 sm1)
       (SIM: forall
           sm_arg args_src args_tgt
           sg_init_src sg_init_tgt
@@ -238,6 +240,8 @@ Section IMPLIES.
             (MLEEXCL: (mle_excl st_at_src st_at_tgt) sm1 sm2)
             (MLE: SimMem.le sm0 sm1),
             <<MLE: SimMem.le sm0 sm2>>)
+        (EXCLPRIV: forall st_init_src st_init_tgt sm0 sm1 (MWF: SimMem.wf sm0),
+            mle_excl st_init_src st_init_tgt sm0 sm1 -> SimMem.lepriv sm0 sm1)
         (SIM: lxsimL ms_src ms_tgt sound_state has_footprint mle_excl idx_init st_init_src st_init_tgt sm_init):
       <<SIM: SimModSem.lxsim ms_src ms_tgt sound_state idx_init st_init_src st_init_tgt sm_init>>.
   Proof.
@@ -262,6 +266,11 @@ Section IMPLIES.
       eexists _, sm_after.
       esplits; eauto.
       { eapply FOOTEXCL; et. etrans; et. eapply SimMemLift.lift_spec; et. }
+      { etrans.
+        - eapply SimMemLift.unlift_priv with (sm_at := sm_arg); eauto.
+          eapply SimMemLift.lift_priv; eauto.
+        - eapply EXCLPRIV; eauto. eapply SimMemLift.unlift_wf; eauto.
+      }
     - econs 4; et.
   Qed.
 

diff --git a/proof/SimModSemSR.v b/proof/SimModSemSR.v
@@ -146,6 +146,7 @@ Section SIMMODSEM.
                 exists st_tgt1 sm_after i1,
                   (<<AFTERTGT: ms_tgt.(after_external) st_tgt0 retv_tgt st_tgt1>>) /\
                   (<<MLE: SimMem.le sm0 sm_after>>) /\
+                  (<<MLEPRIV: SimMem.lepriv sm_ret sm_after>>) /\
                   (<<LXSIMSR: lxsimSR i1 st_src1 st_tgt1 sm_after>>)>>))>>)
 
   | lxsimSR_final

diff --git a/selfsim/IdSimAsm.v b/selfsim/IdSimAsm.v
@@ -1607,6 +1607,7 @@ Proof.
       exists (SimMemInj.unlift' sm_arg sm_ret).
       eexists. eexists (AsmC.mkstate _ (Asm.State _ _)). esplits; eauto.
       - etrans; eauto.
+      - clear - MLE0. inv MLE0. ss. econs; ss; eauto. eapply SimMemInj.frozen_refl.
       - i. esplits; eauto.
         + econs 2; eauto.
         + exploit SimMemInj.unlift_wf; try apply MLE0; eauto. i. inv MLE2.

diff --git a/selfsim/IdSimAsmExtra.v b/selfsim/IdSimAsmExtra.v
@@ -230,7 +230,8 @@ Section MEMORYLEMMA.
                          (Ptrofs.unsigned ofs_tgt) (Ptrofs.unsigned ofs_tgt + sz)
                        = Some sm1.(SimMemInj.tgt)>>)
         /\ (<<MWF: SimMemInj.wf' sm1>>)
-        /\ (<<MLE: SimMemInj.le' sm0 sm1>>).
+        /\ (<<MLE: SimMemInj.le' sm0 sm1>>)
+        /\ (<<MLEPRIV: SimMemInjC.lepriv sm_ret sm1>>).
   Proof.
     assert (DELTA0: SimMemInj.inj sm_ret blk_src = Some (blk_tgt, delta)).
     { inv MLE0. inv MLE1. ss. eapply INCR0. eapply INCR. eauto. }
@@ -314,6 +315,7 @@ Section MEMORYLEMMA.
         + eapply Mem_unfree_perm_restore; try apply UNFREE; eauto.
           * ii. eapply MAXTGT0; eauto. unfold Mem.valid_block in *. erewrite Mem.nextblock_free; eauto.
           * eapply Mem.unchanged_on_nextblock; eauto.
+      - econs; ss; eauto; try by congruence. eapply SimMemInj.frozen_refl.
     }
   Qed.