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
---
 backend/SelectLongproof.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

(limited to 'backend/SelectLongproof.v')

diff --git a/backend/SelectLongproof.v b/backend/SelectLongproof.v
index 3eeeeb5d..39788281 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.
-- 
cgit