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

5 files changed, 36 insertions, 28 deletions

diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 6a1d07e..2b6d80d 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -136,7 +136,7 @@ Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) :=
             Plfd r (Cint ofs) base :: k
           else
             loadimm GPR0 ofs (Plfdx r base GPR0 :: k))
-  | Tlong =>
+  | Tlong | Tsingle =>
       Error (msg "Asmgen.loadind")
   end.
 
@@ -154,7 +154,7 @@ Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) :=
             Pstfd r (Cint ofs) base :: k
           else
             loadimm GPR0 ofs (Pstfdx r base GPR0 :: k))
-  | Tlong =>
+  | Tlong | Tsingle =>
       Error (msg "Asmgen.storeind")
   end.
 
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index e723c86..2c155ea 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -526,9 +526,8 @@ Proof.
   rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR.
   exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]].
   exists rs'; split. eauto.
-  split. change (Mach.undef_regs (destroyed_by_op Omove) rs) with rs. 
-  apply agree_exten with rs0; auto with asmgen.
-  simpl; intros. rewrite Q; auto with asmgen.
+  split. eapply agree_undef_regs; eauto with asmgen.
+  simpl; intros. rewrite Q; auto with asmgen. 
 
 - (* Mgetparam *)
   assert (f0 = f) by congruence; subst f0.
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index ce66e6a..d057dce 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -143,6 +143,12 @@ Definition destroyed_by_builtin (ef: external_function): list mreg :=
   | _ => nil
   end.
 
+Definition destroyed_by_setstack (ty: typ): list mreg :=
+  match ty with
+  | Tsingle => F13 :: nil
+  | _ => nil
+  end.
+
 Definition destroyed_at_function_entry: list mreg :=
   nil.
 
@@ -158,7 +164,7 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list
 Global Opaque
     destroyed_by_op destroyed_by_load destroyed_by_store
     destroyed_by_cond destroyed_by_jumptable destroyed_by_builtin
-    destroyed_at_function_entry temp_for_parent_frame
+    destroyed_by_setstack destroyed_at_function_entry temp_for_parent_frame
     mregs_for_operation mregs_for_builtin.
 
 (** Two-address operations.  Return [true] if the first argument and
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 5835717..3963c6b 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -265,7 +265,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   match op with
   | Omove => (nil, Tint)   (* treated specially *)
   | Ointconst _ => (nil, Tint)
-  | Ofloatconst _ => (nil, Tfloat)
+  | Ofloatconst f => (nil, if Float.is_single_dec f then Tsingle else Tfloat)
   | Oaddrsymbol _ _ => (nil, Tint)
   | Oaddrstack _ => (nil, Tint)
   | Ocast8signed => (Tint :: nil, Tint)
@@ -303,7 +303,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osubf => (Tfloat :: Tfloat :: nil, Tfloat)
   | Omulf => (Tfloat :: Tfloat :: nil, Tfloat)
   | Odivf => (Tfloat :: Tfloat :: nil, Tfloat)
-  | Osingleoffloat => (Tfloat :: nil, Tfloat)
+  | Osingleoffloat => (Tfloat :: nil, Tsingle)
   | Ointoffloat => (Tfloat :: nil, Tint)
   | Ofloatofwords => (Tint :: Tint :: nil, Tfloat)
   | Omakelong => (Tint :: Tint :: nil, Tlong)
@@ -340,7 +340,7 @@ Proof with (try exact I).
   destruct op; simpl in H0; FuncInv; subst; simpl.
   congruence.
   exact I.
-  exact I.
+  destruct (Float.is_single_dec f); auto. 
   unfold symbol_address. destruct (Genv.find_symbol genv i)...
   destruct sp...
   destruct v0...
@@ -380,7 +380,7 @@ Proof with (try exact I).
   destruct v0; destruct v1...
   destruct v0; destruct v1...
   destruct v0; destruct v1...
-  destruct v0...
+  destruct v0... simpl. apply Float.singleoffloat_is_single.
   destruct v0; simpl in H0; inv H0. destruct (Float.intoffloat f); inv H2...
   destruct v0; destruct v1...
   destruct v0; destruct v1...
@@ -389,19 +389,6 @@ Proof with (try exact I).
   destruct (eval_condition c vl m); simpl... destruct b... 
 Qed.
 
-Lemma type_of_chunk_correct:
-  forall chunk m addr v,
-  Mem.loadv chunk m addr = Some v ->
-  Val.has_type v (type_of_chunk chunk).
-Proof.
-  intro chunk.
-  assert (forall v, Val.has_type (Val.load_result chunk v) (type_of_chunk chunk)).
-  destruct v; destruct chunk; exact I.
-  intros until v. unfold Mem.loadv. 
-  destruct addr; intros; try discriminate.
-  eapply Mem.load_type; eauto.
-Qed.
-
 End SOUNDNESS.
 
 (** * Manipulating and transforming operations *)
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.