diff options
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Conventions1.v | 218 | ||||
| -rw-r--r-- | powerpc/Machregs.v | 31 | ||||
| -rw-r--r-- | powerpc/Stacklayout.v | 171 |
3 files changed, 152 insertions, 268 deletions
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 4ee25a32..e78395bf 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -14,6 +14,7 @@ machine registers and stack slots. *) Require Import Coqlib. +Require Import Decidableplus. Require Import AST. Require Import Events. Require Import Locations. @@ -29,6 +30,17 @@ Require Import Locations. of callee- and caller-save registers. *) +Definition is_callee_save (r: mreg): bool := + match r with + | R3 | R4 | R5 | R6 | R7 | R8 | R9 | R10 | R11 | R12 => false + | R14 | R15 | R16 | R17 | R18 | R19 | R20 | R21 | R22 | R23 | R24 + | R25 | R26 | R27 | R28 | R29 | R30 | R31 => true + | F0 | F1 | F2 | F3 | F4 | F5 | F6 | F7 + | F8 | F9 | F10 | F11 | F12 | F13 => false + | F14 | F15 | F16 | F17 | F18 | F19 | F20 | F21 | F22 | F23 + | F24 | F25 | F26 | F27 | F28 | F29 | F30 | F31 => true + end. + Definition int_caller_save_regs := R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: R11 :: R12 :: nil. @@ -44,174 +56,11 @@ Definition float_callee_save_regs := F22 :: F21 :: F20 :: F19 :: F18 :: F17 :: F16 :: F15 :: F14 :: nil. Definition destroyed_at_call := - int_caller_save_regs ++ float_caller_save_regs. + List.filter (fun r => negb (is_callee_save r)) all_mregs. Definition dummy_int_reg := R3. (**r Used in [Coloring]. *) Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) -(** The [index_int_callee_save] and [index_float_callee_save] associate - a unique positive integer to callee-save registers. This integer is - used in [Stacking] to determine where to save these registers in - the activation record if they are used by the current function. *) - -Definition index_int_callee_save (r: mreg) := - match r with - | R14 => 17 | R15 => 16 | R16 => 15 | R17 => 14 - | R18 => 13 | R19 => 12 | R20 => 11 | R21 => 10 - | R22 => 9 | R23 => 8 | R24 => 7 | R25 => 6 - | R26 => 5 | R27 => 4 | R28 => 3 | R29 => 2 - | R30 => 1 | R31 => 0 | _ => -1 - end. - -Definition index_float_callee_save (r: mreg) := - match r with - | F14 => 17 | F15 => 16 | F16 => 15 | F17 => 14 - | F18 => 13 | F19 => 12 | F20 => 11 | F21 => 10 - | F22 => 9 | F23 => 8 | F24 => 7 | F25 => 6 - | F26 => 5 | F27 => 4 | F28 => 3 | F29 => 2 - | F30 => 1 | F31 => 0 | _ => -1 - end. - -Ltac ElimOrEq := - match goal with - | |- (?x = ?y) \/ _ -> _ => - let H := fresh in - (intro H; elim H; clear H; - [intro H; rewrite <- H; clear H | ElimOrEq]) - | |- False -> _ => - let H := fresh in (intro H; contradiction) - end. - -Ltac OrEq := - match goal with - | |- (?x = ?x) \/ _ => left; reflexivity - | |- (?x = ?y) \/ _ => right; OrEq - | |- False => fail - end. - -Ltac NotOrEq := - match goal with - | |- (?x = ?y) \/ _ -> False => - let H := fresh in ( - intro H; elim H; clear H; [intro; discriminate | NotOrEq]) - | |- False -> False => - contradiction - end. - -Lemma index_int_callee_save_pos: - forall r, In r int_callee_save_regs -> index_int_callee_save r >= 0. -Proof. - intro r. simpl; ElimOrEq; unfold index_int_callee_save; omega. -Qed. - -Lemma index_float_callee_save_pos: - forall r, In r float_callee_save_regs -> index_float_callee_save r >= 0. -Proof. - intro r. simpl; ElimOrEq; unfold index_float_callee_save; omega. -Qed. - -Lemma index_int_callee_save_pos2: - forall r, index_int_callee_save r >= 0 -> In r int_callee_save_regs. -Proof. - destruct r; simpl; intro; omegaContradiction || OrEq. -Qed. - -Lemma index_float_callee_save_pos2: - forall r, index_float_callee_save r >= 0 -> In r float_callee_save_regs. -Proof. - destruct r; simpl; intro; omegaContradiction || OrEq. -Qed. - -Lemma index_int_callee_save_inj: - forall r1 r2, - In r1 int_callee_save_regs -> - In r2 int_callee_save_regs -> - r1 <> r2 -> - index_int_callee_save r1 <> index_int_callee_save r2. -Proof. - intros r1 r2. - simpl; ElimOrEq; ElimOrEq; unfold index_int_callee_save; - intros; congruence. -Qed. - -Lemma index_float_callee_save_inj: - forall r1 r2, - In r1 float_callee_save_regs -> - In r2 float_callee_save_regs -> - r1 <> r2 -> - index_float_callee_save r1 <> index_float_callee_save r2. -Proof. - intros r1 r2. - simpl; ElimOrEq; ElimOrEq; unfold index_float_callee_save; - intros; congruence. -Qed. - -(** The following lemmas show that - (temporaries, destroyed at call, integer callee-save, float callee-save) - is a partition of the set of machine registers. *) - -Lemma int_float_callee_save_disjoint: - list_disjoint int_callee_save_regs float_callee_save_regs. -Proof. - red; intros r1 r2. simpl; ElimOrEq; ElimOrEq; discriminate. -Qed. - -Lemma register_classification: - forall r, - In r destroyed_at_call \/ In r int_callee_save_regs \/ In r float_callee_save_regs. -Proof. - destruct r; - try (left; simpl; OrEq); - try (right; left; simpl; OrEq); - try (right; right; simpl; OrEq). -Qed. - -Lemma int_callee_save_not_destroyed: - forall r, - In r destroyed_at_call -> In r int_callee_save_regs -> False. -Proof. - intros. revert H0 H. simpl. ElimOrEq; NotOrEq. -Qed. - -Lemma float_callee_save_not_destroyed: - forall r, - In r destroyed_at_call -> In r float_callee_save_regs -> False. -Proof. - intros. revert H0 H. simpl. ElimOrEq; NotOrEq. -Qed. - -Lemma int_callee_save_type: - forall r, In r int_callee_save_regs -> mreg_type r = Tany32. -Proof. - intro. simpl; ElimOrEq; reflexivity. -Qed. - -Lemma float_callee_save_type: - forall r, In r float_callee_save_regs -> mreg_type r = Tany64. -Proof. - intro. simpl; ElimOrEq; reflexivity. -Qed. - -Ltac NoRepet := - match goal with - | |- list_norepet nil => - apply list_norepet_nil - | |- list_norepet (?a :: ?b) => - apply list_norepet_cons; [simpl; intuition discriminate | NoRepet] - end. - -Lemma int_callee_save_norepet: - list_norepet int_callee_save_regs. -Proof. - unfold int_callee_save_regs; NoRepet. -Qed. - -Lemma float_callee_save_norepet: - list_norepet float_callee_save_regs. -Proof. - unfold float_callee_save_regs; NoRepet. -Qed. - (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers @@ -258,12 +107,12 @@ Qed. Lemma loc_result_caller_save: forall (s: signature) (r: mreg), - In r (loc_result s) -> In r destroyed_at_call. + In r (loc_result s) -> is_callee_save r = false. Proof. intros. assert (r = R3 \/ r = R4 \/ r = F1). unfold loc_result in H. destruct (sig_res s); [destruct t|idtac]; simpl in H; intuition. - destruct H0 as [A | [A | A]]; subst r; simpl; OrEq. + destruct H0 as [A | [A | A]]; subst r; reflexivity. Qed. (** ** Location of function arguments *) @@ -347,20 +196,13 @@ Fixpoint size_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z := Definition size_arguments (s: signature) : Z := size_arguments_rec s.(sig_args) 0 0 0. -(** A tail-call is possible for a signature if the corresponding - arguments are all passed in registers. *) - -Definition tailcall_possible (s: signature) : Prop := - forall l, In l (loc_arguments s) -> - match l with R _ => True | S _ _ _ => False end. - (** Argument locations are either caller-save registers or [Outgoing] stack slots at nonnegative offsets. *) Definition loc_argument_acceptable (l: loc) : Prop := match l with - | R r => In r destroyed_at_call - | S Outgoing ofs ty => ofs >= 0 /\ ty <> Tlong + | R r => is_callee_save r = false + | S Outgoing ofs ty => ofs >= 0 /\ (typealign ty | ofs) | _ => False end. @@ -369,7 +211,7 @@ Remark loc_arguments_rec_charact: In l (loc_arguments_rec tyl ir fr ofs) -> match l with | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= ofs /\ ty <> Tlong + | S Outgoing ofs' ty => ofs' >= ofs /\ (typealign ty | ofs') | S _ _ _ => False end. Proof. @@ -381,13 +223,13 @@ Opaque list_nth_z. destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H. subst. left. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. congruence. + subst. split. omega. apply Z.divide_1_l. exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. - (* float *) destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H. subst. right. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. apply Zle_ge. apply align_le. omega. congruence. + subst. split. apply Zle_ge. apply align_le. omega. apply Z.divide_1_l. exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. assert (ofs <= align ofs 2) by (apply align_le; omega). intuition omega. @@ -399,18 +241,18 @@ Opaque list_nth_z. destruct H. subst; left; eapply list_nth_z_in; eauto. eapply IHtyl; eauto. assert (ofs <= align ofs 2) by (apply align_le; omega). - destruct H. subst. split. omega. congruence. - destruct H. subst. split. omega. congruence. + destruct H. subst. split. omega. apply Z.divide_1_l. + destruct H. subst. split. omega. apply Z.divide_1_l. exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. assert (ofs <= align ofs 2) by (apply align_le; omega). - destruct H. subst. split. omega. congruence. - destruct H. subst. split. omega. congruence. + destruct H. subst. split. omega. apply Z.divide_1_l. + destruct H. subst. split. omega. apply Z.divide_1_l. exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. - (* single *) destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H. subst. right. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. apply Zle_ge. apply align_le. omega. congruence. + subst. split. apply Zle_ge. apply align_le. omega. apply Z.divide_1_l. exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. assert (ofs <= align ofs 2) by (apply align_le; omega). intuition omega. @@ -418,13 +260,13 @@ Opaque list_nth_z. destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H. subst. left. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. congruence. + subst. split. omega. apply Z.divide_1_l. exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. - (* any64 *) destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H. subst. right. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. apply Zle_ge. apply align_le. omega. congruence. + subst. split. apply Zle_ge. apply align_le. omega. apply Z.divide_1_l. exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. assert (ofs <= align ofs 2) by (apply align_le; omega). intuition omega. @@ -435,10 +277,12 @@ Lemma loc_arguments_acceptable: In l (loc_arguments s) -> loc_argument_acceptable l. Proof. unfold loc_arguments; intros. + assert (A: forall r, In r int_param_regs -> is_callee_save r = false) by decide_goal. + assert (B: forall r, In r float_param_regs -> is_callee_save r = false) by decide_goal. generalize (loc_arguments_rec_charact _ _ _ _ _ H). destruct l. - intro H0; elim H0; simpl; ElimOrEq; OrEq. - destruct sl; try contradiction. simpl. intuition omega. + intros [C|C]; simpl; auto. + destruct sl; try contradiction. simpl; auto. Qed. Hint Resolve loc_arguments_acceptable: locs. diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 4ee6493c..24065254 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -12,6 +12,7 @@ Require Import String. Require Import Coqlib. +Require Import Decidableplus. Require Import Maps. Require Import AST. Require Import Op. @@ -53,6 +54,34 @@ Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}. Proof. decide equality. Defined. Global Opaque mreg_eq. +Definition all_mregs := + R3 :: R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 + :: R11 :: R12 :: R14 :: R15 :: R16 :: R17 :: R18 :: R19 :: R20 + :: R21 :: R22 :: R23 :: R24 :: R25 :: R26 :: R27 :: R28 + :: R29 :: R30 :: R31 + :: F0 :: F1 :: F2 :: F3 :: F4 + :: F5 :: F6 :: F7 :: F8 + :: F9 :: F10 :: F11 :: F12 + :: F13 :: F14 :: F15 + :: F16 :: F17 :: F18 :: F19 + :: F20 :: F21 :: F22 :: F23 + :: F24 :: F25 :: F26 :: F27 + :: F28 :: F29 :: F30 :: F31 :: nil. + +Lemma all_mregs_complete: + forall (r: mreg), In r all_mregs. +Proof. + assert (forall r, proj_sumbool (In_dec mreg_eq r all_mregs) = true) by (destruct r; reflexivity). + intros. specialize (H r). InvBooleans. auto. +Qed. + +Instance Decidable_eq_mreg : forall (x y: mreg), Decidable (eq x y) := Decidable_eq mreg_eq. + +Instance Finite_mreg : Finite mreg := { + Finite_elements := all_mregs; + Finite_elements_spec := all_mregs_complete +}. + Definition mreg_type (r: mreg): typ := match r with | R3 | R4 | R5 | R6 | R7 | R8 | R9 | R10 | R11 | R12 @@ -92,7 +121,7 @@ Module IndexedMreg <: INDEXED_TYPE. Lemma index_inj: forall r1 r2, index r1 = index r2 -> r1 = r2. Proof. - destruct r1; destruct r2; simpl; intro; discriminate || reflexivity. + decide_goal. Qed. End IndexedMreg. diff --git a/powerpc/Stacklayout.v b/powerpc/Stacklayout.v index a751fd98..2b78fd11 100644 --- a/powerpc/Stacklayout.v +++ b/powerpc/Stacklayout.v @@ -13,6 +13,7 @@ (** Machine- and ABI-dependent layout information for activation records. *) Require Import Coqlib. +Require Import Memory Separation. Require Import Bounds. (** In the PowerPC/EABI application binary interface, @@ -25,8 +26,7 @@ Require Import Bounds. frame, we will not use these 4 bytes, and just reserve them. - 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 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 @@ -35,100 +35,111 @@ the boundaries between areas in the frame part. Definition fe_ofs_arg := 8. -Record frame_env : Type := mk_frame_env { - fe_size: Z; - fe_ofs_link: Z; - fe_ofs_retaddr: Z; - fe_ofs_local: Z; - fe_ofs_int_callee_save: Z; - fe_num_int_callee_save: Z; - fe_ofs_float_callee_save: Z; - fe_num_float_callee_save: Z; - fe_stack_data: Z -}. - (** Computation of the frame environment from the bounds of the current function. *) Definition make_env (b: bounds) := let ol := align (8 + 4 * b.(bound_outgoing)) 8 in (* locals *) let ora := ol + 4 * b.(bound_local) in (* saved return address *) - let oics := ora + 4 in (* integer callee-saves *) - let oendi := oics + 4 * b.(bound_int_callee_save) in - let ofcs := align oendi 8 in (* float callee-saves *) - let ostkdata := ofcs + 8 * b.(bound_float_callee_save) in (* stack data *) + let ocs := ora + 4 in (* callee-saves *) + let oendcs := size_callee_save_area b ocs in + let ostkdata := align oendcs 8 in (* stack data *) let sz := align (ostkdata + b.(bound_stack_data)) 16 in - mk_frame_env sz 0 ora - ol - oics b.(bound_int_callee_save) - ofcs b.(bound_float_callee_save) - ostkdata. + {| fe_size := sz; + fe_ofs_link := 0; + fe_ofs_retaddr := ora; + fe_ofs_local := ol; + fe_ofs_callee_save := ocs; + fe_stack_data := ostkdata; + fe_used_callee_save := b.(used_callee_save) |}. (** Separation property *) -Remark frame_env_separated: - forall b, +Local Open Scope sep_scope. + +Lemma frame_env_separated: + forall b sp m P, let fe := make_env b in - 0 <= fe.(fe_ofs_link) - /\ fe.(fe_ofs_link) + 4 <= fe_ofs_arg - /\ fe_ofs_arg + 4 * b.(bound_outgoing) <= fe.(fe_ofs_local) - /\ fe.(fe_ofs_local) + 4 * b.(bound_local) <= fe.(fe_ofs_retaddr) - /\ fe.(fe_ofs_retaddr) + 4 <= fe.(fe_ofs_int_callee_save) - /\ fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save) <= fe.(fe_ofs_float_callee_save) - /\ fe.(fe_ofs_float_callee_save) + 8 * b.(bound_float_callee_save) <= fe.(fe_stack_data) - /\ fe.(fe_stack_data) + b.(bound_stack_data) <= fe.(fe_size) - /\ fe.(fe_ofs_retaddr) + 4 <= fe.(fe_size). + m |= range sp 0 (fe_stack_data fe) ** range sp (fe_stack_data fe + bound_stack_data b) (fe_size fe) ** P -> + m |= range sp (fe_ofs_local fe) (fe_ofs_local fe + 4 * bound_local b) + ** range sp fe_ofs_arg (fe_ofs_arg + 4 * bound_outgoing b) + ** range sp (fe_ofs_link fe) (fe_ofs_link fe + 4) + ** range sp (fe_ofs_retaddr fe) (fe_ofs_retaddr fe + 4) + ** range sp (fe_ofs_callee_save fe) (size_callee_save_area b (fe_ofs_callee_save fe)) + ** P. Proof. - intros. - generalize (align_le (8 + 4 * b.(bound_outgoing)) 8 (refl_equal _)). - generalize (align_le (fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save)) 8 (refl_equal _)). - generalize (align_le (fe.(fe_stack_data) + b.(bound_stack_data)) 16 (refl_equal _)). - unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr, - fe_ofs_local, fe_ofs_int_callee_save, - fe_num_int_callee_save, - fe_ofs_float_callee_save, fe_num_float_callee_save, - fe_stack_data, fe_ofs_arg. - intros. - generalize (bound_local_pos b); intro; - generalize (bound_int_callee_save_pos b); intro; - generalize (bound_float_callee_save_pos b); intro; - generalize (bound_outgoing_pos b); intro; - generalize (bound_stack_data_pos b); intro. - omega. +Local Opaque Z.add Z.mul sepconj range. + intros; simpl. + set (ol := align (8 + 4 * b.(bound_outgoing)) 8). + set (ora := ol + 4 * b.(bound_local)). + set (ocs := ora + 4). + set (oendcs := size_callee_save_area b ocs). + set (ostkdata := align oendcs 8). + generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. + unfold fe_ofs_arg. + assert (8 + 4 * b.(bound_outgoing) <= ol) by (apply align_le; omega). + assert (ol <= ora) by (unfold ora; omega). + assert (ora <= ocs) by (unfold ocs; omega). + assert (ocs <= oendcs) by (apply size_callee_save_area_incr). + assert (oendcs <= ostkdata) by (apply align_le; omega). +(* Reorder as: + back link + outgoing + locals + retaddr + callee-save *) + rewrite sep_swap3. +(* Apply range_split and range_split2 repeatedly *) + apply range_drop_right with 8. omega. + apply range_split. omega. + apply range_split_2. fold ol; omega. omega. + apply range_split. omega. + apply range_split. omega. + apply range_drop_right with ostkdata. omega. + eapply sep_drop2. eexact H. Qed. -(** Alignment property *) +Lemma frame_env_range: + forall b, + let fe := make_env b in + 0 <= fe_stack_data fe /\ fe_stack_data fe + bound_stack_data b <= fe_size fe. +Proof. + intros; simpl. + set (ol := align (8 + 4 * b.(bound_outgoing)) 8). + set (ora := ol + 4 * b.(bound_local)). + set (ocs := ora + 4). + set (oendcs := size_callee_save_area b ocs). + set (ostkdata := align oendcs 8). + generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. + unfold fe_ofs_arg. + assert (8 + 4 * b.(bound_outgoing) <= ol) by (apply align_le; omega). + assert (ol <= ora) by (unfold ora; omega). + assert (ora <= ocs) by (unfold ocs; omega). + assert (ocs <= oendcs) by (apply size_callee_save_area_incr). + assert (oendcs <= ostkdata) by (apply align_le; omega). + split. omega. apply align_le. omega. +Qed. -Remark frame_env_aligned: +Lemma frame_env_aligned: forall b, let fe := make_env b in - (4 | fe.(fe_ofs_link)) - /\ (8 | fe.(fe_ofs_local)) - /\ (4 | fe.(fe_ofs_int_callee_save)) - /\ (8 | fe.(fe_ofs_float_callee_save)) - /\ (4 | fe.(fe_ofs_retaddr)) - /\ (8 | fe.(fe_stack_data)) - /\ (16 | fe.(fe_size)). + (8 | fe_ofs_arg) + /\ (8 | fe_ofs_local fe) + /\ (8 | fe_stack_data fe) + /\ (4 | fe_ofs_link fe) + /\ (4 | fe_ofs_retaddr fe). Proof. - intros. - unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr, - fe_ofs_local, fe_ofs_int_callee_save, - fe_num_int_callee_save, - fe_ofs_float_callee_save, fe_num_float_callee_save, - fe_stack_data. - set (x1 := align (8 + 4 * bound_outgoing b) 8). - assert (8 | x1). unfold x1; apply align_divides. omega. - set (x2 := x1 + 4 * bound_local b). - assert (4 | x2). unfold x2; apply Zdivide_plus_r; auto. - apply Zdivides_trans with 8. exists 2; auto. auto. - exists (bound_local b); ring. - set (x3 := x2 + 4). - assert (4 | x3). unfold x3; apply Zdivide_plus_r; auto. exists 1; auto. - set (x4 := align (x3 + 4 * bound_int_callee_save b) 8). - assert (8 | x4). unfold x4. apply align_divides. omega. - set (x5 := x4 + 8 * bound_float_callee_save b). - assert (8 | x5). unfold x5. apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring. - set (x6 := align (x5 + bound_stack_data b) 16). - assert (16 | x6). unfold x6; apply align_divides. omega. - intuition. + intros; simpl. + set (ol := align (8 + 4 * b.(bound_outgoing)) 8). + set (ora := ol + 4 * b.(bound_local)). + set (ocs := ora + 4). + set (oendcs := size_callee_save_area b ocs). + set (ostkdata := align oendcs 8). + split. exists (fe_ofs_arg / 8); reflexivity. + split. apply align_divides; omega. + split. apply align_divides; omega. + split. apply Zdivide_0. + apply Z.divide_add_r. + apply Zdivide_trans with 8. exists 2; auto. apply align_divides; omega. + apply Z.divide_factor_l. Qed. |