Correctness proof for the translation from Linear to Mach.
This file proves semantic preservation for the Stacking pass.
Require Import Coqlib Errors.
Require Import Integers AST Linking.
Require Import Values Memory Separation Events Globalenvs Smallstep.
Require Import LTL Op Locations Linear Mach.
Require Import Bounds Conventions Stacklayout Lineartyping.
Require Import Stacking.
Require Import sflib.
Require SimMemInj.
Local Open Scope sep_scope.
Definition match_prog (
p:
Linear.program) (
tp:
Mach.program) :=
match_program (
fun _ f tf =>
transf_fundef f =
OK tf)
eq p tp.
Lemma transf_program_match:
forall p tp,
transf_program p =
OK tp ->
match_prog p tp.
Proof.
Basic properties of the translation
Lemma typesize_typesize:
forall ty,
AST.typesize ty = 4 *
Locations.typesize ty.
Proof.
destruct ty; auto.
Qed.
Remark size_type_chunk:
forall ty,
size_chunk (
chunk_of_type ty) =
AST.typesize ty.
Proof.
destruct ty; reflexivity.
Qed.
Remark align_type_chunk:
forall ty,
align_chunk (
chunk_of_type ty) = 4 *
Locations.typealign ty.
Proof.
destruct ty; reflexivity.
Qed.
Lemma slot_outgoing_argument_valid:
forall f ofs ty sg,
In (
S Outgoing ofs ty) (
regs_of_rpairs (
loc_arguments sg)) ->
slot_valid f Outgoing ofs ty =
true.
Proof.
Lemma load_stack_transf_ofs
m sp spofs ty ofs:
<<
EQ:
load_stack m (
Vptr sp spofs)
ty ofs =
load_stack m (
Vptr sp Ptrofs.zero)
ty (
Ptrofs.add spofs ofs)>>.
Proof.
Section PRESERVATION.
Variable prog:
Linear.program.
Variable tprog:
Mach.program.
Hypothesis TRANSF:
match_prog prog tprog.
Variable return_address_offset:
Mach.function ->
Mach.code ->
ptrofs ->
Prop.
Section CORELEMMA.
Variable se tse:
Senv.t.
Variable ge :
Linear.genv.
Variable tge :
genv.
Hypothesis SECOMPATSRC:
senv_genv_compat se ge.
Hypothesis SECOMPATTGT:
senv_genv_compat tse tge.
Hypothesis return_address_offset_exists:
forall f sg ros c v (
FUNCT:
Genv.find_funct tge v =
Some (
Internal f)),
is_tail (
Mcall sg ros ::
c) (
fn_code f) ->
exists ofs,
return_address_offset f c ofs.
Context `{
CTX0:
main_args_ctx}.
Lemma load_result_inject:
forall j ty v v',
Val.inject j v v' ->
Val.has_type v ty ->
Val.inject j v (
Val.load_result (
chunk_of_type ty)
v').
Proof.
Section FRAME_PROPERTIES.
Variable f:
Linear.function.
Let b :=
function_bounds f.
Let fe :=
make_env b.
Variable tf:
Mach.function.
Hypothesis TRANSF_F:
transf_function f =
OK tf.
Lemma unfold_transf_function:
tf =
Mach.mkfunction
f.(
Linear.fn_sig)
(
transl_body f fe)
fe.(
fe_size)
(
Ptrofs.repr fe.(
fe_ofs_link))
(
Ptrofs.repr fe.(
fe_ofs_retaddr)).
Proof.
Lemma transf_function_well_typed:
wt_function f =
true.
Proof.
Lemma size_no_overflow:
fe.(
fe_size) <=
Ptrofs.max_unsigned.
Proof.
Remark bound_stack_data_stacksize:
f.(
Linear.fn_stacksize) <=
b.(
bound_stack_data).
Proof.
Memory assertions used to describe the contents of stack frames
Local Opaque Z.add Z.mul Z.divide.
Accessing the stack frame using load_stack and store_stack.
Lemma contains_get_stack:
forall spec m ty sp ofs,
m |=
contains (
chunk_of_type ty)
sp ofs spec ->
exists v,
load_stack m (
Vptr sp Ptrofs.zero)
ty (
Ptrofs.repr ofs) =
Some v /\
spec v.
Proof.
Lemma hasvalue_get_stack:
forall ty m sp ofs v,
m |=
hasvalue (
chunk_of_type ty)
sp ofs v ->
load_stack m (
Vptr sp Ptrofs.zero)
ty (
Ptrofs.repr ofs) =
Some v.
Proof.
Lemma contains_set_stack:
forall (
spec:
val ->
Prop)
v spec1 m ty sp ofs P,
m |=
contains (
chunk_of_type ty)
sp ofs spec1 **
P ->
spec (
Val.load_result (
chunk_of_type ty)
v) ->
exists m',
store_stack m (
Vptr sp Ptrofs.zero)
ty (
Ptrofs.repr ofs)
v =
Some m'
/\
m' |=
contains (
chunk_of_type ty)
sp ofs spec **
P.
Proof.
contains_locations j sp pos bound sl ls is a separation logic assertion
that holds if the memory area at block sp, offset pos, size 4 * bound,
reflects the values of the stack locations of kind sl given by the
location map ls, up to the memory injection j.
Two such contains_locations assertions will be used later, one to
reason about the values of Local slots, the other about the values of
Outgoing slots.
Program Definition contains_locations (
j:
meminj) (
sp:
block) (
pos bound:
Z) (
sl:
slot) (
ls:
locset) :
massert := {|
m_pred :=
fun m =>
(8 |
pos) /\ 0 <=
pos /\
pos + 4 *
bound <=
Ptrofs.modulus /\
Mem.range_perm m sp pos (
pos + 4 *
bound)
Cur Freeable /\
forall ofs ty, 0 <=
ofs ->
ofs +
typesize ty <=
bound -> (
typealign ty |
ofs) ->
exists v,
Mem.load (
chunk_of_type ty)
m sp (
pos + 4 *
ofs) =
Some v
/\
Val.inject j (
ls (
S sl ofs ty))
v;
m_footprint :=
fun b ofs =>
b =
sp /\
pos <=
ofs <
pos + 4 *
bound
|}.
Next Obligation.
Next Obligation.
eauto with mem.
Qed.
Remark valid_access_location:
forall m sp pos bound ofs ty p,
(8 |
pos) ->
Mem.range_perm m sp pos (
pos + 4 *
bound)
Cur Freeable ->
0 <=
ofs ->
ofs +
typesize ty <=
bound -> (
typealign ty |
ofs) ->
Mem.valid_access m (
chunk_of_type ty)
sp (
pos + 4 *
ofs)
p.
Proof.
Lemma get_location:
forall m j sp pos bound sl ls ofs ty,
m |=
contains_locations j sp pos bound sl ls ->
0 <=
ofs ->
ofs +
typesize ty <=
bound -> (
typealign ty |
ofs) ->
exists v,
load_stack m (
Vptr sp Ptrofs.zero)
ty (
Ptrofs.repr (
pos + 4 *
ofs)) =
Some v
/\
Val.inject j (
ls (
S sl ofs ty))
v.
Proof.
Lemma set_location:
forall m j sp pos bound sl ls P ofs ty v v',
m |=
contains_locations j sp pos bound sl ls **
P ->
0 <=
ofs ->
ofs +
typesize ty <=
bound -> (
typealign ty |
ofs) ->
Val.inject j v v' ->
exists m',
store_stack m (
Vptr sp Ptrofs.zero)
ty (
Ptrofs.repr (
pos + 4 *
ofs))
v' =
Some m'
/\
m' |=
contains_locations j sp pos bound sl (
Locmap.set (
S sl ofs ty)
v ls) **
P.
Proof.
Lemma initial_locations:
forall j sp pos bound P sl ls m,
m |=
range sp pos (
pos + 4 *
bound) **
P ->
(8 |
pos) ->
(
forall ofs ty,
ls (
S sl ofs ty) =
Vundef) ->
m |=
contains_locations j sp pos bound sl ls **
P.
Proof.
intros.
destruct H as (
A &
B &
C).
destruct A as (
D &
E &
F).
split.
-
simpl;
intuition auto.
red;
intros;
eauto with mem.
destruct (
Mem.valid_access_load m (
chunk_of_type ty)
sp (
pos + 4 *
ofs))
as [
v LOAD].
eapply valid_access_location;
eauto.
red;
intros;
eauto with mem.
exists v;
split;
auto.
rewrite H1;
auto.
-
split;
assumption.
Qed.
Lemma contains_locations_exten:
forall ls ls'
j sp pos bound sl,
(
forall ofs ty,
Val.lessdef (
ls' (
S sl ofs ty)) (
ls (
S sl ofs ty))) ->
massert_imp (
contains_locations j sp pos bound sl ls)
(
contains_locations j sp pos bound sl ls').
Proof.
intros; split; simpl; intros; auto.
intuition auto. exploit H5; eauto. intros (v & A & B). exists v; split; auto.
specialize (H ofs ty). inv H. congruence. auto.
Qed.
Lemma contains_locations_incr:
forall j j'
sp pos bound sl ls,
inject_incr j j' ->
massert_imp (
contains_locations j sp pos bound sl ls)
(
contains_locations j'
sp pos bound sl ls).
Proof.
intros; split; simpl; intros; auto.
intuition auto. exploit H5; eauto. intros (v & A & B). exists v; eauto.
Qed.
contains_callee_saves j sp pos rl ls is a memory assertion that holds
if block sp, starting at offset pos, contains the values of the
callee-save registers rl as given by the location map ls,
up to the memory injection j. The memory layout of the registers in rl
is the same as that implemented by save_callee_save_rec.
Fixpoint contains_callee_saves (
j:
meminj) (
sp:
block) (
pos:
Z) (
rl:
list mreg) (
ls:
locset) :
massert :=
match rl with
|
nil =>
pure True
|
r ::
rl =>
let ty :=
mreg_type r in
let sz :=
AST.typesize ty in
let pos1 :=
align pos sz in
contains (
chunk_of_type ty)
sp pos1 (
fun v =>
Val.inject j (
ls (
R r))
v)
**
contains_callee_saves j sp (
pos1 +
sz)
rl ls
end.
Lemma contains_callee_saves_incr:
forall j j'
sp ls,
inject_incr j j' ->
forall rl pos,
massert_imp (
contains_callee_saves j sp pos rl ls)
(
contains_callee_saves j'
sp pos rl ls).
Proof.
Lemma contains_callee_saves_exten:
forall j sp ls ls'
rl pos,
(
forall r,
In r rl ->
ls' (
R r) =
ls (
R r)) ->
massert_eqv (
contains_callee_saves j sp pos rl ls)
(
contains_callee_saves j sp pos rl ls').
Proof.
induction rl as [ |
r1 rl];
simpl;
intros.
-
reflexivity.
-
apply sepconj_morph_2;
auto.
rewrite H by auto.
reflexivity.
Qed.
Separation logic assertions describing the stack frame at sp.
It must contain:
- the values of the Local stack slots of ls, as per contains_locations
- the values of the Outgoing stack slots of ls, as per contains_locations
- the parent pointer representing the back link to the caller's frame
- the retaddr pointer representing the saved return address
- the initial values of the used callee-save registers as given by ls0,
as per contains_callee_saves.
In addition, we use a nonseparating conjunction to record the fact that
we have full access rights on the stack frame, except the part that
represents the Linear stack data.
Definition frame_contents_1 (
j:
meminj) (
sp:
block) (
ls ls0:
locset) (
parent retaddr:
val) :=
contains_locations j sp fe.(
fe_ofs_local)
b.(
bound_local)
Local ls
**
contains_locations j sp fe_ofs_arg b.(
bound_outgoing)
Outgoing ls
**
hasvalue Mptr sp fe.(
fe_ofs_link)
parent
**
hasvalue Mptr sp fe.(
fe_ofs_retaddr)
retaddr
**
contains_callee_saves j sp fe.(
fe_ofs_callee_save)
b.(
used_callee_save)
ls0.
Definition frame_contents (
j:
meminj) (
sp:
block) (
ls ls0:
locset) (
parent retaddr:
val) :=
mconj (
frame_contents_1 j sp ls ls0 parent retaddr)
(
range sp 0
fe.(
fe_stack_data) **
range sp (
fe.(
fe_stack_data) +
b.(
bound_stack_data))
fe.(
fe_size)).
Accessing components of the frame.
Lemma frame_get_local:
forall ofs ty j sp ls ls0 parent retaddr m P,
m |=
frame_contents j sp ls ls0 parent retaddr **
P ->
slot_within_bounds b Local ofs ty ->
slot_valid f Local ofs ty =
true ->
exists v,
load_stack m (
Vptr sp Ptrofs.zero)
ty (
Ptrofs.repr (
offset_local fe ofs)) =
Some v
/\
Val.inject j (
ls (
S Local ofs ty))
v.
Proof.
Lemma frame_get_outgoing:
forall ofs ty j sp ls ls0 parent retaddr m P,
m |=
frame_contents j sp ls ls0 parent retaddr **
P ->
slot_within_bounds b Outgoing ofs ty ->
slot_valid f Outgoing ofs ty =
true ->
exists v,
load_stack m (
Vptr sp Ptrofs.zero)
ty (
Ptrofs.repr (
offset_arg ofs)) =
Some v
/\
Val.inject j (
ls (
S Outgoing ofs ty))
v.
Proof.
Lemma frame_get_parent:
forall j sp ls ls0 parent retaddr m P,
m |=
frame_contents j sp ls ls0 parent retaddr **
P ->
load_stack m (
Vptr sp Ptrofs.zero)
Tptr (
Ptrofs.repr fe.(
fe_ofs_link)) =
Some parent.
Proof.
Lemma frame_get_retaddr:
forall j sp ls ls0 parent retaddr m P,
m |=
frame_contents j sp ls ls0 parent retaddr **
P ->
load_stack m (
Vptr sp Ptrofs.zero)
Tptr (
Ptrofs.repr fe.(
fe_ofs_retaddr)) =
Some retaddr.
Proof.
Assigning a Local or Outgoing stack slot.
Lemma frame_set_local:
forall ofs ty v v'
j sp ls ls0 parent retaddr m P,
m |=
frame_contents j sp ls ls0 parent retaddr **
P ->
slot_within_bounds b Local ofs ty ->
slot_valid f Local ofs ty =
true ->
Val.inject j v v' ->
exists m',
store_stack m (
Vptr sp Ptrofs.zero)
ty (
Ptrofs.repr (
offset_local fe ofs))
v' =
Some m'
/\
m' |=
frame_contents j sp (
Locmap.set (
S Local ofs ty)
v ls)
ls0 parent retaddr **
P.
Proof.
Lemma frame_set_outgoing:
forall ofs ty v v'
j sp ls ls0 parent retaddr m P,
m |=
frame_contents j sp ls ls0 parent retaddr **
P ->
slot_within_bounds b Outgoing ofs ty ->
slot_valid f Outgoing ofs ty =
true ->
Val.inject j v v' ->
exists m',
store_stack m (
Vptr sp Ptrofs.zero)
ty (
Ptrofs.repr (
offset_arg ofs))
v' =
Some m'
/\
m' |=
frame_contents j sp (
Locmap.set (
S Outgoing ofs ty)
v ls)
ls0 parent retaddr **
P.
Proof.
Invariance by change of location maps.
Lemma frame_contents_exten:
forall ls ls0 ls'
ls0'
j sp parent retaddr P m,
(
forall ofs ty,
Val.lessdef (
ls' (
S Local ofs ty)) (
ls (
S Local ofs ty))) ->
(
forall ofs ty,
Val.lessdef (
ls' (
S Outgoing ofs ty)) (
ls (
S Outgoing ofs ty))) ->
(
forall r,
In r b.(
used_callee_save) ->
ls0' (
R r) =
ls0 (
R r)) ->
m |=
frame_contents j sp ls ls0 parent retaddr **
P ->
m |=
frame_contents j sp ls'
ls0'
parent retaddr **
P.
Proof.
Invariance by assignment to registers.
Corollary frame_set_reg:
forall r v j sp ls ls0 parent retaddr m P,
m |=
frame_contents j sp ls ls0 parent retaddr **
P ->
m |=
frame_contents j sp (
Locmap.set (
R r)
v ls)
ls0 parent retaddr **
P.
Proof.
Corollary frame_undef_regs:
forall j sp ls ls0 parent retaddr m P rl,
m |=
frame_contents j sp ls ls0 parent retaddr **
P ->
m |=
frame_contents j sp (
LTL.undef_regs rl ls)
ls0 parent retaddr **
P.
Proof.
Corollary frame_set_regpair:
forall j sp ls0 parent retaddr m P p v ls,
m |=
frame_contents j sp ls ls0 parent retaddr **
P ->
m |=
frame_contents j sp (
Locmap.setpair p v ls)
ls0 parent retaddr **
P.
Proof.
Corollary frame_set_res:
forall j sp ls0 parent retaddr m P res v ls,
m |=
frame_contents j sp ls ls0 parent retaddr **
P ->
m |=
frame_contents j sp (
Locmap.setres res v ls)
ls0 parent retaddr **
P.
Proof.
induction res;
simpl;
intros.
-
apply frame_set_reg;
auto.
-
auto.
-
eauto.
Qed.
Invariance by change of memory injection.
Lemma frame_contents_incr:
forall j sp ls ls0 parent retaddr m P j',
m |=
frame_contents j sp ls ls0 parent retaddr **
P ->
inject_incr j j' ->
m |=
frame_contents j'
sp ls ls0 parent retaddr **
P.
Proof.
Agreement between location sets and Mach states
Agreement with Mach register states
Definition agree_regs (
j:
meminj) (
ls:
locset) (
rs:
regset) :
Prop :=
forall r,
Val.inject j (
ls (
R r)) (
rs r).
Agreement over locations
Record agree_locs (
ls ls0:
locset) :
Prop :=
mk_agree_locs {
Unused registers have the same value as in the caller
agree_unused_reg:
forall r, ~(
mreg_within_bounds b r) ->
ls (
R r) =
ls0 (
R r);
Incoming stack slots have the same value as the
corresponding Outgoing stack slots in the caller
agree_incoming:
forall ofs ty,
In (
S Incoming ofs ty) (
regs_of_rpairs (
loc_parameters f.(
Linear.fn_sig))) ->
ls (
S Incoming ofs ty) =
ls0 (
S Outgoing ofs ty)
}.
Properties of agree_regs.
Values of registers
Lemma agree_reg:
forall j ls rs r,
agree_regs j ls rs ->
Val.inject j (
ls (
R r)) (
rs r).
Proof.
intros. auto.
Qed.
Lemma agree_reglist:
forall j ls rs rl,
agree_regs j ls rs ->
Val.inject_list j (
reglist ls rl) (
rs##
rl).
Proof.
induction rl;
simpl;
intros.
auto.
constructor;
auto using agree_reg.
Qed.
Hint Resolve agree_reg agree_reglist:
stacking.
Preservation under assignments of machine registers.
Lemma agree_regs_set_reg:
forall j ls rs r v v',
agree_regs j ls rs ->
Val.inject j v v' ->
agree_regs j (
Locmap.set (
R r)
v ls) (
Regmap.set r v'
rs).
Proof.
Lemma agree_regs_set_pair:
forall j p v v'
ls rs,
agree_regs j ls rs ->
Val.inject j v v' ->
agree_regs j (
Locmap.setpair p v ls) (
set_pair p v'
rs).
Proof.
Lemma agree_regs_set_res:
forall j res v v'
ls rs,
agree_regs j ls rs ->
Val.inject j v v' ->
agree_regs j (
Locmap.setres res v ls) (
set_res res v'
rs).
Proof.
Lemma agree_regs_exten:
forall j ls rs ls'
rs',
agree_regs j ls rs ->
(
forall r,
ls' (
R r) =
Vundef \/
ls' (
R r) =
ls (
R r) /\
rs'
r =
rs r) ->
agree_regs j ls'
rs'.
Proof.
intros; red; intros.
destruct (H0 r) as [A | [A B]].
rewrite A. constructor.
rewrite A; rewrite B; auto.
Qed.
Lemma agree_regs_undef_regs:
forall j rl ls rs,
agree_regs j ls rs ->
agree_regs j (
LTL.undef_regs rl ls) (
Mach.undef_regs rl rs).
Proof.
Lemma agree_regs_undef_caller_save_regs:
forall j ls rs,
agree_regs j ls rs ->
agree_regs j (
LTL.undef_caller_save_regs ls) (
Mach.undef_caller_save_regs rs).
Proof.
Preservation under assignment of stack slot
Lemma agree_regs_set_slot:
forall j ls rs sl ofs ty v,
agree_regs j ls rs ->
agree_regs j (
Locmap.set (
S sl ofs ty)
v ls)
rs.
Proof.
intros;
red;
intros.
rewrite Locmap.gso;
auto.
red.
auto.
Qed.
Preservation by increasing memory injections
Lemma agree_regs_inject_incr:
forall j ls rs j',
agree_regs j ls rs ->
inject_incr j j' ->
agree_regs j'
ls rs.
Proof.
intros; red; intros; eauto with stacking.
Qed.
Preservation at function entry.
Lemma agree_regs_call_regs:
forall j ls rs,
agree_regs j ls rs ->
agree_regs j (
call_regs ls)
rs.
Proof.
intros.
unfold call_regs;
intros;
red;
intros;
auto.
Qed.
Properties of agree_locs
Preservation under assignment of machine register.
Lemma agree_locs_set_reg:
forall ls ls0 r v,
agree_locs ls ls0 ->
mreg_within_bounds b r ->
agree_locs (
Locmap.set (
R r)
v ls)
ls0.
Proof.
intros.
inv H;
constructor;
auto;
intros.
rewrite Locmap.gso.
auto.
red.
intuition congruence.
Qed.
Lemma caller_save_reg_within_bounds:
forall r,
is_callee_save r =
false ->
mreg_within_bounds b r.
Proof.
intros; red; intros. congruence.
Qed.
Lemma agree_locs_set_pair:
forall ls0 p v ls,
agree_locs ls ls0 ->
forall_rpair (
fun r =>
is_callee_save r =
false)
p ->
agree_locs (
Locmap.setpair p v ls)
ls0.
Proof.
Lemma agree_locs_set_res:
forall ls0 res v ls,
agree_locs ls ls0 ->
(
forall r,
In r (
params_of_builtin_res res) ->
mreg_within_bounds b r) ->
agree_locs (
Locmap.setres res v ls)
ls0.
Proof.
Lemma agree_locs_undef_regs:
forall ls0 regs ls,
agree_locs ls ls0 ->
(
forall r,
In r regs ->
mreg_within_bounds b r) ->
agree_locs (
LTL.undef_regs regs ls)
ls0.
Proof.
Lemma agree_locs_undef_locs_1:
forall ls0 regs ls,
agree_locs ls ls0 ->
(
forall r,
In r regs ->
is_callee_save r =
false) ->
agree_locs (
LTL.undef_regs regs ls)
ls0.
Proof.
Lemma agree_locs_undef_locs:
forall ls0 regs ls,
agree_locs ls ls0 ->
existsb is_callee_save regs =
false ->
agree_locs (
LTL.undef_regs regs ls)
ls0.
Proof.
Preservation by assignment to local slot
Lemma agree_locs_set_slot:
forall ls ls0 sl ofs ty v,
agree_locs ls ls0 ->
slot_writable sl =
true ->
agree_locs (
Locmap.set (
S sl ofs ty)
v ls)
ls0.
Proof.
intros.
destruct H;
constructor;
intros.
-
rewrite Locmap.gso;
auto.
red;
auto.
-
rewrite Locmap.gso;
auto.
red.
left.
destruct sl;
discriminate.
Qed.
Preservation at return points (when ls is changed but not ls0).
Lemma agree_locs_return:
forall ls ls0 ls',
agree_locs ls ls0 ->
agree_callee_save ls'
ls ->
agree_locs ls'
ls0.
Proof.
intros.
red in H0.
inv H;
constructor;
auto;
intros.
-
rewrite H0;
auto.
unfold mreg_within_bounds in H.
tauto.
-
rewrite <-
agree_incoming0 by auto.
apply H0.
congruence.
Qed.
Lemma agree_callee_save_set_result:
forall sg v ls1 ls2,
agree_callee_save ls1 ls2 ->
agree_callee_save (
Locmap.setpair (
loc_result sg)
v ls1)
ls2.
Proof.
Lemma agree_callee_save_regs_set_result:
forall sg v ls1 ls2,
agree_callee_save_regs ls1 ls2 ->
agree_callee_save_regs (
Locmap.setpair (
loc_result sg)
v ls1)
ls2.
Proof.
Lemma agree_callee_save_after:
forall ls1 ls2,
agree_callee_save ls1 ls2 ->
agree_callee_save (
LTL.undef_caller_save_regs ls1)
ls2.
Proof.
intros;
red;
intros.
unfold LTL.undef_caller_save_regs.
destruct l;
simpl in *;
auto.
-
rewrite H0.
auto.
-
destruct sl;
auto.
congruence.
Qed.
Lemma agree_callee_save_regs_after:
forall ls1 ls2,
agree_callee_save_regs ls1 ls2 ->
agree_callee_save_regs (
LTL.undef_caller_save_regs ls1)
ls2.
Proof.
Properties of destroyed registers.
Definition no_callee_saves (
l:
list mreg) :
Prop :=
existsb is_callee_save l =
false.
Remark destroyed_by_op_caller_save:
forall op,
no_callee_saves (
destroyed_by_op op).
Proof.
unfold no_callee_saves;
destruct op; (
reflexivity ||
destruct c;
reflexivity).
Qed.
Remark destroyed_by_load_caller_save:
forall chunk addr,
no_callee_saves (
destroyed_by_load chunk addr).
Proof.
Remark destroyed_by_store_caller_save:
forall chunk addr,
no_callee_saves (
destroyed_by_store chunk addr).
Proof.
Remark destroyed_by_cond_caller_save:
forall cond,
no_callee_saves (
destroyed_by_cond cond).
Proof.
Remark destroyed_by_jumptable_caller_save:
no_callee_saves destroyed_by_jumptable.
Proof.
red; reflexivity.
Qed.
Remark destroyed_by_setstack_caller_save:
forall ty,
no_callee_saves (
destroyed_by_setstack ty).
Proof.
Remark destroyed_at_function_entry_caller_save:
no_callee_saves destroyed_at_function_entry.
Proof.
red; reflexivity.
Qed.
Hint Resolve destroyed_by_op_caller_save destroyed_by_load_caller_save
destroyed_by_store_caller_save
destroyed_by_cond_caller_save destroyed_by_jumptable_caller_save
destroyed_at_function_entry_caller_save:
stacking.
Remark destroyed_by_setstack_function_entry:
forall ty,
incl (
destroyed_by_setstack ty)
destroyed_at_function_entry.
Proof.
Remark transl_destroyed_by_op:
forall op e,
destroyed_by_op (
transl_op e op) =
destroyed_by_op op.
Proof.
intros; destruct op; reflexivity.
Qed.
Remark transl_destroyed_by_load:
forall chunk addr e,
destroyed_by_load chunk (
transl_addr e addr) =
destroyed_by_load chunk addr.
Proof.
intros; destruct chunk; reflexivity.
Qed.
Remark transl_destroyed_by_store:
forall chunk addr e,
destroyed_by_store chunk (
transl_addr e addr) =
destroyed_by_store chunk addr.
Proof.
intros; destruct chunk; reflexivity.
Qed.
Let step :=
Mach.step return_address_offset.
Correctness of saving and restoring of callee-save registers
The following lemmas show the correctness of the register saving
code generated by save_callee_save: after this code has executed,
the register save areas of the current frame do contain the
values of the callee-save registers used by the function.
Section SAVE_CALLEE_SAVE.
Variable j:
meminj.
Variable cs:
list stackframe.
Variable fb:
block.
Variable sp:
block.
Variable ls:
locset.
Hypothesis ls_temp_undef:
forall ty r,
In r (
destroyed_by_setstack ty) ->
ls (
R r) =
Vundef.
Hypothesis wt_ls:
forall r,
Val.has_type (
ls (
R r)) (
mreg_type r).
Lemma save_callee_save_rec_correct:
forall k l pos rs m P (
ext_tgt:
block ->
Z ->
Prop),
(
forall r,
In r l ->
is_callee_save r =
true) ->
m |=
range sp pos (
size_callee_save_area_rec l pos) **
P ->
agree_regs j ls rs ->
(
forall b i,
ext_tgt b i -> (
Pos.succ b <
Mem.nextblock m)%
positive) ->
Pos.succ sp =
Mem.nextblock m ->
exists rs',
exists m',
star step tse tge
(
State cs fb (
Vptr sp Ptrofs.zero) (
save_callee_save_rec l pos k)
rs m)
E0 (
State cs fb (
Vptr sp Ptrofs.zero)
k rs'
m')
/\
m' |=
contains_callee_saves j sp pos l ls **
P
/\ (
forall ofs k p,
Mem.perm m sp ofs k p ->
Mem.perm m'
sp ofs k p)
/\
Mem.unchanged_on ext_tgt m m'
/\ (
forall b ofs p,
Mem.valid_block m b ->
Mem.perm m'
b ofs Max p ->
Mem.perm m b ofs Max p)
/\
agree_regs j ls rs'.
Proof.
End SAVE_CALLEE_SAVE.
Remark LTL_undef_regs_same:
forall r rl ls,
In r rl ->
LTL.undef_regs rl ls (
R r) =
Vundef.
Proof.
induction rl;
simpl;
intros.
contradiction.
unfold Locmap.set.
destruct (
Loc.eq (
R a) (
R r)).
auto.
destruct (
Loc.diff_dec (
R a) (
R r));
auto.
apply IHrl.
intuition congruence.
Qed.
Remark LTL_undef_regs_others:
forall r rl ls, ~
In r rl ->
LTL.undef_regs rl ls (
R r) =
ls (
R r).
Proof.
induction rl;
simpl;
intros.
auto.
rewrite Locmap.gso.
apply IHrl.
intuition.
red.
intuition.
Qed.
Remark LTL_undef_regs_slot:
forall sl ofs ty rl ls,
LTL.undef_regs rl ls (
S sl ofs ty) =
ls (
S sl ofs ty).
Proof.
induction rl;
simpl;
intros.
auto.
rewrite Locmap.gso.
apply IHrl.
red;
auto.
Qed.
Remark undef_regs_type:
forall ty l rl ls,
Val.has_type (
ls l)
ty ->
Val.has_type (
LTL.undef_regs rl ls l)
ty.
Proof.
induction rl;
simpl;
intros.
-
auto.
-
unfold Locmap.set.
destruct (
Loc.eq (
R a)
l).
red;
auto.
destruct (
Loc.diff_dec (
R a)
l);
auto.
red;
auto.
Qed.
Lemma save_callee_save_correct:
forall j ls ls0 rs sp cs fb k m P (
ext_tgt:
block ->
Z ->
Prop),
m |=
range sp fe.(
fe_ofs_callee_save) (
size_callee_save_area b fe.(
fe_ofs_callee_save)) **
P ->
(
forall r,
Val.has_type (
ls (
R r)) (
mreg_type r)) ->
agree_callee_save ls ls0 ->
agree_regs j ls rs ->
(
forall b i,
ext_tgt b i -> (
Pos.succ b <
Mem.nextblock m)%
positive) ->
Pos.succ sp =
Mem.nextblock m ->
let ls1 :=
LTL.undef_regs destroyed_at_function_entry (
LTL.call_regs ls)
in
let rs1 :=
undef_regs destroyed_at_function_entry rs in
exists rs',
exists m',
star step tse tge
(
State cs fb (
Vptr sp Ptrofs.zero) (
save_callee_save fe k)
rs1 m)
E0 (
State cs fb (
Vptr sp Ptrofs.zero)
k rs'
m')
/\
m' |=
contains_callee_saves j sp fe.(
fe_ofs_callee_save)
b.(
used_callee_save)
ls0 **
P
/\ (
forall ofs k p,
Mem.perm m sp ofs k p ->
Mem.perm m'
sp ofs k p)
/\
Mem.unchanged_on ext_tgt m m'
/\ (
forall b ofs p,
Mem.valid_block m b ->
Mem.perm m'
b ofs Max p ->
Mem.perm m b ofs Max p)
/\
agree_regs j ls1 rs'.
Proof.
As a corollary of the previous lemmas, we obtain the following
correctness theorem for the execution of a function prologue
(allocation of the frame + saving of the link and return address +
saving of the used callee-save registers).
Lemma function_prologue_correct:
forall j ls ls0 ls1 rs rs1 m1 m1'
m2 sp parent ra cs fb k P (
ext_tgt:
block ->
Z ->
Prop),
agree_regs j ls rs ->
agree_callee_save ls ls0 ->
agree_outgoing_arguments (
Linear.fn_sig f)
ls ls0 ->
(
forall r,
Val.has_type (
ls (
R r)) (
mreg_type r)) ->
ls1 =
LTL.undef_regs destroyed_at_function_entry (
LTL.call_regs ls) ->
rs1 =
undef_regs destroyed_at_function_entry rs ->
Mem.alloc m1 0
f.(
Linear.fn_stacksize) = (
m2,
sp) ->
Val.has_type parent Tptr ->
Val.has_type ra Tptr ->
m1' |=
minjection j m1 **
globalenv_inject ge j **
P ->
(
forall b i,
ext_tgt b i -> (
b <
Mem.nextblock m1')%
positive) ->
exists j',
exists rs',
exists m2',
exists sp',
exists m3',
exists m4',
exists m5',
Mem.alloc m1' 0
tf.(
fn_stacksize) = (
m2',
sp')
/\
store_stack m2' (
Vptr sp'
Ptrofs.zero)
Tptr tf.(
fn_link_ofs)
parent =
Some m3'
/\
store_stack m3' (
Vptr sp'
Ptrofs.zero)
Tptr tf.(
fn_retaddr_ofs)
ra =
Some m4'
/\
star step tse tge
(
State cs fb (
Vptr sp'
Ptrofs.zero) (
save_callee_save fe k)
rs1 m4')
E0 (
State cs fb (
Vptr sp'
Ptrofs.zero)
k rs'
m5')
/\
agree_regs j'
ls1 rs'
/\
agree_locs ls1 ls0
/\
m5' |=
frame_contents j'
sp'
ls1 ls0 parent ra **
minjection j'
m2 **
globalenv_inject ge j' **
P
/\
j'
sp =
Some(
sp',
fe.(
fe_stack_data))
/\
inject_separated j j'
m1 m1'
/\
Mem.unchanged_on ext_tgt m4'
m5'
/\ (
forall b ofs p,
Mem.valid_block m4'
b ->
Mem.perm m5'
b ofs Max p ->
Mem.perm m4'
b ofs Max p)
/\
inject_incr j j'.
Proof.
intros until ext_tgt;
intros AGREGS AGCS AGARGS WTREGS LS1 RS1 ALLOC TYPAR TYRA SEP EXT_TGT_BOUND.
rewrite unfold_transf_function.
unfold fn_stacksize,
fn_link_ofs,
fn_retaddr_ofs.
Local Opaque b fe.
generalize (
frame_env_range b) (
frame_env_aligned b).
replace (
make_env b)
with fe by auto.
simpl.
intros LAYOUT1 LAYOUT2.
destruct (
Mem.alloc m1' 0 (
fe_size fe))
as [
m2'
sp']
eqn:
ALLOC'.
exploit alloc_parallel_rule_2.
eexact SEP.
eexact ALLOC.
eexact ALLOC'.
instantiate (1 :=
fe_stack_data fe).
tauto.
reflexivity.
instantiate (1 :=
fe_stack_data fe +
bound_stack_data b).
rewrite Z.max_comm.
reflexivity.
generalize (
bound_stack_data_pos b)
size_no_overflow;
omega.
tauto.
tauto.
clear SEP.
intros (
j' &
SEP &
INCR &
SAME &
INJ_SEP).
assert (
SEPCONJ:
m2' |=
mconj (
range sp' 0 (
fe_stack_data fe) **
range sp' (
fe_stack_data fe +
bound_stack_data b) (
fe_size fe))
(
range sp' 0 (
fe_stack_data fe) **
range sp' (
fe_stack_data fe +
bound_stack_data b) (
fe_size fe))
**
minjection j'
m2 **
globalenv_inject ge j' **
P).
{
apply mconj_intro;
rewrite sep_assoc;
assumption. }
apply (
frame_env_separated b)
in SEP.
replace (
make_env b)
with fe in SEP by auto.
rewrite sep_swap3 in SEP.
apply (
range_contains Mptr)
in SEP; [|
tauto].
exploit (
contains_set_stack (
fun v' =>
v' =
parent)
parent (
fun _ =>
True)
m2'
Tptr).
rewrite chunk_of_Tptr;
eexact SEP.
apply Val.load_result_same;
auto.
clear SEP;
intros (
m3' &
STORE_PARENT &
SEP).
rewrite sep_swap3 in SEP.
rewrite sep_swap4 in SEP.
apply (
range_contains Mptr)
in SEP; [|
tauto].
exploit (
contains_set_stack (
fun v' =>
v' =
ra)
ra (
fun _ =>
True)
m3'
Tptr).
rewrite chunk_of_Tptr;
eexact SEP.
apply Val.load_result_same;
auto.
clear SEP;
intros (
m4' &
STORE_RETADDR &
SEP).
rewrite sep_swap4 in SEP.
rewrite sep_swap5 in SEP.
assert(
TT:
Mem.nextblock m4' =
Pos.succ (
Mem.nextblock m1')).
{
unfold store_stack,
Mem.storev in *.
ss.
erewrite Mem.nextblock_store;
eauto.
erewrite Mem.nextblock_store;
eauto.
erewrite Mem.nextblock_alloc;
eauto. }
exploit (
save_callee_save_correct j'
ls ls0 rs);
eauto.
apply agree_regs_inject_incr with j;
auto.
{
rewrite TT.
ii.
exploit EXT_TGT_BOUND;
eauto.
xomega. }
{
rewrite TT.
exploit Mem.alloc_result;
eauto.
ii.
congruence. }
replace (
LTL.undef_regs destroyed_at_function_entry (
call_regs ls))
with ls1 by auto.
replace (
undef_regs destroyed_at_function_entry rs)
with rs1 by auto.
clear SEP;
intros (
rs2 &
m5' &
SAVE_CS &
SEP &
PERMS &
UNCH &
MAX &
AGREGS').
rewrite sep_swap5 in SEP.
exploit (
initial_locations j').
eexact SEP.
tauto.
instantiate (1 :=
Local).
instantiate (1 :=
ls1).
intros;
rewrite LS1.
rewrite LTL_undef_regs_slot.
reflexivity.
clear SEP;
intros SEP.
rewrite sep_swap in SEP.
exploit (
initial_locations j').
eexact SEP.
tauto.
instantiate (1 :=
Outgoing).
instantiate (1 :=
ls1).
intros;
rewrite LS1.
rewrite LTL_undef_regs_slot.
reflexivity.
clear SEP;
intros SEP.
rewrite sep_swap in SEP.
assert (
SEPFINAL:
m5' |=
frame_contents j'
sp'
ls1 ls0 parent ra **
minjection j'
m2 **
globalenv_inject ge j' **
P).
{
eapply frame_mconj.
eexact SEPCONJ.
rewrite chunk_of_Tptr in SEP.
unfold frame_contents_1;
rewrite !
sep_assoc.
exact SEP.
assert (
forall ofs k p,
Mem.perm m2'
sp'
ofs k p ->
Mem.perm m5'
sp'
ofs k p).
{
intros.
apply PERMS.
unfold store_stack in STORE_PARENT,
STORE_RETADDR.
simpl in STORE_PARENT,
STORE_RETADDR.
eauto using Mem.perm_store_1. }
eapply sep_preserved.
eapply sep_proj1.
eapply mconj_proj2.
eexact SEPCONJ.
intros;
apply range_preserved with m2';
auto.
intros;
apply range_preserved with m2';
auto.
}
clear SEP SEPCONJ.
exists j',
rs2,
m2',
sp',
m3',
m4',
m5'.
split.
auto.
split.
exact STORE_PARENT.
split.
exact STORE_RETADDR.
split.
eexact SAVE_CS.
split.
exact AGREGS'.
split.
rewrite LS1.
apply agree_locs_undef_locs; [|
reflexivity].
constructor;
intros.
unfold call_regs.
apply AGCS.
unfold mreg_within_bounds in H;
tauto.
unfold call_regs.
apply AGARGS.
apply incoming_slot_in_parameters;
auto.
split.
exact SEPFINAL.
split.
exact SAME.
split.
exact INJ_SEP.
split.
exact UNCH.
split.
exact MAX.
exact INCR.
Qed.
The following lemmas show the correctness of the register reloading
code generated by reload_callee_save: after this code has executed,
all callee-save registers contain the same values they had at
function entry.
Section RESTORE_CALLEE_SAVE.
Variable j:
meminj.
Variable cs:
list stackframe.
Variable fb:
block.
Variable sp:
block.
Variable ls0:
locset.
Variable m:
mem.
Definition agree_unused (
ls0:
locset) (
rs:
regset) :
Prop :=
forall r, ~(
mreg_within_bounds b r) ->
Val.inject j (
ls0 (
R r)) (
rs r).
Lemma restore_callee_save_rec_correct:
forall l ofs rs k,
m |=
contains_callee_saves j sp ofs l ls0 ->
agree_unused ls0 rs ->
(
forall r,
In r l ->
mreg_within_bounds b r) ->
exists rs',
star step tse tge
(
State cs fb (
Vptr sp Ptrofs.zero) (
restore_callee_save_rec l ofs k)
rs m)
E0 (
State cs fb (
Vptr sp Ptrofs.zero)
k rs'
m)
/\ (
forall r,
In r l ->
Val.inject j (
ls0 (
R r)) (
rs'
r))
/\ (
forall r, ~(
In r l) ->
rs'
r =
rs r)
/\
agree_unused ls0 rs'.
Proof.
Local Opaque mreg_type.
induction l as [ |
r l];
simpl;
intros.
-
exists rs.
intuition auto.
apply star_refl.
-
set (
ty :=
mreg_type r)
in *.
set (
sz :=
AST.typesize ty)
in *.
set (
ofs1 :=
align ofs sz).
assert (
SZPOS:
sz > 0)
by (
apply AST.typesize_pos).
assert (
OFSLE:
ofs <=
ofs1)
by (
apply align_le;
auto).
assert (
BOUND:
mreg_within_bounds b r)
by eauto.
exploit contains_get_stack.
eapply sep_proj1;
eassumption.
intros (
v &
LOAD &
SPEC).
exploit (
IHl (
ofs1 +
sz) (
rs#
r <-
v)).
eapply sep_proj2;
eassumption.
red;
intros.
rewrite Regmap.gso.
auto.
intuition congruence.
eauto.
intros (
rs' &
A &
B &
C &
D).
exists rs'.
split.
eapply star_step;
eauto.
econstructor.
exact LOAD.
traceEq.
split.
intros.
destruct (
In_dec mreg_eq r0 l).
auto.
assert (
r =
r0)
by tauto.
subst r0.
rewrite C by auto.
rewrite Regmap.gss.
exact SPEC.
split.
intros.
rewrite C by tauto.
apply Regmap.gso.
intuition auto.
exact D.
Qed.
End RESTORE_CALLEE_SAVE.
Lemma restore_callee_save_correct:
forall m j sp ls ls0 pa ra P rs k cs fb,
m |=
frame_contents j sp ls ls0 pa ra **
P ->
agree_unused j ls0 rs ->
exists rs',
star step tse tge
(
State cs fb (
Vptr sp Ptrofs.zero) (
restore_callee_save fe k)
rs m)
E0 (
State cs fb (
Vptr sp Ptrofs.zero)
k rs'
m)
/\ (
forall r,
is_callee_save r =
true ->
Val.inject j (
ls0 (
R r)) (
rs'
r))
/\ (
forall r,
is_callee_save r =
false ->
rs'
r =
rs r).
Proof.
As a corollary, we obtain the following correctness result for
the execution of a function epilogue (reloading of used callee-save
registers + reloading of the link and return address + freeing
of the frame).
Lemma function_epilogue_correct:
forall m'
j sp'
ls ls0 pa ra P m rs sp m1 k cs fb,
m' |=
frame_contents j sp'
ls ls0 pa ra **
minjection j m **
P ->
agree_regs j ls rs ->
agree_locs ls ls0 ->
j sp =
Some(
sp',
fe.(
fe_stack_data)) ->
Mem.free m sp 0
f.(
Linear.fn_stacksize) =
Some m1 ->
exists rs1,
exists m1',
load_stack m' (
Vptr sp'
Ptrofs.zero)
Tptr tf.(
fn_link_ofs) =
Some pa
/\
load_stack m' (
Vptr sp'
Ptrofs.zero)
Tptr tf.(
fn_retaddr_ofs) =
Some ra
/\
Mem.free m'
sp' 0
tf.(
fn_stacksize) =
Some m1'
/\
star step tse tge
(
State cs fb (
Vptr sp'
Ptrofs.zero) (
restore_callee_save fe k)
rs m')
E0 (
State cs fb (
Vptr sp'
Ptrofs.zero)
k rs1 m')
/\
agree_regs j (
return_regs ls0 ls)
rs1
/\
agree_callee_save (
return_regs ls0 ls)
ls0
/\
m1' |=
minjection j m1 **
P.
Proof.
End FRAME_PROPERTIES.
Call stack invariants
This is the memory assertion that captures the contents of the stack frames
mentioned in the call stacks.
Definition dummy_frame_contents (
j:
meminj) (
ls:
locset) (
sg:
signature) (
sp:
block) (
spofs:
Z):
massert :=
(
contains_locations j sp spofs (
size_arguments sg)
Outgoing ls).
Lemma dummy_frame_contents_incr
j ls sg sp spofs j'
m P
(
DUMMY:
m |=
dummy_frame_contents j ls sg sp spofs **
P)
(
INCR:
inject_incr j j'):
<<
DUMMY:
m |=
dummy_frame_contents j'
ls sg sp spofs **
P>>.
Proof.
Fixpoint stack_contents_noargs (
j:
meminj) (
cs:
list Linear.stackframe) (
cs':
list Mach.stackframe) :
massert :=
match cs,
cs'
with
|
nil,
nil =>
pure True
|
Linear.Stackframe f _ ls c ::
cs,
Mach.Stackframe fb (
Vptr sp'
_)
ra c' ::
cs' =>
frame_contents f j sp'
ls (
parent_locset cs) (
parent_sp cs') (
parent_ra cs')
**
stack_contents_noargs j cs cs'
|
_,
_ =>
pure False
end.
Fixpoint stack_contents_args (
j:
meminj) (
cs:
list Linear.stackframe) (
cs':
list Mach.stackframe) :
massert :=
match cs,
cs'
with
| [
Linear.Stackframe f _ ls _], [
Mach.Stackframe fb (
Vptr sp'
spofs)
ra _] =>
dummy_frame_contents j ls f.(
Linear.fn_sig)
sp'
spofs.(
Ptrofs.unsigned)
|
Linear.Stackframe f _ ls c ::
cs,
Mach.Stackframe fb (
Vptr sp'
_)
ra c' ::
cs' =>
frame_contents f j sp'
ls (
parent_locset cs) (
parent_sp cs') (
parent_ra cs')
**
stack_contents_args j cs cs'
|
_,
_ =>
pure False
end.
Notation "'
stack_contents'" := (
if main_args then stack_contents_args else stack_contents_noargs)
(
only parsing).
Lemma stack_contents_nil_left_false:
forall j cs',
stack_contents_args j []
cs' =
pure False.
Proof.
ss; des_ifs. Qed.
Lemma stack_contents_nil_right_false:
forall j cs,
stack_contents_args j cs [] =
pure False.
Proof.
destruct cs; ss; des_ifs; ss; des_ifs. Qed.
match_stacks captures additional properties (not related to memory)
of the Linear and Mach call stacks.
Inductive match_stacks (
j:
meminj):
list Linear.stackframe ->
list stackframe ->
signature ->
SimMemInj.t' ->
Prop :=
|
match_stacks_empty:
forall sg sm0,
forall (
MAINARGS:
main_args =
false),
forall (
SYMBINJ:
symbols_inject j se tse),
tailcall_possible sg ->
match_stacks j nil nil sg sm0
|
match_stacks_dummy
(
MAINARGS:
main_args =
true)
(
SYMBINJ:
symbols_inject j se tse)
sg_init sp ls_init sg ra sm0
(
RAPTR:
Val.has_type ra Tptr)
(
ARGS:
forall ofs ty
(
LOC:
In (
S Outgoing ofs ty) (
regs_of_rpairs (
loc_arguments sg_init))),
<<
BOUND:
ofs +
typesize ty <=
size_arguments sg_init>>)
(
LE:
sg =
sg_init \/
tailcall_possible sg)
(
SPVALID:
sm0.(
SimMemInj.tgt).(
Mem.valid_block)
sp /\
Ple sm0.(
SimMemInj.tgt_parent_nb)
sp /\
forall i, ~
sm0.(
SimMemInj.tgt_external)
sp i):
match_stacks j [
Linear.dummy_stack sg_init ls_init]
[
Mach.dummy_stack (
Vptr sp Ptrofs.zero)
ra]
sg sm0
|
match_stacks_cons:
forall f sp ls c cs fb sp'
ra c'
cs'
sg trf sm0
(
SPVALID:
sm0.(
SimMemInj.tgt).(
Mem.valid_block)
sp' /\
Ple sm0.(
SimMemInj.tgt_parent_nb)
sp' /\
forall i, ~
sm0.(
SimMemInj.tgt_external)
sp'
i)
(
PRIV:
forall i, 0 <=
i < (
fe_stack_data (
make_env (
function_bounds f))) \/
fe_stack_data (
make_env (
function_bounds f)) +
Linear.fn_stacksize f <=
i <
fe_size (
make_env (
function_bounds f))
->
sm0.(
SimMemInj.tgt_private)
sp'
i)
(
TAIL:
is_tail c (
Linear.fn_code f))
(
FINDF:
Genv.find_funct_ptr tge fb =
Some (
Internal trf))
(
TRF:
transf_function f =
OK trf)
(
TRC:
transl_code (
make_env (
function_bounds f))
c =
c')
(
INJ:
j sp =
Some(
sp', (
fe_stack_data (
make_env (
function_bounds f)))))
(
TY_RA:
Val.has_type ra Tptr)
(
AGL:
agree_locs f ls (
parent_locset cs))
(
ARGS:
forall ofs ty,
In (
S Outgoing ofs ty) (
regs_of_rpairs (
loc_arguments sg)) ->
slot_within_bounds (
function_bounds f)
Outgoing ofs ty)
(
STK:
match_stacks j cs cs' (
Linear.fn_sig f)
sm0)
(
SZARG:
size_arguments sg <=
bound_outgoing (
function_bounds f)),
match_stacks j
(
Linear.Stackframe f (
Vptr sp Ptrofs.zero)
ls c ::
cs)
(
Stackframe fb (
Vptr sp'
Ptrofs.zero)
ra c' ::
cs')
sg sm0.
Invariance with respect to change of memory injection.
Ltac sep_simpl_tac :=
unfold NW in *;
repeat (
try rewrite sep_assoc in *;
try rewrite sep_pure in *;
try rewrite stack_contents_nil_left_false in *;
try assumption;
try rewrite stack_contents_nil_right_false in *;
try assumption;
try match goal with
| [
H:
_ |=
pure False |-
_] =>
simpl in H;
inv H
| [
H:
_ |=
_ **
pure False |-
_] =>
apply sep_proj2 in H
| [
H:
_ |=
_ **
pure False **
_ |-
_] =>
apply sep_pick2 in H
end;
idtac).
Lemma stack_contents_change_meminj:
forall m j j',
inject_incr j j' ->
forall cs cs'
P,
m |=
stack_contents j cs cs' **
P ->
m |=
stack_contents j'
cs cs' **
P.
Proof.
Local Opaque sepconj.
destruct main_args eqn:
MAINARGS;
cycle 1.
-
induction cs as [ | []
cs];
destruct cs'
as [ | []
cs'];
simpl;
intros;
auto.
destruct sp0;
auto.
rewrite sep_assoc in *.
apply frame_contents_incr with (
j :=
j);
auto.
rewrite sep_swap.
apply IHcs.
rewrite sep_swap.
assumption.
-
induction cs as [ | []
cs];
destruct cs'
as [ | []
cs'];
simpl;
intros;
auto.
destruct sp0;
auto.
destruct cs,
cs';
sep_simpl_tac;
des;
try congruence.
{
eapply dummy_frame_contents_incr;
eauto. }
apply frame_contents_incr with (
j :=
j);
auto.
rewrite sep_swap.
apply IHcs.
rewrite sep_swap.
assumption.
Qed.
Lemma spvalid_le
sm0 sm1 sp
(
SPVALID:
sm0.(
SimMemInj.tgt).(
Mem.valid_block)
sp /\
Ple sm0.(
SimMemInj.tgt_parent_nb)
sp /\
forall i, ~
sm0.(
SimMemInj.tgt_external)
sp i)
(
LE:
SimMemInj.le'
sm0 sm1):
<<
SPVALID:
sm1.(
SimMemInj.tgt).(
Mem.valid_block)
sp /\
Ple sm1.(
SimMemInj.tgt_parent_nb)
sp /\
forall i, ~
sm1.(
SimMemInj.tgt_external)
sp i>>.
Proof.
Lemma match_stacks_symbols_inject
j cs cs'
sg sm0
(
MCS:
match_stacks j cs cs'
sg sm0):
<<
SYMBINJ:
symbols_inject j se tse>>.
Proof.
induction MCS; auto. Qed.
Lemma match_stacks_change_meminj:
forall j j',
inject_incr j j' ->
forall (
SAMESRC:
forall b1 b2 delta,
j'
b1 =
Some(
b2,
delta) ->
Plt b1 se.(
Senv.nextblock) ->
j b1 =
Some(
b2,
delta)),
forall (
SAMETGT:
forall b1 b2 delta,
j'
b1 =
Some(
b2,
delta) ->
Plt b2 tse.(
Senv.nextblock) ->
j b1 =
Some(
b2,
delta)),
forall cs cs'
sg sm0,
match_stacks j cs cs'
sg sm0 ->
match_stacks j'
cs cs'
sg sm0.
Proof.
Lemma match_stacks_le:
forall j cs cs'
sg sm0 sm1
(
LE:
SimMemInj.le'
sm0 sm1)
(
INJ:
forall b b2 delta,
Mem.valid_block (
SimMemInj.tgt sm0)
b2 ->
SimMemInj.inj sm1 b =
Some (
b2,
delta)
->
SimMemInj.inj sm0 b =
Some (
b2,
delta))
(
PERM:
forall b b2 delta i,
Mem.valid_block (
SimMemInj.tgt sm0)
b2 ->
SimMemInj.inj sm1 b =
Some (
b2,
delta)
->
Mem.perm (
SimMemInj.src sm1)
b i Max Nonempty ->
Mem.perm (
SimMemInj.src sm0)
b i Max Nonempty),
match_stacks j cs cs'
sg sm0 ->
match_stacks j cs cs'
sg sm1.
Proof.
Invariance with respect to change of signature.
Lemma match_stacks_change_sig:
forall sg1 j cs cs'
sg sm0,
match_stacks j cs cs'
sg sm0 ->
tailcall_possible sg1 ->
match_stacks j cs cs'
sg1 sm0.
Proof.
induction 1;
intros;
econstructor;
eauto.
intros.
elim (
H0 _ H1).
rewrite tailcall_size;
try assumption;
try xomega.
hexploit (
size_arguments_above sg);
eauto.
i;
xomega.
Qed.
Typing properties of match_stacks.
Lemma match_stacks_type_sp:
forall j cs cs'
sg sm0,
match_stacks j cs cs'
sg sm0 ->
Val.has_type (
parent_sp cs')
Tptr.
Proof.
Lemma match_stacks_type_retaddr:
forall j cs cs'
sg sm0,
match_stacks j cs cs'
sg sm0 ->
Val.has_type (
parent_ra cs')
Tptr.
Proof.
Syntactic properties of the translation
Preservation of code labels through the translation.
Section LABELS.
Remark find_label_save_callee_save:
forall lbl l ofs k,
Mach.find_label lbl (
save_callee_save_rec l ofs k) =
Mach.find_label lbl k.
Proof.
induction l; simpl; auto.
Qed.
Remark find_label_restore_callee_save:
forall lbl l ofs k,
Mach.find_label lbl (
restore_callee_save_rec l ofs k) =
Mach.find_label lbl k.
Proof.
induction l; simpl; auto.
Qed.
Lemma transl_code_eq:
forall fe i c,
transl_code fe (
i ::
c) =
transl_instr fe i (
transl_code fe c).
Proof.
Lemma find_label_transl_code:
forall fe lbl c,
Mach.find_label lbl (
transl_code fe c) =
option_map (
transl_code fe) (
Linear.find_label lbl c).
Proof.
Lemma transl_find_label:
forall f tf lbl c,
transf_function f =
OK tf ->
Linear.find_label lbl f.(
Linear.fn_code) =
Some c ->
Mach.find_label lbl tf.(
Mach.fn_code) =
Some (
transl_code (
make_env (
function_bounds f))
c).
Proof.
End LABELS.
Code tail property for Linear executions.
Lemma find_label_tail:
forall lbl c c',
Linear.find_label lbl c =
Some c' ->
is_tail c'
c.
Proof.
induction c;
simpl.
intros;
discriminate.
intro c'.
case (
Linear.is_label lbl a);
intros.
injection H;
intro;
subst c'.
auto with coqlib.
auto with coqlib.
Qed.
Code tail property for translations
Lemma is_tail_save_callee_save:
forall l ofs k,
is_tail k (
save_callee_save_rec l ofs k).
Proof.
induction l; intros; simpl. auto with coqlib.
constructor; auto.
Qed.
Lemma is_tail_restore_callee_save:
forall l ofs k,
is_tail k (
restore_callee_save_rec l ofs k).
Proof.
induction l; intros; simpl. auto with coqlib.
constructor; auto.
Qed.
Lemma is_tail_transl_instr:
forall fe i k,
is_tail k (
transl_instr fe i k).
Proof.
Lemma is_tail_transl_code:
forall fe c1 c2,
is_tail c1 c2 ->
is_tail (
transl_code fe c1) (
transl_code fe c2).
Proof.
Lemma is_tail_transf_function:
forall f tf c,
transf_function f =
OK tf ->
is_tail c (
Linear.fn_code f) ->
is_tail (
transl_code (
make_env (
function_bounds f))
c) (
fn_code tf).
Proof.
Semantic preservation
Preservation / translation of global symbols and functions.
Hypothesis (
MATCH_GENV:
Genv.match_genvs (
match_globdef (
fun _ f tf =>
transf_fundef f =
OK tf)
eq prog)
ge tge).
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof (
Genv.find_symbol_match_genv MATCH_GENV).
Lemma senv_preserved:
Senv.equiv ge tge.
Proof (
Genv.senv_match_genv MATCH_GENV).
Lemma functions_translated:
forall v f,
Genv.find_funct ge v =
Some f ->
exists tf,
Genv.find_funct tge v =
Some tf /\
transf_fundef f =
OK tf.
Proof (
Genv.find_funct_transf_partial_genv MATCH_GENV).
Lemma function_ptr_translated:
forall b f,
Genv.find_funct_ptr ge b =
Some f ->
exists tf,
Genv.find_funct_ptr tge b =
Some tf /\
transf_fundef f =
OK tf.
Proof (
Genv.find_funct_ptr_transf_partial_genv MATCH_GENV).
Lemma sig_preserved:
forall f tf,
transf_fundef f =
OK tf ->
Mach.funsig tf =
Linear.funsig f.
Proof.
Lemma find_function_ptr_translated:
forall j ls rs m ros fptr,
agree_regs j ls rs ->
m |=
globalenv_inject ge j ->
Linear.find_function_ptr ge ros ls =
fptr ->
exists tfptr,
<<
TFPTR:
find_function_ptr tge ros rs =
tfptr>>
/\ <<
FPTR:
Val.inject j fptr tfptr>>.
Proof.
ii.
inv H0;
des.
destruct ros;
ss;
clarify.
-
esplits;
eauto.
-
erewrite symbols_preserved.
des_ifs.
+
esplits;
eauto.
inv H0.
exploit SYMBOLS;
eauto.
+
esplits;
eauto.
Qed.
Preservation of the arguments to an external call.
Section EXTERNAL_ARGUMENTS.
Variable j:
meminj.
Variable cs:
list Linear.stackframe.
Variable cs':
list stackframe.
Variable sg:
signature.
Variables bound bound':
block.
Variables sm0:
SimMemInj.t'.
Hypothesis MS:
match_stacks j cs cs'
sg sm0.
Variable ls:
locset.
Variable rs:
regset.
Hypothesis AGR:
agree_regs j ls rs.
Hypothesis AGCS:
agree_callee_save ls (
parent_locset cs).
Hypothesis AGARGS:
agree_outgoing_arguments sg ls (
parent_locset cs).
Variable m':
mem.
Hypothesis SEP:
m' |=
stack_contents j cs cs'.
Lemma transl_external_argument:
forall l,
In l (
regs_of_rpairs (
loc_arguments sg)) ->
exists v,
extcall_arg rs m' (
parent_sp cs')
l v /\
Val.inject j (
ls l)
v.
Proof.
Lemma transl_external_argument_2:
forall p,
In p (
loc_arguments sg) ->
exists v,
extcall_arg_pair rs m' (
parent_sp cs')
p v /\
Val.inject j (
Locmap.getpair p ls)
v.
Proof.
Lemma transl_external_arguments_rec:
forall locs,
incl locs (
loc_arguments sg) ->
exists vl,
list_forall2 (
extcall_arg_pair rs m' (
parent_sp cs'))
locs vl
/\
Val.inject_list j (
map (
fun p =>
Locmap.getpair p ls)
locs)
vl.
Proof.
induction locs;
simpl;
intros.
exists (@
nil val);
split.
constructor.
constructor.
exploit transl_external_argument_2;
eauto with coqlib.
intros [
v [
A B]].
exploit IHlocs;
eauto with coqlib.
intros [
vl [
C D]].
exists (
v ::
vl);
split;
constructor;
auto.
Qed.
Lemma transl_external_arguments:
exists vl,
extcall_arguments rs m' (
parent_sp cs')
sg vl
/\
Val.inject_list j (
map (
fun p =>
Locmap.getpair p ls) (
loc_arguments sg))
vl.
Proof.
End EXTERNAL_ARGUMENTS.
Preservation of the arguments to a builtin.
Section BUILTIN_ARGUMENTS.
Variable f:
Linear.function.
Let b :=
function_bounds f.
Let fe :=
make_env b.
Variable tf:
Mach.function.
Hypothesis TRANSF_F:
transf_function f =
OK tf.
Variable j:
meminj.
Variables m m':
mem.
Variables ls ls0:
locset.
Variable rs:
regset.
Variables sp sp':
block.
Variables parent retaddr:
val.
Hypothesis INJ:
j sp =
Some(
sp',
fe.(
fe_stack_data)).
Hypothesis AGR:
agree_regs j ls rs.
Hypothesis SEP:
m' |=
frame_contents f j sp'
ls ls0 parent retaddr **
minjection j m **
globalenv_inject ge j.
Lemma transl_builtin_arg_correct:
forall a v,
eval_builtin_arg ge ls (
Vptr sp Ptrofs.zero)
m a v ->
(
forall l,
In l (
params_of_builtin_arg a) ->
loc_valid f l =
true) ->
(
forall sl ofs ty,
In (
S sl ofs ty) (
params_of_builtin_arg a) ->
slot_within_bounds b sl ofs ty) ->
exists v',
eval_builtin_arg ge rs (
Vptr sp'
Ptrofs.zero)
m' (
transl_builtin_arg fe a)
v'
/\
Val.inject j v v'.
Proof.
Lemma transl_builtin_args_correct:
forall al vl,
eval_builtin_args ge ls (
Vptr sp Ptrofs.zero)
m al vl ->
(
forall l,
In l (
params_of_builtin_args al) ->
loc_valid f l =
true) ->
(
forall sl ofs ty,
In (
S sl ofs ty) (
params_of_builtin_args al) ->
slot_within_bounds b sl ofs ty) ->
exists vl',
eval_builtin_args ge rs (
Vptr sp'
Ptrofs.zero)
m' (
List.map (
transl_builtin_arg fe)
al)
vl'
/\
Val.inject_list j vl vl'.
Proof.
induction 1;
simpl;
intros VALID BOUNDS.
-
exists (@
nil val);
split;
constructor.
-
exploit transl_builtin_arg_correct;
eauto using in_or_app.
intros (
v1' &
A &
B).
exploit IHlist_forall2;
eauto using in_or_app.
intros (
vl' &
C &
D).
exists (
v1'::
vl');
split;
constructor;
auto.
Qed.
End BUILTIN_ARGUMENTS.
The proof of semantic preservation relies on simulation diagrams
of the following form:
st1 --------------- st2
| |
t| +|t
| |
v v
st1'--------------- st2'
Matching between source and target states is defined by
match_states
below. It implies:
-
Satisfaction of the separation logic assertions that describe the contents
of memory. This is a separating conjunction of facts about:
-
the current stack frame
-
the frames in the call stack
-
the injection from the Linear memory state into the Mach memory state
-
the preservation of the global environment.
Agreement between, on the Linear side, the location sets ls
and parent_locset s of the current function and its caller,
and on the Mach side the register set rs.
-
The Linear code c is a suffix of the code of the
function f being executed.
-
Well-typedness of f.
Inductive match_states:
Linear.state ->
Mach.state ->
SimMemInj.t' ->
Prop :=
|
match_states_dummy:
forall f ls m fb tsp tc rs m'
j sm0 (
MCOMPAT:
SimMemInj.mcompat sm0 m m'
j) (
MWF:
SimMemInj.wf'
sm0),
match_states (
Linear.State []
f Vundef []
ls m) (
Mach.State []
fb tsp tc rs m')
sm0
|
match_states_intro:
forall cs f sp c ls m cs'
fb sp'
rs m'
j tf
sm0 (
MCOMPAT:
SimMemInj.mcompat sm0 m m'
j)
(
SPVALID:
sm0.(
SimMemInj.tgt).(
Mem.valid_block)
sp' /\
Ple sm0.(
SimMemInj.tgt_parent_nb)
sp' /\
forall i, ~
sm0.(
SimMemInj.tgt_external)
sp'
i)
(
MWF:
SimMemInj.wf'
sm0)
(
PRIV:
forall i, 0 <=
i <
fe_stack_data (
make_env (
function_bounds f)) \/
fe_stack_data (
make_env (
function_bounds f)) +
Linear.fn_stacksize f <=
i <
fe_size (
make_env (
function_bounds f))
->
sm0.(
SimMemInj.tgt_private)
sp'
i)
(
STACKS:
match_stacks j cs cs'
f.(
Linear.fn_sig)
sm0)
(
TRANSL:
transf_function f =
OK tf)
(
FIND:
Genv.find_funct_ptr tge fb =
Some (
Internal tf))
(
AGREGS:
agree_regs j ls rs)
(
AGLOCS:
agree_locs f ls (
parent_locset cs))
(
INJSP:
j sp =
Some(
sp',
fe_stack_data (
make_env (
function_bounds f))))
(
TAIL:
is_tail c (
Linear.fn_code f))
(
SEP:
m' |=
frame_contents f j sp'
ls (
parent_locset cs) (
parent_sp cs') (
parent_ra cs')
**
stack_contents j cs cs'
**
minjection j m
**
globalenv_inject ge j),
match_states (
Linear.State cs f (
Vptr sp Ptrofs.zero)
c ls m)
(
Mach.State cs'
fb (
Vptr sp'
Ptrofs.zero) (
transl_code (
make_env (
function_bounds f))
c)
rs m')
sm0
|
match_states_call:
forall cs fptr sg ls m cs'
tfptr rs m'
j
sm0 (
MCOMPAT:
SimMemInj.mcompat sm0 m m'
j)
(
MWF:
SimMemInj.wf'
sm0)
(
STACKS:
match_stacks j cs cs'
sg sm0)
(
AGREGS:
agree_regs j ls rs)
(
AGCSREGS:
agree_callee_save_regs ls (
parent_locset cs))
(
FPTR:
Val.inject j fptr tfptr)
(
SEP:
m' |=
stack_contents j cs cs'
**
minjection j m
**
globalenv_inject ge j),
match_states (
Linear.Callstate cs fptr sg ls m)
(
Mach.Callstate cs'
tfptr rs m')
sm0
|
match_states_return:
forall cs ls m cs'
rs m'
j sg
sm0 (
MCOMPAT:
SimMemInj.mcompat sm0 m m'
j)
(
MWF:
SimMemInj.wf'
sm0)
(
STACKS:
match_stacks j cs cs'
sg sm0)
(
AGREGS:
agree_regs j ls rs)
(
AGCSREGS:
agree_callee_save_regs ls (
parent_locset cs))
(
SEP:
m' |=
stack_contents j cs cs'
**
minjection j m
**
globalenv_inject ge j),
match_states (
Linear.Returnstate cs ls m)
(
Mach.Returnstate cs'
rs m')
sm0.
Local Opaque fe_stack_data fe_size.
Let step :=
Mach.step return_address_offset.
Theorem transf_step_correct:
forall s1 t s2,
Linear.step se ge s1 t s2 ->
forall (
WTS:
wt_state s1)
s1'
sm0 (
MS:
match_states s1 s1'
sm0),
exists s2',
plus step tse tge s1'
t s2' /\ (
exists sm1,
match_states s2 s2'
sm1 /\ <<
MLE:
SimMemInj.le'
sm0 sm1>>).
Proof.
induction 1;
intros;
try inv MS;
try rewrite transl_code_eq;
try (
generalize (
function_is_within_bounds f _ (
is_tail_in TAIL));
intro BOUND;
simpl in BOUND);
unfold transl_instr.
-
destruct BOUND as [
BOUND1 BOUND2].
exploit wt_state_getstack;
eauto.
intros SV.
unfold destroyed_by_getstack;
destruct sl.
+
exploit frame_get_local;
eauto.
intros (
v &
A &
B).
econstructor;
split.
apply plus_one.
apply exec_Mgetstack.
exact A.
SimMemInj.spl.
econstructor;
eauto with coqlib.
apply agree_regs_set_reg;
auto.
apply agree_locs_set_reg;
auto.
+
unfold slot_valid in SV.
InvBooleans.
exploit incoming_slot_in_parameters;
eauto.
intros IN_ARGS.
inversion STACKS;
clear STACKS.
elim (
H1 _ IN_ARGS).
{
rewrite MAINARGS in *.
subst s cs'.
exploit (
slot_outgoing_argument_valid f);
eauto.
intro VALID.
Local Opaque Z.mul Z.add Z.div make_env.
unfold slot_valid in *.
simpl_bool.
des;
cycle 1.
{
hnf in LE.
exploit LE;
eauto.
ss. }
clarify.
des_sumbool.
ss.
des_ifs;
cycle 1.
{
exploit get_location;
eauto.
apply sep_pick2 in SEP.
eauto.
eapply ARGS;
eauto.
intros (
v &
A &
B).
rewrite <-
Ptrofs.Ptrofs_add_repr,
Ptrofs.repr_unsigned, <-
load_stack_transf_ofs in *.
esplits;
eauto.
-
apply plus_one.
eapply exec_Mgetparam;
eauto.
+
rewrite (
unfold_transf_function _ _ TRANSL).
unfold fn_link_ofs.
eapply frame_get_parent.
eexact SEP.
-
econstructor;
eauto with coqlib.
econstructor;
eauto.
apply agree_regs_set_reg.
apply agree_regs_set_reg.
auto.
auto.
erewrite agree_incoming by eauto.
exact B.
apply agree_locs_set_reg;
auto.
ss.
eapply agree_locs_set_reg;
eauto.
ss.
rewrite MAINARGS.
eauto.
-
reflexivity.
}
}
subst s cs'.
assert(
exists P,
m' |=
frame_contents f0 j sp'0
ls (
parent_locset cs) (
parent_sp cs'0) (
parent_ra cs'0) **
P).
{
destruct main_args eqn:
MAINARGS;
eexists.
apply sep_proj2 in SEP.
simpl in SEP.
des_ifs;
try (
by (
inv STK;
clarify;
inv MAINARGS0)).
rewrite sep_assoc in SEP.
eexact SEP.
apply sep_proj2 in SEP.
simpl in SEP.
rewrite sep_assoc in SEP.
eexact SEP.
}
des.
exploit frame_get_outgoing.
eauto.
eapply ARGS;
eauto.
eapply slot_outgoing_argument_valid;
eauto.
intros (
v &
A &
B).
econstructor;
split.
apply plus_one.
eapply exec_Mgetparam;
eauto.
rewrite (
unfold_transf_function _ _ TRANSL).
unfold fn_link_ofs.
eapply frame_get_parent.
eexact SEP.
SimMemInj.spl.
econstructor;
eauto with coqlib.
econstructor;
eauto.
apply agree_regs_set_reg.
apply agree_regs_set_reg.
auto.
auto.
erewrite agree_incoming by eauto.
exact B.
apply agree_locs_set_reg;
auto.
apply agree_locs_undef_locs;
auto.
+
exploit frame_get_outgoing;
eauto.
intros (
v &
A &
B).
econstructor;
split.
apply plus_one.
apply exec_Mgetstack.
exact A.
SimMemInj.spl.
econstructor;
eauto with coqlib.
apply agree_regs_set_reg;
auto.
apply agree_locs_set_reg;
auto.
-
exploit wt_state_setstack;
eauto.
intros (
SV &
SW).
set (
ofs' :=
match sl with
|
Local =>
offset_local (
make_env (
function_bounds f))
ofs
|
Incoming => 0
|
Outgoing =>
offset_arg ofs
end).
eapply frame_undef_regs with (
rl :=
destroyed_by_setstack ty)
in SEP.
assert (
A:
exists m'',
store_stack m' (
Vptr sp'
Ptrofs.zero)
ty (
Ptrofs.repr ofs') (
rs0 src) =
Some m''
/\
m'' |=
frame_contents f j sp' (
Locmap.set (
S sl ofs ty) (
rs (
R src))
(
LTL.undef_regs (
destroyed_by_setstack ty)
rs))
(
parent_locset s) (
parent_sp cs') (
parent_ra cs')
**
stack_contents j s cs' **
minjection j m **
globalenv_inject ge j).
{
unfold ofs';
destruct sl;
try discriminate.
eapply frame_set_local;
eauto.
eapply frame_set_outgoing;
eauto. }
clear SEP;
destruct A as (
m'' &
STORE &
SEP).
econstructor;
split.
apply plus_one.
destruct sl;
try discriminate.
econstructor.
eexact STORE.
eauto.
econstructor.
eexact STORE.
eauto.
assert(
LE:
SimMemInj.le'
sm0
(
SimMemInj.mk m m''
j sm0.(
SimMemInj.src_external)
sm0.(
SimMemInj.tgt_external)
sm0.(
SimMemInj.src_parent_nb)
sm0.(
SimMemInj.tgt_parent_nb)
sm0.(
SimMemInj.src_ge_nb)
sm0.(
SimMemInj.tgt_ge_nb))).
{
inv MCOMPAT.
inv MWF.
econs;
eauto.
-
eapply Mem.unchanged_on_refl.
-
unfold store_stack,
Mem.storev in *.
simpl in STORE.
simpl.
eapply Mem.store_unchanged_on;
eauto.
des.
eauto.
-
eapply SimMemInj.frozen_refl.
-
eapply SimMemInj.frozen_refl.
-
ii.
ss.
unfold store_stack,
Mem.storev in *.
ss.
eapply Mem.perm_store_2;
eauto.
}
SimMemInj.spl_approx sm0.
econstructor.
{
SimMemInj.compat_tac. }
{
eapply spvalid_le;
eauto. }
{
inv MCOMPAT.
inv MWF.
econs;
ss;
eauto.
-
eapply SEP.
-
etransitivity;
eauto.
unfold SimMemInj.tgt_private.
ii.
ss.
des.
split;
eauto.
unfold SimMemInj.valid_blocks,
Mem.valid_block,
store_stack,
Mem.storev in *.
ss.
erewrite Mem.nextblock_store;
eauto.
-
unfold store_stack,
Mem.storev in *.
ss.
erewrite Mem.nextblock_store;
eauto.
}
{
inv MCOMPAT.
ii.
unfold SimMemInj.tgt_private,
loc_out_of_reach in *.
ss.
exploit PRIV;
eauto.
intros [
X Y].
split;
eauto.
unfold store_stack,
Mem.storev in *.
inv STORE.
eapply Mem.store_valid_block_1;
eauto.
}
{
inv MCOMPAT.
eapply match_stacks_le;
eauto. }
eauto.
eauto.
apply agree_regs_set_slot.
apply agree_regs_undef_regs.
auto.
apply agree_locs_set_slot.
apply agree_locs_undef_locs.
auto.
apply destroyed_by_setstack_caller_save.
auto.
eauto.
eauto with coqlib.
eauto.
-
assert (
exists v',
eval_operation ge (
Vptr sp'
Ptrofs.zero) (
transl_op (
make_env (
function_bounds f))
op)
rs0##
args m' =
Some v'
/\
Val.inject j v v').
eapply eval_operation_inject;
eauto.
eapply globalenv_inject_preserves_globals.
eapply sep_proj2.
eapply sep_proj2.
eapply sep_proj2.
eexact SEP.
eapply agree_reglist;
eauto.
apply sep_proj2 in SEP.
apply sep_proj2 in SEP.
apply sep_proj1 in SEP.
exact SEP.
destruct H0 as [
v' [
A B]].
econstructor;
split.
apply plus_one.
econstructor.
instantiate (1 :=
v').
rewrite <-
A.
apply eval_operation_preserved.
exact symbols_preserved.
eauto.
SimMemInj.spl.
econstructor;
eauto with coqlib.
apply agree_regs_set_reg;
auto.
rewrite transl_destroyed_by_op.
apply agree_regs_undef_regs;
auto.
apply agree_locs_set_reg;
auto.
apply agree_locs_undef_locs.
auto.
apply destroyed_by_op_caller_save.
apply frame_set_reg.
apply frame_undef_regs.
exact SEP.
-
assert (
exists a',
eval_addressing ge (
Vptr sp'
Ptrofs.zero) (
transl_addr (
make_env (
function_bounds f))
addr)
rs0##
args =
Some a'
/\
Val.inject j a a').
eapply eval_addressing_inject;
eauto.
eapply globalenv_inject_preserves_globals.
eapply sep_proj2.
eapply sep_proj2.
eapply sep_proj2.
eexact SEP.
eapply agree_reglist;
eauto.
destruct H1 as [
a' [
A B]].
exploit loadv_parallel_rule.
apply sep_proj2 in SEP.
apply sep_proj2 in SEP.
apply sep_proj1 in SEP.
eexact SEP.
eauto.
eauto.
intros [
v' [
C D]].
econstructor;
split.
apply plus_one.
econstructor.
instantiate (1 :=
a').
rewrite <-
A.
apply eval_addressing_preserved.
exact symbols_preserved.
eexact C.
eauto.
SimMemInj.spl.
econstructor;
eauto with coqlib.
apply agree_regs_set_reg.
rewrite transl_destroyed_by_load.
apply agree_regs_undef_regs;
auto.
auto.
apply agree_locs_set_reg.
apply agree_locs_undef_locs.
auto.
apply destroyed_by_load_caller_save.
auto.
-
assert (
exists a',
eval_addressing ge (
Vptr sp'
Ptrofs.zero) (
transl_addr (
make_env (
function_bounds f))
addr)
rs0##
args =
Some a'
/\
Val.inject j a a').
eapply eval_addressing_inject;
eauto.
eapply globalenv_inject_preserves_globals.
eapply sep_proj2.
eapply sep_proj2.
eapply sep_proj2.
eexact SEP.
eapply agree_reglist;
eauto.
destruct H1 as [
a' [
A B]].
rewrite sep_swap3 in SEP.
exploit storev_parallel_rule.
eexact SEP.
eauto.
eauto.
apply AGREGS.
assert(
INJ:
m'0 |=
minjection j m).
eapply SEP.
clear SEP;
intros (
m1' &
C &
SEP).
rewrite sep_swap3 in SEP.
econstructor;
split.
apply plus_one.
econstructor.
instantiate (1 :=
a').
rewrite <-
A.
apply eval_addressing_preserved.
exact symbols_preserved.
eexact C.
eauto.
inv MCOMPAT.
exploit SimMemInj.storev_mapped;
eauto.
i;
des.
SimMemInj.spl_exact sm1.
econstructor.
SimMemInj.compat_tac.
{
eapply spvalid_le;
eauto. }
eauto.
{
ii.
unfold SimMemInj.tgt_private,
loc_out_of_reach,
Mem.storev in *.
des_ifs_safe.
exploit PRIV;
eauto.
intros [
X Y].
split.
-
ii.
eapply X.
rewrite <-
MINJ.
eauto.
eapply Mem.perm_store_2;
eauto.
-
eapply Mem.store_valid_block_1;
eauto.
}
{
eapply match_stacks_le;
eauto;
try congruence.
ii.
unfold Mem.storev in H0.
des_ifs_safe.
eapply Mem.perm_store_2;
eauto.
}
eauto.
eauto.
rewrite transl_destroyed_by_store.
apply agree_regs_undef_regs;
auto.
apply agree_locs_undef_locs.
auto.
apply destroyed_by_store_caller_save.
auto.
eauto with coqlib.
eapply frame_undef_regs;
eauto.
-
exploit find_function_ptr_translated;
eauto.
eapply sep_proj2.
eapply sep_proj2.
eapply sep_proj2.
eexact SEP.
i;
des.
exploit is_tail_transf_function;
eauto.
intros IST.
rewrite transl_code_eq in IST.
simpl in IST.
exploit return_address_offset_exists. {
rewrite Genv.find_funct_find_funct_ptr.
eauto. }
eexact IST.
intros [
ra D].
econstructor;
split.
apply plus_one.
econstructor;
eauto.
econs;
eauto.
SimMemInj.spl.
econstructor;
eauto.
econstructor;
eauto with coqlib.
apply Val.Vptr_has_type.
intros;
red.
apply Z.le_trans with (
size_arguments sig);
auto.
apply loc_arguments_bounded;
auto.
intro;
auto.
{
inv FPTR.
eauto. }
des_ifs.
{
ss.
des_ifs;
try (
by (
inv STACKS;
clarify;
inv MAINARGS)).
rewrite sep_assoc.
exact SEP. }
simpl.
rewrite sep_assoc.
exact SEP.
-
rewrite (
sep_swap (
stack_contents j s cs'))
in SEP.
exploit function_epilogue_correct;
eauto.
assert(
INJ:
m'0 |=
minjection j m).
apply SEP.
clear SEP.
intros (
rs1 &
m1' &
P &
Q &
R &
S &
T &
U &
SEP).
rewrite sep_swap in SEP.
exploit find_function_ptr_translated;
eauto.
eapply sep_proj2.
eapply sep_proj2.
eexact SEP.
i;
des.
econstructor;
split.
eapply plus_right.
eexact S.
econstructor;
eauto.
econs;
eauto.
traceEq.
inv MCOMPAT.
exploit SimMemInj.free_left;
eauto.
i;
des.
exploit SimMemInj.free_right;
eauto.
{
rewrite MTGT.
eauto. }
{
ii.
red.
esplits.
-
rewrite MINJ.
subst m'.
ii.
exploit unfold_transf_function;
eauto.
ii.
subst tf.
simpl in BDD.
destruct(
Classical_Prop.classic(0 <=
ofs <
fe_stack_data (
make_env (
function_bounds f)) \/
fe_stack_data (
make_env (
function_bounds f)) +
Linear.fn_stacksize f <=
ofs <
fe_size (
make_env (
function_bounds f)))).
+
eapply PRIV;
eauto.
eapply Mem.perm_free_3;
eauto.
+
assert(
fe_stack_data (
make_env (
function_bounds f)) <=
ofs <
fe_stack_data (
make_env (
function_bounds f)) +
Linear.fn_stacksize f).
{
destruct (
zlt ofs (
fe_stack_data (
make_env (
function_bounds f)))).
xomega.
destruct (
zle (
fe_stack_data (
make_env (
function_bounds f)) +
Linear.fn_stacksize f)
ofs);
xomega. }
clear H4.
destruct (
eq_block b0 stk).
*
subst b0.
rewrite INJSP in H.
clarify.
eapply Mem.perm_free_2;
try eapply H2;
eauto.
xomega.
*
exploit Mem.mi_no_overlap;
try eapply INJ;
eauto.
eapply Mem.perm_free_3;
eauto.
exploit Mem.free_range_perm.
eapply H2.
instantiate (1 :=
ofs -
fe_stack_data (
make_env (
function_bounds f))).
xomega.
eauto with mem.
intros [
X |
X].
congruence.
xomega.
-
rewrite MTGT.
red.
exploit Mem.free_range_perm;
eauto.
}
{
ii.
eapply SPVALID1.
inv MLE.
rewrite TGTPARENTEQ.
eauto. }
i;
des.
SimMemInj.spl_exact sm2.
econstructor;
eauto.
{
SimMemInj.compat_tac. }
apply match_stacks_change_sig with (
Linear.fn_sig f);
auto.
{
eapply match_stacks_le;
eauto;
try congruence.
eapply match_stacks_le;
eauto;
try congruence.
ii.
eapply Mem.perm_free_3;
eauto.
congruence.
}
apply zero_size_arguments_tailcall_possible.
eapply wt_state_tailcall;
eauto.
intro;
auto.
{
inv FPTR.
eauto. }
-
assert(
GENVINJ:
m'0 |=
globalenv_inject ge j).
{
eapply sep_proj2.
eapply sep_proj2.
eapply sep_proj2.
eexact SEP. }
assert (
PRES_GLB:
meminj_preserves_globals ge j).
{
eapply globalenv_inject_preserves_globals.
eauto. }
assert(
INJECT:
Mem.inject j m m'0). {
eapply SEP. }
destruct BOUND as [
BND1 BND2].
exploit transl_builtin_args_correct.
eauto.
eauto.
rewrite sep_swap in SEP;
apply sep_proj2 in SEP;
eexact SEP.
eauto.
rewrite <-
forallb_forall.
eapply wt_state_builtin;
eauto.
exact BND2.
intros [
vargs' [
P Q]].
rewrite <-
sep_assoc,
sep_comm,
sep_assoc in SEP.
exploit external_call_parallel_rule;
eauto.
{
eapply match_stacks_symbols_inject;
eauto. }
clear SEP;
intros (
j' &
res' &
m1' &
EC &
RES &
SEP &
INCR &
ISEP &
UNCH1 &
UNCH2).
rewrite <-
sep_assoc,
sep_comm,
sep_assoc in SEP.
econstructor;
split.
apply plus_one.
econstructor;
eauto.
eapply eval_builtin_args_preserved with (
ge1 :=
ge);
eauto.
exact symbols_preserved.
exploit SimMemInj.external_call;
try by (
inv MCOMPAT;
eauto).
{
eapply SEP. }
i;
des.
SimMemInj.spl_exact sm1.
eapply match_states_intro with (
j :=
j');
eauto with coqlib.
SimMemInj.compat_tac.
{
eapply spvalid_le;
eauto. }
{
inv MCOMPAT.
ii.
unfold SimMemInj.tgt_private,
loc_out_of_reach in *.
ss.
exploit PRIV;
eauto.
intros [
X Y].
split.
-
ii.
destruct (
sm0.(
SimMemInj.inj)
b0)
as [[
sp1 delta1] |]
eqn:?.
+
exploit INCR;
eauto.
ii.
clarify.
eapply PRIV;
eauto.
eapply external_call_max_perm;
eauto.
destruct (
plt b0 (
Mem.nextblock sm0.(
SimMemInj.src)));
auto.
exploit Mem.mi_freeblocks;
try eapply n.
eauto.
congruence.
+
eapply ISEP;
eauto.
-
eapply external_call_valid_block;
eauto.
}
inv MCOMPAT.
assert(
SAME:
forall (
b0 b2 :
block) (
delta :
Z),
Mem.valid_block (
SimMemInj.tgt sm0)
b2 -> (
SimMemInj.inj sm1)
b0 =
Some (
b2,
delta) ->
SimMemInj.inj sm0 b0 =
Some (
b2,
delta)).
{
ii.
ss.
eapply SimMemInj.frozen_preserves_tgt;
try (
erewrite <-
SimMemInj.inject_separated_frozen;
eauto);
eauto. }
eapply match_stacks_change_meminj;
eauto.
{
i.
apply SAME;
eauto.
ss.
des.
inv GENVINJ0.
inv SECOMPATSRC.
rewrite NB in *.
exploit DOMAIN;
eauto.
i;
clarify.
exploit INCR;
eauto.
i;
clarify.
unfold Mem.valid_block.
xomega. }
{
i.
apply SAME;
eauto.
ss.
des.
inv GENVINJ0.
inv SECOMPATTGT.
rewrite NB in *.
inv MATCH_GENV.
rewrite mge_next in *.
exploit DOMAIN;
eauto.
i;
clarify.
exploit INCR;
eauto.
i;
clarify.
unfold Mem.valid_block.
xomega. }
{
eapply match_stacks_le;
eauto;
try congruence.
-
ii.
ss.
eapply external_call_max_perm;
eauto.
eapply Mem.valid_block_inject_1;
try eapply SAME;
eauto.
}
apply agree_regs_set_res;
auto.
apply agree_regs_undef_regs;
auto.
eapply agree_regs_inject_incr;
eauto.
apply agree_locs_set_res;
auto.
apply agree_locs_undef_regs;
auto.
apply frame_set_res.
apply frame_undef_regs.
apply frame_contents_incr with j;
auto.
rewrite sep_swap2.
apply stack_contents_change_meminj with j;
auto.
rewrite sep_swap2.
exact SEP.
-
econstructor;
split.
apply plus_one;
apply exec_Mlabel.
SimMemInj.spl.
econstructor;
eauto with coqlib.
-
econstructor;
split.
apply plus_one;
eapply exec_Mgoto;
eauto.
apply transl_find_label;
eauto.
SimMemInj.spl.
econstructor;
eauto.
eapply find_label_tail;
eauto.
-
econstructor;
split.
apply plus_one.
eapply exec_Mcond_true;
eauto.
eapply eval_condition_inject with (
m1 :=
m).
eapply agree_reglist;
eauto.
apply sep_pick3 in SEP;
exact SEP.
auto.
eapply transl_find_label;
eauto.
SimMemInj.spl.
inv MCOMPAT.
econstructor.
SimMemInj.compat_tac.
auto.
auto.
auto.
eauto.
eauto.
eauto.
apply agree_regs_undef_regs;
auto.
apply agree_locs_undef_locs.
auto.
apply destroyed_by_cond_caller_save.
auto.
eapply find_label_tail;
eauto.
apply frame_undef_regs;
auto.
-
econstructor;
split.
apply plus_one.
eapply exec_Mcond_false;
eauto.
eapply eval_condition_inject with (
m1 :=
m).
eapply agree_reglist;
eauto.
apply sep_pick3 in SEP;
exact SEP.
auto.
SimMemInj.spl.
inv MCOMPAT.
econstructor.
SimMemInj.compat_tac.
auto.
auto.
auto.
eauto.
eauto.
eauto.
apply agree_regs_undef_regs;
auto.
apply agree_locs_undef_locs.
auto.
apply destroyed_by_cond_caller_save.
auto.
eauto with coqlib.
apply frame_undef_regs;
auto.
-
assert (
rs0 arg =
Vint n).
{
generalize (
AGREGS arg).
rewrite H.
intro IJ;
inv IJ;
auto. }
econstructor;
split.
apply plus_one;
eapply exec_Mjumptable;
eauto.
apply transl_find_label;
eauto.
SimMemInj.spl.
inv MCOMPAT.
econstructor.
SimMemInj.compat_tac.
auto.
auto.
eauto.
eauto.
eauto.
eauto.
eauto.
apply agree_regs_undef_regs;
auto.
apply agree_locs_undef_locs.
auto.
apply destroyed_by_jumptable_caller_save.
auto.
eapply find_label_tail;
eauto.
apply frame_undef_regs;
auto.
-
rewrite (
sep_swap (
stack_contents j s cs'))
in SEP.
exploit function_epilogue_correct;
eauto.
intros (
rs' &
m1' &
A &
B &
C &
D &
E &
F &
G).
econstructor;
split.
eapply plus_right.
eexact D.
econstructor;
eauto.
traceEq.
inv MCOMPAT.
exploit SimMemInj.free_left;
eauto.
i;
des.
exploit SimMemInj.free_right;
eauto.
{
rewrite MTGT.
eauto. }
{
ii.
red.
esplits.
-
rewrite MINJ.
subst m'.
ii.
exploit unfold_transf_function;
eauto.
ii.
subst tf.
simpl in BDD.
destruct(
Classical_Prop.classic(0 <=
ofs <
fe_stack_data (
make_env (
function_bounds f)) \/
fe_stack_data (
make_env (
function_bounds f)) +
Linear.fn_stacksize f <=
ofs <
fe_size (
make_env (
function_bounds f)))).
+
eapply PRIV;
eauto.
eapply Mem.perm_free_3;
eauto.
+
assert(
fe_stack_data (
make_env (
function_bounds f)) <=
ofs <
fe_stack_data (
make_env (
function_bounds f)) +
Linear.fn_stacksize f).
{
destruct (
zlt ofs (
fe_stack_data (
make_env (
function_bounds f)))).
xomega.
destruct (
zle (
fe_stack_data (
make_env (
function_bounds f)) +
Linear.fn_stacksize f)
ofs);
xomega. }
clear H2.
destruct (
eq_block b0 stk).
*
subst b0.
rewrite INJSP in H0.
clarify.
eapply Mem.perm_free_2;
try eapply H;
eauto.
xomega.
*
exploit Mem.mi_no_overlap;
try eapply SEP;
eauto.
eapply Mem.perm_free_3;
eauto.
exploit Mem.free_range_perm.
eapply H.
instantiate (1 :=
ofs -
fe_stack_data (
make_env (
function_bounds f))).
xomega.
eauto with mem.
intros [
X |
X].
congruence.
xomega.
-
rewrite MTGT.
red.
exploit Mem.free_range_perm;
eauto.
}
{
ii.
eapply SPVALID1.
inv MLE.
rewrite TGTPARENTEQ.
eauto. }
i;
des.
SimMemInj.spl_exact sm2.
econstructor;
eauto.
{
SimMemInj.compat_tac. }
{
eapply match_stacks_le;
eauto;
try congruence.
eapply match_stacks_le;
eauto;
try congruence.
ii.
eapply Mem.perm_free_3;
eauto.
congruence.
}
intro;
auto.
rewrite sep_swap;
exact G.
-
assert(
GENVINJ:
m'0 |=
globalenv_inject ge j).
{
eapply sep_proj2.
eapply sep_proj2.
eexact SEP. }
exploit functions_translated;
eauto.
intros (
tf &
FIND &
TRANSL).
assert(
fptr =
tfptr /\
exists fb,
fptr =
Vptr fb Ptrofs.zero).
{
repeat apply sep_proj2 in SEP.
inv SEP.
des.
inv H1.
unfold Genv.find_funct in *.
des_ifs.
inv FPTR0.
exploit FUNCTIONS;
eauto.
i.
exploit DOMAIN;
eauto.
i;
des.
clarify.
esplits;
eauto. }
des.
clarify.
revert TRANSL.
unfold transf_fundef,
transf_partial_fundef.
destruct (
transf_function f)
as [
tfn|]
eqn:
TRANSL;
simpl;
try congruence.
intros EQ;
inversion EQ;
clear EQ;
subst tf.
rewrite sep_comm,
sep_assoc in SEP.
exploit wt_callstate_agree;
eauto.
intros [
AGCS AGARGS].
exploit function_prologue_correct;
eauto.
red;
intros;
eapply wt_callstate_wt_regs;
eauto.
eapply match_stacks_type_sp;
eauto.
eapply match_stacks_type_retaddr;
eauto.
{
ii.
inv MWF.
inv MCOMPAT.
eapply TGTEXT in H0.
red in H0.
des.
eauto. }
assert (
INJ:
Mem.inject'
j m m'0).
apply SEP.
clear SEP;
intros (
j' &
rs' &
m2' &
sp' &
m3' &
m4' &
m5' &
A &
B &
C &
D &
E &
F &
SEP &
J &
INJ_SEP &
UNCH &
MAX &
K).
rewrite (
sep_comm (
globalenv_inject ge j'))
in SEP.
rewrite (
sep_swap (
minjection j'
m'))
in SEP.
econstructor;
split.
eapply plus_left.
econstructor;
eauto.
rewrite (
unfold_transf_function _ _ TRANSL).
unfold fn_code.
unfold transl_body.
eexact D.
traceEq.
assert(
NEXTBLOCK:
Ple (
Mem.nextblock m'0) (
Mem.nextblock m5')).
{
unfold store_stack,
Mem.storev in *.
ss.
exploit Mem.nextblock_alloc;
eauto.
i.
exploit Mem.nextblock_store.
eapply B.
i.
exploit Mem.nextblock_store.
eauto.
i.
eapply Ple_trans;
try eapply UNCH.
rewrite H2.
rewrite H1.
rewrite H0.
xomega.
}
assert(
LE:
SimMemInj.le'
sm0
(
SimMemInj.mk m'
m5'
j'
sm0.(
SimMemInj.src_external)
sm0.(
SimMemInj.tgt_external)
sm0.(
SimMemInj.src_parent_nb)
sm0.(
SimMemInj.tgt_parent_nb)
sm0.(
SimMemInj.src_ge_nb)
sm0.(
SimMemInj.tgt_ge_nb))).
{
inv MCOMPAT.
inv MWF.
econs;
ss;
eauto.
-
eapply Mem.alloc_unchanged_on;
eauto.
-
unfold store_stack,
Mem.storev in *.
ss.
eapply Mem.unchanged_on_trans.
eapply Mem.alloc_unchanged_on;
eauto.
eapply Mem.unchanged_on_trans with m3'; [|
eapply Mem.unchanged_on_trans with m4'; [|
eauto]].
+
eapply Mem.store_unchanged_on;
eauto.
ii.
eapply Mem.fresh_block_alloc;
eauto.
eapply TGTEXT in H1.
red in H1.
des.
eauto.
+
eapply Mem.store_unchanged_on;
eauto.
ii.
eapply Mem.fresh_block_alloc;
eauto.
eapply TGTEXT in H1.
red in H1.
des.
eauto.
-
eapply SimMemInj.frozen_shortened;
eauto.
eapply SimMemInj.frozen_shortened;
eauto.
eapply SimMemInj.inject_separated_frozen.
eauto.
-
eapply SimMemInj.frozen_shortened;
eauto.
eapply SimMemInj.inject_separated_frozen.
eauto.
-
ii.
eapply Mem.perm_alloc_4;
eauto.
ii.
subst b.
eapply Mem.fresh_block_alloc.
eapply H.
eauto.
-
ii.
unfold store_stack,
Mem.storev in *.
ss.
eapply Mem.perm_alloc_4;
eauto;
cycle 1.
exploit Mem.alloc_result;
eauto.
ii.
subst.
red in VALID.
xomega.
eapply Mem.perm_store_2;
eauto.
eapply Mem.perm_store_2;
eauto.
eapply MAX;
eauto.
unfold Mem.valid_block in *.
erewrite Mem.nextblock_store;
try eapply C.
erewrite Mem.nextblock_store;
try eapply B.
erewrite Mem.nextblock_alloc;
try eapply A.
xomega.
}
SimMemInj.spl_approx sm0.
eapply match_states_intro with (
j :=
j');
eauto with coqlib.
SimMemInj.compat_tac.
{
des.
ss.
inv MCOMPAT.
esplits;
eauto.
-
exploit Mem.valid_new_block;
eauto.
i;
clarify.
eapply Mem.valid_block_unchanged_on;
eauto.
unfold store_stack in *.
ss.
eapply Mem.store_valid_block_1;
eauto.
eapply Mem.store_valid_block_1;
eauto.
-
erewrite Mem.alloc_result with (
b :=
sp');
eauto.
inv MWF.
xomega.
-
erewrite Mem.alloc_result with (
b :=
sp');
eauto.
inv MWF.
intros ?
T.
apply TGTEXT in T.
rr in T.
des.
r in T0.
unfold Mem.valid_block in *.
xomega.
}
{
inv MCOMPAT.
inv MWF.
econs;
ss;
eauto.
-
eapply SEP.
-
etransitivity;
eauto.
unfold SimMemInj.src_private.
ii.
des.
ss.
splits;
eauto.
{
eapply SimMemInj.loc_unmapped_frozen;
eauto.
eapply SimMemInj.inject_separated_frozen;
eauto. }
{
exploit Mem.nextblock_alloc.
eapply H.
i.
unfold SimMemInj.valid_blocks,
Mem.valid_block in *.
rewrite H0.
xomega. }
-
etransitivity;
eauto.
unfold SimMemInj.tgt_private.
ii.
ss.
des.
esplits;
eauto.
{
eapply SimMemInj.loc_out_of_reach_frozen;
eauto.
eapply SimMemInj.inject_separated_frozen;
eauto.
ii.
eapply Mem.perm_alloc_4;
eauto.
ii.
subst b0.
eapply K in MAPPED.
clarify.
eapply Mem.fresh_block_alloc;
eauto. }
{
unfold SimMemInj.valid_blocks,
Mem.valid_block in *.
eapply Mem.nextblock_alloc in A.
xomega. }
-
exploit Mem.nextblock_alloc.
eapply H.
i.
rewrite H0.
xomega.
-
exploit Mem.nextblock_alloc;
eauto.
i.
xomega.
}
{
ii.
unfold SimMemInj.tgt_private,
loc_out_of_reach in *.
simpl.
split.
-
ii.
exploit Mem.perm_alloc_inv.
eexact H.
eauto.
destruct (
eq_block b0 stk);
i.
+
subst.
rewrite J in H1.
assert(
delta =
fe_stack_data (
make_env (
function_bounds f))).
congruence.
subst delta.
exploit unfold_transf_function;
eauto.
ii.
subst tfn.
xomega.
+
eapply Mem.fresh_block_alloc.
eapply A.
eapply Mem.mi_mappedblocks;
eauto.
erewrite SimMemInj.frozen_preserves_src;
eauto.
eapply SimMemInj.inject_separated_frozen;
eauto.
eapply Mem.perm_valid_block;
eauto.
-
eapply Mem.valid_block_unchanged_on;
eauto.
unfold store_stack,
Mem.storev in *.
des_ifs_safe.
eapply Mem.store_valid_block_1;
eauto.
eapply Mem.store_valid_block_1;
eauto.
eapply Mem.valid_new_block;
eauto.
}
inv MCOMPAT.
assert(
SAME:
forall (
b0 b2 :
block) (
delta :
Z),
Mem.valid_block (
SimMemInj.tgt sm0)
b2 ->
j'
b0 =
Some (
b2,
delta) ->
SimMemInj.inj sm0 b0 =
Some (
b2,
delta)).
{
ii.
ss.
eapply SimMemInj.frozen_preserves_tgt;
try (
erewrite <-
SimMemInj.inject_separated_frozen;
eauto);
eauto. }
eapply match_stacks_change_meminj;
eauto.
{
i.
apply SAME;
eauto.
ss.
des.
inv GENVINJ0.
inv SECOMPATSRC.
rewrite NB in *.
exploit DOMAIN;
eauto.
i;
clarify.
exploit K;
eauto.
i;
clarify.
unfold Mem.valid_block.
xomega. }
{
i.
apply SAME;
eauto.
ss.
des.
inv GENVINJ0.
inv SECOMPATTGT.
rewrite NB in *.
inv MATCH_GENV.
rewrite mge_next in *.
exploit DOMAIN;
eauto.
i;
clarify.
exploit K;
eauto.
i;
clarify.
unfold Mem.valid_block.
xomega. }
{
eapply match_stacks_le;
eauto;
try congruence.
-
ii.
ss.
eapply Mem.perm_alloc_4;
eauto.
ii.
subst b.
rewrite J in H1.
clarify.
eapply Mem.fresh_block_alloc;
eauto.
}
rewrite sep_swap in SEP.
rewrite sep_swap.
eapply stack_contents_change_meminj;
eauto.
-
assert(
GENVINJ:
m'0 |=
globalenv_inject ge j).
{
eapply sep_proj2.
eapply sep_proj2.
eexact SEP. }
assert (
PRES_GLB:
meminj_preserves_globals ge j).
{
eapply globalenv_inject_preserves_globals.
eauto. }
assert(
INJECT:
Mem.inject j m m'0). {
eapply SEP. }
exploit functions_translated;
eauto.
intros (
tf &
FIND &
TRANSL).
assert(
fptr =
tfptr /\
exists fb,
fptr =
Vptr fb Ptrofs.zero).
{
repeat apply sep_proj2 in SEP.
inv SEP.
des.
inv H1.
unfold Genv.find_funct in *.
des_ifs.
inv FPTR0.
exploit FUNCTIONS;
eauto.
i.
exploit DOMAIN;
eauto.
i;
des.
clarify.
esplits;
eauto. }
des.
clarify.
simpl in TRANSL.
inversion TRANSL;
subst tf.
exploit wt_callstate_agree;
eauto.
intros [
AGCS AGARGS].
exploit transl_external_arguments;
eauto.
apply sep_proj1 in SEP;
eauto.
intros [
vl [
ARGS VINJ]].
rewrite sep_comm,
sep_assoc in SEP.
exploit external_call_parallel_rule;
eauto.
{
eapply match_stacks_symbols_inject;
eauto. }
intros (
j' &
res' &
m1' &
A &
B &
C &
D &
E &
F &
G).
econstructor;
split.
apply plus_one.
eapply exec_function_external;
eauto.
exploit SimMemInj.external_call;
try by (
inv MCOMPAT;
eauto).
{
eapply C. }
i;
des.
SimMemInj.spl_exact sm1.
eapply match_states_return with (
j :=
j').
SimMemInj.compat_tac.
{
eauto. }
inv MCOMPAT.
assert(
SAME:
forall (
b0 b2 :
block) (
delta :
Z),
Mem.valid_block (
SimMemInj.tgt sm0)
b2 -> (
SimMemInj.inj sm1)
b0 =
Some (
b2,
delta) ->
SimMemInj.inj sm0 b0 =
Some (
b2,
delta)).
{
ii.
ss.
eapply SimMemInj.frozen_preserves_tgt;
try (
erewrite <-
SimMemInj.inject_separated_frozen;
eauto);
eauto. }
eapply match_stacks_change_meminj;
eauto.
{
i.
apply SAME;
eauto.
ss.
des.
inv GENVINJ0.
inv SECOMPATSRC.
rewrite NB in *.
exploit DOMAIN;
eauto.
i;
clarify.
exploit D;
eauto.
i;
clarify.
unfold Mem.valid_block.
xomega. }
{
i.
apply SAME;
eauto.
ss.
des.
inv GENVINJ0.
inv SECOMPATTGT.
rewrite NB in *.
inv MATCH_GENV.
rewrite mge_next in *.
exploit DOMAIN;
eauto.
i;
clarify.
exploit D;
eauto.
i;
clarify.
unfold Mem.valid_block.
xomega. }
{
eapply match_stacks_le;
eauto;
try congruence.
ii.
ss.
eapply external_call_max_perm;
eauto.
eapply Mem.valid_block_inject_1;
try eapply SAME;
eauto.
}
apply agree_regs_set_pair.
apply agree_regs_undef_caller_save_regs.
apply agree_regs_inject_incr with j;
auto.
auto.
apply agree_callee_save_regs_set_result.
apply agree_callee_save_regs_after;
auto.
apply stack_contents_change_meminj with j;
auto.
rewrite sep_comm,
sep_assoc;
auto.
-
inv STACKS;
exploit wt_returnstate_agree;
eauto;
intros [
AGCS OUTU].
{
rewrite MAINARGS in *.
ss.
simpl in AGCS.
econstructor;
split.
apply plus_one.
apply exec_return.
SimMemInj.spl.
econs;
eauto. }
assert(
SEP0:
m' |=
frame_contents f j sp'
rs0 (
parent_locset s) (
parent_sp cs'0) (
parent_ra cs'0) **
stack_contents j s cs'0 **
minjection j m **
globalenv_inject ge j).
{
destruct main_args eqn:
MAINARGS.
simpl in AGCS.
simpl in SEP.
ss.
des_ifs;
try (
by (
inv STK;
clarify;
inv MAINARGS0)).
rewrite sep_assoc in SEP.
ss.
simpl in AGCS.
simpl in SEP.
rewrite sep_assoc in SEP.
ss. }
econstructor;
split.
apply plus_one.
apply exec_return.
SimMemInj.spl.
econstructor;
eauto.
apply agree_locs_return with rs0;
auto.
apply frame_contents_exten with rs0 (
parent_locset s);
auto.
intros;
apply Val.lessdef_same;
apply AGCS;
red;
congruence.
intros;
rewrite (
OUTU ty ofs);
auto.
Unshelve.
all:
by (
try eapply SimMemInj.inject_separated_frozen;
eauto).
Qed.
End CORELEMMA.
Section WHOLE.
Local Existing Instance main_args_none.
Let ge :=
Genv.globalenv prog.
Let tge :=
Genv.globalenv tprog.
Let match_states :=
match_states ge tge ge tge.
Hypothesis return_address_offset_exists:
forall f sg ros c v (
FUNCT:
Genv.find_funct tge v =
Some (
Internal f)),
is_tail (
Mcall sg ros ::
c) (
fn_code f) ->
exists ofs,
return_address_offset f c ofs.
Let MATCH_GENV:
Genv.match_genvs (
match_globdef (
fun _ f tf =>
transf_fundef f =
OK tf)
eq prog)
ge tge.
Proof.
Local Opaque sepconj.
Lemma transf_initial_states:
forall st1,
Linear.initial_state prog st1 ->
exists st2,
Mach.initial_state tprog st2 /\
exists sm,
match_states st1 st2 sm.
Proof.
Lemma transf_final_states:
forall st1 st2 r,
(
exists sm,
match_states st1 st2 sm)->
Linear.final_state st1 r ->
Mach.final_state st2 r.
Proof.
Lemma wt_prog:
forall i fd,
In (
i,
Gfun fd)
prog.(
prog_defs) ->
wt_fundef fd.
Proof.
Theorem transf_program_correct:
forward_simulation (
Linear.semantics prog) (
Mach.semantics return_address_offset tprog).
Proof.
End WHOLE.
End PRESERVATION.