From a0aaa3552d53b20a99566ac7116063fbb31b9964 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 3 Jul 2013 15:07:17 +0000
Subject: 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
---
 cfrontend/Cminorgenproof.v   |  2 ++
 cfrontend/Cop.v              | 12 +++++++-----
 cfrontend/Cshmgen.v          | 12 +++++++-----
 cfrontend/Cshmgenproof.v     |  6 +++---
 cfrontend/SimplLocalsproof.v |  3 ++-
 5 files changed, 21 insertions(+), 14 deletions(-)

(limited to 'cfrontend')

diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index d6b99ed..672f804 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -1532,6 +1532,8 @@ Proof.
   inv H0; simpl in H; inv H. simpl. destruct (Float.longuoffloat f0); simpl in *; inv H1. TrivialExists.
   inv H0; simpl in H; inv H. simpl. TrivialExists.
   inv H0; simpl in H; inv H. simpl. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. TrivialExists.
+  inv H0; simpl in H; inv H. simpl. TrivialExists.
 Qed.
 
 (** Compatibility of [eval_binop] with respect to [val_inject]. *)
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 4932bad..1148d09 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -151,10 +151,12 @@ Definition cast_int_long (si: signedness) (i: int) : int64 :=
   | Unsigned => Int64.repr (Int.unsigned i)
   end.
 
-Definition cast_long_float (si : signedness) (i: int64) : float :=
-  match si with
-  | Signed => Float.floatoflong i
-  | Unsigned => Float.floatoflongu i
+Definition cast_long_float (si: signedness) (sz: floatsize) (i: int64) : float :=
+  match si, sz with
+  | Signed, F64 => Float.floatoflong i
+  | Unsigned, F64 => Float.floatoflongu i
+  | Signed, F32 => Float.singleoflong i
+  | Unsigned, F32 => Float.singleoflongu i
   end.
 
 Definition cast_float_long (si : signedness) (f: float) : option int64 :=
@@ -229,7 +231,7 @@ Definition sem_cast (v: val) (t1 t2: type) : option val :=
       end
   | cast_case_l2f si1 sz2 =>
       match v with
-      | Vlong i => Some (Vfloat (cast_float_float sz2 (cast_long_float si1 i)))
+      | Vlong i => Some (Vfloat (cast_long_float si1 sz2 i))
       | _ => None
       end
   | cast_case_f2l si2 =>
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index ad89a2d..c8a030c 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -72,10 +72,12 @@ Definition make_longofint (e: expr) (sg: signedness) :=
   | Unsigned => Eunop Olongofintu e
   end.
 
-Definition make_floatoflong (e: expr) (sg: signedness) :=
-  match sg with
-  | Signed => Eunop Ofloatoflong e
-  | Unsigned => Eunop Ofloatoflongu e
+Definition make_floatoflong (e: expr) (sg: signedness) (sz: floatsize) :=
+  match sg, sz with
+  | Signed, F64 => Eunop Ofloatoflong e
+  | Unsigned, F64 => Eunop Ofloatoflongu e
+  | Signed, F32 => Eunop Osingleoflong e
+  | Unsigned, F32 => Eunop Osingleoflongu e
   end.
 
 Definition make_longoffloat (e: expr) (sg: signedness) :=
@@ -123,7 +125,7 @@ Definition make_cast (from to: type) (e: expr) :=
   | cast_case_l2l => OK e
   | cast_case_i2l si1 => OK (make_longofint e si1)
   | cast_case_l2i sz2 si2 => OK (make_cast_int (Eunop Ointoflong e) sz2 si2)
-  | cast_case_l2f si1 sz2 => OK (make_cast_float (make_floatoflong e si1) sz2)
+  | cast_case_l2f si1 sz2 => OK (make_floatoflong e si1 sz2)
   | cast_case_f2l si2 => OK (make_longoffloat e si2)
   | cast_case_f2bool => OK (Ebinop (Ocmpf Cne) e (make_floatconst Float.zero))
   | cast_case_l2bool => OK (Ebinop (Ocmpl Cne) e (make_longconst Int64.zero))
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 11f8011..3d5bbba 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -172,12 +172,12 @@ Proof.
 Qed.
 
 Lemma make_floatoflong_correct:
-  forall a n sg e le m,
+  forall a n sg sz e le m,
   eval_expr ge e le m a (Vlong n) ->
-  eval_expr ge e le m (make_floatoflong a sg) (Vfloat(cast_long_float sg n)).
+  eval_expr ge e le m (make_floatoflong a sg sz) (Vfloat(cast_long_float sg sz n)).
 Proof.
   intros. unfold make_floatoflong, cast_int_long. 
-  destruct sg; econstructor; eauto. 
+  destruct sg; destruct sz; econstructor; eauto. 
 Qed.
 
 Lemma make_longoffloat_correct:
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index 515049a..ad8a06a 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -287,7 +287,8 @@ Proof.
 (* float *)
   destruct ty; simpl in H; try discriminate; destruct v; inv H.
   constructor. apply cast_float_float_idem.
-  constructor. apply cast_float_float_idem.
+  constructor. unfold cast_float_float, cast_long_float.
+  destruct f; destruct s; auto. apply Float.singleoflong_idem. apply Float.singleoflongu_idem.
   constructor. apply cast_float_float_idem.
 (* pointer *)
   destruct ty; simpl in H; try discriminate; destruct v; inv H; try constructor.
-- 
cgit v1.2.3