Treat casts int64 -> float32 as primitive operations instead of two

casts int64 -> float64 -> float32.  The latter causes double rounding
errors.


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

7 files changed, 51 insertions, 6 deletions

diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml
index 1ca13ff..f78f470 100644
--- a/backend/CMtypecheck.ml
+++ b/backend/CMtypecheck.ml
@@ -115,6 +115,8 @@ let type_unary_operation = function
   | Olonguoffloat -> tfloat, tlong
   | Ofloatoflong -> tlong, tfloat
   | Ofloatoflongu -> tlong, tfloat
+  | Osingleoflong -> tlong, tfloat
+  | Osingleoflongu -> tlong, tfloat
 
 let type_binary_operation = function
   | Oadd -> tint, tint, tint
diff --git a/backend/Cminor.v b/backend/Cminor.v
index 6b36b4d..9f7244b 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -49,7 +49,7 @@ Inductive unary_operation : Type :=
   | Onotint: unary_operation               (**r bitwise complement  *)
   | Onegf: unary_operation                 (**r float opposite *)
   | Oabsf: unary_operation                 (**r float absolute value *)
-  | Osingleoffloat: unary_operation        (**r float truncation *)
+  | Osingleoffloat: unary_operation        (**r float truncation to float32 *)
   | Ointoffloat: unary_operation           (**r signed integer to float *)
   | Ointuoffloat: unary_operation          (**r unsigned integer to float *)
   | Ofloatofint: unary_operation           (**r float to signed integer *)
@@ -59,10 +59,12 @@ Inductive unary_operation : Type :=
   | Ointoflong: unary_operation            (**r long to int *)
   | Olongofint: unary_operation            (**r signed int to long *)
   | Olongofintu: unary_operation           (**r unsigned int to long *)
-  | Olongoffloat: unary_operation          (**r signed long to float *)
-  | Olonguoffloat: unary_operation         (**r unsigned long to float *)
-  | Ofloatoflong: unary_operation          (**r float to signed long *)
-  | Ofloatoflongu: unary_operation.        (**r float to unsigned long *)
+  | Olongoffloat: unary_operation          (**r float to signed long *)
+  | Olonguoffloat: unary_operation         (**r float to unsigned long *)
+  | Ofloatoflong: unary_operation          (**r signed long to float *)
+  | Ofloatoflongu: unary_operation         (**r unsigned long to float *)
+  | Osingleoflong: unary_operation         (**r signed long to float32 *)
+  | Osingleoflongu: unary_operation.       (**r unsigned long to float32 *)
 
 Inductive binary_operation : Type :=
   | Oadd: binary_operation                 (**r integer addition *)
@@ -271,6 +273,8 @@ Definition eval_unop (op: unary_operation) (arg: val) : option val :=
   | Olonguoffloat => Val.longuoffloat arg
   | Ofloatoflong => Val.floatoflong arg
   | Ofloatoflongu => Val.floatoflongu arg
+  | Osingleoflong => Val.singleoflong arg
+  | Osingleoflongu => Val.singleoflongu arg
   end.
 
 Definition eval_binop
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 4fbc600..ad02ed8 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -69,6 +69,8 @@ let name_of_unop = function
   | Olonguoffloat -> "longuoffloat"
   | Ofloatoflong -> "floatoflong"
   | Ofloatoflongu -> "floatoflongu"
+  | Osingleoflong -> "singleoflong"
+  | Osingleoflongu -> "singleoflongu"
 
 let comparison_name = function
   | Ceq -> "=="
diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp
index aad9d60..76cc79d 100644
--- a/backend/SelectLong.vp
+++ b/backend/SelectLong.vp
@@ -31,6 +31,8 @@ Record helper_functions : Type := mk_helper_functions {
   i64_dtou: ident;                      (**r float -> unsigned long *)
   i64_stod: ident;                      (**r signed long -> float *)
   i64_utod: ident;                      (**r unsigned long -> float *)
+  i64_stof: ident;                      (**r signed long -> float32 *)
+  i64_utof: ident;                      (**r unsigned long -> float32 *)
   i64_neg: ident;                       (**r opposite *)
   i64_add: ident;                       (**r addition *)
   i64_sub: ident;                       (**r subtraction *)
@@ -46,6 +48,7 @@ Record helper_functions : Type := mk_helper_functions {
 
 Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong).
 Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat).
+Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle).
 Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong).
 Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong).
 Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong).
@@ -135,6 +138,10 @@ Definition floatoflong (arg: expr) :=
   Eexternal hf.(i64_stod) sig_l_f (arg ::: Enil).
 Definition floatoflongu (arg: expr) :=
   Eexternal hf.(i64_utod) sig_l_f (arg ::: Enil).
+Definition singleoflong (arg: expr) :=
+  Eexternal hf.(i64_stof) sig_l_s (arg ::: Enil).
+Definition singleoflongu (arg: expr) :=
+  Eexternal hf.(i64_utof) sig_l_s (arg ::: Enil).
 
 Definition andl (e1 e2: expr) :=
   splitlong2 e1 e2 (fun h1 l1 h2 l2 => makelong (and h1 h2) (and l1 l2)).
@@ -361,6 +368,8 @@ Definition get_helpers (ge: Cminor.genv): res helper_functions :=
   do i64_dtou <- get_helper ge "__i64_dtou" sig_f_l ;
   do i64_stod <- get_helper ge "__i64_stod" sig_l_f ;
   do i64_utod <- get_helper ge "__i64_utod" sig_l_f ;
+  do i64_stof <- get_helper ge "__i64_stof" sig_l_s ;
+  do i64_utof <- get_helper ge "__i64_utof" sig_l_s ;
   do i64_neg <- get_builtin "__builtin_negl" sig_l_l ;
   do i64_add <- get_builtin "__builtin_addl" sig_ll_l ;
   do i64_sub <- get_builtin "__builtin_subl" sig_ll_l ;
@@ -373,6 +382,6 @@ Definition get_helpers (ge: Cminor.genv): res helper_functions :=
   do i64_shr <- get_helper ge "__i64_shr" sig_li_l ;
   do i64_sar <- get_helper ge "__i64_sar" sig_li_l ;
   OK (mk_helper_functions
-     i64_dtos i64_dtou i64_stod i64_utod
+     i64_dtos i64_dtou i64_stod i64_utod i64_stof i64_utof
      i64_neg i64_add i64_sub i64_mul i64_sdiv i64_udiv i64_smod i64_umod
      i64_shl i64_shr i64_sar).
diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v
index 3eeeeb5..3978828 100644
--- a/backend/SelectLongproof.v
+++ b/backend/SelectLongproof.v
@@ -51,6 +51,8 @@ Definition i64_helpers_correct (hf: helper_functions) : Prop :=
   /\(forall x z, Val.longuoffloat x = Some z -> helper_implements hf.(i64_dtou) sig_f_l (x::nil) z)
   /\(forall x z, Val.floatoflong x = Some z -> helper_implements hf.(i64_stod) sig_l_f (x::nil) z)
   /\(forall x z, Val.floatoflongu x = Some z -> helper_implements hf.(i64_utod) sig_l_f (x::nil) z)
+  /\(forall x z, Val.singleoflong x = Some z -> helper_implements hf.(i64_stof) sig_l_s (x::nil) z)
+  /\(forall x z, Val.singleoflongu x = Some z -> helper_implements hf.(i64_utof) sig_l_s (x::nil) z)
   /\(forall x, builtin_implements hf.(i64_neg) sig_l_l (x::nil) (Val.negl x))
   /\(forall x y, builtin_implements hf.(i64_add) sig_ll_l (x::y::nil) (Val.addl x y))
   /\(forall x y, builtin_implements hf.(i64_sub) sig_ll_l (x::y::nil) (Val.subl x y))
@@ -433,6 +435,28 @@ Proof.
   auto.
 Qed.
 
+Theorem eval_singleoflong:
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.singleoflong x = Some y ->
+  exists v, eval_expr ge sp e m le (singleoflong hf a) v /\ Val.lessdef y v.
+Proof.
+  intros; unfold singleoflong. econstructor; split. 
+  eapply eval_helper_1; eauto. UseHelper. 
+  auto.
+Qed.
+
+Theorem eval_singleoflongu:
+  forall le a x y,
+  eval_expr ge sp e m le a x ->
+  Val.singleoflongu x = Some y ->
+  exists v, eval_expr ge sp e m le (singleoflongu hf a) v /\ Val.lessdef y v.
+Proof.
+  intros; unfold singleoflongu. econstructor; split. 
+  eapply eval_helper_1; eauto. UseHelper. 
+  auto.
+Qed.
+
 Theorem eval_andl: binary_constructor_sound andl Val.andl.
 Proof.
   red; intros. unfold andl. apply eval_splitlong2; auto.
diff --git a/backend/Selection.v b/backend/Selection.v
index edc63cd..b35c891 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -98,6 +98,8 @@ Definition sel_unop (op: Cminor.unary_operation) (arg: expr) : expr :=
   | Cminor.Olonguoffloat => longuoffloat hf arg
   | Cminor.Ofloatoflong => floatoflong hf arg
   | Cminor.Ofloatoflongu => floatoflongu hf arg
+  | Cminor.Osingleoflong => singleoflong hf arg
+  | Cminor.Osingleoflongu => singleoflongu hf arg
   end.
 
 Definition sel_binop (op: Cminor.binary_operation) (arg1 arg2: expr) : expr :=
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index 93a5c51..e94f85d 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -203,6 +203,8 @@ Proof.
   eapply eval_longuoffloat; eauto.
   eapply eval_floatoflong; eauto.
   eapply eval_floatoflongu; eauto.
+  eapply eval_singleoflong; eauto.
+  eapply eval_singleoflongu; eauto.
 Qed.
 
 Lemma eval_sel_binop: