diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-02-27 10:10:23 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-03-02 10:30:15 +0100 |
| commit | 9190ca38b3ae098186421a7cc21a087666a6a677 (patch) | |
| tree | 2822d34169dfe7c323bcdeab6f32f3c776cd6710 /powerpc | |
| parent | 78d76b65b417b2724cc54a7e5fc5d434d8fc57b5 (diff) | |
| download | compcert-9190ca38b3ae098186421a7cc21a087666a6a677.tar.gz compcert-9190ca38b3ae098186421a7cc21a087666a6a677.zip | |
In strict PPC ABI mode, pass single FP on stack in double FP format
The EABI and the SVR4 ABI state that single-precision FP arguments passed
on stack are passed as a 64-bit word, extended to double-precision.
This commit implements this behavior by using a stack slot of type Tany64.
Not only this ensures that the slot is of size and alignment 8 bytes,
but it also ensures that it is accessed by stfd and lfd instructions,
using single-extended-to-double format.
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Conventions1.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 5639ff8d..5c9cbd4f 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -211,9 +211,9 @@ Fixpoint loc_arguments_rec | Tsingle as ty :: tys => match list_nth_z float_param_regs fr with | None => - let ty := if Archi.single_passed_as_single then Tsingle else Tfloat in + let ty := if Archi.single_passed_as_single then Tsingle else Tany64 in let ofs := align ofs (typesize ty) in - One (S Outgoing ofs Tsingle) :: loc_arguments_rec tys ir fr (ofs + (typesize ty)) + One (S Outgoing ofs ty) :: loc_arguments_rec tys ir fr (ofs + (typesize ty)) | Some freg => One (R freg) :: loc_arguments_rec tys ir (fr + 1) ofs end |