From 5a7acc396131bc452f868d8d913be26240f21cf5 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 26 Aug 2017 19:31:10 +0200 Subject: riscV/Conventions1: in 32-bit mode, wrong size for stack-allocated arguments of type Tfloat A default size of 1 was used instead of the correct "typesize ty". --- riscV/Conventions1.v | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'riscV/Conventions1.v') diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v index 7ce7f7ee..ff993650 100644 --- a/riscV/Conventions1.v +++ b/riscV/Conventions1.v @@ -216,7 +216,7 @@ Definition one_arg (regs: list mreg) (rn: Z) (ofs: Z) (ty: typ) One(R r) :: rec (rn + 1) ofs | None => let ofs := align ofs (typealign ty) in - One(S Outgoing ofs ty) :: rec rn (ofs + (if Archi.ptr64 then 2 else 1)) + One(S Outgoing ofs ty) :: rec rn (ofs + (if Archi.ptr64 then 2 else typesize ty)) end. Definition two_args (regs: list mreg) (rn: Z) (ofs: Z) @@ -310,6 +310,8 @@ Proof. omega. } assert (SK: (if Archi.ptr64 then 2 else 1) > 0). { destruct Archi.ptr64; omega. } + assert (SKK: forall ty, (if Archi.ptr64 then 2 else typesize ty) > 0). + { intros. destruct Archi.ptr64. omega. apply typesize_pos. } assert (A: forall regs rn ofs ty f, OKREGS regs -> OKF f -> ofs >= 0 -> OK (one_arg regs rn ofs ty f)). { intros until f; intros OR OF OO; red; unfold one_arg; intros. @@ -317,7 +319,8 @@ Proof. - subst p; simpl. apply OR. eapply list_nth_z_in; eauto. - eapply OF; eauto. - subst p; simpl. auto using align_divides, typealign_pos. - - eapply OF; [idtac|eauto]. generalize (AL ofs ty OO); omega. + - eapply OF; [idtac|eauto]. + generalize (AL ofs ty OO) (SKK ty); omega. } assert (B: forall regs rn ofs f, OKREGS regs -> OKF f -> ofs >= 0 -> OK (two_args regs rn ofs f)). -- cgit