Require Import CoqlibC Errors.
Require Import IntegersC ASTC Linking.
Require Import ValuesC MemoryC SeparationC Events GlobalenvsC Smallstep.
Require Import LTL Op LocationsC LinearC MachC MachExtra.
Require Import Bounds ConventionsC StacklayoutC LineartypingC.
Require Import Stacking.
Local Open Scope string_scope.
Local Open Scope sep_scope.
Require Export Stackingproof.
Require Import Simulation.
Require Import Skeleton Mod ModSem SimMod SimModSem SimSymb SimMemLift AsmregsC MatchSimModSemExcl.
Require Import Conventions1C.
Require SimMemInjC.
Require Import AxiomsC.
Require SoundTop.
Require Import StoreArguments StoreArgumentsProps.
Require Import ModSemProps.
Require Import LiftDummy.
Require Import JunkBlock.
Set Implicit Arguments.
Local Opaque Z.add Z.mul Z.div.
Local Opaque sepconj.
Local Opaque function_bounds.
Local Opaque make_env.
Ltac sep_simpl_tac :=
unfold NW in *;
repeat (
try rewrite sep_assoc in *;
try rewrite sep_pure in *;
try rewrite stack_contents_nil_left_false in *;
try assumption;
try rewrite stack_contents_nil_right_false in *;
try assumption;
try match goal with
| [
H:
_ |=
pure False |-
_] =>
simpl in H;
inv H
| [
H:
_ |=
_ **
pure False |-
_] =>
apply sep_proj2 in H
| [
H:
_ |=
_ **
pure False **
_ |-
_] =>
apply sep_pick2 in H
end;
idtac).
Notation "'
stack_contents'" := (
stack_contents_args) (
only parsing).
Section STACKINGEXTRA.
Lemma match_stacks_sp_valid
se tse ge j cs cs'
sg sm0 sp'
(
STKS:
match_stacks se tse ge j cs cs'
sg sm0)
(
SP:
parent_sp cs' =
Vptr sp'
Ptrofs.zero):
<<
SPVALID:
sm0.(
SimMemInj.tgt).(
Mem.valid_block)
sp' /\
Ple sm0.(
SimMemInj.tgt_parent_nb)
sp' /\
forall i, ~
sm0.(
SimMemInj.tgt_external)
sp'
i>>.
Proof.
inv STKS; des_safe; ss; clarify; inv MAINARGS; esplits; eauto. Qed.
Lemma match_stacks_sp_ofs:
forall j se tse ge cs cs'
sg sm,
match_stacks se tse ge j cs cs'
sg sm ->
exists sp, (
parent_sp cs') =
Vptr sp Ptrofs.zero.
Proof.
induction 1; ii; ss; esplits; eauto. Qed.
Local Opaque Z.add Z.mul make_env function_bounds.
Lemma arguments_private
sp_tgt spdelta m_src m_tgt stk_src stk_tgt
F sg se tse ge sm
(
MATCH:
m_tgt |=
stack_contents F stk_src stk_tgt **
minjection F m_src)
(
STACKS:
match_stacks se tse ge F stk_src stk_tgt sg sm)
(
SP:
parent_sp stk_tgt =
Vptr sp_tgt spdelta):
<<
_ :
forall ofs (
OFS: 0 <=
ofs < 4 *
size_arguments sg),
(<<
PRIV:
loc_out_of_reach F m_src sp_tgt (
spdelta.(
Ptrofs.unsigned) +
ofs)>>)>>.
Proof.
ii.
eapply separation_private;
eauto.
destruct stk_tgt;
ss. {
inv STACKS.
inv MAINARGS. }
des_ifs.
destruct stk_src;
ss.
{
sep_simpl_tac.
des;
ss. }
des_ifs_safe.
des_ifs;
sep_simpl_tac.
-
unfold dummy_frame_contents in *.
inv MATCH.
ss.
inv STACKS;
ss;
cycle 1.
{
inv STK;
ss. }
des;
cycle 1.
{
apply tailcall_size in LE.
xomega. }
clarify.
-
Local Transparent sepconj.
cbn.
left.
left.
right.
left.
split; [
ss|].
Local Opaque sepconj.
apply sep_pick1 in MATCH.
unfold frame_contents in *.
unfold fe_ofs_arg.
rewrite !
Z.add_0_l in *.
inv STACKS;
ss.
des_ifs_safe.
des.
rewrite Ptrofs.unsigned_zero in *.
esplits;
eauto;
try xomega.
Qed.
Lemma arguments_perm
se tse ge sm sp_tgt spdelta
m_src m_tgt stk_src stk_tgt F sg
(
MATCH:
m_tgt |=
stack_contents F stk_src stk_tgt **
minjection F m_src)
(
STACKS:
match_stacks se tse ge F stk_src stk_tgt sg sm)
(
SP:
parent_sp stk_tgt =
Vptr sp_tgt spdelta):
<<
_ :
forall ofs (
OFS: 0 <=
ofs < 4 *
size_arguments sg),
(<<
PERM:
Mem.perm m_tgt sp_tgt (
spdelta.(
Ptrofs.unsigned) +
ofs)
Cur Freeable>>)>>.
Proof.
ii.
destruct stk_tgt;
ss. {
inv STACKS.
inv MAINARGS. }
des_ifs.
destruct stk_src;
ss.
{
sep_simpl_tac.
des;
ss. }
des_ifs_safe.
des_ifs;
ss;
sep_simpl_tac.
-
unfold dummy_frame_contents in *.
inv MATCH.
ss.
inv STACKS;
ss;
cycle 1.
{
inv STK;
ss. }
des;
cycle 1.
{
apply tailcall_size in LE.
xomega. }
clarify.
eapply H4;
eauto.
-
apply sep_pick1 in MATCH.
unfold frame_contents in *.
ss.
des_ifs.
des.
apply sep_pick2 in MATCH.
unfold fe_ofs_arg in *.
inv MATCH.
des;
ss.
eapply H2;
eauto.
inv STACKS;
ss.
rewrite !
Z.add_0_l in *.
xomega.
Qed.
Lemma contains_locations_range:
forall j sp lo hi k rs,
massert_imp (
contains_locations j sp lo hi k rs)
(
range sp lo (
lo + (4 *
hi))).
Proof.
Lemma contains_locations_range_2
m j sp pos bound slot ls
(
SEP:
m |=
contains_locations j sp pos bound slot ls):
<<
RANEG:
m |=
range sp pos (
pos + 4 *
bound)>>.
Proof.
ss. des. esplits; eauto. ii. eauto with mem. Qed.
Lemma agree_callee_save_regs_undef_outgoing_slots
ls0 ls1
(
AG:
agree_callee_save_regs ls0 ls1):
<<
AG:
agree_callee_save_regs ls0 ls1.(
undef_outgoing_slots)>>.
Proof.
Program Definition freed_contains_locations (
j:
meminj) (
sp:
block) (
pos bound:
Z) (
sl:
slot) (
ls:
locset) :
massert := {|
m_pred :=
fun m =>
(8 |
pos) /\ 0 <=
pos
/\
Mem.valid_block m sp;
m_footprint :=
brange sp pos (
pos + 4 *
bound)
|}.
Next Obligation.
Next Obligation.
rr in H0. des. clarify.
Qed.
Program Definition contains_locations_tl (
j:
meminj) (
sp:
block) (
pos from bound:
Z) (
sl:
slot) (
ls:
locset) :
massert := {|
m_pred :=
fun m =>
from <=
bound /\
pos + 4 *
bound <=
Ptrofs.modulus /\
Mem.range_perm m sp (
pos + 4 *
from) (
pos + 4 *
bound)
Cur Freeable /\
forall ofs ty,
from <=
ofs ->
ofs +
typesize ty <=
bound -> (
Locations.typealign ty |
ofs) ->
exists v,
Mem.load (
chunk_of_type ty)
m sp (
pos + 4 *
ofs) =
Some v
/\
Val.inject j (
ls (
S sl ofs ty))
v;
m_footprint :=
brange sp (
pos + 4 *
from) (
pos + 4 *
bound)
|}.
Next Obligation.
Next Obligation.
Lemma contains_locations_split
j sp pos lo hi sl ls
(
RANGE: 0 <=
lo <=
hi):
massert_imp (
contains_locations j sp pos hi sl ls)
(
contains_locations j sp pos lo sl ls **
contains_locations_tl j sp pos lo hi sl ls).
Proof.
Local Transparent sepconj.
-
econs;
ss.
+
ii.
des.
esplits;
eauto with xomega;
ss.
{
ii.
eauto with xomega mem. }
{
ii.
eauto with xomega mem. }
unfold disjoint_footprint.
ss.
ii.
des.
clarify.
rr in H5.
des.
clarify.
xomega.
+
ii.
u in H.
des;
clarify;
esplits;
et;
try xomega.
Qed.
Lemma contains_locations_split_m_footprint
j sp pos lo hi sl ls
(
RANGE: 0 <=
lo <=
hi):
(
contains_locations j sp pos hi sl ls).(
m_footprint)
= (
contains_locations j sp pos lo sl ls **
contains_locations_tl j sp pos lo hi sl ls).(
m_footprint).
Proof.
Lemma free_freed_contains_locations
j sp pos sz sl ls m0 m1 CTX
(
SEP:
m0 |=
contains_locations j sp pos sz sl ls **
CTX)
(
FREE:
Mem.free m0 sp pos (
pos + 4 *
sz) =
Some m1)
(
VALID:
Mem.valid_block m0 sp):
<<
SEP:
m1 |=
freed_contains_locations j sp pos sz sl ls **
CTX>>.
Proof.
Lemma unfree_freed_contains_locations
j sp pos sz bound ls m0 m1 CTX
(
SEP:
m0 |=
freed_contains_locations j sp pos sz Outgoing ls
**
contains_locations_tl j sp pos sz bound Outgoing ls
**
CTX)
(
FREE:
Mem_unfree m0 sp pos (
pos + 4 *
sz) =
Some m1)
(
BOUND:
sz <=
bound):
<<
SEP:
m1 |=
contains_locations j sp pos bound Outgoing ls.(
undef_outgoing_slots) **
CTX>>.
Proof.
Definition frame_contents_1_at_external f (
j:
meminj) (
sp:
block) (
ls ls0:
locset) (
parent retaddr:
val)
sg :=
let b :=
function_bounds f in
let fe :=
make_env b in
contains_locations j sp fe.(
fe_ofs_local)
b.(
bound_local)
Local ls
**
freed_contains_locations j sp fe_ofs_arg (
size_arguments sg)
Outgoing ls
**
contains_locations_tl j sp fe_ofs_arg (
size_arguments sg) (
bound_outgoing b)
Outgoing ls
**
hasvalue Mptr sp fe.(
fe_ofs_link)
parent
**
hasvalue Mptr sp fe.(
fe_ofs_retaddr)
retaddr
**
contains_callee_saves j sp fe.(
fe_ofs_callee_save)
b.(
used_callee_save)
ls0.
Definition frame_contents_at_external f (
j:
meminj) (
sp:
block) (
ls ls0:
locset) (
parent retaddr:
val)
sg :=
let b :=
function_bounds f in
let fe :=
make_env b in
mconj (
frame_contents_1_at_external f j sp ls ls0 parent retaddr sg)
(
(
freed_range sp fe_ofs_arg (4 * (
size_arguments sg)) **
range sp (4 * (
size_arguments sg))
fe.(
fe_stack_data)) **
range sp (
fe.(
fe_stack_data) +
b.(
bound_stack_data))
fe.(
fe_size)).
Fixpoint stack_contents_at_external (
j:
meminj) (
cs:
list Linear.stackframe) (
cs':
list Mach.stackframe)
sg :
massert :=
match cs,
cs'
with
| [
Linear.Stackframe f _ ls _], [
Mach.Stackframe fb (
Vptr sp'
spofs)
ra _] =>
(
freed_range sp'
spofs.(
Ptrofs.unsigned) (4 * (
size_arguments sg)))
**
range sp' (4 * (
size_arguments sg)) (4 * (
size_arguments f.(
Linear.fn_sig)))
|
Linear.Stackframe f _ ls c ::
cs,
Mach.Stackframe fb (
Vptr sp'
spofs)
ra c' ::
cs' =>
frame_contents_at_external f j sp'
ls (
parent_locset cs) (
parent_sp cs') (
parent_ra cs')
sg
**
stack_contents j cs cs'
|
_,
_ =>
pure False
end.
Lemma stack_contents_at_external_footprint_split
j cs cs'
f sp ls c fb sp'
spofs ra c'
sg
(
NONNIL:
cs <> []):
m_footprint (
stack_contents_at_external j
((
Linear.Stackframe f sp ls c) ::
cs)
((
Mach.Stackframe fb (
Vptr sp'
spofs)
ra c') ::
cs')
sg) =
(
m_footprint (
frame_contents_at_external f j sp'
ls (
parent_locset cs) (
parent_sp cs') (
parent_ra cs')
sg)
\2/
m_footprint (
stack_contents j cs cs')).
Proof.
ii; ss. des_ifs. Qed.
Lemma stackframes_after_external_footprint:
forall j cs cs',
(
stack_contents j cs cs').(
m_footprint) =
(
stack_contents j cs.(
stackframes_after_external)
cs').(
m_footprint).
Proof.
Lemma frame_contents_1_at_external_m_footprint
f j sp rs rs0 sp2 retaddr0 sg
(
SZ: 0 <=
size_arguments sg <=
bound_outgoing (
function_bounds f)):
(
frame_contents_1 f j sp rs rs0 sp2 retaddr0).(
m_footprint) =
(
frame_contents_1_at_external f j sp rs rs0 sp2 retaddr0 sg).(
m_footprint).
Proof.
Lemma frame_contents_at_external_m_footprint
f j sp rs rs0 sp2 retaddr0 sg
(
SZ: 0 <=
size_arguments sg <=
bound_outgoing (
function_bounds f))
(
BOUND: 4 *
bound_outgoing (
function_bounds f) <=
fe_stack_data (
make_env (
function_bounds f))):
(
frame_contents f j sp rs rs0 sp2 retaddr0).(
m_footprint) =
(
frame_contents_at_external f j sp rs rs0 sp2 retaddr0 sg).(
m_footprint).
Proof.
Lemma stack_contents_at_external_m_footprint
se tse tge sm0 stack cs'
sg j F
(
STACKS:
match_stacks se tse tge F stack cs'
sg sm0):
<<
LE: (
stack_contents_at_external j stack cs'
sg).(
m_footprint) =
(
stack_contents j stack cs').(
m_footprint)>>.
Proof.
Lemma frame_contents_footprint_irr:
forall f j0 j1 spb ls0 ls1 sp ra,
(
frame_contents f j0 spb ls0 ls1 sp ra).(
m_footprint) <2=
(
frame_contents f j1 spb ls0 ls1 sp ra).(
m_footprint).
Proof.
Lemma stack_contents_footprint_irr:
forall j0 j1 cs cs',
(
stack_contents j0 cs cs').(
m_footprint) <2=
(
stack_contents j1 cs cs').(
m_footprint).
Proof.
Lemma freed_contains_locations_incr:
forall j j'
sp pos bound sl ls,
inject_incr j j' ->
massert_imp (
freed_contains_locations j sp pos bound sl ls)
(
freed_contains_locations j'
sp pos bound sl ls).
Proof.
intros; split; simpl; intros; auto. Qed.
Lemma contains_locations_tl_incr:
forall j j'
sp pos from bound sl ls,
inject_incr j j' ->
massert_imp (
contains_locations_tl j sp pos from bound sl ls)
(
contains_locations_tl j'
sp pos from bound sl ls).
Proof.
intros; split; simpl; intros; auto.
intuition auto. exploit H4; eauto. intros (v & A & B). exists v; eauto.
Qed.
Local Transparent frame_contents_at_external.
Lemma frame_contents_at_external_incr:
forall f j sp ls ls0 parent retaddr sg m P j',
m |=
frame_contents_at_external f j sp ls ls0 parent retaddr sg **
P ->
inject_incr j j' ->
m |=
frame_contents_at_external f j'
sp ls ls0 parent retaddr sg **
P.
Proof.
Local Opaque frame_contents_at_external.
Lemma stack_contents_at_external_change_meminj:
forall m j j',
inject_incr j j' ->
forall cs cs'
sg,
m |=
stack_contents_at_external j cs cs'
sg ->
m |=
stack_contents_at_external j'
cs cs'
sg.
Proof.
End STACKINGEXTRA.
Definition strong_wf_tgt (
st_tgt0:
Mach.state):
Prop :=
exists parent_sp parent_ra,
last_option st_tgt0.(
MachC.get_stack) =
Some (
Mach.dummy_stack parent_sp parent_ra).
Local Transparent make_env sepconj.
Lemma contains_callee_saves_footprint
j sp b rs0 ofs
(
FOOT:
m_footprint
(
contains_callee_saves j sp (
fe_ofs_callee_save (
make_env b)) (
used_callee_save b)
rs0)
sp ofs)
:
<<
BOUND:
fe_ofs_callee_save (
make_env b) <=
ofs <
size_callee_save_area b (
fe_ofs_callee_save (
make_env b))>>.
Proof.
Local Opaque make_env sepconj.
Section SIMMODSEM.
Variable skenv_link:
SkEnv.t.
Variable sm_link:
SimMem.t.
Variable prog:
Linear.program.
Variable tprog:
Mach.program.
Hypothesis TRANSF:
match_prog prog tprog.
Variable rao:
Mach.function ->
Mach.code ->
ptrofs ->
Prop.
Let md_src:
Mod.t := (
LinearC.module prog).
Let md_tgt:
Mod.t := (
MachC.module tprog rao).
Hypothesis (
INCLSRC:
SkEnv.includes skenv_link md_src.(
Mod.sk)).
Hypothesis (
INCLTGT:
SkEnv.includes skenv_link md_tgt.(
Mod.sk)).
Hypothesis (
WF:
SkEnv.wf skenv_link).
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).
Hypothesis return_address_offset_exists:
forall f sg ros c v (
FUNCT:
Genv.find_funct tge v =
Some (
Internal f)),
is_tail (
Mcall sg ros ::
c) (
fn_code f) ->
exists ofs,
rao f c ofs.
Hypothesis return_address_offset_deterministic:
forall f c ofs ofs',
rao f c ofs ->
rao f c ofs' ->
ofs =
ofs'.
Let match_stacks :=
match_stacks skenv_link skenv_link.
Definition msp:
ModSemPair.t :=
ModSemPair.mk (
md_src skenv_link) (
md_tgt skenv_link)
tt sm_link.
Lemma functions_translated_inject
sm0 fptr_src fd_tgt fptr_tgt
(
SIMGE:
Genv.match_genvs (
match_globdef (
fun _ f tf =>
transf_fundef f =
OK tf)
eq prog)
ge tge)
(
SIMSKE:
SimSymb.sim_skenv sm0 (
ModSemPair.ss msp) (
ModSem.skenv (
ModSemPair.src msp))
(
ModSem.skenv (
ModSemPair.tgt msp)))
(
FUNCSRC:
Genv.find_funct tge fptr_tgt =
Some fd_tgt)
(
INJ:
Val.inject sm0.(
SimMemInj.inj)
fptr_src fptr_tgt):
<<
SRCUB:
fptr_src =
Vundef>> \/
exists fd_src,
<<
FUNCTGT:
Genv.find_funct ge fptr_src =
Some fd_src>>
/\ <<
TRANSF:
transf_fundef fd_src =
OK fd_tgt>>.
Proof.
Hypothesis TRANSL:
match_prog prog tprog.
Lemma transf_function_sig
f tf
(
TRANSFF:
transf_function f =
OK tf):
f.(
Linear.fn_sig) =
tf.(
fn_sig).
Proof.
Local Opaque Pos.of_nat.
Lemma init_match_frame_contents
sm_arg sg m_tgt0 rs vs_src vs_tgt ls sm_init sm_junkinj n
(
SIMSKE:
SimSymb.sim_skenv sm_arg (
ModSemPair.ss msp) (
ModSem.skenv (
ModSemPair.src msp))
(
ModSem.skenv (
ModSemPair.tgt msp)))
(
STORE:
StoreArguments.store_arguments sm_arg.(
SimMemInj.tgt)
rs (
typify_list vs_tgt sg.(
sig_args))
sg m_tgt0)
(
SG: 4 *
size_arguments sg <=
Ptrofs.modulus)
(
LS:
LocationsC.fill_arguments
(
locset_copy (
sm_arg.(
SimMemInj.src).(
Mem.nextblock).(
Zpos) -
m_tgt0.(
Mem.nextblock).(
Zpos))
rs)
(
typify_list vs_src sg.(
sig_args)) (
loc_arguments sg) =
Some ls)
(
SIMVS:
Val.inject_list (
SimMemInj.inj sm_arg)
vs_src vs_tgt)
(
SM0:
sm_init =
sm_arg.(
SimMemInjC.update)
sm_arg.(
SimMemInj.src)
m_tgt0 sm_arg.(
SimMemInj.inj))
(
PRIV:
forall ofs (
BDD: 0 <=
ofs < 4 *
size_arguments sg),
SimMemInj.tgt_private sm_init (
Mem.nextblock sm_arg.(
SimMemInj.tgt))
ofs)
(
MLE0:
SimMem.le sm_arg sm_init)
(
MWF0:
SimMem.wf sm_init)
(
SM1:
sm_junkinj =
sm_init.(
SimMemInjC.update) (
assign_junk_blocks sm_init.(
SimMemInj.src)
n)
(
assign_junk_blocks m_tgt0 n)
(
SimMemInjC.inject_junk_blocks
sm_init.(
SimMemInj.src)
m_tgt0 n
sm_arg.(
SimMemInj.inj)))
(
MLE1:
SimMem.le sm_init sm_junkinj)
(
MWF1:
SimMem.wf sm_junkinj)
(
NB:
Ple (
Genv.genv_next (
SkEnv.project skenv_link md_src.(
Mod.sk))) (
Mem.nextblock m_tgt0)):
assign_junk_blocks m_tgt0 n
|=
dummy_frame_contents sm_arg.(
SimMemInj.inj)
ls sg (
Mem.nextblock sm_arg.(
SimMemInj.tgt)) 0
**
minjection sm_junkinj.(
SimMemInj.inj)
sm_junkinj.(
SimMemInj.src)
**
globalenv_inject ge sm_junkinj.(
SimMemInj.inj).
Proof.
Lemma stack_contents_at_external_intro
sm0 stack cs'
sg sp sm1
(
STACKS:
match_stacks tge _ (
SimMemInj.inj sm0)
stack cs'
sg sm0)
(
RSP:
parent_sp cs' =
Vptr sp Ptrofs.zero)
(
FREETGT:
Mem.free (
SimMemInj.tgt sm0)
sp 0 (4 *
size_arguments sg) =
Some (
SimMemInj.tgt sm1))
(
SEP:
SimMemInj.tgt sm0 |=
stack_contents (
SimMemInj.inj sm0)
stack cs'):
<<
SEP:
SimMemInj.tgt sm1 |=
stack_contents_at_external (
SimMemInj.inj sm0)
stack cs'
sg>>.
Proof.
Lemma stack_contents_at_external_spec_elim
sm_ret stack cs'
sg sp sm_after
(
STACKS:
match_stacks tge _ (
SimMemInj.inj sm_ret)
stack.(
stackframes_after_external)
cs'
sg sm_after)
(
RSP:
parent_sp cs' =
Vptr sp Ptrofs.zero)
(
UNFREETGT:
Mem_unfree (
SimMemInj.tgt sm_ret)
sp 0 (4 *
size_arguments sg) =
Some (
SimMemInj.tgt sm_after))
(
SEP:
SimMemInj.tgt sm_ret |=
stack_contents_at_external (
SimMemInj.inj sm_ret)
stack cs'
sg):
<<
SEP:
SimMemInj.tgt sm_after |=
stack_contents (
SimMemInj.inj sm_ret)
stack.(
stackframes_after_external)
cs'>>.
Proof.
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)
(
MWF:
SimMem.wf sm0)
(
INITRS:
exists dummy_stack_src,
<<
DUMMY:
st_src0.(
LinearC.get_stack).(
last_option) =
Some dummy_stack_src>> /\
<<
GOOD:
forall mr (
CALLEESAVE:
Conventions1.is_callee_save mr),
(<<
UIU:
dummy_stack_src.(
current_locset) (
R mr) =
Vundef ->
st_tgt0.(
init_rs)
mr =
Vundef>>)
/\ (<<
INJ:
Val.inject sm0.(
SimMemInj.inj) (
dummy_stack_src.(
current_locset) (
R mr))
(
st_tgt0.(
init_rs)
mr)>>)>> /\
<<
SIG:
dummy_stack_src.(
current_function).(
Linear.fn_sig) =
st_tgt0.(
init_sg)>>)
(
WFTGT:
strong_wf_tgt st_tgt0.(
MachC.st)).
Inductive match_states_at
(
st_src0:
Linear.state) (
st_tgt0:
MachC.state) (
sm_at sm_arg:
SimMem.t):
Prop :=
|
match_states_at_intro
(
INJ:
sm_at.(
SimMemInj.inj) =
sm_arg.(
SimMemInj.inj))
(
INJ:
sm_at.(
SimMem.src) =
sm_arg.(
SimMem.src))
init_rs init_sg cs'
tfptr rs sp skd fptr cs ls sig
(
SIGEQ:
Sk.get_csig skd =
Some sig)
(
SRCST:
st_src0 =
Linear.Callstate cs fptr sig ls (
SimMemInj.src sm_arg))
(
TGTST:
st_tgt0 =
mkstate init_rs init_sg (
Callstate cs'
tfptr rs (
SimMemInj.tgt sm_at)))
(
RSP:
parent_sp cs' =
Vptr sp Ptrofs.zero)
(
PRIV:
brange sp 0 (4 *
size_arguments sig) <2=
sm_arg.(
SimMemInj.tgt_private))
(
SIG:
Genv.find_funct skenv_link fptr =
Some skd)
(
VALID:
Mem.valid_block (
SimMemInj.tgt sm_arg)
sp)
(
NB:
sm_at.(
SimMem.tgt).(
Mem.nextblock) =
sm_arg.(
SimMem.tgt).(
Mem.nextblock))
(
SEP:
SimMemInj.tgt sm_arg |=
stack_contents_at_external (
SimMemInj.inj sm_arg)
cs cs'
sig
**
minjection (
SimMemInj.inj sm_arg) (
SimMemInj.src sm_arg) **
globalenv_inject ge (
SimMemInj.inj sm_arg)).
Theorem make_match_genvs :
SimSymbId.sim_skenv (
SkEnv.project skenv_link md_src.(
Mod.sk)) (
SkEnv.project skenv_link md_tgt.(
Mod.sk)) ->
Genv.match_genvs (
match_globdef (
fun cunit f tf =>
transf_fundef f =
OK tf)
eq prog)
ge tge.
Proof.
Inductive has_footprint (
st_src0:
Linear.state):
MachC.state ->
SimMem.t ->
Prop :=
|
has_footprint_intro
copied from MachC *
stack rs m0 fptr sg blk ofs
(
SIG:
exists skd,
skenv_link.(
Genv.find_funct)
fptr =
Some skd /\
Sk.get_csig skd =
Some sg)
(
RSP: (
parent_sp stack) =
Vptr blk ofs)
(
OFSZERO:
ofs =
Ptrofs.zero)
init_rs init_sg
newly added *
sm0
(
FOOT:
SimMemInjC.has_footprint bot2 (
brange blk (
ofs.(
Ptrofs.unsigned))
(
ofs.(
Ptrofs.unsigned) + 4 * (
size_arguments sg)))
sm0)
:
has_footprint st_src0 (
mkstate init_rs init_sg (
Callstate stack fptr rs m0))
sm0.
Inductive mle_excl (
st_src0:
Linear.state):
MachC.state ->
SimMem.t ->
SimMem.t ->
Prop :=
|
mle_excl_intro
copied from MachC *
init_rs init_sg stack fptr ls0 m0
sg blk ofs
(
SIG:
exists skd,
skenv_link.(
Genv.find_funct)
fptr =
Some skd /\
Sk.get_csig skd =
Some sg)
(
RSP: (
parent_sp stack) =
Vptr blk ofs)
newly added *
sm0 sm1
(
MLEEXCL:
SimMemInjC.le_excl bot2 (
brange blk (
ofs.(
Ptrofs.unsigned))
(
ofs.(
Ptrofs.unsigned) + 4 * (
size_arguments sg)))
sm0 sm1)
:
mle_excl st_src0 (
mkstate init_rs init_sg (
Callstate stack fptr ls0 m0))
sm0 sm1.
Let SEGESRC:
senv_genv_compat skenv_link ge.
Proof.
eapply SkEnv.senv_genv_compat;
et. Qed.
Proof.
Proof.