Require Import Program.
Require Import Sem SimProg Skeleton Mod ModSem SimMod SimModSem SimSymb SimMem Sound SimSymb.
Require Import AsmC.
Require SimMemId SimMemExt SimMemInj.
Require SoundTop UnreachC.
Require SimSymbId SimSymbDrop.
Require Import CoqlibC.
Require Import ValuesC.
Require Import LinkingC.
Require Import MapsC.
Require Import AxiomsC.
Require Import Ord.
Require Import MemoryC.
Require Import SmallstepC.
Require Import Events.
Require Import Preservation.
Require Import Integers.
Require Import LocationsC Conventions.
Require Import AsmregsC.
Require Import MatchSimModSemExcl2 MatchSimModSem.
Require Import StoreArguments StoreArgumentsProps.
Require Import AsmStepInj AsmStepExt IntegersC.
Require Import Coq.Logic.PropExtensionality.
Require Import AsmExtra IdSimExtra.
Require Import Conventions1C.
Require Import mktac.
Set Implicit Arguments.
Local Opaque Z.mul Z.add Z.sub Z.div.
Lemma lessdef_commute j src0 src1 tgt0 tgt1
(
INJ0:
Val.inject j src0 tgt0)
(
INJ1:
Val.inject j src1 tgt1)
(
LESS:
Val.lessdef src0 src1)
(
UNDEF:
src0 =
Vundef ->
tgt0 =
Vundef):
Val.lessdef tgt0 tgt1.
Proof.
inv LESS.
- inv INJ0; inv INJ1; ss; try econs; clarify. rewrite UNDEF; auto.
- rewrite UNDEF; auto.
Qed.
Section MEMORYLEMMA.
Lemma Plt_lemma a b c
(
LE: ~
Plt a b):
~
Plt (
a +
c -
b)
c.
Proof.
Lemma Plt_lemma2 a b c d
(
LE: ~
Plt a b)
(
LT:
Plt a (
b +
d)):
Plt (
a +
c -
b) (
c +
d).
Proof.
Lemma Z2Nat_range n:
Z.of_nat (
Z.to_nat n) =
if (
zle 0
n)
then n else 0.
Proof.
Theorem Mem_unfree_parallel_inject
j m1 m2 b ofs_src ofs_tgt sz m1'
b'
delta
(
INJECT:
Mem.inject j m1 m2)
(
UNFREE:
Mem_unfree m1 b (
Ptrofs.unsigned ofs_src) (
Ptrofs.unsigned ofs_src +
sz) =
Some m1')
(
VAL:
ofs_tgt =
Ptrofs.add ofs_src (
Ptrofs.repr delta))
(
DELTA:
j b =
Some (
b',
delta))
(
ALIGN:
forall ofs chunk p (
PERM:
forall ofs0 (
BOUND:
ofs <=
ofs0 <
ofs +
size_chunk chunk),
(
Ptrofs.unsigned ofs_src) <=
ofs0 < (
Ptrofs.unsigned ofs_src +
sz) \/
Mem.perm m1 b ofs0 Max p),
(
align_chunk chunk |
delta))
(
REPRESENTABLE:
forall ofs (
PERM:
Mem.perm m1 b (
Ptrofs.unsigned ofs)
Max Nonempty \/
Mem.perm m1 b (
Ptrofs.unsigned ofs - 1)
Max Nonempty \/
(
Ptrofs.unsigned ofs_src) <=
Ptrofs.unsigned ofs < (
Ptrofs.unsigned ofs_src +
sz) \/
(
Ptrofs.unsigned ofs_src) <=
Ptrofs.unsigned ofs - 1 < (
Ptrofs.unsigned ofs_src +
sz)),
delta >= 0 /\ 0 <=
Ptrofs.unsigned ofs +
delta <=
Ptrofs.max_unsigned)
(
NOPERM:
Mem_range_noperm m2 b' (
Ptrofs.unsigned ofs_tgt) (
Ptrofs.unsigned ofs_tgt +
sz)):
exists m2',
(<<
UNFREE:
Mem_unfree m2 b' (
Ptrofs.unsigned ofs_tgt) (
Ptrofs.unsigned ofs_tgt +
sz) =
Some m2'>>)
/\ (<<
INJECT:
Mem.inject j m1'
m2'>>).
Proof.
Lemma Mem_unfree_perm_restore m0 m1 m2 m3 blk lo hi
(
FREE:
Mem.free m0 blk lo hi =
Some m1)
(
MAXPERM:
forall b ofs
(
VALID:
Mem.valid_block m0 b),
<<
MAX:
Mem.perm m2 b ofs Max <1=
Mem.perm m1 b ofs Max>>)
(
UNFREE:
Mem_unfree m2 blk lo hi =
Some m3)
(
NBLE:
Ple (
Mem.nextblock m1) (
Mem.nextblock m2)):
forall b ofs (
VALID:
Mem.valid_block m0 b),
(<<
MAX:
Mem.perm m3 b ofs Max <1=
Mem.perm m0 b ofs Max>>).
Proof.
Lemma Mem_unfree_parallel
sm0 sm_arg sm_ret blk_src ofs_src ofs_tgt sz blk_tgt delta m_src1
(
DELTA:
sm0.(
SimMemInj.inj)
blk_src =
Some (
blk_tgt,
delta))
(
VAL:
ofs_tgt =
Ptrofs.add ofs_src (
Ptrofs.repr delta))
(
MLE0:
SimMemInj.le'
sm0 sm_arg)
(
FREESRC:
Mem.free
(
SimMemInj.src sm0)
blk_src
(
Ptrofs.unsigned ofs_src) (
Ptrofs.unsigned ofs_src +
sz) =
Some (
SimMemInj.src sm_arg))
(
FREETGT:
Mem.free
(
SimMemInj.tgt sm0)
blk_tgt
(
Ptrofs.unsigned ofs_tgt) (
Ptrofs.unsigned ofs_tgt +
sz) =
Some (
SimMemInj.tgt sm_arg))
(
MWF0:
SimMemInj.wf'
sm0)
(
MWF1:
SimMemInj.wf'
sm_arg)
(
MWF2:
SimMemInj.wf'
sm_ret)
(
MLE1:
SimMemInj.le' (
SimMemInj.lift'
sm_arg)
sm_ret)
(
UNFREESRC:
Mem_unfree
(
SimMemInj.src sm_ret)
blk_src
(
Ptrofs.unsigned ofs_src) (
Ptrofs.unsigned ofs_src +
sz) =
Some m_src1):
exists sm1,
(<<
MSRC:
sm1.(
SimMemInj.src) =
m_src1>>)
/\ (<<
MINJ:
sm1.(
SimMemInj.inj) =
sm_ret.(
SimMemInj.inj)>>)
/\ (<<
FREETGT:
Mem_unfree
(
SimMemInj.tgt sm_ret)
blk_tgt
(
Ptrofs.unsigned ofs_tgt) (
Ptrofs.unsigned ofs_tgt +
sz)
=
Some sm1.(
SimMemInj.tgt)>>)
/\ (<<
MWF:
SimMemInj.wf'
sm1>>)
/\ (<<
MLE:
SimMemInj.le'
sm0 sm1>>).
Proof.
End MEMORYLEMMA.
Definition junk_inj (
m_src0 m_tgt0:
mem) (
j:
meminj) (
n:
nat):
meminj :=
fun blk =>
if plt blk (
Mem.nextblock m_src0)
then j blk
else
if plt blk (
Mem.nextblock (
JunkBlock.assign_junk_blocks m_src0 n))
then
Some ((
blk + (
Mem.nextblock m_tgt0) - (
Mem.nextblock m_src0))%
positive, 0)
else j blk.
Definition src_junk_val (
m_src0 m_tgt0:
mem) (
n:
nat) (
v:
val):
val :=
match v with
|
Vptr blk ofs =>
if plt blk (
Mem.nextblock m_tgt0)
then Vundef
else if plt blk (
Mem.nextblock (
JunkBlock.assign_junk_blocks m_tgt0 n))
then
Vptr (
blk + (
Mem.nextblock m_src0) - (
Mem.nextblock m_tgt0))%
positive ofs
else Vundef
|
_ =>
v
end.
Lemma src_junk_val_inj m_src0 m_tgt0 j n v
(
INJ:
Mem.inject j m_src0 m_tgt0):
Val.inject (
junk_inj m_src0 m_tgt0 j n) (
src_junk_val m_src0 m_tgt0 n v)
v.
Proof.
Lemma src_junk_val_junk m_src0 m_tgt0 n v
(
JUNK:
JunkBlock.is_junk_value m_tgt0 (
JunkBlock.assign_junk_blocks m_tgt0 n)
v):
JunkBlock.is_junk_value
m_src0 (
JunkBlock.assign_junk_blocks m_src0 n)
(
src_junk_val m_src0 m_tgt0 n v).
Proof.
Definition set_regset_junk
(
m_src0 m_tgt0:
mem) (
n:
nat)
(
rs0 rs1:
Mach.regset) (
sg:
signature) (
mr:
mreg) :
val :=
if Loc.notin_dec (
R mr) (
regs_of_rpairs (
loc_arguments sg))
then src_junk_val m_src0 m_tgt0 n (
rs1 mr)
else rs0 mr.
Lemma junk_inj_incr m_src0 m_tgt0 j n
(
INJ:
Mem.inject j m_src0 m_tgt0):
inject_incr j (
junk_inj m_src0 m_tgt0 j n).
Proof.
Lemma assign_junk_blocks_parallel_inject m_src0 m_tgt0 j n
(
INJ:
Mem.inject j m_src0 m_tgt0)
:
Mem.inject
(
junk_inj m_src0 m_tgt0 j n)
(
JunkBlock.assign_junk_blocks m_src0 n)
(
JunkBlock.assign_junk_blocks m_tgt0 n).
Proof.
Lemma junk_inj_separated m_src0 m_tgt0 j n
(
INJ:
Mem.inject j m_src0 m_tgt0):
inject_separated j (
junk_inj m_src0 m_tgt0 j n)
m_src0 m_tgt0.
Proof.
Lemma assign_junk_blocks_parallel n sm0
(
MWF:
SimMemInj.wf'
sm0):
exists sm1,
(<<
MSRC:
sm1.(
SimMemInj.src) =
JunkBlock.assign_junk_blocks (
SimMemInj.src sm0)
n>>)
/\ (<<
MTGT:
sm1.(
SimMemInj.tgt) =
JunkBlock.assign_junk_blocks (
SimMemInj.tgt sm0)
n>>)
/\ (<<
MINJ:
sm1.(
SimMemInj.inj) =
junk_inj (
SimMemInj.src sm0) (
SimMemInj.tgt sm0) (
SimMemInj.inj sm0)
n>>)
/\ (<<
MWF:
SimMemInj.wf'
sm1>>)
/\ (<<
MLE:
SimMemInj.le'
sm0 sm1>>)
.
Proof.
Lemma store_arguments_nextblock
m0 m1 rs vs sg
(
STORE:
store_arguments m0 rs vs sg m1):
Plt (
Mem.nextblock m0) (
Mem.nextblock m1).
Proof.
Lemma store_arguments_max_perm
m0 m1 rs vs sg
(
STORE:
store_arguments m0 rs vs sg m1)
b ofs
(
VALID:
Mem.valid_block m0 b):
Mem.perm m1 b ofs <2=
Mem.perm m0 b ofs.
Proof.
Lemma store_arguments_parallel
sm0 m_tgt1 rs_tgt vs vs'
sg
(
ARGSRC:
store_arguments sm0.(
SimMemInj.tgt)
rs_tgt vs'
sg m_tgt1)
(
TYP:
Val.has_type_list vs'
sg.(
sig_args))
(
SZ: 4 *
size_arguments sg <=
Ptrofs.max_unsigned)
(
VALINJ:
Val.inject_list sm0.(
SimMemInj.inj)
vs vs')
(
MWF:
SimMemInj.wf'
sm0):
exists sm1 rs_src,
(<<
ARGTGT:
store_arguments sm0.(
SimMemInj.src)
rs_src vs sg sm1.(
SimMemInj.src)>>) /\
(<<
INJ:
sm1.(
SimMemInj.inj) = (
update_meminj sm0.(
SimMemInj.inj) (
Mem.nextblock sm0.(
SimMemInj.src)) (
Mem.nextblock sm0.(
SimMemInj.tgt)) 0)>>) /\
(<<
MWF:
SimMemInj.wf'
sm1>>) /\
(<<
MLE:
SimMemInj.le'
sm0 sm1>>) /\
(<<
MTGT:
sm1.(
SimMemInj.tgt) =
m_tgt1>>) /\
(<<
AGREE:
StoreArgumentsProps.agree
(
update_meminj sm0.(
SimMemInj.inj) (
Mem.nextblock sm0.(
SimMemInj.src)) (
Mem.nextblock sm0.(
SimMemInj.tgt)) 0)
rs_src
rs_tgt>>).
Proof.
Definition undef_bisim (
rs_src rs_tgt:
regset):
Prop :=
forall (
r:
mreg) (
IN:
Conventions1.is_callee_save r =
true) (
UNDEF:
rs_src (
to_preg r) =
Vundef),
rs_tgt (
to_preg r) =
Vundef.
Inductive wf_init_rs (
rs:
regset):
Prop :=
|
wf_init_rs_intro
(
RSPDEF:
rs RSP <>
Vundef)
(
TPTR:
Val.has_type (
rs RA)
Tptr)
(
RADEF:
rs RA <>
Vundef)
:
wf_init_rs rs.
Inductive wf_init_rs_asmstyle (
rs:
regset):
Prop :=
|
wf_init_rs_amstyle_intro
(
TPTR:
Val.has_type (
rs RA)
Tptr)
(
RADEF:
rs RA <>
Vundef)
:
wf_init_rs_asmstyle rs
.
Inductive wf_init_rss:
signature ->
regset ->
regset ->
Prop :=
|
wf_init_rss_intro
sg init_rs_src init_rs_tgt
(
WFINITSRC:
wf_init_rs init_rs_src)
(
WFINITTGT:
wf_init_rs init_rs_tgt)
(
UNDEF:
undef_bisim init_rs_src init_rs_tgt)
(
CSTYLE:
sg.(
sig_cstyle) =
true)
:
wf_init_rss sg init_rs_src init_rs_tgt
|
wf_init_rss_asmstyle
sg init_rs_src init_rs_tgt
(
WFINITSRC:
wf_init_rs_asmstyle init_rs_src)
(
WFINITTGT:
wf_init_rs_asmstyle init_rs_tgt)
(
CSTYLE:
sg.(
sig_cstyle) =
false)
:
wf_init_rss sg init_rs_src init_rs_tgt
.
Inductive match_states_ext
(
skenv_link_tgt :
SkEnv.t)
(
ge_src ge_tgt:
genv)
(
sm_init : @
SimMem.t SimMemExt.SimMemExt)
:
unit ->
AsmC.state ->
AsmC.state -> (@
SimMem.t SimMemExt.SimMemExt) ->
Prop :=
|
match_states_ext_intro
init_rs_src init_rs_tgt rs_src rs_tgt m_src m_tgt
(
sm0 : @
SimMem.t SimMemExt.SimMemExt)
(
AGREE:
AsmStepExt.agree rs_src rs_tgt)
(
AGREEINIT:
AsmStepExt.agree init_rs_src init_rs_tgt)
(
MCOMPATSRC:
m_src =
sm0.(
SimMem.src))
(
MCOMPATTGT:
m_tgt =
sm0.(
SimMem.tgt))
(
MWF:
SimMem.wf 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)
:
match_states_ext
skenv_link_tgt ge_src ge_tgt sm_init tt
(
AsmC.mkstate init_rs_src (
Asm.State rs_src m_src))
(
AsmC.mkstate init_rs_tgt (
Asm.State rs_tgt m_tgt))
sm0.
Definition asm_init_rs (
rs_src rs_tgt:
Mach.regset)
sg v_pc v_ra blk :=
(((
to_pregset (
set_regset rs_src rs_tgt sg)) #
PC <-
v_pc)
#
RA <-
v_ra)
#
RSP <- (
Vptr blk Ptrofs.zero).
Lemma asm_init_rs_undef_bisim
rs_src rs_tgt sg v_pc v_ra blk:
undef_bisim (
asm_init_rs rs_src (
to_mregset rs_tgt)
sg v_pc v_ra blk)
rs_tgt.
Proof.