From a0aaa3552d53b20a99566ac7116063fbb31b9964 Mon Sep 17 00:00:00 2001 From: xleroy 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 --- backend/CMtypecheck.ml | 2 ++ backend/Cminor.v | 14 +++++++++----- backend/PrintCminor.ml | 2 ++ backend/SelectLong.vp | 11 ++++++++++- backend/SelectLongproof.v | 24 ++++++++++++++++++++++++ backend/Selection.v | 2 ++ backend/Selectionproof.v | 2 ++ 7 files changed, 51 insertions(+), 6 deletions(-) (limited to 'backend') 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: -- cgit v1.2.3