diff options
Diffstat (limited to 'arm/Archi.v')
-rw-r--r-- | arm/Archi.v | 56 |
1 files changed, 39 insertions, 17 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 |