From 4840f26d17f65fcd4a5161492362e6cbe4993e02 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 19 Jul 2024 22:11:28 +0200
Subject: [PATCH] [kernel] Removes lattice_messages.
---
.../abstract_interp/abstract_interp.ml | 12 ++--
.../abstract_interp/abstract_interp.mli | 2 +
.../abstract_interp/int_interval.ml | 6 +-
.../abstract_interp/int_set.ml | 4 --
.../abstract_interp/int_val.ml | 11 +---
src/kernel_services/abstract_interp/ival.ml | 4 --
.../abstract_interp/lattice_messages.ml | 64 -------------------
.../abstract_interp/lattice_messages.mli | 50 ---------------
src/kernel_services/abstract_interp/lmap.ml | 6 +-
.../abstract_interp/locations.ml | 4 +-
.../abstract_interp/offsetmap.ml | 8 +--
11 files changed, 17 insertions(+), 154 deletions(-)
delete mode 100644 src/kernel_services/abstract_interp/lattice_messages.ml
delete mode 100644 src/kernel_services/abstract_interp/lattice_messages.mli
diff --git a/src/kernel_services/abstract_interp/abstract_interp.ml b/src/kernel_services/abstract_interp/abstract_interp.ml
index 85565195642..109cf2d8e18 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.ml
+++ b/src/kernel_services/abstract_interp/abstract_interp.ml
@@ -25,7 +25,11 @@ exception Error_Bottom
exception Not_less_than
exception Can_not_subdiv
-let msg_emitter = Lattice_messages.register "Abstract_interp"
+let dkey = Kernel.register_category "approximation"
+let () = Kernel.add_debug_keys dkey
+
+let feedback_approximation format =
+ Kernel.feedback ~dkey ~current:true ~once:true format
type truth = True | False | Unknown
@@ -269,8 +273,7 @@ module Int = struct
let nb_loop = e_div (sub sup inf) step in
let rec fold_incr ~counter ~inf acc =
if equal counter onethousand then
- Lattice_messages.emit_costly msg_emitter
- "enumerating %a integers" pretty nb_loop;
+ feedback_approximation "enumerating %a integers" pretty nb_loop;
if le inf sup then begin
(* Format.printf "Int.fold: %a@\n" pretty inf; *)
fold_incr ~counter:(succ counter) ~inf:(add step inf) (f inf acc)
@@ -278,8 +281,7 @@ module Int = struct
in
let rec fold_decr ~counter ~sup acc =
if equal counter onethousand then
- Lattice_messages.emit_costly msg_emitter
- "enumerating %a integers" pretty nb_loop;
+ feedback_approximation "enumerating %a integers" pretty nb_loop;
if le inf sup then begin
(* Format.printf "Int.fold: %a@\n" pretty inf; *)
fold_decr ~counter:(succ counter) ~sup:(add step sup) (f sup acc)
diff --git a/src/kernel_services/abstract_interp/abstract_interp.mli b/src/kernel_services/abstract_interp/abstract_interp.mli
index 5fcbdcdd7b7..9316a481170 100644
--- a/src/kernel_services/abstract_interp/abstract_interp.mli
+++ b/src/kernel_services/abstract_interp/abstract_interp.mli
@@ -23,6 +23,8 @@
(** Functors for generic lattices implementations.
@see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf> *)
+val feedback_approximation: ('a, Format.formatter, unit) format -> 'a
+
exception Error_Top
(** Raised by some functions when encountering a top value. *)
diff --git a/src/kernel_services/abstract_interp/int_interval.ml b/src/kernel_services/abstract_interp/int_interval.ml
index 4ec276b83bb..21565bdbb10 100644
--- a/src/kernel_services/abstract_interp/int_interval.ml
+++ b/src/kernel_services/abstract_interp/int_interval.ml
@@ -22,9 +22,6 @@
open Abstract_interp
-let emitter = Lattice_messages.register "Int_interval";;
-let log_imprecision s = Lattice_messages.emit_imprecision emitter s
-
(* Represents the interval between [min] and [max], congruent to [rem] modulo
[modulo]. A value of [None] for [min] (resp. [max]) represents -infinity
(resp. +infinity). [modulo] is > 0, and [0 <= rem < modulo]. *)
@@ -683,12 +680,11 @@ let div_range x ymn ymx =
let max = Int.max (Int.max c1 c2) (Int.max c3 c4) in
inject_range (Some min) (Some max)
| _ ->
- log_imprecision "Ival.div_range";
top
let div x y =
match y.min, y.max with
- | None, _ | _, None -> log_imprecision "Ival.div"; `Value top
+ | None, _ | _, None -> `Value top
| Some min, Some max ->
let result_pos =
if Int.gt max Int.zero
diff --git a/src/kernel_services/abstract_interp/int_set.ml b/src/kernel_services/abstract_interp/int_set.ml
index 43f46c43e38..852f06a86f2 100644
--- a/src/kernel_services/abstract_interp/int_set.ml
+++ b/src/kernel_services/abstract_interp/int_set.ml
@@ -30,9 +30,6 @@ let set_small_cardinal i = small_cardinal := i
let debug_cardinal = false
-let emitter = Lattice_messages.register "Int_set";;
-let log_imprecision s = Lattice_messages.emit_imprecision emitter s
-
(* Small sets of integers, implemented as sorted non-empty arrays. *)
type set = Int.t array
@@ -335,7 +332,6 @@ let set_to_ival_under set =
(* Else: arbitrarily drop some elements of the under approximation. *)
else
let a = Array.make !small_cardinal Int.zero in
- log_imprecision "Ival.set_to_ival_under";
try
ignore (Int.Set.fold (fun elt i ->
if i = !small_cardinal then raise Exit;
diff --git a/src/kernel_services/abstract_interp/int_val.ml b/src/kernel_services/abstract_interp/int_val.ml
index ed4c2b7551e..dfa194dc7a3 100644
--- a/src/kernel_services/abstract_interp/int_val.ml
+++ b/src/kernel_services/abstract_interp/int_val.ml
@@ -27,9 +27,6 @@ open Bottom.Operators
let small_cardinal = Int_set.get_small_cardinal
let small_cardinal_Int () = Int.of_int (small_cardinal ())
-let emitter = Lattice_messages.register "Int_val"
-let log_imprecision s = Lattice_messages.emit_imprecision emitter s
-
type widen_hint = Datatype.Integer.Set.t
(* --------------------------------- Datatype ------------------------------- *)
@@ -315,7 +312,6 @@ let diff_if_one value rem =
| _ -> `Value value
let diff value rem =
- log_imprecision "Ival.diff";
diff_if_one value rem
(* ------------------------------- Lattice ---------------------------------- *)
@@ -426,8 +422,6 @@ let add_under v1 v2 =
| Set s1, Set s2 -> `Value (inject_set_or_top (Int_set.add_under s1 s2))
| Itv i1, Itv i2 -> Int_interval.add_under i1 i2 >>-: inject_itv
| Set s, Itv i | Itv i, Set s ->
- if Int_set.cardinal s <> 1
- then log_imprecision "Ival.add_int_under";
(* This is precise if [s] has only one element. Otherwise, this is not worse
than another computation. *)
`Value (Itv (Int_interval.add_singleton_int (Int_set.min s) i))
@@ -527,7 +521,6 @@ let shift_aux scale op (x: t) (y: t) =
let factor = check_make ~min ~max ~rem:Int.zero ~modu in
op x factor
with Z.Overflow ->
- Lattice_messages.emit_imprecision emitter "Ival.shift_aux";
(* We only preserve the sign of the result *)
if is_included x positive_integers then positive_integers
else
@@ -659,9 +652,7 @@ let extract_bits ~start ~stop = function
let dived = scale_div ~pos:true (Int.two_power start) d in
let factor = Int.two_power (Int.length start stop) in
scale_rem ~pos:true factor dived
- with Z.Overflow ->
- Lattice_messages.emit_imprecision emitter "Ival.extract_bits";
- top
+ with Z.Overflow -> top
let make = check_make
diff --git a/src/kernel_services/abstract_interp/ival.ml b/src/kernel_services/abstract_interp/ival.ml
index dd3c6a9e3ed..7d64c801fb9 100644
--- a/src/kernel_services/abstract_interp/ival.ml
+++ b/src/kernel_services/abstract_interp/ival.ml
@@ -24,9 +24,6 @@ open Abstract_interp
open Lattice_bounds
open Bottom.Operators
-let emitter = Lattice_messages.register "Ival"
-let log_imprecision s = Lattice_messages.emit_imprecision emitter s
-
module type Type = sig
(* Binary abstract operations do not model precisely float/integer operations.
It is the responsibility of the callers to have two operands of the same
@@ -667,7 +664,6 @@ let diff_if_one value rem =
| _, _ -> value
let diff value rem =
- log_imprecision "Ival.diff";
diff_if_one value rem
(* This function is an iterator, but it needs [diff_if_one] just above. *)
diff --git a/src/kernel_services/abstract_interp/lattice_messages.ml b/src/kernel_services/abstract_interp/lattice_messages.ml
deleted file mode 100644
index 632534aef17..00000000000
--- a/src/kernel_services/abstract_interp/lattice_messages.ml
+++ /dev/null
@@ -1,64 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-type t =
- | Approximation of string
- | Imprecision of string
- | Costly of string
- | Unsoundness of string
-
-type emitter = unit
-
-let dkey = Kernel.register_category "approximation"
-let () = Kernel.add_debug_keys dkey
-
-let emit _emitter msg =
- match msg with
- | Imprecision _ -> () (* Only for debug purposes *)
- | Approximation str
- | Costly str
- | Unsoundness str ->
- Kernel.feedback ~dkey ~current:true ~once:true "%s" str
-;;
-
-let register _name = ()
-
-let emit_approximation emitter = Format.kfprintf (fun _fmt ->
- let str = Format.flush_str_formatter() in
- emit emitter (Approximation str)) Format.str_formatter
-;;
-
-let emit_costly emitter = Format.kfprintf (fun _fmt ->
- let str = Format.flush_str_formatter() in
- emit emitter (Costly str)) Format.str_formatter
-;;
-
-let emit_imprecision emitter str =
- emit emitter (Imprecision str)
-;;
-
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/abstract_interp/lattice_messages.mli b/src/kernel_services/abstract_interp/lattice_messages.mli
deleted file mode 100644
index 9cb5cce0628..00000000000
--- a/src/kernel_services/abstract_interp/lattice_messages.mli
+++ /dev/null
@@ -1,50 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-(** Message and logging facility for abstract lattices. *)
-
-type t =
- | Approximation of string
- (** Abstract transfer function that intentionally approximates its result *)
- | Imprecision of string
- (** Abstract transfer function not fully implemented *)
- | Costly of string
- (** Abstract operation will be costly *)
- | Unsoundness of string
- (** Unsound abstract operation *)
-
-type emitter
-
-(** Register a new emitter for a message. *)
-val register: string -> emitter;;
-
-(** Emit a message. *)
-val emit: emitter -> t -> unit
-val emit_imprecision: emitter -> string -> unit
-val emit_approximation: emitter -> ('a, Format.formatter, unit) format -> 'a
-val emit_costly: emitter -> ('a, Format.formatter, unit) format -> 'a
-
-(*
-Local Variables:
-compile-command: "make -C ../../.."
-End:
-*)
diff --git a/src/kernel_services/abstract_interp/lmap.ml b/src/kernel_services/abstract_interp/lmap.ml
index 148cd8beb4c..7c4689e11b9 100644
--- a/src/kernel_services/abstract_interp/lmap.ml
+++ b/src/kernel_services/abstract_interp/lmap.ml
@@ -24,8 +24,6 @@ open Abstract_interp
open Locations
open Lattice_bounds
-let msg_emitter = Lattice_messages.register "Lmap";;
-
type 'a default_contents =
| Bottom
| Top of 'a
@@ -201,7 +199,7 @@ struct
in
match loc with
| Location_Bits.Top (Base.SetLattice.Top, orig) ->
- Lattice_messages.emit_approximation msg_emitter
+ Abstract_interp.feedback_approximation
"writing at a completely unknown address @[%a@]"
Origin.pretty_as_reason orig;
raise Result_is_top
@@ -526,7 +524,7 @@ struct
!had_non_bottom, result
| Location_Bits.Top (top, orig) ->
if not (Base.SetLattice.equal top Base.SetLattice.top) then
- Lattice_messages.emit_approximation msg_emitter
+ Abstract_interp.feedback_approximation
"writing somewhere in @[%a@]@[%a@]."
Base.SetLattice.pretty top
Origin.pretty_as_reason orig;
diff --git a/src/kernel_services/abstract_interp/locations.ml b/src/kernel_services/abstract_interp/locations.ml
index c65885af13a..56d9349940e 100644
--- a/src/kernel_services/abstract_interp/locations.ml
+++ b/src/kernel_services/abstract_interp/locations.ml
@@ -24,8 +24,6 @@ open Cil_types
open Cil
open Abstract_interp
-let emitter = Lattice_messages.register "Locations"
-
module Initial_Values = struct
let v = [ [Base.null,Ival.zero];
[Base.null,Ival.one];
@@ -548,7 +546,7 @@ let int_base_size_of_varinfo v =
let s = Int.of_int s in
Int_Base.inject s
with Cil.SizeOfError (msg, _) ->
- Lattice_messages.emit_approximation emitter
+ Abstract_interp.feedback_approximation
"imprecise size for variable %a (%s)" Printer.pp_varinfo v msg;
Int_Base.top
diff --git a/src/kernel_services/abstract_interp/offsetmap.ml b/src/kernel_services/abstract_interp/offsetmap.ml
index a22454c830a..43fe9f3436b 100644
--- a/src/kernel_services/abstract_interp/offsetmap.ml
+++ b/src/kernel_services/abstract_interp/offsetmap.ml
@@ -38,8 +38,6 @@ let ( %~ ) = Integer.e_rem
let succ = Integer.succ
let pred = Integer.pred
-let msg_emitter = Lattice_messages.register "Offsetmap"
-
(** Offsetmaps are unbalanced trees that map intervals to values, with
the additional properties that the shape of the tree is entirely determined
by the intervals that are mapped (see function [is_above] for the ordering).
@@ -1885,7 +1883,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
if size <~ period then
(* We are going to write the locations that are between [size+1] and
[period] unnecessarily, warn the user *)
- Lattice_messages.emit_approximation msg_emitter
+ Abstract_interp.feedback_approximation
"more than %d(%a) %s. Approximating."
plevel pretty_int number !imprecise_write_msg;
let abs_max = pred (mx +~ size) in
@@ -1895,7 +1893,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
let origin = Origin.(current Misalign_write) in
let v' = V.topify_with_origin origin v in
if not (V.equal v v') then
- Lattice_messages.emit_approximation msg_emitter
+ Abstract_interp.feedback_approximation
"approximating value to write.";
v'
in
@@ -2066,7 +2064,7 @@ module Make (V : Offsetmap_lattice_with_isotropy.S) = struct
| _ -> true (* at least two nodes *)
in
if imprecise then
- Lattice_messages.emit_approximation msg_emitter
+ Abstract_interp.feedback_approximation
"too many locations to update in array. Approximating.";
update ~validity ~exact ~offsets ~size v dst
--
GitLab