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, 34 insertions, 79 deletions

diff --git a/backend/Stacking.v b/backend/Stacking.v
index cf797a11..d1c17029 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -22,88 +22,45 @@ Require Import Bounds Conventions Stacklayout Lineartyping.
 (** The machine- and ABI-dependent aspects of the layout are defined
   in module [Stacklayout]. *)
 
-(** Computation the frame offset for the given component of the frame.
-  The component is expressed by the following [frame_index] sum type. *)
-
-Inductive frame_index: Type :=
-  | FI_link: frame_index
-  | FI_retaddr: frame_index
-  | FI_local: Z -> typ -> frame_index
-  | FI_arg: Z -> typ -> frame_index
-  | FI_saved_int: Z -> frame_index
-  | FI_saved_float: Z -> frame_index.
-
-Definition offset_of_index (fe: frame_env) (idx: frame_index) :=
-  match idx with
-  | FI_link => fe.(fe_ofs_link)
-  | FI_retaddr => fe.(fe_ofs_retaddr)
-  | FI_local x ty => fe.(fe_ofs_local) + 4 * x
-  | FI_arg x ty => fe_ofs_arg + 4 * x
-  | FI_saved_int x => fe.(fe_ofs_int_callee_save) + 4 * x
-  | FI_saved_float x => fe.(fe_ofs_float_callee_save) + 8 * x
-  end.
-
-(** * Saving and restoring callee-save registers *)
-
-(** [save_callee_save fe k] adds before [k] the instructions that
-  store in the frame the values of callee-save registers used by the
-  current function. *)
+(** Offsets (in bytes) corresponding to stack slots. *)
 
-Definition save_callee_save_reg
-    (bound: frame_env -> Z) (number: mreg -> Z) (mkindex: Z -> frame_index)
-    (ty: typ) (fe: frame_env) (cs: mreg) (k: Mach.code) :=
-  let i := number cs in
-  if zlt i (bound fe)
-  then Msetstack cs (Int.repr (offset_of_index fe (mkindex i))) ty :: k
-  else k.
+Definition offset_local (fe: frame_env) (x: Z) := fe.(fe_ofs_local) + 4 * x.
 
-Definition save_callee_save_regs
-    (bound: frame_env -> Z) (number: mreg -> Z) (mkindex: Z -> frame_index)
-    (ty: typ) (fe: frame_env) (csl: list mreg) (k: Mach.code) :=
-  List.fold_right (save_callee_save_reg bound number mkindex ty fe) k csl.
+Definition offset_arg (x: Z) := fe_ofs_arg + 4 * x.
 
-Definition save_callee_save_int (fe: frame_env) :=
-  save_callee_save_regs
-    fe_num_int_callee_save index_int_callee_save FI_saved_int
-    Tany32 fe int_callee_save_regs.
+(** [save_callee_save rl ofs k] adds before [k] the instructions that
+  store in the frame the values of callee-save registers [rl],
+  starting at offset [ofs]. *)
 
-Definition save_callee_save_float (fe: frame_env) :=
-  save_callee_save_regs
-    fe_num_float_callee_save index_float_callee_save FI_saved_float
-    Tany64 fe float_callee_save_regs.
+Fixpoint save_callee_save_rec (rl: list mreg) (ofs: Z) (k: Mach.code) :=
+  match rl with
+  | nil => k
+  | r :: rl =>
+      let ty := mreg_type r in
+      let sz := AST.typesize ty in
+      let ofs1 := align ofs sz in
+      Msetstack r (Int.repr ofs1) ty :: save_callee_save_rec rl (ofs1 + sz) k
+  end.
 
 Definition save_callee_save (fe: frame_env) (k: Mach.code) :=
-  save_callee_save_int fe (save_callee_save_float fe k).
+  save_callee_save_rec fe.(fe_used_callee_save) fe.(fe_ofs_callee_save) k.
 
 (** [restore_callee_save fe k] adds before [k] the instructions that
   re-load from the frame the values of callee-save registers used by the
   current function, restoring these registers to their initial values. *)
 
-Definition restore_callee_save_reg
-    (bound: frame_env -> Z) (number: mreg -> Z) (mkindex: Z -> frame_index)
-    (ty: typ) (fe: frame_env) (cs: mreg) (k: Mach.code) :=
-  let i := number cs in
-  if zlt i (bound fe)
-  then Mgetstack (Int.repr (offset_of_index fe (mkindex i))) ty cs :: k
-  else k.
-
-Definition restore_callee_save_regs
-    (bound: frame_env -> Z) (number: mreg -> Z) (mkindex: Z -> frame_index)
-    (ty: typ) (fe: frame_env) (csl: list mreg) (k: Mach.code) :=
-  List.fold_right (restore_callee_save_reg bound number mkindex ty fe) k csl.
-
-Definition restore_callee_save_int (fe: frame_env) :=
-  restore_callee_save_regs
-    fe_num_int_callee_save index_int_callee_save FI_saved_int
-    Tany32 fe int_callee_save_regs.
-
-Definition restore_callee_save_float (fe: frame_env) :=
-  restore_callee_save_regs
-    fe_num_float_callee_save index_float_callee_save FI_saved_float
-    Tany64 fe float_callee_save_regs.
+Fixpoint restore_callee_save_rec (rl: list mreg) (ofs: Z) (k: Mach.code) :=
+  match rl with
+  | nil => k
+  | r :: rl =>
+      let ty := mreg_type r in
+      let sz := AST.typesize ty in
+      let ofs1 := align ofs sz in
+      Mgetstack (Int.repr ofs1) ty r :: restore_callee_save_rec rl (ofs1 + sz) k
+  end.
 
 Definition restore_callee_save (fe: frame_env) (k: Mach.code) :=
-  restore_callee_save_int fe (restore_callee_save_float fe k).
+  restore_callee_save_rec fe.(fe_used_callee_save) fe.(fe_ofs_callee_save) k.
 
 (** * Code transformation. *)
 
@@ -126,7 +83,7 @@ Fixpoint transl_builtin_arg (fe: frame_env) (a: builtin_arg loc) : builtin_arg m
   match a with
   | BA (R r) => BA r
   | BA (S Local ofs ty) =>
-      BA_loadstack (chunk_of_type ty) (Int.repr (offset_of_index fe (FI_local ofs ty)))
+      BA_loadstack (chunk_of_type ty) (Int.repr (offset_local fe ofs))
   | BA (S _ _ _) => BA_int Int.zero  (**r never happens *)
   | BA_int n => BA_int n
   | BA_long n => BA_long n
@@ -157,20 +114,20 @@ Definition transl_instr
   | Lgetstack sl ofs ty r =>
       match sl with
       | Local =>
-          Mgetstack (Int.repr (offset_of_index fe (FI_local ofs ty))) ty r :: k
+          Mgetstack (Int.repr (offset_local fe ofs)) ty r :: k
       | Incoming =>
-          Mgetparam (Int.repr (offset_of_index fe (FI_arg ofs ty))) ty r :: k
+          Mgetparam (Int.repr (offset_arg ofs)) ty r :: k
       | Outgoing =>
-          Mgetstack (Int.repr (offset_of_index fe (FI_arg ofs ty))) ty r :: k
+          Mgetstack (Int.repr (offset_arg ofs)) ty r :: k
       end
   | Lsetstack r sl ofs ty =>
       match sl with
       | Local =>
-          Msetstack r (Int.repr (offset_of_index fe (FI_local ofs ty))) ty :: k
+          Msetstack r (Int.repr (offset_local fe ofs)) ty :: k
       | Incoming =>
           k (* should not happen *)
       | Outgoing =>
-          Msetstack r (Int.repr (offset_of_index fe (FI_arg ofs ty))) ty :: k
+          Msetstack r (Int.repr (offset_arg ofs)) ty :: k
       end
   | Lop op args res =>
       Mop (transl_op fe op) args res :: k
@@ -181,8 +138,7 @@ Definition transl_instr
   | Lcall sig ros =>
       Mcall sig ros :: k
   | Ltailcall sig ros =>
-      restore_callee_save fe
-        (Mtailcall sig ros :: k)
+      restore_callee_save fe (Mtailcall sig ros :: k)
   | Lbuiltin ef args dst =>
       Mbuiltin ef (map (transl_builtin_arg fe) args) dst :: k
   | Llabel lbl =>
@@ -194,8 +150,7 @@ Definition transl_instr
   | Ljumptable arg tbl =>
       Mjumptable arg tbl :: k
   | Lreturn =>
-      restore_callee_save fe
-        (Mreturn :: k)
+      restore_callee_save fe (Mreturn :: k)
   end.
 
 (** Translation of a function.  Code that saves the values of used