Require Import CoqlibC.
Require Import MemoryC.
Require Import Values.
Require Import Maps.
Require Import Events.
Require Import Globalenvs.
Require Import AST.
Require Import IntegersC LinkingC.
Require Import SimSymb Skeleton Mod ModSem.
Require Import SimMemLift.
Require SimSymbId.
Require Import Conventions1.
Require Export SimMemInj.
Set Implicit Arguments.
Section MEMINJ.
Definition update (
sm0:
t') (
src tgt:
mem) (
inj:
meminj):
t' :=
mk src tgt inj sm0.(
src_external)
sm0.(
tgt_external)
sm0.(
src_parent_nb)
sm0.(
tgt_parent_nb)
sm0.(
src_ge_nb)
sm0.(
tgt_ge_nb).
Hint Unfold update.
Hint Unfold src_private tgt_private valid_blocks.
Lemma update_src_private
sm0 sm1
(
INJ:
sm0.(
inj) =
sm1.(
inj))
(
SRC:
sm0.(
src).(
Mem.nextblock) =
sm1.(
src).(
Mem.nextblock)):
sm0.(
src_private) = (
sm1).(
src_private).
Proof.
Lemma update_tgt_private
sm0 sm1
(
SRC:
sm0.(
src) =
sm1.(
src))
(
TGT:
sm0.(
tgt).(
Mem.nextblock) =
sm1.(
tgt).(
Mem.nextblock))
(
INJ:
sm0.(
inj) =
sm1.(
inj)):
sm0.(
tgt_private) =
sm1.(
tgt_private).
Proof.
Inductive lepriv (
sm0 sm1:
SimMemInj.t'):
Prop :=
|
lepriv_intro
(
INCR:
inject_incr sm0.(
inj)
sm1.(
inj))
(
SRCGENB:
sm0.(
src_ge_nb) =
sm1.(
src_ge_nb))
(
TGTGENB:
sm0.(
tgt_ge_nb) =
sm1.(
tgt_ge_nb))
(
FROZEN:
frozen sm0.(
inj)
sm1.(
inj) (
sm0.(
src_ge_nb)) (
sm0.(
tgt_ge_nb))).
Global Program Instance SimMemInj :
SimMem.class :=
{
t :=
t';
src :=
src;
tgt :=
tgt;
wf :=
wf';
le :=
le';
lepriv :=
lepriv;
sim_val :=
fun (
mrel:
t') =>
Val.inject mrel.(
inj);
sim_val_list :=
fun (
mrel:
t') =>
Val.inject_list mrel.(
inj);
}.
Next Obligation.
rename H into LE. inv LE. econs; et. Qed.
Next Obligation.
Next Obligation.
Next Obligation.
inv H. ss. Qed.
Global Program Instance lepriv_Transitive:
RelationClasses.Transitive lepriv.
Next Obligation.
ii.
inv H;
inv H0.
des;
clarify.
econs;
eauto with mem congruence.
+
eapply inject_incr_trans;
eauto.
+
econs;
eauto.
ii;
des.
destruct (
inj y b_src)
eqn:
T.
*
destruct p.
exploit INCR0;
eauto.
i;
clarify.
inv FROZEN.
hexploit NEW_IMPLIES_OUTSIDE;
eauto.
*
inv FROZEN0.
hexploit NEW_IMPLIES_OUTSIDE;
eauto; [];
i;
des.
esplits;
congruence.
Qed.
Global Program Instance SimMemInjLift :
SimMemLift.class SimMemInj :=
{
lift :=
lift';
unlift :=
unlift';
}.
Next Obligation.
rename H into VALID.
inv VALID.
econs;
ss;
eauto;
ii;
des;
ss;
eauto;
eapply Pos.compare_gt_iff in H;
xomega.
Qed.
Next Obligation.
Next Obligation.
Next Obligation.
inv MWF.
destruct sm0;
ss.
econs;
ss;
et.
eapply frozen_refl. Qed.
Next Obligation.
inv MWF.
inv MLE.
inv MLIFT.
econs;
ss;
et;
try congruence.
eapply frozen_refl. Qed.
Section ORIGINALS.
Inductive le_excl (
excl_src excl_tgt:
block ->
Z ->
Prop) (
mrel0 mrel1:
t'):
Prop :=
|
le_excl_intro
(
INCR:
inject_incr mrel0.(
inj)
mrel1.(
inj))
(
SRCUNCHANGED:
Mem.unchanged_on mrel0.(
src_external)
mrel0.(
src)
mrel1.(
src))
(
TGTUNCHANGED:
Mem.unchanged_on mrel0.(
tgt_external)
mrel0.(
tgt)
mrel1.(
tgt))
(
SRCPARENTEQ:
mrel0.(
src_external) =
mrel1.(
src_external))
(
SRCPARENTEQNB:
mrel0.(
src_parent_nb) =
mrel1.(
src_parent_nb))
(
SRCGENB:
mrel0.(
src_ge_nb) =
mrel1.(
src_ge_nb))
(
TGTPARENTEQ:
mrel0.(
tgt_external) =
mrel1.(
tgt_external))
(
TGTPARENTEQNB:
mrel0.(
tgt_parent_nb) =
mrel1.(
tgt_parent_nb))
(
TGTGENB:
mrel0.(
tgt_ge_nb) =
mrel1.(
tgt_ge_nb))
(
FROZEN:
frozen mrel0.(
inj)
mrel1.(
inj) (
mrel0.(
src_parent_nb))
(
mrel0.(
tgt_parent_nb)))
(
MAXSRC:
forall b ofs
(
VALID:
Mem.valid_block mrel0.(
src)
b)
(
EXCL: ~
excl_src b ofs),
<<
MAX:
Mem.perm mrel1.(
src)
b ofs Max <1=
Mem.perm mrel0.(
src)
b ofs Max>>)
(
MAXTGT:
forall b ofs
(
VALID:
Mem.valid_block mrel0.(
tgt)
b)
(
EXCL: ~
excl_tgt b ofs),
<<
MAX:
Mem.perm mrel1.(
tgt)
b ofs Max <1=
Mem.perm mrel0.(
tgt)
b ofs Max>>).
Inductive has_footprint (
excl_src excl_tgt:
block ->
Z ->
Prop) (
sm0:
t'):
Prop :=
|
has_footprint_intro
(
FOOTSRC:
forall blk ofs
(
EXCL:
excl_src blk ofs),
<<
PERM:
Mem.perm sm0.(
src)
blk ofs Cur Freeable>>)
(
FOOTTGT:
forall blk ofs
(
EXCL:
excl_tgt blk ofs),
<<
PERM:
Mem.perm sm0.(
tgt)
blk ofs Cur Freeable>>).
Lemma unfree_right
sm0 lo hi blk m_tgt0
(
MWF:
wf'
sm0)
(
NOPERM:
Mem_range_noperm sm0.(
tgt)
blk lo hi)
(
UNFR:
Mem_unfree sm0.(
tgt)
blk lo hi =
Some m_tgt0)
(
RANGE:
brange blk lo hi <2= ~2
sm0.(
tgt_external)):
exists sm1,
(<<
MSRC:
sm1.(
src) =
sm0.(
src)>>)
/\ (<<
MTGT:
sm1.(
tgt) =
m_tgt0>>)
/\ (<<
MINJ:
sm1.(
inj) =
sm0.(
inj)>>)
/\ (<<
MWF:
wf'
sm1>>)
/\ (<<
MLE:
le_excl bot2 (
brange blk lo hi)
sm0 sm1>>).
Proof.
Lemma foot_excl
sm0 sm1 sm2 excl_src excl_tgt
(
MWF:
SimMem.wf sm0)
(
FOOT:
has_footprint excl_src excl_tgt sm0)
(
MLE:
le'
sm0 sm1)
(
MLEEXCL:
le_excl excl_src excl_tgt sm1 sm2):
<<
MLE:
le'
sm0 sm2>>.
Proof.
inv MLE.
inv MLEEXCL.
assert(
FROZENHI:
frozen (
inj sm0) (
inj sm2) (
src_parent_nb sm0) (
tgt_parent_nb sm0)).
{ -
clear -
FROZEN FROZEN0 INCR0 SRCPARENTEQNB TGTPARENTEQNB.
inv FROZEN.
inv FROZEN0.
econs.
i.
des.
destruct (
inj sm1 b_src)
eqn:
T.
+
destruct p;
ss.
exploit INCR0;
et.
i;
clarify.
exploit NEW_IMPLIES_OUTSIDE;
et.
+
exploit NEW_IMPLIES_OUTSIDE0;
et.
i;
des.
esplits;
eauto with congruence xomega. }
econs;
et;
try (
by etrans;
et).
-
etrans;
et.
rewrite SRCPARENTEQ.
ss.
-
etrans;
et.
rewrite TGTPARENTEQ.
ss.
-
eapply frozen_shortened;
et;
try apply MWF.
-
ii.
destruct (
classic (
excl_src b ofs)).
+
inv FOOT.
eapply Mem.perm_cur_max.
eapply Mem.perm_implies with (
p1 :=
Freeable); [|
eauto with mem].
eapply FOOTSRC;
et.
+
eapply MAXSRC;
et.
eapply MAXSRC0;
et.
eapply Mem.valid_block_unchanged_on;
et.
-
ii.
destruct (
classic (
excl_tgt b ofs)).
+
inv FOOT.
eapply Mem.perm_cur_max.
eapply Mem.perm_implies with (
p1 :=
Freeable); [|
eauto with mem].
eapply FOOTTGT;
et.
+
eapply MAXTGT;
et.
eapply MAXTGT0;
et.
eapply Mem.valid_block_unchanged_on;
et.
Qed.
End ORIGINALS.
Lemma parallel_gen sm0 m_src1 m_tgt1 j1
(
WF:
wf'
sm0)
(
INJECT:
Mem.inject j1 m_src1 m_tgt1)
(
INCR:
inject_incr sm0.(
inj)
j1)
(
SEP:
inject_separated sm0.(
inj)
j1 sm0.(
src)
sm0.(
tgt))
(
UNCHSRC:
Mem.unchanged_on
(
loc_unmapped sm0.(
inj))
sm0.(
src)
m_src1)
(
UNCHTGT:
Mem.unchanged_on
(
loc_out_of_reach sm0.(
inj)
sm0.(
src))
sm0.(
tgt)
m_tgt1)
(
MAXSRC:
forall b ofs
(
VALID:
Mem.valid_block sm0.(
src)
b),
<<
MAX:
Mem.perm m_src1 b ofs Max <1=
Mem.perm sm0.(
src)
b ofs Max>>)
(
MAXTGT:
forall b ofs
(
VALID:
Mem.valid_block sm0.(
tgt)
b),
<<
MAX:
Mem.perm m_tgt1 b ofs Max <1=
Mem.perm sm0.(
tgt)
b ofs Max>>):
(<<
MLE:
le'
sm0 (
mk m_src1 m_tgt1 j1
(
src_external sm0) (
tgt_external sm0)
(
src_parent_nb sm0) (
tgt_parent_nb sm0)
(
src_ge_nb sm0) (
tgt_ge_nb sm0))>>) /\
(<<
MWF:
wf' (
mk m_src1 m_tgt1 j1
(
src_external sm0) (
tgt_external sm0)
(
src_parent_nb sm0) (
tgt_parent_nb sm0)
(
src_ge_nb sm0) (
tgt_ge_nb sm0))>>).
Proof.
Lemma alloc_left_zero_simmem
sm0 blk_src sz m_src1 blk_tgt
(
MWF:
SimMem.wf sm0)
(
ALLOC:
Mem.alloc sm0.(
SimMem.src) 0
sz = (
m_src1,
blk_src))
(
TGTPRIV: (
range 0
sz) <1=
sm0.(
tgt_private)
blk_tgt)
(
TGTNOTEXT: ((
range 0
sz) /1\
sm0.(
tgt_external)
blk_tgt) <1=
bot1)
(
TGTPERM:
forall ofs k p (
BOUND: 0 <=
ofs <
sz),
Mem.perm sm0.(
SimMem.tgt)
blk_tgt ofs k p)
(
VALID:
Mem.valid_block sm0.(
tgt)
blk_tgt)
(
PARENT: (
sm0.(
tgt_parent_nb) <=
blk_tgt)%
positive):
let sm1 := (
mk m_src1 sm0.(
tgt)
(
fun blk =>
if eq_block blk blk_src then Some (
blk_tgt, 0)
else sm0.(
inj)
blk)
sm0.(
src_external)
sm0.(
tgt_external)
sm0.(
src_parent_nb)
sm0.(
tgt_parent_nb)
sm0.(
src_ge_nb)
sm0.(
tgt_ge_nb)
)
in
<<
MWF:
SimMem.wf sm1>> /\
<<
MLE:
SimMem.le sm0 sm1>>.
Proof.
Local Opaque Z.mul.
Require StoreArguments.
End MEMINJ.
Hint Unfold valid_blocks src_private tgt_private range.
Section SIMSYMB.
Lemma skenv_inject_meminj_preserves_globals
F V (
skenv:
Genv.t F V)
j
(
INJECT:
skenv_inject skenv j):
<<
INJECT:
meminj_preserves_globals skenv j>>.
Proof.
Inductive sim_skenv_inj (
sm:
SimMem.t) (
__noname__:
unit) (
skenv_src skenv_tgt:
SkEnv.t):
Prop :=
|
sim_skenv_inj_intro
(
INJECT:
skenv_inject skenv_src sm.(
inj))
(
SIMSKENV:
SimSymbId.sim_skenv skenv_src skenv_tgt)
(
NBSRC:
skenv_src.(
Genv.genv_next) =
sm.(
src_ge_nb))
(
NBTGT:
skenv_tgt.(
Genv.genv_next) =
sm.(
tgt_ge_nb)).
Section REVIVE.
Context {
F1 V1:
Type} {
LF:
Linker F1} {
LV:
Linker V1}.
Context `{
HasExternal F1}.
Variables (
p_src:
AST.program F1 V1).
Lemma skenv_inject_revive
skenv_proj_src ge_src j
(
REVIVESRC:
ge_src =
SkEnv.revive skenv_proj_src p_src)
(
SIMSKENV:
skenv_inject skenv_proj_src j):
<<
SIMSKENV:
skenv_inject ge_src j>>.
Proof.
clarify. inv SIMSKENV. econs; eauto. Qed.
End REVIVE.
Global Program Instance SimSymbId:
SimSymb.class SimMemInj := {
t :=
unit;
le :=
SimSymbId.le;
sim_sk :=
SimSymbId.sim_sk;
sim_skenv :=
sim_skenv_inj;
}.
Next Obligation.
ss. Qed.
Next Obligation.
rr in SIMSK. clarify. Qed.
Next Obligation.
Next Obligation.
inv SIMSKE. inv SIMSKENV. ss. Qed.
Next Obligation.
Next Obligation.
inv SIMSKENV.
inv INJECT.
econs;
eauto.
econs;
eauto.
-
ii.
exploit DOMAIN;
eauto.
i.
eapply MLE;
eauto.
-
ii.
inv MLE.
eapply IMAGE;
eauto.
erewrite frozen_preserves_tgt;
eauto.
eapply Plt_Ple_trans;
eauto.
rewrite <-
NBTGT.
rr in SIMSKENV0.
clarify.
refl.
-
inv MLE.
eauto with congruence.
-
inv MLE.
eauto with congruence.
Qed.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Local Existing Instance SimMemInj.
Local Existing Instance SimSymbId.
Lemma sim_skenv_symbols_inject
sm0 ss0 skenv_src skenv_tgt
(
SIMSKE:
SimSymb.sim_skenv sm0 ss0 skenv_src skenv_tgt):
symbols_inject sm0.(
SimMemInj.inj)
skenv_src skenv_tgt.
Proof.
End SIMSYMB.
Arguments skenv_inject_revive [
_ _ _].
Require Import JunkBlock.
Section JUNK.
Lemma inject_junk_blocks_tgt
sm0 n m_tgt0
(
MWF:
SimMem.wf sm0)
(
JUNKTGT:
assign_junk_blocks sm0.(
SimMem.tgt)
n =
m_tgt0):
exists sm1,
(<<
DEF:
sm1 =
update sm0 sm0.(
SimMem.src)
m_tgt0 sm0.(
SimMemInj.inj)>>) /\
(<<
MWF:
SimMem.wf sm1>>) /\
(<<
MLE:
SimMem.le sm0 sm1>>) /\
(<<
PRIVSRC:
sm0.(
SimMemInj.src_private) =
sm1.(
SimMemInj.src_private)>>) /\
(<<
PRIVTGT:
sm0.(
SimMemInj.tgt_private) <2=
sm1.(
SimMemInj.tgt_private)>>).
Proof.
Definition inject_junk_blocks (
m_src0 m_tgt0:
mem) (
n:
nat) (
j:
meminj):
meminj :=
if (
Zerob.zerob n)
then j else
fun blk =>
if negb (
plt blk m_src0.(
Mem.nextblock)) && (
plt blk (
Mem.nextblock m_src0 +
Pos.of_nat n))
then Some ((
blk +
m_tgt0.(
Mem.nextblock) -
m_src0.(
Mem.nextblock))%
positive , 0%
Z)
else j blk.
Lemma inject_junk_blocks_parallel
sm0 n m_tgt0
(
MWF:
SimMem.wf sm0)
(
JUNKTGT:
assign_junk_blocks sm0.(
SimMem.tgt)
n =
m_tgt0):
exists sm1,
(<<
DEF:
sm1 =
update sm0 (
assign_junk_blocks sm0.(
SimMem.src)
n)
m_tgt0
(
inject_junk_blocks sm0.(
SimMem.src)
sm0.(
SimMem.tgt)
n sm0.(
SimMemInj.inj))>>) /\
(<<
MWF:
SimMem.wf sm1>>) /\
(<<
MLE:
SimMem.le sm0 sm1>>) /\
(<<
PRIVSRC:
sm0.(
SimMemInj.src_private) =
sm1.(
SimMemInj.src_private)>>) /\
(<<
PRIVTGT:
sm0.(
SimMemInj.tgt_private) <2=
sm1.(
SimMemInj.tgt_private)>>).
Proof.
End JUNK.
Lemma Mem_free_parallel'
sm0 blk_src blk_tgt ofs_src ofs_tgt sz m_src0
(
MWF:
wf'
sm0)
(
VAL:
Val.inject sm0.(
inj) (
Vptr blk_src ofs_src) (
Vptr blk_tgt ofs_tgt))
(
FREESRC:
Mem.free sm0.(
src)
blk_src ofs_src.(
Ptrofs.unsigned) (
ofs_src.(
Ptrofs.unsigned) +
sz) =
Some m_src0):
exists sm1,
(<<
MSRC:
sm1.(
src) =
m_src0>>)
/\ (<<
MINJ:
sm1.(
inj) =
sm0.(
inj)>>)
/\ (<<
FREETGT:
Mem.free sm0.(
tgt)
blk_tgt ofs_tgt.(
Ptrofs.unsigned) (
ofs_tgt.(
Ptrofs.unsigned) +
sz) =
Some sm1.(
tgt)>>)
/\ (<<
MWF:
wf'
sm1>>)
/\ (<<
MLE:
le'
sm0 sm1>>).
Proof.
Lemma storebytes_mapped
sm0 b tb ofs bytes1 bytes2 m_src delta
(
MWF :
SimMemInj.wf'
sm0)
(
STRSRC:
Mem.storebytes (
SimMemInj.src sm0)
b ofs bytes1 =
Some m_src)
(
SIMBLK: (
SimMemInj.inj sm0)
b =
Some (
tb,
delta))
(
BYTESINJ:
list_forall2 (
memval_inject (
SimMemInj.inj sm0))
bytes1 bytes2):
exists sm1,
(<<
MSRC: (
SimMemInj.src sm1) =
m_src>>)
/\ (<<
MINJ: (
SimMemInj.inj sm1) = (
SimMemInj.inj sm0)>>)
/\ (<<
STRTGT:
Mem.storebytes (
SimMemInj.tgt sm0)
tb (
ofs +
delta)
bytes2 =
Some (
SimMemInj.tgt sm1)>>)
/\ (<<
MWF:
SimMemInj.wf'
sm1>>)
/\ (<<
MLE:
SimMemInj.le'
sm0 sm1>>)
.
Proof.
Require Import SeparationC.
Section SEP.
Local Open Scope sep_scope.
Lemma minjection_disjoint_footprint_private
sm0 P
(
SEP: (
SimMemInj.tgt sm0) |=
P)
(
DISJ:
disjoint_footprint (
minjection (
SimMemInj.inj sm0) (
SimMemInj.src sm0))
P):
P.(
m_footprint) <2=
sm0.(
SimMemInj.tgt_private).
Proof.
u. ii. esplits; eauto.
- ii. eapply DISJ; eauto. ss. esplits; eauto.
- destruct P; ss. eapply m_valid; eauto.
Qed.
Lemma minjection_private_disjoint_footprint
sm0 P
(
PRIV:
P.(
m_footprint) <2=
sm0.(
SimMemInj.tgt_private)):
<<
DISJ:
disjoint_footprint (
minjection (
SimMemInj.inj sm0) (
SimMemInj.src sm0))
P>>.
Proof.
- ii. ss. des. eapply PRIV; eauto.
Qed.
Lemma external_call_parallel_rule_simmem
(
F V:
Type) (
ge0:
Genv.t F V)
sm_at sm_after P
(
SEP:
sm_at.(
SimMem.tgt) |= (
minjection sm_at.(
SimMemInj.inj)
sm_at.(
SimMem.src))
**
globalenv_inject ge0 sm_at.(
SimMemInj.inj) **
P)
sm_arg sm_ret
(
MWF:
SimMem.wf sm_at)
(
MWF0:
SimMem.wf sm_arg)
(
MWF1:
SimMem.wf sm_ret)
(
MWF2:
SimMem.wf sm_after)
(
MWFAFTR :
SimMem.wf (
SimMemInj.unlift'
sm_arg sm_ret))
(
MLE:
SimMem.le sm_at sm_arg)
(
MLE0:
SimMem.le (
SimMemLift.lift sm_arg)
sm_ret)
(
MLE1:
SimMem.le (
SimMemLift.unlift sm_at sm_ret)
sm_after)
(
MLEAFTR:
SimMem.le sm_arg (
SimMemLift.unlift sm_arg sm_ret))
(
PRIV0:
sm_at.(
SimMemInj.tgt_private) =
sm_arg.(
SimMemInj.tgt_private))
(
PRIV1:
sm_ret.(
SimMemInj.tgt_private) =
sm_after.(
SimMemInj.tgt_private))
(
UNCH0:
Mem.unchanged_on (
SimMemInj.tgt_private sm_arg) (
SimMemInj.tgt sm_at) (
SimMemInj.tgt sm_arg))
(
UNCH1:
Mem.unchanged_on (
SimMemInj.tgt_private sm_arg) (
SimMemInj.tgt sm_ret) (
SimMemInj.tgt sm_after)):
<<
SEP:
sm_after.(
SimMem.tgt) |= (
minjection sm_after.(
SimMemInj.inj)
sm_after.(
SimMem.src))
**
globalenv_inject ge0 sm_at.(
SimMemInj.inj) **
P>>.
Proof.
Lemma sim_skenv_inj_globalenv_inject
F `{
HasExternal F}
V
skenv_proj_src skenv_proj_tgt sm_arg (
prog:
AST.program F V)
m_tgt0
(
SIMSKE:
sim_skenv_inj sm_arg tt skenv_proj_src skenv_proj_tgt)
(
NB:
Ple (
Genv.genv_next skenv_proj_src) (
Mem.nextblock m_tgt0)):
m_tgt0 |=
globalenv_inject (
SkEnv.revive skenv_proj_src prog) (
SimMemInj.inj sm_arg).
Proof.
End SEP.