Merge remote-tracking branch 'origin/mppa-work-upstream-merge' into mppa-work

Conflicts:
	configure
	mppa_k1c/Archi.v
	mppa_k1c/Asmexpand.ml

1 files changed, 25 insertions, 12 deletions

diff --git a/mppa_k1c/Archi.v b/mppa_k1c/Archi.v
index 96571841..cdcf58c3 100644
--- a/mppa_k1c/Archi.v
+++ b/mppa_k1c/Archi.v
@@ -16,7 +16,8 @@
 
 (** Architecture-dependent parameters for MPPA K1c. Mostly copied from the Risc-V backend *)
 
-Require Import ZArith.
+Require Import ZArith List.
+(*From Flocq*)
 Require Import Binary Bits.
 
 Definition ptr64 := true.
@@ -33,6 +34,8 @@ Proof.
   unfold splitlong. destruct ptr64; simpl; congruence. 
 Qed.
 
+(** THIS IS NOT CHECKED ! NONE OF THIS ! *)
+
 (** Section 7.3: "Except when otherwise stated, if the result of a
    floating-point operation is NaN, it is the canonical NaN. The
    canonical NaN has a positive sign and all significand bits clear
@@ -40,26 +43,36 @@ Qed.
    We need to extend the [choose_binop_pl] functions to account for
    this case. *)
 
-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 := (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 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.
 
-(* TODO check *)
 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 fma_order {A: Type} (x y z: A) := (x, z, y).
+
+Definition fma_invalid_mul_is_nan := false.
 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
+              default_nan_64 choose_nan_64
+              default_nan_32 choose_nan_32
+              fma_order fma_invalid_mul_is_nan
               float_of_single_preserves_sNaN.
 
 (** Whether to generate position-independent code or not *)