Require Import CoqlibC Maps.
Require Import ASTC Integers Floats Values MemoryC EventsC GlobalenvsC Smallstep.
Require Import Locations Stacklayout Conventions Linking.
newly added *
Require Export Csem Cop Ctypes Ctyping Csyntax Cexec.
Require Import Simulation Memory ValuesC.
Require Import Skeleton ModSem Mod sflib SemProps.
Require Import CtypesC CsemC Sem Syntax LinkingC Program.
Require Import BehaviorsC.
Require Import CtypingC.
Set Implicit Arguments.
Local Opaque Z.mul.
Definition is_external (
ge:
genv) (
s:
Csem.state) :
Prop :=
match s with
|
Csem.Callstate fptr ty args k m =>
match Genv.find_funct ge fptr with
|
Some f =>
match f with
|
External ef targs tres cconv =>
is_external_ef ef =
true
|
_ =>
False
end
|
None =>
False
end
|
_ =>
False
end.
Definition internal_function_state (
ge:
genv) (
s:
Csem.state) :
Prop :=
match s with
|
Csem.Callstate fptr ty args k m =>
match Genv.find_funct ge fptr with
|
Some f =>
match f with
|
Internal func =>
type_of_fundef f =
Tfunction Tnil type_int32s cc_default
|
_ =>
False
end
|
None =>
False
end
|
_ =>
False
end.
Section PRESERVATION.
Inductive my_eq {
A:
Type} (
x:
A):
A ->
Prop :=
|
my_eq_refl:
my_eq x x.
Notation "
a m=
b" := (
my_eq a b) (
at level 10).
Ltac Eq :=
match goal with
| [
H1: ?
a = ?
b,
H2: ?
a = ?
c |-
_ ] =>
rewrite H1 in H2;
inv H2;
Eq
| [
H1: ?
a m= ?
b,
H2: ?
a m= ?
c |-
_ ] =>
rewrite H1 in H2;
inv H2;
Eq
|
_ =>
idtac
end.
Section PLANB0.
linking ********************************
Variable prog:
Csyntax.program.
Let tprog :
Syntax.program :=
List.map CsemC.module [
prog].
genv ********************************
Variable sk_tgt:
Sk.t.
Hypothesis LINK_SK_TGT:
link_sk tprog =
Some sk_tgt.
Let skenv_link :=
Sk.load_skenv sk_tgt.
Hypothesis WTSK:
Sk.wf sk_tgt.
Let SKEWF:
SkEnv.wf skenv_link.
Proof.
Let ge :=
globalenv prog.
Let tge_ce :
composite_env :=
prog_comp_env prog.
Let tge :=
load_genv tprog skenv_link.
Hypothesis MAIN_INTERNAL:
forall st_src,
Csem.initial_state prog st_src ->
internal_function_state ge st_src.
Hypothesis WTPROG:
wt_program prog.
Hypothesis WT_EXTERNAL:
forall id ef args res cc vargs m t vres m',
In (
id,
Gfun (
External ef args res cc))
prog.(
prog_defs) ->
external_call ef skenv_link vargs m t vres m' ->
wt_retval vres res.
Hypothesis CSTYLE_EXTERN:
forall id ef tyargs ty cc,
In (
id, (
Gfun (
Ctypes.External ef tyargs ty cc)))
prog.(
prog_defs) ->
ef.(
ef_sig).(
sig_cstyle).
Definition local_genv (
p :
Csyntax.program) :=
(
skenv_link.(
SkEnv.project)
p.(
CSk.of_program signature_of_function)).(
SkEnv.revive)
p.
Inductive match_states :
Csem.state ->
Sem.state ->
nat ->
Prop :=
|
match_states_intro
fr (
st:
Csem.state)
(
FRAME:
fr =
Frame.mk (
CsemC.modsem skenv_link prog)
st):
match_states st (
Sem.State [
fr]) 1
|
match_states_call
fptr tyf vargs k m args fr (
st:
Csem.state)
cconv tres targs n
(
STATE:
st = (
Csem.Callstate fptr tyf vargs k m))
(
FRAME:
fr =
Frame.mk (
CsemC.modsem skenv_link prog)
st)
(
SIG:
exists skd,
skenv_link.(
Genv.find_funct)
fptr =
Some skd
/\
Some (
signature_of_type targs tres cconv) =
Sk.get_csig skd)
(
FPTR:
args.(
Args.fptr) =
fptr)
(
ARGS:
args.(
Args.vs) =
vargs)
(
MEM:
args.(
Args.m) =
m)
(
NOTPROG:
Genv.find_funct (
local_genv prog) (
Args.fptr args) =
None)
(
ORD:
n = 0%
nat):
match_states (
Csem.Callstate fptr tyf vargs k m) (
Callstate args [
fr])
n
|
match_states_init
st_src st_tgt
(
INITSRC:
Csem.initial_state prog st_src)
(
INITTGT:
initial_state tprog st_tgt):
match_states st_src st_tgt 0.
Let INCL:
SkEnv.includes (
Sk.load_skenv (
CSk.of_program signature_of_function prog)) (
CSk.of_program signature_of_function prog).
Proof.
init_memory ********************************
Variable m_init :
mem.
Hypothesis INIT_MEM:
sk_tgt.(
Sk.load_mem) =
Some m_init.
Definition m_src_init :=
m_init.
Lemma prog_sk_tgt:
CSk.of_program signature_of_function prog =
sk_tgt.
Proof.
Lemma SRC_INIT_MEM:
Genv.init_mem prog =
Some m_src_init.
Proof.
Lemma skenv_link_wf:
SkEnv.wf skenv_link.
Proof.
Lemma proj_wf:
SkEnv.project_spec skenv_link prog.(
CSk.of_program signature_of_function) (
SkEnv.project skenv_link prog.(
CSk.of_program signature_of_function)).
Proof.
Lemma match_ge_skenv_link :
Genv.match_genvs (
fun fdef skdef =>
skdef_of_gdef signature_of_function ((
globdef_of_globdef (
V:=
type))
fdef) =
skdef)
ge skenv_link.
Proof.
Lemma symb_preserved id:
Senv.public_symbol (
symbolenv (
sem tprog))
id =
Senv.public_symbol (
symbolenv (
semantics prog))
id.
Proof.
Lemma transf_initial_states:
forall st1,
Csem.initial_state prog st1 ->
exists st2,
Sem.initial_state tprog st2 /\
match_states st1 st2 0.
Proof.
transf step ********************************
Inductive valid_owner fptr (
p:
Csyntax.program) :
Prop :=
|
valid_owner_intro
fd
(
MSFIND:
tge.(
Ge.find_fptr_owner)
fptr (
CsemC.modsem skenv_link p))
(
FINDF:
Genv.find_funct (
local_genv p)
fptr =
Some (
Internal fd)).
Lemma find_fptr_owner_determ
fptr ms0 ms1
(
FIND0:
Ge.find_fptr_owner tge fptr ms0)
(
FIND1:
Ge.find_fptr_owner tge fptr ms1):
ms0 =
ms1.
Proof.
Lemma alloc_variables_determ
g e m
vars e2 m2
e2'
m2'
(
ALLOCV1:
alloc_variables g e m vars e2 m2)
(
ALLOCV2:
alloc_variables g e m vars e2'
m2'):
e2' =
e2 /\
m2' =
m2.
Proof.
generalize dependent g.
generalize dependent e2'.
generalize dependent m2'.
induction 1; i; inv ALLOCV2; auto.
rewrite H in H7. inv H7. eapply IHALLOCV1 in H8. auto.
Qed.
Notation "'
assign_loc'" := (
assign_loc skenv_link) (
only parsing).
Notation "'
bind_parameters'" := (
bind_parameters skenv_link) (
only parsing).
Notation "'
rred'" := (
rred skenv_link) (
only parsing).
Notation "'
estep'" := (
estep skenv_link) (
only parsing).
Lemma assign_loc_determ
g ty m b
ofs v tr m1 m1'
(
ASSIGN1:
assign_loc g ty m b ofs v tr m1)
(
ASSIGN2:
assign_loc g ty m b ofs v tr m1'):
m1 =
m1'.
Proof.
generalize dependent g.
generalize dependent m1'.
induction 1; i; inv ASSIGN2; f_equal; Eq; auto.
inv H1; inv H4. inv H5; inv H15; try congruence. Eq. auto.
Qed.
Lemma bind_parameters_determ
g env m l vl m1 m1'
(
BIND1:
bind_parameters g env m l vl m1)
(
BIND2:
bind_parameters g env m l vl m1'):
m1 =
m1'.
Proof.
generalize dependent g.
generalize dependent m1'.
induction 1;
i;
inv BIND2;
f_equal;
Eq;
auto.
determ_tac assign_loc_determ.
eapply IHBIND1;
eauto.
Qed.
aux lemmas ********************************
Lemma senv_equiv_ge_link:
Senv.equiv (
Genv.globalenv prog)
skenv_link.
Proof.
Lemma id_in_prog id:
defs prog id <->
In id (
prog_defs_names prog).
Proof.
Lemma id_not_in_prog id:
~
defs prog id <-> ~
In id (
prog_defs_names prog).
Proof.
Lemma not_prog_defmap_spec F V p id:
~
In id (
prog_defs_names p) <-> ~ (
exists g :
globdef F V, (
prog_defmap p) !
id =
Some g).
Proof.
Lemma var_info_same
blk g
(
VAR:
Genv.find_var_info (
Genv.globalenv prog)
blk =
Some g):
Genv.find_var_info (
local_genv prog)
blk =
Some g
.
Proof.
Lemma var_info_same'
blk g
(
VAR:
Genv.find_var_info (
local_genv prog)
blk =
Some g):
Genv.find_var_info (
Genv.globalenv prog)
blk =
Some g.
Proof.
Lemma volatile_block_same
blk b
(
VOLATILE:
Genv.block_is_volatile (
local_genv prog)
blk =
b):
Genv.block_is_volatile (
Genv.globalenv prog)
blk =
b.
Proof.
Lemma volatile_block_same'
blk b
(
VOLATILE:
Genv.block_is_volatile (
Genv.globalenv prog)
blk =
b):
Genv.block_is_volatile (
local_genv prog)
blk =
b.
Proof.
Lemma symbol_same id:
Genv.find_symbol (
local_genv prog)
id =
Genv.find_symbol (
Genv.globalenv prog)
id.
Proof.
Lemma public_same id:
Genv.public_symbol {|
genv_genv := (
local_genv prog);
genv_cenv :=
prog_comp_env prog |}
id =
Genv.public_symbol (
Genv.globalenv prog)
id.
Proof.
Lemma Senv_equiv1:
Senv.equiv (
Genv.globalenv prog) {|
genv_genv := (
local_genv prog);
genv_cenv :=
prog_comp_env prog |}.
Proof.
Lemma Senv_equiv2:
Senv.equiv {|
genv_genv := (
local_genv prog);
genv_cenv :=
prog_comp_env prog |} (
Genv.globalenv prog).
Proof.
Lemma volatile_load_same chunk m'
b ofs tr v:
volatile_load {|
genv_genv := (
local_genv prog);
genv_cenv :=
prog_comp_env prog |}
chunk
m'
b ofs tr v
<->
volatile_load (
globalenv prog)
chunk m'
b ofs tr v.
Proof.
Lemma deref_loc_same ty m'
b ofs tr v:
deref_loc {|
genv_genv := (
local_genv prog);
genv_cenv :=
prog_comp_env prog |}
ty m'
b ofs tr v
<->
deref_loc (
globalenv prog)
ty m'
b ofs tr v.
Proof.
Lemma volatile_store_same chunk m b ofs v tr m':
volatile_store
{|
genv_genv := (
local_genv prog);
genv_cenv :=
prog_comp_env prog |}
chunk m b ofs v tr m'
<->
volatile_store (
globalenv prog)
chunk m b ofs v tr m'.
Proof.
Lemma assign_loc_same ty m b ofs v tr m':
assign_loc
{|
genv_genv := (
local_genv prog);
genv_cenv :=
prog_comp_env prog |}
ty m b ofs v tr m'
<->
assign_loc (
globalenv prog)
ty m b ofs v tr m'.
Proof.
destruct match_ge_skenv_link.
split;
intro ASSIGN;
inv ASSIGN;
try (
by econs;
eauto);
econs 2;
eauto.
Qed.
Lemma bind_parameters_same e m1 params vl m2:
bind_parameters {|
genv_genv :=
local_genv prog;
genv_cenv :=
prog_comp_env prog |}
e m1 params vl m2
<->
bind_parameters (
globalenv prog)
e m1 params vl m2.
Proof.
Lemma lred_same e a m a'
m':
lred {|
genv_genv := (
local_genv prog);
genv_cenv :=
prog_comp_env prog |}
e a m a'
m'
<->
lred (
globalenv prog)
e a m a'
m'.
Proof.
Lemma rred_same
a m tr a'
m'
:
rred {|
genv_genv := (
local_genv prog);
genv_cenv :=
prog_comp_env prog |}
a m tr a'
m'
<->
rred (
globalenv prog)
a m tr a'
m'.
Proof.
Lemma estep_same
st_src tr st0
(
ESTEP:
estep
{|
genv_genv := (
local_genv prog);
genv_cenv :=
prog_comp_env prog |}
st_src tr st0):
estep (
globalenv prog)
st_src tr st0.
Proof.
destruct match_ge_skenv_link.
inv ESTEP;
ss;
try (
by econs;
eauto).
-
econs;
eauto.
rewrite <-
lred_same;
eauto.
-
econs 2;
eauto.
rewrite <-
rred_same;
eauto.
-
econs;
eauto.
unfold not in *.
i.
eapply H0.
inv H1;
try (
by econs);
ss.
+
econs;
eauto.
rewrite lred_same;
eauto.
+
econs 4;
eauto.
rewrite rred_same;
eauto.
+
econs 5;
eauto.
Qed.
Ltac o_bind_b :=
match goal with
| [
H : (
do id <- ?
stmt; ?
next) =
Some ?
f |-
_ ] =>
destruct stmt eqn:
SYMB;
clarify;
unfold o_bind in *;
ss
end.
Lemma def_same
b f
(
DEF:
Genv.find_def
{|
genv_genv := (
local_genv prog);
genv_cenv :=
prog_comp_env prog |}
b =
Some f):
Genv.find_def ge b =
Some f.
Proof.
Lemma function_find_same
fptr f
(
FUNC:
Genv.find_funct (
local_genv prog)
fptr =
Some f):
Genv.find_funct ge fptr =
Some f.
Proof.
Definition is_external_fd :=
fun (
F :
Type) (
f :
fundef) =>
match f with
|
Internal _ =>
false
|
External ef _ _ _ =>
is_external_ef ef
end.
Lemma not_external_function_find_same
f fptr
(
INTERN :
is_external_fd function f =
false)
(
FUNC :
Genv.find_funct (
Genv.globalenv prog)
fptr =
Some f):
Genv.find_funct (
local_genv prog)
fptr =
Some f.
Proof.
Notation "'
sstep'" := (
sstep skenv_link) (
only parsing).
Lemma sstep_same
st_src tr st0
(
SSTEP:
sstep
{|
genv_genv := (
local_genv prog);
genv_cenv :=
prog_comp_env prog |}
st_src tr st0):
sstep (
globalenv prog)
st_src tr st0.
Proof.
inv SSTEP;
ss;
try (
by econs;
eauto).
-
econs;
eauto.
+
exploit function_find_same;
eauto.
+
instantiate (1 :=
m1).
clear -
H0.
induction H0;
try (
by econs).
econs;
eauto.
+
induction H1;
try (
by econs).
econs;
eauto.
rewrite assign_loc_same in H2.
eauto.
rewrite bind_parameters_same in H3.
eauto.
-
econs;
eauto;
ss.
exploit function_find_same;
eauto.
Qed.
Lemma cstep_same
st_src tr st0
(
STEP:
Csem.step skenv_link
{|
genv_genv := (
local_genv prog);
genv_cenv :=
prog_comp_env prog |}
st_src tr st0):
Csem.step skenv_link (
globalenv prog)
st_src tr st0.
Proof.
Lemma system_internal
ptr fn_sig f
(
SYSCALL:
Genv.find_funct (
System.skenv skenv_link)
ptr =
Some (
AST.Internal fn_sig))
(
INTERNAL:
Genv.find_funct ge ptr =
Some (
Internal f)):
False.
Proof.
Lemma estep_progress
st_src tr st0
(
ESTEP:
estep (
globalenv prog)
st_src tr st0):
estep
{|
genv_genv := (
local_genv prog);
genv_cenv :=
prog_comp_env prog |}
st_src tr st0.
Proof.
destruct match_ge_skenv_link.
inv ESTEP;
try (
by econs;
eauto).
-
econs;
eauto.
rewrite lred_same;
eauto.
-
econs 2;
eauto.
rewrite rred_same;
eauto.
-
econs;
eauto.
unfold not in *.
i.
eapply H0.
inv H1;
try (
by econs);
ss.
+
econs;
eauto.
rewrite <-
lred_same;
eauto.
+
econs 4;
eauto.
rewrite <-
rred_same;
eauto.
+
econs 5;
eauto.
Qed.
Lemma sstep_progress
st_src tr st0
(
INTERN: ~
is_external ge st_src)
(
SSTEP:
sstep (
globalenv prog)
st_src tr st0):
sstep
{|
genv_genv := (
local_genv prog);
genv_cenv :=
prog_comp_env prog |}
st_src tr st0.
Proof.
Lemma senv_same : ((
Genv.globalenv prog):
Senv.t) = (
skenv_link:
Senv.t).
Proof.
Lemma progress_step
st_src frs n t st_src'
(
INTERN: ~
is_external ge st_src)
(
MTCHST :
match_states st_src (
State frs)
n)
(
STEP:
Step (
semantics prog)
st_src t st_src'):
exists (
tr :
trace) (
st_tgt1 :
Smallstep.state (
sem tprog)),
Step (
sem tprog) (
State frs)
tr st_tgt1.
Proof.
inv MTCHST;
inv STEP;
ss;
exists t.
-
esplits.
econs;
ss.
econs 1.
exploit estep_progress;
eauto.
rewrite <-
senv_same.
eauto.
-
esplits.
econs;
ss.
econs 2.
exploit sstep_progress;
eauto.
rewrite <-
senv_same.
eauto.
-
inv INITSRC;
inv INITTGT;
inv H.
-
inv INITSRC;
inv INITTGT;
inv H.
Qed.
Lemma init_case st args frs fptr tr st_src st_src'
(
STATE:
st =
Callstate args frs)
(
FPTR:
fptr =
args.(
Args.fptr))
(
MTCHST:
match_states st_src st 0)
(
SAFESRC:
Step (
semantics prog)
st_src tr st_src'):
(<<
CMOD:
valid_owner fptr prog>>) \/
(<<
SYSMOD:
tge.(
Ge.find_fptr_owner)
fptr (
System.modsem skenv_link)>>).
Proof.
Lemma prog_precise:
SkEnv.genv_precise (
SkEnv.revive (
SkEnv.project skenv_link (
CSk.of_program signature_of_function prog))
prog)
prog.
Proof.
Lemma preservation_prog
st0 tr st1
(
WT:
wt_state prog ge st0)
(
STEP:
Csem.step skenv_link ge st0 tr st1):
<<
WT:
wt_state prog ge st1>>.
Proof.
Lemma match_state_xsim:
forall st_src st_tgt n (
MTCHST:
match_states st_src st_tgt n) (
WTST:
wt_state prog ge st_src),
xsim (
Csem.semantics prog) (
Sem.sem tprog)
lt n%
nat st_src st_tgt.
Proof.
pcofix CIH.
i.
pfold.
destruct match_ge_skenv_link.
destruct st_tgt.
-
inversion MTCHST;
subst.
+
left.
right.
econs;
i.
econs;
i;
cycle 1.
*
inv FINALSRC.
*
econs;
i.
--
exploit init_case;
eauto.
i.
des.
{
inv CMOD.
clarify. }
assert (
CSTYLEARGS:
exists fptr vs m,
args =
Args.Cstyle fptr vs m).
{
inv SYSMOD;
ss.
destruct args;
ss.
eauto. }
des;
subst args;
econs;
i.
esplits.
++
left.
split;
cycle 1. {
--
econs.
++
i.
inv H;
inv H1;
ss;
clarify.
{
inv H0.
eexists.
econs 2.
eapply step_internal_function;
eauto. }
{
exploit external_call_receptive;
eauto.
i.
des.
eexists.
econs 2.
eapply step_external_function;
eauto. }
++
red.
i.
inv H;
inv H0;
ss;
clarify;
auto.
exploit external_call_trace_length;
eauto. }
eapply plus_left'.
**
econs;
i.
---
econs;
i.
{
inv H;
inv H0.
split.
econs.
i.
ss.
dup LINK_SK_TGT.
unfold tge,
skenv_link,
link_sk,
link_list in LINK_SK_TGT0,
SYSMOD;
inversion LINK_SK_TGT0.
rewrite ->
H1 in *.
unfold Args.get_fptr in *.
des_ifs.
determ_tac find_fptr_owner_determ.
subst ms0.
exploit find_fptr_owner_determ.
unfold tge,
skenv_link,
link_sk,
link_list.
rewrite <-
H1 in *.
eapply MSFIND.
unfold tge,
skenv_link,
link_sk,
link_list.
rewrite <-
H1 in *.
eapply MSFIND0.
i.
subst ms.
rewrite H1.
auto.
inversion INIT0;
inversion INIT.
rewrite CSTYLE in *.
clarify.
rewrite H5.
rewrite H6.
rewrite H7.
eauto. }
{
inv FINAL. }
{
red.
i.
inv H.
auto. }
---
eapply step_init;
ss.
{
unfold Args.get_fptr.
des_ifs.
unfold tge,
skenv_link,
link_sk,
link_list in *;
inversion LINK_SK_TGT.
rewrite H0.
eauto. }
{
ss. }
**
inv STEPSRC;
inv H.
{
ss.
exploit not_external_function_find_same;
eauto;
ss.
i.
unfold local_genv in *.
Eq. }
eapply plus_left'.
---
econs;
i.
+++
econs;
i.
{
inv H;
inv H0;
try (
by ss);
try (
by inv FINAL).
inv STEP;
inv STEP0;
ss.
rewrite FPTR1 in FPTR0.
inv FPTR0.
exploit external_call_determ.
eapply EXTCALL.
eapply EXTCALL0.
i.
des.
splits;
eauto.
{
eapply match_traces_le;
eauto.
ii.
destruct senv_equiv_ge_link.
des.
rewrite symb_preserved.
rewrite <-
H2.
auto. }
{
i.
subst.
exploit H0;
eauto.
i.
des.
rewrite H1.
rewrite H2.
eauto. } }
{
inv FINAL. }
{
red.
i.
inv H;
auto.
inv STEP.
exploit external_call_trace_length;
eauto. }
+++
instantiate (2 :=
tr).
eapply step_internal.
ss.
instantiate (1 := (
System.Returnstate vres m')).
econs;
ss.
{
instantiate (1 :=
ef).
unfold System.globalenv.
unfold Genv.find_funct in *.
des_ifs.
rewrite Genv.find_funct_ptr_iff in *.
specialize (
mge_defs b).
inv mge_defs;
unfold Genv.find_def in *;
unfold fundef.
{
rewrite SIG in H.
inv H. }
unfold fundef in *.
rewrite FPTR in H.
inv H;
ss. }
unfold System.globalenv.
exploit external_call_symbols_preserved;
eauto.
eapply senv_equiv_ge_link.
---
eapply plus_one.
instantiate (2:=
E0).
econs;
i.
+++
econs;
i.
{
inv H;
inv H0;
try (
by ss);
try (
by inv FINAL;
inv AFTER;
inv STEP).
-
inv STEP;
inv STEP0.
-
inv FINAL;
inv FINAL0.
inv AFTER;
inv AFTER0.
split;
eauto.
{
econs. }
{
ii;
ss.
repeat f_equal.
des.
determ_tac typify_c_dtm. } }
{
inv FINAL. }
{
red.
i.
inv H;
auto.
inv STEP. }
+++
ss.
eapply step_return.
{
instantiate (1 := (
Retv.mk vres m')).
econs. }
ss.
assert (
after_external (
Csem.Callstate fptr (
Tfunction targs0 tres0 cc)
vs k m)
(
Retv.mk vres m') (
Returnstate vres k m')).
{
econs.
ss.
econs.
ss.
unfold Genv.find_funct in FPTR.
des_ifs.
rewrite Genv.find_funct_ptr_iff in *.
exploit Genv.find_def_inversion;
eauto.
i.
des.
exploit WT_EXTERNAL.
eauto.
exploit external_call_symbols_preserved.
eapply senv_equiv_ge_link.
eauto.
i.
eauto.
i.
eauto. }
eauto.
---
traceEq.
**
traceEq.
++
right.
eapply CIH.
{
econs.
ss. }
{
ss.
eapply preservation_prog;
eauto.
rewrite <-
senv_same.
et. }
+
inversion INITSRC;
subst;
ss.
left.
right.
econs;
i.
econs;
i;
cycle 1.
*
inv FINALSRC.
*
econs;
i;
cycle 1.
--
exploit init_case;
eauto.
i.
des.
++
inv CMOD;
ss.
inversion STEPSRC;
inv H3;
cycle 1.
**
exploit MAIN_INTERNAL;
eauto.
intro INTERN.
inv MSFIND;
ss.
des_ifs.
**
esplits.
---
left.
split;
cycle 1. {
--
econs;
i.
++
inv H3;
inv H5.
{
inv H4.
eexists.
econs 2.
eapply step_internal_function;
eauto. }
{
exploit external_call_receptive;
eauto.
i.
des.
eexists.
econs 2.
eapply step_external_function;
eauto. }
++
red.
i.
inv H3;
inv H4;
auto.
exploit external_call_trace_length;
eauto.
}
eapply plus_two.
econs;
i.
+++
econs;
i.
{
inv H3;
inv H4.
split.
econs.
i.
ss.
dup LINK_SK_TGT.
unfold tge,
skenv_link,
link_sk,
link_list in LINK_SK_TGT0;
inversion LINK_SK_TGT0.
rewrite ->
H5 in *.
dup LINK_SK_TGT.
unfold Args.get_fptr in *.
destruct args;
ss.
exploit find_fptr_owner_determ.
unfold tge.
eauto.
eapply MSFIND.
i.
generalize dependent st_init0.
subst ms0.
exploit find_fptr_owner_determ.
unfold tge.
eapply MSFIND0.
eauto.
i.
des.
subst ms.
ss.
inversion INIT0;
inversion INIT.
auto.
rewrite FINDF0 in FINDF1.
inversion FINDF1.
subst fd0.
rewrite TYPE0 in TYPE1.
rewrite TYPE1 in *.
auto. }
{
inv FINAL. }
{
red.
i.
inv H3.
auto. }
+++
ss.
eapply step_init.
{
instantiate (1 :=
modsem skenv_link prog).
ss.
unfold tge in MSFIND.
unfold tge,
skenv_link,
link_sk,
link_list in *.
des_ifs.
inversion Heq.
rewrite <-
H4 in MSFIND.
unfold Args.get_fptr.
des_ifs. }
ss.
des_ifs.
instantiate (1 := (
Csem.Callstate (
Vptr b Ptrofs.zero) (
Tfunction Tnil type_int32s cc_default) []
Kstop m0)).
assert (
Genv.symbol_address (
Sk.load_skenv sk_tgt) (
AST.prog_main sk_tgt)
Ptrofs.zero = (
Vptr b Ptrofs.zero)).
{
destruct match_ge_skenv_link.
specialize (
mge_symb (
prog_main prog)).
destruct senv_equiv_ge_link;
ss.
unfold Genv.symbol_address.
des_ifs.
-
unfold fundef in *.
rewrite H3 in Heq.
rewrite <-
prog_sk_tgt in *;
ss.
rewrite H0 in Heq.
clarify.
-
unfold fundef in *.
rewrite H3 in Heq.
rewrite <-
prog_sk_tgt in *;
ss.
rewrite H0 in Heq.
clarify. }
assert (
Genv.init_mem prog =
Some m_init).
{
eapply SRC_INIT_MEM. }
unfold Sk.load_mem in *.
Eq.
clarify.
inv INITTGT;
ss;
unfold Sk.load_mem in *.
rewrite LINK_SK_TGT in INITSK.
inversion INITSK.
rewrite <-
H5 in *.
rewrite INIT_MEM in INITMEM.
inversion INITMEM.
rewrite <-
H6 in *.
rewrite H3.
econs;
ss;
des_ifs;
eauto.
{
unfold fundef in *.
exploit (@
not_external_function_find_same (
Internal f) (
Vptr b Ptrofs.zero));
eauto. }
{
unfold type_of_function in *.
clarify.
destruct (
fn_params f)
eqn:
T;
ss;
des_ifs.
econs;
ss. }
+++
econs;
i.
***
econs;
i.
{
inv H3;
inv H4;
ss;
try (
by ss);
try (
by inv FINAL).
-
inv AT;
inv AT0.
ss.
-
inv AT.
ss.
-
inv AT.
ss.
-
inv STEP;
inv STEP0;
inv H3;
inv H4;
ss;
des_ifs.
+
des_ifs.
exploit alloc_variables_determ.
eapply H16.
eauto.
i.
des.
subst.
exploit bind_parameters_determ.
eapply H17.
eapply H19.
i.
subst.
split; [
apply match_traces_E0 |
i;
auto].
+
unfold fundef in *.
exploit (@
not_external_function_find_same (
Internal f) (
Vptr b Ptrofs.zero));
eauto.
i.
ss.
des_ifs.
unfold local_genv in *.
des_ifs. }
{
inv STEP;
inv FINAL;
inv FINAL0. }
{
red.
i.
inv H3;
auto.
inv STEP;
inv H3;
auto.
exploit external_call_trace_length;
eauto. }
***
instantiate (2:=
E0).
eapply step_internal.
ss.
econs 2.
inv STEPSRC;
inv H3.
des_ifs.
instantiate (1 := (
Csem.State f (
fn_body f)
Kstop e m2)).
eapply step_internal_function;
ss;
eauto.
{
des_ifs.
unfold fundef in *.
exploit (@
not_external_function_find_same (
Internal f) (
Vptr b Ptrofs.zero));
eauto. }
{
instantiate (1 :=
m3).
clear -
INIT_MEM m_init ge LINK_SK_TGT tprog H17.
induction H17;
try (
by econs).
econs;
eauto. }
{
clear -
INCL WT_EXTERNAL WTPROG MAIN_INTERNAL SKEWF WTSK INIT_MEM m_init ge LINK_SK_TGT tprog H18.
induction H18;
try (
by econs).
econs;
eauto.
unfold fundef in *.
rewrite senv_same in H0.
rewrite <-
assign_loc_same in H0.
eauto. }
+++
traceEq.
---
right.
eapply CIH.
{
ss.
instantiate (1:= 1%
nat).
inv INITTGT.
eapply match_states_intro.
ss. }
{
ss.
eapply preservation_prog;
eauto.
rewrite <-
senv_same;
et. }
++
inv SYSMOD.
inv INITTGT.
ss.
assert (
SAME:
sk_tgt =
sk_link)
by (
Eq;
auto).
clear INITSK.
exploit MAIN_INTERNAL;
eauto.
i.
unfold internal_function_state in H3.
assert (
Genv.symbol_address (
Sk.load_skenv sk_tgt) (
AST.prog_main sk_tgt)
Ptrofs.zero = (
Vptr b Ptrofs.zero)).
{
des_ifs.
destruct match_ge_skenv_link.
specialize (
mge_symb (
prog_main prog)).
unfold Genv.find_symbol,
skenv_link,
Genv.symbol_address in *.
rewrite <-
prog_sk_tgt in *.
unfold Genv.find_symbol in *.
des_ifs;
ss;
unfold fundef in *;
rewrite mge_symb in Heq0;
Eq;
auto. }
destruct (
Genv.find_funct ge (
Vptr b Ptrofs.zero))
eqn:
HFUNC;
ss.
destruct f.
ss.
exploit system_internal;
eauto;
clarify.
des_ifs.
rewrite SAME in *.
rewrite H4 in *.
unfold fundef in *.
eauto.
i.
clarify.
-
right.
econs;
i;
ss.
+
inv MTCHST.
*
inv FINALTGT.
inv FINAL.
ss.
subst.
esplits.
{
eapply star_refl. }
econs.
*
inv INITTGT.
+
econs;
i.
*
inv MTCHST;
cycle 1.
{
inv INITTGT. }
inv STEPTGT;
ss.
--
inv AT;
ss.
des.
esplits.
++
right.
splits;
auto.
eapply star_refl.
++
right.
eapply CIH.
{
econs;
eauto. }
{
ss. }
--
assert(
STEPSRC:
Csem.step skenv_link (
globalenv prog)
st_src tr st0).
{
exploit cstep_same;
eauto. }
esplits.
++
left.
eapply plus_one.
unfold fundef in *.
rewrite senv_same.
eauto.
++
right.
eapply CIH.
{
econs;
eauto. }
{
ss.
eapply preservation_prog;
eauto. }
*
specialize (
SAFESRC _ (
star_refl _ _ _ _)).
des.
--
inv SAFESRC;
inv MTCHST;
cycle 1.
{
inv INITTGT. }
left.
exists r0.
econs;
ss.
--
destruct (
classic (
is_external ge st_src)).
++
right.
inv SAFESRC;
inv H0;
ss;
des_ifs.
inv MTCHST;
cycle 1.
{
inv INITTGT. }
set ef as XX.
exists E0.
esplits.
eapply step_call;
ss.
econs.
{
unfold Genv.find_funct.
des_ifs.
unfold Genv.find_funct_ptr.
des_ifs.
eapply CSkEnv.project_revive_no_external in Heq0;
clarify;
cycle 1.
{
rpapply link_includes;
et.
{
ss.
left.
et. }
ss. }
ss.
des_ifs.
rewrite Genv.find_funct_ptr_iff in Heq.
exploit def_same;
eauto.
i.
unfold ge in H0.
ss.
Eq.
ss. }
{
exists (
External ef targs tres cc);
ss.
splits.
{
unfold Genv.find_funct in *.
des_ifs.
rewrite Genv.find_funct_ptr_iff in *.
destruct match_ge_skenv_link.
specialize (
mge_defs b).
inv mge_defs;
unfold Genv.find_def in *;
ss.
-
unfold fundef in *.
rewrite <-
H2 in Heq.
clarify.
-
assert (
x = (
Gfun (
External ef targs tres cc))).
{
unfold fundef in *.
rewrite <-
H0 in Heq.
clarify. }
subst.
ss. }
exploit Genv.find_funct_inversion;
eauto.
i;
des.
f_equal.
inv WTPROG.
exploit CSTYLE_EXTERN;
eauto.
i.
des_ifs.
f_equal.
eapply H3;
eauto. }
{
inv WTST;
ss.
exploit WTKS;
eauto. {
ii.
clarify. }
esplits;
ss;
eauto.
rr.
des.
des_ifs. }
++
exploit progress_step;
eauto.
Qed.
Lemma transf_xsim_properties:
xsim_properties (
Csem.semantics prog) (
Sem.sem tprog)
nat lt.
Proof.
Lemma transf_program_correct:
mixed_simulation (
Csem.semantics prog) (
Sem.sem tprog).
Proof.
End PLANB0.
End PRESERVATION.
Theorem upperbound_b_correct
builtins
(
cprog:
Csyntax.program)
(
MAIN:
exists main_f,
(<<
INTERNAL:
cprog.(
prog_defmap) ! (
cprog.(
prog_main)) =
Some (
Gfun (
Internal main_f))>>)
/\
(<<
SIG:
type_of_function main_f =
Tfunction Tnil type_int32s cc_default>>))
(
TYPED:
typechecked builtins cprog):
(<<
REFINE:
improves (
Csem.semantics cprog) (
Sem.sem (
map CsemC.module [
cprog]))>>).
Proof.