Require Import CoqlibC Maps.
Require Import ASTC Integers Floats Values MemoryC EventsC Globalenvs Smallstep.
Require Import Locations Stacklayout Conventions.
newly added *
Require Import Mach Simulation ValuesC.
Require Export Asm.
Require Import Skeleton ModSem Mod sflib.
Require Import LocationsC AsmregsC StoreArguments.
Require Import JunkBlock.
Set Implicit Arguments.
Local Obligation Tactic :=
ii;
ss;
des;
inv_all_once;
des;
ss;
clarify;
eauto with congruence.
Definition get_mem (
st:
state):
mem :=
match st with
|
State _ m0 =>
m0
end.
Definition st_rs (
st0:
state):
regset :=
match st0 with
|
State rs _ =>
rs
end.
Definition st_m (
st0:
state):
mem :=
match st0 with
|
State _ m =>
m
end.
Definition store_arguments (
m0:
mem) (
rs:
regset) (
vs:
list val) (
sg:
signature) (
m2:
mem) :
Prop :=
(<<
STORE:
StoreArguments.store_arguments m0 (
to_mregset rs)
vs sg m2>>) /\
(<<
RSRSP:
rs RSP =
Vptr m0.(
Mem.nextblock)
Ptrofs.zero>>).
Definition external_state F V (
ge:
Genv.t F V) (
v :
val) :
bool :=
match v with
|
Vptr blk ofs =>
match (
Genv.find_funct ge (
Vptr blk Ptrofs.zero))
with
|
None =>
true
|
_ =>
false
end
|
_ =>
true
end.
Section MODSEM.
Variable skenv_link:
SkEnv.t.
Variable p:
program.
Let skenv:
SkEnv.t :=
skenv_link.(
SkEnv.project)
p.(
Sk.of_program fn_sig).
Let ge:
genv :=
skenv.(
SkEnv.revive)
p.
Record state :=
mkstate {
init_rs:
regset;
st:>
Asm.state;
}.
Inductive step (
se:
Senv.t) (
ge:
genv) (
st0:
state) (
tr:
trace) (
st1:
state):
Prop :=
|
step_intro
(
STEP:
Asm.step se ge st0.(
st)
tr st1.(
st))
(
INITRS:
st0.(
init_rs) =
st1.(
init_rs)).
Inductive at_external:
state ->
Args.t ->
Prop :=
|
at_external_cstyle
fptr rs m0 m1 sg vs blk1 ofs init_rs
(
FPTR:
rs #
PC =
fptr)
(
EXTERNAL:
Genv.find_funct ge fptr =
None)
(
SIG:
exists skd,
skenv_link.(
Genv.find_funct)
fptr =
Some skd /\
Sk.get_csig skd =
Some sg)
(
RAPTR: <<
TPTR:
Val.has_type (
rs RA)
Tptr>> /\ <<
RADEF:
rs RA <>
Vundef>>)
(
VALS:
Asm.extcall_arguments rs m0 sg vs)
(
RSP:
rs RSP =
Vptr blk1 ofs)
(
ARGSRANGE:
Ptrofs.unsigned ofs + 4 *
size_arguments sg <=
Ptrofs.max_unsigned)
(
ALIGN:
forall chunk (
CHUNK:
size_chunk chunk <= 4 * (
size_arguments sg)),
(
align_chunk chunk |
ofs.(
Ptrofs.unsigned)))
(
FREE:
Mem.free m0 blk1 ofs.(
Ptrofs.unsigned) (
ofs.(
Ptrofs.unsigned) + 4 * (
size_arguments sg)) =
Some m1)
:
at_external (
mkstate init_rs (
State rs m0)) (
Args.Cstyle fptr vs m1)
|
at_external_asmstyle
fptr rs m0
init_rs
(
FPTR:
rs #
PC =
fptr)
(
EXTERNAL:
Genv.find_funct ge fptr =
None)
(
SIG:
exists skd,
skenv_link.(
Genv.find_funct)
fptr =
Some skd /\
Sk.get_csig skd =
None)
(
RAPTR: <<
TPTR:
Val.has_type (
rs RA)
Tptr>> /\ <<
RADEF:
rs RA <>
Vundef>>)
:
at_external (
mkstate init_rs (
State rs m0)) (
Args.Asmstyle rs m0)
.
Inductive initial_frame (
args:
Args.t):
state ->
Prop :=
|
initial_frame_cstyle
fd m0 rs sg targs n m1 fptr_arg vs_arg m_arg
(
SIG:
sg =
fd.(
fn_sig))
(
CSTYLE0:
sg.(
sig_cstyle) =
true)
(
CSTYLE:
args =
Args.Cstyle fptr_arg vs_arg m_arg)
(
FINDF:
Genv.find_funct ge fptr_arg =
Some (
Internal fd))
(
JUNK:
assign_junk_blocks m0 n =
m1)
(
RAPTR: <<
TPTR:
Val.has_type (
rs RA)
Tptr>> /\ <<
RADEF:
rs RA <>
Vundef>>)
(
RANOTFPTR:
forall blk ofs (
RAVAL:
rs RA =
Vptr blk ofs),
~
Plt blk (
Genv.genv_next skenv))
(
RSPC:
rs #
PC =
fptr_arg)
(
TYP:
typecheck vs_arg sg targs)
(
STORE:
store_arguments m_arg rs targs sg m0)
(
PTRFREE:
forall pr (
PTR: ~
is_junk_value m0 m1 (
rs pr)),
(<<
INARG:
exists mr,
(<<
MR:
to_mreg pr =
Some mr>>) /\
(<<
ARG:
In (
R mr) (
regs_of_rpairs (
loc_arguments sg))>>)>>) \/
(<<
INPC:
pr =
PC>>) \/
(<<
INRSP:
pr =
RSP>>)):
initial_frame args (
mkstate rs (
State rs m1))
|
initial_frame_asmstyle
fd ra n m1 rs_arg rs m_arg
(
SIG:
fd.(
fn_sig).(
sig_cstyle) =
false)
(
ASMSTYLE:
args =
Args.Asmstyle rs_arg m_arg)
(
FINDF:
Genv.find_funct ge (
rs_arg #
PC) =
Some (
Internal fd))
(
JUNK:
assign_junk_blocks m_arg n =
m1)
(
RAPTR: <<
TPTR:
Val.has_type ra Tptr>> /\ <<
RADEF:
ra <>
Vundef>>)
(
RANOTFPTR:
forall blk ofs (
RAVAL:
ra =
Vptr blk ofs),
~
Plt blk (
Genv.genv_next skenv))
(
RAJUNK:
is_junk_value m_arg m1 ra)
(
RS:
rs =
rs_arg #
RA <-
ra)
:
initial_frame args (
mkstate rs (
State rs m1))
.
Inductive final_frame:
state ->
Retv.t ->
Prop :=
|
final_frame_cstyle
(
init_rs rs:
regset)
m0 m1 blk sg mr
(
INITSIG:
exists fd,
ge.(
Genv.find_funct) (
init_rs #
PC) =
Some (
Internal fd) /\
fd.(
fn_sig) =
sg /\
sg.(
sig_cstyle) =
true)
(
EXTERNAL:
external_state ge (
rs #
PC))
(
RSRA:
rs #
PC =
init_rs #
RA)
(
RANOTFPTR:
Genv.find_funct skenv_link (
init_rs RA) =
None)
(
CALLEESAVE:
forall mr,
Conventions1.is_callee_save mr ->
Val.lessdef (
init_rs mr.(
to_preg)) (
rs mr.(
to_preg)))
(
INITRSP:
init_rs #
RSP =
Vptr blk Ptrofs.zero)
(
RSRSP:
rs #
RSP =
init_rs #
RSP)
(
FREE:
Mem.free m0 blk 0 (4 *
size_arguments sg) =
Some m1)
(
RETV:
loc_result sg =
One mr)
:
final_frame (
mkstate init_rs (
State rs m0)) (
Retv.Cstyle (
rs mr.(
to_preg))
m1)
|
final_frame_asmstyle
(
init_rs rs:
regset)
m0
(
INITSIG:
exists fd,
ge.(
Genv.find_funct) (
init_rs #
PC) =
Some (
Internal fd) /\
fd.(
fn_sig).(
sig_cstyle) =
false)
(
EXTERNAL:
external_state ge (
rs #
PC))
(
RSRA:
rs #
PC =
init_rs #
RA)
(
RANOTFPTR:
Genv.find_funct skenv_link (
init_rs RA) =
None)
:
final_frame (
mkstate init_rs (
State rs m0)) (
Retv.Asmstyle rs m0)
.
Inductive after_external:
state ->
Retv.t ->
state ->
Prop :=
|
after_external_cstyle
init_rs rs0 m0 rs1 m1 retv retv_v retv_m sg blk ofs
(
CSTYLE:
retv = (
Retv.Cstyle retv_v retv_m))
(
SIG:
exists skd,
skenv_link.(
Genv.find_funct) (
rs0 #
PC)
=
Some skd /\
Sk.get_csig skd =
Some sg)
(
RS:
rs1 = (
set_pair (
loc_external_result sg)
retv_v (
regset_after_external rs0)) #
PC <- (
rs0 RA))
(
RSRSP:
rs0 RSP =
Vptr blk ofs)
(
UNFREE:
Mem_unfree retv_m blk ofs.(
Ptrofs.unsigned) (
ofs.(
Ptrofs.unsigned) + 4 * (
size_arguments sg)) =
Some m1):
after_external (
mkstate init_rs (
State rs0 m0))
retv
(
mkstate init_rs (
State rs1 m1))
|
after_external_asmstyle
init_rs rs0 m0 rs1 retv retv_rs retv_m
(
ASMSTYLE:
retv = (
Retv.Asmstyle retv_rs retv_m))
(
SIG:
exists skd,
skenv_link.(
Genv.find_funct) (
rs0 #
PC) =
Some skd /\
Sk.get_csig skd =
None)
(
RS:
rs1 =
retv_rs #
PC <- (
rs0 #
RA))
:
after_external (
mkstate init_rs (
State rs0 m0))
retv
(
mkstate init_rs (
State rs1 retv_m)).
Program Definition modsem:
ModSem.t :=
{|
ModSem.step :=
step;
ModSem.at_external :=
at_external;
ModSem.initial_frame :=
initial_frame;
ModSem.final_frame :=
final_frame;
ModSem.after_external :=
after_external;
ModSem.globalenv :=
ge;
ModSem.skenv :=
skenv;
ModSem.skenv_link :=
skenv_link;
|}.
Next Obligation.
Next Obligation.
all: inv STEP; rewrite H2 in *; ss; des_ifs.
Qed.
Next Obligation.
all:
inv EXTERNAL;
unfold external_state in *;
des_ifs;
inv STEP;
ss;
des_ifs;
rewrite Heq in *;
clarify.
Qed.
Lemma modsem_receptive:
forall st,
receptive_at modsem st.
Proof.
econs;
eauto.
-
ii;
ss.
inv H.
destruct st0;
ss.
destruct s1;
ss.
clarify.
inv STEP;
try (
exploit external_call_receptive;
eauto;
check_safe;
intro T;
des);
try by (
inv_match_traces; (
eexists (
mkstate _ _);
econs; [
econs|];
eauto;
ss)).
-
ii.
inv H.
inv STEP;
try (
exploit external_call_trace_length;
eauto;
check_safe;
intro T;
des);
ss;
try xomega.
Qed.
Lemma modsem_determinate:
forall st,
determinate_at modsem st.
Proof.
econs;
eauto.
-
ii;
ss.
inv H;
inv H0.
destruct st0;
ss.
destruct s1;
ss.
destruct s2;
ss.
clarify.
inv STEP;
inv STEP0;
eq_closure_tac;
clarify_meq;
try (
determ_tac extcall_arguments_determ;
check_safe);
try (
determ_tac eval_builtin_args_determ;
check_safe);
try (
determ_tac external_call_determ;
check_safe);
esplits;
eauto;
try (
econs;
eauto);
ii;
eq_closure_tac;
clarify_meq.
-
ii.
inv H.
inv STEP;
try (
exploit external_call_trace_length;
eauto;
check_safe;
intro T;
des);
ss;
try xomega.
Qed.
End MODSEM.
Program Definition module (
p:
program):
Mod.t :=
{|
Mod.data :=
p;
Mod.get_sk :=
Sk.of_program fn_sig;
Mod.get_modsem :=
modsem; |}.