Require Import CoqlibC.
Require Import LinkingC.
Require Import Skeleton.
Require Import Values.
Require Import JMeq.
Require Import Smallstep.
Require Import Simulation.
Require Import Integers.
Require Import EventsC.
Require Import MapsC.
Require Import BehaviorsC.
Require Import Skeleton ModSem Mod Sem.
Require Import SimSymb SimMem.
Require Import ModSemProps.
Set Implicit Arguments.
Lemma includes_refl
sk:
<<
INCL:
SkEnv.includes (
Sk.load_skenv sk)
sk>>.
Proof.
Lemma link_includes
p sk_link_src
(
LINK:
link_sk p =
Some sk_link_src)
md
(
IN:
In md p):
SkEnv.includes (
Sk.load_skenv sk_link_src)
md.(
Mod.sk).
Proof.
Definition definitive_initializer (
init:
list init_data) :
bool :=
match init with
|
nil =>
false
|
Init_space _ ::
nil =>
false
|
_ =>
true
end.
Local Transparent Linker_def Linker_vardef Linker_varinit Linker_unit.
Lemma definitive_initializer_is_definitive_left
gv1 gv0
(
sk0 sk1:
Sk.t)
id_fr
(
LINK:
link_prog_merge (
prog_defmap sk0) !
id_fr (
prog_defmap sk1) !
id_fr =
Some (
Gvar gv1))
(
IN: (
prog_defmap sk0) !
id_fr =
Some (
Gvar gv0))
(
DEF:
definitive_initializer (
gvar_init gv0)):
gv0 =
gv1.
Proof.
unfold link_prog_merge in *.
des_ifs_safe.
ss.
des_ifs_safe.
unfold link_vardef in *.
des_ifs_safe.
ss.
destruct gv0;
ss.
unfold link_varinit in *.
des_ifs_safe.
bsimpl.
des.
rewrite eqb_true_iff in *.
f_equal.
{
destruct gvar_info;
ss. }
des_ifs.
Qed.
Lemma definitive_initializer_is_definitive_right
gv1 gv0
(
sk0 sk1:
Sk.t)
id_fr
(
LINK:
link_prog_merge (
prog_defmap sk0) !
id_fr (
prog_defmap sk1) !
id_fr =
Some (
Gvar gv1))
(
IN: (
prog_defmap sk1) !
id_fr =
Some (
Gvar gv0))
(
DEF:
definitive_initializer (
gvar_init gv0)):
gv0 =
gv1.
Proof.
Lemma definitive_initializer_split
(
g0 g1 g:
globvar unit)
(
DEF:
definitive_initializer g.(
gvar_init))
(
LINK:
link g0 g1 =
Some g):
<<
DEF:
definitive_initializer g0.(
gvar_init) \/
definitive_initializer g1.(
gvar_init)>>.
Proof.
Local Opaque Linker_def Linker_vardef Linker_varinit Linker_unit.
Theorem link_preserves_wf_sk
sk0 sk1 sk_link
(
WFSK0:
Sk.wf sk0)
(
WFSK1:
Sk.wf sk1)
(
LINK:
link sk0 sk1 =
Some sk_link):
<<
WF:
Sk.wf sk_link>>.
Proof.
Local Transparent Linker_prog.
ss.
Local Opaque Linker_prog.
hexploit (
link_prog_inv _ _ _ LINK);
et.
intro INV;
des.
clarify.
clear LINK.
econs;
et;
ss.
-
unfold prog_defs_names.
ss.
eapply NoDup_norepet.
eapply PTree.elements_keys_norepet;
et.
-
i.
unfold prog_defs_names.
ss.
apply PTree.elements_complete in IN.
rewrite PTree.gcombine in *;
ss.
apply in_map_iff.
assert((
exists x, (
prog_defmap sk0) !
id_to =
Some x)
\/ (
exists x, (
prog_defmap sk1) !
id_to =
Some x));
cycle 1.
{
des.
-
destruct ((
prog_defmap sk1) !
id_to)
eqn:
T.
+
exploit (
INV0 id_to);
eauto.
intro X;
des.
eexists (
_,
_).
ss.
esplits;
eauto.
apply PTree.elements_correct.
rewrite PTree.gcombine;
ss.
unfold link_prog_merge.
rewrite H.
rewrite T.
et.
+
eexists (
_,
_).
ss.
esplits;
eauto.
apply PTree.elements_correct.
rewrite PTree.gcombine;
ss.
unfold link_prog_merge.
rewrite H.
rewrite T.
et.
-
destruct ((
prog_defmap sk0) !
id_to)
eqn:
T.
+
exploit (
INV0 id_to);
eauto.
intro X;
des.
eexists (
_,
_).
ss.
esplits;
eauto.
apply PTree.elements_correct.
rewrite PTree.gcombine;
ss.
unfold link_prog_merge.
rewrite H.
rewrite T.
et.
+
eexists (
_,
_).
ss.
esplits;
eauto.
apply PTree.elements_correct.
rewrite PTree.gcombine;
ss.
unfold link_prog_merge.
rewrite H.
rewrite T.
et.
}
assert((
exists gv, (
prog_defmap sk0) !
id_fr =
Some (
Gvar gv) /\
definitive_initializer gv.(
gvar_init))
\/ (
exists gv, (
prog_defmap sk1) !
id_fr =
Some (
Gvar gv) /\
definitive_initializer gv.(
gvar_init))).
{
unfold link_prog_merge in *.
des_ifs.
-
exploit (
INV0 id_fr);
et.
intro X;
des.
Local Transparent Linker_def.
ss.
Local Opaque Linker_def.
destruct g,
g0;
ss;
des_ifs.
exploit (@
definitive_initializer_split v v0 gv);
et.
{
unfold definitive_initializer.
des_ifs;
ss;
des;
clarify. }
i;
des;
et.
-
left.
esplits;
et.
unfold definitive_initializer.
des_ifs;
ss;
des;
clarify.
-
right.
esplits;
et.
unfold definitive_initializer.
des_ifs;
ss;
des;
clarify.
}
des.
+
assert(
gv0 =
gv).
{
eapply (
definitive_initializer_is_definitive_left);
eauto. }
clarify.
left.
inv WFSK0.
exploit (
WFPTR id_fr);
et.
{
apply in_prog_defmap;
et. }
intro X;
des.
eapply prog_defmap_dom;
et.
+
assert(
gv0 =
gv).
{
eapply (
definitive_initializer_is_definitive_right);
eauto. }
clarify.
right.
inv WFSK1.
exploit (
WFPTR id_fr);
et.
{
apply in_prog_defmap;
et. }
intro X;
des.
eapply prog_defmap_dom;
et.
-
ii.
assert(
exists gd,
link_prog_merge (
prog_defmap sk0) !
a (
prog_defmap sk1) !
a =
Some gd).
{
unfold link_prog_merge.
des_ifs;
eauto.
-
exploit INV0;
eauto.
i;
des.
esplits;
et.
-
rewrite in_app_iff in *.
des.
+
inv WFSK0.
exploit PUBINCL;
eauto.
intro T.
exploit prog_defmap_dom;
et.
i;
des.
clarify.
+
inv WFSK1.
exploit PUBINCL;
eauto.
intro T.
exploit prog_defmap_dom;
et.
}
unfold prog_defs_names.
ss.
rewrite in_map_iff.
des.
eexists (
_,
_).
s.
esplits;
eauto.
eapply PTree.elements_correct.
rewrite PTree.gcombine;
ss.
unfold link_prog_merge.
des_ifs;
eauto.
-
i.
eapply PTree.elements_complete in IN.
rewrite PTree.gcombine in IN;
ss.
unfold link_prog_merge in IN.
des_ifs.
+
Local Transparent Linker_def.
ss.
unfold link_def in IN.
des_ifs.
Local Transparent Linker_skfundef.
ss.
inv WFSK0;
inv WFSK1.
unfold link_skfundef in Heq1.
des_ifs;
eauto using in_prog_defmap.
+
inv WFSK0.
eapply WFPARAM;
eauto.
eapply in_prog_defmap;
eauto.
+
inv WFSK1.
eapply WFPARAM;
eauto.
eapply in_prog_defmap;
eauto.
Qed.
Theorem link_list_preserves_wf_sk
p sk_link
(
LINK:
link_sk p =
Some sk_link)
(
WFSK:
forall md,
In md p -> <<
WF:
Sk.wf md >>):
<<
WF:
Sk.wf sk_link>>.
Proof.
unfold link_sk in *.
ginduction p;
ii;
ss.
unfold link_list in LINK.
des_ifs_safe.
ss.
destruct (
link_list_aux (
map Mod.sk p))
eqn:
T;
ss.
{
clarify.
destruct p;
ss;
des_ifs.
eapply WFSK.
eauto. }
des_ifs.
rename t into tl.
rename a into hd.
specialize (
IHp tl).
exploit IHp;
eauto.
{
unfold link_list.
des_ifs. }
i;
des.
eapply (@
link_preserves_wf_sk hd tl);
et.
eapply WFSK;
et.
Qed.
Section INITDTM.
Lemma link_sk_disjoint
md0 md1 p0 id skenv_link b if_sig if_sig0 restl sk_link gd_big0
(
IN :
In md0 p0)
(
NOTSAME :
md0 <>
md1)
(
DEFS1 :
defs (
Mod.get_sk md1 (
Mod.data md1))
id)
(
DEFS0 :
defs (
Mod.get_sk md0 (
Mod.data md0))
id)
(
DEFBIG0 :
Genv.find_def skenv_link b =
Some gd_big0)
(
SYMBBIG0 :
Genv.find_symbol skenv_link id =
Some b)
(
WFBIG :
SkEnv.wf skenv_link)
(
DEF0 :
Genv.find_def (
ModSem.skenv (
Mod.get_modsem md0 skenv_link (
Mod.data md0)))
b =
Some (
Gfun (
Internal if_sig)))
(
DEF1 :
Genv.find_def (
ModSem.skenv (
Mod.get_modsem md1 skenv_link (
Mod.data md1)))
b =
Some (
Gfun (
Internal if_sig0)))
(
INCLS :
forall md :
Mod.t,
md1 =
md \/
In md p0 ->
SkEnv.includes skenv_link (
Mod.get_sk md (
Mod.data md)))
(
TL :
link_list (
map (
fun md :
Mod.t =>
Mod.get_sk md (
Mod.data md))
p0) =
Some restl)
(
HD :
link (
Mod.get_sk md1 (
Mod.data md1))
restl =
Some sk_link)
(
SKLINK :
link_list (
Mod.get_sk md1 (
Mod.data md1) ::
map (
fun md :
Mod.t =>
Mod.get_sk md (
Mod.data md))
p0) =
Some sk_link)
(
TLORD :
Forall (
fun x :
Sk.t =>
linkorder x restl) (
map (
fun md :
Mod.t =>
Mod.get_sk md (
Mod.data md))
p0))
(
HDORD :
linkorder (
Mod.get_sk md1 (
Mod.data md1))
sk_link)
(
HDORD0 :
linkorder restl sk_link):
False.
Proof.
Context `{
SM:
SimMem.class}.
Context {
SS:
SimSymb.class SM}.
Variable p:
program.
Hypothesis (
WFSK:
forall md (
IN:
In md p), <<
WF:
Sk.wf md>>).
Let sem :=
Sem.sem p.
Lemma skenv_fill_internals_preserves_wf
skenv0 skenv1
(
WF:
SkEnv.wf skenv0)
(
FILL:
skenv0.(
skenv_fill_internals) =
skenv1):
<<
WF:
SkEnv.wf skenv1>>.
Proof.
Lemma system_disjoint
skenv_link sys_def fptr md md_def
(
WFBIG:
SkEnv.wf skenv_link)
(
SYSTEM:
Genv.find_funct (
System.skenv skenv_link)
fptr =
Some (
Internal sys_def))
(
MOD:
In md p)
(
MODSEM:
Genv.find_funct (
ModSem.skenv (
Mod.get_modsem md skenv_link (
Mod.data md)))
fptr =
Some (
Internal md_def))
(
INCL:
SkEnv.includes skenv_link md.(
Mod.sk)):
False.
Proof.
Theorem genv_disjoint: <<
DISJ:
sem.(
globalenv).(
Ge.disjoint)>>.
Proof.
ss.
des_ifs;
cycle 1.
{
econs;
eauto.
ii;
ss.
inv FIND0.
ss. }
assert(
WFBIG:
t.(
Sk.load_skenv).(
SkEnv.wf)).
{
eapply SkEnv.load_skenv_wf.
eapply link_list_preserves_wf_sk;
et. }
econs;
eauto.
ii;
ss.
inv FIND0;
inv FIND1.
generalize (
link_includes p Heq).
intro INCLS.
unfold Sk.load_skenv in *.
unfold load_genv in *.
unfold load_modsems in *.
ss.
abstr (
Genv.globalenv t)
skenv_link.
rename t into sk_link.
rename Heq into SKLINK.
rewrite in_map_iff in *.
u in *.
destruct MODSEM.
{
clarify.
des;
ss.
exfalso.
clarify.
eapply system_disjoint;
eauto. }
des;
ss.
{
clarify.
ss.
exfalso.
eapply system_disjoint;
eauto. }
rename x into md0.
rename x0 into md1.
clarify.
destruct fptr;
ss.
des_ifs.
unfold Genv.find_funct_ptr in *.
des_ifs.
rename Heq0 into DEF0.
rename Heq into DEF1.
hexploit (@
Mod.get_modsem_projected_sk md0 skenv_link);
eauto.
intro SPEC0;
des.
hexploit (@
Mod.get_modsem_projected_sk md1 skenv_link);
eauto.
intro SPEC1;
des.
remember (
ModSem.skenv (
Mod.get_modsem md0 skenv_link (
Mod.data md0)))
as skenv_proj0 eqn:
T0 in *.
remember (
ModSem.skenv (
Mod.get_modsem md1 skenv_link (
Mod.data md1)))
as skenv_proj1 eqn:
T1 in *.
assert(
WFSMALL0:
skenv_proj0.(
SkEnv.wf_proj)).
{
eapply SkEnv.project_spec_preserves_wf;
try apply SPEC0;
eauto. }
assert(
WFSMALL1:
skenv_proj1.(
SkEnv.wf_proj)).
{
eapply SkEnv.project_spec_preserves_wf;
try apply SPEC1;
eauto. }
bar.
inv WFSMALL0.
exploit DEFSYMB;
eauto.
i;
des.
inv WFSMALL1.
exploit DEFSYMB0;
eauto.
i;
des.
rename SYMB0 into SYMB1.
rename SYMB into SYMB0.
rename id0 into id1.
rename id into id0.
move SYMB0 at top.
move SYMB1 at top.
clear_until_bar.
inv SPEC0.
assert(
DEFS0:
defs (
Mod.get_sk md0 (
Mod.data md0))
id0).
{
apply NNPP.
ii.
exploit SYMBDROP;
eauto.
i;
des.
clarify. }
exploit SYMBKEEP;
eauto.
intro SYMBBIG0;
des.
rewrite SYMB0 in *.
symmetry in SYMBBIG0.
exploit DEFKEPT;
eauto.
{
eapply Genv.find_invert_symbol;
eauto. }
i;
des.
move SYMBBIG0 at top.
move DEFBIG at top.
move DEFS0 at top.
clear_until_bar.
inv SPEC1.
assert(
DEFS1:
defs (
Mod.get_sk md1 (
Mod.data md1))
id1).
{
apply NNPP.
ii.
exploit SYMBDROP;
eauto.
i;
des.
clarify. }
exploit SYMBKEEP;
eauto.
intro SYMBBIG1;
des.
rewrite SYMB1 in *.
symmetry in SYMBBIG1.
exploit DEFKEPT;
eauto.
{
eapply Genv.find_invert_symbol;
eauto. }
i;
des.
move SYMBBIG1 at top.
move DEFBIG0 at top.
move DEFS1 at top.
clear_until_bar.
assert(
id0 =
id1).
{
eapply Genv.genv_vars_inj;
try eapply SYMBBIG0;
eauto. }
clarify.
rename id1 into id.
clear -
SYMBBIG0 WFBIG INCLS DEF0 DEF1 DEFBIG DEFS0 DEFS1 SKLINK H0 MODSEM1.
destruct (
classic (
md0 =
md1));
ss.
{
clarify. }
exfalso.
clear_tac.
generalize dependent sk_link.
ginduction p;
i;
ss.
dup SKLINK.
eapply link_list_cons_inv in SKLINK;
cycle 1.
{
destruct p0;
ss.
inv H0;
inv MODSEM1;
clarify. }
des_safe.
hexploit (
link_list_linkorder _ TL);
eauto.
intro TLORD;
des_safe.
hexploit (
link_linkorder _ _ _ HD);
eauto.
intro HDORD;
des_safe.
des;
clarify;
try (
by eapply link_sk_disjoint;
try eapply DEFBIG;
eauto).
-
eapply IHp0;
try eapply DEFS1;
try eapply DEFS0;
try eapply DEFBIG;
eauto.
Qed.
Lemma find_fptr_owner_determ
fptr ms0 ms1
(
FIND0:
Ge.find_fptr_owner sem.(
globalenv)
fptr ms0)
(
FIND1:
Ge.find_fptr_owner sem.(
globalenv)
fptr ms1):
ms0 =
ms1.
Proof.
inv FIND0;
inv FIND1.
ss.
des_ifs.
unfold load_genv in *.
ss.
generalize genv_disjoint;
i.
inv H.
eapply DISJOINT;
eauto;
econs;
eauto;
ss;
des_ifs.
Qed.
Theorem initial_state_determ
st_init0 st_init1
(
INIT0:
sem.(
Smallstep.initial_state)
st_init0)
(
INIT1:
sem.(
Smallstep.initial_state)
st_init1):
st_init0 =
st_init1.
Proof.
ss. inv INIT0; inv INIT1; ss. clarify.
Qed.
End INITDTM.
Lemma lift_step
(
ms:
ModSem.t)
st0 tr st1
(
STEP:
Step ms st0 tr st1):
forall prog tail,
<<
STEP:
Step (
Sem.sem prog)
(
State ((
Frame.mk ms st0) ::
tail))
tr
(
State ((
Frame.mk ms st1) ::
tail))>>.
Proof.
ii. econs 3; eauto. Qed.
Lemma lift_star
(
ms:
ModSem.t)
st0 tr st1
(
STAR:
Star ms st0 tr st1):
forall prog tail,
<<
STAR:
Star (
Sem.sem prog) (
State ((
Frame.mk ms st0) ::
tail))
tr (
State ((
Frame.mk ms st1) ::
tail))>>.
Proof.
ii.
ginduction STAR;
ii;
ss.
-
econs 1;
eauto.
-
clarify.
econs 2;
eauto.
+
eapply lift_step;
eauto.
+
eapply IHSTAR;
eauto.
Qed.
Lemma lift_plus
(
ms:
ModSem.t)
st0 tr st1
(
PLUS:
Plus ms st0 tr st1):
forall prog tail,
<<
PLUS:
Plus (
Sem.sem prog) (
State ((
Frame.mk ms st0) ::
tail))
tr (
State ((
Frame.mk ms st1) ::
tail))>>.
Proof.
i.
inv PLUS;
ii;
ss.
econs;
eauto.
-
eapply lift_step;
eauto.
-
eapply lift_star;
eauto.
Qed.
Lemma lift_dstep
(
ms:
ModSem.t)
st0 tr st1 prog
(
PUBEQ:
ms.(
symbolenv).(
Senv.public_symbol) = (
Sem.sem prog).(
symbolenv).(
Senv.public_symbol))
(
DSTEP:
DStep ms st0 tr st1):
forall tail,
<<
DSTEP:
DStep (
Sem.sem prog) (
State ((
Frame.mk ms st0) ::
tail))
tr (
State ((
Frame.mk ms st1) ::
tail))>>.
Proof.
ii.
destruct DSTEP as [
DTM STEP].
econs;
eauto;
cycle 1.
-
econs;
ss;
eauto.
-
inv DTM.
econs;
eauto.
+
ii.
ss.
inv H;
ss;
ModSem.tac.
inv H0;
ss;
ModSem.tac.
clear STEP.
determ_tac sd_determ_at.
esplits;
auto.
*
eapply match_traces_preserved;
try apply H.
i.
s.
congruence.
*
ii.
clarify.
special H0;
ss.
clarify.
+
ii.
ss.
inv STEP0;
ss;
ModSem.tac.
inv FINAL;
ss;
ModSem.tac.
+
ii.
inv H;
ss;
ModSem.tac.
exploit sd_traces_at;
eauto.
Qed.
Lemma lift_dstar
(
ms:
ModSem.t)
st0 tr st1 prog
(
PUBEQ:
ms.(
symbolenv).(
Senv.public_symbol) = (
Sem.sem prog).(
symbolenv).(
Senv.public_symbol))
(
DSTAR:
DStar ms st0 tr st1):
forall tail,
<<
DSTAR:
DStar (
Sem.sem prog) (
State ((
Frame.mk ms st0) ::
tail))
tr (
State ((
Frame.mk ms st1) ::
tail))>>.
Proof.
i.
ginduction DSTAR;
ii;
ss.
-
econs 1;
eauto.
-
clarify.
econs 2;
eauto.
+
eapply lift_dstep;
eauto.
+
eapply IHDSTAR;
eauto.
Qed.
Lemma lift_dplus
(
ms:
ModSem.t)
st0 tr st1 prog
(
PUBEQ:
ms.(
symbolenv).(
Senv.public_symbol) = (
Sem.sem prog).(
symbolenv).(
Senv.public_symbol))
(
DPLUS:
DPlus ms st0 tr st1):
forall tail,
<<
DPLUS:
DPlus (
Sem.sem prog) (
State ((
Frame.mk ms st0) ::
tail))
tr (
State ((
Frame.mk ms st1) ::
tail))>>.
Proof.
Lemma lift_receptive_at
(
ms:
ModSem.t)
st0 prog
(
PUBEQ:
ms.(
symbolenv).(
Senv.public_symbol) = (
Sem.sem prog).(
symbolenv).(
Senv.public_symbol))
(
RECEP:
receptive_at ms st0):
forall tail, <<
RECEP:
receptive_at (
Sem.sem prog) (
State ((
Frame.mk ms st0) ::
tail))>>.
Proof.
ii.
inv RECEP.
ss.
econs;
eauto;
ii.
-
inv H.
+
inv H0.
esplits;
eauto.
econs 1;
eauto.
+
ss.
exploit sr_receptive_at;
eauto.
{
eapply match_traces_preserved;
try apply H0.
i.
s.
congruence. }
i;
des.
esplits;
eauto.
econs;
eauto.
+
inv H0.
esplits;
eauto.
econs 4;
eauto.
-
inv H;
s;
try omega.
exploit sr_traces_at;
eauto.
Qed.
Lemma lift_determinate_at
(
ms:
ModSem.t)
st0 prog
(
PUBEQ:
ms.(
symbolenv).(
Senv.public_symbol) = (
Sem.sem prog).(
symbolenv).(
Senv.public_symbol))
(
DTM:
determinate_at ms st0):
forall tail,
<<
DTM:
determinate_at (
Sem.sem prog) (
State ((
Frame.mk ms st0) ::
tail))>>.
Proof.
ii.
inv DTM.
ss.
econs;
eauto;
ii.
-
inv H;
inv H0;
ModSem.tac.
+
esplits;
et.
{
econs;
et. }
i.
f_equal.
eapply ModSem.at_external_dtm;
et.
+
ss.
determ_tac sd_determ_at.
esplits;
et.
{
eapply match_traces_preserved;
try apply H.
i.
s.
congruence. }
i.
clarify.
repeat f_equal.
eauto.
+
ss.
esplits;
et.
{
econs;
et. }
i.
repeat f_equal.
determ_tac ModSem.final_frame_dtm.
eapply ModSem.after_external_dtm;
et.
-
ss.
inv FINAL.
ss.
inv STEP;
ss;
ModSem.tac.
-
inv H;
s;
try omega.
exploit sd_traces_at;
eauto.
Qed.
Require Import MemoryC.
Section WFMEM.
Lemma Genv_bytes_of_init_data_length
F V (
ge:
Genv.t F V)
a:
Datatypes.length (
Genv.bytes_of_init_data ge a) =
nat_of_Z (
init_data_size a).
Proof.
Inductive wf_mem_weak (
skenv ge0:
SkEnv.t) (
sk:
Sk.t) (
m0:
mem):
Prop :=
|
wf_mem_weak_intro
(
WFPTR:
forall blk_fr _ofs_fr blk_to _ofs_to id_fr _q _n gv
(
SYMB:
ge0.(
Genv.find_symbol)
id_fr =
Some blk_fr)
(
IN:
In (
id_fr, (
Gvar gv))
sk.(
prog_defs))
(
NONVOL:
gv.(
gvar_volatile) =
false)
(
DEFINITIVE:
classify_init gv.(
gvar_init) =
Init_definitive gv.(
gvar_init))
(
LOAD:
Mem.loadbytes m0 blk_fr _ofs_fr 1 =
Some [
Fragment (
Vptr blk_to _ofs_to)
_q _n]),
exists id_to, (<<
SYMB:
skenv.(
Genv.invert_symbol)
blk_to =
Some id_to>>)
/\ (<<
IN:
In id_to sk.(
prog_defs_names)>>)).
Let link_load_skenv_wf_sem_one:
forall md sk_link m0 m1 id gd ge0
(
WF:
Sk.wf md)
(
LO:
linkorder md sk_link)
(
IN:
In (
id,
gd)
sk_link.(
prog_defs))
(
NODUP:
NoDup (
prog_defs_names md))
(
NODUP:
NoDup (
prog_defs_names sk_link))
(
LOADM:
Genv.alloc_global (
Sk.load_skenv sk_link)
m0 (
id,
gd) =
Some m1)
(
NOTIN:
Genv.find_symbol ge0 id =
None)
(
WFM:
wf_mem_weak (
Sk.load_skenv sk_link)
ge0 md m0)
(
WFMA:
Genv.globals_initialized (
Sk.load_skenv sk_link)
ge0 m0)
(
WFMB:
Genv.genv_next ge0 =
Mem.nextblock m0),
(<<
WFM:
wf_mem_weak (
Sk.load_skenv sk_link) (
Genv.add_global ge0 (
id,
gd))
md m1>>)
/\ (<<
WFMA:
Genv.globals_initialized (
Sk.load_skenv sk_link) (
Genv.add_global ge0 (
id,
gd))
m1>>)
/\ (<<
WFMB:
Genv.genv_next ge0 =
Mem.nextblock m0>>).
Proof.
Let link_load_skenv_wf_sem_mult:
forall md sk_link idgs m0 m1 ge0
(
WF:
Sk.wf md)
(
LO:
linkorder md sk_link)
(
INCL:
incl idgs sk_link.(
prog_defs))
(
NODUP:
NoDup (
prog_defs_names md))
(
NODUP:
NoDup (
prog_defs_names sk_link))
(
NODUP:
NoDup (
map fst idgs))
(
LOADM:
Genv.alloc_globals (
Sk.load_skenv sk_link)
m0 idgs =
Some m1)
(
NOTIN:
forall id (
IN:
In id (
map fst idgs)),
Genv.find_symbol ge0 id =
None)
(
WFM:
wf_mem_weak (
Sk.load_skenv sk_link)
ge0 md m0)
(
WFMA:
Genv.globals_initialized (
Sk.load_skenv sk_link)
ge0 m0)
(
WFMB:
Genv.genv_next ge0 =
Mem.nextblock m0),
<<
WFM:
wf_mem_weak (
Sk.load_skenv sk_link) (
Genv.add_globals ge0 idgs)
md m1>>
/\ <<
WFMA:
Genv.globals_initialized (
Sk.load_skenv sk_link)
(
Genv.add_globals ge0 idgs)
m1>>
/\ <<
WFMB:
Genv.genv_next ge0 =
Mem.nextblock m0>>.
Proof.
i.
generalize dependent ge0.
generalize dependent m0.
generalize dependent m1.
induction idgs;
ii;
ss.
{
clarify. }
des_ifs.
destruct a.
exploit link_load_skenv_wf_sem_one;
et.
{
eapply INCL;
et.
s.
et. }
i;
des.
exploit IHidgs;
try apply WFM0;
et.
{
ii.
eapply INCL;
et.
s.
et. }
{
ss.
inv NODUP1.
ss. }
{
i.
uge.
unfold Genv.add_global.
s.
rewrite PTree.gsspec.
des_ifs.
-
inv NODUP1.
ss.
-
apply NOTIN.
right.
ss. }
{
s.
clear -
WFMB0 Heq.
exploit Genv.alloc_global_nextblock;
eauto.
congruence. }
i;
des.
esplits;
et.
Qed.
Lemma link_load_skenv_wf_mem
p sk_link m_init
(
LINK:
link_sk p =
Some sk_link)
(
WF:
forall md (
IN:
In md p),
Sk.wf md)
(
LOADM:
Sk.load_mem sk_link =
Some m_init):
let skenv_link :=
Sk.load_skenv sk_link in
<<
WFM:
forall md (
IN:
In md p),
SkEnv.wf_mem skenv_link md m_init>>.
Proof.
End WFMEM.
Require Import Sem SimModSem.
Theorem safe_implies_safe_modsem
p sk ms lst tail
(
LINK:
link_sk p =
Some sk)
(
SAFE:
safe (
sem p) (
State ({|
Frame.ms :=
ms;
Frame.st :=
lst |} ::
tail))):
<<
SAFE:
safe_modsem ms lst>>.
Proof.
ii.
ss.
exploit SAFE.
{
instantiate (1:= (
State ({|
Frame.ms :=
ms;
Frame.st :=
st1 |} ::
tail))).
eapply lift_star;
eauto. }
i;
des.
-
ss.
inv H.
ss.
right.
left.
eauto.
-
ss.
des_ifs.
inv H;
ss.
+
left.
eauto.
+
right.
right.
eauto.
+
right.
left.
eauto.
Qed.
Lemma backward_simulation_refl:
forall SEM,
backward_simulation SEM SEM.
Proof.
i.
eapply (@
Backward_simulation _ _ unit bot2).
econs;
eauto.
{
apply unit_ord_wf. }
ii.
ss.
exists tt.
esplits;
eauto.
clear st_init_src_ INITSRC INITTGT.
rename st_init_tgt into st.
revert st.
pcofix CIH.
i.
pfold.
econs;
eauto.
{
ii.
esplits;
eauto.
econs;
eauto. }
ii.
econs;
eauto.
{
ii.
esplits;
eauto.
left.
apply plus_one.
ss. }
i.
r in SAFESRC.
specialize (
SAFESRC st (
star_refl _ _ _ _)).
ss.
Qed.
Lemma sk_nwf_improves (
mds_src mds_tgt:
program)
(
NWF: ~ (
forall x (
IN:
In x mds_src),
Sk.wf x)):
improves (
sem mds_src) (
sem mds_tgt).
Proof.