Revise the Stacking pass and its proof to make it easier to adapt to 64-bit architectures

The original Stacking pass and its proof hard-wire assumptions about the processor and the register allocation, namely that integer registers are 32 bit wide and that all stack slots have natural alignment 4, which precludes having stack slots of type Tlong.  Those assumptions become false if the target processor has 64-bit integer registers.

This commit makes minimal adjustments to the Stacking pass so as to lift these assumptions:
- Stack slots of type Tlong (or more generally of natural alignment 8) are supported.  For slots produced by register allocation, the alignment is validated a posteriori in Lineartyping.  For slots produced by the calling conventions, alignment is proved as part of the "loc_argument_acceptable" property in Conventions1.
- The code generated by Stacking to save and restore used callee-save registers no longer assumes 32-bit integer registers.  Actually, it supports any combination of sizes for registers.
- To support the new save/restore code, Bounds was changed to record the set of all callee-save registers used, rather than just the max index of callee-save registers used.

On CompCert's current 32-bit target architectures, the new Stacking pass should generate pretty much the same code as the old one, modulo minor differences in the layout of the stack frame.  (E.g. padding could be introduced at different places.)

The bulk of this big commit is related to the proof of the Stacking phase.  The old proof strategy was painful and not obviously adaptable to the new Stacking phase, so I rewrote Stackingproof entirely, using an approach inspired by separation logic.  The new library common/Separation.v defines assertions about memory states that can be composed using a separating conjunction, just like pre- and post-conditions in separation logic.  Those assertions are used in Stackingproof to describe the contents of the stack frames during the execution of the generated Mach code, and relate them with the Linear location maps.

As a further simplification, the callee-save/caller-save distinction is now defined in Conventions1 by a function is_callee_save: mreg -> bool, instead of lists of registers of either kind as before.  This eliminates many boring classification lemmas from Conventions1.  LTL and Lineartyping were adapted accordingly.

Finally, this commit introduces a new library called Decidableplus to prove some propositions by reflection as Boolean computations.  It is used to further simplify the proofs in Conventions1.

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.