Require Import CoqlibC.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import ValuesC.
Require Import MemoryC.
Require Import Globalenvs.
Require Import Events.
Require Import Smallstep.
Require Import Op.
Require Import LocationsC.
Require Import Conventions.
Require Import SimMemInj.
Require Stacklayout.
Require Import Asm Mach mktac MemdataC AsmregsC StoreArguments.
Definition agree (
j:
meminj) (
rs0 rs1:
Mach.regset) :
Prop :=
forall mr,
Val.inject j (
rs0 mr) (
rs1 mr).
Lemma typesize_chunk:
forall ty,
size_chunk (
chunk_of_type ty) = 4 *
ty.(
typesize).
Proof.
destruct ty; ss. Qed.
Section STOREARGUMENTS_PROPERTY.
Lemma extcall_arguments_same (
rs0 rs1:
Mach.regset)
sp m sg args
(
ARGS:
extcall_arguments rs0 m sp sg args)
(
SAME:
forall r (
IN:
In (
R r) (
regs_of_rpairs (
loc_arguments sg))),
rs0 r =
rs1 r):
extcall_arguments rs1 m sp sg args.
Proof.
clear -
ARGS SAME.
unfold extcall_arguments in *.
revert args ARGS SAME.
generalize (
loc_arguments sg).
induction l;
ss;
i;
inv ARGS;
econs;
eauto.
-
inv H1.
+
econs 1.
inv H;
eauto;
try econs;
eauto.
erewrite SAME;
econs;
eauto.
+
inv H;
inv H0;
econs;
eauto;
try erewrite SAME;
eauto; (
try by econs;
eauto);
ss;
eauto.
-
eapply IHl;
eauto.
ii.
eapply SAME.
eapply in_app;
eauto.
Qed.
Definition extcall_arg_in_reg (
rs:
regset) (
l:
rpair loc) (
v:
val) :
Prop :=
forall r (
EQ:
l =
One (
R r)),
v =
rs r.
Definition extcall_arg_in_stack (
m:
ZMap.t memval) (
lo:
Z) (
l:
rpair loc) (
v:
val) :
Prop :=
forall ofs ty (
EQ:
l =
One (
S Outgoing ofs ty)),
decode_val (
chunk_of_type ty) (
Mem.getN (
size_chunk_nat (
chunk_of_type ty)) (
lo + 4 *
ofs)
m) =
v.
Lemma extcall_arguments_extcall_arg_in_reg
rs m blk sg vs lo
(
SZ: 0 <=
lo /\
lo + 4 *
size_arguments sg <=
Ptrofs.max_unsigned)
(
ARGS:
list_forall2
(
extcall_arg_pair rs m (
Vptr blk (
Ptrofs.repr lo)))
(
loc_arguments sg)
vs):
list_forall2 (
extcall_arg_in_reg rs) (
loc_arguments sg)
vs.
Proof.
Lemma extcall_arguments_extcall_arg_in_stack
rs m blk sg vs lo
(
SZ: 0 <=
lo /\
lo + 4 *
size_arguments sg <=
Ptrofs.max_unsigned)
(
ARGS:
list_forall2
(
extcall_arg_pair rs m (
Vptr blk (
Ptrofs.repr lo)))
(
loc_arguments sg)
vs):
list_forall2
(
extcall_arg_in_stack (
m.(
Mem.mem_contents) !!
blk)
lo)
(
loc_arguments sg)
vs.
Proof.
Lemma extcall_arg_in_stack_in_reg_extcall_argument
m blk m_blk rs vs sg
(
STACK:
list_forall2
(
extcall_arg_in_stack m_blk 0)
(
loc_arguments sg)
vs)
(
REGS:
list_forall2
(
extcall_arg_in_reg rs)
(
loc_arguments sg)
vs)
(
MBLK:
m.(
Mem.mem_contents) !!
blk =
m_blk)
(
PERM:
Mem.range_perm m blk 0 (4 *
size_arguments sg)
Cur Freeable)
(
SZ: 4 *
size_arguments sg <=
Ptrofs.max_unsigned):
list_forall2
(
extcall_arg_pair rs m (
Vptr blk Ptrofs.zero)) (
loc_arguments sg)
vs.
Proof.
Lemma store_arguments_unchanged_on m0 m1 rs args sg
(
STORE:
store_arguments m0 rs args sg m1):
Mem.unchanged_on top2 m0 m1.
Proof.
End STOREARGUMENTS_PROPERTY.
Module _FillArgsParallel.
Lemma unsigned_add ofs delta
(
RANGE:
delta >= 0 /\ 0 <=
Ptrofs.unsigned ofs +
delta <=
Ptrofs.max_unsigned):
Ptrofs.unsigned (
Ptrofs.add ofs (
Ptrofs.repr delta))
=
Ptrofs.unsigned ofs +
delta.
Proof.
Definition copy_memval (
v:
val) (
mv:
memval) :
memval :=
match v,
mv with
|
Vundef,
_ =>
Undef
|
_,
Fragment _ q n =>
Fragment v q n
|
_,
_ =>
mv
end.
Definition copy_list_memval (
v:
val):
list memval ->
list memval :=
map (
copy_memval v).
Lemma copy_list_memval_decode_undef vl vl'
(
COPY:
copy_list_memval Vundef vl =
vl'):
vl' =
list_repeat (
List.length vl)
Undef.
Proof.
revert vl' COPY. induction vl; ss; i; clarify. f_equal. eapply IHvl; eauto.
Qed.
Lemma copy_list_memval_decode_pointer j vl vl'
chunk v blk ofs
(
INJ:
Val.inject j v (
decode_val chunk vl))
(
COPY:
copy_list_memval v vl =
vl')
(
VALUE:
v =
Vptr blk ofs):
decode_val chunk vl' =
v.
Proof.
assert(
H:
DUMMY_PROP)
by ss.
clarify.
inv INJ;
ss.
-
unfold decode_val in H2.
destruct vl;
ss.
+
des_ifs.
+
des_ifs_safe.
destruct m,
chunk;
ss;
des_ifs_safe;
cycle 10.
{
repeat ((
repeat apply_all_once andb_prop;
des);
des_sumbool;
clarify;
des_ifs_safe;
ss;
des;
ss;
clarify).
unfold decode_val;
des_ifs.
ss.
unfold proj_sumbool,
andb.
des_ifs. }
{
destruct v;
ss. }
{
repeat ((
repeat apply_all_once andb_prop;
des);
des_sumbool;
clarify;
des_ifs_safe;
ss;
des;
ss;
clarify).
unfold decode_val;
des_ifs.
ss.
unfold proj_sumbool,
andb.
des_ifs. }
all:
des_ifs.
Qed.
Lemma copy_list_memval_decode j vl vl'
chunk v
(
INJ:
Val.inject j v (
decode_val chunk vl))
(
COPY:
copy_list_memval v vl =
vl')
(
LENGTH:
Nat.lt 0 (
length vl)):
decode_val chunk vl' =
v.
Proof.
Lemma copy_list_memval_inject j vl vl'
chunk v
(
INJ:
Val.inject j v (
decode_val chunk vl))
(
COPY:
copy_list_memval v vl =
vl'):
list_forall2 (
memval_inject j)
vl'
vl.
Proof.
Definition fill_arg_src_reg (
rs:
regset) (
arg:
val) (
loc:
rpair loc):
regset :=
match loc with
|
One (
R r) =>
rs#
r <-
arg
|
_ =>
rs
end.
Fixpoint fill_args_src_reg (
args:
list val) (
locs:
list (
rpair loc)):
regset :=
match args,
locs with
|
vhd::
vtl,
lhd::
ltl =>
fill_arg_src_reg (
fill_args_src_reg vtl ltl)
vhd lhd
|
_,
_ =>
fun _ =>
Vundef
end.
Lemma fill_args_src_reg_args args locs
(
NOREPEAT:
Loc.norepet (
regs_of_rpairs locs))
(
ONES:
forall l (
IN:
In l locs),
is_one l)
(
LENGTH:
length args =
length locs):
list_forall2 (
extcall_arg_in_reg (
fill_args_src_reg args locs))
locs args.
Proof.
revert NOREPEAT args LENGTH.
induction locs;
ss;
i.
-
destruct args;
ss.
econs.
-
destruct args;
ss.
inv LENGTH.
destruct a;
inv NOREPEAT.
+
exploit IHlocs;
eauto.
i.
unfold fill_arg_src_reg.
des_ifs.
*
econs;
eauto.
--
ii.
inv EQ.
rewrite Regmap.gss.
auto.
--
eapply list_forall2_lift; [|
eauto].
{
ii.
clarify.
unfold Regmap.set.
des_ifs;
eauto.
exfalso.
eapply loc_notin_not_in;
eauto.
eapply in_one_in_rpair;
eauto. }
*
econs;
eauto.
ii.
inv EQ.
+
exfalso.
exploit ONES;
eauto.
Qed.
Lemma fill_args_src_reg_agree j args args_tgt locs rs_tgt
(
INJECT:
Val.inject_list j args args_tgt)
(
LENGTH:
length args =
length locs)
(
ARGS:
list_forall2 (
extcall_arg_in_reg rs_tgt)
locs args_tgt):
agree j (
fill_args_src_reg args locs)
rs_tgt.
Proof.
generalize dependent args.
revert rs_tgt args_tgt ARGS.
induction locs;
ss;
eauto;
i.
-
inv LENGTH.
destruct args;
ss.
-
destruct args;
ss.
inv INJECT.
inv LENGTH.
inv ARGS.
unfold fill_arg_src_reg.
des_ifs;
try eapply IHlocs;
eauto.
ii.
unfold Regmap.set.
des_ifs.
+
exploit H5;
eauto.
i.
clarify.
+
eapply IHlocs;
eauto.
Qed.
Definition fill_arg_src_blk (
m_tgt m:
ZMap.t memval) (
lo_tgt lo:
Z)
(
arg:
val) (
loc:
rpair loc):
ZMap.t memval :=
match loc with
|
One (
S Outgoing ofs ty) =>
Mem.setN (
copy_list_memval arg (
Mem.getN (
size_chunk_nat (
chunk_of_type ty)) (
lo_tgt + 4 *
ofs)
m_tgt)) (
lo + 4 *
ofs)
m
|
_ =>
m
end.
Fixpoint fill_args_src_blk (
m_tgt m:
ZMap.t memval) (
lo_tgt lo:
Z)
(
args:
list val) (
locs:
list (
rpair loc)):
ZMap.t memval :=
match args,
locs with
|
vhd::
vtl,
lhd::
ltl =>
fill_arg_src_blk m_tgt (
fill_args_src_blk m_tgt m lo_tgt lo vtl ltl)
lo_tgt lo vhd lhd
|
_,
_ =>
m
end.
Definition only_args_blk (
m:
ZMap.t memval) (
locs:
list loc) :=
forall ofs,
(<<
UNDEF:
ZMap.get ofs m =
Undef >>) \/
(<<
INARGS:
exists ofs0 ty v,
(<<
IN:
In (
S Outgoing ofs0 ty)
locs>>) /\
(<<
RANGE: 4 *
ofs0 <=
ofs < 4 *
ofs0 +
size_chunk (
chunk_of_type ty)>>) /\
(<<
LOAD:
decode_val (
chunk_of_type ty) (
Mem.getN (
size_chunk_nat (
chunk_of_type ty)) (4 *
ofs0)
m) =
v>>) /\
(<<
VDEF:
v <>
Vundef>>)>>).
Lemma only_args_blk_incr
m a l
(
ONLY:
only_args_blk m l):
only_args_blk m (
a::
l).
Proof.
ii. specialize (ONLY ofs). des; auto. right. esplits; eauto. ss. auto.
Qed.
Lemma fill_args_src_blk_only_args m_tgt j args_tgt args locs lo_tgt
(
INJECT:
Val.inject_list j args args_tgt)
(
NOREPEAT:
Loc.norepet (
regs_of_rpairs locs))
(
LENGTH:
length args =
length locs)
(
ONES:
forall l (
IN:
In l locs),
is_one l)
(
ARGS:
list_forall2 (
extcall_arg_in_stack m_tgt lo_tgt)
locs args_tgt):
only_args_blk
(
fill_args_src_blk m_tgt (
ZMap.init Undef)
lo_tgt 0
args locs) (
regs_of_rpairs locs).
Proof.
Lemma fill_args_src_blk_inject m_tgt j args_tgt args locs lo_tgt lo
(
INJECT:
Val.inject_list j args args_tgt)
(
LENGTH:
length args =
length locs)
(
ARGS:
list_forall2 (
extcall_arg_in_stack m_tgt lo_tgt)
locs args_tgt):
forall ofs,
memval_inject
j
(
ZMap.get (
lo +
ofs) (
fill_args_src_blk m_tgt (
ZMap.init Undef)
lo_tgt lo args locs))
(
ZMap.get (
lo_tgt +
ofs)
m_tgt).
Proof.
generalize dependent args.
revert m_tgt args_tgt ARGS.
induction locs;
ss;
eauto;
i.
-
inv LENGTH.
destruct args;
ss.
rewrite ZMap.gi.
econs.
-
destruct args;
ss.
inv INJECT.
inv LENGTH.
inv ARGS.
unfold fill_arg_src_blk.
des_ifs;
try eapply IHlocs;
eauto.
+
exploit IHlocs;
eauto.
instantiate (1:=
ofs).
intros INJ.
{
exploit Mem.setN_inj.
-
instantiate (3:=
j).
instantiate (2:=
copy_list_memval v (
Mem.getN (
size_chunk_nat (
chunk_of_type ty)) (
lo_tgt + 4 *
pos)
m_tgt)).
instantiate (1:=
Mem.getN (
size_chunk_nat (
chunk_of_type ty)) (
lo_tgt + 4 *
pos)
m_tgt).
specialize (
H5 pos ty eq_refl).
des.
clarify.
{
eapply copy_list_memval_inject;
eauto. }
-
instantiate (4:=
top1).
instantiate (3:=
fill_args_src_blk m_tgt (
ZMap.init Undef)
lo_tgt lo args locs).
instantiate (1:=
m_tgt).
instantiate (1:=
lo_tgt -
lo).
i.
exploit IHlocs;
eauto.
instantiate (1:=
q -
lo).
i.
rpapply H2;
f_equal;
lia.
-
econs.
-
instantiate (2:=
lo +
ofs).
instantiate (1:=
lo + 4 *
pos).
repeat rewrite Z.add_0_r.
i.
rpapply H.
{
replace (
lo +
ofs + (
lo_tgt -
lo))
with (
lo_tgt +
ofs);
try lia.
replace (
lo + 4 *
pos + (
lo_tgt -
lo))
with (
lo_tgt + 4 *
pos);
try lia.
generalize ofs.
clear -
m_tgt.
generalize (4 *
pos).
revert m_tgt.
generalize (
size_chunk_nat (
chunk_of_type ty)).
induction n;
ss;
i.
repeat rewrite <-
Z.add_assoc.
replace (
Mem.getN n (
lo_tgt + (
z + 1))
m_tgt)
with
(
Mem.getN n (
lo_tgt + (
z + 1)) (
ZMap.set (
lo_tgt +
z) (
ZMap.get (
lo_tgt +
z)
m_tgt)
m_tgt)).
-
rewrite <-
IHn.
rewrite ZMap.gsspec.
des_ifs.
rewrite e.
auto.
-
clear IHn.
generalize z m_tgt (
z+1).
induction n;
ss;
i.
f_equal.
+
rewrite ZMap.gsspec.
des_ifs.
rewrite e.
auto.
+
repeat rewrite <-
Z.add_assoc.
rewrite IHn.
eauto. }
}
Qed.
Lemma fill_args_src_blk_args m_tgt m j args_tgt args locs lo_tgt lo
(
INJECT:
Val.inject_list j args args_tgt)
(
NOREPEAT:
Loc.norepet (
regs_of_rpairs locs))
(
LENGTH:
length args =
length locs)
(
ARGS:
list_forall2 (
extcall_arg_in_stack m_tgt lo_tgt)
locs args_tgt):
list_forall2 (
extcall_arg_in_stack (
fill_args_src_blk m_tgt m lo_tgt lo args locs)
lo)
locs args.
Proof.
Lemma fill_args_src_blk_default m_tgt m args locs lo_tgt lo :
fst (
fill_args_src_blk m_tgt m lo_tgt lo args locs) =
fst m.
Proof.
Program Definition fill_args_src_mem (
m_tgt0 m_tgt1 :
mem) (
m_src0:
mem)
(
args:
list val) (
locs:
list (
rpair loc)) :
mem :=
Mem.mkmem
(
PMap.set
(
m_src0.(
Mem.nextblock))
(
fill_args_src_blk
(
m_tgt1.(
Mem.mem_contents) !! (
m_tgt0.(
Mem.nextblock)))
(
ZMap.init Undef) 0 0
args locs)
(
m_src0.(
Mem.mem_contents)))
(
PMap.set
(
m_src0.(
Mem.nextblock))
(
m_tgt1.(
Mem.mem_access) !! (
m_tgt0.(
Mem.nextblock)))
(
m_src0.(
Mem.mem_access)))
(
Pos.succ m_src0.(
Mem.nextblock))
_ _ _.
Next Obligation.