Module IdSimInvExtra
Require Import Sem SimProg Skeleton Mod ModSem SimMod SimModSem SimSymb SimMemLift Sound SimSymb.
Require SimMemInjInv.
Require SoundTop SimSymbId SimSymbDropInv.
Require Import CoqlibC.
Require Import ValuesC.
Require Import MapsC.
Require Import AxiomsC.
Require Import Ord.
Require Import MemoryC.
Require Import SmallstepC.
Require Import Events.
Require Import Preservation.
Require Import IdSimExtra.
Set Implicit Arguments.
Section INJINVDROP.
Local Existing Instance SimSymbDropInv.SimMemInvTop.
Local Existing Instance SimSymbDropInv.SimSymbDropInv.
Lemma SimSymbDropInv_match_globals F `{
HasExternal F}
V sm0 skenv_src skenv_tgt (
p:
AST.program F V)
(
SIMSKE:
SimSymbDropInv.sim_skenv sm0 bot1 skenv_src skenv_tgt)
:
meminj_match_globals
eq
(
SkEnv.revive skenv_src p)
(
SkEnv.revive skenv_tgt p)
(
SimMemInj.inj sm0.(
SimMemInjInv.minj)).
Proof.
inv SIMSKE.
econs.
-
i.
unfold SkEnv.revive in *.
exists d_src.
apply Genv_map_defs_def in FINDSRC.
des.
unfold o_bind,
o_bind2,
o_join,
o_map,
curry2,
fst in MAP.
des_ifs_safe.
apply Genv.invert_find_symbol in Heq0.
exploit SIMDEF;
try apply FIND;
eauto.
i.
des.
clarify.
esplits;
eauto.
exploit Genv_map_defs_def_inv;
try apply DEFTGT.
i.
rewrite H0.
unfold o_bind,
o_bind2,
o_join,
o_map,
curry2,
fst.
erewrite Genv.find_invert_symbol.
+
rewrite Heq1;
eauto.
+
exploit SIMSYMB1;
eauto.
i.
des.
eauto.
-
i.
unfold SkEnv.revive in *.
rewrite Genv_map_defs_symb in FINDSRC.
exploit SIMSYMB2;
try apply FINDSRC;
eauto.
Qed.
Lemma SimSymbDropInv_find_None F `{
HasExternal F}
V (
p:
AST.program F V)
sm0 skenv_src skenv_tgt fptr_src fptr_tgt
(
FINDSRC:
Genv.find_funct (
SkEnv.revive skenv_src p)
fptr_src =
None)
(
SIMSKE:
SimSymbDropInv.sim_skenv sm0 bot1 skenv_src skenv_tgt)
(
FPTR:
Val.inject (
SimMemInj.inj sm0.(
SimMemInjInv.minj))
fptr_src fptr_tgt)
(
FPTRDEF:
fptr_src <>
Vundef)
:
Genv.find_funct (
SkEnv.revive skenv_tgt p)
fptr_tgt =
None.
Proof.
unfold Genv.find_funct,
Genv.find_funct_ptr in *.
des_ifs_safe.
exfalso.
unfold SkEnv.revive in *.
ss.
apply Genv_map_defs_def in Heq.
des.
unfold o_bind,
o_bind2,
o_join,
o_map,
curry2,
fst in MAP.
des_ifs_safe.
apply Genv.invert_find_symbol in Heq0.
inv SIMSKE.
ss.
inv FPTR;
clarify.
exploit SIMDEFINV;
try apply FIND;
eauto.
i.
des.
clarify.
erewrite Integers.Ptrofs.add_zero in H4.
clarify.
exploit Genv_map_defs_def_inv;
try apply DEFSRC.
i.
revert FINDSRC.
rewrite H0.
unfold o_bind,
o_bind2,
o_join,
o_map,
curry2,
fst.
erewrite Genv.find_invert_symbol.
-
rewrite Heq1;
eauto.
i.
des_ifs.
-
exploit SIMSYMB3;
eauto.
i.
des.
assert (
blk_src =
b1).
{
exploit DISJ;
eauto. }
clarify.
Qed.
End INJINVDROP.
Section INJINVID.
Variable P:
SimMemInjInv.memblk_invariant.
Lemma SimSymbIdInv_match_globals F `{
HasExternal F}
V sm0 skenv_src skenv_tgt (
p:
AST.program F V)
(
SIMSKE:
SimMemInjInvC.sim_skenv_inj sm0 bot1 skenv_src skenv_tgt)
:
meminj_match_globals
eq
(
SkEnv.revive skenv_src p)
(
SkEnv.revive skenv_tgt p)
(
SimMemInj.inj sm0.(
SimMemInjInv.minj)).
Proof.
inv SIMSKE.
inv INJECT.
inv SIMSKENV.
econs;
ss;
eauto.
-
ii.
exploit IMAGE;
eauto.
+
left.
eapply Genv.genv_defs_range in FINDSRC.
eauto.
+
i.
des.
clarify.
esplits;
eauto.
-
i.
exploit INVCOMPAT;
eauto.
i.
des.
exploit DOMAIN;
eauto.
eapply Genv.genv_symb_range in FINDSRC.
eauto.
Qed.
Lemma SimSymbIdInv_find_None F `{
HasExternal F}
V (
p:
AST.program F V)
sm0 skenv_src skenv_tgt fptr_src fptr_tgt
(
FINDSRC:
Genv.find_funct (
SkEnv.revive skenv_src p)
fptr_src =
None)
(
SIMSKE:
SimMemInjInvC.sim_skenv_inj sm0 bot1 skenv_src skenv_tgt)
(
FPTR:
Val.inject (
SimMemInj.inj sm0.(
SimMemInjInv.minj))
fptr_src fptr_tgt)
(
FPTRDEF:
fptr_src <>
Vundef)
:
Genv.find_funct (
SkEnv.revive skenv_tgt p)
fptr_tgt =
None.
Proof.
End INJINVID.
Require Import IdSimAsmExtra.
Require Import Integers.
Require Import mktac.
Section UNFREEPARALLEL.
Variable P_tgt :
SimMemInjInv.memblk_invariant.
Local Instance SimMemInvP :
SimMem.class :=
SimMemInjInvC.SimMemInjInv SimMemInjInv.top_inv P_tgt.
Lemma Mem_unfree_parallel
(
sm0 sm_arg sm_ret:
SimMem.t)
blk_src ofs_src ofs_tgt sz blk_tgt delta
m_src1
(
DELTA:
sm0.(
SimMemInjInv.minj).(
SimMemInj.inj)
blk_src =
Some (
blk_tgt,
delta))
(
VAL:
ofs_tgt =
Ptrofs.add ofs_src (
Ptrofs.repr delta))
(
MLE0:
SimMemInjInv.le'
sm0 sm_arg)
(
FREESRC:
Mem.free
(
SimMem.src sm0)
blk_src
(
Ptrofs.unsigned ofs_src) (
Ptrofs.unsigned ofs_src +
sz) =
Some (
SimMem.src sm_arg))
(
FREETGT:
Mem.free
(
SimMem.tgt sm0)
blk_tgt
(
Ptrofs.unsigned ofs_tgt) (
Ptrofs.unsigned ofs_tgt +
sz) =
Some (
SimMem.tgt sm_arg))
(
MWF0:
SimMem.wf sm0)
(
MWF1:
SimMem.wf sm_arg)
(
MWF2:
SimMem.wf sm_ret)
(
MLE1:
SimMem.le (
SimMemLift.lift sm_arg)
sm_ret)
(
UNFREESRC:
Mem_unfree
(
SimMem.src sm_ret)
blk_src
(
Ptrofs.unsigned ofs_src) (
Ptrofs.unsigned ofs_src +
sz) =
Some m_src1)
:
exists sm1,
(<<
MSRC:
sm1.(
SimMem.src) =
m_src1>>)
/\ (<<
MINJ:
sm1.(
SimMemInjInv.minj).(
SimMemInj.inj) =
sm_ret.(
SimMemInjInv.minj).(
SimMemInj.inj)>>)
/\ (<<
FREETGT:
Mem_unfree
(
SimMem.tgt sm_ret)
blk_tgt
(
Ptrofs.unsigned ofs_tgt) (
Ptrofs.unsigned ofs_tgt +
sz)
=
Some sm1.(
SimMem.tgt)>>)
/\ (<<
MWF:
SimMem.wf sm1>>)
/\ (<<
MLE:
SimMem.le sm0 sm1>>).
Proof.
End UNFREEPARALLEL.
Require Import AsmC.
Inductive match_states P0 P1
(
skenv_link_tgt:
SkEnv.t)
(
ge_src ge_tgt:
genv)
(
sm_init :
SimMemInjInv.t')
:
nat->
AsmC.state ->
AsmC.state ->
SimMemInjInv.t' ->
Prop :=
|
match_states_intro
j init_rs_src init_rs_tgt rs_src rs_tgt m_src m_tgt
(
sm0 :
SimMemInjInv.t')
(
AGREE:
AsmStepInj.agree j rs_src rs_tgt)
(
AGREEINIT:
AsmStepInj.agree j init_rs_src init_rs_tgt)
(
MCOMPATSRC:
m_src =
sm0.(
SimMemInjInv.minj).(
SimMemInj.src))
(
MCOMPATTGT:
m_tgt =
sm0.(
SimMemInjInv.minj).(
SimMemInj.tgt))
(
MCOMPATINJ:
j =
sm0.(
SimMemInjInv.minj).(
SimMemInj.inj))
(
MWF: @
SimMemInjInv.wf'
P0 P1 sm0)
fd
(
FINDF:
Genv.find_funct ge_src (
init_rs_src PC) =
Some (
Internal fd))
(
WFINITRS:
wf_init_rss fd.(
fn_sig)
init_rs_src init_rs_tgt)
(
RAWF:
Genv.find_funct skenv_link_tgt (
init_rs_tgt RA) =
None)
(
RSPDELTA:
forall (
SIG:
sig_cstyle fd.(
fn_sig) =
true)
blk_src ofs (
RSPSRC:
init_rs_src RSP =
Vptr blk_src ofs),
exists blk_tgt,
(
j blk_src =
Some (
blk_tgt, 0)))
:
match_states
P0 P1
skenv_link_tgt
ge_src ge_tgt sm_init 0
(
AsmC.mkstate init_rs_src (
Asm.State rs_src m_src))
(
AsmC.mkstate init_rs_tgt (
Asm.State rs_tgt m_tgt))
sm0
.