From bdac1f6aba5370b21b34c9ee12429c3920b3dffb Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 8 Jul 2013 08:38:02 +0000 Subject: 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 --- cfrontend/Cop.v | 12 +++++++----- cfrontend/Cshmgen.v | 12 +++++++----- cfrontend/Cshmgenproof.v | 10 +++++++--- cfrontend/SimplLocalsproof.v | 5 ++++- 4 files changed, 25 insertions(+), 14 deletions(-) (limited to 'cfrontend') 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. -- cgit v1.2.3