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/Cshmgen.v | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'cfrontend/Cshmgen.v') diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index c8a030c9..a303a7fd 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) -- cgit