From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Aug 2007 07:27:50 +0000 Subject: Fusion des modifications faites sur les branches "tailcalls" et "smallstep". En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Lineartyping.v | 208 +++++++------------------------------------------ 1 file changed, 26 insertions(+), 182 deletions(-) (limited to 'backend/Lineartyping.v') diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index cbe18311..baf522aa 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -1,4 +1,4 @@ -(** Typing rules and computation of stack bounds for Linear. *) +(** Typing rules for Linear. *) Require Import Coqlib. Require Import Maps. @@ -9,218 +9,55 @@ Require Import Locations. Require Import Linear. Require Import Conventions. -(** * 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. *) - -Record bounds : Set := mkbounds { - bound_int_local: Z; - bound_float_local: Z; - bound_int_callee_save: Z; - bound_float_callee_save: Z; - bound_outgoing: Z -}. - -(** The resource bounds for a function are computed by a linear scan - of its instructions. *) - -Section BOUNDS. - -Variable f: function. - -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 :: args - | Lload chunk addr args dst => dst :: args - | Lstore chunk addr args src => src :: args - | Lcall sig (inl fn) => fn :: nil - | Lcall sig (inr _) => nil - | Lalloc => nil - | Llabel lbl => nil - | Lgoto lbl => nil - | Lcond cond args lbl => args - | 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: Set) (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. - -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 6 - (Zmax (max_over_instrs outgoing_space) - (max_over_slots_of_funct outgoing_slot))). - -(** We show that bounds computed by [function_bounds] are all positive - or null, and moreover [bound_outgoing] is greater or equal to 6. - These properties are used later to reason about the layout of - the activation record. *) - -Lemma max_over_list_pos: - forall (A: Set) (valu: A -> Z) (l: list A), - max_over_list A 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). - induction l; simpl; intros. - omega. apply Zge_trans with (Zmax z (valu a)). - auto. apply Zle_ge. apply Zmax1. auto. -Qed. - -Lemma max_over_slots_of_funct_pos: - forall (valu: slot -> 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. -Qed. - -Lemma max_over_regs_of_funct_pos: - forall (valu: mreg -> Z), max_over_regs_of_funct valu >= 0. -Proof. - intros. unfold max_over_regs_of_funct. - unfold max_over_instrs. apply max_over_list_pos. -Qed. - -Lemma bound_int_local_pos: - bound_int_local function_bounds >= 0. -Proof. - simpl. apply max_over_slots_of_funct_pos. -Qed. - -Lemma bound_float_local_pos: - bound_float_local function_bounds >= 0. -Proof. - simpl. apply max_over_slots_of_funct_pos. -Qed. - -Lemma bound_int_callee_save_pos: - bound_int_callee_save function_bounds >= 0. -Proof. - simpl. apply max_over_regs_of_funct_pos. -Qed. - -Lemma bound_float_callee_save_pos: - bound_float_callee_save function_bounds >= 0. -Proof. - simpl. apply max_over_regs_of_funct_pos. -Qed. - -Lemma bound_outgoing_pos: - bound_outgoing function_bounds >= 6. -Proof. - simpl. apply Zle_ge. apply Zmax_bound_l. omega. -Qed. - -End BOUNDS. - -(** * Typing rules for Linear *) - -(** The typing rules for Linear are similar to those for LTL: we check +(** The typing rules for Linear are similar to those for LTLin: we check that instructions receive the right number of arguments, and that the types of the argument and result registers agree - with what the instruction expects. Moreover, we state that references - to callee-save registers and to stack slots are within the bounds - computed by [function_bounds]. This is true by construction of - [function_bounds], and is proved in [Linearizetyping], but it - is convenient to integrate this property within the typing judgement. -*) + with what the instruction expects. Moreover, we also + enforces some correctness conditions on the offsets of stack slots + accessed through [Lgetstack] and [Lsetstack] Linear instructions. *) Section WT_INSTR. Variable funct: function. -Let b := function_bounds funct. -Definition mreg_bounded (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 +Definition slot_valid (s: slot) := + match s with + | Local ofs ty => 0 <= ofs + | Outgoing ofs ty => 14 <= ofs + | Incoming ofs ty => 14 <= ofs /\ ofs + typesize ty <= size_arguments funct.(fn_sig) end. -Definition slot_bounded (s: slot) := +Definition slot_writable (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 => 6 <= ofs /\ ofs + typesize ty <= bound_outgoing b - | Incoming ofs ty => 6 <= ofs /\ ofs + typesize ty <= size_arguments funct.(fn_sig) + | Local ofs ty => True + | Outgoing ofs ty => True + | Incoming ofs ty => False end. Inductive wt_instr : instruction -> Prop := | wt_Lgetstack: forall s r, slot_type s = mreg_type r -> - slot_bounded s -> mreg_bounded r -> + slot_valid s -> wt_instr (Lgetstack s r) | wt_Lsetstack: forall s r, - match s with Incoming _ _ => False | _ => True end -> slot_type s = mreg_type r -> - slot_bounded s -> + slot_valid s -> slot_writable s -> wt_instr (Lsetstack r s) | wt_Lopmove: forall r1 r, mreg_type r1 = mreg_type r -> - mreg_bounded r -> wt_instr (Lop Omove (r1 :: nil) r) - | wt_Lopundef: - forall r, - mreg_bounded r -> - wt_instr (Lop Oundef nil r) | wt_Lop: forall op args res, - op <> Omove -> op <> Oundef -> + op <> Omove -> (List.map mreg_type args, mreg_type res) = type_of_operation op -> - mreg_bounded res -> wt_instr (Lop op args res) | wt_Lload: forall chunk addr args dst, List.map mreg_type args = type_of_addressing addr -> mreg_type dst = type_of_chunk chunk -> - mreg_bounded dst -> wt_instr (Lload chunk addr args dst) | wt_Lstore: forall chunk addr args src, @@ -229,9 +66,13 @@ Inductive wt_instr : instruction -> Prop := wt_instr (Lstore chunk addr args src) | wt_Lcall: forall sig ros, - size_arguments sig <= bound_outgoing b -> match ros with inl r => mreg_type r = Tint | _ => True end -> wt_instr (Lcall sig ros) + | wt_Ltailcall: + forall sig ros, + tailcall_possible sig -> + match ros with inl r => r = IT3 | _ => True end -> + wt_instr (Ltailcall sig ros) | wt_Lalloc: wt_instr Lalloc | wt_Llabel: @@ -249,8 +90,11 @@ Inductive wt_instr : instruction -> Prop := End WT_INSTR. +Definition wt_code (f: function) (c: code) : Prop := + forall instr, In instr c -> wt_instr f instr. + Definition wt_function (f: function) : Prop := - forall instr, In instr f.(fn_code) -> wt_instr f instr. + wt_code f f.(fn_code). Inductive wt_fundef: fundef -> Prop := | wt_fundef_external: forall ef, -- cgit