From 459b31178aa584623d57beb1e9cf38b0e07d2eff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Thu, 26 Sep 2024 14:42:49 +0200
Subject: [PATCH] [Eva] Creates domain log_category in functor
Domain_builder.Complete.
---
doc/eva/main.tex | 12 ++++----
src/plugins/eva/domains/abstract_domain.ml | 2 +-
src/plugins/eva/domains/apron/apron_domain.ml | 29 ++++++++++---------
src/plugins/eva/domains/domain_builder.ml | 8 ++---
src/plugins/eva/domains/domain_builder.mli | 2 ++
.../eva/domains/equality/equality_domain.ml | 4 ---
.../eva/domains/gauges/gauges_domain.ml | 4 ---
src/plugins/eva/domains/inout_domain.ml | 2 --
.../eva/domains/multidim/multidim_domain.ml | 4 ---
src/plugins/eva/domains/octagons.ml | 2 --
src/plugins/eva/domains/offsm_domain.ml | 4 ---
src/plugins/eva/domains/simple_memory.ml | 2 --
src/plugins/eva/domains/symbolic_locs.ml | 4 ---
src/plugins/eva/domains/taint_domain.ml | 4 ---
src/plugins/eva/domains/traces_domain.ml | 2 --
src/plugins/eva/domains/unit_domain.ml | 3 --
tests/value/symbolic_locs.i | 6 ++--
17 files changed, 32 insertions(+), 62 deletions(-)
diff --git a/doc/eva/main.tex b/doc/eva/main.tex
index 1ac09840397..58ff1fbd0b1 100644
--- a/doc/eva/main.tex
+++ b/doc/eva/main.tex
@@ -4228,7 +4228,7 @@ Most domains are also presented in more details in the following subsections.
Useful on most analyses and very efficient.
\tabularnewline
\midrule
- symbolic-locations & d-symblocs & \ref{sec:reuse} &
+ symbolic-locations & d-symbolic-locations & \ref{sec:reuse} &
Infers values at symbolic locations. \\
Useful on most analyses and very efficient.
\tabularnewline
@@ -4256,13 +4256,13 @@ Most domains are also presented in more details in the following subsections.
Infers the sign of variables. Rarely useful.
\tabularnewline
\midrule
- apron-box & \multirow{5}{*}{d-apron} & \multirow{5}{*}{\ref{sec:apron}} &
+ apron-box & d-apron-box & \multirow{5}{*}{\ref{sec:apron}} &
\multirow{5}{7.5cm}{Experimental and often costly. \\
Binding to the Apron library domains.}\tabularnewline
- apron-octagon & & & \tabularnewline
- apron-polka-equality & & & \tabularnewline
- apron-polka-loose & & & \tabularnewline
- apron-polka-strict & & & \tabularnewline
+ apron-octagon & d-apron-octagon & & \tabularnewline
+ apron-polka-equality & d-apron-polka-equality & & \tabularnewline
+ apron-polka-loose & d-apron-polka-loose & & \tabularnewline
+ apron-polka-strict & d-apron-polka-strict & & \tabularnewline
\midrule
taint & d-taint & \ref{sec:taint} &
Experimental. Performs a taint analysis.
diff --git a/src/plugins/eva/domains/abstract_domain.ml b/src/plugins/eva/domains/abstract_domain.ml
index 79e3f38dfd2..2e5d59d8a5c 100644
--- a/src/plugins/eva/domains/abstract_domain.ml
+++ b/src/plugins/eva/domains/abstract_domain.ml
@@ -498,7 +498,7 @@ module type S = sig
include Reuse with type t := t
(** Category for the messages about the domain.
- Must be created through {!Self.register_category}. *)
+ Created by {!Domain_builder.Complete} using the domain name. *)
val log_category : Self.category
(** This function is called after the analysis. The argument is the state
diff --git a/src/plugins/eva/domains/apron/apron_domain.ml b/src/plugins/eva/domains/apron/apron_domain.ml
index a8628869f24..4546f28956b 100644
--- a/src/plugins/eva/domains/apron/apron_domain.ml
+++ b/src/plugins/eva/domains/apron/apron_domain.ml
@@ -24,8 +24,6 @@ open Eval
open Eva_ast
open Apron
-let dkey = Self.register_category "d-apron"
-
let debug = false
let abort exclog =
@@ -347,6 +345,7 @@ let ival_to_interval = function
module type Input = sig
type t
val manager: t Manager.t
+ val name: string
end
module Make (Man : Input) = struct
@@ -360,7 +359,6 @@ module Make (Man : Input) = struct
let location_dependencies = Main_locations.ploc
let man = Man.manager
- let log_category = dkey
let empty_env = Environment.make [||] [||]
@@ -371,7 +369,7 @@ module Make (Man : Input) = struct
struct
include Datatype.Undefined
type t = state
- let name = Manager.get_library Man.manager
+ let name = Man.name
let reprs = [top]
let structural_descr = Structural_descr.t_unknown
@@ -689,44 +687,49 @@ end
module Apron_Octagon = struct
type t = Oct.t
let manager = Oct.manager_alloc ()
+ let name = "apron-octagon"
end
module Apron_Box = struct
type t = Box.t
let manager = Box.manager_alloc ()
+ let name = "apron-box"
end
module Apron_Polka_Loose = struct
type t = Polka.loose Polka.t
let manager = Polka.manager_alloc_loose ()
+ let name = "apron-polka-loose"
end
module Apron_Polka_Strict = struct
type t = Polka.strict Polka.t
let manager = Polka.manager_alloc_strict ()
+ let name = "apron-polka-strict"
end
module Apron_Polka_Equalities = struct
type t = Polka.equalities Polka.t
let manager = Polka.manager_alloc_equalities ()
+ let name = "apron-polka-equality"
end
(** Apron manager allocation changes the rounding mode. *)
let () = Floating_point.set_round_nearest_even ()
-let make name (module Man: Input) =
+let make (module Man: Input) =
let module Domain = Make (Man) in
- let name = "apron-" ^ name and experimental = true and priority = 1 in
+ let experimental = true and priority = 1 in
let descr =
- "Binding to the " ^ name ^ " domain of the Apron library. " ^
+ "Binding to the " ^ Man.name ^ " domain of the Apron library. " ^
"See http://apron.cri.ensmp.fr/library for more details."
in
- Abstractions.Domain.register ~name ~descr ~experimental ~priority
+ Abstractions.Domain.register ~name:Man.name ~descr ~experimental ~priority
(module Domain)
-let octagon = make "octagon" (module Apron_Octagon)
-let box = make "box" (module Apron_Box)
-let polka_loose = make "polka-loose" (module Apron_Polka_Loose)
-let polka_strict = make "polka-strict" (module Apron_Polka_Strict)
-let polka_equality = make "polka-equality" (module Apron_Polka_Equalities)
+let octagon = make (module Apron_Octagon)
+let box = make (module Apron_Box)
+let polka_loose = make (module Apron_Polka_Loose)
+let polka_strict = make (module Apron_Polka_Strict)
+let polka_equality = make (module Apron_Polka_Equalities)
(* When the value abstraction contains both a cvalue and an interval
component (coming currently from an Apron domain), reduce them from each
diff --git a/src/plugins/eva/domains/domain_builder.ml b/src/plugins/eva/domains/domain_builder.ml
index eff6e6bf4f0..4df72ddebb9 100644
--- a/src/plugins/eva/domains/domain_builder.ml
+++ b/src/plugins/eva/domains/domain_builder.ml
@@ -66,6 +66,8 @@ module type LeafDomain = sig
module Store: Domain_store.S with type t := t
+ val log_category: Self.category
+
val key: t Abstract_domain.key
end
@@ -97,6 +99,8 @@ module Complete (Domain: InputDomain) = struct
module Store = Domain_store.Make (Domain)
+ let log_category = Self.register_category ("d-" ^ Domain.name)
+
let key: Domain.t Structure.Key_Domain.key =
Structure.Key_Domain.create_key Domain.name
end
@@ -125,8 +129,6 @@ module Make_Minimal
include Domain
- let log_category = Self.register_category ("d-" ^ name)
-
type value = Value.t
type location = Location.location
type state = Domain.t
@@ -240,8 +242,6 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
(Domain) (struct let module_name = Domain.name end)
: Datatype.S_with_collections with type t := t)
- let log_category = Self.register_category ("d-" ^ name)
-
type value = Cvalue.V.t
type location = Precise_locs.precise_location
type state = Domain.t
diff --git a/src/plugins/eva/domains/domain_builder.mli b/src/plugins/eva/domains/domain_builder.mli
index b7d44a0cf73..c44cb7fab8c 100644
--- a/src/plugins/eva/domains/domain_builder.mli
+++ b/src/plugins/eva/domains/domain_builder.mli
@@ -70,6 +70,8 @@ module type LeafDomain = sig
module Store: Domain_store.S with type t := t
+ val log_category: Self.category
+
val key: t Abstract_domain.key
end
diff --git a/src/plugins/eva/domains/equality/equality_domain.ml b/src/plugins/eva/domains/equality/equality_domain.ml
index 78c7105fe3e..c087751c8ee 100644
--- a/src/plugins/eva/domains/equality/equality_domain.ml
+++ b/src/plugins/eva/domains/equality/equality_domain.ml
@@ -38,8 +38,6 @@ let call_init_state kf =
| "none" -> ISEmpty
| _ -> assert false
-let dkey = Self.register_category "d-equality"
-
open Hcexprs
(* ------------------------- Dependences ------------------------------------ *)
@@ -122,8 +120,6 @@ module Internal = struct
let name = "equality"
- let log_category = dkey
-
let pretty fmt (eqs, _, _) = Equality.Set.pretty fmt eqs
let _pretty_debug fmt (eqs, deps, modified) =
diff --git a/src/plugins/eva/domains/gauges/gauges_domain.ml b/src/plugins/eva/domains/gauges/gauges_domain.ml
index 49416c570c0..29e4391cb7e 100644
--- a/src/plugins/eva/domains/gauges/gauges_domain.ml
+++ b/src/plugins/eva/domains/gauges/gauges_domain.ml
@@ -1107,8 +1107,6 @@ module G = struct
end
-let dkey = Self.register_category "d-gauges"
-
module D : Abstract_domain.Leaf
with type state = G.t
and type value = Cvalue.V.t
@@ -1125,8 +1123,6 @@ module D : Abstract_domain.Leaf
include G
include Domain_builder.Complete (struct include G let top = empty end)
- let log_category = dkey
-
let empty _ = G.empty
let pretty = G.pretty
diff --git a/src/plugins/eva/domains/inout_domain.ml b/src/plugins/eva/domains/inout_domain.ml
index 0b2f3dd185b..409ddb4ac0a 100644
--- a/src/plugins/eva/domains/inout_domain.ml
+++ b/src/plugins/eva/domains/inout_domain.ml
@@ -221,8 +221,6 @@ module Domain = struct
include Domain_builder.Complete (LatticeInout)
- let log_category = Self.register_category "d-inout"
-
let enter_scope _kind _vars state = state
let leave_scope _kf vars state = Transfer.remove_variables vars state
diff --git a/src/plugins/eva/domains/multidim/multidim_domain.ml b/src/plugins/eva/domains/multidim/multidim_domain.ml
index ed430145d4c..574830344de 100644
--- a/src/plugins/eva/domains/multidim/multidim_domain.ml
+++ b/src/plugins/eva/domains/multidim/multidim_domain.ml
@@ -23,8 +23,6 @@
open Eval
open Lattice_bounds
-let dkey = Self.register_category "d-multidim"
-
let map_to_singleton map =
let aux base offset = function
| None -> Some (base, offset)
@@ -377,8 +375,6 @@ struct
type mdlocation = Location.t (* should be = to location *)
type origin
- let log_category = dkey
-
let cache_name s =
Hptmap_sig.PersistentCache ("Multidim_domain." ^ s)
diff --git a/src/plugins/eva/domains/octagons.ml b/src/plugins/eva/domains/octagons.ml
index e4a757b1b39..2d213923304 100644
--- a/src/plugins/eva/domains/octagons.ml
+++ b/src/plugins/eva/domains/octagons.ml
@@ -1177,8 +1177,6 @@ module State = struct
Format.fprintf fmt "@[%a@]" Octagons.pretty octagons
end)
- let log_category = Self.register_category "d-octagon"
-
let pretty_debug fmt { octagons; intervals; relations; deps } =
Format.fprintf fmt
"@[<v> Octagons: %a@; Intervals: %a@; Relations: %a@; Dependencies: %a@.]"
diff --git a/src/plugins/eva/domains/offsm_domain.ml b/src/plugins/eva/domains/offsm_domain.ml
index 4c5051422b7..e5c70d01a2d 100644
--- a/src/plugins/eva/domains/offsm_domain.ml
+++ b/src/plugins/eva/domains/offsm_domain.ml
@@ -30,8 +30,6 @@ let store_redundant = false
unsoundnesses in the domain through testing, because many more expressions
end up being handled. *)
-let dkey = Self.register_category "d-bitwise"
-
module Default_offsetmap = struct
open Cvalue
@@ -111,8 +109,6 @@ module D : Abstract_domain.Leaf
include Domain_builder.Complete (Memory)
- let log_category = dkey
-
let empty _ = Memory.empty_map
let enter_scope _kind _vars state = state (* default is Top, nothing to do *)
diff --git a/src/plugins/eva/domains/simple_memory.ml b/src/plugins/eva/domains/simple_memory.ml
index b935f55c6a9..e3aa413b1c7 100644
--- a/src/plugins/eva/domains/simple_memory.ml
+++ b/src/plugins/eva/domains/simple_memory.ml
@@ -196,8 +196,6 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
let value_dependencies = Abstract_value.Leaf (module Value)
let location_dependencies = Main_locations.ploc
- let log_category = Self.register_category ("d-" ^ Info.name)
-
let widen _kf _stmt = widen
(* This function returns the information known about the location
diff --git a/src/plugins/eva/domains/symbolic_locs.ml b/src/plugins/eva/domains/symbolic_locs.ml
index b7e3cf5ecc7..2dcedc78349 100644
--- a/src/plugins/eva/domains/symbolic_locs.ml
+++ b/src/plugins/eva/domains/symbolic_locs.ml
@@ -24,8 +24,6 @@ open Eval
open Eva_ast
open Locations
-let dkey = Self.register_category "d-symblocs"
-
module K = Hcexprs
module V = Cvalue.V (* TODO: functorize (with locations too ?) *)
@@ -470,8 +468,6 @@ module D : Abstract_domain.Leaf
include Domain_builder.Complete (Memory)
- let log_category = dkey
-
let empty _ = Memory.empty_map
let enter_scope _kind _vars state = state
diff --git a/src/plugins/eva/domains/taint_domain.ml b/src/plugins/eva/domains/taint_domain.ml
index bb9a3ed3a24..5721c9a5ae7 100644
--- a/src/plugins/eva/domains/taint_domain.ml
+++ b/src/plugins/eva/domains/taint_domain.ml
@@ -41,8 +41,6 @@ type taint_state = {
dependent_call: bool;
}
-let dkey = Self.register_category "d-taint"
-
(* Debug key to also include [assume_stmts] in the output of the
Frama_C_domain_show_each directive. *)
let dkey_debug = Self.register_category "d-taint-debug"
@@ -316,8 +314,6 @@ module Domain = struct
and type location := location
and type origin := origin)
- let log_category = dkey
-
(* Logic. *)
diff --git a/src/plugins/eva/domains/traces_domain.ml b/src/plugins/eva/domains/traces_domain.ml
index b6de18a2a56..1c7fbf5cef2 100644
--- a/src/plugins/eva/domains/traces_domain.ml
+++ b/src/plugins/eva/domains/traces_domain.ml
@@ -1103,8 +1103,6 @@ module D = struct
include Domain_builder.Complete (Traces)
- let log_category = Self.register_category "d-traces"
-
let assign ki lv e _v _valuation state =
let cil_lval = Eva_ast.to_cil_lval lv.Eval.lval in
let cil_exp = Eva_ast.to_cil_exp e in
diff --git a/src/plugins/eva/domains/unit_domain.ml b/src/plugins/eva/domains/unit_domain.ml
index caba1937bd9..ee1b2625f7a 100644
--- a/src/plugins/eva/domains/unit_domain.ml
+++ b/src/plugins/eva/domains/unit_domain.ml
@@ -20,15 +20,12 @@
(* *)
(**************************************************************************)
-let log_key = Self.register_category "unit-domain"
-
module Static = struct
module D = struct
include Datatype.Unit
type state = t
let name = "unit"
- let log_category = log_key
let structure = Abstract.Domain.Unit
let top = ()
diff --git a/tests/value/symbolic_locs.i b/tests/value/symbolic_locs.i
index 88195506235..4c6aae5ee2e 100644
--- a/tests/value/symbolic_locs.i
+++ b/tests/value/symbolic_locs.i
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: +"-eva-domains symbolic-locations -eva-msg-key d-symblocs"
+ STDOPT: +"-eva-domains symbolic-locations -eva-msg-key d-symbolic-locations"
*/
volatile int v;
@@ -9,10 +9,10 @@ void main1() {
unsigned int i = v;
int k = v;
- t[i] = 3;
+ t[i] = 3;
t[i] = t[i]+1; // The equality domain loses information here
u[k] = t[i] + 2; Frama_C_dump_each();
- int j = t[i] + u[k];
+ int j = t[i] + u[k];
int *p = &t[i]; Frama_C_dump_each();
int q = *p+1; // Does not write without adding something here, because otherwise we do a copy...
--
GitLab