summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-05-02 15:03:58 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2013-05-02 15:03:58 +0000
commit850524f31aef255418db8fa2b0f25050b0535b82 (patch)
tree3427dc3ff3b8932ba4d4b560436ec097ac0fd46c
parent84b0112efdff702b1774287626ee56812f0cb953 (diff)
Stack-align to 8 arguments of Tfloat and Tlong types, as per the SVR4 ABI and the EABI.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2230 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
-rw-r--r--powerpc/eabi/Conventions1.v48
1 files changed, 32 insertions, 16 deletions
diff --git a/powerpc/eabi/Conventions1.v b/powerpc/eabi/Conventions1.v
index 8ff0dc0..369a81a 100644
--- a/powerpc/eabi/Conventions1.v
+++ b/powerpc/eabi/Conventions1.v
@@ -288,6 +288,7 @@ Fixpoint loc_arguments_rec
| Tfloat :: tys =>
match list_nth_z float_param_regs fr with
| None =>
+ let ofs := align ofs 2 in
S Outgoing ofs Tfloat :: loc_arguments_rec tys ir fr (ofs + 2)
| Some freg =>
R freg :: loc_arguments_rec tys ir (fr + 1) ofs
@@ -298,6 +299,7 @@ Fixpoint loc_arguments_rec
| Some r1, Some r2 =>
R r1 :: R r2 :: loc_arguments_rec tys (ir + 2) fr ofs
| _, _ =>
+ let ofs := align ofs 2 in
S Outgoing ofs Tint :: S Outgoing (ofs + 1) Tint :: loc_arguments_rec tys ir fr (ofs + 2)
end
end.
@@ -321,18 +323,17 @@ Fixpoint size_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z :=
end
| Tfloat :: tys =>
match list_nth_z float_param_regs fr with
- | None => size_arguments_rec tys ir fr (ofs + 2)
+ | 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 (ofs + 2)
+ | _, _ => 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.
@@ -366,25 +367,32 @@ Opaque list_nth_z.
induction tyl; simpl loc_arguments_rec; intros.
elim H.
destruct a.
- destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H.
+- (* int *)
+ destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H.
subst. left. eapply list_nth_z_in; eauto.
eapply IHtyl; eauto.
subst. split. omega. congruence.
exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
+- (* float *)
destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H.
subst. right. eapply list_nth_z_in; eauto.
eapply IHtyl; eauto.
- subst. split. omega. congruence.
- exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
+ subst. split. apply Zle_ge. apply align_le. omega. congruence.
+ exploit IHtyl; eauto. destruct l; auto. destruct sl; auto.
+ assert (ofs <= align ofs 2) by (apply align_le; omega).
+ intuition omega.
+- (* long *)
set (ir' := align ir 2) in *.
destruct (list_nth_z int_param_regs ir') as [r1|] eqn:E1.
destruct (list_nth_z int_param_regs (ir' + 1)) as [r2|] eqn:E2.
destruct H. subst; left; eapply list_nth_z_in; eauto.
destruct H. subst; left; eapply list_nth_z_in; eauto.
eapply IHtyl; eauto.
+ assert (ofs <= align ofs 2) by (apply align_le; omega).
destruct H. subst. split. omega. congruence.
destruct H. subst. split. omega. congruence.
- exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
+ exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
+ assert (ofs <= align ofs 2) by (apply align_le; omega).
destruct H. subst. split. omega. congruence.
destruct H. subst. split. omega. congruence.
exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega.
@@ -412,12 +420,16 @@ Proof.
omega.
destruct a.
destruct (list_nth_z int_param_regs ir); eauto. apply Zle_trans with (ofs0 + 1); auto; omega.
- destruct (list_nth_z float_param_regs fr); eauto. apply Zle_trans with (ofs0 + 2); auto; omega.
+ destruct (list_nth_z float_param_regs fr); eauto.
+ apply Zle_trans with (align ofs0 2). apply align_le; omega.
+ apply Zle_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 Zle_trans with (ofs0 + 2); auto; omega.
- apply Zle_trans with (ofs0 + 2); auto; omega.
+ apply Zle_trans with (align ofs0 2). apply align_le; omega.
+ apply Zle_trans with (align ofs0 2 + 2); auto; omega.
+ apply Zle_trans with (align ofs0 2). apply align_le; omega.
+ apply Zle_trans with (align ofs0 2 + 2); auto; omega.
Qed.
Lemma size_arguments_above:
@@ -436,32 +448,36 @@ Proof.
assert (forall tyl ir fr ofs0,
In (S Outgoing ofs ty) (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.
+ inv H0. apply size_arguments_rec_above. eauto.
+- (* long *)
set (ir' := align ir 2) in *.
destruct (list_nth_z int_param_regs ir').
destruct (list_nth_z int_param_regs (ir' + 1)).
destruct H0. congruence. destruct H0. congruence. eauto.
destruct H0. inv H0.
- transitivity (ofs + 2). simpl; omega. eauto. apply size_arguments_rec_above.
+ transitivity (align ofs0 2 + 2). simpl; omega. eauto. apply size_arguments_rec_above.
destruct H0. inv H0.
- transitivity (ofs0 + 2). simpl; omega. eauto. apply size_arguments_rec_above.
+ transitivity (align ofs0 2 + 2). simpl; omega. eauto. apply size_arguments_rec_above.
eauto.
destruct H0. inv H0.
- transitivity (ofs + 2). simpl; omega. eauto. apply size_arguments_rec_above.
+ transitivity (align ofs0 2 + 2). simpl; omega. eauto. apply size_arguments_rec_above.
destruct H0. inv H0.
- transitivity (ofs0 + 2). simpl; omega. eauto. apply size_arguments_rec_above.
+ transitivity (align ofs0 2 + 2). simpl; omega. eauto. apply size_arguments_rec_above.
eauto.
+}
eauto.
Qed.