From d48aabe4c7fd104f22190d375fd1201c9771322a Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime.jacquemin@cea.fr>
Date: Wed, 31 Jan 2024 11:28:41 +0100
Subject: [PATCH] [Kernel] Add two unit tests for linear filter invariant
computation
---
.../analysis/filter/linear_filter_test.ml | 129 ++++++++++++++++++
.../analysis/filter/linear_filter_test.mli | 23 ++++
tests/float/linear_filter_test.ml | 5 +-
.../oracle/linear_filter_test.res.oracle | 2 +
4 files changed, 155 insertions(+), 4 deletions(-)
create mode 100644 src/kernel_services/analysis/filter/linear_filter_test.ml
create mode 100644 src/kernel_services/analysis/filter/linear_filter_test.mli
diff --git a/src/kernel_services/analysis/filter/linear_filter_test.ml b/src/kernel_services/analysis/filter/linear_filter_test.ml
new file mode 100644
index 00000000000..43e0564ca21
--- /dev/null
+++ b/src/kernel_services/analysis/filter/linear_filter_test.ml
@@ -0,0 +1,129 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+
+
+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
+
+let max_exponent = 200
+let fin size n = Finite.of_int size n |> Option.get
+let set row col i j n = Linear.Matrix.set (fin row i) (fin col j) n
+
+let pretty_invariant fmt = function
+ | None -> Format.fprintf fmt "%s" (Unicode.top_string ())
+ | Some invariant -> Format.fprintf fmt "%a" Rational.pretty invariant
+
+
+
+module Circle = struct
+
+ let order = Nat.(succ one)
+
+ let state =
+ Linear.Matrix.zero order order
+ |> set order order 0 0 Rational.(of_float 0.68)
+ |> set order order 0 1 Rational.(of_float ~-.0.68)
+ |> set order order 1 0 Rational.(of_float 0.68)
+ |> set order order 1 1 Rational.(of_float 0.68)
+
+ let input = Linear.Matrix.id order
+
+ let measure = Linear.Vector.repeat Rational.one order
+
+ let compute () =
+ let filter = Filter.create state input measure in
+ let invariant = Filter.invariant filter max_exponent in
+ Kernel.result "Circle : %a@." pretty_invariant invariant
+
+end
+
+
+
+module Simple = struct
+
+ let order = Nat.(succ one)
+ let delay = Nat.one
+
+ let state =
+ Linear.Matrix.zero order order
+ |> set order order 0 0 Rational.(of_float 1.5)
+ |> set order order 0 1 Rational.(of_float ~-.0.7)
+ |> set order order 1 0 Rational.(of_float 1.)
+ |> set order order 1 1 Rational.(of_float 0.)
+
+ let input =
+ Linear.Matrix.zero order delay
+ |> set order delay 0 0 Rational.one
+ |> set order delay 1 0 Rational.zero
+
+ let measure = Linear.Vector.repeat (Rational.of_float 0.1) delay
+
+ let compute () =
+ let filter = Filter.create state input measure in
+ let invariant = Filter.invariant filter max_exponent in
+ Kernel.result "Simple : %a@." pretty_invariant invariant
+
+end
+
+
+
+let run () =
+ Circle.compute () ;
+ Simple.compute ()
diff --git a/src/kernel_services/analysis/filter/linear_filter_test.mli b/src/kernel_services/analysis/filter/linear_filter_test.mli
new file mode 100644
index 00000000000..cc9eb1f5468
--- /dev/null
+++ b/src/kernel_services/analysis/filter/linear_filter_test.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2023 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+val run : unit -> unit
diff --git a/tests/float/linear_filter_test.ml b/tests/float/linear_filter_test.ml
index 6a356eaf372..420df28ae1e 100644
--- a/tests/float/linear_filter_test.ml
+++ b/tests/float/linear_filter_test.ml
@@ -1,7 +1,4 @@
(* Programmatic tests of the invariant computation of linear filters by the
module Linear_filter. Run by linear_filter_test.i. *)
-let main _ =
- ()
-
-let () = Db.Main.extend main
+let () = Boot.Main.extend Linear_filter_test.run
diff --git a/tests/float/oracle/linear_filter_test.res.oracle b/tests/float/oracle/linear_filter_test.res.oracle
index 9fb7d2ecaff..27e5f9d3051 100644
--- a/tests/float/oracle/linear_filter_test.res.oracle
+++ b/tests/float/oracle/linear_filter_test.res.oracle
@@ -1 +1,3 @@
[kernel] Parsing linear_filter_test.i (no preprocessing)
+[kernel] Circle : 31.3829787
+[kernel] Simple : 9.2732747E-1
--
GitLab