diff options
| -rw-r--r-- | backend/Bounds.v | 30 | ||||
| -rw-r--r-- | backend/Conventions.v | 17 | ||||
| -rw-r--r-- | backend/Lineartyping.v | 2 | ||||
| -rw-r--r-- | backend/Machabstr.v | 3 | ||||
| -rw-r--r-- | backend/Machconcr.v | 3 | ||||
| -rw-r--r-- | backend/PPCgenproof1.v | 10 | ||||
| -rw-r--r-- | backend/Stacking.v | 6 | ||||
| -rw-r--r-- | backend/Stackingproof.v | 52 |
8 files changed, 65 insertions, 58 deletions
diff --git a/backend/Bounds.v b/backend/Bounds.v index 415a85f..e598245 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -41,7 +41,7 @@ Record bounds : Set := mkbounds { 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 >= 6 + bound_outgoing_pos: bound_outgoing >= 0 }. (** The following predicates define the correctness of a set of bounds @@ -62,7 +62,7 @@ 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 => 14 <= ofs /\ ofs + typesize ty <= bound_outgoing b + | Outgoing ofs ty => 0 <= ofs /\ ofs + typesize ty <= bound_outgoing b | Incoming ofs ty => In (S s) (loc_parameters funct.(fn_sig)) end. @@ -176,26 +176,24 @@ Proof. intros. unfold max_over_regs_of_funct. unfold max_over_instrs. apply max_over_list_pos. Qed. - -Remark Zmax_6: forall x, Zmax 6 x >= 6. -Proof. - intros. apply Zle_ge. apply Zmax_bound_l. omega. -Qed. -Definition function_bounds := +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 6 - (Zmax (max_over_instrs outgoing_space) - (max_over_slots_of_funct outgoing_slot))) + (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) - (Zmax_6 _). + _. +Next Obligation. + apply Zle_ge. eapply Zle_trans. 2: apply Zmax2. + apply Zge_le. apply max_over_slots_of_funct_pos. +Qed. (** We now show the correctness of the inferred bounds. *) @@ -297,8 +295,7 @@ Lemma outgoing_slot_bound: Proof. intros. change (ofs + typesize ty) with (outgoing_slot (Outgoing ofs ty)). unfold function_bounds, bound_outgoing. - apply Zmax_bound_r. apply Zmax_bound_r. - eapply max_over_slots_of_funct_bound; eauto. + apply Zmax_bound_r. eapply max_over_slots_of_funct_bound; eauto. Qed. Lemma size_arguments_bound: @@ -308,8 +305,7 @@ Lemma size_arguments_bound: Proof. intros. change (size_arguments sig) with (outgoing_space (Lcall sig ros)). unfold function_bounds, bound_outgoing. - apply Zmax_bound_r. apply Zmax_bound_l. - apply max_over_instrs_bound; auto. + apply Zmax_bound_l. apply max_over_instrs_bound; auto. Qed. (** Consequently, all machine registers or stack slots mentioned by one @@ -337,7 +333,7 @@ Proof. split. exact H1. eapply int_local_slot_bound; eauto. split. exact H1. eapply float_local_slot_bound; eauto. exact H1. - split. exact H1. eapply outgoing_slot_bound; eauto. + split. simpl in H1. exact H1. eapply outgoing_slot_bound; eauto. Qed. (** It follows that every instruction in the function is within bounds, diff --git a/backend/Conventions.v b/backend/Conventions.v index 2ab2ca9..a861eb8 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -373,8 +373,7 @@ Qed. integer arguments. - Extra arguments are passed on the stack, in [Outgoing] slots, consecutively assigned (1 word for an integer argument, 2 words for a float), - starting at word offset 6 (the bottom 24 bytes of the stack are reserved - for other purposes). + starting at word offset 0. - Stack space is reserved (as unused [Outgoing] slots) for the arguments that are passed in registers. @@ -411,7 +410,7 @@ Definition float_param_regs := when calling a function with signature [s]. *) Definition loc_arguments (s: signature) : list loc := - loc_arguments_rec s.(sig_args) int_param_regs float_param_regs 14. + loc_arguments_rec s.(sig_args) int_param_regs float_param_regs 8. (** [size_arguments s] returns the number of [Outgoing] slots used to call a function with signature [s]. *) @@ -434,7 +433,7 @@ Fixpoint size_arguments_rec end. Definition size_arguments (s: signature) : Z := - size_arguments_rec s.(sig_args) int_param_regs float_param_regs 14. + size_arguments_rec s.(sig_args) int_param_regs float_param_regs 8. (** A tail-call is possible for a signature if the corresponding arguments are all passed in registers. *) @@ -444,12 +443,12 @@ Definition tailcall_possible (s: signature) : Prop := match l with R _ => True | S _ => False end. (** Argument locations are either non-temporary registers or [Outgoing] - stack slots at offset 14 or more. *) + stack slots at nonnegative offsets. *) Definition loc_argument_acceptable (l: loc) : Prop := match l with | R r => ~(In l temporaries) - | S (Outgoing ofs ty) => ofs >= 14 + | S (Outgoing ofs ty) => ofs >= 0 | _ => False end. @@ -488,7 +487,7 @@ Proof. intro H0; elim H0. simpl. unfold not. ElimOrEq; NotOrEq. simpl. unfold not. ElimOrEq; NotOrEq. destruct s0; try contradiction. - simpl. auto. + simpl. omega. Qed. Hint Resolve loc_arguments_acceptable: locs. @@ -585,9 +584,9 @@ Proof. Qed. Lemma size_arguments_above: - forall s, size_arguments s >= 14. + forall s, size_arguments s >= 0. Proof. - intros; unfold size_arguments. apply Zle_ge. + intros; unfold size_arguments. apply Zle_ge. apply Zle_trans with 8. omega. apply size_arguments_rec_above. Qed. diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 551462c..7dc601f 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -35,7 +35,7 @@ Variable funct: function. Definition slot_valid (s: slot) := match s with | Local ofs ty => 0 <= ofs - | Outgoing ofs ty => 14 <= ofs + | Outgoing ofs ty => 0 <= ofs | Incoming ofs ty => In (S s) (loc_parameters funct.(fn_sig)) end. diff --git a/backend/Machabstr.v b/backend/Machabstr.v index 76e37e8..9ef75ec 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.v @@ -26,6 +26,7 @@ Require Import Op. Require Import Locations. Require Conventions. Require Import Mach. +Require Stacking. (** This file defines the "abstract" semantics for the Mach intermediate language, as opposed to the more concrete @@ -133,7 +134,7 @@ Inductive extcall_arg: regset -> frame -> loc -> val -> Prop := | extcall_arg_reg: forall rs fr r, extcall_arg rs fr (R r) (rs r) | extcall_arg_stack: forall rs fr ofs ty v, - get_slot fr ty (Int.signed (Int.repr (4 * ofs))) v -> + get_slot fr ty (Int.signed (Int.repr (Stacking.fe_ofs_arg + 4 * ofs))) v -> extcall_arg rs fr (S (Outgoing ofs ty)) v. Inductive extcall_args: regset -> frame -> list loc -> list val -> Prop := diff --git a/backend/Machconcr.v b/backend/Machconcr.v index 0cfd8f1..5ca3cad 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.v @@ -25,6 +25,7 @@ Require Import Op. Require Import Locations. Require Conventions. Require Import Mach. +Require Stacking. Require PPCgenretaddr. (** In the concrete semantics for Mach, the three stack-related Mach @@ -69,7 +70,7 @@ Inductive extcall_arg: regset -> mem -> val -> loc -> val -> Prop := | extcall_arg_reg: forall rs m sp r, extcall_arg rs m sp (R r) (rs r) | extcall_arg_stack: forall rs m sp ofs ty v, - load_stack m sp ty (Int.repr (4 * ofs)) = Some v -> + load_stack m sp ty (Int.repr (Stacking.fe_ofs_arg + 4 * ofs)) = Some v -> extcall_arg rs m sp (S (Outgoing ofs ty)) v. Inductive extcall_args: regset -> mem -> val -> list loc -> list val -> Prop := diff --git a/backend/PPCgenproof1.v b/backend/PPCgenproof1.v index 107ea05..d3ecbdd 100644 --- a/backend/PPCgenproof1.v +++ b/backend/PPCgenproof1.v @@ -451,7 +451,7 @@ Lemma extcall_args_match: (forall r, In r iregl -> mreg_type r = Tint) -> (forall r, In r fregl -> mreg_type r = Tfloat) -> Machconcr.extcall_args ms m sp (Conventions.loc_arguments_rec tyl iregl fregl ofs) args -> - PPC.extcall_args rs m tyl (List.map ireg_of iregl) (List.map freg_of fregl) (4 * ofs) args. + PPC.extcall_args rs m tyl (List.map ireg_of iregl) (List.map freg_of fregl) (Stacking.fe_ofs_arg + 4 * ofs) args. Proof. induction tyl; intros. inversion H2; constructor. @@ -463,7 +463,7 @@ Proof. constructor. replace (rs GPR1) with sp. assumption. eapply sp_val; eauto. change (@nil ireg) with (ireg_of ## nil). - replace (4 * ofs + 4) with (4 * (ofs + 1)) by omega. + replace (Stacking.fe_ofs_arg + 4 * ofs + 4) with (Stacking.fe_ofs_arg + 4 * (ofs + 1)) by omega. apply IHtyl; auto. (* register *) inversion H2; subst; clear H2. inversion H8; subst; clear H8. @@ -479,13 +479,12 @@ Proof. constructor. replace (rs GPR1) with sp. assumption. eapply sp_val; eauto. change (@nil freg) with (freg_of ## nil). - replace (4 * ofs + 8) with (4 * (ofs + 2)) by omega. + replace (Stacking.fe_ofs_arg + 4 * ofs + 8) with (Stacking.fe_ofs_arg + 4 * (ofs + 2)) by omega. apply IHtyl; auto. (* register *) inversion H2; subst; clear H2. inversion H8; subst; clear H8. simpl map. econstructor. eapply freg_val; eauto. apply H1; simpl; auto. - replace (4 * ofs + 8) with (4 * (ofs + 2)) by omega. rewrite list_map_drop2. apply IHtyl; auto. intros; apply H0. apply list_drop2_incl. auto. @@ -511,7 +510,8 @@ Proof. unfold Machconcr.extcall_arguments, PPC.extcall_arguments; intros. change (extcall_args rs m sg.(sig_args) (List.map ireg_of Conventions.int_param_regs) - (List.map freg_of Conventions.float_param_regs) (4 * 14) args). + (List.map freg_of Conventions.float_param_regs) + (Stacking.fe_ofs_arg + 4 * 8) args). eapply extcall_args_match; eauto. intro; simpl; ElimOrEq; reflexivity. intro; simpl; ElimOrEq; reflexivity. diff --git a/backend/Stacking.v b/backend/Stacking.v index a1310aa..3f08daa 100644 --- a/backend/Stacking.v +++ b/backend/Stacking.v @@ -52,6 +52,8 @@ The [frame_env] compilation environment records the positions of the boundaries between areas in the frame part. *) +Definition fe_ofs_arg := 24. + Record frame_env : Set := mk_frame_env { fe_size: Z; fe_ofs_link: Z; @@ -68,7 +70,7 @@ Record frame_env : Set := mk_frame_env { function. *) Definition make_env (b: bounds) := - let oil := 4 * b.(bound_outgoing) in (* integer locals *) + let oil := 24 + 4 * b.(bound_outgoing) in (* integer locals *) let oics := oil + 4 * b.(bound_int_local) in (* integer callee-saves *) let oendi := oics + 4 * b.(bound_int_callee_save) in let ofl := align oendi 8 in (* float locals *) @@ -95,7 +97,7 @@ Definition offset_of_index (fe: frame_env) (idx: frame_index) := | FI_retaddr => fe.(fe_ofs_retaddr) | FI_local x Tint => fe.(fe_ofs_int_local) + 4 * x | FI_local x Tfloat => fe.(fe_ofs_float_local) + 8 * x - | FI_arg x ty => 4 * x + | FI_arg x ty => fe_ofs_arg + 4 * x | FI_saved_int x => fe.(fe_ofs_int_callee_save) + 4 * x | FI_saved_float x => fe.(fe_ofs_float_callee_save) + 8 * x end. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index fc2b63a..1759d7f 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -188,7 +188,7 @@ Definition index_valid (idx: frame_index) := | FI_retaddr => True | FI_local x Tint => 0 <= x < b.(bound_int_local) | FI_local x Tfloat => 0 <= x < b.(bound_float_local) - | FI_arg x ty => 14 <= x /\ x + typesize ty <= b.(bound_outgoing) + | FI_arg x ty => 0 <= x /\ x + typesize ty <= b.(bound_outgoing) | FI_saved_int x => 0 <= x < b.(bound_int_callee_save) | FI_saved_float x => 0 <= x < b.(bound_float_callee_save) end. @@ -220,8 +220,8 @@ Definition index_diff (idx1 idx2: frame_index) : Prop := end. Remark align_float_part: - 4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b <= - align (4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b) 8. + 24 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b <= + align (24 + 4 * bound_outgoing b + 4 * bound_int_local b + 4 * bound_int_callee_save b) 8. Proof. apply align_le. omega. Qed. @@ -256,7 +256,7 @@ Proof. unfold offset_of_index, fe, make_env, fe_size, fe_ofs_int_local, fe_ofs_int_callee_save, fe_ofs_float_local, fe_ofs_float_callee_save, - fe_ofs_link, fe_ofs_retaddr, + fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg, type_of_index, typesize; simpl in H5; simpl in H6; simpl in H7; try omega. @@ -322,7 +322,7 @@ Proof. unfold offset_of_index, fe, make_env, fe_size, fe_ofs_int_local, fe_ofs_int_callee_save, fe_ofs_float_local, fe_ofs_float_callee_save, - fe_ofs_link, fe_ofs_retaddr, + fe_ofs_link, fe_ofs_retaddr, fe_ofs_arg, type_of_index, typesize; simpl in H5; omega. @@ -435,7 +435,8 @@ Proof. destruct (orb_prop _ _ H0). apply Loc.overlap_aux_true_1. auto. apply Loc.overlap_aux_true_2. auto. unfold update. - destruct (zeq (4 * ofs1 - fn_framesize tf) (4 * ofs2 - fn_framesize tf)). + destruct (zeq (fe_ofs_arg + 4 * ofs1 - fn_framesize tf) + (fe_ofs_arg + 4 * ofs2 - fn_framesize tf)). destruct (typ_eq ty1 ty2). elim H. decEq. decEq. omega. auto. auto. @@ -443,6 +444,12 @@ Proof. rewrite zle_false. apply zle_false. omega. omega. Qed. +(** Accessing stack-based arguments in the caller's frame. *) + +Definition get_parent_slot (cs: list stackframe) (ofs: Z) (ty: typ) (v: val) : Prop := + get_slot (parent_function cs) (parent_frame cs) + ty (Int.signed (Int.repr (fe_ofs_arg + 4 * ofs))) v. + (** * Agreement between location sets and Mach environments *) (** The following [agree] predicate expresses semantic agreement between: @@ -481,8 +488,7 @@ Record agree (ls ls0: locset) (rs: regset) (fr: frame) (cs: list stackframe): Pr agree_incoming: forall ofs ty, In (S (Incoming ofs ty)) (loc_parameters f.(Linear.fn_sig)) -> - get_slot (parent_function cs) (parent_frame cs) - ty (Int.signed (Int.repr (4 * ofs))) (ls (S (Incoming ofs ty))); + get_parent_slot cs ofs ty (ls (S (Incoming ofs ty))); (** The areas of the frame reserved for saving used callee-save registers always contain the values that those registers had @@ -977,8 +983,7 @@ Lemma save_callee_save_correct: (forall r, rs r = ls (R r)) -> (forall ofs ty, In (S (Outgoing ofs ty)) (loc_arguments f.(Linear.fn_sig)) -> - get_slot (parent_function cs) (parent_frame cs) - ty (Int.signed (Int.repr (4 * ofs))) (ls (S (Outgoing ofs ty)))) -> + get_parent_slot cs ofs ty (ls (S (Outgoing ofs ty)))) -> exists fr', star step tge (State stack tf sp (save_callee_save fe k) rs empty_frame m) @@ -1390,21 +1395,20 @@ Qed. Section EXTERNAL_ARGUMENTS. -Variable f: function. +Variable cs: list Machabstr.stackframe. Variable ls: locset. -Variable fr: frame. Variable rs: regset. Variable sg: signature. + Hypothesis AG1: forall r, rs r = ls (R r). Hypothesis AG2: forall (ofs : Z) (ty : typ), In (S (Outgoing ofs ty)) (loc_arguments sg) -> - get_slot f fr ty (Int.signed (Int.repr (4 * ofs))) - (ls (S (Outgoing ofs ty))). + get_parent_slot cs ofs ty (ls (S (Outgoing ofs ty))). Lemma transl_external_arguments_rec: forall locs, incl locs (loc_arguments sg) -> - extcall_args f rs fr locs ls##locs. + extcall_args (parent_function cs) rs (parent_frame cs) locs ls##locs. Proof. induction locs; simpl; intros. constructor. @@ -1414,12 +1418,13 @@ Proof. destruct a; red in H0. rewrite <- AG1. constructor. destruct s; try contradiction. - constructor. apply AG2. auto with coqlib. + constructor. change (get_parent_slot cs z t (ls (S (Outgoing z t)))). +apply AG2. auto with coqlib. apply IHlocs; eauto with coqlib. Qed. Lemma transl_external_arguments: - extcall_arguments f rs fr sg (ls ## (loc_arguments sg)). + extcall_arguments (parent_function cs) rs (parent_frame cs) sg (ls ## (loc_arguments sg)). Proof. unfold extcall_arguments. apply transl_external_arguments_rec. @@ -1481,7 +1486,7 @@ Inductive match_states: Linear.state -> Machabstr.state -> Prop := (AG1: forall r, rs r = ls (R r)) (AG2: forall ofs ty, In (S (Outgoing ofs ty)) (loc_arguments (Linear.funsig f)) -> - get_slot (parent_function ts) (parent_frame ts) ty (Int.signed (Int.repr (4 * ofs))) (ls (S (Outgoing ofs ty)))) + get_parent_slot ts ofs ty (ls (S (Outgoing ofs ty)))) (AG3: agree_callee_save ls (parent_locset s)), match_states (Linear.Callstate s f ls m) (Machabstr.Callstate ts tf rs m) @@ -1521,7 +1526,8 @@ Proof. eapply agree_locals; eauto. (* Lgetstack, incoming *) apply plus_one; apply exec_Mgetparam. - unfold offset_of_index. eapply agree_incoming; eauto. + change (get_parent_slot ts z t (rs (S (Incoming z t)))). + eapply agree_incoming; eauto. (* Lgetstack, outgoing *) apply plus_one; apply exec_Mgetstack. apply get_slot_index. auto. apply index_arg_valid. auto. congruence. congruence. auto. @@ -1589,12 +1595,14 @@ Proof. econstructor; eauto with coqlib. exists rs0; auto. intro. symmetry. eapply agree_reg; eauto. - intros. unfold parent_function, parent_frame. + intros. assert (slot_within_bounds f (function_bounds f) (Outgoing ofs ty)). red. simpl. generalize (loc_arguments_bounded _ _ _ H0). generalize (loc_arguments_acceptable _ _ H0). unfold loc_argument_acceptable. - omega. - change (4 * ofs) with (offset_of_index (make_env (function_bounds f)) (FI_arg ofs ty)). + omega. + unfold get_parent_slot, parent_function, parent_frame. + change (fe_ofs_arg + 4 * ofs) + with (offset_of_index (make_env (function_bounds f)) (FI_arg ofs ty)). apply get_slot_index. auto. apply index_arg_valid. auto. congruence. congruence. auto. eapply agree_outgoing; eauto. simpl. red; auto. |