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.

1 files changed, 93 insertions, 81 deletions

diff --git a/ia32/Stacklayout.v b/ia32/Stacklayout.v
index f9d1dafe..f19f036c 100644
--- a/ia32/Stacklayout.v
+++ b/ia32/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,
@@ -24,107 +25,118 @@ Require Import Bounds.
 - Local stack slots.
 - Space for the stack-allocated data declared in Cminor
 - Return address.
-
-The [frame_env] compilation environment records the positions of
-the boundaries between these areas of the activation record.
 *)
 
 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) :=
+Definition make_env (b: bounds) : frame_env :=
   let olink := 4 * b.(bound_outgoing) in  (* back link *)
-  let oics := olink + 4 in                (* integer callee-saves *)
-  let ofcs := align (oics + 4 * b.(bound_int_callee_save)) 8 in (* float callee-saves *)
-  let ol := ofcs + 8 * b.(bound_float_callee_save) in (* locals *)
+  let ocs := olink + 4 in                 (* callee-saves *)
+  let ol :=  align (size_callee_save_area b ocs) 8 in (* locals *)
   let ostkdata := align (ol + 4 * b.(bound_local)) 8 in (* stack data *)
   let oretaddr := align (ostkdata + b.(bound_stack_data)) 4 in (* return address *)
   let sz := oretaddr + 4 in (* total size *)
-  mk_frame_env sz olink oretaddr
-                  ol
-                  oics b.(bound_int_callee_save)
-                  ofcs b.(bound_float_callee_save)
-                  ostkdata.
+  {| fe_size := sz;
+     fe_ofs_link := olink;
+     fe_ofs_retaddr := oretaddr;
+     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_link)
-  /\ fe.(fe_ofs_link) + 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_ofs_local)
-  /\ fe.(fe_ofs_local) + 4 * b.(bound_local) <= fe.(fe_stack_data)
-  /\ fe.(fe_stack_data) + b.(bound_stack_data) <= fe.(fe_ofs_retaddr)
-  /\ 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 (fe.(fe_ofs_int_callee_save) + 4 * b.(bound_int_callee_save)) 8 (refl_equal _)).
-  generalize (align_le (fe.(fe_ofs_local) + 4 * b.(bound_local)) 8 (refl_equal _)).
-  generalize (align_le (fe.(fe_stack_data) + b.(bound_stack_data)) 4 (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 (olink := 4 * b.(bound_outgoing)).
+  set (ocs := olink + 4).
+  set (ol :=  align (size_callee_save_area b ocs) 8).
+  set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
+  set (oretaddr := align (ostkdata + b.(bound_stack_data)) 4).
+  generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
+  assert (0 <= olink) by (unfold olink; omega).
+  assert (olink + 4 <= 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 <= ol) by (apply align_le; omega).
+  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega).
+  assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega).
+(* Reorder as:
+     outgoing
+     back link
+     callee-save
+     local
+     retaddr *)
+  rewrite sep_swap12.
+  rewrite sep_swap23.
+  rewrite sep_swap45.
+  rewrite sep_swap34.
+(* Apply range_split and range_split2 repeatedly *)
+  unfold fe_ofs_arg.
+  apply range_split. omega.
+  apply range_split. omega.
+  apply range_split_2. fold ol. omega. omega.
+  apply range_drop_right with ostkdata. omega.
+  rewrite sep_swap.
+  apply range_drop_left with (ostkdata + bound_stack_data b). omega.
+  rewrite sep_swap. 
+  exact H.
 Qed.
 
-(** Alignment property *)
-
-Remark frame_env_aligned:
+Lemma frame_env_range:
   forall b,
   let fe := make_env b in
-  (4 | fe.(fe_ofs_link))
-  /\ (4 | fe.(fe_ofs_int_callee_save))
-  /\ (8 | fe.(fe_ofs_float_callee_save))
-  /\ (8 | fe.(fe_ofs_local))
-  /\ (8 | fe.(fe_stack_data))
-  /\ (4 | fe.(fe_ofs_retaddr))
-  /\ (4 | fe.(fe_size)).
+  0 <= fe_stack_data fe /\ fe_stack_data fe + bound_stack_data b <= fe_size 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 := x1 + 4).
-  assert (4 | x2). unfold x2; apply Zdivide_plus_r; auto. exists 1; auto.
-  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_callee_save b).
-  assert (8 | x5). unfold x5; apply Zdivide_plus_r; auto. exists (bound_float_callee_save b); ring.
-  set (x6 := align (x5 + 4 * bound_local b) 8).
-  assert (8 | x6). unfold x6; apply align_divides; omega.
-  set (x7 := align (x6 + bound_stack_data b) 4).
-  assert (4 | x7). unfold x7; apply align_divides; omega.
-  set (x8 := x7 + 4).
-  assert (4 | x8). unfold x8; apply Zdivide_plus_r; auto. exists 1; auto.
-  tauto.
+  intros; simpl.
+  set (olink := 4 * b.(bound_outgoing)).
+  set (ocs := olink + 4).
+  set (ol :=  align (size_callee_save_area b ocs) 8).
+  set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
+  set (oretaddr := align (ostkdata + b.(bound_stack_data)) 4).
+  generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros.
+  assert (0 <= olink) by (unfold olink; omega).
+  assert (olink + 4 <= 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 <= ol) by (apply align_le; omega).
+  assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega).
+  assert (ostkdata + bound_stack_data b <= oretaddr) by (apply align_le; omega).
+  split. omega. omega. 
 Qed.
 
+Lemma frame_env_aligned:
+  forall b,
+  let fe := make_env b in
+     (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; simpl.
+  set (olink := 4 * b.(bound_outgoing)).
+  set (ocs := olink + 4).
+  set (ol :=  align (size_callee_save_area b ocs) 8).
+  set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
+  set (oretaddr := align (ostkdata + b.(bound_stack_data)) 4).
+  split. apply Zdivide_0.
+  split. apply align_divides; omega.
+  split. apply align_divides; omega.
+  split. apply Z.divide_factor_l.
+  apply align_divides; omega.
+Qed.