Upgrade embedded version of Flocq to 3.1.

Main changes to CompCert outside of Flocq are as follows:

- Minimal supported version of Coq is now 8.7, due to Flocq requirements.

- Most modifications are due to Z2R being dropped in favor of IZR and to
  the way Flocq now handles NaNs.

- CompCert now correctly handles NaNs for the Risc-V architecture
  (hopefully).

1 files changed, 15 insertions, 14 deletions

diff --git a/arm/Archi.v b/arm/Archi.v
index 353731e0..39a424ec 100644
--- a/arm/Archi.v
+++ b/arm/Archi.v
@@ -17,8 +17,8 @@
 (** Architecture-dependent parameters for ARM *)
 
 Require Import ZArith.
-Require Import Fappli_IEEE.
-Require Import Fappli_IEEE_bits.
+(*From Flocq*)
+Require Import Binary Bits.
 
 Definition ptr64 := false.
 
@@ -34,29 +34,30 @@ Proof.
   unfold splitlong, ptr64; congruence.
 Qed.
 
-Program Definition default_pl_64 : bool * nan_pl 53 :=
-  (false, iter_nat 51 _ xO xH).
+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 choose_binop_pl_64 (s1: bool) (pl1: nan_pl 53) (s2: bool) (pl2: nan_pl 53) :=
+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 (proj1_sig pl1) 51 &&
-   negb (Pos.testbit (proj1_sig pl2) 51))%bool.
+  (Pos.testbit pl1 51 && negb (Pos.testbit pl2 51))%bool.
 
-Program Definition default_pl_32 : bool * nan_pl 24 :=
-  (false, iter_nat 22 _ xO xH).
+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_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_pl 24) :=
+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 (proj1_sig pl1) 22 &&
-   negb (Pos.testbit (proj1_sig pl2) 22))%bool.
+  (Pos.testbit pl1 22 && negb (Pos.testbit pl2 22))%bool.
+
+Definition fpu_returns_default_qNaN := false.
 
 Definition float_of_single_preserves_sNaN := false.
 
 Global Opaque ptr64 big_endian splitlong
-              default_pl_64 choose_binop_pl_64
-              default_pl_32 choose_binop_pl_32
+              default_nan_64 choose_binop_pl_64
+              default_nan_32 choose_binop_pl_32
+              fpu_returns_default_qNaN
               float_of_single_preserves_sNaN.
 
 (** Which ABI to use: either the standard ARM EABI with floats passed