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

2 files changed, 8 insertions, 1 deletions

diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index a19a0e2..70a02c1 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -104,6 +104,7 @@ Definition eventval_of_val (v: val) (t: typ) : option eventval :=
   match v, t with
   | Vint i, AST.Tint => Some (EVint i)
   | Vfloat f, AST.Tfloat => Some (EVfloat f)
+  | Vfloat f, AST.Tsingle => if Float.is_single_dec f then Some (EVfloatsingle f) else None
   | Vlong n, AST.Tlong => Some (EVlong n)
   | Vptr b ofs, AST.Tint => do id <- Genv.invert_symbol ge b; Some (EVptr_global id ofs)
   | _, _ => None
@@ -123,6 +124,7 @@ Definition val_of_eventval (ev: eventval) (t: typ) : option val :=
   match ev, t with
   | EVint i, AST.Tint => Some (Vint i)
   | EVfloat f, AST.Tfloat => Some (Vfloat f)
+  | EVfloatsingle f, AST.Tsingle => if Float.is_single_dec f then Some (Vfloat f) else None
   | EVlong n, AST.Tlong => Some (Vlong n)
   | EVptr_global id ofs, AST.Tint => do b <- Genv.find_symbol ge id; Some (Vptr b ofs)
   | _, _ => None
@@ -135,6 +137,7 @@ Proof.
   constructor.
   constructor.
   constructor.
+  destruct (Float.is_single_dec f); inv H1. constructor; auto.
   destruct (Genv.invert_symbol ge b) as [id|] eqn:?; inv H1. 
   constructor. apply Genv.invert_find_symbol; auto.
 Qed.
@@ -143,6 +146,7 @@ Lemma eventval_of_val_complete:
   forall ev t v, eventval_match ge ev t v -> eventval_of_val v t = Some ev.
 Proof.
   induction 1; simpl; auto.
+  rewrite pred_dec_true; auto.
   rewrite (Genv.find_invert_symbol _ _ H). auto. 
 Qed.
 
@@ -170,6 +174,7 @@ Proof.
   constructor.
   constructor.
   constructor.
+  destruct (Float.is_single_dec f); inv H1. constructor; auto.
   destruct (Genv.find_symbol ge i) as [b|] eqn:?; inv H1.
   constructor. auto.
 Qed.
@@ -177,7 +182,7 @@ Qed.
 Lemma val_of_eventval_complete:
   forall ev t v, eventval_match ge ev t v -> val_of_eventval ev t = Some v.
 Proof.
-  induction 1; simpl; auto. rewrite H; auto.
+  induction 1; simpl; auto. rewrite pred_dec_true; auto. rewrite H; auto.
 Qed.
 
 (** Volatile memory accesses. *)
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index bf483a0..8d00b95 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -530,6 +530,7 @@ Fixpoint type_of_params (params: list (ident * type)) : typelist :=
 
 Definition typ_of_type (t: type) : AST.typ :=
   match t with
+  | Tfloat F32 _ => AST.Tsingle
   | Tfloat _ _ => AST.Tfloat
   | Tlong _ _ => AST.Tlong
   | _ => AST.Tint
@@ -538,6 +539,7 @@ Definition typ_of_type (t: type) : AST.typ :=
 Definition opttyp_of_type (t: type) : option AST.typ :=
   match t with
   | Tvoid => None
+  | Tfloat F32 _ => Some AST.Tsingle
   | Tfloat _ _ => Some AST.Tfloat
   | Tlong _ _ => Some AST.Tlong
   | _ => Some AST.Tint