Recognition of tail calls: correctness proof
Require Import Coqlib Maps Integers AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Registers RTL Conventions Tailcall.
Require Import StackInj.
Syntactic properties of the code transformation
Measuring the number of instructions eliminated
The return_measure c pc function counts the number of instructions
eliminated by the code transformation, where pc is the successor
of a call turned into a tailcall. This is the length of the
move/nop/return sequence recognized by the is_return boolean function.
Fixpoint return_measure_rec (
n:
nat) (
c:
code) (
pc:
node)
{
struct n}:
nat :=
match n with
|
O =>
O
|
S n' =>
match c!
pc with
|
Some(
Inop s) =>
S(
return_measure_rec n'
c s)
|
Some(
Iop op args dst s) =>
S(
return_measure_rec n'
c s)
|
_ =>
O
end
end.
Definition return_measure (
c:
code) (
pc:
node) :=
return_measure_rec niter c pc.
Lemma return_measure_bounds:
forall f pc, (
return_measure f pc <=
niter)%
nat.
Proof.
intro f.
assert (
forall n pc, (
return_measure_rec n f pc <=
n)%
nat).
induction n;
intros;
simpl.
omega.
destruct (
f!
pc);
try omega.
destruct i;
try omega.
generalize (
IHn n0).
omega.
generalize (
IHn n0).
omega.
intros.
unfold return_measure.
apply H.
Qed.
Remark return_measure_rec_incr:
forall f n1 n2 pc,
(
n1 <=
n2)%
nat ->
(
return_measure_rec n1 f pc <=
return_measure_rec n2 f pc)%
nat.
Proof.
induction n1; intros; simpl.
omega.
destruct n2. omegaContradiction. assert (n1 <= n2)%nat by omega.
simpl. destruct f!pc; try omega. destruct i; try omega.
generalize (IHn1 n2 n H0). omega.
generalize (IHn1 n2 n H0). omega.
Qed.
Lemma is_return_measure_rec:
forall f n n'
pc r,
is_return n f pc r =
true -> (
n <=
n')%
nat ->
return_measure_rec n f.(
fn_code)
pc =
return_measure_rec n'
f.(
fn_code)
pc.
Proof.
induction n;
simpl;
intros.
congruence.
destruct n'.
omegaContradiction.
simpl.
destruct (
fn_code f)!
pc;
try congruence.
destruct i;
try congruence.
decEq.
apply IHn with r.
auto.
omega.
destruct (
is_move_operation o l);
try congruence.
destruct (
Reg.eq r r1);
try congruence.
decEq.
apply IHn with r0.
auto.
omega.
Qed.
Relational characterization of the code transformation
The is_return_spec characterizes the instruction sequences
recognized by the is_return boolean function.
Inductive is_return_spec (
f:
function):
node ->
reg ->
Prop :=
|
is_return_none:
forall pc r,
f.(
fn_code)!
pc =
Some(
Ireturn None) ->
is_return_spec f pc r
|
is_return_some:
forall pc r,
f.(
fn_code)!
pc =
Some(
Ireturn (
Some r)) ->
is_return_spec f pc r
|
is_return_nop:
forall pc r s,
f.(
fn_code)!
pc =
Some(
Inop s) ->
is_return_spec f s r ->
(
return_measure f.(
fn_code)
s <
return_measure f.(
fn_code)
pc)%
nat ->
is_return_spec f pc r
|
is_return_move:
forall pc r r'
s,
f.(
fn_code)!
pc =
Some(
Iop Omove (
r::
nil)
r'
s) ->
is_return_spec f s r' ->
(
return_measure f.(
fn_code)
s <
return_measure f.(
fn_code)
pc)%
nat ->
is_return_spec f pc r.
Lemma is_return_charact:
forall f n pc rret,
is_return n f pc rret =
true -> (
n <=
niter)%
nat ->
is_return_spec f pc rret.
Proof.
The transf_instr_spec predicate relates one instruction in the
initial code with its possible transformations in the optimized code.
Inductive transf_instr_spec (
f:
function):
instruction ->
instruction ->
Prop :=
|
transf_instr_tailcall:
forall sig ros args res s,
f.(
fn_stacksize) = 0 ->
is_return_spec f s res ->
transf_instr_spec f (
Icall sig ros args res s) (
Itailcall sig ros args)
|
transf_instr_default:
forall i,
transf_instr_spec f i i.
Lemma transf_instr_charact:
forall f pc instr,
f.(
fn_stacksize) = 0 ->
transf_instr_spec f instr (
transf_instr f pc instr).
Proof.
Lemma transf_instr_lookup:
forall f pc i,
f.(
fn_code)!
pc =
Some i ->
exists i', (
transf_function f).(
fn_code)!
pc =
Some i' /\
transf_instr_spec f i i'.
Proof.
Semantic properties of the code transformation
The ``less defined than'' relation between register states
A call followed by a return without an argument can be turned
into a tail call. In this case, the original function returns
Vundef, while the transformed function can return any value.
We account for this situation by using the ``less defined than''
relation between values and between memory states. We need to
extend it pointwise to register states.
Lemma regs_lessdef_init_regs:
forall params vl vl',
Val.lessdef_list vl vl' ->
regs_lessdef (
init_regs vl params) (
init_regs vl'
params).
Proof.
induction params;
intros.
simpl.
red;
intros.
rewrite Regmap.gi.
constructor.
simpl.
inv H.
red;
intros.
rewrite Regmap.gi.
constructor.
apply set_reg_lessdef.
auto.
auto.
Qed.
Proof of semantic preservation
Definition match_prog (
p tp:
RTL.program) :=
match_program (
fun cu f tf =>
tf =
transf_fundef f)
eq p tp.
Lemma transf_program_match:
forall p,
match_prog p (
transf_program p).
Proof.
Section PRESERVATION.
Context `{
external_calls_prf:
ExternalCalls}.
Existing Instance inject_perm_all.
Variable prog tprog:
program.
Hypothesis TRANSL:
match_prog prog tprog.
Definition regs_inject (
j:
meminj) (
rs1 rs2:
Regmap.t val) :=
forall r,
Val.inject j (
rs1 #
r) (
rs2 #
r).
Definition inject_globals {
F V} (
g:
Genv.t F V)
j:=
(
forall b,
Plt b (
Genv.genv_next g) ->
j b =
Some (
b,0)) /\
(
forall b1 b2 delta,
j b1 =
Some (
b2,
delta) ->
Plt b2 (
Genv.genv_next g) ->
b2 =
b1 /\
delta = 0).
Let ge :=
Genv.globalenv prog.
Let tge :=
Genv.globalenv tprog.
Lemma symbols_preserved:
forall (
s:
ident),
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof (
Genv.find_symbol_transf TRANSL).
Lemma functions_translated:
forall (
v:
val) (
f:
RTL.fundef),
Genv.find_funct ge v =
Some f ->
Genv.find_funct tge v =
Some (
transf_fundef f).
Proof (
Genv.find_funct_transf TRANSL).
Lemma funct_ptr_translated:
forall (
b:
block) (
f:
RTL.fundef),
Genv.find_funct_ptr ge b =
Some f ->
Genv.find_funct_ptr tge b =
Some (
transf_fundef f).
Proof (
Genv.find_funct_ptr_transf TRANSL).
Lemma senv_preserved:
Senv.equiv ge tge.
Proof (
Genv.senv_transf TRANSL).
Lemma genv_next_preserved:
Genv.genv_next tge =
Genv.genv_next ge.
Proof.
Lemma sig_preserved:
forall f,
funsig (
transf_fundef f) =
funsig f.
Proof.
Lemma stacksize_preserved:
forall f,
fn_stacksize (
transf_function f) =
fn_stacksize f.
Proof.
Lemma find_function_translated:
forall ros rs rs'
f j,
find_function ge ros rs =
Some f ->
regs_inject j rs rs' ->
inject_globals ge j ->
find_function tge ros rs' =
Some (
transf_fundef f).
Proof.
Consider an execution of a call/move/nop/return sequence in the
original code and the corresponding tailcall in the transformed code.
The transition sequences are of the following form
(left: original code, right: transformed code).
f is the calling function and
fd the called function.
State stk f (Icall instruction) State stk' f' (Itailcall)
Callstate (frame::stk) fd args Callstate stk' fd' args'
. .
. .
. .
Returnstate (frame::stk) res Returnstate stk' res'
State stk f (move/nop/return seq)
.
.
.
State stk f (return instr)
Returnstate stk res
The simulation invariant must therefore account for two kinds of
mismatches between the transition sequences:
-
The call stack of the original program can contain more frames
than that of the transformed program (e.g. frame in the example above).
-
The regular states corresponding to executing the move/nop/return
sequence must all correspond to the single Returnstate stk' res'
state of the transformed program.
We first define the simulation invariant between call stacks.
The first two cases are standard, but the third case corresponds
to a frame that was eliminated by the transformation.
:
meminj ->
nat ->
list nat ->
list stackframe ->
list stackframe ->
Prop :=
|
match_stackframes_nil j:
match_stackframes j O nil nil nil
|
match_stackframes_normal:
forall j n l stk stk'
res sp sp'
pc rs rs'
f,
match_stackframes j n l stk stk' ->
regs_inject j rs rs' ->
j sp =
Some (
sp',0) ->
match_stackframes j O (
S n::
l)
(
Stackframe res f (
Vptr sp Ptrofs.zero)
pc rs ::
stk)
(
Stackframe res (
transf_function f) (
Vptr sp'
Ptrofs.zero)
pc rs' ::
stk')
|
match_stackframes_tail:
forall j n l stk stk'
res sp pc rs f,
match_stackframes j n l stk stk' ->
is_return_spec f pc res ->
f.(
fn_stacksize) = 0 ->
match_stackframes j
(
S n)
l
(
Stackframe res f (
Vptr sp Ptrofs.zero)
pc rs ::
stk)
stk'.
Here is the invariant relating two states. The first three
cases are standard. Note the ``less defined than'' conditions
over values and register states, and the corresponding ``extends''
relation over memory states.
Lemma sizes_upstar:
forall n g s1 s2 l,
sizes (
n ::
g)
s1 s2 ->
sizes (
S n ::
g) ((
None,
l) ::
s1)
s2.
Proof.
intros n g s1 s2 l SZ.
inv SZ. simpl in *. repeat destr_in H2.
econstructor; simpl; auto. rewrite Heqo. eauto. right; auto.
Qed.
Lemma sizes_upstar':
forall n g s1 s2 f l,
sizes (
n ::
g)
s1 (
f::
s2) ->
sizes (
S n ::
g) ((
None,
l) ::
s1) ((
None,
opt_cons (
fst f) (
snd f))::
s2).
Proof.
intros n g s1 s2 f l SZ.
inv SZ.
simpl in *.
repeat destr_in H5.
econstructor;
simpl;
auto.
rewrite Heqo.
eauto.
right;
auto.
rewrite size_frames_tc.
auto.
Qed.
Lemma sizes_up:
forall g s1 s2,
sizes g s1 s2 ->
sizes (1%
nat ::
g) ((
None,
nil) ::
s1) ((
None,
nil) ::
s2).
Proof.
intros g s1 s2 SZ. econstructor; simpl; eauto.
left. omega.
Qed.
Lemma sizes_record:
forall g tf1 r1 tf2 r2 fr1 fr2
(
SZ:
sizes g (
tf1 ::
r1) (
tf2 ::
r2))
(
EQ:
frame_adt_size fr1 =
frame_adt_size fr2),
sizes g ((
Some fr1,
opt_cons (
fst tf1) (
snd tf1)) ::
r1) ((
Some fr2 ,
opt_cons (
fst tf2) (
snd tf2)) ::
r2).
Proof.
Definition tc_sizes:
frameinj ->
stack ->
stack ->
Prop :=
sizes.
Definition tc_sizes_upstar:
forall n g s1 s2 l,
tc_sizes (
n ::
g)
s1 s2 ->
tc_sizes (
S n ::
g) ((
None,
l) ::
s1)
s2 :=
sizes_upstar.
Definition tc_sizes_up:
forall g s1 s2,
tc_sizes g s1 s2 ->
tc_sizes (1%
nat ::
g) ((
None,
nil) ::
s1) ((
None,
nil) ::
s2) :=
sizes_up.
Definition tc_sizes_ndown:
forall n g s1 s2,
tc_sizes (
S n ::
g)
s1 s2 ->
tc_sizes g (
drop (
S n)
s1) (
tl s2) :=
compat_sizes_drop.
Definition tc_sizes_size_stack:
forall g s1 s2,
tc_sizes g s1 s2 ->
size_stack s2 <=
size_stack s1 :=
sizes_size_stack.
Definition tc_sizes_record:
forall g tf1 r1 tf2 r2 fr1 fr2
(
SZ:
tc_sizes g (
tf1 ::
r1) (
tf2 ::
r2))
(
EQ:
frame_adt_size fr1 =
frame_adt_size fr2),
tc_sizes g ((
Some fr1,
opt_cons (
fst tf1) (
snd tf1)) ::
r1)
((
Some fr2,
opt_cons (
fst tf2) (
snd tf2)) ::
r2) :=
sizes_record.
Variable fn_stack_requirements:
ident ->
Z.
Section WITHINITMEM.
Variable init_m:
mem.
Inductive match_states:
state ->
state ->
Prop :=
|
match_states_normal:
forall s sp sp'
pc rs m s'
rs'
m'
f g j n l
(
STACKS:
match_stackframes j n g s s')
(
RLD:
regs_inject j rs rs')
(
MLD:
Mem.inject j (
S n ::
g ++
l)
m m')
(
SZ:
tc_sizes (
S n ::
g ++
l) (
Mem.stack m) (
Mem.stack m'))
(
IG:
inject_globals ge j)
(
JB:
j sp =
Some (
sp', 0))
(
INCR:
inject_incr (
Mem.flat_inj (
Mem.nextblock init_m))
j)
(
SEP:
inject_separated (
Mem.flat_inj (
Mem.nextblock init_m))
j init_m init_m),
match_states (
State s f (
Vptr sp Ptrofs.zero)
pc rs m)
(
State s' (
transf_function f) (
Vptr sp'
Ptrofs.zero)
pc rs'
m')
|
match_states_call:
forall s f args m s'
args'
m'
sz g j n l
(
MS:
match_stackframes j n g s s')
(
LDargs:
Val.inject_list j args args')
(
MLD:
Mem.inject j (
S n ::
g ++
l)
m m')
(
SZ:
tc_sizes (
S n ::
g ++
l) (
Mem.stack m) (
Mem.stack m'))
(
IG:
inject_globals ge j)
(
INCR:
inject_incr (
Mem.flat_inj (
Mem.nextblock init_m))
j)
(
SEP:
inject_separated (
Mem.flat_inj (
Mem.nextblock init_m))
j init_m init_m),
match_states (
Callstate s f args m sz)
(
Callstate s' (
transf_fundef f)
args'
m'
sz)
|
match_states_return:
forall s v m s'
v'
m'
g j n l
(
MS:
match_stackframes j n g s s')
(
LDret:
Val.inject j v v')
(
MLD:
Mem.inject j (
S n ::
g ++
l)
m m')
(
SZ:
tc_sizes (
g ++
l) (
drop (
S n) (
Mem.stack m)) (
tl (
Mem.stack m')))
(
IG:
inject_globals ge j)
(
INCR:
inject_incr (
Mem.flat_inj (
Mem.nextblock init_m))
j)
(
SEP:
inject_separated (
Mem.flat_inj (
Mem.nextblock init_m))
j init_m init_m),
match_states (
Returnstate s v m)
(
Returnstate s'
v'
m')
|
match_states_interm:
forall s sp pc rs m s'
m'
f r v'
g j n l
(
STACKS:
match_stackframes j n g s s')
(
MLD:
Mem.inject j (
S n ::
g ++
l)
m m')
(
RETspec:
is_return_spec f pc r)
(
SZzero:
f.(
fn_stacksize) = 0)
(
LDret:
Val.inject j (
rs#
r)
v')
(
SZ:
tc_sizes (
g++
l) (
drop (
S n) (
Mem.stack m)) (
tl (
Mem.stack m')))
(
IG:
inject_globals ge j)
(
INCR:
inject_incr (
Mem.flat_inj (
Mem.nextblock init_m))
j)
(
SEP:
inject_separated (
Mem.flat_inj (
Mem.nextblock init_m))
j init_m init_m),
match_states (
State s f (
Vptr sp Ptrofs.zero)
pc rs m)
(
Returnstate s'
v'
m').
Definition mem_state (
s:
state) :
mem :=
match s with
State _ _ _ _ _ m
|
Callstate _ _ _ m _
|
Returnstate _ _ m =>
m
end.
Definition current_sp_state (
s:
state) :
option (
option (
block *
Z)) :=
match s with
State _ f (
Vptr sp _)
_ _ _ =>
Some (
Some (
sp,
fn_stacksize f))
|
State _ _ _ _ _ _ =>
None
|
_ =>
Some None
end.
Definition stackblocks_of_stackframe (
sf:
stackframe) :
option (
block *
Z) :=
match sf with
| (
Stackframe _ f (
Vptr sp _)
_ _) =>
Some (
sp,
fn_stacksize f)
|
_ =>
None
end.
Definition stackframes_state (
s:
state) :
list stackframe :=
match s with
State stk _ _ _ _ _
|
Callstate stk _ _ _ _
|
Returnstate stk _ _ =>
stk
end.
Definition stack_blocks_of_state (
s:
state) :
list (
option (
block *
Z)) :=
match current_sp_state s with
Some (
Some x) =>
Some x ::
map stackblocks_of_stackframe (
stackframes_state s)
|
Some None =>
map stackblocks_of_stackframe (
stackframes_state s)
|
None =>
None ::
map stackblocks_of_stackframe (
stackframes_state s)
end.
Definition sp_valid (
s :
state) :
Prop :=
Forall (
fun bz =>
match bz with
Some (
b,
z) =>
Mem.valid_block (
mem_state s)
b
|
None =>
True
end) (
stack_blocks_of_state s).
The last case of
match_states corresponds to the execution
of a move/nop/return sequence in the original code that was
eliminated by the transformation:
State stk f (move/nop/return seq) ~~ Returnstate stk' res'
.
.
.
State stk f (return instr) ~~ Returnstate stk' res'
To preserve non-terminating behaviors, we need to make sure
that the execution of this sequence in the original code cannot
diverge. For this, we introduce the following complicated
measure over states, which will decrease strictly whenever
the original code makes a transition but the transformed code
does not.
(
st:
state) :
nat :=
match st with
|
State s f sp pc rs m => (
List.length s * (
niter + 2) +
return_measure f.(
fn_code)
pc + 1)%
nat
|
Callstate s f args m sz => 0%
nat
|
Returnstate s v m => (
List.length s * (
niter + 2))%
nat
end.
Ltac TransfInstr :=
match goal with
|
H: (
PTree.get _ (
fn_code _) =
_) |-
_ =>
destruct (
transf_instr_lookup _ _ _ H)
as [
i' [
TINSTR TSPEC]];
inv TSPEC
end.
Ltac EliminatedInstr :=
match goal with
|
H: (
is_return_spec _ _ _) |-
_ =>
inv H;
try congruence
|
_ =>
idtac
end.
The proof of semantic preservation, then, is a simulation diagram
of the ``option'' kind.
Lemma regs_inject_regs:
forall j rs1 rs2,
regs_inject j rs1 rs2 ->
forall rl,
Val.inject_list j rs1##
rl rs2##
rl.
Proof.
induction rl; constructor; auto.
Qed.
Lemma set_reg_inject:
forall j r v1 v2 rs1 rs2,
Val.inject j v1 v2 ->
regs_inject j rs1 rs2 ->
regs_inject j (
rs1#
r <-
v1) (
rs2#
r <-
v2).
Proof.
intros;
red;
intros.
repeat rewrite Regmap.gsspec.
destruct (
peq r0 r);
auto.
Qed.
Lemma set_res_inject:
forall j res v1 v2 rs1 rs2,
Val.inject j v1 v2 ->
regs_inject j rs1 rs2 ->
regs_inject j (
regmap_setres res v1 rs1) (
regmap_setres res v2 rs2).
Proof.
Lemma ros_is_function_transf:
forall j ros rs rs'
id,
inject_globals ge j ->
ros_is_function ge ros rs id ->
regs_inject j rs rs' ->
ros_is_function tge ros rs'
id.
Proof.
unfold ros_is_function.
intros.
destr_in H0.
simpl.
destruct H0 as (
b &
o &
RS &
FS).
specialize (
H1 r).
rewrite RS in H1;
inv H1.
eexists;
eexists;
split;
eauto.
rewrite symbols_preserved.
rewrite FS.
f_equal.
destruct H.
erewrite H in H4.
inv H4.
auto.
eapply Genv.genv_symb_range;
eauto.
Qed.
Lemma inject_globals_meminj_preserves_globals:
forall {
F V} (
g:
Genv.t F V)
j,
inject_globals g j ->
meminj_preserves_globals g j.
Proof.
Lemma regs_inject_init_regs:
forall j params vl vl',
Val.inject_list j vl vl' ->
regs_inject j (
init_regs vl params) (
init_regs vl'
params).
Proof.
induction params;
intros.
simpl.
red;
intros.
rewrite Regmap.gi.
constructor.
simpl.
inv H.
red;
intros.
rewrite Regmap.gi.
constructor.
apply set_reg_inject.
auto.
auto.
Qed.
Lemma match_stackframes_incr:
forall f n l s s'
(
MS:
match_stackframes f n l s s')
f' (
INCR:
inject_incr f f'),
match_stackframes f'
n l s s'.
Proof.
induction 1; simpl; intros; eauto; try now econstructor; eauto.
econstructor; eauto.
red; intros; eauto.
Qed.
Lemma inject_globals_incr:
forall f f'
(
INCR :
inject_incr f f')
(
SEP :
forall b1 b2 delta,
f b1 =
None ->
f'
b1 =
Some (
b2,
delta) ->
Ple (
Genv.genv_next ge)
b1 /\
Ple (
Genv.genv_next ge)
b2)
(
IG:
inject_globals ge f),
inject_globals ge f'.
Proof.
intros f f' INCR SEP (IG1 & IG2); split; intros; eauto.
eapply IG2; eauto.
destruct (f b1) eqn:FB1.
- destruct p. eapply INCR in FB1. congruence.
- specialize (SEP _ _ _ FB1 H).
xomega.
Qed.
Lemma tl_iter_commut:
forall {
A} (
l:
list A)
n,
tl (
Nat.iter n (@
tl _)
l) =
Nat.iter n (@
tl _) (
tl l).
Proof.
induction n; simpl; intros; eauto. rewrite IHn. auto.
Qed.
Hypothesis init_m_genv_next:
Ple (
Genv.genv_next ge) (
Mem.nextblock init_m).
Definition nextblock_inv (
s:
state) :=
Ple (
Mem.nextblock init_m) (
Mem.nextblock (
mem_state s)).
Lemma tc_sizes_same_top:
forall g f1 r1 f2 r2 f1'
f2',
tc_sizes g (
f1::
r1) (
f2::
r2) ->
size_frames f1 =
size_frames f1' ->
size_frames f2 =
size_frames f2' ->
tc_sizes g (
f1'::
r1) (
f2'::
r2).
Proof.
intros g f1 r1 f2 r2 f1' f2' SZ EQ1 EQ2.
inv SZ. simpl in *. repeat destr_in H4.
econstructor; simpl. eauto. rewrite Heqo. eauto.
rewrite <- EQ2.
inv H5; [left|right]. omega. auto.
Qed.
Lemma match_stackframes_no_perm':
forall j n g s s'
P,
match_stackframes j n g s s' ->
forall stk sp,
stack_agree_perms P stk ->
match_stack (
Some (
sp, 0) ::
map block_of_stackframe s)
stk ->
forall l0,
take (
S n)
stk =
Some l0 ->
Forall (
fun tf =>
forall b,
in_frames tf b ->
forall o k p, ~
P b o k p)
l0.
Proof.
induction 1;
simpl;
intros stk0 sp0 SAP MS l0 TAKE;
eauto.
-
repeat destr_in TAKE.
constructor;
auto.
inv MS.
unfold in_frames;
simpl.
unfold get_frame_blocks;
rewrite BLOCKS.
simpl.
intros b [[]|[]].
intros o k p PERM.
exploit SAP.
left.
reflexivity.
simpl.
reflexivity.
rewrite BLOCKS;
left;
reflexivity.
eauto.
rewrite SIZE.
rewrite Z.max_id.
omega.
-
repeat destr_in TAKE.
constructor;
auto.
inv MS.
unfold in_frames;
simpl.
unfold get_frame_blocks;
rewrite BLOCKS.
simpl.
intros b [[]|[]].
intros o k p PERM.
exploit SAP.
left.
reflexivity.
simpl.
reflexivity.
rewrite BLOCKS;
left;
reflexivity.
eauto.
rewrite SIZE.
rewrite Z.max_id.
omega.
-
repeat destr_in TAKE.
repeat destr_in Heqo.
constructor;
eauto.
+
inv MS.
unfold in_frames;
simpl.
unfold get_frame_blocks;
rewrite BLOCKS.
simpl.
intros b [[]|[]].
intros o k p PERM.
exploit SAP.
left.
reflexivity.
simpl.
reflexivity.
rewrite BLOCKS;
left;
reflexivity.
eauto.
rewrite SIZE.
rewrite Z.max_id.
omega.
+
inv MS.
rewrite H1 in REC.
eapply IHmatch_stackframes in REC;
eauto.
eapply stack_agree_perms_tl in SAP;
simpl in *;
auto.
simpl.
rewrite Heqo0.
reflexivity.
Qed.
Lemma match_stackframes_no_perm:
forall j n g s s',
match_stackframes j n g s s' ->
forall m sp sz,
sz = 0 ->
match_stack (
Some (
sp,
sz) ::
map block_of_stackframe s) (
Mem.stack m) ->
forall l0,
take (
S n) (
Mem.stack m) =
Some l0 ->
Forall (
fun tf =>
forall b,
in_frames tf b ->
forall o k p, ~
Mem.perm m b o k p)
l0.
Proof.
Lemma transf_step_correct:
forall s1 t s2,
step fn_stack_requirements ge s1 t s2 ->
forall s1' (
MS:
match_states s1 s1') (
NI1:
nextblock_inv s1) (
NI2:
nextblock_inv s1') (
SPV:
sp_valid s1) (
MSA:
stack_inv s1) (
MSA':
stack_inv s1'),
(
exists s2',
step fn_stack_requirements tge s1'
t s2' /\
match_states s2 s2')
\/ (
measure s2 <
measure s1 /\
t =
E0 /\
match_states s2 s1')%
nat.
Proof.
Lemma nextblock_inv_step:
forall ge s1 t s1'
(
MSG:
nextblock_inv s1)
(
STEP:
step fn_stack_requirements ge s1 t s1'),
nextblock_inv s1'.
Proof.
intros ge0 s1 t s1' MSG STEP.
inv STEP; red in MSG; red; simpl in *; rewnb; auto.
xomega.
Qed.
Lemma sp_valid_step:
forall s1 t s1',
sp_valid s1 ->
step fn_stack_requirements ge s1 t s1' ->
sp_valid s1'.
Proof.
Definition match_states'
s1 s2 :=
match_states s1 s2 /\
stack_inv s1 /\
stack_inv s2 /\
sp_valid s1 /\
nextblock_inv s1 /\
nextblock_inv s2.
Hint Resolve nextblock_inv_step sp_valid_step stack_inv_inv.
Lemma transf_step_correct':
forall s1 t s2,
step fn_stack_requirements ge s1 t s2 ->
forall s1',
match_states'
s1 s1' ->
(
exists s2',
step fn_stack_requirements tge s1'
t s2' /\
match_states'
s2 s2') \/
(
measure s2 <
measure s1)%
nat /\
t =
E0 /\
match_states'
s2 s1'.
Proof.
intros s1 t s2 STEP s1'
MS.
destruct MS as (
MS &
MSA &
MSA' &
SPV &
MSG &
MSG').
edestruct (
transf_step_correct _ _ _ STEP _ MS)
as
[(
s2' &
STEP' &
MS')|(
MLT &
TE0 &
MS')];
eauto.
-
left.
eexists;
split;
eauto.
repeat split;
eauto.
-
right;
repeat split;
eauto.
Qed.
End WITHINITMEM.
Inductive ms (
s1 s2 :
state) :
Prop :=
|
ms_intro init_m (
INIT:
Genv.init_mem prog =
Some init_m) (
MS:
match_states'
init_m s1 s2).
Lemma transf_initial_states:
forall st1,
initial_state fn_stack_requirements prog st1 ->
exists st2,
initial_state fn_stack_requirements tprog st2 /\
ms st1 st2.
Proof.
Lemma transf_final_states:
forall st1 st2 r,
ms st1 st2 ->
final_state st1 r ->
final_state st2 r.
Proof.
intros st1 st2 r MS FS. inv FS. inv MS. inv MS0. inv H. inv LDret. inv MS. constructor.
Qed.
The preservation of the observable behavior of the program then
follows.
Theorem transf_program_correct:
forward_simulation (
RTL.semantics fn_stack_requirements prog) (
RTL.semantics fn_stack_requirements tprog).
Proof.
End PRESERVATION.