[Kernel] Regroup all arithmetic modules in one place

- Add a Rational module that implements a field over rationals.
- Add rationals to Datatype
- Move field, nat, finite and linear into libraries/arithmetic
- Update linear_filter_test to use the Rational module
- Update oracles

src/kernel_services/analysis/filter/linear_filter_test.ml

@@ -20,43 +20,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module Rational = struct
-
-  type scalar = Q.t
-
-  module Type = struct
-    include Datatype.Serializable_undefined
-    type t = scalar
-    let name = "Linear.Filter.Test.Rational"
-    let reprs = [ Q.zero ]
-    let compare = Q.compare
-    let equal = Q.equal
-    let hash q = Z.hash (Q.num q) + 11 * Z.hash (Q.den q)
-  end
-
-  include Datatype.Make_with_collections (Type)
-
-  let pretty fmt n =
-    let ten = Z.of_int 10 in
-    let sign = if Q.sign n >= 0 then "" else "-" in
-    let num = Q.num n |> Z.abs and den = Q.den n |> Z.abs in
-    let finish n = Z.Compare.(n >= den || n = Z.zero) in
-    let rec f e n = if finish n then (n, e) else f (e + 1) Z.(n * ten) in
-    let num, exponent = f 0 num in
-    let default fmt n = Format.fprintf fmt "%1.7f" (Q.to_float n) in
-    if exponent > 0 then
-      let number = Q.make num den in
-      Format.fprintf fmt "%s%aE-%d" sign default number exponent
-    else default fmt n
-
-  include Q
-  let infinity = Q.inf
-  let ( = ) = Q.equal
-
-end
-
-
-
 module Filter = Linear_filter.Make (Rational)
 module Linear = Filter.Linear
 

src/kernel_services/analysis/filter/field.ml → src/libraries/arithmetic/field.ml

@@ -20,33 +20,43 @@
 (*                                                                        *)
 (**************************************************************************)
 
+type 't bounds = { lower : 't ; upper : 't }
+
 module type S = sig
 
-  type scalar
-  include Datatype.S_with_collections with type t = scalar
+  include Datatype.S_with_collections
+  type scalar = t
 
-  val zero     : scalar
-  val one      : scalar
-  val infinity : scalar
+  val zero    : scalar
+  val one     : scalar
+  val two     : scalar
+  val pos_inf : scalar
+  val neg_inf : scalar
 
-  val of_int : int -> scalar
-  val of_float : float -> scalar
-  val to_float : scalar -> float
+  val of_int    : int -> scalar
+  val of_float  : float -> scalar
+  val to_float  : scalar -> float
+  val of_string : string -> scalar
 
   val neg : scalar -> scalar
   val abs : scalar -> scalar
   val max : scalar -> scalar -> scalar
   val min : scalar -> scalar -> scalar
 
-  val ( =  ) : scalar -> scalar -> bool
-  val ( <= ) : scalar -> scalar -> bool
-  val ( <  ) : scalar -> scalar -> bool
-  val ( >= ) : scalar -> scalar -> bool
-  val ( >  ) : scalar -> scalar -> bool
+  val pow2 : int -> scalar
+  val log2 : scalar -> int bounds
+  val sqrt : scalar -> scalar bounds
 
   val ( + ) : scalar -> scalar -> scalar
   val ( - ) : scalar -> scalar -> scalar
   val ( * ) : scalar -> scalar -> scalar
   val ( / ) : scalar -> scalar -> scalar
 
+  val ( =  ) : scalar -> scalar -> bool
+  val ( != ) : scalar -> scalar -> bool
+  val ( <= ) : scalar -> scalar -> bool
+  val ( <  ) : scalar -> scalar -> bool
+  val ( >= ) : scalar -> scalar -> bool
+  val ( >  ) : scalar -> scalar -> bool
+
 end

src/libraries/arithmetic/rational.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2025                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+include Datatype.Rational
+type scalar = t
+
+let zero = Q.zero
+let one = Q.one
+let two = Q.of_int 2
+let pos_inf = Q.inf
+let neg_inf = Q.minus_inf
+let of_float = Q.of_float
+let to_float = Q.to_float
+let of_int = Q.of_int
+
+let pow10 e = Z.(pow (of_int 10) e) |> Q.of_bigint
+
+let split_significant_exponent s =
+  match String.split_on_char 'e' s with
+  | [] | _ :: _ :: _ :: _ -> assert false
+  | [ s ] -> s, 0
+  | [ m ; e ] -> m, int_of_string e
+
+let significant_of_string significant =
+  match String.split_on_char '.' significant with
+  | [] | _ :: _ :: _ :: _ -> assert false
+  | [ m ] -> Q.of_string m
+  | [ integer ; fractional ] ->
+    let shift = pow10 (String.length fractional) in
+    Q.(of_string (integer ^ fractional) / shift)
+
+let of_string str =
+  let str = String.lowercase_ascii str in
+  let length = String.length str in
+  let last = String.get str (length - 1) in
+  let str = if last == 'f' then String.sub str 0 (length - 1) else str in
+  let significant, e = split_significant_exponent str in
+  let significant = significant_of_string significant in
+  let shift = if e >= 0 then pow10 e else Q.inv (pow10 ~-e) in
+  Q.(significant * shift)
+
+let pow2 e =
+  let p = Z.(shift_left one (Stdlib.abs e)) in
+  if e >= 0 then Q.(make p Z.one) else Q.(make Z.one p)
+
+let log2 q =
+  if Q.(q <= zero) then raise (Invalid_argument (Q.to_string q)) ;
+  let num = Q.num q |> Z.log2 and den = Q.den q |> Z.log2 in
+  let start = num - den - 1 in
+  let rec aux acc e =
+    let acc' = Q.(acc * two) in
+    if Q.(acc' > q) then Field.{ lower = e ; upper = e + 1 }
+    else aux acc' (e + 1)
+  in aux (pow2 start) start
+
+let neg = Q.neg
+let abs = Q.abs
+let min = Q.min
+let max = Q.max
+
+let sqrt q =
+  if Q.sign q = 1 then
+    let ten = Z.of_int 10 in
+    let num = Q.num q and den = Q.den q in
+    let acceptable_delta = Q.inv (Q.of_bigint @@ Z.pow ten 32) in
+    let rec approx_starting_at_scaling scaling =
+      let lower = Z.(sqrt (num * den * scaling * scaling)) in
+      let upper = Z.(lower + one) in
+      let denominator = Z.(den * scaling) in
+      let lower = Q.(make lower denominator) in
+      let upper = Q.(make upper denominator) in
+      let delta = Q.(upper - lower) in
+      if Q.(delta <= acceptable_delta) then Field.{ lower ; upper }
+      else approx_starting_at_scaling Z.(scaling * scaling)
+    in approx_starting_at_scaling ten
+  else { lower = neg_inf ; upper = pos_inf }
+
+let ( + ) = Q.( + )
+let ( - ) = Q.( - )
+let ( * ) = Q.( * )
+let ( / ) = Q.( / )
+
+let ( =  ) l r = Q.equal l r
+let ( != ) l r = not (l = r)
+let ( <= ) = Q.( <= )
+let ( <  ) = Q.( <  )
+let ( >= ) = Q.( >= )
+let ( >  ) = Q.( >  )

src/libraries/arithmetic/rational.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of Frama-C.                                         *)
+(*                                                                        *)
+(*  Copyright (C) 2007-2025                                               *)
+(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
+(*         alternatives)                                                  *)
+(*                                                                        *)
+(*  you can redistribute it and/or modify it under the terms of the GNU   *)
+(*  Lesser General Public License as published by the Free Software       *)
+(*  Foundation, version 2.1.                                              *)
+(*                                                                        *)
+(*  It is distributed in the hope that it will be useful,                 *)
+(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
+(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
+(*  GNU Lesser General Public License for more details.                   *)
+(*                                                                        *)
+(*  See the GNU Lesser General Public License version 2.1                 *)
+(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+include Field.S with type t = Q.t

src/libraries/datatype/datatype.ml

@@ -1601,6 +1601,23 @@ module Filepath = struct
 end
 let filepath = Filepath.ty
 
+module Rational =
+  Make_with_collections
+    (struct
+      type t = Q.t
+      let name = "Datatype.Rational"
+      let reprs = [ Q.zero ; Q.one ]
+      let structural_descr = Structural_descr.t_abstract
+      let equal = Q.equal
+      let compare = Q.compare
+      let copy = identity
+      let rehash = identity
+      let mem_project = never_any_project
+      let pretty fmt q = Format.pp_print_float fmt (Q.to_float q)
+      let hash q = Z.hash (Q.num q) + 3 * Z.hash (Q.den q)
+    end)
+let rational = Rational.ty
+
 (* ****************************************************************************)
 (** {3 Triple} *)
 (* ****************************************************************************)

src/libraries/datatype/datatype.mli

@@ -377,6 +377,9 @@ val formatter: Format.formatter Type.t
 module Integer: S_with_collections with type t = Integer.t
 val integer: Integer.t Type.t
 
+module Rational: S_with_collections with type t = Q.t
+val rational : Rational.t Type.t
+
 (** Type-safe strings representing normalized filepaths.
     See module {!Filepath.Normalized}.
     @since 18.0-Argon *)

tests/float/oracle/linear_filter_test.res.oracle

 [kernel] Parsing linear_filter_test.i (no preprocessing)
 [kernel] Circle :
-  * 0 : [-31.3829787 .. 31.3829787]
-  * 1 : [-31.3829787 .. 31.3829787]
+  * 0 : [-31.3829787234 .. 31.3829787234]
+  * 1 : [-31.3829787234 .. 31.3829787234]
 [kernel] Simple :
-  * 0 : [5.7267253E-1 .. 2.4273275]
-  * 1 : [1.5726725 .. 3.4273275]
+  * 0 : [0.572672526718 .. 2.42732747328]
+  * 1 : [1.57267252672 .. 3.42732747328]