Library Bounds
Computation of resource bounds forr Linear code.
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Op.
Require Import Locations.
Require Import Linear.
Require Import Lineartyping.
Require Import Conventions.
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 {
bound_int_local: Z;
bound_float_local: Z;
bound_int_callee_save: Z;
bound_float_callee_save: Z;
bound_outgoing: Z;
bound_int_local_pos: bound_int_local >= 0;
bound_float_local_pos: bound_float_local >= 0;
bound_int_callee_save_pos: bound_int_callee_save >= 0;
bound_float_callee_save_pos: bound_float_callee_save >= 0;
bound_outgoing_pos: bound_outgoing >= 0
}.
The following predicates define the correctness of a set of bounds
for the code of a function.
Section BELOW.
Variable funct: function.
Variable b: bounds.
Definition mreg_within_bounds (r: mreg) :=
match mreg_type r with
| Tint => index_int_callee_save r < bound_int_callee_save b
| Tfloat => index_float_callee_save r < bound_float_callee_save b
end.
Definition slot_within_bounds (s: slot) :=
match s with
| Local ofs Tint => 0 <= ofs < bound_int_local b
| Local ofs Tfloat => 0 <= ofs < bound_float_local b
| Outgoing ofs ty => 0 <= ofs /\ ofs + typesize ty <= bound_outgoing b
| Incoming ofs ty => In (S s) (loc_parameters funct.(fn_sig))
end.
Definition instr_within_bounds (i: instruction) :=
match i with
| Lgetstack s r => slot_within_bounds s /\ mreg_within_bounds r
| Lsetstack r s => slot_within_bounds s
| 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
| _ => True
end.
End BELOW.
Definition function_within_bounds (f: function) (b: bounds) : Prop :=
forall instr, In instr f.(fn_code) -> instr_within_bounds f b instr.
The resource bounds for a function are computed by a linear scan
of its instructions.
Section BOUNDS.
Variable f: function.
In the proof of the
Stacking pass, we only need to bound the
registers written by an instruction. Therefore, this function
returns these registers, ignoring registers used only as
arguments.
Definition regs_of_instr (i: instruction) : list mreg :=
match i with
| Lgetstack s r => r :: nil
| Lsetstack r s => r :: nil
| Lop op args res => res :: nil
| Lload chunk addr args dst => dst :: nil
| Lstore chunk addr args src => nil
| Lcall sig ros => nil
| Ltailcall sig ros => nil
| Llabel lbl => nil
| Lgoto lbl => nil
| Lcond cond args lbl => nil
| Ljumptable arg tbl => nil
| Lreturn => nil
end.
Definition slots_of_instr (i: instruction) : list slot :=
match i with
| Lgetstack s r => s :: nil
| Lsetstack r s => s :: nil
| _ => 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 instruction valu f.(fn_code).
Definition max_over_regs_of_instr (valu: mreg -> Z) (i: instruction) : Z :=
max_over_list mreg valu (regs_of_instr i).
Definition max_over_slots_of_instr (valu: slot -> Z) (i: instruction) : Z :=
max_over_list slot valu (slots_of_instr i).
Definition max_over_regs_of_funct (valu: mreg -> Z) : Z :=
max_over_instrs (max_over_regs_of_instr valu).
Definition max_over_slots_of_funct (valu: slot -> Z) : Z :=
max_over_instrs (max_over_slots_of_instr valu).
Definition int_callee_save (r: mreg) := 1 + index_int_callee_save r.
Definition float_callee_save (r: mreg) := 1 + index_float_callee_save r.
Definition int_local (s: slot) :=
match s with Local ofs Tint => 1 + ofs | _ => 0 end.
Definition float_local (s: slot) :=
match s with Local ofs Tfloat => 1 + ofs | _ => 0 end.
Definition outgoing_slot (s: slot) :=
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 A valu l >= 0.
Lemma max_over_slots_of_funct_pos:
forall (valu: slot -> Z), max_over_slots_of_funct valu >= 0.
Lemma max_over_regs_of_funct_pos:
forall (valu: mreg -> Z), max_over_regs_of_funct valu >= 0.
Program Definition function_bounds :=
mkbounds
(max_over_slots_of_funct int_local)
(max_over_slots_of_funct float_local)
(max_over_regs_of_funct int_callee_save)
(max_over_regs_of_funct float_callee_save)
(Zmax (max_over_instrs outgoing_space)
(max_over_slots_of_funct outgoing_slot))
(max_over_slots_of_funct_pos int_local)
(max_over_slots_of_funct_pos float_local)
(max_over_regs_of_funct_pos int_callee_save)
(max_over_regs_of_funct_pos float_callee_save)
_.
Next Obligation.
apply Zle_ge. eapply Zle_trans. 2: apply Zmax2.
apply Zge_le. apply max_over_slots_of_funct_pos.
We now show the correctness of the inferred bounds.
Lemma max_over_list_bound:
forall (A: Type) (valu: A -> Z) (l: list A) (x: A),
In x l -> valu x <= max_over_list A valu l.
Lemma max_over_instrs_bound:
forall (valu: instruction -> Z) i,
In i f.(fn_code) -> valu i <= max_over_instrs valu.
Lemma max_over_regs_of_funct_bound:
forall (valu: mreg -> Z) i r,
In i f.(fn_code) -> In r (regs_of_instr i) ->
valu r <= max_over_regs_of_funct valu.
Lemma max_over_slots_of_funct_bound:
forall (valu: slot -> Z) i s,
In i f.(fn_code) -> In s (slots_of_instr i) ->
valu s <= max_over_slots_of_funct valu.
Lemma int_callee_save_bound:
forall i r,
In i f.(fn_code) -> In r (regs_of_instr i) ->
index_int_callee_save r < bound_int_callee_save function_bounds.
Lemma float_callee_save_bound:
forall i r,
In i f.(fn_code) -> In r (regs_of_instr i) ->
index_float_callee_save r < bound_float_callee_save function_bounds.
Lemma int_local_slot_bound:
forall i ofs,
In i f.(fn_code) -> In (Local ofs Tint) (slots_of_instr i) ->
ofs < bound_int_local function_bounds.
Lemma float_local_slot_bound:
forall i ofs,
In i f.(fn_code) -> In (Local ofs Tfloat) (slots_of_instr i) ->
ofs < bound_float_local function_bounds.
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.
Lemma size_arguments_bound:
forall sig ros,
In (Lcall sig ros) f.(fn_code) ->
size_arguments sig <= bound_outgoing function_bounds.
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, In r (regs_of_instr i) ->
mreg_within_bounds function_bounds r.
Lemma slot_is_within_bounds:
forall i, In i f.(fn_code) ->
forall s, In s (slots_of_instr i) -> Lineartyping.slot_valid f s ->
slot_within_bounds f function_bounds s.
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) ->
Lineartyping.wt_instr f i ->
instr_within_bounds f function_bounds i.
Lemma function_is_within_bounds:
Lineartyping.wt_code f f.(fn_code) ->
function_within_bounds f function_bounds.
End BOUNDS.