From b9c5a9b8160f0a5dce00ec21e4dabb26372dba2e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Fri, 27 May 2022 15:34:21 +0200
Subject: [PATCH] Add tests for farith2

---
 colibri2.opam                        |  8 ----
 colibrics.opam                       |  8 ----
 dune                                 |  2 +-
 farith2/extract/farith_Big.ml        |  2 +-
 farith2/farith2.ml                   | 21 +++++++++-
 farith2/farith2.mli                  | 10 ++++-
 farith2/tests/issue_005.expected     |  1 +
 farith2/tests/issue_005.ml           | 11 +++++
 farith2/tests/mode.expected          | 61 ++++++++++++++++++++++++++++
 farith2/tests/mode.ml                | 43 ++++++++++++++++++++
 farith2/tests/subnormal.expected     |  7 ++++
 farith2/tests/subnormal.ml           | 39 ++++++++++++++++++
 farith2/tests/test.expected          | 18 ++++++++
 farith2/tests/test.ml                | 26 ++++++++++++
 farith2/tests/tie.expected           | 22 ++++++++++
 farith2/tests/tie.ml                 | 34 ++++++++++++++++
 src_colibri2/theories/FP/fp_value.ml | 10 ++---
 17 files changed, 298 insertions(+), 25 deletions(-)
 create mode 100644 farith2/tests/issue_005.expected
 create mode 100644 farith2/tests/issue_005.ml
 create mode 100644 farith2/tests/mode.expected
 create mode 100644 farith2/tests/mode.ml
 create mode 100644 farith2/tests/subnormal.expected
 create mode 100644 farith2/tests/subnormal.ml
 create mode 100644 farith2/tests/test.expected
 create mode 100644 farith2/tests/test.ml
 create mode 100644 farith2/tests/tie.expected
 create mode 100644 farith2/tests/tie.ml

diff --git a/colibri2.opam b/colibri2.opam
index d1c4ee231..e67d68c23 100644
--- a/colibri2.opam
+++ b/colibri2.opam
@@ -49,11 +49,3 @@ build: [
   ]
 ]
 dev-repo: "git+https://git.frama-c.com/bobot/colibrics.git"
-pin-depends: [
-  [ "dune.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "dune-site.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "dune-private-libs.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "dyn.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "ordering.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "stdune.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-]
diff --git a/colibrics.opam b/colibrics.opam
index 423c9412a..0f90f1de7 100644
--- a/colibrics.opam
+++ b/colibrics.opam
@@ -36,11 +36,3 @@ build: [
   ]
 ]
 dev-repo: "git+https://git.frama-c.com/bobot/colibrics.git"
-pin-depends: [
-  [ "dune.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "dune-site.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "dune-private-libs.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "dyn.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "ordering.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-  [ "stdune.3.1" "git+https://github.com/ocaml/dune.git#b12a5cd2664ae9e0820f52c816c88c372f0054ee" ]
-]
diff --git a/dune b/dune
index 81b443b85..357ed95ef 100644
--- a/dune
+++ b/dune
@@ -1,4 +1,4 @@
-(vendored_dirs dolmen farith farith2)
+(vendored_dirs dolmen farith)
 
 (rule (copy generic.opam.template colibrics.opam.template))
 (rule (copy generic.opam.template colibri2.opam.template))
diff --git a/farith2/extract/farith_Big.ml b/farith2/extract/farith_Big.ml
index 3ba55d18b..6dcac828f 100644
--- a/farith2/extract/farith_Big.ml
+++ b/farith2/extract/farith_Big.ml
@@ -248,7 +248,7 @@ module Z = Z (* zarith *)
 
 (* Q *)
 (* must be already normalize *)
-let q_mk (den, num) = { Q.den; Q.num }
+let q_mk (num, den) = { Q.den; Q.num }
 
 let q_case f q = f q.Q.den q.Q.num
 
diff --git a/farith2/farith2.ml b/farith2/farith2.ml
index c3bacd31e..a99fe6652 100644
--- a/farith2/farith2.ml
+++ b/farith2/farith2.ml
@@ -20,6 +20,8 @@
 (**************************************************************************)
 open Base
 
+module Format = Stdlib.Format
+
 module Z = struct
   include Z
 
@@ -85,7 +87,7 @@ module F = struct
         (Z.of_string m, Z.of_string e)
     | None -> (Z.of_string s, Z.zero)
 
-  let of_q ~mw ~ew ~mode q = of_q (Z.of_int mw) (Z.of_int ew) mode q
+  let of_q ~mw ~ew mode q = of_q (Z.of_int mw) (Z.of_int ew) mode q
   let of_bits ~mw ~ew z = of_bits (Z.of_int mw) (Z.of_int ew) z
   let to_bits t = to_bits t
   let nan ~mw ~ew = nan (Z.of_int mw) (Z.of_int ew)
@@ -95,6 +97,23 @@ module F = struct
   let is_infinite t = match t.value with B754_infinity _ -> true | _ -> false
   let is_nan t = match t.value with B754_nan -> true | _ -> false
 
+  let round ~mw ~ew mode (f:t) : t =
+    (match f.value with
+        | B754_zero _
+        | B754_infinity _
+        | B754_nan -> { mw = Z.of_int mw; ew = Z.of_int ew; value = f.value }
+        | B754_finite (_, _, _) ->
+          (of_q ~mw ~ew mode (to_q f))
+    )
+
+  let of_float f = of_bits ~mw:52 ~ew:11
+    @@ Z.extract (Z.of_int64 (Int64.bits_of_float f)) 0 64
+  let to_float mode f = round ~mw:52 ~ew:11 mode f
+                        |> to_bits
+                        |> fun z -> Z.signed_extract z 0 64
+                        |> Z.to_int64
+                        |> Int64.float_of_bits
+
   let is_negative t =
     match t.value with
     | B754_zero true | B754_finite (true, _, _) -> true
diff --git a/farith2/farith2.mli b/farith2/farith2.mli
index afae526f5..936004966 100644
--- a/farith2/farith2.mli
+++ b/farith2/farith2.mli
@@ -46,7 +46,7 @@ module F : sig
 
   val pp : Format.formatter -> t -> unit
 
-  val of_q : mw:int -> ew:int -> mode:mode -> Q.t -> t
+  val of_q : mw:int -> ew:int -> mode -> Q.t -> t
 
   val to_q : t -> Q.t
 
@@ -74,6 +74,12 @@ module F : sig
 
   val to_bits : t -> Z.t
 
+  val of_float : float -> t
+
+  val to_float : mode -> t -> float
+
+  val round: mw:int -> ew:int -> mode -> t -> t
+
   val ge : t -> t -> bool
 
   val gt : t -> t -> bool
@@ -133,6 +139,8 @@ module I : sig
   val is_singleton : t -> F.t option
 end
 
+val flocq_version: Z.t
+
 (* (\** {2 Generic Version } *\)
  * 
  * 
diff --git a/farith2/tests/issue_005.expected b/farith2/tests/issue_005.expected
new file mode 100644
index 000000000..ed3078295
--- /dev/null
+++ b/farith2/tests/issue_005.expected
@@ -0,0 +1 @@
+[F] 0.100000 : +3602879701896397p-55
diff --git a/farith2/tests/issue_005.ml b/farith2/tests/issue_005.ml
new file mode 100644
index 000000000..363837f36
--- /dev/null
+++ b/farith2/tests/issue_005.ml
@@ -0,0 +1,11 @@
+open Format
+open Farith2
+
+let f_convert r =
+  let fp = F.of_float r in
+  printf "[F] %f : %a@." r F.pp fp ; fp
+
+let () =
+  begin
+    ignore (f_convert 0.1) ;
+  end
diff --git a/farith2/tests/mode.expected b/farith2/tests/mode.expected
new file mode 100644
index 000000000..5d6065ed5
--- /dev/null
+++ b/farith2/tests/mode.expected
@@ -0,0 +1,61 @@
+[F]  3.1 = +6980579422424269p-51
+[Fp] 3.1 = +6501171p-21
+[Fq] 3.1 = +6501171p-21
+-----------------------
+ Simple Roundings
+-----------------------
+Q=31/10
+[F-NE] +6980579422424269p-51
+[F-NE] -6980579422424269p-51
+-----------------------
+Q=31/10
+[F-NA] +6980579422424269p-51
+[F-NA] -6980579422424269p-51
+-----------------------
+Q=31/10
+[F-ZR] +1745144855606067p-49
+[F-ZR] -1745144855606067p-49
+-----------------------
+Q=31/10
+[F-UP] +6980579422424269p-51
+[F-UP] -1745144855606067p-49
+-----------------------
+Q=31/10
+[F-DN] +1745144855606067p-49
+[F-DN] -6980579422424269p-51
+-----------------------
+ Tie Breaks (NE)
+-----------------------
+Q=562949953421313/562949953421312
+[F-NE-ex] +562949953421313p-49
+[F-NE-ex] -562949953421313p-49
+-----------------------
+Q=2251799813685253/2251799813685248
+[F-NE-lo] +2251799813685253p-51
+[F-NE-lo] -2251799813685253p-51
+-----------------------
+Q=1125899906842627/1125899906842624
+[F-NE-ti] +1125899906842627p-50
+[F-NE-ti] -1125899906842627p-50
+-----------------------
+Q=2251799813685255/2251799813685248
+[F-NE-up] +2251799813685255p-51
+[F-NE-up] -2251799813685255p-51
+-----------------------
+ Tie Breaks (NA)
+-----------------------
+Q=562949953421313/562949953421312
+[F-NA-ex] +562949953421313p-49
+[F-NA-ex] -562949953421313p-49
+-----------------------
+Q=2251799813685253/2251799813685248
+[F-NA-lo] +2251799813685253p-51
+[F-NA-lo] -2251799813685253p-51
+-----------------------
+Q=1125899906842627/1125899906842624
+[F-NA-ti] +1125899906842627p-50
+[F-NA-ti] -1125899906842627p-50
+-----------------------
+Q=2251799813685255/2251799813685248
+[F-NA-up] +2251799813685255p-51
+[F-NA-up] -2251799813685255p-51
diff --git a/farith2/tests/mode.ml b/farith2/tests/mode.ml
new file mode 100644
index 000000000..8771308e8
--- /dev/null
+++ b/farith2/tests/mode.ml
@@ -0,0 +1,43 @@
+module F = Farith2.F
+
+let fpp mode fmt q = F.pp fmt (F.of_q mode ~mw:52 ~ew:11 q)
+
+let () =
+  begin
+    let f = (F.of_float 3.1) in
+    Format.printf "[F]  3.1 = %a@." F.pp f;
+    let q = Q.make (Z.of_int 31) (Z.of_int 10) in
+    Format.printf "[Fp] 3.1 = %a@." F.pp (F.round ~mw:24 ~ew:11 ZR (F.of_float 3.1)) ;
+    Format.printf "[Fq] 3.1 = %a@." F.pp (F.of_q ~mw:24 ~ew:11 ZR q) ;
+    Format.printf "-----------------------@." ;
+    Format.printf " Simple Roundings@." ;
+    let job m m2 q =
+      begin
+        Format.printf "-----------------------@." ;
+        Format.printf "Q=%a@." Q.pp_print q ;
+        Format.printf "[F-%s] %a@." m (fpp m2) q ;
+        Format.printf "[F-%s] %a@." m (fpp m2) (Q.neg q) ;
+      end in
+    job "NE" Farith2.NE q ;
+    job "NA" Farith2.NA q ;
+    job "ZR" Farith2.ZR q ;
+    job "UP" Farith2.UP q ;
+    job "DN" Farith2.DN q ;
+    Format.printf "-----------------------@." ;
+    Format.printf " Tie Breaks (NE)@." ;
+    let eps = Z.shift_left Z.one 51 in
+    let e_ex = Q.make (Z.of_int 0b100) eps in
+    let e_lo = Q.make (Z.of_int 0b101) eps in
+    let e_ti = Q.make (Z.of_int 0b110) eps in
+    let e_up = Q.make (Z.of_int 0b111) eps in
+    job "NE-ex" Farith2.NE (Q.add Q.one e_ex) ;
+    job "NE-lo" Farith2.NE (Q.add Q.one e_lo) ;
+    job "NE-ti" Farith2.NE (Q.add Q.one e_ti) ;
+    job "NE-up" Farith2.NE (Q.add Q.one e_up) ;
+    Format.printf "-----------------------@." ;
+    Format.printf " Tie Breaks (NA)@." ;
+    job "NA-ex" Farith2.NA (Q.add Q.one e_ex) ;
+    job "NA-lo" Farith2.NA (Q.add Q.one e_lo) ;
+    job "NA-ti" Farith2.NA (Q.add Q.one e_ti) ;
+    job "NA-up" Farith2.NA (Q.add Q.one e_up) ;
+  end
diff --git a/farith2/tests/subnormal.expected b/farith2/tests/subnormal.expected
new file mode 100644
index 000000000..cf3afb2fc
--- /dev/null
+++ b/farith2/tests/subnormal.expected
@@ -0,0 +1,7 @@
+of-float 1p1023 = +1p1023 (normal)
+of-float 1p1024 = +∞ (infinity)
+of-float 1p-1022 = +1p-1022 (normal)
+of-float 1p-1023 = +1p-1023 (sub-normal)
+of-float 1p-1048 = +1p-1048 (sub-normal)
+of-float 1p-1074 = +1p-1074 (sub-normal)
+of-float 1p-1075 = +0 (zero)
diff --git a/farith2/tests/subnormal.ml b/farith2/tests/subnormal.ml
new file mode 100644
index 000000000..75445605c
--- /dev/null
+++ b/farith2/tests/subnormal.ml
@@ -0,0 +1,39 @@
+open Farith2
+
+let eps n = Stdlib.ldexp 1.0 n
+
+let pp_class fmt u =
+  Format.pp_print_string fmt
+    begin
+      match classify_float u with
+      | FP_zero -> "zero"
+      | FP_normal -> "normal"
+      | FP_subnormal -> "sub-normal"
+      | FP_infinite -> "infinity"
+      | FP_nan -> "nan"
+    end
+
+let test_of_float n =
+  let u = eps n in
+    let f = F.of_float u in
+    Format.printf "of-float 1p%d = %a (%a)@." n F.pp f pp_class u
+
+(* let test_to_float n =
+ *   begin
+ *     let u = eps n in
+ *     let f = F.power2 n in
+ *     let v = F.to_float f in
+ *     Format.printf "to-float %a = %f (%a)@." F.pp f v pp_class v ;
+ *     let fu,eu = Stdlib.frexp u in
+ *     let fv,ev = Stdlib.frexp v in
+ *     Format.printf "   expected = %fp%d@\n" fu eu ;
+ *     Format.printf "   obtained = %fp%d@." fv ev ;
+ *   end *)
+
+let limits = [ 1023;1024;-1022;-1023;-1048;-1074;-1075 ]
+
+let () =
+  begin
+    List.iter test_of_float limits ;
+    (* List.iter test_to_float limits ; *)
+  end
diff --git a/farith2/tests/test.expected b/farith2/tests/test.expected
new file mode 100644
index 000000000..e823e1d3c
--- /dev/null
+++ b/farith2/tests/test.expected
@@ -0,0 +1,18 @@
+Flocq version: 40000
+Run tests with Farith2.F
+   0.100000 + 2.000000 = 2.100000
+   0.100000 : +3602879701896397p-55
+   2.000000 : +1p1
+   2.100000 : +4728779608739021p-51
+-0.100000 + 2.000000 = 1.900000
+-0.100000 : -3602879701896397p-55
+2.000000 : +1p1
+1.900000 : +4278419646001971p-51
+-0.100000 + -2.000000 = -2.100000
+-0.100000 : -3602879701896397p-55
+-2.000000 : -1p1
+-2.100000 : -4728779608739021p-51
+0.100000 + -2.000000 = -1.900000
+0.100000 : +3602879701896397p-55
+-2.000000 : -1p1
+-1.900000 : -4278419646001971p-51
diff --git a/farith2/tests/test.ml b/farith2/tests/test.ml
new file mode 100644
index 000000000..2b49f0f11
--- /dev/null
+++ b/farith2/tests/test.ml
@@ -0,0 +1,26 @@
+open Format
+
+let () =
+  printf "Flocq version: %a@."
+    Z.pp_print Farith2.flocq_version
+
+open Farith2
+
+module Run = struct
+  let () =
+    printf "@[<3>Run tests with %s@\n" "Farith2.F";
+    let add u v =
+      let fu = F.of_float u in
+      let fv = F.of_float v in
+      let fr = F.add NE fu fv in
+      let r = F.to_float NE fr in
+      printf "%f + %f = %f@\n" u v r;
+      printf "%f : %a@\n" u F.pp fu;
+      printf "%f : %a@\n" v F.pp fv;
+      printf "%f : %a@]@\n" r F.pp fr;
+    in
+    add (0.1)   (2.0);
+    add (-.0.1) (2.0);
+    add (-.0.1) (-.2.0);
+    add (0.1)   (-.2.0)
+end
diff --git a/farith2/tests/tie.expected b/farith2/tests/tie.expected
new file mode 100644
index 000000000..8b916f281
--- /dev/null
+++ b/farith2/tests/tie.expected
@@ -0,0 +1,22 @@
+------------------------------------------
+         - +4503599627370496    (+1p52)
+1p52+1/2 = +9007199254740993p-1 (+9007199254740993p-1)
+         + +4503599627370497    (+4503599627370497)
+mantissa =  9007199254740992
+=NE +1p52
++NE +1p52 (+4503599627370496)
+-NE -1p52 (-4503599627370496)
+=NA +4503599627370497p0
++NA +4503599627370497 (+4503599627370497)
+-NA -4503599627370497 (-4503599627370497)
+------------------------------------------
+         - +4503599627370497    (+4503599627370497)
+1p52+3/2 = +9007199254740995p-1 (+9007199254740995p-1)
+         + +4503599627370498    (+2251799813685249p1)
+mantissa =  9007199254740992
+=NE +2251799813685249p1
++NE +2251799813685249p1 (+4503599627370498)
+-NE -2251799813685249p1 (-4503599627370498)
+=NA +2251799813685249p1
++NA +2251799813685249p1 (+4503599627370498)
+-NA -2251799813685249p1 (-4503599627370498)
diff --git a/farith2/tests/tie.ml b/farith2/tests/tie.ml
new file mode 100644
index 000000000..111be991c
--- /dev/null
+++ b/farith2/tests/tie.ml
@@ -0,0 +1,34 @@
+open Farith2
+
+(** not tested *)
+
+let tiebreak a b n =
+  begin
+    (* Tie breaks at [2^(n-1) + e] with [n] bits precision *)
+    let m = n-1 in
+    let up = Q.mul_2exp Q.one m in
+    let q = Q.(up + Q.make (Z.of_int a) (Z.of_int b)) in
+    let f0 = F.of_qint ~bits:(n+1) q in (* exact *)
+    let f1,f2 = F.seize ~bits:n f0 in
+    Format.printf "------------------------------------------@\n" ;
+    Format.printf "         - %a    (%a)@\n" F.pp f1 F.pp f1 ;
+    Format.printf "1p%d+%d/%d = %a (%a)@\n" m a b pp f0 F.pp f0 ;
+    Format.printf "         + %a    (%a)@\n" pp f2 F.pp f2 ;
+    Format.printf "mantissa =  %a@\n" Z.pp_print (Z.shift_left Z.one n) ;
+    let f1 = F.neg f0 in
+    let pos_ne = F.round ~mode:F.NE ~bits:n f0 in
+    let pos_na = F.round ~mode:F.NA ~bits:n f0 in
+    let neg_ne = F.round ~mode:F.NE ~bits:n f1 in
+    let neg_na = F.round ~mode:F.NA ~bits:n f1 in
+    Format.printf "+NE %a (%a)@\n" F.pp pos_ne pp pos_ne ;
+    Format.printf "-NE %a (%a)@\n" F.pp neg_ne pp neg_ne ;
+    Format.printf "+NA %a (%a)@\n" F.pp pos_na pp pos_na ;
+    Format.printf "-NA %a (%a)@\n" F.pp neg_na pp neg_na ;
+    Format.print_flush () ;
+  end
+
+let () =
+  begin
+    tiebreak 1 2 F.b64 ;
+    tiebreak 3 2 F.b64 ;
+  end
diff --git a/src_colibri2/theories/FP/fp_value.ml b/src_colibri2/theories/FP/fp_value.ml
index 85f19507a..1bdb8211f 100644
--- a/src_colibri2/theories/FP/fp_value.ml
+++ b/src_colibri2/theories/FP/fp_value.ml
@@ -93,18 +93,18 @@ let compute_ground d t =
   | { app = { builtin = Expr.Real_to_fp (ew, prec); _ }; args; _ } ->
       let m, r = IArray.extract2_exn args in
       let r = match !>>>r with Q q -> q | A _ -> assert false (* TODO *) in
-      !<(F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m r)
+      !<(F.of_q ~ew ~mw:(prec - 1) !>>m r)
   | { app = { builtin = Expr.Fp_to_fp (_ew1, _prec1, ew2, prec2); _ }; args; _ }
     ->
       let m, f1 = IArray.extract2_exn args in
-      !<(F.of_q ~ew:ew2 ~mw:(prec2 - 1) ~mode:!>>m (F.to_q !>f1))
+      !<(F.of_q ~ew:ew2 ~mw:(prec2 - 1) !>>m (F.to_q !>f1))
   | { app = { builtin = Expr.Sbv_to_fp (n, ew, prec); _ }; args; _ } ->
       let m, bv = IArray.extract2_exn args in
-      !<(F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m
+      !<(F.of_q ~ew ~mw:(prec - 1) !>>m
            (Q.of_bigint (Colibri2_theories_LRA.RealValue.signed_bitv n !>>>bv)))
   | { app = { builtin = Expr.Ubv_to_fp (n, ew, prec); _ }; args; _ } ->
       let m, bv = IArray.extract2_exn args in
-      !<(F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m
+      !<(F.of_q ~ew ~mw:(prec - 1) !>>m
            (Q.of_bigint
               (Colibri2_theories_LRA.RealValue.unsigned_bitv n !>>>bv)))
   | { app = { builtin = Expr.Fp (ew, prec); _ }; args; _ } ->
@@ -256,7 +256,7 @@ let converter d (f : Ground.t) =
         (set r
            (let* va = getq a in
             match va with
-            | Q va -> Some (F.of_q ~ew ~mw:(prec - 1) ~mode:!>>m va)
+            | Q va -> Some (F.of_q ~ew ~mw:(prec - 1) !>>m va)
             | A _ -> None
             (* TODO *)))
   | { app = { builtin = Expr.NaN (ew, prec); _ }; args; _ } ->
-- 
GitLab