Simplify MatchSimModSem

snu-sf · Oct 24, 2019 · a1ab19c · a1ab19c
1 parent c75990e
commit a1ab19c
Show file tree

Hide file tree

Showing 45 changed files with 214 additions and 280 deletions.
diff --git a/backend/AllocproofC.v b/backend/AllocproofC.v
@@ -79,7 +79,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
 Inductive match_states
-          (sm_init: SimMem.t)
           (idx: nat) (st_src0: RTL.state) (st_tgt0: LTL.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: Allocproof.match_states skenv_link tge st_src0 st_tgt0)

diff --git a/backend/CSEproofC.v b/backend/CSEproofC.v
@@ -32,7 +32,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
 Inductive match_states
-          (sm_init: SimMem.t)
           (idx: unit) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: CSEproof.match_states prog ge st_src0 st_tgt0)

diff --git a/backend/CleanupLabelsproofC.v b/backend/CleanupLabelsproofC.v
@@ -37,7 +37,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
 Inductive match_states
-          (sm_init: SimMem.t)
           (idx: nat) (st_src0 st_tgt0: Linear.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: CleanupLabelsproof.match_states st_src0 st_tgt0)
@@ -142,7 +141,7 @@ Proof.
       * right. esplits; et.
         { eapply star_refl. }
       * instantiate (1:= SimMemId.mk _ _). econs; ss.
-        
+
 Unshelve.
   all: ss; try (by econs). apply msp.
 Qed.

diff --git a/backend/ConstpropproofC.v b/backend/ConstpropproofC.v
@@ -29,7 +29,7 @@ Let ge := (SkEnv.revive (SkEnv.project skenv_link md_src.(Mod.sk)) prog).
 Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
-Inductive match_states (sm_init: SimMem.t)
+Inductive match_states
           (idx: nat) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: Constpropproof.match_states prog idx st_src0 st_tgt0)

diff --git a/backend/DeadcodeproofC.v b/backend/DeadcodeproofC.v
@@ -32,7 +32,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
 Inductive match_states
-          (sm_init: SimMem.t)
           (idx: unit) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: Deadcodeproof.match_states prog ge st_src0 st_tgt0)

diff --git a/backend/DebugvarproofC.v b/backend/DebugvarproofC.v
@@ -33,7 +33,7 @@ Let ge := (SkEnv.revive (SkEnv.project skenv_link md_src.(Mod.sk)) prog).
 Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
-Inductive match_states (sm_init: SimMem.t)
+Inductive match_states
           (idx: nat) (st_src0: Linear.state) (st_tgt0: Linear.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: Debugvarproof.match_states st_src0 st_tgt0)
@@ -176,4 +176,3 @@ Proof.
 Qed.
 
 End SIMMOD.
-
diff --git a/backend/InliningproofC.v b/backend/InliningproofC.v
@@ -34,7 +34,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
 Inductive match_states
-          (sm_init: SimMem.t)
           (idx: nat) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: Inliningproof.match_states prog skenv_link skenv_link ge st_src0 st_tgt0 sm0)

diff --git a/backend/LinearizeproofC.v b/backend/LinearizeproofC.v
@@ -38,7 +38,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
 Inductive match_states
-          (sm_init: SimMem.t)
           (idx: nat) (st_src0: LTL.state) (st_tgt0: Linear.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: Linearizeproof.match_states st_src0 st_tgt0)

diff --git a/backend/RTLgenproofC.v b/backend/RTLgenproofC.v
@@ -31,7 +31,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
 Inductive match_states
-          (sm_init: SimMem.t)
           (idx: nat * nat) (st_src0: CminorSel.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: RTLgenproof.match_states st_src0 st_tgt0)

diff --git a/backend/RenumberproofC.v b/backend/RenumberproofC.v
@@ -27,7 +27,7 @@ Let ge := (SkEnv.revive (SkEnv.project skenv_link md_src.(Mod.sk)) prog).
 Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
-Inductive match_states (sm_init: SimMem.t)
+Inductive match_states
           (idx: nat) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: Renumberproof.match_states st_src0 st_tgt0)
@@ -117,4 +117,3 @@ Proof.
 Qed.
 
 End SIMMOD.
-
diff --git a/backend/SelectionproofC.v b/backend/SelectionproofC.v
@@ -37,7 +37,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
 Inductive match_states
-          (sm_init: SimMem.t)
           (idx: nat) (st_src0: Cminor.state) (st_tgt0: CminorSel.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: Selectionproof.match_states prog skenv_link ge tge st_src0 st_tgt0)

diff --git a/backend/StackingproofC.v b/backend/StackingproofC.v
@@ -863,7 +863,6 @@ Qed.
 Local Opaque sepconj.
 
 Inductive match_states
-          (sm_init: SimMem.t)
           (idx: nat) (st_src0: Linear.state) (st_tgt0: MachC.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: Stackingproof.match_states skenv_link skenv_link ge tge st_src0 st_tgt0.(st) sm0)

diff --git a/backend/TailcallproofC.v b/backend/TailcallproofC.v
@@ -29,7 +29,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
 Inductive match_states
-          (sm_init: SimMem.t)
           (idx: nat) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: Tailcallproof.match_states st_src0 st_tgt0)

diff --git a/backend/TunnelingproofC.v b/backend/TunnelingproofC.v
@@ -35,7 +35,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
 Inductive match_states
-          (sm_init: SimMem.t)
           (idx: nat) (st_src0: LTL.state) (st_tgt0: LTL.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: Tunnelingproof.match_states st_src0 st_tgt0)
@@ -91,7 +90,7 @@ Proof.
     + econs; eauto; ss.
       * rpapply match_states_call; eauto.
         { econs; eauto.
-          - instantiate (1:= (dummy_stack (fn_sig fd) ls1)). unfold dummy_stack, dummy_function. econs; eauto. 
+          - instantiate (1:= (dummy_stack (fn_sig fd) ls1)). unfold dummy_stack, dummy_function. econs; eauto.
           - econs; eauto. }
         { eapply JunkBlock.assign_junk_block_extends; eauto. }
       * rr. ss. esplits; eauto.

diff --git a/backend/UnusedglobproofC.v b/backend/UnusedglobproofC.v
@@ -39,7 +39,6 @@ Definition msp: ModSemPair.t :=
                 sm_link.
 
 Inductive match_states
-          (sm_init: SimMem.t)
           (idx: nat) (st_src0: RTL.state) (st_tgt0: RTL.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: Unusedglobproof.match_states prog tprog (used_set tprog) skenv_link_src skenv_link_tgt ge tge st_src0 st_tgt0 sm0).

diff --git a/cfrontend/CminorgenproofC.v b/cfrontend/CminorgenproofC.v
@@ -35,7 +35,6 @@ Let tge: Cminor.genv := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk))
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
 Inductive match_states
-          (sm_init: SimMem.t)
           (idx: nat) (st_src0: Csharpminor.state) (st_tgt0: Cminor.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: Cminorgenproof.match_states skenv_link skenv_link ge st_src0 st_tgt0 sm0)

diff --git a/cfrontend/CshmgenproofC.v b/cfrontend/CshmgenproofC.v
@@ -45,7 +45,6 @@ Let tge := (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog).
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
 Inductive match_states
-          (sm_init: SimMem.t)
           (idx: nat) (st_src0: Clight.state) (st_tgt0: Csharpminor.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: Cshmgenproof.match_states prog ge st_src0 st_tgt0)

diff --git a/cfrontend/CstrategyproofC.v b/cfrontend/CstrategyproofC.v
@@ -41,7 +41,6 @@ Let tge: genv := Build_genv (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
 Inductive match_states
-          (sm_init: SimMem.t)
           (idx: nat) (st_src0: Csem.state) (st_tgt0: Csem.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: st_src0 = st_tgt0)

diff --git a/cfrontend/SimplExprproofC.v b/cfrontend/SimplExprproofC.v
@@ -33,7 +33,7 @@ Let ge: Csem.genv := Csem.Build_genv (SkEnv.revive (SkEnv.project skenv_link md_
 Let tge: genv := Build_genv (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) tprog) tprog.(prog_comp_env).
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
-Inductive match_states (sm_init: SimMem.t)
+Inductive match_states
           (idx: nat) (st_src0: Csem.state) (st_tgt0: Clight.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: SimplExprproof.match_states tge st_src0 st_tgt0)

diff --git a/cfrontend/SimplLocalsproofC.v b/cfrontend/SimplLocalsproofC.v
@@ -75,7 +75,6 @@ Let tge := Build_genv (SkEnv.revive (SkEnv.project skenv_link md_tgt.(Mod.sk)) t
 Definition msp: ModSemPair.t := ModSemPair.mk (md_src skenv_link) (md_tgt skenv_link) (SimSymbId.mk md_src md_tgt) sm_link.
 
 Inductive match_states
-          (sm_init: SimMem.t)
           (idx: nat) (st_src0: Clight.state) (st_tgt0: Clight.state) (sm0: SimMem.t): Prop :=
 | match_states_intro
     (MATCHST: SimplLocalsproof.match_states skenv_link skenv_link ge st_src0 st_tgt0 sm0).

diff --git a/demo/mutrec/IdSimClightIdInv.v b/demo/mutrec/IdSimClightIdInv.v
@@ -44,7 +44,7 @@ Local Instance SimSymbP: SimSymb.class SimMemP := SimMemInjInvC.SimSymbIdInv P.
 
 Local Existing Instance SoundTop.Top.
 
-Inductive match_states_clight_inv (sm_arg: SimMem.t)
+Inductive match_states_clight_inv
   : unit -> Clight.state -> Clight.state -> SimMem.t -> Prop :=
 | match_states_clight_intro
     st_src st_tgt j m_src m_tgt sm0
@@ -55,7 +55,7 @@ Inductive match_states_clight_inv (sm_arg: SimMem.t)
     (MWF: SimMem.wf sm0)
   :
     match_states_clight_inv
-      sm_arg tt st_src st_tgt sm0
+      tt st_src st_tgt sm0
 .
 
 Lemma clight_inj_inv_id

diff --git a/demo/mutrec/IdSimMutrecAB.v b/demo/mutrec/IdSimMutrecAB.v
@@ -26,7 +26,7 @@ Set Implicit Arguments.
 
 Local Opaque Z.mul Z.add Z.sub Z.div.
 
-Inductive match_states_ext_ab (sm_arg: SimMemExt.t')
+Inductive match_states_ext_ab
   : unit -> state -> state -> SimMemExt.t' -> Prop :=
 | match_ext_Callstate
     i m_src m_tgt sm0
@@ -35,7 +35,7 @@ Inductive match_states_ext_ab (sm_arg: SimMemExt.t')
     (MWF: Mem.extends m_src m_tgt)
   :
     match_states_ext_ab
-      sm_arg tt
+      tt
       (Callstate i m_src)
       (Callstate i m_tgt)
       sm0
@@ -46,7 +46,7 @@ Inductive match_states_ext_ab (sm_arg: SimMemExt.t')
     (MWF: Mem.extends m_src m_tgt)
   :
     match_states_ext_ab
-      sm_arg tt
+      tt
       (Returnstate i m_src)
       (Returnstate i m_tgt)
       sm0.
@@ -55,7 +55,7 @@ Section ABSOUNDSTATE.
 
   Variable skenv_link: SkEnv.t.
   Variable su: Sound.t.
-  
+
   Inductive sound_state_ab
     : state -> Prop :=
   | sound_Callstate
@@ -124,7 +124,7 @@ Inductive match_states_ab_internal:
       j m_src m_tgt
 .
 
-Inductive match_states_ab (sm_arg: SimMemInj.t')
+Inductive match_states_ab
   : unit -> state -> state -> SimMemInj.t' -> Prop :=
 | match_states_ab_intro
     st_src st_tgt j m_src m_tgt sm0
@@ -135,7 +135,7 @@ Inductive match_states_ab (sm_arg: SimMemInj.t')
     (MWF: SimMemInj.wf' sm0)
   :
     match_states_ab
-      sm_arg tt st_src st_tgt sm0
+      tt st_src st_tgt sm0
 .
 
 Lemma a_id
@@ -150,7 +150,7 @@ Proof.
   eapply any_id; auto.
 Qed.
 
-Lemma a_ext_unreach 
+Lemma a_ext_unreach
       (WF: Sk.wf MutrecABspec.module)
  :
     exists mp,
@@ -284,14 +284,14 @@ Proof.
     inv SIMSKENV. ss. inv SIMSKE. ss. inv FPTR.  exploit SIMDEF; eauto.
     i. des. clarify. esplits; eauto. econs; ss; eauto.
     unfold Genv.find_funct_ptr. des_ifs.
-      
+
   - i. inv MATCH; eauto.
 
   - i. ss. inv FINALSRC. inv MATCH. inv MATCHST. esplits; eauto.
     + econs.
     + econs; eauto. econs.
     + refl.
-      
+
   - right. ii. des.
     esplits.
     + i. inv MATCH; inv MATCHST; ss.
@@ -338,7 +338,7 @@ Local Existing Instance SimSymbDropInv.SimSymbDropInv.
 Local Existing Instance SoundTop.Top.
 
 
-Inductive match_states_ab_inv (sm_arg: SimMem.t)
+Inductive match_states_ab_inv
   : unit -> state -> state -> SimMem.t -> Prop :=
 | match_states_ab_inv_intro
     st_src st_tgt j m_src m_tgt sm0
@@ -349,7 +349,7 @@ Inductive match_states_ab_inv (sm_arg: SimMem.t)
     (MWF: SimMem.wf sm0)
   :
     match_states_ab_inv
-      sm_arg tt st_src st_tgt sm0.
+      tt st_src st_tgt sm0.
 
 
 Lemma ab_inj_inv_id
@@ -385,14 +385,14 @@ Proof.
     inv SIMSKENV. ss. inv SIMSKE. ss. inv FPTR.  exploit SIMDEF; eauto.
     i. des. clarify. esplits; eauto. econs; ss; eauto.
     unfold Genv.find_funct_ptr. des_ifs.
-      
+
   - i. inv MATCH; eauto.
 
   - i. ss. inv FINALSRC. inv MATCH. inv MATCHST. esplits; eauto.
     + econs.
     + econs; eauto. econs.
     + refl.
-      
+
   - right. ii. des.
     esplits.
     + i. inv MATCH; inv MATCHST; ss.

diff --git a/demo/mutrec/IdSimMutrecAIdInv.v b/demo/mutrec/IdSimMutrecAIdInv.v
@@ -71,7 +71,7 @@ Local Instance SimSymbP: SimSymb.class SimMemP := SimMemInjInvC.SimSymbIdInv P.
 
 Local Existing Instance SoundTop.Top.
 
-Inductive match_states_a_inv (sm_arg: SimMem.t)
+Inductive match_states_a_inv
   : unit -> state -> state -> SimMem.t -> Prop :=
 | match_states_a_intro
     st_src st_tgt j m_src m_tgt sm0
@@ -82,7 +82,7 @@ Inductive match_states_a_inv (sm_arg: SimMem.t)
     (MWF: SimMem.wf sm0)
   :
     match_states_a_inv
-      sm_arg tt st_src st_tgt sm0
+      tt st_src st_tgt sm0
 .
 
 Lemma a_inj_inv_id

diff --git a/demo/mutrec/IdSimMutrecBIdInv.v b/demo/mutrec/IdSimMutrecBIdInv.v
@@ -71,7 +71,7 @@ Local Instance SimSymbP: SimSymb.class SimMemP := SimMemInjInvC.SimSymbIdInv P.
 
 Local Existing Instance SoundTop.Top.
 
-Inductive match_states_b_inv (sm_arg: SimMem.t)
+Inductive match_states_b_inv
   : unit -> state -> state -> SimMem.t -> Prop :=
 | match_states_a_intro
     st_src st_tgt j m_src m_tgt sm0
@@ -82,7 +82,7 @@ Inductive match_states_b_inv (sm_arg: SimMem.t)
     (MWF: SimMem.wf sm0)
   :
     match_states_b_inv
-      sm_arg tt st_src st_tgt sm0
+      tt st_src st_tgt sm0
 .
 
 Lemma b_inj_inv_id