Platform-independent implementation of Conventions.size_arguments (#222)

The "size_arguments" function and its properties can be systematically
derived from the "loc_arguments" function and its properties.

Before, the RISC-V port used this derivation, and all other ports
used hand-written "size_arguments" functions and proofs.

This commit moves the definition of "size_arguments" to the
platform-independent file backend/Conventions.v, using the systematic
derivation, and removes the platform-specific definitions.

This reduces code and proof size, and makes it easier to change the
calling conventions.

1 files changed, 67 insertions, 0 deletions

diff --git a/backend/Conventions.v b/backend/Conventions.v
index 6025c6b4..14ffb587 100644
--- a/backend/Conventions.v
+++ b/backend/Conventions.v
@@ -34,6 +34,73 @@ Proof.
   apply IHpl; auto.
 Qed.
 
+(** ** Stack size of function arguments *)
+
+(** [size_arguments s] returns the number of [Outgoing] slots used
+  to call a function with signature [s]. *)
+
+Definition max_outgoing_1 (accu: Z) (l: loc) : Z :=
+  match l with
+  | S Outgoing ofs ty => Z.max accu (ofs + typesize ty)
+  | _ => accu
+  end.
+
+Definition max_outgoing_2 (accu: Z) (rl: rpair loc) : Z :=
+  match rl with
+  | One l => max_outgoing_1 accu l
+  | Twolong l1 l2 => max_outgoing_1 (max_outgoing_1 accu l1) l2
+  end.
+
+Definition size_arguments (s: signature) : Z :=
+  List.fold_left max_outgoing_2 (loc_arguments s) 0.
+
+(** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
+
+Remark fold_max_outgoing_above:
+  forall l n, fold_left max_outgoing_2 l n >= n.
+Proof.
+  assert (A: forall n l, max_outgoing_1 n l >= n).
+  { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. }
+  induction l; simpl; intros. 
+  - omega.
+  - eapply Zge_trans. eauto.
+    destruct a; simpl. apply A. eapply Zge_trans; eauto.
+Qed.
+
+Lemma size_arguments_above:
+  forall s, size_arguments s >= 0.
+Proof.
+  intros. apply fold_max_outgoing_above.
+Qed.
+
+Lemma loc_arguments_bounded:
+  forall (s: signature) (ofs: Z) (ty: typ),
+  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments s)) ->
+  ofs + typesize ty <= size_arguments s.
+Proof.
+  intros until ty.
+  assert (A: forall n l, n <= max_outgoing_1 n l).
+  { intros; unfold max_outgoing_1. destruct l as [_ | []]; xomega. }
+  assert (B: forall p n,
+             In (S Outgoing ofs ty) (regs_of_rpair p) ->
+             ofs + typesize ty <= max_outgoing_2 n p).
+  { intros. destruct p; simpl in H; intuition; subst; simpl.
+  - xomega.
+  - eapply Z.le_trans. 2: apply A. xomega.
+  - xomega. }
+  assert (C: forall l n,
+             In (S Outgoing ofs ty) (regs_of_rpairs l) ->
+             ofs + typesize ty <= fold_left max_outgoing_2 l n).
+  { induction l; simpl; intros.
+  - contradiction.
+  - rewrite in_app_iff in H. destruct H.
+  + eapply Z.le_trans. eapply B; eauto.
+    apply Z.ge_le. apply fold_max_outgoing_above.
+  + apply IHl; auto.
+  }
+  apply C. 
+Qed.
+
 (** ** Location of function parameters *)
 
 (** A function finds the values of its parameter in the same locations