From fc1b2bfea598354a3e939de35d270376c880e1b0 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 17 Aug 2017 11:46:29 +0200 Subject: ARM: tweak stack layout so that back link and return address are lower This reduces the chances that back link and return address cannot be saved by a single str instruction. We generate correct code for the overflow case, but the code isn't very efficient, so let's make it uncommon. --- arm/Stacklayout.v | 71 ++++++++++++++++++++++++++----------------------------- 1 file changed, 34 insertions(+), 37 deletions(-) (limited to 'arm/Stacklayout.v') diff --git a/arm/Stacklayout.v b/arm/Stacklayout.v index c867ba59..043393bf 100644 --- a/arm/Stacklayout.v +++ b/arm/Stacklayout.v @@ -19,11 +19,10 @@ Require Import Bounds. (** The general shape of activation records is as follows, from bottom (lowest offsets) to top: - Space for outgoing arguments to function calls. -- Local stack slots. -- Saved values of integer callee-save registers used by the function. -- Saved values of float callee-save registers used by the function. -- Saved return address into caller. - Pointer to activation record of the caller. +- Saved return address into caller. +- Local stack slots. +- Saved values of callee-save registers used by the function. - Space for the stack-allocated data declared in Cminor. The [frame_env] compilation environment records the positions of @@ -36,11 +35,11 @@ Definition fe_ofs_arg := 0. function. *) Definition make_env (b: bounds) := - let ol := align (4 * b.(bound_outgoing)) 8 in (* locals *) + let olink := 4 * b.(bound_outgoing) in (* back link*) + let ora := olink + 4 in (* return address *) + let ol := align (ora + 4) 8 in (* locals *) let ocs := ol + 4 * b.(bound_local) in (* callee-saves *) - let ora := align (size_callee_save_area b ocs) 4 in (* retaddr *) - let olink := ora + 4 in (* back link *) - let ostkdata := align (olink + 4) 8 in (* stack data *) + let ostkdata := align (size_callee_save_area b ocs) 8 in (* retaddr *) let sz := align (ostkdata + b.(bound_stack_data)) 8 in {| fe_size := sz; fe_ofs_link := olink; @@ -67,33 +66,32 @@ Lemma frame_env_separated: Proof. Local Opaque Z.add Z.mul sepconj range. intros; simpl. - set (ol := align (4 * b.(bound_outgoing)) 8); + set (olink := 4 * b.(bound_outgoing)); + set (ora := olink + 4); + set (ol := align (ora + 4) 8); set (ocs := ol + 4 * b.(bound_local)); - set (ora := align (size_callee_save_area b ocs) 4); - set (olink := ora + 4); - set (ostkdata := align (olink + 4) 8). + set (ostkdata := align (size_callee_save_area b ocs) 8). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (4 * b.(bound_outgoing) <= ol) by (apply align_le; omega). + assert (0 <= olink) by (unfold olink; omega). + assert (olink <= ora) by (unfold ora; omega). + assert (ora + 4 <= ol) by (apply align_le; omega). assert (ol + 4 * b.(bound_local) <= ocs) by (unfold ocs; omega). assert (ocs <= size_callee_save_area b ocs) by apply size_callee_save_area_incr. - assert (size_callee_save_area b ocs <= ora) by (apply align_le; omega). - assert (ora <= olink) by (unfold olink; omega). - assert (olink + 4 <= ostkdata) by (apply align_le; omega). + assert (size_callee_save_area b ocs <= ostkdata) by (apply align_le; omega). (* Reorder as: outgoing - local - callee-save + back link retaddr - back link *) + local + callee-save *) rewrite sep_swap12. - rewrite sep_swap45. + rewrite sep_swap23. rewrite sep_swap34. - rewrite sep_swap45. (* Apply range_split and range_split2 repeatedly *) unfold fe_ofs_arg. - apply range_split_2. fold ol; omega. omega. apply range_split. omega. - apply range_split_2. fold ora; omega. omega. + apply range_split. omega. + apply range_split_2. fold ol; omega. omega. apply range_split. omega. apply range_drop_right with ostkdata. omega. eapply sep_drop2. eexact H. @@ -105,18 +103,18 @@ Lemma frame_env_range: 0 <= fe_stack_data fe /\ fe_stack_data fe + bound_stack_data b <= fe_size fe. Proof. intros; simpl. - set (ol := align (4 * b.(bound_outgoing)) 8); + set (olink := 4 * b.(bound_outgoing)); + set (ora := olink + 4); + set (ol := align (ora + 4) 8); set (ocs := ol + 4 * b.(bound_local)); - set (ora := align (size_callee_save_area b ocs) 4); - set (olink := ora + 4); - set (ostkdata := align (olink + 4) 8). + set (ostkdata := align (size_callee_save_area b ocs) 8). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (4 * b.(bound_outgoing) <= ol) by (apply align_le; omega). + assert (0 <= olink) by (unfold olink; omega). + assert (olink <= ora) by (unfold ora; omega). + assert (ora + 4 <= ol) by (apply align_le; omega). assert (ol + 4 * b.(bound_local) <= ocs) by (unfold ocs; omega). assert (ocs <= size_callee_save_area b ocs) by apply size_callee_save_area_incr. - assert (size_callee_save_area b ocs <= ora) by (apply align_le; omega). - assert (ora <= olink) by (unfold olink; omega). - assert (olink + 4 <= ostkdata) by (apply align_le; omega). + assert (size_callee_save_area b ocs <= ostkdata) by (apply align_le; omega). split. omega. apply align_le; omega. Qed. @@ -130,14 +128,13 @@ Lemma frame_env_aligned: /\ (4 | fe_ofs_retaddr fe). Proof. intros; simpl. - set (ol := align (4 * b.(bound_outgoing)) 8); + set (olink := 4 * b.(bound_outgoing)); + set (ora := olink + 4); + set (ol := align (ora + 4) 8); set (ocs := ol + 4 * b.(bound_local)); - set (ora := align (size_callee_save_area b ocs) 4); - set (olink := ora + 4); - set (ostkdata := align (olink + 4) 8). + set (ostkdata := align (size_callee_save_area b ocs) 8). split. apply Zdivide_0. split. apply align_divides; omega. split. apply align_divides; omega. - split. apply Z.divide_add_r. apply align_divides; omega. apply Z.divide_refl. - apply align_divides; omega. + unfold ora, olink; auto using Z.divide_mul_l, Z.divide_add_r, Z.divide_refl. Qed. -- cgit