diff options
Diffstat (limited to 'arm/linux')
| -rw-r--r-- | arm/linux/Conventions1.v | 337 | ||||
| -rw-r--r-- | arm/linux/Stacklayout.v | 83 |
2 files changed, 153 insertions, 267 deletions
diff --git a/arm/linux/Conventions1.v b/arm/linux/Conventions1.v index f1ddc23..1731eba 100644 --- a/arm/linux/Conventions1.v +++ b/arm/linux/Conventions1.v @@ -32,34 +32,19 @@ Require Import Locations. *) Definition int_caller_save_regs := - R0 :: R1 :: R2 :: R3 :: nil. + R0 :: R1 :: R2 :: R3 :: R12 :: nil. Definition float_caller_save_regs := - F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: nil. + F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: nil. Definition int_callee_save_regs := - R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R11 :: nil. + R4 :: R5 :: R6 :: R7 :: R8 :: R9 :: R10 :: R11 :: nil. Definition float_callee_save_regs := F8 :: F9 :: F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: nil. -Definition destroyed_at_call_regs := - int_caller_save_regs ++ float_caller_save_regs. - Definition destroyed_at_call := - List.map R destroyed_at_call_regs. - -Definition int_temporaries := IT1 :: IT2 :: nil. - -Definition float_temporaries := FT1 :: FT2 :: nil. - -Definition temporary_regs := int_temporaries ++ float_temporaries. - -Definition temporaries := List.map R temporary_regs. - -Definition destroyed_at_move_regs: list mreg := nil. - -Definition destroyed_at_move := List.map R destroyed_at_move_regs. + int_caller_save_regs ++ float_caller_save_regs. Definition dummy_int_reg := R0. (**r Used in [Coloring]. *) Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) @@ -72,7 +57,7 @@ Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) Definition index_int_callee_save (r: mreg) := match r with | R4 => 0 | R5 => 1 | R6 => 2 | R7 => 3 - | R8 => 4 | R9 => 5 | R11 => 6 + | R8 => 4 | R9 => 5 | R10 => 6 | R11 => 7 | _ => -1 end. @@ -169,34 +154,27 @@ Qed. Lemma register_classification: forall r, - (In (R r) temporaries \/ In (R r) destroyed_at_call) \/ - (In r int_callee_save_regs \/ In r float_callee_save_regs). + In r destroyed_at_call \/ In r int_callee_save_regs \/ In r float_callee_save_regs. Proof. destruct r; - try (left; left; simpl; OrEq); - try (left; right; simpl; OrEq); + 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 r) temporaries \/ In (R r) destroyed_at_call -> - ~(In r int_callee_save_regs). + In r destroyed_at_call -> In r int_callee_save_regs -> False. Proof. - intros; red; intros. elim H. - generalize H0. simpl; ElimOrEq; NotOrEq. - generalize H0. simpl; ElimOrEq; NotOrEq. + intros. revert H0 H. simpl. ElimOrEq; NotOrEq. Qed. Lemma float_callee_save_not_destroyed: forall r, - In (R r) temporaries \/ In (R r) destroyed_at_call -> - ~(In r float_callee_save_regs). + In r destroyed_at_call -> In r float_callee_save_regs -> False. Proof. - intros; red; intros. elim H. - generalize H0. simpl; ElimOrEq; NotOrEq. - generalize H0. simpl; ElimOrEq; NotOrEq. + intros. revert H0 H. simpl. ElimOrEq; NotOrEq. Qed. Lemma int_callee_save_type: @@ -245,51 +223,33 @@ Qed. Calling conventions are largely arbitrary: they must respect the properties proved in this section (such as no overlapping between the locations of function arguments), but this leaves much liberty in choosing actual - locations. To ensure binary interoperability of code generated by our - compiler with libraries compiled by another ARM EABI compiler, we - implement *almost* the standard conventions defined in the ARM EABI application - binary interface, with two exceptions: -- Double-precision arguments and results are passed in VFP double registers - instead of pairs of integer registers. -- Single-precision arguments and results are passed as double-precision floats. -*) + locations. *) (** ** Location of function result *) (** The result value of a function is passed back to the caller in - registers [R0] or [F0], depending on the type of the returned value. - We treat a function without result as a function with one integer result. *) + registers [R0] or [F0] or [R0,R1], depending on the type of the + returned value. We treat a function without result as a function + with one integer result. *) -Definition loc_result (s: signature) : mreg := +Definition loc_result (s: signature) : list mreg := match s.(sig_res) with - | None => R0 - | Some Tint => R0 - | Some Tfloat => F0 + | None => R0 :: nil + | Some Tint => R0 :: nil + | Some Tfloat => F0 :: nil + | Some Tlong => R1 :: R0 :: nil end. -(** The result location has the type stated in the signature. *) - -Lemma loc_result_type: - forall sig, - mreg_type (loc_result sig) = - match sig.(sig_res) with None => Tint | Some ty => ty end. -Proof. - intros; unfold loc_result. - destruct (sig_res sig). - destruct t; reflexivity. - reflexivity. -Qed. - (** The result location is a caller-save register or a temporary *) Lemma loc_result_caller_save: - forall (s: signature), - In (R (loc_result s)) destroyed_at_call \/ In (R (loc_result s)) temporaries. + forall (s: signature) (r: mreg), + In r (loc_result s) -> In r destroyed_at_call. Proof. - intros; unfold loc_result. left; - destruct (sig_res s). - destruct t; simpl; OrEq. - simpl; OrEq. + intros. + assert (r = R0 \/ r = R1 \/ r = F0). + 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. Qed. (** ** Location of function arguments *) @@ -299,34 +259,37 @@ Qed. - The first 2 float arguments are passed in registers [F0] and [F1]. - Each float argument passed in a float register ``consumes'' an aligned pair of two integer registers. +- Each long integer argument is passed in an aligned pair of two integer + registers. - Extra arguments are passed on the stack, in [Outgoing] slots, consecutively - assigned (1 word for an integer argument, 2 words for a float), + assigned (1 word for an integer argument, 2 words for a float or a long), starting at word offset 0. *) -Function ireg_param (n: Z) : mreg := +Definition ireg_param (n: Z) : mreg := if zeq n (-4) then R0 else if zeq n (-3) then R1 else if zeq n (-2) then R2 - else if zeq n (-1) then R3 - else R4. (**r should not happen *) - -Function freg_param (n: Z) : mreg := - if zeq n (-4) then F0 - else if zeq n (-3) then F1 - else if zeq n (-2) then F1 - else F2. (**r should not happen *) + else R3. +Definition freg_param (n: Z) : mreg := + if zeq n (-4) then F0 else F1. Fixpoint loc_arguments_rec (tyl: list typ) (ofs: Z) {struct tyl} : list loc := match tyl with | nil => nil | Tint :: tys => - (if zle 0 ofs then S (Outgoing ofs Tint) else R (ireg_param ofs)) + (if zle 0 ofs then S Outgoing ofs Tint else R (ireg_param ofs)) :: loc_arguments_rec tys (ofs + 1) | Tfloat :: tys => - (if zle (-1) ofs then S (Outgoing (align ofs 2) Tfloat) else R (freg_param ofs)) - :: loc_arguments_rec tys (align ofs 2 + 2) + let ofs := align ofs 2 in + (if zle 0 ofs then S Outgoing ofs Tfloat else R (freg_param ofs)) + :: loc_arguments_rec tys (ofs + 2) + | Tlong :: tys => + let ofs := align ofs 2 in + (if zle 0 ofs then S Outgoing (ofs + 1) Tint else R (ireg_param (ofs + 1))) + :: (if zle 0 ofs then S Outgoing ofs Tint else R (ireg_param ofs)) + :: loc_arguments_rec tys (ofs + 2) end. (** [loc_arguments s] returns the list of locations where to store arguments @@ -342,7 +305,7 @@ Fixpoint size_arguments_rec (tyl: list typ) (ofs: Z) {struct tyl} : Z := match tyl with | nil => ofs | Tint :: tys => size_arguments_rec tys (ofs + 1) - | Tfloat :: tys => size_arguments_rec tys (align ofs 2 + 2) + | (Tfloat | Tlong) :: tys => size_arguments_rec tys (align ofs 2 + 2) end. Definition size_arguments (s: signature) : Z := @@ -353,109 +316,85 @@ Definition size_arguments (s: signature) : Z := Definition loc_argument_acceptable (l: loc) : Prop := match l with - | R r => ~(In l temporaries) - | S (Outgoing ofs ty) => ofs >= 0 + | R r => In r destroyed_at_call + | S Outgoing ofs ty => ofs >= 0 /\ ty <> Tlong | _ => False end. +(* Lemma align_monotone: forall x1 x2 y, y > 0 -> x1 <= x2 -> align x1 y <= align x2 y. Proof. intros. unfold align. apply Zmult_le_compat_r. apply Z_div_le. omega. omega. omega. Qed. +*) + +Remark ireg_param_caller_save: + forall n, In (ireg_param n) destroyed_at_call. +Proof. + unfold ireg_param; intros. + destruct (zeq n (-4)). simpl; auto. + destruct (zeq n (-3)). simpl; auto. + destruct (zeq n (-2)); simpl; auto. +Qed. + +Remark freg_param_caller_save: + forall n, In (freg_param n) destroyed_at_call. +Proof. + unfold freg_param; intros. destruct (zeq n (-4)); simpl; OrEq. +Qed. Remark loc_arguments_rec_charact: forall tyl ofs l, In l (loc_arguments_rec tyl ofs) -> match l with - | R r => - (exists n, ofs <= n < 0 /\ r = ireg_param n) - \/ (exists n, ofs <= n < -1 /\ r = freg_param n) - | S (Outgoing ofs' ty) => ofs' >= 0 /\ ofs' >= ofs - | S _ => False + | R r => In r destroyed_at_call + | S Outgoing ofs' ty => ofs' >= 0 /\ ofs <= ofs' /\ ty <> Tlong + | S _ _ _ => False end. Proof. induction tyl; simpl loc_arguments_rec; intros. elim H. - destruct a; elim H; intro. - subst l. destruct (zle 0 ofs). omega. - left. exists ofs; split; auto; omega. - generalize (IHtyl _ _ H0). - destruct l. intros [[n A] | [n A]]; [left|right]; exists n; intuition omega. - destruct s; auto; omega. - subst l. destruct (zle (-1) ofs). - split. apply Zle_ge. change 0 with (align (-1) 2). apply align_monotone; omega. - apply Zle_ge. apply align_le. omega. - right. exists ofs. intuition. + destruct a. +- (* Tint *) + destruct H. + subst l. destruct (zle 0 ofs). + split. omega. split. omega. congruence. + apply ireg_param_caller_save. + exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. +- (* Tfloat *) assert (ofs <= align ofs 2) by (apply align_le; omega). - generalize (IHtyl _ _ H0). - destruct l. intros [[n A] | [n A]]; [left|right]; exists n; intuition omega. - destruct s; auto; omega. -Qed. - -Lemma loc_notin_in_diff: - forall l ll, - Loc.notin l ll <-> (forall l', In l' ll -> Loc.diff l l'). -Proof. - induction ll; simpl; intuition. subst l'. auto. -Qed. - -Remark loc_arguments_rec_notin_local: - forall tyl ofs ofs0 ty0, - Loc.notin (S (Local ofs0 ty0)) (loc_arguments_rec tyl ofs). -Proof. - intros. rewrite loc_notin_in_diff. intros. - exploit loc_arguments_rec_charact; eauto. - destruct l'; intros; simpl; auto. destruct s; auto; contradiction. + destruct H. + subst l. destruct (zle 0 (align ofs 2)). + split. omega. split. auto. congruence. + apply freg_param_caller_save. + exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. +- (* Tlong *) + assert (ofs <= align ofs 2) by (apply align_le; omega). + destruct H. + subst l. destruct (zle 0 (align ofs 2)). + split. omega. split. omega. congruence. + apply ireg_param_caller_save. + destruct H. + subst l. destruct (zle 0 (align ofs 2)). + split. omega. split. omega. congruence. + apply ireg_param_caller_save. + exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. Qed. Lemma loc_arguments_acceptable: forall (s: signature) (r: loc), In r (loc_arguments s) -> loc_argument_acceptable r. Proof. - unfold loc_arguments; intros. + unfold loc_arguments, loc_argument_acceptable; intros. generalize (loc_arguments_rec_charact _ _ _ H). - destruct r; simpl. - intros [[n [A B]] | [n [A B]]]; subst m. - functional induction (ireg_param n); intuition congruence. - functional induction (freg_param n); intuition congruence. - destruct s0; tauto. + destruct r; auto. + destruct sl; auto. + tauto. Qed. Hint Resolve loc_arguments_acceptable: locs. -(** Arguments are parwise disjoint (in the sense of [Loc.norepet]). *) - -Lemma loc_arguments_norepet: - forall (s: signature), Loc.norepet (loc_arguments s). -Proof. - unfold loc_arguments; intros. - assert (forall tyl ofs, -4 <= ofs -> Loc.norepet (loc_arguments_rec tyl ofs)). - induction tyl; simpl; intros. - constructor. - destruct a; constructor. - rewrite loc_notin_in_diff. intros. exploit loc_arguments_rec_charact; eauto. - destruct (zle 0 ofs); destruct l'; simpl; auto. - destruct s0; intuition. - intros [[n [A B]] | [n [A B]]]; subst m. - functional induction (ireg_param ofs); functional induction (ireg_param n); congruence || omegaContradiction. - functional induction (ireg_param ofs); functional induction (freg_param n); congruence || omegaContradiction. - apply IHtyl. omega. - rewrite loc_notin_in_diff. intros. exploit loc_arguments_rec_charact; eauto. - destruct (zle (-1) ofs); destruct l'; simpl; auto. - destruct s0; intuition. - intros [[n [A B]] | [n [A B]]]; subst m. - functional induction (freg_param ofs); functional induction (ireg_param n); congruence || omegaContradiction. - functional induction (freg_param ofs); functional induction (freg_param n); try (congruence || omegaContradiction). - compute in A. intuition. - compute in A. intuition. - compute in A. intuition. - compute in A. intuition. - compute in A. intuition. - apply IHtyl. assert (ofs <= align ofs 2) by (apply align_le; omega). omega. - apply H. omega. -Qed. - (** The offsets of [Outgoing] arguments are below [size_arguments s]. *) Remark size_arguments_rec_above: @@ -468,6 +407,8 @@ Proof. apply Zle_trans with (ofs + 1); auto; omega. assert (ofs <= align ofs 2) by (apply align_le; omega). apply Zle_trans with (align ofs 2 + 2); auto; omega. + assert (ofs <= align ofs 2) by (apply align_le; omega). + apply Zle_trans with (align ofs 2 + 2); auto; omega. Qed. Lemma size_arguments_above: @@ -478,79 +419,35 @@ Qed. Lemma loc_arguments_bounded: forall (s: signature) (ofs: Z) (ty: typ), - In (S (Outgoing ofs ty)) (loc_arguments s) -> + In (S Outgoing ofs ty) (loc_arguments s) -> ofs + typesize ty <= size_arguments s. Proof. intros. assert (forall tyl ofs0, 0 <= ofs0 -> ofs0 <= Zmax 0 (size_arguments_rec tyl ofs0)). + { intros. generalize (size_arguments_rec_above tyl ofs0). intros. - rewrite Zmax_spec. rewrite zlt_false. auto. omega. + rewrite Zmax_spec. rewrite zlt_false. auto. omega. + } assert (forall tyl ofs0, - In (S (Outgoing ofs ty)) (loc_arguments_rec tyl ofs0) -> + In (S Outgoing ofs ty) (loc_arguments_rec tyl ofs0) -> ofs + typesize ty <= Zmax 0 (size_arguments_rec tyl ofs0)). - induction tyl; simpl; intros. - elim H1. - destruct a; elim H1; intros. - destruct (zle 0 ofs0); inv H2. apply H0. omega. auto. - destruct (zle (-1) ofs0); inv H2. apply H0. - assert (align (-1) 2 <= align ofs0 2). apply align_monotone. omega. auto. - change (align (-1) 2) with 0 in H2. omega. - auto. - + { + induction tyl; simpl; intros. + elim H1. + destruct a. + - (* Tint *) + destruct H1; auto. destruct (zle 0 ofs0); inv H1. apply H0. omega. + - (* Tfloat *) + destruct H1; auto. destruct (zle 0 (align ofs0 2)); inv H1. apply H0. omega. + - (* Tlong *) + destruct H1. + destruct (zle 0 (align ofs0 2)); inv H1. + eapply Zle_trans. 2: apply H0. simpl typesize; omega. omega. + destruct H1; auto. + destruct (zle 0 (align ofs0 2)); inv H1. + eapply Zle_trans. 2: apply H0. simpl typesize; omega. omega. + } unfold size_arguments. apply H1. auto. Qed. - -(** Temporary registers do not overlap with argument locations. *) - -Lemma loc_arguments_not_temporaries: - forall sig, Loc.disjoint (loc_arguments sig) temporaries. -Proof. - intros; red; intros x1 x2 A B. - exploit loc_arguments_acceptable; eauto. unfold loc_argument_acceptable. - destruct x1; intros. simpl. destruct x2; auto. intuition congruence. - destruct s; try contradiction. revert B. simpl. ElimOrEq; auto. -Qed. -Hint Resolve loc_arguments_not_temporaries: locs. - -(** Argument registers are caller-save. *) - -Lemma arguments_caller_save: - forall sig r, - In (R r) (loc_arguments sig) -> In (R r) destroyed_at_call. -Proof. - unfold loc_arguments; intros. - destruct (loc_arguments_rec_charact _ _ _ H) as [[n [A B]] | [n [A B]]]; subst r. - functional induction (ireg_param n); simpl; auto. omegaContradiction. - functional induction (freg_param n); simpl; auto 10. -Qed. - -(** Argument locations agree in number with the function signature. *) - -Lemma loc_arguments_length: - forall sig, - List.length (loc_arguments sig) = List.length sig.(sig_args). -Proof. - assert (forall tyl ofs, List.length (loc_arguments_rec tyl ofs) = List.length tyl). - induction tyl; simpl; intros. - auto. - destruct a; simpl; decEq; auto. - - intros. unfold loc_arguments. auto. -Qed. - -(** Argument locations agree in types with the function signature. *) - -Lemma loc_arguments_type: - forall sig, List.map Loc.type (loc_arguments sig) = sig.(sig_args). -Proof. - assert (forall tyl ofs, List.map Loc.type (loc_arguments_rec tyl ofs) = tyl). - induction tyl; simpl; intros. - auto. - destruct a; simpl; decEq; auto. - destruct (zle 0 ofs). auto. functional induction (ireg_param ofs); auto. - destruct (zle (-1) ofs). auto. functional induction (freg_param ofs); auto. - - intros. unfold loc_arguments. apply H. -Qed. diff --git a/arm/linux/Stacklayout.v b/arm/linux/Stacklayout.v index d84da6b..7694dcf 100644 --- a/arm/linux/Stacklayout.v +++ b/arm/linux/Stacklayout.v @@ -18,11 +18,8 @@ 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 of integer type. +- Local stack slots. - Saved values of integer callee-save registers used by the function. -- One word of padding, if necessary to align the following data - on a 8-byte boundary. -- Local stack slots of float type. - Saved values of float callee-save registers used by the function. - Saved return address into caller. - Pointer to activation record of the caller. @@ -38,10 +35,9 @@ Record frame_env : Type := mk_frame_env { fe_size: Z; fe_ofs_link: Z; fe_ofs_retaddr: Z; - fe_ofs_int_local: Z; + fe_ofs_local: Z; fe_ofs_int_callee_save: Z; fe_num_int_callee_save: Z; - fe_ofs_float_local: Z; fe_ofs_float_callee_save: Z; fe_num_float_callee_save: Z; fe_stack_data: Z @@ -51,18 +47,17 @@ Record frame_env : Type := mk_frame_env { function. *) Definition make_env (b: bounds) := - let oil := 4 * b.(bound_outgoing) in (* integer locals *) - let oics := oil + 4 * b.(bound_int_local) in (* integer callee-saves *) + let ol := align (4 * b.(bound_outgoing)) 8 in (* locals *) + let oics := ol + 4 * b.(bound_local) in (* integer callee-saves *) let oendi := oics + 4 * b.(bound_int_callee_save) in - let ofl := align oendi 8 in (* float locals *) - let ofcs := ofl + 8 * b.(bound_float_local) in (* float callee-saves *) + let ofcs := align oendi 8 in (* float callee-saves *) let ora := ofcs + 8 * b.(bound_float_callee_save) in (* retaddr *) let olink := ora + 4 in (* back link *) let ostkdata := olink + 4 in (* stack data *) let sz := align (ostkdata + b.(bound_stack_data)) 8 in - mk_frame_env sz olink ora - oil oics b.(bound_int_callee_save) - ofl ofcs b.(bound_float_callee_save) + mk_frame_env sz olink ora ol + oics b.(bound_int_callee_save) + ofcs b.(bound_float_callee_save) ostkdata. (** Separation property *) @@ -71,26 +66,24 @@ Remark frame_env_separated: forall b, let fe := make_env b in 0 <= fe_ofs_arg - /\ fe_ofs_arg + 4 * b.(bound_outgoing) <= fe.(fe_ofs_int_local) - /\ fe.(fe_ofs_int_local) + 4 * b.(bound_int_local) <= fe.(fe_ofs_int_callee_save) - /\ fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save) <= fe.(fe_ofs_float_local) - /\ fe.(fe_ofs_float_local) + 8 * b.(bound_float_local) <= fe.(fe_ofs_float_callee_save) + /\ fe_ofs_arg + 4 * b.(bound_outgoing) <= fe.(fe_ofs_local) + /\ fe.(fe_ofs_local) + 4 * b.(bound_local) <= 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_ofs_retaddr) /\ fe.(fe_ofs_retaddr) + 4 <= fe.(fe_ofs_link) /\ fe.(fe_ofs_link) + 4 <= fe.(fe_stack_data) /\ fe.(fe_stack_data) + b.(bound_stack_data) <= fe.(fe_size). Proof. intros. - 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)) 8 (refl_equal _)). + generalize (align_le (4 * bound_outgoing b) 8 (refl_equal)). + generalize (align_le (fe_ofs_int_callee_save fe + 4 * b.(bound_int_callee_save)) 8 (refl_equal _)). + generalize (align_le (fe_stack_data fe + b.(bound_stack_data)) 8 (refl_equal)). unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr, - fe_ofs_int_local, fe_ofs_int_callee_save, - fe_num_int_callee_save, - fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save, + 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_int_local_pos b); intro; - generalize (bound_float_local_pos b); intro; + 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; @@ -104,9 +97,8 @@ Remark frame_env_aligned: forall b, let fe := make_env b in (4 | fe.(fe_ofs_link)) - /\ (4 | fe.(fe_ofs_int_local)) + /\ (8 | fe.(fe_ofs_local)) /\ (4 | fe.(fe_ofs_int_callee_save)) - /\ (8 | fe.(fe_ofs_float_local)) /\ (8 | fe.(fe_ofs_float_callee_save)) /\ (4 | fe.(fe_ofs_retaddr)) /\ (8 | fe.(fe_stack_data)) @@ -114,30 +106,27 @@ Remark frame_env_aligned: Proof. intros. unfold fe, make_env, fe_size, fe_ofs_link, fe_ofs_retaddr, - fe_ofs_int_local, fe_ofs_int_callee_save, - fe_num_int_callee_save, - fe_ofs_float_local, fe_ofs_float_callee_save, fe_num_float_callee_save, + 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 := 4 * bound_outgoing b). assert (4 | x1). unfold x1; exists (bound_outgoing b); ring. - set (x2 := x1 + 4 * bound_int_local b). - assert (4 | x2). unfold x2; apply Zdivide_plus_r; auto. exists (bound_int_local b); ring. - set (x3 := x2 + 4 * bound_int_callee_save b). - set (x4 := align x3 8). - assert (8 | x4). unfold x4. apply align_divides. omega. - set (x5 := x4 + 8 * bound_float_local b). - assert (8 | x5). unfold x5. apply Zdivide_plus_r; auto. exists (bound_float_local b); ring. - set (x6 := x5 + 8 * bound_float_callee_save b). - assert (8 | x6). - unfold x6. apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring. - assert (4 | x6). - apply Zdivides_trans with 8. exists 2; auto. auto. + set (x2 := align x1 8). + assert (8 | x2). apply align_divides. omega. + set (x3 := x2 + 4 * bound_local b). + assert (4 | x3). apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto. + exists (bound_local b); ring. + set (x4 := align (x3 + 4 * bound_int_callee_save b) 8). + assert (8 | x4). apply align_divides. omega. + set (x5 := x4 + 8 * bound_float_callee_save b). + assert (8 | x5). apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring. + assert (4 | x5). apply Zdivides_trans with 8; auto. exists 2; auto. + set (x6 := x5 + 4). + assert (4 | x6). apply Zdivide_plus_r; auto. exists 1; auto. set (x7 := x6 + 4). - assert (4 | x7). unfold x7; apply Zdivide_plus_r; auto. exists 1; auto. - set (x8 := x7 + 4). - assert (8 | x8). unfold x8, x7. replace (x6 + 4 + 4) with (x6 + 8) by omega. - apply Zdivide_plus_r; auto. exists 1; auto. - set (x9 := align (x8 + bound_stack_data b) 8). - assert (8 | x9). unfold x9; apply align_divides. omega. + assert (8 | x7). unfold x7, x6. replace (x5 + 4 + 4) with (x5 + 8) by omega. + apply Zdivide_plus_r; auto. exists 1; auto. + set (x8 := align (x7 + bound_stack_data b) 8). + assert (8 | x8). apply align_divides. omega. tauto. Qed. |