From 265fa07b34a813ba9d8249ddad82d71e6002c10d Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 2 Sep 2010 12:42:19 +0000 Subject: Merge of the reuse-temps branch: - Reload temporaries are marked as destroyed (set to Vundef) across operations in the semantics of LTL, LTLin, Linear and Mach, allowing Asmgen to reuse them. - Added IA32 port. - Cleaned up float conversions and axiomatization of floats. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- lib/Floats.v | 118 ++++++++++++++++++++++++++++++++++++++++++++++++++--------- 1 file changed, 101 insertions(+), 17 deletions(-) (limited to 'lib') diff --git a/lib/Floats.v b/lib/Floats.v index c9dda095..6257bcc0 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -23,29 +23,33 @@ Require Import Coqlib. Require Import Integers. -Parameter float: Type. +Parameter float: Type. (**r the type of IEE754 doubles *) Module Float. -Parameter zero: float. -Parameter one: float. +Parameter zero: float. (**r the float [+0.0] *) -Parameter neg: float -> float. -Parameter abs: float -> float. -Parameter singleoffloat: float -> float. -Parameter intoffloat: float -> int. -Parameter intuoffloat: float -> int. -Parameter floatofint: int -> float. -Parameter floatofintu: int -> float. +Axiom eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2}. -Parameter add: float -> float -> float. -Parameter sub: float -> float -> float. -Parameter mul: float -> float -> float. -Parameter div: float -> float -> float. +(** Arithmetic operations *) -Parameter cmp: comparison -> float -> float -> bool. +Parameter neg: float -> float. (**r opposite (change sign) *) +Parameter abs: float -> float. (**r absolute value (set sign to [+]) *) +Parameter singleoffloat: float -> float. (**r conversion to single precision *) +Parameter intoffloat: float -> int. (**r conversion to signed 32-bit int *) +Parameter intuoffloat: float -> int. (**r conversion to unsigned 32-bit int *) +Parameter floatofint: int -> float. (**r conversion from signed 32-bit int *) +Parameter floatofintu: int -> float. (**r conversion from unsigned 32-bit int *) -Axiom eq_dec: forall (f1 f2: float), {f1 = f2} + {f1 <> f2}. +Parameter add: float -> float -> float. (**r addition *) +Parameter sub: float -> float -> float. (**r subtraction *) +Parameter mul: float -> float -> float. (**r multiplication *) +Parameter div: float -> float -> float. (**r division *) + +Parameter cmp: comparison -> float -> float -> bool. (**r comparison *) + +(** Conversions between floats and their concrete in-memory representation + as a sequence of 64 bits (double precision) or 32 bits (single precision). *) Parameter bits_of_double: float -> int64. Parameter double_of_bits: int64 -> float. @@ -53,6 +57,11 @@ Parameter double_of_bits: int64 -> float. Parameter bits_of_single: float -> int. Parameter single_of_bits: int -> float. +Definition from_words (hi lo: int) : float := + double_of_bits + (Int64.or (Int64.shl (Int64.repr (Int.unsigned hi)) (Int64.repr 32)) + (Int64.repr (Int.unsigned lo))). + (** Below are the only properties of floating-point arithmetic that we rely on in the compiler proof. *) @@ -63,12 +72,39 @@ Axiom subf_addf_opp: forall f1 f2, sub f1 f2 = add f1 (neg f2). Axiom singleoffloat_idem: forall f, singleoffloat (singleoffloat f) = singleoffloat f. +(** Properties of comparisons. *) + +Axiom cmp_swap: + forall c x y, Float.cmp (swap_comparison c) x y = Float.cmp c y x. Axiom cmp_ne_eq: forall f1 f2, cmp Cne f1 f2 = negb (cmp Ceq f1 f2). +Axiom cmp_lt_eq_false: + forall x y, cmp Clt x y = true -> cmp Ceq x y = true -> False. Axiom cmp_le_lt_eq: forall f1 f2, cmp Cle f1 f2 = cmp Clt f1 f2 || cmp Ceq f1 f2. -Axiom cmp_ge_gt_eq: + +Corollary cmp_gt_eq_false: + forall x y, cmp Cgt x y = true -> cmp Ceq x y = true -> False. +Proof. + intros. rewrite <- cmp_swap in H. rewrite <- cmp_swap in H0. + eapply cmp_lt_eq_false; eauto. +Qed. + +Corollary cmp_ge_gt_eq: forall f1 f2, cmp Cge f1 f2 = cmp Cgt f1 f2 || cmp Ceq f1 f2. +Proof. + intros. + change Cge with (swap_comparison Cle). + change Cgt with (swap_comparison Clt). + change Ceq with (swap_comparison Ceq). + repeat rewrite cmp_swap. + apply cmp_le_lt_eq. +Qed. + +(** Properties of conversions to/from in-memory representation. + The double-precision conversions are bijective (one-to-one). + The single-precision conversions lose precision exactly + as described by [singleoffloat] rounding. *) Axiom double_of_bits_of_double: forall f, double_of_bits (bits_of_double f) = f. @@ -80,4 +116,52 @@ Axiom bits_of_singleoffloat: Axiom singleoffloat_of_bits: forall b, singleoffloat (single_of_bits b) = single_of_bits b. +(** Conversions between floats and unsigned ints can be defined + in terms of conversions between floats and signed ints. + (Most processors provide only the latter, forcing the compiler + to emulate the former.) *) + +Definition ox8000_0000 := Int.repr Int.half_modulus. (**r [0x8000_0000] *) + +Axiom floatofintu_floatofint_1: + forall x, + Int.ltu x ox8000_0000 = true -> + floatofintu x = floatofint x. + +Axiom floatofintu_floatofint_2: + forall x, + Int.ltu x ox8000_0000 = false -> + floatofintu x = add (floatofint (Int.sub x ox8000_0000)) + (floatofintu ox8000_0000). + +Axiom intuoffloat_intoffloat_1: + forall x, + cmp Clt x (floatofintu ox8000_0000) = true -> + intuoffloat x = intoffloat x. + +Axiom intuoffloat_intoffloat_2: + forall x, + cmp Clt x (floatofintu ox8000_0000) = false -> + intuoffloat x = + Int.add (intoffloat (sub x (floatofintu ox8000_0000))) + ox8000_0000. + +(** Conversions from ints to floats can be defined as bitwise manipulations + over the in-memory representation. This is what the PowerPC port does. + The trick is that [from_words 0x4330_0000 x] is the float + [2^52 + floatofintu x]. *) + +Definition ox4330_0000 := Int.repr 1127219200. (**r [0x4330_0000] *) + +Axiom floatofintu_from_words: + forall x, + floatofintu x = + sub (from_words ox4330_0000 x) (from_words ox4330_0000 Int.zero). + +Axiom floatofint_from_words: + forall x, + floatofint x = + sub (from_words ox4330_0000 (Int.add x ox8000_0000)) + (from_words ox4330_0000 ox8000_0000). + End Float. -- cgit