Computation of resource bounds for Linear code.
Require Import FSets FSetAVL.
Require Import Coqlib Ordered.
Require Intv.
Require Import AST.
Require Import Op.
Require Import Machregs Locations.
Require Import Linear.
Require Import Conventions.
Module RegOrd :=
OrderedIndexed (
IndexedMreg).
Module RegSet :=
FSetAVL.Make (
RegOrd).
Resource bounds for a function
The bounds record capture how many local and outgoing stack slots
and callee-save registers are used by a function.
We demand that all bounds are positive or null.
These properties are used later to reason about the layout of
the activation record.
Record bounds :
Type :=
mkbounds {
used_callee_save:
list mreg;
bound_local:
Z;
bound_outgoing:
Z;
bound_stack_data:
Z;
bound_local_pos:
bound_local >= 0;
bound_outgoing_pos:
bound_outgoing >= 0;
bound_stack_data_pos:
bound_stack_data >= 0;
used_callee_save_norepet:
list_norepet used_callee_save;
used_callee_save_prop:
forall r,
In r used_callee_save ->
is_callee_save r =
true
}.
The following predicates define the correctness of a set of bounds
for the code of a function.
Section WITHIN_BOUNDS.
Variable b:
bounds.
Definition mreg_within_bounds (
r:
mreg) :=
is_callee_save r =
true ->
In r (
used_callee_save b).
Definition slot_within_bounds (
sl:
slot) (
ofs:
Z) (
ty:
typ) :=
match sl with
|
Local =>
ofs +
typesize ty <=
bound_local b
|
Outgoing =>
ofs +
typesize ty <=
bound_outgoing b
|
Incoming =>
True
end.
Definition instr_within_bounds (
i:
instruction) :=
match i with
|
Lgetstack sl ofs ty r =>
slot_within_bounds sl ofs ty /\
mreg_within_bounds r
|
Lsetstack r sl ofs ty =>
slot_within_bounds sl ofs ty
|
Lop op args res =>
mreg_within_bounds res
|
Lload chunk addr args dst =>
mreg_within_bounds dst
|
Lcall sig ros =>
size_arguments sig <=
bound_outgoing b
|
Lbuiltin ef args res =>
(
forall r,
In r (
params_of_builtin_res res) \/
In r (
destroyed_by_builtin ef) ->
mreg_within_bounds r)
/\ (
forall sl ofs ty,
In (
S sl ofs ty) (
params_of_builtin_args args) ->
slot_within_bounds sl ofs ty)
|
_ =>
True
end.
End WITHIN_BOUNDS.
Definition function_within_bounds (
f:
function) (
b:
bounds) :
Prop :=
forall instr,
In instr f.(
fn_code) ->
instr_within_bounds b instr.
Inference of resource bounds for a function
The resource bounds for a function are computed by a linear scan
of its instructions.
Section BOUNDS.
Variable f:
function.
Definition record_reg (
u:
RegSet.t) (
r:
mreg) :
RegSet.t :=
if is_callee_save r then RegSet.add r u else u.
Definition record_regs (
u:
RegSet.t) (
rl:
list mreg) :
RegSet.t :=
fold_left record_reg rl u.
In the proof of the Stacking pass, we only need to bound the
registers written by an instruction. Therefore, we examine the
result registers only, not the argument registers.
Definition record_regs_of_instr (
u:
RegSet.t) (
i:
instruction) :
RegSet.t :=
match i with
|
Lgetstack sl ofs ty r =>
record_reg u r
|
Lsetstack r sl ofs ty =>
record_reg u r
|
Lop op args res =>
record_reg u res
|
Lload chunk addr args dst =>
record_reg u dst
|
Lstore chunk addr args src =>
u
|
Lcall sig ros =>
u
|
Ltailcall sig ros =>
u
|
Lbuiltin ef args res =>
record_regs (
record_regs u (
params_of_builtin_res res)) (
destroyed_by_builtin ef)
|
Llabel lbl =>
u
|
Lgoto lbl =>
u
|
Lcond cond args lbl =>
u
|
Ljumptable arg tbl =>
u
|
Lreturn =>
u
end.
Definition record_regs_of_function :
RegSet.t :=
fold_left record_regs_of_instr f.(
fn_code)
RegSet.empty.
Fixpoint slots_of_locs (
l:
list loc) :
list (
slot *
Z *
typ) :=
match l with
|
nil =>
nil
|
S sl ofs ty ::
l' => (
sl,
ofs,
ty) ::
slots_of_locs l'
|
R r ::
l' =>
slots_of_locs l'
end.
Definition slots_of_instr (
i:
instruction) :
list (
slot *
Z *
typ) :=
match i with
|
Lgetstack sl ofs ty r => (
sl,
ofs,
ty) ::
nil
|
Lsetstack r sl ofs ty => (
sl,
ofs,
ty) ::
nil
|
Lbuiltin ef args res =>
slots_of_locs (
params_of_builtin_args args)
|
_ =>
nil
end.
Definition max_over_list {
A:
Type} (
valu:
A ->
Z) (
l:
list A) :
Z :=
List.fold_left (
fun m l =>
Zmax m (
valu l))
l 0.
Definition max_over_instrs (
valu:
instruction ->
Z) :
Z :=
max_over_list valu f.(
fn_code).
Definition max_over_slots_of_instr (
valu:
slot *
Z *
typ ->
Z) (
i:
instruction) :
Z :=
max_over_list valu (
slots_of_instr i).
Definition max_over_slots_of_funct (
valu:
slot *
Z *
typ ->
Z) :
Z :=
max_over_instrs (
max_over_slots_of_instr valu).
Definition local_slot (
s:
slot *
Z *
typ) :=
match s with (
Local,
ofs,
ty) =>
ofs +
typesize ty |
_ => 0
end.
Definition outgoing_slot (
s:
slot *
Z *
typ) :=
match s with (
Outgoing,
ofs,
ty) =>
ofs +
typesize ty |
_ => 0
end.
Definition outgoing_space (
i:
instruction) :=
match i with Lcall sig _ =>
size_arguments sig |
_ => 0
end.
Lemma max_over_list_pos:
forall (
A:
Type) (
valu:
A ->
Z) (
l:
list A),
max_over_list valu l >= 0.
Proof.
Lemma max_over_slots_of_funct_pos:
forall (
valu:
slot *
Z *
typ ->
Z),
max_over_slots_of_funct valu >= 0.
Proof.
Remark fold_left_preserves:
forall (
A B:
Type) (
f:
A ->
B ->
A) (
P:
A ->
Prop),
(
forall a b,
P a ->
P (
f a b)) ->
forall l a,
P a ->
P (
fold_left f l a).
Proof.
induction l; simpl; auto.
Qed.
Remark fold_left_ensures:
forall (
A B:
Type) (
f:
A ->
B ->
A) (
P:
A ->
Prop)
b0,
(
forall a b,
P a ->
P (
f a b)) ->
(
forall a,
P (
f a b0)) ->
forall l a,
In b0 l ->
P (
fold_left f l a).
Proof.
induction l;
simpl;
intros.
contradiction.
destruct H1.
subst a.
apply fold_left_preserves;
auto.
apply IHl;
auto.
Qed.
Definition only_callee_saves (
u:
RegSet.t) :
Prop :=
forall r,
RegSet.In r u ->
is_callee_save r =
true.
Lemma record_reg_only:
forall u r,
only_callee_saves u ->
only_callee_saves (
record_reg u r).
Proof.
Lemma record_regs_only:
forall rl u,
only_callee_saves u ->
only_callee_saves (
record_regs u rl).
Proof.
Lemma record_regs_of_instr_only:
forall u i,
only_callee_saves u ->
only_callee_saves (
record_regs_of_instr u i).
Proof.
Lemma record_regs_of_function_only:
only_callee_saves record_regs_of_function.
Proof.
Program Definition function_bounds := {|
used_callee_save :=
RegSet.elements record_regs_of_function;
bound_local :=
max_over_slots_of_funct local_slot;
bound_outgoing :=
Zmax (
max_over_instrs outgoing_space) (
max_over_slots_of_funct outgoing_slot);
bound_stack_data :=
Zmax f.(
fn_stacksize) 0
|}.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
Next Obligation.
We now show the correctness of the inferred bounds.
Lemma record_reg_incr:
forall u r r',
RegSet.In r'
u ->
RegSet.In r' (
record_reg u r).
Proof.
Lemma record_reg_ok:
forall u r,
is_callee_save r =
true ->
RegSet.In r (
record_reg u r).
Proof.
Lemma record_regs_incr:
forall r'
rl u,
RegSet.In r'
u ->
RegSet.In r' (
record_regs u rl).
Proof.
Lemma record_regs_ok:
forall r rl u,
In r rl ->
is_callee_save r =
true ->
RegSet.In r (
record_regs u rl).
Proof.
Lemma record_regs_of_instr_incr:
forall r'
u i,
RegSet.In r'
u ->
RegSet.In r' (
record_regs_of_instr u i).
Proof.
Definition defined_by_instr (
r':
mreg) (
i:
instruction) :=
match i with
|
Lgetstack sl ofs ty r =>
r' =
r
|
Lop op args res =>
r' =
res
|
Lload chunk addr args dst =>
r' =
dst
|
Lbuiltin ef args res =>
In r' (
params_of_builtin_res res) \/
In r' (
destroyed_by_builtin ef)
|
_ =>
False
end.
Lemma record_regs_of_instr_ok:
forall r'
u i,
defined_by_instr r'
i ->
is_callee_save r' =
true ->
RegSet.In r' (
record_regs_of_instr u i).
Proof.
Lemma record_regs_of_function_ok:
forall r i,
In i f.(
fn_code) ->
defined_by_instr r i ->
is_callee_save r =
true ->
RegSet.In r record_regs_of_function.
Proof.
Lemma max_over_list_bound:
forall (
A:
Type) (
valu:
A ->
Z) (
l:
list A) (
x:
A),
In x l ->
valu x <=
max_over_list valu l.
Proof.
intros until x.
unfold max_over_list.
assert (
forall c z,
let f :=
fold_left (
fun x y =>
Zmax x (
valu y))
c z in
z <=
f /\ (
In x c ->
valu x <=
f)).
induction c;
simpl;
intros.
split.
omega.
tauto.
elim (
IHc (
Zmax z (
valu a)));
intros.
split.
apply Zle_trans with (
Zmax z (
valu a)).
apply Zmax1.
auto.
intro H1;
elim H1;
intro.
subst a.
apply Zle_trans with (
Zmax z (
valu x)).
apply Zmax2.
auto.
auto.
intro.
elim (
H l 0);
intros.
auto.
Qed.
Lemma max_over_instrs_bound:
forall (
valu:
instruction ->
Z)
i,
In i f.(
fn_code) ->
valu i <=
max_over_instrs valu.
Proof.
Lemma max_over_slots_of_funct_bound:
forall (
valu:
slot *
Z *
typ ->
Z)
i s,
In i f.(
fn_code) ->
In s (
slots_of_instr i) ->
valu s <=
max_over_slots_of_funct valu.
Proof.
Lemma local_slot_bound:
forall i ofs ty,
In i f.(
fn_code) ->
In (
Local,
ofs,
ty) (
slots_of_instr i) ->
ofs +
typesize ty <=
bound_local function_bounds.
Proof.
Lemma outgoing_slot_bound:
forall i ofs ty,
In i f.(
fn_code) ->
In (
Outgoing,
ofs,
ty) (
slots_of_instr i) ->
ofs +
typesize ty <=
bound_outgoing function_bounds.
Proof.
Lemma size_arguments_bound:
forall sig ros,
In (
Lcall sig ros)
f.(
fn_code) ->
size_arguments sig <=
bound_outgoing function_bounds.
Proof.
Consequently, all machine registers or stack slots mentioned by one
of the instructions of function f are within bounds.
Lemma mreg_is_within_bounds:
forall i,
In i f.(
fn_code) ->
forall r,
defined_by_instr r i ->
mreg_within_bounds function_bounds r.
Proof.
Lemma slot_is_within_bounds:
forall i,
In i f.(
fn_code) ->
forall sl ty ofs,
In (
sl,
ofs,
ty) (
slots_of_instr i) ->
slot_within_bounds function_bounds sl ofs ty.
Proof.
Lemma slots_of_locs_charact:
forall sl ofs ty l,
In (
sl,
ofs,
ty) (
slots_of_locs l) <->
In (
S sl ofs ty)
l.
Proof.
induction l; simpl; intros.
tauto.
destruct a; simpl; intuition congruence.
Qed.
It follows that every instruction in the function is within bounds,
in the sense of the instr_within_bounds predicate.
Lemma instr_is_within_bounds:
forall i,
In i f.(
fn_code) ->
instr_within_bounds function_bounds i.
Proof.
Lemma function_is_within_bounds:
function_within_bounds f function_bounds.
Proof.
End BOUNDS.
Helper to determine the size of the frame area that holds the contents of saved registers.
Fixpoint size_callee_save_area_rec (
l:
list mreg) (
ofs:
Z) :
Z :=
match l with
|
nil =>
ofs
|
r ::
l =>
let ty :=
mreg_type r in
let sz :=
AST.typesize ty in
size_callee_save_area_rec l (
align ofs sz +
sz)
end.
Definition size_callee_save_area (
b:
bounds) (
ofs:
Z) :
Z :=
size_callee_save_area_rec (
used_callee_save b)
ofs.
Lemma size_callee_save_area_rec_incr:
forall l ofs,
ofs <=
size_callee_save_area_rec l ofs.
Proof.
Lemma size_callee_save_area_incr:
forall b ofs,
ofs <=
size_callee_save_area b ofs.
Proof.
Layout of the stack frame and its properties. These definitions
are used in the machine-dependent Stacklayout module and in the
Stacking pass.
Record frame_env :
Type :=
mk_frame_env {
fe_size:
Z;
fe_ofs_retaddr:
Z;
fe_ofs_local:
Z;
fe_ofs_callee_save:
Z;
fe_stack_data:
Z;
fe_used_callee_save:
list mreg
}.