From 83cb8b8d9b6fca28362ce12b65a4e83a47ae1621 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Wed, 8 Jun 2022 10:28:03 +0200
Subject: [PATCH] [Eva] In each domain module, defines the domain name.
Documents the need for a clear and simple name in the domain interface.
In the engine, the registration of abstractions does not change the domain name
anymore.
---
src/plugins/value/domains/abstract_domain.mli | 4 ++++
src/plugins/value/domains/cvalue/cvalue_domain.ml | 3 ++-
src/plugins/value/domains/domain_builder.ml | 1 +
src/plugins/value/domains/domain_builder.mli | 2 ++
src/plugins/value/domains/domain_product.ml | 7 ++++---
src/plugins/value/domains/equality/equality_domain.ml | 2 ++
src/plugins/value/domains/gauges/gauges_domain.ml | 2 ++
src/plugins/value/domains/inout_domain.ml | 2 +-
src/plugins/value/domains/multidim/multidim_domain.ml | 2 ++
src/plugins/value/domains/octagons.ml | 2 +-
src/plugins/value/domains/offsm_domain.ml | 2 ++
src/plugins/value/domains/printer_domain.ml | 1 +
src/plugins/value/domains/simple_memory.ml | 8 +++++---
src/plugins/value/domains/simple_memory.mli | 2 +-
src/plugins/value/domains/symbolic_locs.ml | 2 +-
src/plugins/value/domains/taint_domain.ml | 2 +-
src/plugins/value/domains/traces_domain.ml | 2 +-
src/plugins/value/domains/unit_domain.ml | 2 +-
src/plugins/value/engine/abstractions.ml | 1 -
19 files changed, 34 insertions(+), 15 deletions(-)
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index e8536eb1f6e..255d42d7ecd 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -376,6 +376,10 @@ module type S = sig
type state
include Datatype.S_with_collections with type t = state
+ (* The domain name, shown in some logs and in the GUI. Be sure to redefine a
+ clear and simple name instead of the default one coming from Datatype. *)
+ val name: string
+
(** {3 Lattice Structure } *)
include Lattice with type state := t
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 77f90be12ff..5a81d35d4f1 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -181,7 +181,8 @@ module State = struct
let mem_project = Datatype.never_any_project
end )
- let key = Structure.Key_Domain.create_key "cvalue_domain"
+ let name = "cvalue"
+ let key = Structure.Key_Domain.create_key name
type value = Model.value
type location = Model.location
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index 141c643cc70..6eadb1af7c2 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -325,6 +325,7 @@ module Restrict
module I = struct let module_name = Domain.name ^ " option" end
include Datatype.Option_with_collections (D) (I)
+ let name = Domain.name
let default = Domain.top, Mode.all
let structure: t Abstract.Domain.structure =
diff --git a/src/plugins/value/domains/domain_builder.mli b/src/plugins/value/domains/domain_builder.mli
index bf3c05b8f0c..bd0fd0c5f24 100644
--- a/src/plugins/value/domains/domain_builder.mli
+++ b/src/plugins/value/domains/domain_builder.mli
@@ -27,6 +27,8 @@ open Cil_types
open Eval
module type InputDomain = sig
+ (* The [name] value from Datatype should be the domain name and will be used
+ in some logs and in the GUI for the end-user. *)
include Datatype.S
val top: t
val join: t -> t -> t
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index 550a86f3d45..e158cb43b03 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -42,14 +42,15 @@ module Make
}
let () = incr counter
- let name = Left.name ^ "*" ^ Right.name ^
- "(" ^ string_of_int !counter ^ ")"
+ let unique_name = Left.name ^ "*" ^ Right.name ^
+ "(" ^ string_of_int !counter ^ ")"
include Datatype.Pair_with_collections
(Left)
(Right)
- (struct let module_name = name end)
+ (struct let module_name = unique_name end)
type state = t
+ let name = Left.name ^ " * " ^ Right.name
let structure = Abstract.Domain.Node (Left.structure, Right.structure)
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 44604b43c15..542d48cc2ce 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -121,6 +121,8 @@ module Internal = struct
type state = t
+ let name = "equality"
+
let log_category = dkey
let pretty fmt (eqs, _, _) = Equality.Set.pretty fmt eqs
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 7a91a6af3f8..829afa08364 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -532,6 +532,8 @@ module G = struct
(Datatype.List(Datatype.Pair(Cil_datatype.Stmt)(IterationInfo)))
(struct let module_name = "Values.Gauges_domain.G" end)
+ let name = "gauges"
+
let empty = MV.empty, []
let top (state: t) : t =
let top_iteration_info = function
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index 8028b618a1d..63af3599eaf 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -44,7 +44,7 @@ module LatticeInout = struct
include Datatype.Serializable_undefined
type t = inout
- let name = "Value.Inout.t"
+ let name = "inout"
let reprs = [ {
over_outputs = List.hd Zone.reprs;
diff --git a/src/plugins/value/domains/multidim/multidim_domain.ml b/src/plugins/value/domains/multidim/multidim_domain.ml
index 2f6459d9c5c..0a65d601baf 100644
--- a/src/plugins/value/domains/multidim/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim/multidim_domain.ml
@@ -363,6 +363,8 @@ struct
(Datatype.Option (Tracking))
(struct let module_name = "DomainLattice" end)
+ let name = "multidim"
+
type state = t
type value = Value.t
type value_or_uninitialized = Value_or_Uninitialized.t
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index 757ad4d87ec..b96b6bb17a5 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -701,7 +701,7 @@ module State = struct
type t = state
include Datatype.Serializable_undefined
- let name = "Octagons.State"
+ let name = "octagon"
let structural_descr =
Structural_descr.t_record
[| Octagons.packed_descr;
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 66ffd1337c2..65d6d1a2f6d 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -81,6 +81,8 @@ module Memory = struct
include
Lmap.Make_LOffset(V_Or_Uninitialized)(V_Offsetmap)(Default_offsetmap)
+ let name = "bitwise"
+
let widen kf stmt s1 s2 =
let wh = Widen.getWidenHints kf stmt in
widen wh s1 s2
diff --git a/src/plugins/value/domains/printer_domain.ml b/src/plugins/value/domains/printer_domain.ml
index ab4c24f45a6..93abea72d3e 100644
--- a/src/plugins/value/domains/printer_domain.ml
+++ b/src/plugins/value/domains/printer_domain.ml
@@ -34,6 +34,7 @@ module Simple : Simpler_domains.Simple_Cvalue = struct
(* In this domain, the states contain nothing. We use [unit] as type formal
the state and we reuse [Datatype.Unit] as a base for our domain. *)
include Datatype.Unit
+ let name = "printer"
(* --- Lattice operators --- *)
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 33bae1ed3a0..721c68c5ea8 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -47,7 +47,7 @@ module type S = sig
val fold: (Base.t -> value -> 'a -> 'a) -> t -> 'a -> 'a
end
-module Make_Memory (Value: Value) = struct
+module Make_Memory (Info: sig val name: string end) (Value: Value) = struct
module Initial_Values = struct let v = [] end
module Deps = struct let l = [Ast.self] end
@@ -55,8 +55,10 @@ module Make_Memory (Value: Value) = struct
include Hptmap.Make
(Base.Base) (Value) (Hptmap.Comp_unused) (Initial_Values) (Deps)
+ let name = Info.name
+
let cache_name s =
- Hptmap_sig.PersistentCache ("Value." ^ Value.name ^ "." ^ s)
+ Hptmap_sig.PersistentCache ("Value." ^ name ^ "." ^ s)
let disjoint_union =
let cache = cache_name "union" in
@@ -186,7 +188,7 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
try Some (Hashtbl.find table name)
with Not_found -> None
- module M = Make_Memory (Value)
+ module M = Make_Memory (Info) (Value)
include M
include Domain_builder.Complete (M)
diff --git a/src/plugins/value/domains/simple_memory.mli b/src/plugins/value/domains/simple_memory.mli
index a194b4fe987..bbbd93735a9 100644
--- a/src/plugins/value/domains/simple_memory.mli
+++ b/src/plugins/value/domains/simple_memory.mli
@@ -86,7 +86,7 @@ module type S = sig
end
(* Builds a memory from a value abstraction. *)
-module Make_Memory (Value: Value) : sig
+module Make_Memory (Info: sig val name: string end) (Value: Value) : sig
include Datatype.S_with_collections
include S with type t := t
and type value := Value.t
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 0d95237c647..a29ebf76b60 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -182,7 +182,7 @@ module Memory = struct
include Datatype.Serializable_undefined
type t = memory
- let name = "Value.Symbolic_locs.Memory.t"
+ let name = "symbolic-locations"
let reprs = [ { values = List.hd K2V.M.reprs;
zones = List.hd K2Z.reprs;
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index 7d46ca1e809..7cd38c393a8 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -75,7 +75,7 @@ module LatticeTaint = struct
type t = taint
- let name = "Value.Taint.t"
+ let name = "taint"
let reprs =
[ { locs_data = List.hd Zone.reprs;
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 52e14219be6..98cd954008c 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -532,7 +532,7 @@ module Traces = struct
include Datatype.Serializable_undefined
type t = state
- let name = "Value.Traces_domain.Traces.state"
+ let name = "traces"
let reprs = [empty]
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index 5307ef978d6..d7f7bb0a244 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -27,7 +27,7 @@ module Static = struct
include Datatype.Unit
type state = t
- let name = "Unit domain"
+ let name = "unit"
let log_category = log_key
let structure = Abstract.Domain.Unit
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index fedceb3f36f..c2221af9591 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -342,7 +342,6 @@ let add_domain (type v) dname mode (abstraction: v abstraction) (module Acc: Acc
(* Set the name of the domain. *)
let module Domain = struct
include (val domain)
- let name = dname
module Store = struct
include Store
let register_global_state storage state =
--
GitLab