diff options
Diffstat (limited to 'backend/Bounds.v')
| -rw-r--r-- | backend/Bounds.v | 160 |
1 files changed, 65 insertions, 95 deletions
diff --git a/backend/Bounds.v b/backend/Bounds.v index ef78b2e..bcd2848 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -17,7 +17,6 @@ Require Import AST. Require Import Op. Require Import Locations. Require Import Linear. -Require Import Lineartyping. Require Import Conventions. (** * Resource bounds for a function *) @@ -30,14 +29,12 @@ Require Import Conventions. the activation record. *) Record bounds : Type := mkbounds { - bound_int_local: Z; - bound_float_local: Z; + bound_local: Z; bound_int_callee_save: Z; bound_float_callee_save: Z; bound_outgoing: Z; bound_stack_data: Z; - bound_int_local_pos: bound_int_local >= 0; - bound_float_local_pos: bound_float_local >= 0; + bound_local_pos: bound_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; @@ -47,41 +44,39 @@ Record bounds : Type := mkbounds { (** The following predicates define the correctness of a set of bounds for the code of a function. *) -Section BELOW. +Section WITHIN_BOUNDS. -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)) + index_int_callee_save r < bound_int_callee_save b + /\ index_float_callee_save r < bound_float_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 s r => slot_within_bounds s /\ mreg_within_bounds r - | Lsetstack r s => slot_within_bounds s + | 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 => mreg_within_bounds res - | Lannot ef args => forall s, In (S s) args -> slot_within_bounds s + | Lbuiltin ef args res => + forall r, In r res \/ In r (destroyed_by_builtin ef) -> mreg_within_bounds r + | Lannot ef args => + forall sl ofs ty, In (S sl ofs ty) args -> slot_within_bounds sl ofs ty | _ => True end. -End BELOW. +End WITHIN_BOUNDS. Definition function_within_bounds (f: function) (b: bounds) : Prop := - forall instr, In instr f.(fn_code) -> instr_within_bounds f b instr. + forall instr, In instr f.(fn_code) -> instr_within_bounds b instr. (** * Inference of resource bounds for a function *) @@ -99,14 +94,14 @@ Variable f: function. Definition regs_of_instr (i: instruction) : list mreg := match i with - | Lgetstack s r => r :: nil - | Lsetstack r s => r :: nil + | Lgetstack sl ofs ty r => r :: nil + | Lsetstack r sl ofs ty => 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 - | Lbuiltin ef args res => res :: nil + | Lbuiltin ef args res => res ++ destroyed_by_builtin ef | Lannot ef args => nil | Llabel lbl => nil | Lgoto lbl => nil @@ -115,58 +110,55 @@ Definition regs_of_instr (i: instruction) : list mreg := | Lreturn => nil end. -Fixpoint slots_of_locs (l: list loc) : list slot := +Fixpoint slots_of_locs (l: list loc) : list (slot * Z * typ) := match l with | nil => nil - | S s :: l' => s :: slots_of_locs l' + | 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 := +Definition slots_of_instr (i: instruction) : list (slot * Z * typ) := match i with - | Lgetstack s r => s :: nil - | Lsetstack r s => s :: nil + | Lgetstack sl ofs ty r => (sl, ofs, ty) :: nil + | Lsetstack r sl ofs ty => (sl, ofs, ty) :: nil | Lannot ef args => slots_of_locs args | _ => nil end. -Definition max_over_list (A: Type) (valu: A -> Z) (l: list A) : Z := +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). + max_over_list 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). + max_over_list 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_slots_of_instr (valu: slot * Z * typ -> Z) (i: instruction) : Z := + max_over_list 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 := +Definition max_over_slots_of_funct (valu: slot * Z * typ -> 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 local_slot (s: slot * Z * typ) := + match s with (Local, ofs, ty) => ofs + typesize ty | _ => 0 end. -Definition outgoing_slot (s: slot) := - match s with Outgoing 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 A valu l >= 0. + max_over_list valu l >= 0. Proof. intros until valu. unfold max_over_list. assert (forall l z, fold_left (fun x y => Zmax x (valu y)) l z >= z). @@ -176,7 +168,7 @@ Proof. Qed. Lemma max_over_slots_of_funct_pos: - forall (valu: slot -> Z), max_over_slots_of_funct valu >= 0. + forall (valu: slot * Z * typ -> Z), max_over_slots_of_funct valu >= 0. Proof. intros. unfold max_over_slots_of_funct. unfold max_over_instrs. apply max_over_list_pos. @@ -188,18 +180,16 @@ Proof. intros. unfold max_over_regs_of_funct. unfold max_over_instrs. apply max_over_list_pos. Qed. - + Program Definition function_bounds := mkbounds - (max_over_slots_of_funct int_local) - (max_over_slots_of_funct float_local) + (max_over_slots_of_funct local_slot) (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)) (Zmax f.(fn_stacksize) 0) - (max_over_slots_of_funct_pos int_local) - (max_over_slots_of_funct_pos float_local) + (max_over_slots_of_funct_pos local_slot) (max_over_regs_of_funct_pos int_callee_save) (max_over_regs_of_funct_pos float_callee_save) _ _. @@ -215,7 +205,7 @@ Qed. 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. + In x l -> valu x <= max_over_list valu l. Proof. intros until x. unfold max_over_list. assert (forall c z, @@ -250,7 +240,7 @@ Proof. Qed. Lemma max_over_slots_of_funct_bound: - forall (valu: slot -> Z) i s, + 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. @@ -282,34 +272,23 @@ Proof. eapply max_over_regs_of_funct_bound; eauto. Qed. -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. -Proof. - intros. apply Zlt_le_trans with (int_local (Local ofs Tint)). - unfold int_local. omega. - unfold function_bounds, bound_int_local. - eapply max_over_slots_of_funct_bound; eauto. -Qed. - -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 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. - intros. apply Zlt_le_trans with (float_local (Local ofs Tfloat)). - unfold float_local. omega. - unfold function_bounds, bound_float_local. + intros. + unfold function_bounds, bound_local. + change (ofs + typesize ty) with (local_slot (Local, ofs, ty)). eapply max_over_slots_of_funct_bound; eauto. Qed. Lemma outgoing_slot_bound: forall i ofs ty, - In i f.(fn_code) -> In (Outgoing ofs ty) (slots_of_instr i) -> + In i f.(fn_code) -> In (Outgoing, ofs, ty) (slots_of_instr i) -> ofs + typesize ty <= bound_outgoing function_bounds. Proof. - intros. change (ofs + typesize ty) with (outgoing_slot (Outgoing ofs ty)). + 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. Qed. @@ -332,28 +311,25 @@ Lemma mreg_is_within_bounds: forall r, In r (regs_of_instr i) -> mreg_within_bounds function_bounds r. Proof. - intros. unfold mreg_within_bounds. - case (mreg_type r). + intros. unfold mreg_within_bounds. split. eapply int_callee_save_bound; eauto. eapply float_callee_save_bound; eauto. Qed. 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. + forall sl ty ofs, In (sl, ofs, ty) (slots_of_instr i) -> + slot_within_bounds function_bounds sl ofs ty. Proof. intros. unfold slot_within_bounds. - destruct s. - destruct t. - split. exact H1. eapply int_local_slot_bound; eauto. - split. exact H1. eapply float_local_slot_bound; eauto. - exact H1. - split. simpl in H1. exact H1. eapply outgoing_slot_bound; eauto. + destruct sl. + eapply local_slot_bound; eauto. + auto. + eapply outgoing_slot_bound; eauto. Qed. Lemma slots_of_locs_charact: - forall s l, In s (slots_of_locs l) <-> In (S s) l. + 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. @@ -366,27 +342,21 @@ Qed. Lemma instr_is_within_bounds: forall i, In i f.(fn_code) -> - Lineartyping.wt_instr f i -> - instr_within_bounds f function_bounds i. + instr_within_bounds function_bounds i. Proof. intros; destruct i; generalize (mreg_is_within_bounds _ H); generalize (slot_is_within_bounds _ H); simpl; intros; auto. -(* getstack *) - inv H0. split; auto. -(* setstack *) - inv H0; auto. (* call *) eapply size_arguments_bound; eauto. +(* builtin *) + apply H1. apply in_or_app; auto. (* annot *) - inv H0. apply H1. rewrite slots_of_locs_charact; auto. - generalize (H8 _ H3). unfold loc_acceptable, slot_valid. - destruct s; (contradiction || omega). + apply H0. rewrite slots_of_locs_charact; auto. Qed. Lemma function_is_within_bounds: - Lineartyping.wt_code f f.(fn_code) -> function_within_bounds f function_bounds. Proof. intros; red; intros. apply instr_is_within_bounds; auto. |