diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2020-02-24 19:59:43 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-03-02 10:30:15 +0100 |
| commit | e66be6e05b190c51b38d628884ef3e015ebf73fd (patch) | |
| tree | 4a2e85c65530596418981238e5672998d5ad0857 /powerpc | |
| parent | 5003b8d93c2a20821b776f7f74f5096a308a03cf (diff) | |
| download | compcert-e66be6e05b190c51b38d628884ef3e015ebf73fd.tar.gz compcert-e66be6e05b190c51b38d628884ef3e015ebf73fd.zip | |
Make single arg alignment depend on toolchain.
GCC does passes single arguments as singles on the stack but diab
and the eabi say single arguments should be passed as double on
the stack.
This commit changes the alignment of single arguments to 4 for
gcc based backends.
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Archi.v | 3 | ||||
| -rw-r--r-- | powerpc/Conventions1.v | 17 | ||||
| -rw-r--r-- | powerpc/extractionMachdep.v | 3 |
3 files changed, 20 insertions, 3 deletions
diff --git a/powerpc/Archi.v b/powerpc/Archi.v index ab348c14..88fff302 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -30,6 +30,9 @@ Definition align_float64 := 8%Z. (** Can we use the 64-bit extensions to the PowerPC architecture? *) Parameter ppc64 : bool. +(** Should singles be passed as single or double *) +Parameter single_passed_as_single : bool. + Definition splitlong := negb ppc64. Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 1f048694..5639ff8d 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -208,7 +208,16 @@ Fixpoint loc_arguments_rec | Some ireg => One (R ireg) :: loc_arguments_rec tys (ir + 1) fr ofs end - | (Tfloat | Tsingle | Tany64) as ty :: tys => + | 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 ofs := align ofs (typesize ty) in + One (S Outgoing ofs Tsingle) :: loc_arguments_rec tys ir fr (ofs + (typesize ty)) + | Some freg => + One (R freg) :: loc_arguments_rec tys ir (fr + 1) ofs + end + | (Tfloat | Tany64) as ty :: tys => match list_nth_z float_param_regs fr with | None => let ofs := align ofs 2 in @@ -295,12 +304,14 @@ Opaque list_nth_z. apply align_divides; omega. apply Z.divide_1_l. apply Z.divide_1_l. eapply Y; eauto. omega. - (* single *) + assert (ofs <= align ofs 1) by (apply align_le; omega). assert (ofs <= align ofs 2) by (apply align_le; omega). 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. apply Z.divide_1_l. - eapply Y; eauto. omega. + subst. split. destruct Archi.single_passed_as_single; simpl; omega. + destruct Archi.single_passed_as_single; simpl; apply Z.divide_1_l. + eapply Y; eauto. destruct Archi.single_passed_as_single; simpl; omega. - (* any32 *) destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H. subst. left. eapply list_nth_z_in; eauto. diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v index 7482435f..a3e945bf 100644 --- a/powerpc/extractionMachdep.v +++ b/powerpc/extractionMachdep.v @@ -34,3 +34,6 @@ Extract Constant Archi.ppc64 => | ""e5500"" -> true | _ -> false end". + +(* Choice of passing of single *) +Extract Constant Archi.single_passed_as_single => "Configuration.gnu_toolchain". |