Correctness of instruction selection
Require Import Coqlib Maps.
Require Import AST Linking Errors Integers Values Memory Events Globalenvs Smallstep.
Require Import Switch Cminor Op CminorSel.
Require Import SelectOp SelectDiv SplitLong SelectLong Selection.
Require Import SelectOpproof SelectDivproof SplitLongproof SelectLongproof.
Require Import CUAST Footprint Blockset LDSimDefs_local LDSim_local.
Require Import InteractionSemantics IS_local val_casted InjRels
MemOpFP Op_fp Cminor_op_footprint Cminor_local CminorSel_local
selectop_proof selectdiv_proof splitlong_proof selectlong_proof
selection.
Local Notation empfp:=
FP.emp.
Local Notation footprint:=
FP.t.
Local Open Scope cminorsel_scope.
Local Open Scope error_monad_scope.
Relational specification of instruction selection
Definition match_fundef (
scu:
cminor_comp_unit) (
f:
Cminor.fundef) (
tf:
CminorSel.fundef) :
Prop :=
exists hf,
helper_functions_declared scu hf /\
sel_fundef (
comp_unit_defmap scu)
hf f =
OK tf.
Definition match_cu (
scu:
cminor_comp_unit) (
tcu:
cminorsel_comp_unit) :=
match_comp_unit_gen (
match_fundef scu)
eq scu tcu.
Lemma record_globdefs_sound:
forall dm id gd, (
record_globdefs dm)!
id =
Some gd ->
dm!
id =
Some gd.
Proof.
Lemma lookup_helper_correct_1:
forall globs name sg id,
lookup_helper globs name sg =
OK id ->
globs!
id =
Some (
Gfun (
External (
EF_runtime name sg))).
Proof.
Lemma lookup_helper_correct:
forall cu name sg id,
lookup_helper (
record_globdefs (
comp_unit_defmap cu))
name sg =
OK id ->
helper_declared cu id name sg.
Proof.
Lemma get_helpers_correct:
forall cu hf,
get_helpers (
comp_unit_defmap cu) =
OK hf ->
helper_functions_declared cu hf.
Proof.
Theorem transf_program_match:
forall scu tcu,
transf_program scu =
OK tcu ->
match_cu scu tcu.
Proof.
Correctness of the instruction selection functions for expressions
Section PRESERVATION.
Variable scu:
cminor_comp_unit.
Variable tcu:
cminorsel_comp_unit.
Variable sge:
Cminor.genv.
Variable tge:
CminorSel.genv.
Hypothesis SGEINIT:
globalenv_generic scu sge.
Hypothesis TGEINIT:
globalenv_generic tcu tge.
Hypothesis S_EQ:
sge.(
Genv.genv_next) =
tge.(
Genv.genv_next).
Hypothesis TRANSF:
match_cu scu tcu.
Lemma ge_match:
ge_match_strict sge tge.
Proof.
Lemma genv_match:
Genv.match_genvs (
match_globdef (
fun f tf =>
match_fundef scu f tf)
eq)
sge tge.
Proof.
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol sge s.
Proof.
Lemma senv_preserved:
Senv.equiv sge tge.
Proof.
Lemma function_ptr_translated:
forall (
b:
block) (
f:
Cminor.fundef),
Genv.find_funct_ptr sge b =
Some f ->
exists tf,
Genv.find_funct_ptr tge b =
Some tf /\
match_fundef scu f tf.
Proof.
Lemma functions_translated:
forall v v'
f,
Genv.find_funct sge v =
Some f ->
Val.lessdef v v' ->
exists tf,
Genv.find_funct tge v' =
Some tf /\
match_fundef scu f tf.
Proof.
Lemma sig_function_translated:
forall f tf,
match_fundef scu f tf ->
funsig tf =
Cminor.funsig f.
Proof.
intros. destruct H as (hf & P & Q). destruct f; monadInv Q; auto. monadInv EQ; auto.
Qed.
Lemma stackspace_function_translated:
forall dm hf f tf,
sel_function dm hf f =
OK tf ->
fn_stackspace tf =
Cminor.fn_stackspace f.
Proof.
intros. monadInv H. auto. Qed.
Lemma helper_functions_preserved:
forall hf,
helper_functions_declared scu hf ->
helper_functions_declared tcu hf.
Proof.
Section CMCONSTR.
Variable hf:
helper_functions.
Hypothesis HF:
helper_functions_declared scu hf.
Let HF':
helper_functions_declared tcu hf.
Proof.
Variable sp:
val.
Variable e:
env.
Variable m:
mem.
Lemma eval_condexpr_of_expr_fp:
forall a le v fp b,
eval_expr tge sp e m le a v ->
eval_expr_fp tge sp e m le a fp ->
Val.bool_of_val v b ->
eval_condexpr tge sp e m le (
condexpr_of_expr a)
b /\
eval_condexpr_fp tge sp e m le (
condexpr_of_expr a)
fp.
Proof.
intros until a.
functional induction (
condexpr_of_expr a);
intros.
compare *)
inv H.
inv H0.
eqexpr.
simpl in H7,
H9.
destruct (
eval_condition)
eqn:
EC;[
inv H7|
discriminate].
assert (
b0 =
b)
by (
destruct b0;
inv H1;
auto).
subst.
split;
econstructor;
eauto.
condition *)
inv H.
inv H0.
eqexpr.
destruct va0; [
exploit IHc|
exploit IHc0];
eauto;
intros [
EC ECFP];
split;
econstructor;
eauto.
let *)
inv H.
inv H0.
eqexpr.
exploit IHc;
eauto.
intros [
EC ECFP].
split;
econstructor;
eauto.
default *)
inv H1.
split;
repeat econstructor;
simpl;
eauto.
simpl.
eauto.
simpl.
eauto.
TrivFP.
Qed.
Lemma eval_load_fp:
forall le a v fp chunk v',
eval_expr tge sp e m le a v ->
eval_expr_fp tge sp e m le a fp ->
Mem.loadv chunk m v =
Some v' ->
eval_expr tge sp e m le (
load chunk a)
v' /\
eval_expr_fp tge sp e m le (
load chunk a) (
FP.union (
loadv_fp chunk v)
fp).
Proof.
Lemma eval_store_fp:
forall chunk a1 a2 v1 v2 fp1 fp2 f k m',
eval_expr tge sp e m nil a1 v1 ->
eval_expr_fp tge sp e m nil a1 fp1 ->
eval_expr tge sp e m nil a2 v2 ->
eval_expr_fp tge sp e m nil a2 fp2 ->
Mem.storev chunk m v1 v2 =
Some m' ->
step tge (
Core_State f (
store chunk a1 a2)
k sp e)
m
(
FP.union (
FP.union fp1 fp2) (
storev_fp chunk v1)) (
Core_State f Sskip k sp e)
m'.
Proof.
intros.
generalize H3;
destruct v1;
simpl;
intro;
try discriminate.
unfold store.
generalize (
eval_addressing_fp _ _ _ _ _ chunk _ _ _ _ _ H H0 (
refl_equal _)).
destruct (
addressing chunk a1).
intros [
vl [
EV [
EF EQ]]].
eapply step_store;
eauto.
Qed.
Correctness of instruction selection for operators
Ltac uopexploit H1 H2:=
let v :=
fresh in
let A :=
fresh in
let B :=
fresh in
exploit H1;
try exacteval H2;
eauto;
intros [
v [
A B]];
evalge A.
Lemma eval_sel_unop_fp:
forall le op a1 v1 fp v,
eval_expr tge sp e m le a1 v1 ->
eval_expr_fp tge sp e m le a1 fp ->
eval_unop op v1 =
Some v ->
(
exists v',
eval_expr tge sp e m le (
sel_unop op a1)
v' /\
Val.lessdef v v') /\
(
exists fp',
eval_expr_fp tge sp e m le (
sel_unop op a1)
fp' /\
FP.subset fp'
fp).
Proof.
Let tprog :=
mkprogram (
cu_defs tcu) (
cu_public tcu) 1%
positive.
Ltac bexploit1 T1 H1 H2 :=
(
exploit T1; [
exact H1|
exact H2|]) || (
exploit T1; [
exact H1|
exact H2| |]).
Ltac bexploit2 T1 H1 H2 :=
((
exploit (
T1 tprog);
subst tprog; [
exacteval H1|
exacteval H2|])
|| (
exploit (
T1 tprog);
subst tprog; [
exacteval H1|
exacteval H2| | ])
|| (
exploit (
T1 tprog);
subst tprog; [|
exacteval H1|
exacteval H2| ])
|| (
exploit (
T1 tprog);
subst tprog; [|
exacteval H1|
exacteval H2| | ])).
Ltac bexploit T1 T2:=
match goal with
| [
H1: (
eval_expr _ _ _ _ _ ?
a1 _),
H2: (
eval_expr _ _ _ _ _ ?
a2 _)
|-
context[(
_ ?
a1 ?
a2)] ]
=> (((
bexploit2 T1 H1 H2);
eauto;
intros [?
v [?
A ?
B]];
evalge A)
|| ((
bexploit1 T1 H1 H2);
eauto;
intros [?
v [?
A ?
B]]));
split; [
eauto|
try eapply T2;
eauto];
try (
exploit T2; [
exact H1|
eauto|
exact H2|
eauto|
eauto|];
simpl;
TrivFP;
fail)
end.
Lemma eval_sel_binop_fp:
forall le op a1 a2 v1 v2 fp1 fp2 v fp,
eval_expr tge sp e m le a1 v1 ->
eval_expr_fp tge sp e m le a1 fp1 ->
eval_expr tge sp e m le a2 v2 ->
eval_expr_fp tge sp e m le a2 fp2 ->
eval_binop op v1 v2 m =
Some v ->
eval_binop_fp op v1 v2 m =
Some fp ->
(
exists v',
eval_expr tge sp e m le (
sel_binop op a1 a2)
v' /\
Val.lessdef v v') /\
(
exists fp',
eval_expr_fp tge sp e m le (
sel_binop op a1 a2)
fp' /\
FP.subset fp' (
FP.union (
FP.union fp1 fp2)
fp)).
Proof.
End CMCONSTR.
Recognition of calls to built-in functions
TODO: modified spec.. could be useless
Lemma expr_is_addrof_ident_correct:
forall e id,
expr_is_addrof_ident e =
Some id ->
e =
Cminor.Econst (
Cminor.Oaddrsymbol id Ptrofs.zero).
Proof.
Lemma classify_call_correct:
forall sp e m a v fd,
Cminor.eval_expr sge sp e m a v ->
Genv.find_funct sge v =
Some fd ->
match classify_call (
comp_unit_defmap scu)
a with
|
Call_default =>
True
|
Call_imm id =>
exists b,
Genv.find_symbol sge id =
Some b /\
v =
Vptr b Ptrofs.zero
|
Call_builtin ef =>
fd =
External ef
end.
Proof.
Translation of switch statements
Inductive Rint:
Z ->
val ->
Prop :=
|
Rint_intro:
forall n,
Rint (
Int.unsigned n) (
Vint n).
Inductive Rlong:
Z ->
val ->
Prop :=
|
Rlong_intro:
forall n,
Rlong (
Int64.unsigned n) (
Vlong n).
Section SEL_SWITCH.
Variable make_cmp_eq:
expr ->
Z ->
expr.
Variable make_cmp_ltu:
expr ->
Z ->
expr.
Variable make_sub:
expr ->
Z ->
expr.
Variable make_to_int:
expr ->
expr.
Variable modulus:
Z.
Variable R:
Z ->
val ->
Prop.
Hypothesis no_ptr:
forall z v b i,
R z v ->
v <>
Vptr b i.
Hypothesis eval_make_cmp_eq:
forall sp e m le a v i n,
eval_expr tge sp e m le a v ->
R i v -> 0 <=
n <
modulus ->
eval_expr tge sp e m le (
make_cmp_eq a n) (
Val.of_bool (
zeq i n)).
Hypothesis eval_make_cmp_eq_fp:
forall sp e m le a v fp i n,
eval_expr tge sp e m le a v ->
eval_expr_fp tge sp e m le a fp ->
R i v -> 0 <=
n <
modulus ->
exists fp',
eval_expr_fp tge sp e m le (
make_cmp_eq a n)
fp' /\
FP.subset fp'
fp.
Hypothesis eval_make_cmp_ltu:
forall sp e m le a v i n,
eval_expr tge sp e m le a v ->
R i v -> 0 <=
n <
modulus ->
eval_expr tge sp e m le (
make_cmp_ltu a n) (
Val.of_bool (
zlt i n)).
Hypothesis eval_make_cmp_ltu_fp:
forall sp e m le a v fp i n,
eval_expr tge sp e m le a v ->
eval_expr_fp tge sp e m le a fp ->
R i v -> 0 <=
n <
modulus ->
exists fp',
eval_expr_fp tge sp e m le (
make_cmp_ltu a n)
fp' /\
FP.subset fp'
fp.
Hypothesis eval_make_sub:
forall sp e m le a v i n,
eval_expr tge sp e m le a v ->
R i v -> 0 <=
n <
modulus ->
exists v',
eval_expr tge sp e m le (
make_sub a n)
v' /\
R ((
i -
n)
mod modulus)
v'.
Hypothesis eval_make_sub_fp:
forall sp e m le a v fp i n,
eval_expr tge sp e m le a v ->
eval_expr_fp tge sp e m le a fp ->
R i v -> 0 <=
n <
modulus ->
exists fp',
eval_expr_fp tge sp e m le (
make_sub a n)
fp' /\
FP.subset fp'
fp.
Hypothesis eval_make_to_int:
forall sp e m le a v i,
eval_expr tge sp e m le a v ->
R i v ->
exists v',
eval_expr tge sp e m le (
make_to_int a)
v' /\
Rint (
i mod Int.modulus)
v'.
Hypothesis eval_make_to_int_fp:
forall sp e m le a v fp i,
eval_expr tge sp e m le a v ->
eval_expr_fp tge sp e m le a fp ->
R i v ->
exists fp',
eval_expr_fp tge sp e m le (
make_to_int a)
fp' /\
FP.subset fp'
fp.
Ltac exactcond A :=
eapply eval_condexpr_preserved;
try exact A;
try gegen;
eauto with gegen.
Lemma sel_switch_correct_rec_fp:
forall sp e m varg i x,
R i varg ->
forall t arg le,
wf_comptree modulus t ->
nth_error le arg =
Some varg ->
comptree_match modulus i t =
Some x ->
eval_exitexpr tge sp e m le (
sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int arg t)
x /\
eval_exitexpr_fp tge sp e m le (
sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int arg t)
empfp.
Proof.
Lemma sel_switch_correct_fp:
forall dfl cases arg sp e m varg fp i t le,
validate_switch modulus dfl cases t =
true ->
eval_expr tge sp e m le arg varg ->
eval_expr_fp tge sp e m le arg fp ->
R i varg ->
0 <=
i <
modulus ->
eval_exitexpr tge sp e m le
(
XElet arg (
sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int O t))
(
switch_target i dfl cases) /\
eval_exitexpr_fp tge sp e m le
(
XElet arg (
sel_switch make_cmp_eq make_cmp_ltu make_sub make_to_int O t))
fp .
Proof.
End SEL_SWITCH.
Lemma sel_switch_int_correct_fp:
forall dfl cases arg sp e m i fp t le,
validate_switch Int.modulus dfl cases t =
true ->
eval_expr tge sp e m le arg (
Vint i) ->
eval_expr_fp tge sp e m le arg fp ->
eval_exitexpr tge sp e m le (
XElet arg (
sel_switch_int O t)) (
switch_target (
Int.unsigned i)
dfl cases) /\
eval_exitexpr_fp tge sp e m le (
XElet arg (
sel_switch_int O t))
fp.
Proof.
Lemma sel_switch_long_correct_fp:
forall dfl cases arg sp e m i fp t le,
validate_switch Int64.modulus dfl cases t =
true ->
eval_expr tge sp e m le arg (
Vlong i) ->
eval_expr_fp tge sp e m le arg fp ->
eval_exitexpr tge sp e m le (
XElet arg (
sel_switch_long O t)) (
switch_target (
Int64.unsigned i)
dfl cases) /\
eval_exitexpr_fp tge sp e m le (
XElet arg (
sel_switch_long O t))
fp.
Proof.
Compatibility of evaluation functions with the "less defined than" relation.
Ltac TrivialExists :=
match goal with
| [ |-
exists v,
Some ?
x =
Some v /\
_ ] =>
exists x;
split;
auto
|
_ =>
idtac
end.
Lemma eval_unop_lessdef:
forall op v1 v1'
v,
eval_unop op v1 =
Some v ->
Val.lessdef v1 v1' ->
exists v',
eval_unop op v1' =
Some v' /\
Val.lessdef v v'.
Proof.
intros until v; intros EV LD. inv LD.
exists v; auto.
destruct op; simpl in *; inv EV; TrivialExists.
Qed.
Lemma eval_binop_lessdef:
forall op v1 v1'
v2 v2'
v m m',
eval_binop op v1 v2 m =
Some v ->
Val.lessdef v1 v1' ->
Val.lessdef v2 v2' ->
Mem.extends m m' ->
exists v',
eval_binop op v1'
v2'
m' =
Some v' /\
Val.lessdef v v'.
Proof.
Lemma eval_binop_lessdef_fp:
forall op v1 v1'
v2 v2'
v fp m m',
eval_binop op v1 v2 m =
Some v ->
eval_binop_fp op v1 v2 m =
Some fp ->
Val.lessdef v1 v1' ->
Val.lessdef v2 v2' ->
Mem.extends m m' ->
exists fp',
eval_binop_fp op v1'
v2'
m' =
Some fp' /\
FP.subset fp'
fp.
Proof.
Semantic preservation for instruction selection.
Relationship between the local environments.
Definition env_lessdef (
e1 e2:
env) :
Prop :=
forall id v1,
e1!
id =
Some v1 ->
exists v2,
e2!
id =
Some v2 /\
Val.lessdef v1 v2.
Lemma set_var_lessdef:
forall e1 e2 id v1 v2,
env_lessdef e1 e2 ->
Val.lessdef v1 v2 ->
env_lessdef (
PTree.set id v1 e1) (
PTree.set id v2 e2).
Proof.
intros;
red;
intros.
rewrite PTree.gsspec in *.
destruct (
peq id0 id).
exists v2;
split;
congruence.
auto.
Qed.
Lemma set_optvar_lessdef:
forall e1 e2 optid v1 v2,
env_lessdef e1 e2 ->
Val.lessdef v1 v2 ->
env_lessdef (
set_optvar optid v1 e1) (
set_optvar optid v2 e2).
Proof.
Lemma set_params_lessdef:
forall il vl1 vl2,
Val.lessdef_list vl1 vl2 ->
env_lessdef (
set_params vl1 il) (
set_params vl2 il).
Proof.
Lemma set_locals_lessdef:
forall e1 e2,
env_lessdef e1 e2 ->
forall il,
env_lessdef (
set_locals il e1) (
set_locals il e2).
Proof.
Semantic preservation for expressions.
Section EXPRESSIONS.
Variable hf:
helper_functions.
Hypothesis HF:
helper_functions_declared scu hf.
Ltac TrivEval :=
do 2
eexists;
split;[
repeat econstructor;
eauto|
split;[
eauto|
split;[
repeat econstructor;
eauto|
TrivFP]]].
Lemma sel_expr_correct_fp:
forall sp e m a fp,
Cminor_local.eval_expr_fp sge sp e m a fp ->
forall v,
Cminor.eval_expr sge sp e m a v ->
forall e'
le m',
env_lessdef e e' ->
Mem.extends m m' ->
exists v'
fp',
eval_expr tge sp e'
m'
le (
sel_expr a)
v' /\
Val.lessdef v v' /\
eval_expr_fp tge sp e'
m'
le (
sel_expr a)
fp' /\
FP.subset fp'
fp.
Proof.
Lemma sel_exprlist_correct_fp:
forall sp e m a fp,
Cminor_local.eval_exprlist_fp sge sp e m a fp ->
forall v,
Cminor.eval_exprlist sge sp e m a v ->
forall e'
le m',
env_lessdef e e' ->
Mem.extends m m' ->
exists v'
fp',
eval_exprlist tge sp e'
m'
le (
sel_exprlist a)
v' /\
Val.lessdef_list v v' /\
eval_exprlist_fp tge sp e'
m'
le (
sel_exprlist a)
fp' /\
FP.subset fp'
fp.
Proof.
induction 1;
intros;
simpl.
inv H.
exists (@
nil val),
empfp.
split;[|
split;[
auto|
split;[|
TrivFP]]];
constructor.
exploit sel_expr_correct_fp;
eauto.
intros (
v1' &
fp1' &
A &
B &
A' &
B').
exploit IHeval_exprlist_fp;
eauto.
intros (
vl' &
fpl' &
C &
D &
C' &
D').
exists (
v1' ::
vl'), (
FP.union fp1'
fpl');
split.
constructor;
eauto.
split.
inv H4.
assert (
v0 =
v1)
by (
eapply Cminor_local.eval_expr_det;
eauto).
assert (
vl0 =
vl)
by (
eapply Cminor_local.eval_exprlist_det;
eauto).
subst.
auto.
split;
subst.
econstructor;
eauto.
apply subset2_union;
TrivFP.
Qed.
Lemma sel_builtin_arg_correct_fp:
forall sp e e'
m m'
a v fp c,
env_lessdef e e' ->
Mem.extends m m' ->
Cminor.eval_expr sge sp e m a v ->
Cminor_local.eval_expr_fp sge sp e m a fp ->
exists v'
fp',
CminorSel.eval_builtin_arg tge sp e'
m' (
sel_builtin_arg a c)
v' /\
Val.lessdef v v' /\
CminorSel_local.eval_builtin_arg_fp tge sp e'
m' (
sel_builtin_arg a c)
fp' /\
FP.subset fp'
fp.
Proof.
Lemma sel_builtin_args_correct_fp:
forall sp e e'
m m',
env_lessdef e e' ->
Mem.extends m m' ->
forall al fp,
Cminor_local.eval_exprlist_fp sge sp e m al fp ->
forall vl,
Cminor.eval_exprlist sge sp e m al vl ->
forall cl,
exists vl'
fpl',
list_forall2 (
CminorSel.eval_builtin_arg tge sp e'
m')
(
sel_builtin_args al cl)
vl'
/\
Val.lessdef_list vl vl'
/\
list_forall2 (
CminorSel_local.eval_builtin_arg_fp tge sp e'
m')
(
sel_builtin_args al cl)
fpl'
/\
FP.subset (
fold_right (
fun fph fpt =>
FP.union fph fpt)
empfp fpl')
fp.
Proof.
induction 3;
intros;
simpl.
-
exists (@
nil val),
nil;
split;
constructor.
inv H1.
auto.
split.
constructor.
simpl.
TrivFP.
-
exploit sel_builtin_arg_correct_fp;
eauto.
intros (
v1' &
fp1' &
A &
B &
A' &
B').
edestruct IHeval_exprlist_fp as (
vl' &
fpl' &
C &
D &
C' &
D').
eauto.
inv H6.
assert (
v0 =
v1)
by (
eapply Cminor_local.eval_expr_det;
eauto).
assert (
vl =
vl1)
by (
eapply Cminor_local.eval_exprlist_det;
eauto).
subst.
clear H9 H11.
exists (
v1' ::
vl'), (
fp1' ::
fpl').
split.
constructor;
eauto.
split.
auto.
split.
constructor;
eauto.
simpl.
apply FP.subset_parallel_union;
TrivFP.
Qed.
End EXPRESSIONS.
Semantic preservation for functions and statements.
Inductive match_cont:
helper_functions ->
Cminor.cont ->
CminorSel.cont ->
Prop :=
|
match_cont_stop:
forall hf,
match_cont hf Cminor.Kstop Kstop
|
match_cont_seq:
forall hf s s'
k k',
sel_stmt (
comp_unit_defmap scu)
s =
OK s' ->
match_cont hf k k' ->
match_cont hf (
Cminor.Kseq s k) (
Kseq s'
k')
|
match_cont_block:
forall hf k k',
match_cont hf k k' ->
match_cont hf (
Cminor.Kblock k) (
Kblock k')
|
match_cont_call:
forall hf hf'
id f sp e k f'
e'
k',
helper_functions_declared scu hf ->
sel_function (
comp_unit_defmap scu)
hf f =
OK f' ->
match_cont hf k k' ->
env_lessdef e e' ->
match_cont hf' (
Cminor.Kcall id f sp e k) (
Kcall id f'
sp e'
k').
Definition match_call_cont (
k:
Cminor.cont) (
k':
CminorSel.cont) :
Prop :=
forall hf,
match_cont hf k k'.
Definition union_fp_list (
fpl:
list FP.t) :
FP.t :=
(
fold_right (
fun fph fpt =>
FP.union fph fpt)
empfp fpl).
Inductive match_state:
FP.t ->
FP.t ->
Cminor_local.core *
mem ->
CminorSel_local.core *
mem ->
Prop :=
|
match_state_intro:
forall fp fp'
hf f f'
s k s'
k'
sp e m e'
m'
(
HF:
helper_functions_declared scu hf)
(
TF:
sel_function (
comp_unit_defmap scu)
hf f =
OK f')
(
TS:
sel_stmt (
comp_unit_defmap scu)
s =
OK s')
(
MC:
match_cont hf k k')
(
LD:
env_lessdef e e')
(
ME:
Mem.extends m m')
NEW
(
FPMATCH:
FP.subset fp'
fp),
match_state fp fp'
(
Cminor_local.Core_State f s k sp e,
m)
(
Core_State f'
s'
k'
sp e',
m')
|
match_callstate:
forall fp fp'
f f'
args args'
k k'
m m'
(
TF:
match_fundef scu f f')
(
MC:
match_call_cont k k')
(
LD:
Val.lessdef_list args args')
(
ME:
Mem.extends m m')
NEW
(
FPMATCH:
FP.subset fp'
fp),
match_state fp fp'
(
Cminor_local.Core_Callstate f args k,
m)
(
Core_Callstate f'
args'
k',
m')
|
match_returnstate:
forall fp fp'
v v'
k k'
m m'
(
MC:
match_call_cont k k')
(
LD:
Val.lessdef v v')
(
ME:
Mem.extends m m')
NEW
(
FPMATCH:
FP.subset fp'
fp),
match_state fp fp'
(
Cminor_local.Core_Returnstate v k,
m)
(
Core_Returnstate v'
k',
m')
|
match_builtin_1:
forall fp fp'
fpl hf ef args args'
optid f sp e k m al f'
e'
k'
m'
(
TF:
sel_function (
comp_unit_defmap scu)
hf f =
OK f')
(
MC:
match_cont hf k k')
(
LDA:
Val.lessdef_list args args')
(
LDE:
env_lessdef e e')
(
ME:
Mem.extends m m')
(
EA:
list_forall2 (
CminorSel.eval_builtin_arg tge sp e'
m')
al args')
(
INLINE:
ef_inline ef =
true)
NEW
(
EAFP:
list_forall2 (
CminorSel_local.eval_builtin_arg_fp tge sp e'
m')
al fpl)
(
FPMATCH:
FP.subset (
FP.union fp' (
union_fp_list fpl))
fp),
match_state fp fp'
(
Cminor_local.Core_Callstate (
External ef)
args (
Cminor.Kcall optid f sp e k),
m)
(
Core_State f' (
Sbuiltin (
sel_builtin_res optid)
ef al)
k'
sp e',
m').
Definition MS b n mu fp fp'
cm cm':
Prop :=
match_state fp fp'
cm cm' /\
let (
c,
m) :=
cm in
let (
c',
m') :=
cm'
in
(
forall b,
Bset.belongsto (
Injections.SharedSrc mu)
b ->
Mem.valid_block m b) /\
(
forall b,
Bset.belongsto (
Injections.SharedTgt mu)
b ->
Mem.valid_block m'
b) /\
(
proper_mu sge tge inject_id mu) /\
(
MemClosures_local.unmapped_closed mu m m') /\
match c with
|
Cminor_local.Core_State _ _ _ _ _ =>
n = 1%
nat /\
b =
true
|
Cminor_local.Core_Callstate _ _ _ =>
n = 0%
nat
|
Cminor_local.Core_Returnstate _ _ =>
n = 2%
nat
end.
Ltac invMS :=
match goal with
|
H:
MS _ _ _ _ _ ?
cm1 ?
cm2 |-
_ =>
destruct cm1 as [
sc Hm];
destruct cm2 as [
tc Lm];
unfold MS in H;
simpl in H;
destruct H as [
MS [
SVALID [
TVALID [
AGMU [
RCPRESV INDEX]]]]]
|
H:
MS _ _ _ _ _ ?
cm1 ?
cm2 |-
_ =>
unfold MS in H;
simpl in H;
destruct H as [
MS [
SVALID [
TVALID [
AGMU [
RCPRESV INDEX]]]]]
end.
Remark call_cont_commut:
forall hf k k',
match_cont hf k k' ->
match_call_cont (
Cminor.call_cont k) (
call_cont k').
Proof.
induction 1;
simpl;
auto;
red;
intros.
-
constructor.
-
eapply match_cont_call with (
hf :=
hf);
eauto.
Qed.
Remark match_is_call_cont:
forall hf k k',
match_cont hf k k' ->
Cminor.is_call_cont k ->
match_call_cont k k'.
Proof.
destruct 1;
intros;
try contradiction;
red;
intros.
-
constructor.
-
eapply match_cont_call with (
hf :=
hf);
eauto.
Qed.
Remark match_call_cont_cont:
forall k k',
match_call_cont k k' ->
exists hf,
match_cont hf k k'.
Proof.
intros.
simple refine (
let hf :
helper_functions :=
_ in _).
econstructor;
apply xH.
exists hf;
auto.
Qed.
Remark find_label_commut:
forall hf lbl s k s'
k',
match_cont hf k k' ->
sel_stmt (
comp_unit_defmap scu)
s =
OK s' ->
match Cminor.find_label lbl s k,
find_label lbl s'
k'
with
|
None,
None =>
True
|
Some(
s1,
k1),
Some(
s1',
k1') =>
sel_stmt (
comp_unit_defmap scu)
s1 =
OK s1' /\
match_cont hf k1 k1'
|
_,
_ =>
False
end.
Proof.
induction s;
intros until k';
simpl;
intros MC SE;
try (
monadInv SE);
simpl;
auto.
store *)
unfold store.
destruct (
addressing m (
sel_expr e));
simpl;
auto.
call *)
destruct (
classify_call (
comp_unit_defmap scu)
e);
simpl;
auto.
tailcall *)
destruct (
classify_call (
comp_unit_defmap scu)
e);
simpl;
auto.
seq *)
exploit (
IHs1 (
Cminor.Kseq s2 k)).
constructor;
eauto.
eauto.
destruct (
Cminor.find_label lbl s1 (
Cminor.Kseq s2 k))
as [[
sx kx] | ];
destruct (
find_label lbl x (
Kseq x0 k'))
as [[
sy ky] | ];
intuition.
apply IHs2;
auto.
ifthenelse *)
exploit (
IHs1 k);
eauto.
destruct (
Cminor.find_label lbl s1 k)
as [[
sx kx] | ];
destruct (
find_label lbl x k')
as [[
sy ky] | ];
intuition.
apply IHs2;
auto.
loop *)
apply IHs.
constructor;
auto.
simpl;
rewrite EQ;
auto.
auto.
block *)
apply IHs.
constructor;
auto.
auto.
switch *)
destruct b.
destruct (
validate_switch Int64.modulus n l (
compile_switch Int64.modulus n l));
inv SE.
simpl;
auto.
destruct (
validate_switch Int.modulus n l (
compile_switch Int.modulus n l));
inv SE.
simpl;
auto.
return *)
destruct o;
inv SE;
simpl;
auto.
label *)
destruct (
ident_eq lbl l).
auto.
apply IHs;
auto.
Qed.
Ltac Ex_index :=
match goal with
| |-
context[
Cminor_local.Core_State] =>
exists 1%
nat
| |-
context[
Cminor_local.Core_Callstate] =>
exists 0%
nat
| |-
context[
Cminor_local.Core_Returnstate] =>
exists 2%
nat
end.
Ltac resolvfp:=
match goal with
| |-
context[
FP.union _ empfp] =>
rewrite FP.fp_union_emp;
resolvfp
| |-
context[
FP.union empfp _] =>
rewrite FP.emp_union_fp;
resolvfp
|
H:
Some _ =
Some _ |-
_ =>
inv H;
resolvfp
|
H:
FP.subset ?
fp1' ?
fp1 |-
Injections.FPMatch' ?
mu (
FP.union ?
fp1 _) (
FP.union ?
fp1'
_) =>
eapply Injections.fp_match_union';
resolvfp
|
H:
FP.subset ?
fp1' ?
fp1 |-
FP.subset (
FP.union ?
fp1'
_) (
FP.union ?
fp1 _) =>
eapply FP.subset_parallel_union;
resolvfp
|
H:
FP.subset ?
fp1' ?
fp1 |-
FP.subset (
FP.union (
FP.union ?
fp1'
_)
_) (
FP.union (
FP.union ?
fp1 _)
_)=>
eapply FP.subset_parallel_union;
resolvfp
|
H:
FP.subset ?
fp ?
fp' |-
FP.subset ?
fp (
FP.union ?
fp1 ?
fp') =>
rewrite FP.union_comm_eq;
resolvfp
|
H:
FP.subset ?
fp ?
fp' |-
FP.subset ?
fp (
FP.union ?
fp'
_) =>
apply FP.subset_union_subset;
auto
| |-
Injections.FPMatch'
_ _ empfp =>
apply Injections.fp_match_emp'
|
H:
FP.subset ?
fp1 ?
fp2 |-
Injections.FPMatch'
_ ?
fp2 ?
fp1 =>
apply Injections.fp_match_subset_T'
with fp2;
try exact H;
resolvfp
|
H:
FP.subset ?
fp2 ?
fp1 |-
Injections.FPMatch'
_ (
FP.union ?
fp1 _) ?
fp2 =>
apply Injections.fp_match_union_S';
resolvfp
| |-
FP.subset ?
fp ?
fp =>
apply FP.subset_refl
|
H:
proper_mu _ _ _ _ |-
Injections.FPMatch'
_ ?
fp ?
fp =>
inv H;
eapply fp_match_id;
eauto
|
_ =>
idtac
end.
Ltac eresolvfp:=
resolvfp;
eauto.
Ltac resvalid:=
match goal with
valid blocks
|
H: (
forall x,
Bset.belongsto ?
S x ->
Mem.valid_block ?
m1 x),
H':
Mem.free ?
m1 _ _ _ =
Some ?
m2
|- (
forall x,
Bset.belongsto ?
S x ->
Mem.valid_block ?
m2 x)
=>
let X :=
fresh in
intros ?
X;
apply H in X;
eapply Mem.valid_block_free_1;
eauto
|
H: (
forall x,
Bset.belongsto ?
S x ->
Mem.valid_block ?
m1 x),
H':
Mem.alloc ?
m1 _ _ = (?
m2,
_)
|- (
forall x,
Bset.belongsto ?
S x ->
Mem.valid_block ?
m2 x)
=>
let X :=
fresh in
intros ?
X;
apply H in X;
eapply Mem.valid_block_alloc;
eauto
|
H: (
forall x,
Bset.belongsto ?
S x ->
Mem.valid_block ?
m1 x),
H':
Mem.store _ ?
m1 _ _ _ =
Some ?
m2
|- (
forall x,
Bset.belongsto ?
S x ->
Mem.valid_block ?
m2 x)
=>
let X :=
fresh in
intros ?
X;
apply H in X;
eapply Mem.store_valid_block_1;
eauto
Mem inv
|
H1:
Mem.store _ ?
m1 _ _ _ =
Some ?
m2,
H2:
Mem.store _ ?
m1'
_ _ _ =
Some ?
m2',
H3:
proper_mu _ _ _ _
|-
MemClosures_local.unmapped_closed _ ?
m2 ?
m2'
=>
inv H3;
eapply MemClosures_local.store_val_inject_unmapped_closed_preserved;
try (
rewrite Z.add_0_r);
try eassumption;
try (
compute;
eauto;
fail);
try omega
|
H1:
Mem.free ?
m1 _ _ _ =
Some ?
m2,
H2:
Mem.free ?
m1'
_ _ _ =
Some ?
m2',
H3:
proper_mu _ _ _ _
|-
MemClosures_local.unmapped_closed _ ?
m2 ?
m2'
=>
inv H3;
eapply MemClosures_local.free_inject_unmapped_closed_preserved;
eauto;
try (
rewrite Z.add_0_r);
try eassumption;
try (
compute;
eauto;
fail);
try omega
|
H1:
Mem.alloc ?
m1 _ _ = (?
m2,
_),
H2:
Mem.alloc ?
m1'
_ _ = (?
m2',
_),
H3:
proper_mu _ _ _ _
|-
MemClosures_local.unmapped_closed _ ?
m2 ?
m2'
=>
inv H3;
eapply MemClosures_local.unchanged_on_unmapped_closed_preserved;
eauto;
try (
eapply Mem.alloc_unchanged_on;
eauto;
fail)
|
_ =>
idtac
end.
Ltac Right :=
right;
Ex_index;
do 3
eexists;
split; [
apply plus_one|
resolvfp].
Ltac FP:=
match goal with |- ?
P /\
_ =>
assert P; [
eresolvfp|
try (
split;[
auto;
fail|])]
end.
Ltac Left :=
left;
Ex_index;
split; [
auto|
eresolvfp].
Ltac splitMS :=
split;
[
econstructor;
eresolvfp |
split;
[
try resvalid;
auto |
split; [
try resvalid;
auto
|
split; [
auto|
split;
try resvalid;
eauto]]]].
Theorem TRANSF_local_ldsim:
@
local_ldsim Cminor_IS CminorSel_IS sge tge sge tge.
Proof.
eapply (@
Local_ldsim Cminor_IS CminorSel_IS _ _ _ _ _ lt%
nat MS).
constructor.
index wf *) -
apply lt_wf.
wd_mu *) -
intros.
invMS.
eapply proper_mu_inject;
eauto.
inj ge *) -
intros.
invMS;
eapply proper_mu_ge_init_inj;
eauto.
ge match *) -
apply ge_match.
initial call *) -
intros mu fid args args'
score GE_INIT_INJ INJID GARG ARGREL INITCORE.
unfold init_core_local in *.
simpl in *.
unfold Cminor_local.init_core,
init_core in *.
unfold generic_init_core in INITCORE |- * .
rewrite symbols_preserved.
destruct (
Genv.find_symbol sge fid)
eqn:
FIND;
try discriminate.
destruct (
Genv.find_funct_ptr sge b)
eqn:
FINDB;
try discriminate.
exploit function_ptr_translated;
eauto.
intros (
tf &
FINDB' & (
hf &
HF &
MATCHF)).
rewrite FINDB'.
unfold Cminor_local.fundef_init in INITCORE.
destruct f;
try discriminate.
assert (
exists tfd,
tf =
Internal tfd)
as [
tfd INTERNAL]
by (
monadInv MATCHF;
eauto).
subst tf.
unfold fundef_init.
erewrite sig_function_translated;[|
eexists;
eauto].
destruct (
wd_args args (
sig_args (
Cminor.funsig (
Internal f))))
eqn:
WDARGS; [|
discriminate].
erewrite wd_args_inject;
eauto.
eexists.
split.
eauto.
intros sm0 tm0 INITSM INITTM MEMINITINJ sm tm [
HRELY LRELY MINJ].
exists 0%
nat.
inv INITCORE.
This could be a general purposed lemma...
assert (
args' =
args).
{
generalize ARGREL GARG MEMINITINJ;
clear.
revert args'.
induction args;
intros args'
REL G MEMREL;
inv REL.
auto.
inv G.
f_equal.
inv H1;
auto.
inv MEMREL.
apply inj_inject_id in H.
inv H.
rewrite Ptrofs.add_zero;
auto.
contradiction.
apply IHargs;
auto. }
subst args'.
exploit sig_function_translated; [
eexists;
eauto|].
simpl.
split.
econstructor;
eauto.
{
eexists.
eauto. }
{
constructor. }
{
clear;
induction args;
auto. }
{
inv MEMINITINJ.
inv HRELY.
inv LRELY.
eapply inject_implies_extends;
eauto.
intros b0 A.
unfold Mem.valid_block in A;
rewrite EQNEXT, <-
dom_eq_src in A.
eapply Bset.inj_dom in A;
eauto.
destruct A as [
b'
A].
unfold Bset.inj_to_meminj.
rewrite A.
eauto.
inv GE_INIT_INJ.
rewrite mu_shared_src in dom_eq_src.
rewrite mu_shared_tgt in dom_eq_tgt.
rewrite S_EQ in dom_eq_src.
assert (
forall b,
Plt b (
Mem.nextblock sm0) <->
Plt b (
Mem.nextblock tm0)).
{
intro.
rewrite <-
dom_eq_src, <-
dom_eq_tgt.
tauto. }
rewrite EQNEXT,
EQNEXT0.
destruct (
Pos.lt_total (
Mem.nextblock sm0) (
Mem.nextblock tm0))
as [
LT | [
EQ |
LT]];
auto;
(
generalize H4 LT;
clear;
intros;
exfalso;
apply H4 in LT;
eapply Pos.lt_irrefl;
eauto). }
apply FP.subset_emp.
split.
inv MEMINITINJ.
inv HRELY.
unfold Mem.valid_block in *.
intros.
rewrite EQNEXT.
apply dom_eq_src;
auto.
split.
inv MEMINITINJ.
inv LRELY.
unfold Mem.valid_block in *.
intros.
rewrite EQNEXT.
apply dom_eq_tgt;
auto.
split.
inv MEMINITINJ;
econstructor;
eauto.
simpl.
intro.
intros ? ? ? ? ? .
exploit inj_inject_id.
exact H0.
intro.
inv H1.
intro A.
inv A.
auto.
split;
auto.
apply MemClosures_local.reach_closed_unmapped_closed.
inv LRELY.
auto.
-
intros i mu Hfp Lfp Hcore Hm Lcore Lm Hfp'
Hcore'
Hm'
MS STEP.
simpl in STEP.
revert i mu Hfp Lfp Lcore Lm MS.
induction STEP;
intros until Lm;
intros MS';
invMS;
inv MS;
try (
monadInv TS).
+
inv MC.
Right.
econstructor.
FP.
splitMS.
+
inv MC.
Right.
econstructor.
FP.
splitMS.
+
exploit Mem.free_parallel_extends;
eauto.
intros [
m2' [
A B]].
Right.
econstructor;
eauto.
inv MC;
simpl in H;
auto.
erewrite stackspace_function_translated;
eauto.
erewrite stackspace_function_translated;
eauto.
FP.
splitMS.
eapply match_is_call_cont;
eauto.
+
exploit sel_expr_correct_fp;
eauto.
intros (
v' &
fp' &
A &
B &
A' &
B').
Right.
econstructor;
eauto.
FP.
splitMS.
apply set_var_lessdef;
auto.
+
exploit sel_expr_correct_fp;
try exact H;
eauto.
intros (
vaddr' &
fp1' &
A &
B &
A' &
B').
exploit sel_expr_correct_fp;
try exact H1;
eauto.
intros (
v' &
fp2' &
C &
D &
C' &
D').
exploit Mem.storev_extends;
eauto.
intros [
m2' [
P Q]].
Right.
eapply eval_store_fp;
eauto.
destruct vaddr;
try discriminate.
inv B.
simpl in H3,
P.
FP.
repeat apply Injections.fp_match_union';
resolvfp.
splitMS.
+
exploit classify_call_correct;
eauto.
destruct (
classify_call (
comp_unit_defmap scu)
a)
as [ |
id |
ef]
eqn:
CC.
++
exploit sel_expr_correct_fp;
eauto.
intros (
vf' &
fp1' &
A &
B &
A' &
B').
exploit sel_exprlist_correct_fp;
eauto.
intros (
vargs' &
fp2' &
C &
D &
C' &
D').
exploit functions_translated;
eauto.
intros (
fd' &
U &
V ).
Right.
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
eapply sig_function_translated;
eauto.
FP.
splitMS.
red;
intros.
eapply match_cont_call with (
hf :=
hf);
eauto.
++
intros [
b [
U V]].
exploit sel_exprlist_correct_fp;
eauto.
intros (
vargs' &
fp2' &
C &
D &
C' &
D').
exploit functions_translated;
eauto.
intros (
fd' &
X &
Y).
Right.
econstructor;
eauto.
subst vf.
econstructor;
eauto.
rewrite symbols_preserved;
eauto.
econstructor;
eauto.
rewrite symbols_preserved;
eauto.
eapply sig_function_translated;
eauto.
FP.
rewrite FP.union_comm_eq.
apply Injections.fp_match_union_S';
resolvfp.
splitMS.
red;
intros;
eapply match_cont_call with (
hf :=
hf);
eauto.
++
which we do not support currently *)
intros EQ.
subst fd.
assert (
INLINE:
ef_inline ef =
true).
{
revert CC;
clear.
unfold classify_call,
ef_inline.
do 4
match goal with | |-
context[
match ?
x with _ =>
_ end] =>
destruct x eqn:?;
try discriminate end.
destruct e,
ef;
try discriminate;
auto. }
exploit sel_builtin_args_correct_fp;
eauto.
intros (
vargs' &
fp2' &
C &
D &
C' &
D').
Left.
destruct INDEX.
subst.
auto.
splitMS.
rewrite (
FP.union_comm_eq);
resolvfp.
+
exploit Mem.free_parallel_extends;
eauto.
intros [
m2' [
P Q]].
erewrite <-
stackspace_function_translated in P by eauto.
exploit sel_expr_correct_fp;
eauto.
intros (
vf' &
fp1' &
A &
B &
A' &
B').
exploit sel_exprlist_correct_fp;
eauto.
intros (
vargs' &
fp2' &
C &
D &
C' &
D').
exploit functions_translated;
eauto.
intros (
fd' &
E &
F).
Right.
exploit classify_call_correct.
eauto.
eauto.
destruct (
classify_call (
comp_unit_defmap scu))
as [ |
id |
ef]
eqn:
CC;
intros.
*)
repeat econstructor;
eauto.
eapply sig_function_translated;
eauto.
*)
destruct H4 as [
b [
U V]].
subst vf.
inv B.
econstructor.
econstructor.
rewrite symbols_preserved;
eauto.
econstructor.
rewrite symbols_preserved;
eauto.
eauto.
eauto.
eauto.
eapply sig_function_translated;
eauto.
eauto.
eauto.
assert (
fp1' =
empfp).
{
generalize CC A';
clear;
intros.
unfold classify_call in CC.
destruct a;
simpl in CC;
try discriminate.
repeat match goal with
CC:
context[
match ?
x with _ =>
_ end] |-
_ =>
destruct x eqn:?;
try discriminate;
unfold addrsymbol,
Olea_ptr in *;
InvEvalFP;
InvEval;
simpl in *;
FuncInv;
subst;
TrivFP
end. }
subst.
TrivFP.
*)
econstructor;
eauto.
econstructor;
eauto.
econstructor;
eauto.
eapply sig_function_translated;
eauto.
erewrite stackspace_function_translated;
eauto.
FP.
repeat apply Injections.fp_match_union';
resolvfp.
splitMS.
eapply call_cont_commut;
eauto.
erewrite stackspace_function_translated;
eauto.
omega.
+
Right.
constructor.
FP.
splitMS.
econstructor;
eauto.
+
exploit sel_expr_correct_fp;
eauto.
intros (
v' &
fp' &
A &
B &
A' &
B').
assert (
Val.bool_of_val v'
b).
inv B.
auto.
inv H1.
exploit eval_condexpr_of_expr_fp;
eauto.
intros [
C C'].
Right.
econstructor;
eauto.
FP.
splitMS.
destruct b;
auto.
+
Right.
econstructor.
FP.
splitMS.
constructor;
auto.
simpl;
rewrite EQ;
auto.
+
Right.
econstructor.
FP.
splitMS.
constructor;
auto.
+
inv MC.
Right.
econstructor.
FP.
splitMS.
+
inv MC.
Right.
econstructor.
FP.
splitMS.
+
inv MC.
Right.
econstructor.
FP.
splitMS.
+
inv H1;
simpl in TS.
++
set (
ct :=
compile_switch Int.modulus default cases)
in *.
destruct (
validate_switch Int.modulus default cases ct)
eqn:
VALID;
inv TS.
exploit sel_expr_correct_fp;
eauto.
intros (
v' &
fp' &
A &
B &
A' &
B').
inv B.
exploit sel_switch_int_correct_fp;
eauto.
intros [
C C'].
Right.
econstructor;
eauto.
FP.
splitMS.
++
set (
ct :=
compile_switch Int64.modulus default cases)
in *.
destruct (
validate_switch Int64.modulus default cases ct)
eqn:
VALID;
inv TS.
exploit sel_expr_correct_fp;
eauto.
intros (
v' &
fp' &
A &
B &
A' &
B').
inv B.
exploit sel_switch_long_correct_fp;
eauto.
intros [
C C'].
Right.
econstructor;
eauto.
FP.
splitMS.
+
exploit Mem.free_parallel_extends;
eauto.
intros [
m2' [
P Q]].
erewrite <-
stackspace_function_translated in *
by eauto.
Right.
econstructor;
simpl;
eauto.
FP.
splitMS.
eapply call_cont_commut;
eauto.
+
exploit Mem.free_parallel_extends;
eauto.
intros [
m2' [
P Q]].
erewrite <-
stackspace_function_translated in *
by eauto.
exploit sel_expr_correct_fp;
eauto.
intros [
v' [
fp' [
A [
B [
A'
B']]]]].
Right.
econstructor;
eauto.
FP.
splitMS.
eapply call_cont_commut;
eauto.
+
Right.
econstructor;
eauto.
FP.
splitMS.
+
assert (
sel_stmt (
comp_unit_defmap scu) (
Cminor.fn_body f) =
OK (
fn_body f')).
{
monadInv TF;
simpl;
auto. }
exploit (
find_label_commut hf lbl (
Cminor.fn_body f) (
Cminor.call_cont k)).
eapply call_cont_commut;
eauto.
eauto.
rewrite H.
destruct (
find_label lbl (
fn_body f') (
call_cont k'0))
as [[
s''
k'']|]
eqn:?;
intros;
try contradiction.
destruct H1.
Right.
econstructor;
eauto.
FP.
splitMS.
+
destruct TF as (
hf &
HF &
TF).
specialize (
MC hf).
monadInv TF.
generalize EQ;
intros TF;
monadInv TF.
exploit Mem.alloc_extends.
eauto.
eauto.
apply Zle_refl.
apply Zle_refl.
intros [
m2' [
A B]].
Right.
econstructor;
simpl;
eauto.
FP.
unfold alloc_fp.
erewrite Mem.mext_next;
eauto.
resolvfp.
splitMS.
apply set_locals_lessdef.
apply set_params_lessdef;
auto.
unfold alloc_fp.
erewrite <-
Mem.mext_next;
eauto.
resolvfp.
+
apply match_call_cont_cont in MC.
destruct MC as (
hf0 &
MC).
inv MC.
Right.
econstructor.
FP.
splitMS.
destruct optid;
simpl;
auto.
apply set_var_lessdef;
auto.
-
simpl in *.
unfold Cminor_local.at_external,
at_external.
intros i mu Hfp Lfp Hcore Hm Lcore Lm f sg argSrc MS ATEXT RC GARG.
destruct Hcore;
try discriminate.
destruct f0;
try discriminate.
destruct e eqn:?;
try discriminate.
destruct (
invert_symbol_from_string sge name)
eqn:
SYMBNAME;
try discriminate.
destruct peq;
simpl in *.
discriminate.
destruct peq;
simpl in *.
discriminate.
inv ATEXT.
invMS;
inv MS;
try discriminate.
destruct TF as [
hf0 [
HF0 SEL]].
simpl in SEL.
inv SEL.
erewrite match_genvs_invert_symbol_from_string_preserved;
eauto.
Ex_index.
destruct peq;
try contradiction.
destruct peq;
try contradiction.
eexists.
simpl.
split;
auto.
split.
{
simpl in *.
unfold LDSimDefs.arg_rel.
revert args'
AGMU LD GARG;
clear.
should be extracted as a lemma ...
induction argSrc;
intros.
simpl.
inv LD.
auto.
inv LD.
inv GARG.
constructor;
auto.
clear H3 H4 IHargSrc.
inv H1;
auto.
destruct v2;
auto.
simpl in H2.
eapply Bset.inj_dom in H2;
inv AGMU;
eauto.
destruct H2.
exploit proper_mu_inject_incr.
unfold Bset.inj_to_meminj;
rewrite H;
eauto.
intro.
inv H0.
econstructor.
unfold Bset.inj_to_meminj;
rewrite H.
eauto.
rewrite Ptrofs.add_zero;
auto. }
split.
eapply MemClosures_local.unmapped_closed_reach_closed_preserved_by_extends;
inv AGMU;
eauto.
split;
eresolvfp.
split.
eapply extends_reach_closed_implies_inject;
inv AGMU;
eauto.
splitMS.
eexists;
eauto.
eapply match_cu_match_genv;
eauto.
intros.
inv H;
auto.
destruct H0 as [
hf' [
HF'
SEL']].
destruct f1;
monadInv SEL';
auto.
-
simpl.
unfold Cminor_local.after_external,
after_external.
intros i mu Hcore Hm Lcore Lm oresSrc Hcore'
oresTgt MS GRES AFTEXT RESREL.
destruct Hcore;
try discriminate.
destruct f;
try discriminate.
destruct e;
try discriminate.
invMS;
inv MS;
try discriminate.
destruct TF as [
hf0 [
HF0 TF]].
monadInv TF.
assert (
Hcore' =
Cminor_local.Core_Returnstate (
match oresSrc with Some v =>
v |
None =>
Vundef end)
k).
{
destruct oresSrc, (
sig_res sg);
inv AFTEXT;
auto.
destruct (
val_has_type_func v t);
inv H0.
auto. }
assert (
match oresSrc, (
sig_res sg)
with
|
None,
None =>
True
|
Some v,
Some ty =>
Val.has_type v ty
|
_,
_ =>
False
end)
as HRES.
{
destruct oresSrc, (
sig_res sg);
inv AFTEXT;
auto.
destruct (
val_has_type_func v t)
eqn:
A;
inv H1.
apply val_has_type_funcP;
auto. }
clear AFTEXT.
rename H into AFTEXT.
exists (
Core_Returnstate (
match oresTgt with Some v =>
v |
None =>
Vundef end)
k').
split.
{
destruct oresSrc,
oresTgt, (
sig_res sg);
try contradiction;
auto.
inv RESREL;
destruct t;
try contradiction;
simpl in *;
auto.
rewrite HRES.
auto. }
intros Hm'
Lm' [
HRELY LRELY INV].
subst.
Ex_index.
splitMS.
{
destruct oresSrc, (
sig_res sg),
oresTgt;
simpl in *;
try contradiction;
auto.
inv RESREL;
auto.
inv AGMU.
apply proper_mu_inject_incr in H.
inv H.
rewrite Ptrofs.add_zero.
auto. }
inv AGMU;
eapply extends_rely_extends;
eauto.
econstructor;
eauto.
intros ?
S.
apply SVALID in S.
unfold Mem.valid_block in *.
inv HRELY.
rewrite EQNEXT;
auto.
intros ?
T.
apply TVALID in T.
unfold Mem.valid_block in *.
inv LRELY.
rewrite EQNEXT;
auto.
inv LRELY.
eapply MemClosures_local.reach_closed_unmapped_closed;
eauto.
-
simpl.
unfold Cminor_local.halted,
halted.
intros i mu Hfp Lfp Hcore Hm Lcore Lm resSrc MS HALT RC GRES.
destruct Hcore,
k;
try discriminate.
inv HALT.
invMS;
inv MS.
apply match_call_cont_cont in MC.
destruct MC as (
hf0 &
MC).
inv MC.
exists resSrc.
split. {
f_equal.
inv LD;
auto.
contradiction. }
split.
{
revert AGMU GRES.
clear;
intros.
destruct resSrc;
try constructor.
econstructor.
simpl in GRES.
inv AGMU.
eapply Bset.inj_dom in GRES;
eauto.
destruct GRES as [
b'
INJ].
exploit proper_mu_inject_incr.
unfold Bset.inj_to_meminj;
rewrite INJ;
eauto.
intro A.
inv A.
unfold Bset.inj_to_meminj;
rewrite INJ;
eauto.
rewrite Ptrofs.add_zero;
auto. }
split.
inv AGMU;
eapply MemClosures_local.unmapped_closed_reach_closed_preserved_by_extends;
eauto.
split.
resolvfp.
inv AGMU;
eapply extends_reach_closed_implies_inject;
eauto.
Qed.
End PRESERVATION.
Theorem transf_local_ldsim:
forall scu tcu,
selection.transf_program scu =
OK tcu ->
forall sge sG tge tG,
init_genv_local Cminor_IS scu sge sG ->
init_genv_local CminorSel_IS tcu tge tG ->
Genv.genv_next sge =
Genv.genv_next tge ->
local_ldsim sG tG sge tge.
Proof.