From 83deaa4b3a164423254008d8594de99edc491c3b Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
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 +++++++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 39 insertions(+), 17 deletions(-)

(limited to 'arm/Archi.v')

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
-- 
cgit