From 83deaa4b3a164423254008d8594de99edc491c3b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 11 Jul 2019 10:56:23 +0200 Subject: Revised specification of NaN payload behavior When an FP arithmetic instruction produces a NaN result, the payload of this NaN depends on the architecture. Before, the payload behavior was specified by 3 architecture-dependent parameters: `Archi.choose_binop_pl_64` and `Archi.choose_binop_pl_32` and `Archi.fpu_results_default_qNaN`. This was adequate for two-argument operations, but doesn't extend to FMA. In preparation for FMA support, this commit generalizes the `Archi.choose` functions from two arguments to any number of arguments. In passing, `Archi.fpu_results_default_qNaN` is no longer needed. --- arm/Archi.v | 56 +++++++++----- lib/Floats.v | 228 ++++++++++++++++++++++++++------------------------------ powerpc/Archi.v | 30 ++++---- riscV/Archi.v | 28 +++---- x86_32/Archi.v | 30 ++++---- x86_64/Archi.v | 30 ++++---- 6 files changed, 209 insertions(+), 193 deletions(-) diff --git a/arm/Archi.v b/arm/Archi.v index 39a424ec..e78ff6ce 100644 --- a/arm/Archi.v +++ b/arm/Archi.v @@ -16,7 +16,7 @@ (** Architecture-dependent parameters for ARM *) -Require Import ZArith. +Require Import ZArith List. (*From Flocq*) Require Import Binary Bits. @@ -34,30 +34,52 @@ Proof. unfold splitlong, ptr64; congruence. Qed. -Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } := - exist _ (B754_nan 53 1024 false (iter_nat 51 _ xO xH) (eq_refl true)) (eq_refl true). +Definition default_nan_64 := (false, iter_nat 51 _ xO xH). +Definition default_nan_32 := (false, iter_nat 22 _ xO xH). + +(** Choose the first signaling NaN, if any; + otherwise choose the first NaN; + otherwise use default. *) + +Definition choose_nan (is_signaling: positive -> bool) + (default: bool * positive) + (l0: list (bool * positive)) : bool * positive := + let fix choose_snan (l1: list (bool * positive)) := + match l1 with + | nil => + match l0 with nil => default | n :: _ => n end + | ((s, p) as n) :: l1 => + if is_signaling p then n else choose_snan l1 + end + in choose_snan l0. + +Lemma choose_nan_idem: forall is_signaling default n, + choose_nan is_signaling default (n :: n :: nil) = + choose_nan is_signaling default (n :: nil). +Proof. + intros. destruct n as [s p]; unfold choose_nan; simpl. + destruct (is_signaling p); auto. +Qed. -Definition choose_binop_pl_64 (pl1 pl2 : positive) := - (** Choose second NaN if pl2 is sNaN but pl1 is qNan. - In all other cases, choose first NaN *) - (Pos.testbit pl1 51 && negb (Pos.testbit pl2 51))%bool. +Definition choose_nan_64 := + choose_nan (fun p => negb (Pos.testbit p 51)) default_nan_64. -Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } := - exist _ (B754_nan 24 128 false (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true). +Definition choose_nan_32 := + choose_nan (fun p => negb (Pos.testbit p 22)) default_nan_32. -Definition choose_binop_pl_32 (pl1 pl2 : positive) := - (** Choose second NaN if pl2 is sNaN but pl1 is qNan. - In all other cases, choose first NaN *) - (Pos.testbit pl1 22 && negb (Pos.testbit pl2 22))%bool. +Lemma choose_nan_64_idem: forall n, + choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil). +Proof. intros; apply choose_nan_idem. Qed. -Definition fpu_returns_default_qNaN := false. +Lemma choose_nan_32_idem: forall n, + choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil). +Proof. intros; apply choose_nan_idem. Qed. Definition float_of_single_preserves_sNaN := false. Global Opaque ptr64 big_endian splitlong - default_nan_64 choose_binop_pl_64 - default_nan_32 choose_binop_pl_32 - fpu_returns_default_qNaN + default_nan_64 choose_nan_64 + default_nan_32 choose_nan_32 float_of_single_preserves_sNaN. (** Which ABI to use: either the standard ARM EABI with floats passed diff --git a/lib/Floats.v b/lib/Floats.v index 8b118c8d..98ccc173 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -94,17 +94,49 @@ Proof. destruct x as [[]|]; simpl; intros; discriminate. Qed. -(** Relation between number of bits and base-2 logarithm *) +(** Normalization of NaN payloads *) -Lemma digits2_log2: - forall p, Z.pos (Digits.digits2_pos p) = Z.succ (Z.log2 (Z.pos p)). +Lemma normalized_nan: forall prec n p, + Z.of_nat n = prec - 1 -> 1 < prec -> + nan_pl prec (Z.to_pos (P_mod_two_p p n)) = true. Proof. - assert (E: forall p, Digits.digits2_pos p = Pos.size p). - { induction p; simpl; rewrite ?IHp; auto. } - intros p. rewrite E. - destruct p; simpl; rewrite ?Pos.add_1_r; reflexivity. + intros. unfold nan_pl. apply Z.ltb_lt. rewrite Digits.Zpos_digits2_pos. + set (p' := P_mod_two_p p n). + assert (A: 0 <= p' < 2 ^ Z.of_nat n). + { rewrite <- two_power_nat_equiv; apply P_mod_two_p_range. } + assert (B: Digits.Zdigits radix2 p' <= prec - 1). + { apply Digits.Zdigits_le_Zpower. rewrite <- H. rewrite Z.abs_eq; tauto. } + destruct (zeq p' 0). +- rewrite e. simpl; auto. +- rewrite Z2Pos.id by omega. omega. Qed. +(** Transform a Nan payload to a quiet Nan payload. *) + +Definition quiet_nan_64_payload (p: positive) := + Z.to_pos (P_mod_two_p (Pos.lor p ((iter_nat xO 51 1%positive))) 52%nat). + +Lemma quiet_nan_64_proof: forall p, nan_pl 53 (quiet_nan_64_payload p) = true. +Proof. intros; apply normalized_nan; auto; omega. Qed. + +Definition quiet_nan_64 (sp: bool * positive) : {x :float | is_nan _ _ x = true} := + let (s, p) := sp in + exist _ (B754_nan 53 1024 s (quiet_nan_64_payload p) (quiet_nan_64_proof p)) (eq_refl true). + +Definition default_nan_64 := quiet_nan_64 Archi.default_nan_64. + +Definition quiet_nan_32_payload (p: positive) := + Z.to_pos (P_mod_two_p (Pos.lor p ((iter_nat xO 22 1%positive))) 23%nat). + +Lemma quiet_nan_32_proof: forall p, nan_pl 24 (quiet_nan_32_payload p) = true. +Proof. intros; apply normalized_nan; auto; omega. Qed. + +Definition quiet_nan_32 (sp: bool * positive) : {x :float32 | is_nan _ _ x = true} := + let (s, p) := sp in + exist _ (B754_nan 24 128 s (quiet_nan_32_payload p) (quiet_nan_32_proof p)) (eq_refl true). + +Definition default_nan_32 := quiet_nan_32 Archi.default_nan_32. + Local Notation __ := (eq_refl Datatypes.Lt). Local Hint Extern 1 (Prec_gt_0 _) => exact (eq_refl Datatypes.Lt). @@ -119,29 +151,15 @@ Module Float. (** The following definitions are not part of the IEEE754 standard but apply to all architectures supported by CompCert. *) -(** Transform a Nan payload to a quiet Nan payload. *) - -Lemma transform_quiet_nan_proof (p : positive) : - nan_pl 53 p = true -> - nan_pl 53 (Pos.lor p (iter_nat xO 51 1%positive)) = true. -Proof. - unfold nan_pl. intros K. - simpl. rewrite Z.ltb_lt, digits2_log2 in *. - change (Z.pos (Pos.lor p 2251799813685248)) with (Z.lor (Z.pos p) 2251799813685248%Z). - rewrite Z.log2_lor by xomega. - now apply Z.max_case. -Qed. - -Definition transform_quiet_nan s p H : {x :float | is_nan _ _ x = true} := - exist _ (B754_nan 53 1024 s _ (transform_quiet_nan_proof p H)) (eq_refl true). - (** Nan payload operations for single <-> double conversions. *) +Definition expand_nan_payload (p: positive) := Pos.shiftl_nat p 29. + Lemma expand_nan_proof (p : positive) : nan_pl 24 p = true -> - nan_pl 53 (Pos.shiftl_nat p 29) = true. + nan_pl 53 (expand_nan_payload p) = true. Proof. - unfold nan_pl. intros K. + unfold nan_pl, expand_nan_payload. intros K. rewrite Z.ltb_lt in *. unfold Pos.shiftl_nat, nat_rect, Digits.digits2_pos. fold (Digits.digits2_pos p). @@ -149,38 +167,28 @@ Proof. Qed. Definition expand_nan s p H : {x | is_nan 53 1024 x = true} := - exist _ (B754_nan 53 1024 s _ (expand_nan_proof p H)) (eq_refl true). + exist _ (B754_nan 53 1024 s (expand_nan_payload p) (expand_nan_proof p H)) (eq_refl true). Definition of_single_nan (f : float32) : { x : float | is_nan _ _ x = true } := match f with | B754_nan s p H => if Archi.float_of_single_preserves_sNaN then expand_nan s p H - else transform_quiet_nan s _ (expand_nan_proof p H) - | _ => Archi.default_nan_64 + else quiet_nan_64 (s, expand_nan_payload p) + | _ => default_nan_64 end. -Lemma reduce_nan_proof (p : positive) : - nan_pl 53 p = true -> - nan_pl 24 (Pos.shiftr_nat p 29) = true. -Proof. - unfold nan_pl. intros K. - rewrite Z.ltb_lt in *. - unfold Pos.shiftr_nat, nat_rect. - assert (H : forall x, Digits.digits2_pos (Pos.div2 x) = (Digits.digits2_pos x - 1)%positive) - by (destruct x; simpl; auto; rewrite Pplus_one_succ_r, Pos.add_sub; auto). - rewrite !H, !Pos2Z.inj_sub_max. - repeat (apply Z.max_lub_lt; [reflexivity |apply Z.lt_sub_lt_add_l]). - exact K. -Qed. - -Definition reduce_nan s p H : {x : float32 | is_nan _ _ x = true} := - exist _ (B754_nan 24 128 s _ (reduce_nan_proof p H)) (eq_refl true). +Definition reduce_nan_payload (p: positive) := + (* The [quiet_nan_64_payload p] before the right shift is redundant with + the [quiet_nan_32_payload p] performed after, in [to_single_nan]. + However the former ensures that the result of the right shift is + not 0 and therefore representable as a positive. *) + Pos.shiftr_nat (quiet_nan_64_payload p) 29. Definition to_single_nan (f : float) : { x : float32 | is_nan _ _ x = true } := match f with - | B754_nan s p H => reduce_nan s _ (transform_quiet_nan_proof p H) - | _ => Archi.default_nan_32 + | B754_nan s p H => quiet_nan_32 (s, reduce_nan_payload p) + | _ => default_nan_32 end. (** NaN payload operations for opposite and absolute value. *) @@ -188,34 +196,37 @@ Definition to_single_nan (f : float) : { x : float32 | is_nan _ _ x = true } := Definition neg_nan (f : float) : { x : float | is_nan _ _ x = true } := match f with | B754_nan s p H => exist _ (B754_nan 53 1024 (negb s) p H) (eq_refl true) - | _ => Archi.default_nan_64 + | _ => default_nan_64 end. Definition abs_nan (f : float) : { x : float | is_nan _ _ x = true } := match f with | B754_nan s p H => exist _ (B754_nan 53 1024 false p H) (eq_refl true) - | _ => Archi.default_nan_64 + | _ => default_nan_64 end. -(** The NaN payload operations for two-argument arithmetic operations - are not part of the IEEE754 standard, but all architectures of - Compcert share a similar NaN behavior, parameterized by: -- a "default" payload which occurs when an operation generates a NaN from - non-NaN arguments; -- a choice function determining which of the payload arguments to choose, - when an operation is given two NaN arguments. *) - -Definition binop_nan (x y : float) : {x : float | is_nan 53 1024 x = true} := - if Archi.fpu_returns_default_qNaN then Archi.default_nan_64 else - match x, y with - | B754_nan s1 pl1 H1, B754_nan s2 pl2 H2 => - if Archi.choose_binop_pl_64 pl1 pl2 - then transform_quiet_nan s2 pl2 H2 - else transform_quiet_nan s1 pl1 H1 - | B754_nan s1 pl1 H1, _ => transform_quiet_nan s1 pl1 H1 - | _, B754_nan s2 pl2 H2 => transform_quiet_nan s2 pl2 H2 - | _, _ => Archi.default_nan_64 - end. +(** When an arithmetic operation returns a NaN, the sign and payload + of this NaN are not fully specified by the IEEE standard, and vary + among the architectures supported by CompCert. However, the following + behavior applies to all the supported architectures: the payload is either +- a default payload, independent of the arguments, or +- the payload of one of the NaN arguments, if any. + +For each supported architecture, the functions [Archi.choose_nan_64] +and [Archi.choose_nan_32] determine the payload of the result as a +function of the payloads of the NaN arguments. + +Additionally, signaling NaNs are converted to quiet NaNs, as required by the standard. +*) + +Definition cons_pl (x: float) (l: list (bool * positive)) := + match x with B754_nan s p _ => (s, p) :: l | _ => l end. + +Definition unop_nan (x: float) : {x : float | is_nan 53 1024 x = true} := + quiet_nan_64 (Archi.choose_nan_64 (cons_pl x [])). + +Definition binop_nan (x y: float) : {x : float | is_nan 53 1024 x = true} := + quiet_nan_64 (Archi.choose_nan_64 (cons_pl x (cons_pl y []))). (** ** Operations over double-precision floats *) @@ -302,19 +313,15 @@ Ltac smart_omega := Theorem add_commut: forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> add x y = add y x. Proof. - intros. apply Bplus_commut. unfold binop_nan. - destruct Archi.fpu_returns_default_qNaN. easy. - destruct x, y; try reflexivity. - now destruct H. + intros. apply Bplus_commut. + destruct x, y; try reflexivity; now destruct H. Qed. Theorem mul_commut: forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> mul x y = mul y x. Proof. - intros. apply Bmult_commut. unfold binop_nan. - destruct Archi.fpu_returns_default_qNaN. easy. - destruct x, y; try reflexivity. - now destruct H. + intros. apply Bmult_commut. + destruct x, y; try reflexivity; now destruct H. Qed. (** Multiplication by 2 is diagonal addition. *) @@ -324,9 +331,8 @@ Theorem mul2_add: Proof. intros. apply Bmult2_Bplus. intros x y Hx Hy. unfold binop_nan. - destruct Archi.fpu_returns_default_qNaN. easy. - destruct x as [| |sx px Nx|]; try discriminate. - now destruct y, Archi.choose_binop_pl_64. + destruct x; try discriminate. simpl. rewrite Archi.choose_nan_64_idem. + destruct y; reflexivity || discriminate. Qed. (** Divisions that can be turned into multiplication by an inverse. *) @@ -338,9 +344,8 @@ Theorem div_mul_inverse: Proof. intros. apply Bdiv_mult_inverse. 2: easy. intros x0 y0 z0 Hx Hy Hz. unfold binop_nan. - destruct Archi.fpu_returns_default_qNaN. easy. - destruct x0 as [| |sx px Nx|]; try discriminate. - now destruct y0, z0. + destruct x0; try discriminate. + destruct y0, z0; reflexivity || discriminate. Qed. (** Properties of comparisons. *) @@ -919,45 +924,26 @@ End Float. Module Float32. -(** ** NaN payload manipulations *) - -Lemma transform_quiet_nan_proof (p : positive) : - nan_pl 24 p = true -> - nan_pl 24 (Pos.lor p (iter_nat xO 22 1%positive)) = true. -Proof. - unfold nan_pl. intros K. - simpl. rewrite Z.ltb_lt, digits2_log2 in *. - change (Z.pos (Pos.lor p 4194304)) with (Z.lor (Z.pos p) 4194304%Z). - rewrite Z.log2_lor by xomega. - now apply Z.max_case. -Qed. - -Definition transform_quiet_nan s p H : {x : float32 | is_nan _ _ x = true} := - exist _ (B754_nan 24 128 s _ (transform_quiet_nan_proof p H)) (eq_refl true). - Definition neg_nan (f : float32) : { x : float32 | is_nan _ _ x = true } := match f with | B754_nan s p H => exist _ (B754_nan 24 128 (negb s) p H) (eq_refl true) - | _ => Archi.default_nan_32 + | _ => default_nan_32 end. Definition abs_nan (f : float32) : { x : float32 | is_nan _ _ x = true } := match f with | B754_nan s p H => exist _ (B754_nan 24 128 false p H) (eq_refl true) - | _ => Archi.default_nan_32 + | _ => default_nan_32 end. -Definition binop_nan (x y : float32) : {x : float32 | is_nan _ _ x = true} := - if Archi.fpu_returns_default_qNaN then Archi.default_nan_32 else - match x, y with - | B754_nan s1 pl1 H1, B754_nan s2 pl2 H2 => - if Archi.choose_binop_pl_32 pl1 pl2 - then transform_quiet_nan s2 pl2 H2 - else transform_quiet_nan s1 pl1 H1 - | B754_nan s1 pl1 H1, _ => transform_quiet_nan s1 pl1 H1 - | _, B754_nan s2 pl2 H2 => transform_quiet_nan s2 pl2 H2 - | _, _ => Archi.default_nan_32 - end. +Definition cons_pl (x: float32) (l: list (bool * positive)) := + match x with B754_nan s p _ => (s, p) :: l | _ => l end. + +Definition unop_nan (x: float32) : {x : float32 | is_nan _ _ x = true} := + quiet_nan_32 (Archi.choose_nan_32 (cons_pl x [])). + +Definition binop_nan (x y: float32) : {x : float32 | is_nan _ _ x = true} := + quiet_nan_32 (Archi.choose_nan_32 (cons_pl x (cons_pl y []))). (** ** Operations over single-precision floats *) @@ -1024,19 +1010,15 @@ Definition of_bits (b: int): float32 := b32_of_bits (Int.unsigned b). Theorem add_commut: forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> add x y = add y x. Proof. - intros. apply Bplus_commut. unfold binop_nan. - destruct Archi.fpu_returns_default_qNaN. easy. - destruct x, y; try reflexivity. - now destruct H. + intros. apply Bplus_commut. + destruct x, y; try reflexivity; now destruct H. Qed. Theorem mul_commut: forall x y, is_nan _ _ x = false \/ is_nan _ _ y = false -> mul x y = mul y x. Proof. - intros. apply Bmult_commut. unfold binop_nan. - destruct Archi.fpu_returns_default_qNaN. easy. - destruct x, y; try reflexivity. - now destruct H. + intros. apply Bmult_commut. + destruct x, y; try reflexivity; now destruct H. Qed. (** Multiplication by 2 is diagonal addition. *) @@ -1046,9 +1028,8 @@ Theorem mul2_add: Proof. intros. apply Bmult2_Bplus. intros x y Hx Hy. unfold binop_nan. - destruct Archi.fpu_returns_default_qNaN. easy. - destruct x as [| |sx px Nx|]; try discriminate. - now destruct y, Archi.choose_binop_pl_32. + destruct x; try discriminate. simpl. rewrite Archi.choose_nan_32_idem. + destruct y; reflexivity || discriminate. Qed. (** Divisions that can be turned into multiplication by an inverse. *) @@ -1060,9 +1041,8 @@ Theorem div_mul_inverse: Proof. intros. apply Bdiv_mult_inverse. 2: easy. intros x0 y0 z0 Hx Hy Hz. unfold binop_nan. - destruct Archi.fpu_returns_default_qNaN. easy. - destruct x0 as [| |sx px Nx|]; try discriminate. - now destruct y0, z0. + destruct x0; try discriminate. + destruct y0, z0; reflexivity || discriminate. Qed. (** Properties of comparisons. *) diff --git a/powerpc/Archi.v b/powerpc/Archi.v index d792e4fe..b99e4812 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -16,7 +16,7 @@ (** Architecture-dependent parameters for PowerPC *) -Require Import ZArith. +Require Import ZArith List. (*From Flocq*) Require Import Binary Bits. @@ -37,24 +37,28 @@ Proof. reflexivity. Qed. -Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } := - exist _ (B754_nan 53 1024 false (iter_nat 51 _ xO xH) (eq_refl true)) (eq_refl true). +Definition default_nan_64 := (false, iter_nat 51 _ xO xH). +Definition default_nan_32 := (false, iter_nat 22 _ xO xH). -Definition choose_binop_pl_64 (pl1 pl2 : positive) := - false. (**r always choose first NaN *) +(* Always choose the first NaN argument, if any *) -Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } := - exist _ (B754_nan 24 128 false (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true). +Definition choose_nan_64 (l: list (bool * positive)) : bool * positive := + match l with nil => default_nan_64 | n :: _ => n end. -Definition choose_binop_pl_32 (pl1 pl2 : positive) := - false. (**r always choose first NaN *) +Definition choose_nan_32 (l: list (bool * positive)) : bool * positive := + match l with nil => default_nan_32 | n :: _ => n end. -Definition fpu_returns_default_qNaN := false. +Lemma choose_nan_64_idem: forall n, + choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil). +Proof. auto. Qed. + +Lemma choose_nan_32_idem: forall n, + choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil). +Proof. auto. Qed. Definition float_of_single_preserves_sNaN := true. Global Opaque ptr64 big_endian splitlong - default_nan_64 choose_binop_pl_64 - default_nan_32 choose_binop_pl_32 - fpu_returns_default_qNaN + default_nan_64 choose_nan_64 + default_nan_32 choose_nan_32 float_of_single_preserves_sNaN. diff --git a/riscV/Archi.v b/riscV/Archi.v index 3758d686..e4078132 100644 --- a/riscV/Archi.v +++ b/riscV/Archi.v @@ -16,7 +16,7 @@ (** Architecture-dependent parameters for RISC-V *) -Require Import ZArith. +Require Import ZArith List. (*From Flocq*) Require Import Binary Bits. @@ -40,26 +40,28 @@ Qed. except the MSB, a.k.a. the quiet bit." Exceptions are operations manipulating signs. *) -Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } := - exist _ (B754_nan 53 1024 false (iter_nat 51 _ xO xH) (eq_refl true)) (eq_refl true). +Definition default_nan_64 := (false, iter_nat 51 _ xO xH). +Definition default_nan_32 := (false, iter_nat 22 _ xO xH). -Definition choose_binop_pl_64 (pl1 pl2 : positive) := - false. (**r irrelevant *) +Definition choose_nan_64 (l: list (bool * positive)) : bool * positive := + default_nan_64. -Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } := - exist _ (B754_nan 24 128 false (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true). +Definition choose_nan_32 (l: list (bool * positive)) : bool * positive := + default_nan_32. -Definition choose_binop_pl_32 (pl1 pl2 : positive) := - false. (**r irrelevant *) +Lemma choose_nan_64_idem: forall n, + choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil). +Proof. auto. Qed. -Definition fpu_returns_default_qNaN := true. +Lemma choose_nan_32_idem: forall n, + choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil). +Proof. auto. Qed. Definition float_of_single_preserves_sNaN := false. Global Opaque ptr64 big_endian splitlong - default_nan_64 choose_binop_pl_64 - default_nan_32 choose_binop_pl_32 - fpu_returns_default_qNaN + default_nan_64 choose_nan_64 + default_nan_32 choose_nan_32 float_of_single_preserves_sNaN. (** Whether to generate position-independent code or not *) diff --git a/x86_32/Archi.v b/x86_32/Archi.v index f10570e2..c6d66e09 100644 --- a/x86_32/Archi.v +++ b/x86_32/Archi.v @@ -16,7 +16,7 @@ (** Architecture-dependent parameters for x86 in 32-bit mode *) -Require Import ZArith. +Require Import ZArith List. (*From Flocq*) Require Import Binary Bits. @@ -34,24 +34,28 @@ Proof. unfold splitlong. destruct ptr64; simpl; congruence. Qed. -Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } := - exist _ (B754_nan 53 1024 true (iter_nat 51 _ xO xH) (eq_refl true)) (eq_refl true). +Definition default_nan_64 := (true, iter_nat 51 _ xO xH). +Definition default_nan_32 := (true, iter_nat 22 _ xO xH). -Definition choose_binop_pl_64 (pl1 pl2 : positive) := - false. (**r always choose first NaN *) +(* Always choose the first NaN argument, if any *) -Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } := - exist _ (B754_nan 24 128 true (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true). +Definition choose_nan_64 (l: list (bool * positive)) : bool * positive := + match l with nil => default_nan_64 | n :: _ => n end. -Definition choose_binop_pl_32 (pl1 pl2 : positive) := - false. (**r always choose first NaN *) +Definition choose_nan_32 (l: list (bool * positive)) : bool * positive := + match l with nil => default_nan_32 | n :: _ => n end. -Definition fpu_returns_default_qNaN := false. +Lemma choose_nan_64_idem: forall n, + choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil). +Proof. auto. Qed. + +Lemma choose_nan_32_idem: forall n, + choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil). +Proof. auto. Qed. Definition float_of_single_preserves_sNaN := false. Global Opaque ptr64 big_endian splitlong - default_nan_64 choose_binop_pl_64 - default_nan_32 choose_binop_pl_32 - fpu_returns_default_qNaN + default_nan_64 choose_nan_64 + default_nan_32 choose_nan_32 float_of_single_preserves_sNaN. diff --git a/x86_64/Archi.v b/x86_64/Archi.v index 01eb36dd..8523fdce 100644 --- a/x86_64/Archi.v +++ b/x86_64/Archi.v @@ -16,7 +16,7 @@ (** Architecture-dependent parameters for x86 in 64-bit mode *) -Require Import ZArith. +Require Import ZArith List. (*From Flocq*) Require Import Binary Bits. @@ -34,24 +34,28 @@ Proof. unfold splitlong. destruct ptr64; simpl; congruence. Qed. -Definition default_nan_64 : { x : binary64 | is_nan _ _ x = true } := - exist _ (B754_nan 53 1024 true (iter_nat 51 _ xO xH) (eq_refl true)) (eq_refl true). +Definition default_nan_64 := (true, iter_nat 51 _ xO xH). +Definition default_nan_32 := (true, iter_nat 22 _ xO xH). -Definition choose_binop_pl_64 (pl1 pl2 : positive) := - false. (**r always choose first NaN *) +(* Always choose the first NaN argument, if any *) -Definition default_nan_32 : { x : binary32 | is_nan _ _ x = true } := - exist _ (B754_nan 24 128 true (iter_nat 22 _ xO xH) (eq_refl true)) (eq_refl true). +Definition choose_nan_64 (l: list (bool * positive)) : bool * positive := + match l with nil => default_nan_64 | n :: _ => n end. -Definition choose_binop_pl_32 (pl1 pl2 : positive) := - false. (**r always choose first NaN *) +Definition choose_nan_32 (l: list (bool * positive)) : bool * positive := + match l with nil => default_nan_32 | n :: _ => n end. -Definition fpu_returns_default_qNaN := false. +Lemma choose_nan_64_idem: forall n, + choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil). +Proof. auto. Qed. + +Lemma choose_nan_32_idem: forall n, + choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil). +Proof. auto. Qed. Definition float_of_single_preserves_sNaN := false. Global Opaque ptr64 big_endian splitlong - default_nan_64 choose_binop_pl_64 - default_nan_32 choose_binop_pl_32 - fpu_returns_default_qNaN + default_nan_64 choose_nan_64 + default_nan_32 choose_nan_32 float_of_single_preserves_sNaN. -- cgit