Merge of the float32 branch:

- added RTL type "Tsingle"
- ABI-compatible passing of single-precision floats on ARM and x86


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 21 insertions, 5 deletions

diff --git a/powerpc/eabi/Conventions1.v b/powerpc/eabi/Conventions1.v
index 369a81a..2db1f73 100644
--- a/powerpc/eabi/Conventions1.v
+++ b/powerpc/eabi/Conventions1.v
@@ -240,7 +240,7 @@ Definition loc_result (s: signature) : list mreg :=
   match s.(sig_res) with
   | None => R3 :: nil
   | Some Tint => R3 :: nil
-  | Some Tfloat => F1 :: nil
+  | Some (Tfloat | Tsingle) => F1 :: nil
   | Some Tlong => R3 :: R4 :: nil
   end.
 
@@ -285,7 +285,7 @@ Fixpoint loc_arguments_rec
       | Some ireg =>
           R ireg :: loc_arguments_rec tys (ir + 1) fr ofs
       end
-  | Tfloat :: tys =>
+  | (Tfloat | Tsingle) :: tys =>
       match list_nth_z float_param_regs fr with
       | None =>
           let ofs := align ofs 2 in
@@ -321,7 +321,7 @@ Fixpoint size_arguments_rec (tyl: list typ) (ir fr ofs: Z) {struct tyl} : Z :=
       | None => size_arguments_rec tys ir fr (ofs + 1)
       | Some ireg => size_arguments_rec tys (ir + 1) fr ofs
       end
-  | Tfloat :: tys =>
+  | (Tfloat | Tsingle) :: tys =>
       match list_nth_z float_param_regs fr with
       | None => size_arguments_rec tys ir fr (align ofs 2 + 2)
       | Some freg => size_arguments_rec tys ir (fr + 1) ofs
@@ -396,6 +396,14 @@ Opaque list_nth_z.
   destruct H. subst. split. omega. congruence. 
   destruct H. subst. split. omega. congruence.
   exploit IHtyl; eauto. destruct l; auto. destruct sl; auto. intuition omega. 
+- (* single *)
+  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. 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.
 Qed.
 
 Lemma loc_arguments_acceptable:
@@ -430,6 +438,9 @@ Proof.
   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.
+  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.
 Qed.
 
 Lemma size_arguments_above:
@@ -477,7 +488,12 @@ Proof.
   transitivity (align ofs0 2 + 2). simpl; omega. eauto.  apply size_arguments_rec_above.
   destruct H0. inv H0.
   transitivity (align ofs0 2 + 2). simpl; omega. eauto.  apply size_arguments_rec_above.
-  eauto. 
-}
+  eauto.
+- (* single *)
+  destruct (list_nth_z float_param_regs fr); destruct H0. 
+  congruence.
+  eauto.
+  inv H0. apply size_arguments_rec_above. eauto. 
+  }
   eauto.
 Qed.