Revised handling of int->float conversions:

- introduce Float.floatofint{,u} and use it in the semantics of C
- prove that it is equivalent to int->double conversion followed by
  double->float rounding, and use this fact to justify code generation
  in Cshmgen.


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

4 files changed, 25 insertions, 14 deletions

diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 1148d09..a1860ec 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -127,10 +127,12 @@ Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int :=
   | IBool, _ => if Int.eq i Int.zero then Int.zero else Int.one
   end.
 
-Definition cast_int_float (si : signedness) (i: int) : float :=
-  match si with
-  | Signed => Float.floatofint i
-  | Unsigned => Float.floatofintu i
+Definition cast_int_float (si: signedness) (sz: floatsize) (i: int) : float :=
+  match si, sz with
+  | Signed, F64 => Float.floatofint i
+  | Unsigned, F64 => Float.floatofintu i
+  | Signed, F32 => Float.singleofint i
+  | Unsigned, F32 => Float.singleofintu i
   end.
 
 Definition cast_float_int (si : signedness) (f: float) : option int :=
@@ -184,7 +186,7 @@ Definition sem_cast (v: val) (t1 t2: type) : option val :=
       end
   | cast_case_i2f si1 sz2 =>
       match v with
-      | Vint i => Some (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
+      | Vint i => Some (Vfloat (cast_int_float si1 sz2 i))
       | _ => None
       end
   | cast_case_f2i sz2 si2 =>
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index c8a030c..a303a7f 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -54,10 +54,12 @@ Definition make_floatconst (f: float) :=  Econst (Ofloatconst f).
 
 Definition make_longconst (f: int64) :=  Econst (Olongconst f).
 
-Definition make_floatofint (e: expr) (sg: signedness) :=
-  match sg with
-  | Signed => Eunop Ofloatofint e
-  | Unsigned => Eunop Ofloatofintu e
+Definition make_floatofint (e: expr) (sg: signedness) (sz: floatsize) :=
+  match sg, sz with
+  | Signed, F64 => Eunop Ofloatofint e
+  | Unsigned, F64 => Eunop Ofloatofintu e
+  | Signed, F32 => Eunop Osingleoffloat (Eunop Ofloatofint e)
+  | Unsigned, F32 => Eunop Osingleoffloat (Eunop Ofloatofintu e)
   end.
 
 Definition make_intoffloat (e: expr) (sg: signedness) :=
@@ -120,7 +122,7 @@ Definition make_cast (from to: type) (e: expr) :=
   | cast_case_neutral => OK e
   | cast_case_i2i sz2 si2 => OK (make_cast_int e sz2 si2)
   | cast_case_f2f sz2 => OK (make_cast_float e sz2)
-  | cast_case_i2f si1 sz2 => OK (make_cast_float (make_floatofint e si1) sz2)
+  | cast_case_i2f si1 sz2 => OK (make_floatofint e si1 sz2)
   | cast_case_f2i sz2 si2 => OK (make_cast_int (make_intoffloat e si2) sz2 si2)
   | cast_case_l2l => OK e
   | cast_case_i2l si1 => OK (make_longofint e si1)
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 3d5bbba..24576fc 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -144,11 +144,15 @@ Proof.
 Qed.
 
 Lemma make_floatofint_correct:
-  forall a n sg e le m,
+  forall a n sg sz e le m,
   eval_expr ge e le m a (Vint n) ->
-  eval_expr ge e le m (make_floatofint a sg) (Vfloat(cast_int_float sg n)).
+  eval_expr ge e le m (make_floatofint a sg sz) (Vfloat(cast_int_float sg sz n)).
 Proof.
-  intros. unfold make_floatofint, cast_int_float. 
+  intros. unfold make_floatofint, cast_int_float.
+  destruct sz.
+  destruct sg. 
+  rewrite Float.singleofint_floatofint. econstructor. econstructor; eauto. simpl; reflexivity. auto.
+  rewrite Float.singleofintu_floatofintu. econstructor. econstructor; eauto. simpl; reflexivity. auto.
   destruct sg; econstructor; eauto. 
 Qed.
 
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index ad8a06a..83e7375 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -286,7 +286,10 @@ Proof.
   destruct v; inv H. constructor.
 (* float *)
   destruct ty; simpl in H; try discriminate; destruct v; inv H.
-  constructor. apply cast_float_float_idem.
+  constructor. unfold cast_float_float, cast_int_float.
+  destruct f; destruct s; auto.
+  rewrite Float.singleofint_floatofint. apply Float.singleoffloat_idem.
+  rewrite Float.singleofintu_floatofintu. apply Float.singleoffloat_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.