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.

Author: xavierleroy

aarch64/Conventions1.v

@@ -190,27 +190,6 @@ Fixpoint loc_arguments_rec
 Definition loc_arguments (s: signature) : list (rpair loc) :=
   loc_arguments_rec s.(sig_args) 0 0 0.
 
-(** [size_arguments s] returns the number of [Outgoing] slots used
-  to call a function with signature [s]. *)
-
-Fixpoint size_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z :=
-  match tyl with
-  | nil => ofs
-  | (Tint | Tlong | Tany32 | Tany64) :: tys =>
-      match list_nth_z int_param_regs ir with
-      | None => size_arguments_rec tys ir fr (ofs + 2)
-      | Some ireg => size_arguments_rec tys (ir + 1) fr ofs
-      end
-  | (Tfloat | Tsingle) :: tys =>
-      match list_nth_z float_param_regs fr with
-      | None => size_arguments_rec tys ir fr (ofs + 2)
-      | Some freg => size_arguments_rec tys ir (fr + 1) ofs
-      end
-  end.
-
-Definition size_arguments (s: signature) : Z :=
-  size_arguments_rec s.(sig_args) 0 0 0.
-
 (** Argument locations are either caller-save registers or [Outgoing]
   stack slots at nonnegative offsets. *)
 
@@ -285,92 +264,6 @@ Qed.
 
 Hint Resolve loc_arguments_acceptable: locs.
 
-(** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
-
-Remark size_arguments_rec_above:
-  forall tyl ir fr ofs0,
-  ofs0 <= size_arguments_rec tyl ir fr ofs0.
-Proof.
-  induction tyl; simpl; intros.
-  omega.
-  assert (A: ofs0 <=
-    match list_nth_z int_param_regs ir with
-    | Some _ => size_arguments_rec tyl (ir + 1) fr ofs0
-    | None => size_arguments_rec tyl ir fr (ofs0 + 2)
-    end).
-  { destruct (list_nth_z int_param_regs ir); eauto.
-    apply Z.le_trans with (ofs0 + 2); auto. omega. }
-  assert (B: ofs0 <=
-    match list_nth_z float_param_regs fr with
-    | Some _ => size_arguments_rec tyl ir (fr + 1) ofs0
-    | None => size_arguments_rec tyl ir fr (ofs0 + 2)
-    end).
-  { destruct (list_nth_z float_param_regs fr); eauto.
-    apply Z.le_trans with (ofs0 + 2); auto. omega. }
-  destruct a; auto.
-Qed.
-
-Lemma size_arguments_above:
-  forall s, size_arguments s >= 0.
-Proof.
-  intros; unfold size_arguments. apply Z.le_ge. apply size_arguments_rec_above.
-Qed.
-
-Lemma loc_arguments_rec_bounded:
-  forall ofs ty tyl ir fr ofs0,
-  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_rec tyl ir fr ofs0)) ->
-  ofs + typesize ty <= size_arguments_rec tyl ir fr ofs0.
-Proof.
-  induction tyl; simpl; intros.
-- contradiction.
-- assert (T: forall ty0, typesize ty0 <= 2).
-  { destruct ty0; simpl; omega. }
-  assert (A: forall ty0,
-             In (S Outgoing ofs ty) (regs_of_rpairs
-              match list_nth_z int_param_regs ir with
-              | Some ireg =>
-                  One (R ireg) :: loc_arguments_rec tyl (ir + 1) fr ofs0
-              | None => One (S Outgoing ofs0 ty0) :: loc_arguments_rec tyl ir fr (ofs0 + 2)
-              end) ->
-             ofs + typesize ty <=
-             match list_nth_z int_param_regs ir with
-             | Some _ => size_arguments_rec tyl (ir + 1) fr ofs0
-             | None => size_arguments_rec tyl ir fr (ofs0 + 2)
-             end).
-  { intros. destruct (list_nth_z int_param_regs ir); simpl in H0; destruct H0.
-  - discriminate.
-  - eapply IHtyl; eauto.
-  - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_rec_above.
-  - eapply IHtyl; eauto. }
-  assert (B: forall ty0,
-             In (S Outgoing ofs ty) (regs_of_rpairs
-              match list_nth_z float_param_regs fr with
-              | Some ireg =>
-                  One (R ireg) :: loc_arguments_rec tyl ir (fr + 1) ofs0
-              | None => One (S Outgoing ofs0 ty0) :: loc_arguments_rec tyl ir fr (ofs0 + 2)
-              end) ->
-             ofs + typesize ty <=
-             match list_nth_z float_param_regs fr with
-             | Some _ => size_arguments_rec tyl ir (fr + 1) ofs0
-             | None => size_arguments_rec tyl ir fr (ofs0 + 2)
-             end).
-  { intros. destruct (list_nth_z float_param_regs fr); simpl in H0; destruct H0.
-  - discriminate.
-  - eapply IHtyl; eauto.
-  - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_rec_above.
-  - eapply IHtyl; eauto. }
-  destruct a; eauto.
-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.
-  unfold loc_arguments, size_arguments; intros.
-  eauto using loc_arguments_rec_bounded.
-Qed.
-
 Lemma loc_arguments_main:
   loc_arguments signature_main = nil.
 Proof.

arm/Conventions1.v

@@ -269,48 +269,6 @@ Definition loc_arguments (s: signature) : list (rpair loc) :=
       else loc_arguments_hf s.(sig_args) 0 0 0
   end.
 
-(** [size_arguments s] returns the number of [Outgoing] slots used
-  to call a function with signature [s]. *)
-
-Fixpoint size_arguments_hf (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z :=
-  match tyl with
-  | nil => ofs
-  | (Tint|Tany32) :: tys =>
-      if zlt ir 4
-      then size_arguments_hf tys (ir + 1) fr ofs
-      else size_arguments_hf tys ir fr (ofs + 1)
-  | (Tfloat|Tany64) :: tys =>
-      if zlt fr 8
-      then size_arguments_hf tys ir (fr + 1) ofs
-      else size_arguments_hf tys ir fr (align ofs 2 + 2)
-  | Tsingle :: tys =>
-      if zlt fr 8
-      then size_arguments_hf tys ir (fr + 1) ofs
-      else size_arguments_hf tys ir fr (ofs + 1)
-  | Tlong :: tys =>
-      let ir := align ir 2 in
-      if zlt ir 4
-      then size_arguments_hf tys (ir + 2) fr ofs
-      else size_arguments_hf tys ir fr (align ofs 2 + 2)
-  end.
-
-Fixpoint size_arguments_sf (tyl: list typ) (ofs: Z) {struct tyl} : Z :=
-  match tyl with
-  | nil => Z.max 0 ofs
-  | (Tint | Tsingle | Tany32) :: tys => size_arguments_sf tys (ofs + 1)
-  | (Tfloat | Tlong | Tany64) :: tys => size_arguments_sf tys (align ofs 2 + 2)
-  end.
-
-Definition size_arguments (s: signature) : Z :=
-  match Archi.abi with
-  | Archi.Softfloat =>
-      size_arguments_sf s.(sig_args) (-4)
-  | Archi.Hardfloat =>
-      if s.(sig_cc).(cc_vararg)
-      then size_arguments_sf s.(sig_args) (-4)
-      else size_arguments_hf s.(sig_args) 0 0 0
-  end.
-
 (** Argument locations are either non-temporary registers or [Outgoing]
   stack slots at nonnegative offsets. *)
 
@@ -471,170 +429,6 @@ Qed.
 
 Hint Resolve loc_arguments_acceptable: locs.
 
-(** The offsets of [Outgoing] arguments are below [size_arguments s]. *)
-
-Remark size_arguments_hf_above:
-  forall tyl ir fr ofs0,
-  ofs0 <= size_arguments_hf tyl ir fr ofs0.
-Proof.
-  induction tyl; simpl; intros.
-  omega.
-  destruct a.
-  destruct (zlt ir 4); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega.
-  destruct (zlt fr 8); eauto.
-  apply Z.le_trans with (align ofs0 2). apply align_le; omega.
-  apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
-  set (ir' := align ir 2).
-  destruct (zlt ir' 4); eauto.
-  apply Z.le_trans with (align ofs0 2). apply align_le; omega.
-  apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
-  destruct (zlt fr 8); eauto.
-  apply Z.le_trans with (ofs0 + 1); eauto. omega.
-  destruct (zlt ir 4); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega.
-  destruct (zlt fr 8); eauto.
-  apply Z.le_trans with (align ofs0 2). apply align_le; omega.
-  apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
-Qed.
-
-Remark size_arguments_sf_above:
-  forall tyl ofs0,
-  Z.max 0 ofs0 <= size_arguments_sf tyl ofs0.
-Proof.
-  induction tyl; simpl; intros.
-  omega.
-  destruct a; (eapply Z.le_trans; [idtac|eauto]).
-  xomega.
-  assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega.
-  assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega.
-  xomega.
-  xomega.
-  assert (ofs0 <= align ofs0 2) by (apply align_le; omega). xomega.
-Qed.
-
-Lemma size_arguments_above:
-  forall s, size_arguments s >= 0.
-Proof.
-  intros; unfold size_arguments. apply Z.le_ge.
-  assert (0 <= size_arguments_sf (sig_args s) (-4)).
-  { change 0 with (Z.max 0 (-4)). apply size_arguments_sf_above. }
-  assert (0 <= size_arguments_hf (sig_args s) 0 0 0).
-  { apply size_arguments_hf_above. }
-  destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; auto.
-Qed.
-
-Lemma loc_arguments_hf_bounded:
-  forall ofs ty tyl ir fr ofs0,
-  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_hf tyl ir fr ofs0)) ->
-  ofs + typesize ty <= size_arguments_hf tyl ir fr ofs0.
-Proof.
-  induction tyl; simpl; intros.
-  elim H.
-  destruct a.
-- (* int *)
-  destruct (zlt ir 4); destruct H.
-  discriminate.
-  eauto.
-  inv H. apply size_arguments_hf_above.
-  eauto.
-- (* float *)
-  destruct (zlt fr 8); destruct H.
-  discriminate.
-  eauto.
-  inv H. apply size_arguments_hf_above.
-  eauto.
-- (* long *)
-  destruct (zlt (align ir 2) 4).
-  destruct H. discriminate. destruct H. discriminate. eauto.
-  destruct Archi.big_endian.
-  destruct H. inv H.
-  eapply Z.le_trans. 2: apply size_arguments_hf_above. simpl; omega.
-  destruct H. inv H.
-  rewrite <- Z.add_assoc. simpl. apply size_arguments_hf_above.
-  eauto.
-  destruct H. inv H.
-  rewrite <- Z.add_assoc. simpl. apply size_arguments_hf_above.
-  destruct H. inv H.
-  eapply Z.le_trans. 2: apply size_arguments_hf_above. simpl; omega.
-  eauto.
-- (* float *)
-  destruct (zlt fr 8); destruct H.
-  discriminate.
-  eauto.
-  inv H. apply size_arguments_hf_above.
-  eauto.
-- (* any32 *)
-  destruct (zlt ir 4); destruct H.
-  discriminate.
-  eauto.
-  inv H. apply size_arguments_hf_above.
-  eauto.
-- (* any64 *)
-  destruct (zlt fr 8); destruct H.
-  discriminate.
-  eauto.
-  inv H. apply size_arguments_hf_above.
-  eauto.
-Qed.
-
-Lemma loc_arguments_sf_bounded:
-  forall ofs ty tyl ofs0,
-  In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf tyl ofs0)) ->
-  Z.max 0 (ofs + typesize ty) <= size_arguments_sf tyl ofs0.
-Proof.
-  induction tyl; simpl; intros.
-  elim H.
-  destruct a.
-- (* int *)
-  destruct H.
-  destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above.
-  eauto.
-- (* float *)
-  destruct H.
-  destruct (zlt (align ofs0 2) 0); inv H. apply size_arguments_sf_above.
-  eauto.
-- (* long *)
-  destruct H.
-  destruct Archi.big_endian.
-  destruct (zlt (align ofs0 2) 0); inv H.
-  eapply Z.le_trans. 2: apply size_arguments_sf_above. simpl; xomega.
-  destruct (zlt (align ofs0 2) 0); inv H.
-  rewrite <- Z.add_assoc. simpl. apply size_arguments_sf_above.
-  destruct H.
-  destruct Archi.big_endian.
-  destruct (zlt (align ofs0 2) 0); inv H.
-  rewrite <- Z.add_assoc. simpl. apply size_arguments_sf_above.
-  destruct (zlt (align ofs0 2) 0); inv H.
-  eapply Z.le_trans. 2: apply size_arguments_sf_above. simpl; xomega.
-  eauto.
-- (* float *)
-  destruct H.
-  destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above.
-  eauto.
-- (* any32 *)
-  destruct H.
-  destruct (zlt ofs0 0); inv H. apply size_arguments_sf_above.
-  eauto.
-- (* any64 *)
-  destruct H.
-  destruct (zlt (align ofs0 2) 0); inv H. apply size_arguments_sf_above.
-  eauto.
-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.
-  unfold loc_arguments, size_arguments; intros.
-  assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_sf (sig_args s) (-4))) ->
-          ofs + typesize ty <= size_arguments_sf (sig_args s) (-4)).
-  { intros. eapply Z.le_trans. 2: eapply loc_arguments_sf_bounded; eauto. xomega. }
-  assert (In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_hf (sig_args s) 0 0 0)) ->
-          ofs + typesize ty <= size_arguments_hf (sig_args s) 0 0 0).
-  { intros. eapply loc_arguments_hf_bounded; eauto. }
-  destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; eauto.
-Qed.
-
 Lemma loc_arguments_main:
   loc_arguments signature_main = nil.
 Proof.