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, 244 insertions, 0 deletions

diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v
new file mode 100644
index 00000000..932b885a
--- /dev/null
+++ b/lib/Decidableplus.v
@@ -0,0 +1,244 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*                Xavier Leroy, INRIA Paris                            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** This library provides type classes and tactics to decide logical
+  propositions by reflection into computable Boolean equalities.
+  It extends the [DecidableClass] module from the standard library
+  of Coq 8.5 with more instances of decidable properties, including
+  universal and existential quantification over finite types. *)
+
+(** Temporarily and for compatibility with Coq 8.4, this file includes
+  a copy of the relevant definitions from the Coq 8.5 [DecidableClass]
+  library.  This library is copyright INRIA. *)
+
+Require Import Coqlib.
+
+Class Decidable (P : Prop) := {
+  Decidable_witness : bool;
+  Decidable_spec : Decidable_witness = true <-> P
+}.
+
+Lemma Decidable_sound : forall P (H : Decidable P),
+  Decidable_witness = true -> P.
+Proof.
+  intros. rewrite <- Decidable_spec. auto.
+Qed.
+
+Lemma Decidable_complete : forall P (H : Decidable P),
+  P -> Decidable_witness = true.
+Proof.
+  intros. rewrite Decidable_spec. auto.
+Qed.
+
+Lemma Decidable_sound_alt : forall P (H : Decidable P),
+   ~ P -> Decidable_witness = false.
+Proof.
+  intros. destruct Decidable_witness eqn:E; auto. elim H0. eapply Decidable_sound; eauto.
+Qed.
+
+Lemma Decidable_complete_alt : forall P (H : Decidable P),
+  Decidable_witness = false -> ~ P.
+Proof.
+  intros; red; intros. rewrite (Decidable_complete P H) in H0 by auto. discriminate.
+Qed.
+
+Definition decide P {H : Decidable P} := Decidable_witness (Decidable:=H).
+
+Ltac _decide_ P H :=
+  let b := fresh "b" in
+  set (b := decide P) in *;
+  assert (H : decide P = b) by reflexivity;
+  clearbody b;
+  destruct b; [apply Decidable_sound in H|apply Decidable_complete_alt in H].
+
+Tactic Notation "decide" constr(P) "as" ident(H) :=
+  _decide_ P H.
+
+Tactic Notation "decide" constr(P) :=
+  let H := fresh "H" in _decide_ P H.
+
+Ltac decide_goal := eapply Decidable_sound; reflexivity.
+
+(** Deciding logical connectives *)
+
+Program Instance Decidable_not (P: Prop) (dP: Decidable P) : Decidable (~ P) := {
+  Decidable_witness := negb (@Decidable_witness P dP)
+}.
+Next Obligation.
+  rewrite negb_true_iff. split. apply Decidable_complete_alt. apply Decidable_sound_alt. 
+Qed.
+
+Program Instance Decidable_equiv (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P <-> Q) := {
+  Decidable_witness := Bool.eqb (@Decidable_witness P dP) (@Decidable_witness Q dQ)
+}.
+Next Obligation.
+  rewrite eqb_true_iff. 
+  split; intros.
+  split; intros; eapply Decidable_sound; [rewrite <- H | rewrite H]; eapply Decidable_complete; eauto.
+  destruct (@Decidable_witness Q dQ) eqn:D.
+  eapply Decidable_complete; rewrite H; eapply Decidable_sound; eauto.
+  eapply Decidable_sound_alt; rewrite H; eapply Decidable_complete_alt; eauto.
+Qed.
+
+Program Instance Decidable_and (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P /\ Q) := {
+  Decidable_witness := @Decidable_witness P dP && @Decidable_witness Q dQ
+}.
+Next Obligation.
+  rewrite andb_true_iff. rewrite ! Decidable_spec. tauto.
+Qed.
+
+Program Instance Decidable_or (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P \/ Q) := {
+  Decidable_witness := @Decidable_witness P dP || @Decidable_witness Q dQ
+}.
+Next Obligation.
+  rewrite orb_true_iff. rewrite ! Decidable_spec. tauto.
+Qed.
+
+Program Instance Decidable_implies (P Q: Prop) (dP: Decidable P) (dQ: Decidable Q) : Decidable (P -> Q) := {
+  Decidable_witness := if @Decidable_witness P dP then @Decidable_witness Q dQ else true
+}.
+Next Obligation.
+  split.
+- intros. rewrite Decidable_complete in H by auto. eapply Decidable_sound; eauto.
+- intros. destruct (@Decidable_witness P dP) eqn:WP; auto. 
+  eapply Decidable_complete. apply H. eapply Decidable_sound; eauto.
+Qed.
+
+(** Deciding equalities. *)
+
+Program Definition Decidable_eq {A: Type} (eqdec: forall (x y: A), {x=y} + {x<>y}) (x y: A) : Decidable (eq x y) := {|
+  Decidable_witness := proj_sumbool (eqdec x y)
+|}.
+Next Obligation.
+  split; intros. InvBooleans. auto. subst y. apply dec_eq_true. 
+Qed.
+
+Program Instance Decidable_eq_bool : forall (x y : bool), Decidable (eq x y) := {
+  Decidable_witness := Bool.eqb x y
+}.
+Next Obligation.
+  apply eqb_true_iff.
+Qed.
+
+Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := {
+  Decidable_witness := beq_nat x y
+}.
+Next Obligation.
+  apply beq_nat_true_iff.
+Qed.
+
+Program Instance Decidable_eq_positive : forall (x y : positive), Decidable (eq x y) := {
+  Decidable_witness := Pos.eqb x y
+}.
+Next Obligation.
+  apply Pos.eqb_eq.
+Qed.
+
+Program Instance Decidable_eq_Z : forall (x y : Z), Decidable (eq x y) := {
+  Decidable_witness := Z.eqb x y
+}.
+Next Obligation.
+  apply Z.eqb_eq.
+Qed.
+
+(** Deciding order on Z *)
+
+Program Instance Decidable_le_Z : forall (x y: Z), Decidable (x <= y) := {
+  Decidable_witness := Z.leb x y
+}.
+Next Obligation.
+  apply Z.leb_le. 
+Qed.
+
+Program Instance Decidable_lt_Z : forall (x y: Z), Decidable (x < y) := {
+  Decidable_witness := Z.ltb x y
+}.
+Next Obligation.
+  apply Z.ltb_lt. 
+Qed.
+
+(** Deciding properties over lists *)
+
+Program Instance Decidable_forall_in_list : 
+      forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)),
+      Decidable (forall x:A, In x l -> P x) := {
+  Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) l
+}.
+Next Obligation.
+  rewrite List.forallb_forall. split; intros.
+- eapply Decidable_sound; eauto.
+- eapply Decidable_complete; eauto. 
+Qed.
+
+Program Instance Decidable_exists_in_list : 
+      forall (A: Type) (l: list A) (P: A -> Prop) (dP: forall x:A, Decidable (P x)),
+      Decidable (exists x:A, In x l /\ P x) := {
+  Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) l
+}.
+Next Obligation.
+  rewrite List.existsb_exists. split.
+- intros (x & U & V). exists x; split; auto. eapply Decidable_sound; eauto.
+- intros (x & U & V). exists x; split; auto. eapply Decidable_complete; eauto.
+Qed.
+
+(** Types with finitely many elements. *)
+
+Class Finite (T: Type) := {
+  Finite_elements: list T;
+  Finite_elements_spec: forall x:T, In x Finite_elements
+}.
+
+(** Deciding forall and exists quantification over finite types. *)
+
+Program Instance Decidable_forall : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (forall x, P x) := {
+  Decidable_witness := List.forallb (fun x => @Decidable_witness (P x) (dP x)) (@Finite_elements T fT)
+}.
+Next Obligation.
+  rewrite List.forallb_forall. split; intros.
+- eapply Decidable_sound; eauto. apply H. apply Finite_elements_spec. 
+- eapply Decidable_complete; eauto. 
+Qed.
+
+Program Instance Decidable_exists : forall (T: Type) (fT: Finite T) (P: T -> Prop) (dP: forall x:T, Decidable (P x)), Decidable (exists x, P x) := {
+  Decidable_witness := List.existsb (fun x => @Decidable_witness (P x) (dP x)) (@Finite_elements T fT)
+}.
+Next Obligation.
+  rewrite List.existsb_exists. split.
+- intros (x & A & B). exists x. eapply Decidable_sound; eauto.
+- intros (x & A). exists x; split. eapply Finite_elements_spec. eapply Decidable_complete; eauto. 
+Qed.
+
+(** Some examples of finite types. *)
+
+Program Instance Finite_bool : Finite bool := {
+  Finite_elements := false :: true :: nil
+}.
+Next Obligation.
+  destruct x; auto.
+Qed.
+
+Program Instance Finite_pair : forall (A B: Type) (fA: Finite A) (fB: Finite B), Finite (A * B) := {
+  Finite_elements := list_prod (@Finite_elements A fA) (@Finite_elements B fB)
+}.
+Next Obligation.
+  apply List.in_prod; eapply Finite_elements_spec.
+Qed.
+
+Program Instance Finite_option : forall (A: Type) (fA: Finite A), Finite (option A) := {
+  Finite_elements := None :: List.map (@Some A) (@Finite_elements A fA)
+}.
+Next Obligation.
+  destruct x; auto. right; apply List.in_map; eapply Finite_elements_spec.
+Qed.