From f81f29f6e9570813c73841d92be93fb1fd508e7c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 25 Jun 2021 15:14:32 +0200
Subject: [PATCH] [Eva] Sets domains names when building them in
abstractions.ml.
In domains, changes [Store.register_global_state] that now takes a boolean
argument indicating whether the domain states must be saved during the
analysis.
---
.../value/domains/apron/apron_domain.ml | 9 ---------
.../value/domains/cvalue/cvalue_domain.ml | 3 +--
src/plugins/value/domains/domain_builder.ml | 4 ++--
src/plugins/value/domains/domain_product.ml | 6 +++---
src/plugins/value/domains/domain_store.ml | 5 ++---
src/plugins/value/domains/domain_store.mli | 8 +++++++-
.../value/domains/equality/equality_domain.ml | 1 -
.../value/domains/gauges/gauges_domain.ml | 2 --
src/plugins/value/domains/inout_domain.ml | 2 --
src/plugins/value/domains/multidim_domain.ml | 1 -
src/plugins/value/domains/octagons.ml | 1 -
src/plugins/value/domains/offsm_domain.ml | 2 --
src/plugins/value/domains/printer_domain.ml | 1 -
src/plugins/value/domains/simple_memory.ml | 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/engine/abstractions.ml | 20 +++++++++++++++----
src/plugins/value/engine/compute_functions.ml | 3 ++-
src/plugins/value/engine/initialization.ml | 3 ++-
20 files changed, 35 insertions(+), 44 deletions(-)
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index 9d3ca7a4649..f112996ac47 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -352,7 +352,6 @@ 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
@@ -404,8 +403,6 @@ module Make (Man : Input) = struct
end )
include D
- let name = Man.name
-
let is_included = Abstract1.is_leq man
let join s1 s2 =
@@ -432,7 +429,6 @@ module Make (Man : Input) = struct
include Domain_builder.Complete
(struct
include D
- let name = name
let top = top
let join = join
end)
@@ -694,29 +690,24 @@ 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. *)
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index b7a0e91e222..a3df62f2573 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -181,7 +181,6 @@ module State = struct
let mem_project = Datatype.never_any_project
end )
- let name = "cvalue"
let key = Structure.Key_Domain.create_key "cvalue_domain"
type value = Model.value
@@ -455,7 +454,7 @@ module State = struct
let default () = false
end)
- let register_global_state _ = Storage.set true
+ let register_global_state _ _ = Storage.set true
let register_initial_state callstack (state, _clob) =
Db.Value.merge_initial_state callstack state
let register_state_before_stmt callstack stmt (state, _clob) =
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index d92cfab7144..6cb8e354211 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -589,9 +589,9 @@ module Restrict
module Store = struct
- let register_global_state state =
+ let register_global_state b state =
let state = state >>-: get_state in
- Domain.Store.register_global_state state
+ Domain.Store.register_global_state b state
let lift_register f state = f (get_state state)
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index 4ea88b8b41f..79ceb9c5876 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -324,9 +324,9 @@ module Make
| `Bottom, _ | _, `Bottom -> `Bottom
module Store = struct
- let register_global_state state =
- Left.Store.register_global_state (state >>-: fst);
- Right.Store.register_global_state (state >>-: snd)
+ let register_global_state b state =
+ Left.Store.register_global_state b (state >>-: fst);
+ Right.Store.register_global_state b (state >>-: snd)
let register_initial_state callstack (left, right) =
Left.Store.register_initial_state callstack left;
Right.Store.register_initial_state callstack right
diff --git a/src/plugins/value/domains/domain_store.ml b/src/plugins/value/domains/domain_store.ml
index c33e654ebac..23cf9353b87 100644
--- a/src/plugins/value/domains/domain_store.ml
+++ b/src/plugins/value/domains/domain_store.ml
@@ -31,7 +31,7 @@ end
module type S = sig
type t
- val register_global_state: t or_bottom -> unit
+ val register_global_state: bool -> t or_bottom -> unit
val register_initial_state: Value_types.callstack -> t -> unit
val register_state_before_stmt: Value_types.callstack -> stmt -> t -> unit
val register_state_after_stmt: Value_types.callstack -> stmt -> t -> unit
@@ -172,8 +172,7 @@ module Make (Domain: InputDomain) = struct
Callstack.Hashtbl.add r callstack v;
add stmt r
- let register_global_state state =
- let storage = not (Value_parameters.NoResultsDomains.mem Domain.name) in
+ let register_global_state storage state =
Storage.set storage;
if storage then
match state with
diff --git a/src/plugins/value/domains/domain_store.mli b/src/plugins/value/domains/domain_store.mli
index 136b3ba458e..fd9ddfd450d 100644
--- a/src/plugins/value/domains/domain_store.mli
+++ b/src/plugins/value/domains/domain_store.mli
@@ -32,7 +32,13 @@ end
(** Automatic storage of the states computed during the analysis. *)
module type S = sig
type t
- val register_global_state: t or_bottom -> unit
+
+ (** Called once at the analysis beginning for the entry state of the main
+ function. The boolean indicates whether the states of this domain must be
+ saved during the analysis, according to options -eva-no-results. If it is
+ false, register functions must do nothing, and get functions return Top. *)
+ val register_global_state: bool -> t or_bottom -> unit
+
val register_initial_state: Value_types.callstack -> t -> unit
val register_state_before_stmt: Value_types.callstack -> stmt -> t -> unit
val register_state_after_stmt: Value_types.callstack -> stmt -> t -> unit
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 2d02024b041..e345ba15493 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -121,7 +121,6 @@ module Internal = struct
type state = t
- let name = "equality"
let log_category = dkey
let key = Structure.Key_Domain.create_key "equality_domain"
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index cb2df307734..3d5c2e30191 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -538,8 +538,6 @@ 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 4dcf4b41c17..946b34461d0 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -95,8 +95,6 @@ module LatticeInout = struct
end)
- let name = "inout"
-
(* Initial abstract at the beginning of the computation: nothing written
or read so far. *)
let empty = {
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index 98f7f2f7912..90abdbb2f7b 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -241,7 +241,6 @@ struct
(Base.Base) (Memory)
(Hptmap.Comp_unused) (Initial_Values) (Deps)
- let name = "multidim"
let log_category = dkey
let cache_name s =
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index 66376372155..b8968a5f139 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -753,7 +753,6 @@ module State = struct
Format.fprintf fmt "@[%a@]" Octagons.pretty octagons
end)
- let name = "octagon"
let log_category = Value_parameters.register_category "d-octagon"
let pretty_debug fmt { octagons; intervals; relations } =
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 826c01725ab..235d98ba990 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -86,8 +86,6 @@ module Memory = struct
widen wh s1 s2
let narrow x _y = `Value x
-
- let name = "bitwise"
end
diff --git a/src/plugins/value/domains/printer_domain.ml b/src/plugins/value/domains/printer_domain.ml
index c550a08af7a..0be9f3fb61d 100644
--- a/src/plugins/value/domains/printer_domain.ml
+++ b/src/plugins/value/domains/printer_domain.ml
@@ -34,7 +34,6 @@ 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 1e44803fbce..fa09688306a 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -191,8 +191,6 @@ module Make_Domain (Info: sig val name: string end) (Value: Value) = struct
include Domain_builder.Complete (M)
- let name = Info.name
-
type state = t
type value = Value.t
type location = Precise_locs.precise_location
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 2c854e77977..f4d8f92b93d 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -215,8 +215,6 @@ module Memory = struct
end)
- let name = "symbolic-locations"
-
let top = {
values = K2V.M.empty;
zones = K2Z.empty;
diff --git a/src/plugins/value/domains/taint_domain.ml b/src/plugins/value/domains/taint_domain.ml
index 53d5dcd618f..aec330a279e 100644
--- a/src/plugins/value/domains/taint_domain.ml
+++ b/src/plugins/value/domains/taint_domain.ml
@@ -106,8 +106,6 @@ module LatticeTaint = struct
end)
- let name = "taint"
-
(* Initial state at the start of the computation: nothing is tainted yet. *)
let empty = {
locs_data = Zone.bottom;
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 20918ad9f2c..88ccb4412c5 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -571,8 +571,6 @@ module Traces = struct
end)
- let name = "traces"
-
let view m =
if m == top then `Top
else `Other m
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 4497123b493..3915bb1a4f0 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -323,7 +323,7 @@ let eq_value:
| Abstract.Value.Leaf (key, _) -> Abstract.Value.eq_type key V.key
| _ -> None
-let add_domain (type v) mode (abstraction: v abstraction) (module Acc: Acc) =
+let add_domain (type v) dname mode (abstraction: v abstraction) (module Acc: Acc) =
let domain : (module internal_domain with type value = Acc.Val.t) =
match abstraction.domain with
| Functor make ->
@@ -343,15 +343,27 @@ let add_domain (type v) mode (abstraction: v abstraction) (module Acc: Acc) =
let module Convert = Internal_Value.Convert (Acc.Val) (Struct) in
(module Domain_lift.Make (Domain) (Convert))
in
+ (* 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 =
+ let no_results = Value_parameters.NoResultsDomains.mem dname in
+ register_global_state (storage && not no_results) state
+ end
+ end in
+ (* Restricts the domain according to [mode]. *)
let domain : (module internal_domain with type value = Acc.Val.t) =
match mode with
- | None -> domain
+ | None -> (module Domain)
| Some kf_modes ->
let module Scope = struct let functions = kf_modes end in
let module Domain =
Domain_builder.Restrict
(Acc.Val)
- ((val domain))
+ (Domain)
(Scope)
in
(module Domain)
@@ -378,7 +390,7 @@ let warn_experimental flag =
let build_domain config abstract =
let build (Flag flag, mode) acc =
warn_experimental flag;
- add_domain mode flag.abstraction acc
+ add_domain flag.name mode flag.abstraction acc
in
(* Domains in the [config] are sorted by increasing priority: domains with
higher priority are added last: they will be at the top of the domains
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index ece699c60df..4d517e199e2 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -375,7 +375,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let compute_from_init_state kf init_state =
pre_analysis ();
- Abstract.Dom.Store.register_global_state (`Value init_state);
+ let b = Value_parameters.ResultsAll.get () in
+ Abstract.Dom.Store.register_global_state b (`Value init_state);
compute kf init_state
end
diff --git a/src/plugins/value/engine/initialization.ml b/src/plugins/value/engine/initialization.ml
index 2be609d248d..eacfe860a70 100644
--- a/src/plugins/value/engine/initialization.ml
+++ b/src/plugins/value/engine/initialization.ml
@@ -397,7 +397,8 @@ module Make
state
end
in
- Domain.Store.register_global_state init_state;
+ let b = Value_parameters.ResultsAll.get () in
+ Domain.Store.register_global_state b init_state;
print_initial_cvalue_state init_state;
init_state >>-: add_main_formals kf
--
GitLab