From 08efc2a09b850476e39469791650faf99dd06183 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavierleroy@users.noreply.github.com>
Date: Mon, 24 Feb 2020 13:56:07 +0100
Subject: 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.
---
 riscV/Conventions1.v | 64 ----------------------------------------------------
 1 file changed, 64 deletions(-)

(limited to 'riscV/Conventions1.v')

diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index 27d09d94..a705c954 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -265,24 +265,6 @@ Fixpoint loc_arguments_rec (va: bool)
 Definition loc_arguments (s: signature) : list (rpair loc) :=
   loc_arguments_rec s.(sig_cc).(cc_vararg) s.(sig_args) 0 0.
 
-(** [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.
-
 (** Argument locations are either non-temporary registers or [Outgoing]
   stack slots at nonnegative offsets. *)
 
@@ -387,52 +369,6 @@ Proof.
   unfold loc_arguments; intros. eapply loc_arguments_rec_charact; eauto. omega.
 Qed.
 
-(** 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.
-
 Lemma loc_arguments_main:
   loc_arguments signature_main = nil.
 Proof.
-- 
cgit