diff options
Diffstat (limited to 'arm')
| -rw-r--r-- | arm/Conventions1.v | 235 | ||||
| -rw-r--r-- | arm/Machregs.v | 23 | ||||
| -rw-r--r-- | arm/Stacklayout.v | 171 |
3 files changed, 157 insertions, 272 deletions
diff --git a/arm/Conventions1.v b/arm/Conventions1.v index e27a9293..abd28b18 100644 --- a/arm/Conventions1.v +++ b/arm/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. @@ -33,6 +34,14 @@ Require Archi. of callee- and caller-save registers. *) +Definition is_callee_save (r: mreg): bool := + match r with + | R0 | R1 | R2 | R3 | R12 => false + | R4 | R5 | R6 | R7 | R8 | R9 | R10 | R11 => true + | F0 | F1 | F2 | F3 | F4 | F5 | F6 | F7 => false + | F8 | F9 | F10 | F11 | F12 | F13 | F14 | F15 => true + end. + Definition int_caller_save_regs := R0 :: R1 :: R2 :: R3 :: R12 :: nil. @@ -46,171 +55,11 @@ Definition float_callee_save_regs := F8 :: F9 :: F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: 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 := R0. (**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 - | R4 => 0 | R5 => 1 | R6 => 2 | R7 => 3 - | R8 => 4 | R9 => 5 | R10 => 6 | R11 => 7 - | _ => -1 - end. - -Definition index_float_callee_save (r: mreg) := - match r with - | F8 => 0 | F9 => 1 | F10 => 2 | F11 => 3 - | F12 => 4 | F13 => 5 | F14 => 6 | F15 => 7 - | _ => -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 @@ -260,12 +109,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 = 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. + destruct H0 as [A | [A | A]]; subst r; auto. Qed. (** ** Location of function arguments *) @@ -425,8 +274,8 @@ Definition size_arguments (s: signature) : Z := 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. @@ -451,20 +300,20 @@ Remark loc_arguments_hf_charact: In l (loc_arguments_hf 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 = 1 | S _ _ _ => False end. Proof. assert (INCR: forall l ofs1 ofs2, match l with | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= ofs2 /\ ty <> Tlong + | S Outgoing ofs' ty => ofs' >= ofs2 /\ typealign ty = 1 | S _ _ _ => False end -> ofs1 <= ofs2 -> match l with | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= ofs1 /\ ty <> Tlong + | S Outgoing ofs' ty => ofs' >= ofs1 /\ typealign ty = 1 | S _ _ _ => False end). { @@ -477,13 +326,13 @@ Proof. destruct (zlt ir 4); destruct H. subst. left; apply ireg_param_in_params. eapply IHtyl; eauto. - subst. split; [omega | congruence]. + subst. split; [omega | auto]. eapply INCR. eapply IHtyl; eauto. omega. - (* float *) destruct (zlt fr 8); destruct H. subst. right; apply freg_param_in_params. eapply IHtyl; eauto. - subst. split. apply Zle_ge. apply align_le. omega. congruence. + subst. split. apply Zle_ge. apply align_le. omega. auto. eapply INCR. eapply IHtyl; eauto. apply Zle_trans with (align ofs 2). apply align_le; omega. omega. - (* long *) @@ -493,26 +342,26 @@ Proof. destruct H. subst l; left; apply ireg_param_in_params. destruct H. subst l; left; apply ireg_param_in_params. eapply IHtyl; eauto. - destruct H. subst l; split; [ omega | congruence ]. - destruct H. subst l; split; [ omega | congruence ]. + destruct H. subst l; split; [ omega | auto ]. + destruct H. subst l; split; [ omega | auto ]. eapply INCR. eapply IHtyl; eauto. omega. - (* single *) destruct (zlt fr 8); destruct H. subst. right; apply freg_param_in_params. eapply IHtyl; eauto. - subst. split; [omega | congruence]. + subst. split; [omega | auto]. eapply INCR. eapply IHtyl; eauto. omega. - (* any32 *) destruct (zlt ir 4); destruct H. subst. left; apply ireg_param_in_params. eapply IHtyl; eauto. - subst. split; [omega | congruence]. + subst. split; [omega | auto]. eapply INCR. eapply IHtyl; eauto. omega. - (* any64 *) destruct (zlt fr 8); destruct H. subst. right; apply freg_param_in_params. eapply IHtyl; eauto. - subst. split. apply Zle_ge. apply align_le. omega. congruence. + subst. split. apply Zle_ge. apply align_le. omega. auto. eapply INCR. eapply IHtyl; eauto. apply Zle_trans with (align ofs 2). apply align_le; omega. omega. Qed. @@ -522,20 +371,20 @@ Remark loc_arguments_sf_charact: In l (loc_arguments_sf tyl ofs) -> match l with | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs /\ ty <> Tlong + | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs /\ typealign ty = 1 | S _ _ _ => False end. Proof. assert (INCR: forall l ofs1 ofs2, match l with | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs2 /\ ty <> Tlong + | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs2 /\ typealign ty = 1 | S _ _ _ => False end -> ofs1 <= ofs2 -> match l with | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs1 /\ ty <> Tlong + | S Outgoing ofs' ty => ofs' >= Zmax 0 ofs1 /\ typealign ty = 1 | S _ _ _ => False end). { @@ -548,7 +397,7 @@ Proof. destruct H. destruct (zlt ofs 0); subst l. left; apply ireg_param_in_params. - split. xomega. congruence. + split. xomega. auto. eapply INCR. eapply IHtyl; eauto. omega. - (* float *) set (ofs' := align ofs 2) in *. @@ -556,7 +405,7 @@ Proof. destruct H. destruct (zlt ofs' 0); subst l. right; apply freg_param_in_params. - split. xomega. congruence. + split. xomega. auto. eapply INCR. eapply IHtyl; eauto. omega. - (* long *) set (ofs' := align ofs 2) in *. @@ -564,23 +413,23 @@ Proof. destruct H. destruct (zlt ofs' 0); subst l. left; apply ireg_param_in_params. - split. xomega. congruence. + split. xomega. auto. destruct H. destruct (zlt ofs' 0); subst l. left; apply ireg_param_in_params. - split. xomega. congruence. + split. xomega. auto. eapply INCR. eapply IHtyl; eauto. omega. - (* single *) destruct H. destruct (zlt ofs 0); subst l. right; apply freg_param_in_params. - split. xomega. congruence. + split. xomega. auto. eapply INCR. eapply IHtyl; eauto. omega. - (* any32 *) destruct H. destruct (zlt ofs 0); subst l. left; apply ireg_param_in_params. - split. xomega. congruence. + split. xomega. auto. eapply INCR. eapply IHtyl; eauto. omega. - (* any64 *) set (ofs' := align ofs 2) in *. @@ -588,7 +437,7 @@ Proof. destruct H. destruct (zlt ofs' 0); subst l. right; apply freg_param_in_params. - split. xomega. congruence. + split. xomega. auto. eapply INCR. eapply IHtyl; eauto. omega. Qed. @@ -597,14 +446,18 @@ Lemma loc_arguments_acceptable: In l (loc_arguments s) -> loc_argument_acceptable l. Proof. unfold loc_arguments; intros. - assert (forall r, In r int_param_regs \/ In r float_param_regs -> In r destroyed_at_call). - { - intros. elim H0; simpl; ElimOrEq; OrEq. - } + 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. + assert (C: forall r, In r int_param_regs \/ In r float_param_regs -> is_callee_save r = false). + { intros. destruct H0; auto. } assert (In l (loc_arguments_sf (sig_args s) (-4)) -> loc_argument_acceptable l). - { intros. red. exploit loc_arguments_sf_charact; eauto. destruct l; auto. } + { intros. red. exploit loc_arguments_sf_charact; eauto. + destruct l as [r | [] ofs ty]; auto. + intros [P Q]. rewrite Q; split. auto. apply Z.divide_1_l. } assert (In l (loc_arguments_hf (sig_args s) 0 0 0) -> loc_argument_acceptable l). - { intros. red. exploit loc_arguments_hf_charact; eauto. destruct l; auto. } + { intros. red. exploit loc_arguments_hf_charact; eauto. + destruct l as [r | [] ofs ty]; auto. + intros [P Q]. rewrite Q; split. auto. apply Z.divide_1_l. } destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; auto. Qed. diff --git a/arm/Machregs.v b/arm/Machregs.v index 211d2791..b43f9be6 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -12,6 +12,7 @@ Require Import String. Require Import Coqlib. +Require Import Decidableplus. Require Import Maps. Require Import AST. Require Import Op. @@ -43,6 +44,26 @@ Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}. Proof. decide equality. Defined. Global Opaque mreg_eq. +Definition all_mregs := + R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 + :: R8 :: R9 :: R10 :: R11 :: R12 + :: F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 + :: F8 :: F9 :: F10 :: F11 :: F12 :: F13 :: F14 :: F15 :: 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 | R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 @@ -70,7 +91,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/arm/Stacklayout.v b/arm/Stacklayout.v index 82d11727..f5c07fff 100644 --- a/arm/Stacklayout.v +++ b/arm/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. (** The general shape of activation records is as follows, @@ -31,102 +32,112 @@ the boundaries between areas in the frame part. Definition fe_ofs_arg := 0. -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 (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 ofcs := align oendi 8 in (* float callee-saves *) - let ora := ofcs + 8 * b.(bound_float_callee_save) in (* retaddr *) + 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 := olink + 4 in (* stack data *) + let ostkdata := align (olink + 4) 8 in (* stack data *) let sz := align (ostkdata + b.(bound_stack_data)) 8 in - mk_frame_env sz olink ora ol - oics b.(bound_int_callee_save) - ofcs b.(bound_float_callee_save) - ostkdata. + {| fe_size := sz; + fe_ofs_link := olink; + 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_ofs_arg - /\ 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). + 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 (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_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 (4 * b.(bound_outgoing)) 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). + 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 (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). +(* Reorder as: + outgoing + local + callee-save + retaddr + back link *) + rewrite sep_swap12. + rewrite sep_swap45. + 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_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 (4 * b.(bound_outgoing)) 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). + 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 (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). + 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)) - /\ (8 | 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 := 4 * bound_outgoing b). - assert (4 | x1). unfold x1; exists (bound_outgoing b); ring. - 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 (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. + intros; simpl. + set (ol := align (4 * b.(bound_outgoing)) 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). + 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. Qed. |