Merge of Flocq version 2.2.0.

More precise modeling of NaNs.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2303 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 34 insertions, 0 deletions

diff --git a/arm/Nan.v b/arm/Nan.v
new file mode 100644
index 0000000..d66d6ec
--- /dev/null
+++ b/arm/Nan.v
@@ -0,0 +1,34 @@
+Require Import Fappli_IEEE.
+Require Import Fappli_IEEE_bits.
+Require Import Floats.
+Require Import ZArith.
+Require Import Integers.
+
+(* Needed to break a circular reference after extraction *)
+Definition transform_quiet_pl :=
+  Eval unfold Float.transform_quiet_pl in Float.transform_quiet_pl.
+
+Program Definition default_pl : bool * nan_pl 53 := (false, nat_iter 51 xO xH).
+
+Definition binop_pl (pl1 pl2:binary64) : bool*nan_pl 53 :=
+  match pl1, pl2 with
+    | B754_nan s1 pl1, B754_nan s2 pl2 =>
+      if (Pos.testbit (proj1_sig pl1) 51 && (* pl2 is sNan but pl1 is qNan *)
+         negb (Pos.testbit (proj1_sig pl2) 51))%bool
+      then (s2, transform_quiet_pl pl2)
+      else (s1, transform_quiet_pl pl1)
+    | B754_nan s1 pl1, _ => (s1, transform_quiet_pl pl1)
+    | _, B754_nan s2 pl2 => (s2, transform_quiet_pl pl2)
+    | _, _ => default_pl
+  end.
+
+Theorem binop_propagate1: Float.binop_propagate1_prop binop_pl.
+Proof.
+  repeat intro. destruct f1, f2; try discriminate; simpl;
+  destruct Pos.testbit; reflexivity.
+Qed.
+
+Theorem binop_propagate2: Float.binop_propagate2_prop binop_pl.
+Proof.
+  repeat intro. destruct f1, f2, f3; try discriminate; simpl; reflexivity.
+Qed.