Library compcert.backend.Bounds

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.
The following predicates define the correctness of a set of bounds for the code of a function.


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
  | Localofs + typesize ty bound_local b
  | Outgoingofs + typesize ty bound_outgoing b
  | IncomingTrue

Definition instr_within_bounds (i: instruction) :=
  match i with
  | Lgetstack sl ofs ty rslot_within_bounds sl ofs ty mreg_within_bounds r
  | Lsetstack r sl ofs tyslot_within_bounds sl ofs ty
  | Lop op args resmreg_within_bounds res
  | Lload chunk addr args dstmreg_within_bounds dst
  | Lcall sig rossize_arguments sig bound_outgoing b
  | Lbuiltin ef args res
       ( r, In r (params_of_builtin_res res) In r (destroyed_by_builtin ef) mreg_within_bounds r)
     ( sl ofs ty, In (S sl ofs ty) (params_of_builtin_args args) slot_within_bounds sl ofs ty)
  | _True


Definition function_within_bounds (f: function) (b: bounds) : Prop :=
   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 rrecord_reg u r
  | Lsetstack r sl ofs tyrecord_reg u r
  | Lop op args resrecord_reg u res
  | Lload chunk addr args dstrecord_reg u dst
  | Lstore chunk addr args srcu
  | Lcall sig rosu
  | Ltailcall sig rosu
  | Lbuiltin ef args res
      record_regs (record_regs u (params_of_builtin_res res)) (destroyed_by_builtin ef)
  | Llabel lblu
  | Lgoto lblu
  | Lcond cond args lblu
  | Ljumptable arg tblu
  | Lreturnu

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
  | nilnil
  | S sl ofs ty :: l'(sl, ofs, ty) :: slots_of_locs l'
  | R r :: l'slots_of_locs l'

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 resslots_of_locs (params_of_builtin_args args)
  | _nil

Definition max_over_list {A: Type} (valu: A Z) (l: list A) : Z :=
  List.fold_left (fun m lZmax 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:
   (A: Type) (valu: A Z) (l: list A),
  max_over_list valu l 0.
  intros until valu. unfold max_over_list.
  assert ( l z, fold_left (fun x yZmax x (valu y)) l z z).
  induction l; simpl; intros.
  omega. apply Zge_trans with (Zmax z (valu a)).
  auto. apply Zle_ge. apply Zmax1. auto.

Lemma max_over_slots_of_funct_pos:
   (valu: slot × Z × typ Z), max_over_slots_of_funct valu 0.
  intros. unfold max_over_slots_of_funct.
  unfold max_over_instrs. apply max_over_list_pos.

Remark fold_left_preserves:
   (A B: Type) (f: A B A) (P: A Prop),
  ( a b, P a P (f a b))
   l a, P a P (fold_left f l a).
  induction l; simpl; auto.

Remark fold_left_ensures:
   (A B: Type) (f: A B A) (P: A Prop) b0,
  ( a b, P a P (f a b))
  ( a, P (f a b0))
   l a, In b0 l P (fold_left f l a).
  induction l; simpl; intros. contradiction.
  destruct H1. subst a. apply fold_left_preserves; auto. apply IHl; auto.

Definition only_callee_saves (u: RegSet.t) : Prop :=
   r, RegSet.In r u is_callee_save r = true.

Lemma record_reg_only: u r, only_callee_saves u only_callee_saves (record_reg u r).
  unfold only_callee_saves, record_reg; intros.
  destruct (is_callee_save r) eqn:CS; auto.
  destruct (mreg_eq r r0). congruence. apply H; eapply RegSet.add_3; eauto.

Lemma record_regs_only: rl u, only_callee_saves u only_callee_saves (record_regs u rl).
  intros. unfold record_regs. apply fold_left_preserves; auto using record_reg_only.

Lemma record_regs_of_instr_only: u i, only_callee_saves u only_callee_saves (record_regs_of_instr u i).
  intros. destruct i; simpl; auto using record_reg_only, record_regs_only.

Lemma record_regs_of_function_only:
  only_callee_saves record_regs_of_function.
  intros. unfold record_regs_of_function.
  apply fold_left_preserves. apply record_regs_of_instr_only.
  red; intros. eelim RegSet.empty_1; eauto.

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.
  apply max_over_slots_of_funct_pos.
Next Obligation.
  apply Zle_ge. eapply Zle_trans. 2: apply Zmax2.
  apply Zge_le. apply max_over_slots_of_funct_pos.
Next Obligation.
  apply Zle_ge. apply Zmax2.
Next Obligation.
  generalize (RegSet.elements_3w record_regs_of_function).
  generalize (RegSet.elements record_regs_of_function).
  induction 1. constructor. constructor; auto.
  red; intros; elim H. apply InA_alt. x; auto.
Next Obligation.
  apply record_regs_of_function_only. apply RegSet.elements_2.
  apply InA_alt. r; auto.

We now show the correctness of the inferred bounds.

Lemma record_reg_incr: u r r', RegSet.In r' u RegSet.In r' (record_reg u r).
  unfold record_reg; intros. destruct (is_callee_save r); auto. apply RegSet.add_2; auto.

Lemma record_reg_ok: u r, is_callee_save r = true RegSet.In r (record_reg u r).
  unfold record_reg; intros. rewrite H. apply RegSet.add_1; auto.

Lemma record_regs_incr: r' rl u, RegSet.In r' u RegSet.In r' (record_regs u rl).
  intros. unfold record_regs. apply fold_left_preserves; auto using record_reg_incr.

Lemma record_regs_ok: r rl u, In r rl is_callee_save r = true RegSet.In r (record_regs u rl).
  intros. unfold record_regs. eapply fold_left_ensures; eauto using record_reg_incr, record_reg_ok.

Lemma record_regs_of_instr_incr: r' u i, RegSet.In r' u RegSet.In r' (record_regs_of_instr u i).
  intros. destruct i; simpl; auto using record_reg_incr, record_regs_incr.

Definition defined_by_instr (r': mreg) (i: instruction) :=
  match i with
  | Lgetstack sl ofs ty rr' = r
  | Lop op args resr' = res
  | Lload chunk addr args dstr' = dst
  | Lbuiltin ef args resIn r' (params_of_builtin_res res) In r' (destroyed_by_builtin ef)
  | _False

Lemma record_regs_of_instr_ok: r' u i, defined_by_instr r' i is_callee_save r' = true RegSet.In r' (record_regs_of_instr u i).
  intros. destruct i; simpl in *; try contradiction; subst; auto using record_reg_ok.
  destruct H; auto using record_regs_incr, record_regs_ok.

Lemma record_regs_of_function_ok:
   r i, In i f.(fn_code) defined_by_instr r i is_callee_save r = true RegSet.In r record_regs_of_function.
  intros. unfold record_regs_of_function.
  eapply fold_left_ensures; eauto using record_regs_of_instr_incr, record_regs_of_instr_ok.

Lemma max_over_list_bound:
   (A: Type) (valu: A Z) (l: list A) (x: A),
  In x l valu x max_over_list valu l.
  intros until x. unfold max_over_list.
  assert ( c z,
            let f := fold_left (fun x yZmax 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.

Lemma max_over_instrs_bound:
   (valu: instruction Z) i,
  In i f.(fn_code) valu i max_over_instrs valu.
  intros. unfold max_over_instrs. apply max_over_list_bound; auto.

Lemma max_over_slots_of_funct_bound:
   (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.
  intros. unfold max_over_slots_of_funct.
  apply Zle_trans with (max_over_slots_of_instr valu i).
  unfold max_over_slots_of_instr. apply max_over_list_bound. auto.
  apply max_over_instrs_bound. auto.

Lemma local_slot_bound:
   i ofs ty,
  In i f.(fn_code) In (Local, ofs, ty) (slots_of_instr i)
  ofs + typesize ty bound_local function_bounds.
  unfold function_bounds, bound_local.
  change (ofs + typesize ty) with (local_slot (Local, ofs, ty)).
  eapply max_over_slots_of_funct_bound; eauto.

Lemma outgoing_slot_bound:
   i ofs ty,
  In i f.(fn_code) In (Outgoing, ofs, ty) (slots_of_instr i)
  ofs + typesize ty bound_outgoing function_bounds.
  intros. change (ofs + typesize ty) with (outgoing_slot (Outgoing, ofs, ty)).
  unfold function_bounds, bound_outgoing.
  apply Zmax_bound_r. eapply max_over_slots_of_funct_bound; eauto.

Lemma size_arguments_bound:
   sig ros,
  In (Lcall sig ros) f.(fn_code)
  size_arguments sig bound_outgoing function_bounds.
  intros. change (size_arguments sig) with (outgoing_space (Lcall sig ros)).
  unfold function_bounds, bound_outgoing.
  apply Zmax_bound_l. apply max_over_instrs_bound; auto.

Consequently, all machine registers or stack slots mentioned by one of the instructions of function f are within bounds.

Lemma mreg_is_within_bounds:
   i, In i f.(fn_code)
   r, defined_by_instr r i
  mreg_within_bounds function_bounds r.
  intros. unfold mreg_within_bounds. intros.
  exploit record_regs_of_function_ok; eauto. intros.
  apply RegSet.elements_1 in H2. rewrite InA_alt in H2. destruct H2 as (r' & A & B).
  subst r'; auto.

Lemma slot_is_within_bounds:
   i, In i f.(fn_code)
   sl ty ofs, In (sl, ofs, ty) (slots_of_instr i)
  slot_within_bounds function_bounds sl ofs ty.
  intros. unfold slot_within_bounds.
  destruct sl.
  eapply local_slot_bound; eauto.
  eapply outgoing_slot_bound; eauto.

Lemma slots_of_locs_charact:
   sl ofs ty l, In (sl, ofs, ty) (slots_of_locs l) In (S sl ofs ty) l.
  induction l; simpl; intros.
  destruct a; simpl; intuition congruence.

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:
  In i f.(fn_code)
  instr_within_bounds function_bounds i.
  destruct i;
  generalize (mreg_is_within_bounds _ H); generalize (slot_is_within_bounds _ H);
  simpl; intros; auto.
  eapply size_arguments_bound; eauto.
  split; intros.
  apply H1; auto.
  apply H0. rewrite slots_of_locs_charact; auto.

Lemma function_is_within_bounds:
  function_within_bounds f function_bounds.
  intros; red; intros. apply instr_is_within_bounds; auto.


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
  | nilofs
  | r :: l
      let ty := mreg_type r in
      let sz := AST.typesize ty in
      size_callee_save_area_rec l (align ofs sz + sz)

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:
   l ofs, ofs size_callee_save_area_rec l ofs.
Local Opaque mreg_type.
  induction l as [ | r l]; intros; simpl.
- omega.
- eapply Zle_trans. 2: apply IHl.
  generalize (AST.typesize_pos (mreg_type r)); intros.
  apply Zle_trans with (align ofs (AST.typesize (mreg_type r))).
  apply align_le; auto.

Lemma size_callee_save_area_incr:
   b ofs, ofs size_callee_save_area b ofs.
  intros. apply size_callee_save_area_rec_incr.

Layout of the stack frame and its properties. These definitions are used in the machine-dependent Stacklayout module and in the Stacking pass.