diff options
author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-02-24 13:56:07 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-24 13:56:07 +0100 |
commit | 08efc2a09b850476e39469791650faf99dd06183 (patch) | |
tree | f83f23a30d7e374a2b1f3b616e1bcb7396498baf | |
parent | 3bdb983e0b21c8d45e85aff08278475396038f4f (diff) | |
download | compcert-kvx-08efc2a09b850476e39469791650faf99dd06183.tar.gz compcert-kvx-08efc2a09b850476e39469791650faf99dd06183.zip |
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.
-rw-r--r-- | aarch64/Conventions1.v | 107 | ||||
-rw-r--r-- | arm/Conventions1.v | 206 | ||||
-rw-r--r-- | backend/Conventions.v | 67 | ||||
-rw-r--r-- | powerpc/Conventions1.v | 126 | ||||
-rw-r--r-- | riscV/Conventions1.v | 64 | ||||
-rw-r--r-- | x86/Asmexpand.ml | 2 | ||||
-rw-r--r-- | x86/Conventions1.v | 145 |
7 files changed, 68 insertions, 649 deletions
diff --git a/aarch64/Conventions1.v b/aarch64/Conventions1.v index 14cb199f..efda835d 100644 --- a/aarch64/Conventions1.v +++ b/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. diff --git a/arm/Conventions1.v b/arm/Conventions1.v index 7016c1ee..fe49a781 100644 --- a/arm/Conventions1.v +++ b/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. 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 diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 25d9c081..1f048694 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -236,33 +236,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 | Tany32) :: tys => - match list_nth_z int_param_regs ir with - | None => size_arguments_rec tys ir fr (ofs + 1) - | Some ireg => size_arguments_rec tys (ir + 1) fr ofs - end - | (Tfloat | Tsingle | Tany64) :: tys => - match list_nth_z float_param_regs fr with - | None => size_arguments_rec tys ir fr (align ofs 2 + 2) - | Some freg => size_arguments_rec tys ir (fr + 1) ofs - end - | Tlong :: tys => - let ir := align ir 2 in - match list_nth_z int_param_regs ir, list_nth_z int_param_regs (ir + 1) with - | Some r1, Some r2 => size_arguments_rec tys (ir + 2) fr ofs - | _, _ => size_arguments_rec tys ir fr (align ofs 2 + 2) - 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. *) @@ -359,105 +332,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. - destruct a. - destruct (list_nth_z int_param_regs ir); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. - destruct (list_nth_z float_param_regs fr); 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 (list_nth_z int_param_regs ir'); eauto. - destruct (list_nth_z int_param_regs (ir' + 1)); eauto. - apply Z.le_trans with (align ofs0 2). apply align_le; omega. - apply Z.le_trans with (align ofs0 2 + 2); auto; omega. - apply Z.le_trans with (align ofs0 2). apply align_le; omega. - apply Z.le_trans with (align ofs0 2 + 2); auto; omega. - destruct (list_nth_z float_param_regs fr); 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 (list_nth_z int_param_regs ir); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega. - destruct (list_nth_z float_param_regs fr); 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. - -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_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. - assert (forall 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). -{ - induction tyl; simpl; intros. - elim H0. - destruct a. -- (* int *) - destruct (list_nth_z int_param_regs ir); destruct H0. - congruence. - eauto. - inv H0. apply size_arguments_rec_above. - eauto. -- (* float *) - destruct (list_nth_z float_param_regs fr); destruct H0. - congruence. - eauto. - inv H0. apply size_arguments_rec_above. eauto. -- (* long *) - set (ir' := align ir 2) in *. - assert (DFL: - In (S Outgoing ofs ty) (regs_of_rpairs - ((if Archi.ptr64 - then One (S Outgoing (align ofs0 2) Tlong) - else Twolong (S Outgoing (align ofs0 2) Tint) - (S Outgoing (align ofs0 2 + 1) Tint)) - :: loc_arguments_rec tyl ir' fr (align ofs0 2 + 2))) -> - ofs + typesize ty <= size_arguments_rec tyl ir' fr (align ofs0 2 + 2)). - { destruct Archi.ptr64; intros IN. - - destruct IN. inv H1. apply size_arguments_rec_above. auto. - - destruct IN. inv H1. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above. - destruct H1. inv H1. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above. - auto. } - destruct (list_nth_z int_param_regs ir'); auto. - destruct (list_nth_z int_param_regs (ir' + 1)); auto. - destruct H0. congruence. destruct H0. congruence. eauto. -- (* single *) - destruct (list_nth_z float_param_regs fr); destruct H0. - congruence. - eauto. - inv H0. transitivity (align ofs0 2 + 2). simpl; omega. apply size_arguments_rec_above. - eauto. -- (* any32 *) - destruct (list_nth_z int_param_regs ir); destruct H0. - congruence. - eauto. - inv H0. apply size_arguments_rec_above. - eauto. -- (* any64 *) - destruct (list_nth_z float_param_regs fr); destruct H0. - congruence. - eauto. - inv H0. apply size_arguments_rec_above. eauto. - } - eauto. -Qed. - Lemma loc_arguments_main: loc_arguments signature_main = nil. Proof. 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. diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml index c82d406e..b8353046 100644 --- a/x86/Asmexpand.ml +++ b/x86/Asmexpand.ml @@ -251,7 +251,7 @@ let expand_builtin_va_start_32 r = invalid_arg "Fatal error: va_start used in non-vararg function"; let ofs = Int32.(add (add !PrintAsmaux.current_function_stacksize 4l) - (mul 4l (Z.to_int32 (Conventions1.size_arguments + (mul 4l (Z.to_int32 (Conventions.size_arguments (get_current_function_sig ()))))) in emit (Pleal (RAX, linear_addr RSP (Z.of_uint32 ofs))); emit (Pmovl_mr (linear_addr r _0z, RAX)) diff --git a/x86/Conventions1.v b/x86/Conventions1.v index 01b15e98..fdd94239 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -220,36 +220,6 @@ Definition loc_arguments (s: signature) : list (rpair loc) := then loc_arguments_64 s.(sig_args) 0 0 0 else loc_arguments_32 s.(sig_args) 0. -(** [size_arguments s] returns the number of [Outgoing] slots used - to call a function with signature [s]. *) - -Fixpoint size_arguments_32 - (tyl: list typ) (ofs: Z) {struct tyl} : Z := - match tyl with - | nil => ofs - | ty :: tys => size_arguments_32 tys (ofs + typesize ty) - end. - -Fixpoint size_arguments_64 (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_64 tys ir fr (ofs + 2) - | Some ireg => size_arguments_64 tys (ir + 1) fr ofs - end - | (Tfloat | Tsingle) :: tys => - match list_nth_z float_param_regs fr with - | None => size_arguments_64 tys ir fr (ofs + 2) - | Some freg => size_arguments_64 tys ir (fr + 1) ofs - end - end. - -Definition size_arguments (s: signature) : Z := - if Archi.ptr64 - then size_arguments_64 s.(sig_args) 0 0 0 - else size_arguments_32 s.(sig_args) 0. - (** Argument locations are either caller-save registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -351,121 +321,6 @@ Qed. Hint Resolve loc_arguments_acceptable: locs. -(** The offsets of [Outgoing] arguments are below [size_arguments s]. *) - -Remark size_arguments_32_above: - forall tyl ofs0, ofs0 <= size_arguments_32 tyl ofs0. -Proof. - induction tyl; simpl; intros. - omega. - apply Z.le_trans with (ofs0 + typesize a); auto. - generalize (typesize_pos a); omega. -Qed. - -Remark size_arguments_64_above: - forall tyl ir fr ofs0, - ofs0 <= size_arguments_64 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_64 tyl (ir + 1) fr ofs0 - | None => size_arguments_64 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_64 tyl ir (fr + 1) ofs0 - | None => size_arguments_64 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. - destruct Archi.ptr64; [apply size_arguments_64_above|apply size_arguments_32_above]. -Qed. - -Lemma loc_arguments_32_bounded: - forall ofs ty tyl ofs0, - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_32 tyl ofs0)) -> - ofs + typesize ty <= size_arguments_32 tyl ofs0. -Proof. - induction tyl as [ | t l]; simpl; intros x IN. -- contradiction. -- rewrite in_app_iff in IN; destruct IN as [IN|IN]. -+ apply Z.le_trans with (x + typesize t); [|apply size_arguments_32_above]. - Ltac decomp := - match goal with - | [ H: _ \/ _ |- _ ] => destruct H; decomp - | [ H: S _ _ _ = S _ _ _ |- _ ] => inv H - | [ H: False |- _ ] => contradiction - end. - destruct t; simpl in IN; decomp; simpl; omega. -+ apply IHl; auto. -Qed. - -Lemma loc_arguments_64_bounded: - forall ofs ty tyl ir fr ofs0, - In (S Outgoing ofs ty) (regs_of_rpairs (loc_arguments_64 tyl ir fr ofs0)) -> - ofs + typesize ty <= size_arguments_64 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_64 tyl (ir + 1) fr ofs0 - | None => One (S Outgoing ofs0 ty0) :: loc_arguments_64 tyl ir fr (ofs0 + 2) - end) -> - ofs + typesize ty <= - match list_nth_z int_param_regs ir with - | Some _ => size_arguments_64 tyl (ir + 1) fr ofs0 - | None => size_arguments_64 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_64_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_64 tyl ir (fr + 1) ofs0 - | None => One (S Outgoing ofs0 ty0) :: loc_arguments_64 tyl ir fr (ofs0 + 2) - end) -> - ofs + typesize ty <= - match list_nth_z float_param_regs fr with - | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0 - | None => size_arguments_64 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_64_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. - destruct Archi.ptr64; eauto using loc_arguments_32_bounded, loc_arguments_64_bounded. -Qed. - Lemma loc_arguments_main: loc_arguments signature_main = nil. Proof. |