diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-26 19:31:10 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-08-26 19:31:10 +0200 |
| commit | 5a7acc396131bc452f868d8d913be26240f21cf5 (patch) | |
| tree | dcb842844b730da2a6d28b96b72277553c19d6d2 /riscV/Conventions1.v | |
| parent | ae3ff874f99fcde33901ac13f4ee9ea23aa984e5 (diff) | |
| download | compcert-kvx-5a7acc396131bc452f868d8d913be26240f21cf5.tar.gz compcert-kvx-5a7acc396131bc452f868d8d913be26240f21cf5.zip | |
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".
Diffstat (limited to 'riscV/Conventions1.v')
| -rw-r--r-- | riscV/Conventions1.v | 7 |
1 files changed, 5 insertions, 2 deletions
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)). |