From e342fcf1bfdb76af808bdd392cb4c1e041b090cc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 23 Aug 2019 16:17:20 +0200
Subject: [PATCH] [Eva] New file abstract defining the Internal and External
module types.
These module definitions were previously in abstract_value, abstract_location
and abstract_domain. They are now grouped in this new file for the three
abstractions.
These module types should only be useful for the engine, and need not to be
visible in the implementation of the various abstractions.
New module type Leaf in abstract_value, abstract_location and abstract_domain
with the key identifying the module. The internal structure is no longer needed
in these abstractions, and is instead built by the engine from this key.
Keys are no longer exported outside the modules.
For abstract domains, the key is automatically created by the functor
Domain_builder.Complete from the domain name.
Many changes throughout the analyzer:
- in the engine, Abstract_value.{Internal|External} becomes
Abstract.Value.{Internal|External}.
- in the abstractions, Abstract_value.Internal becomes Abstract_value.Leaf.
---
Makefile | 2 +-
headers/header_spec.txt | 2 +
src/plugins/value/domains/abstract_domain.mli | 74 +------
.../value/domains/apron/apron_domain.ko.ml | 15 +-
.../value/domains/apron/apron_domain.mli | 12 +-
.../value/domains/apron/apron_domain.ok.ml | 17 +-
.../value/domains/cvalue/cvalue_domain.ml | 11 +-
.../value/domains/cvalue/cvalue_domain.mli | 13 +-
.../value/domains/cvalue/locals_scoping.ml | 2 -
.../value/domains/cvalue/locals_scoping.mli | 2 -
src/plugins/value/domains/domain_builder.ml | 7 +-
src/plugins/value/domains/domain_builder.mli | 26 +--
src/plugins/value/domains/domain_lift.ml | 1 -
src/plugins/value/domains/domain_product.ml | 2 -
.../value/domains/equality/equality_domain.ml | 9 +-
.../domains/equality/equality_domain.mli | 7 +-
.../value/domains/gauges/gauges_domain.ml | 4 +-
.../value/domains/gauges/gauges_domain.mli | 2 +-
src/plugins/value/domains/inout_domain.ml | 4 +-
src/plugins/value/domains/inout_domain.mli | 4 +-
.../domains/numerors/numerors_domain.mli | 8 +-
.../domains/numerors/numerors_domain.ok.ml | 21 +-
src/plugins/value/domains/offsm_domain.ml | 1 -
src/plugins/value/domains/offsm_domain.mli | 2 +-
src/plugins/value/domains/printer_domain.mli | 4 +-
src/plugins/value/domains/sign_domain.mli | 4 +-
src/plugins/value/domains/simple_memory.ml | 3 -
src/plugins/value/domains/simple_memory.mli | 4 +-
src/plugins/value/domains/symbolic_locs.ml | 1 -
src/plugins/value/domains/symbolic_locs.mli | 2 +-
src/plugins/value/domains/traces_domain.ml | 6 +-
src/plugins/value/domains/traces_domain.mli | 2 +-
src/plugins/value/domains/unit_domain.ml | 2 +-
src/plugins/value/domains/unit_domain.mli | 2 +-
src/plugins/value/engine/abstractions.ml | 205 +++++++++++-------
src/plugins/value/engine/abstractions.mli | 8 +-
src/plugins/value/engine/compute_functions.ml | 19 +-
src/plugins/value/engine/evaluation.ml | 2 +-
src/plugins/value/engine/evaluation.mli | 2 +-
src/plugins/value/engine/initialization.ml | 14 +-
src/plugins/value/engine/initialization.mli | 2 +-
src/plugins/value/engine/iterator.ml | 4 +-
src/plugins/value/engine/partition.ml | 4 +-
.../value/engine/partitioning_index.ml | 7 +-
.../value/engine/partitioning_index.mli | 3 +-
.../value/engine/subdivided_evaluation.ml | 8 +-
.../value/engine/subdivided_evaluation.mli | 2 +-
.../value/engine/transfer_specification.ml | 8 +-
src/plugins/value/engine/transfer_stmt.ml | 12 +-
src/plugins/value/gui_files/gui_eval.ml | 6 +-
src/plugins/value/gui_files/gui_types.ml | 4 +-
src/plugins/value/register.ml | 9 +-
src/plugins/value/utils/abstract.ml | 75 +++++++
src/plugins/value/utils/abstract.mli | 113 ++++++++++
.../value/values/abstract_location.mli | 17 +-
src/plugins/value/values/abstract_value.mli | 17 +-
src/plugins/value/values/location_lift.ml | 4 +-
src/plugins/value/values/location_lift.mli | 8 +-
src/plugins/value/values/main_locations.ml | 4 +-
src/plugins/value/values/main_locations.mli | 6 +-
src/plugins/value/values/main_values.ml | 8 +-
src/plugins/value/values/main_values.mli | 10 +-
.../value/values/numerors/numerors_value.ml | 3 +-
.../value/values/numerors/numerors_value.mli | 4 +-
src/plugins/value/values/offsm_value.ml | 11 +-
src/plugins/value/values/offsm_value.mli | 7 +-
src/plugins/value/values/sign_value.ml | 3 +-
src/plugins/value/values/sign_value.mli | 4 +-
src/plugins/value/values/value_product.ml | 6 +-
src/plugins/value/values/value_product.mli | 6 +-
70 files changed, 502 insertions(+), 401 deletions(-)
create mode 100644 src/plugins/value/utils/abstract.ml
create mode 100644 src/plugins/value/utils/abstract.mli
diff --git a/Makefile b/Makefile
index ce5d740b6d4..334437fc823 100644
--- a/Makefile
+++ b/Makefile
@@ -878,7 +878,7 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
slevel/per_stmt_slevel \
utils/library_functions \
utils/eval_typ utils/backward_formals \
- alarmset eval utils/structure \
+ alarmset eval utils/structure utils/abstract \
values/value_product values/location_lift \
values/cvalue_forward values/cvalue_backward \
values/main_values values/main_locations \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index f5f65ba9305..b66be1d6251 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1272,6 +1272,8 @@ src/plugins/value/slevel/split_strategy.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/slevel/split_strategy.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/test.assert.sh: .ignore
src/plugins/value/test.sh: .ignore
+src/plugins/value/utils/abstract.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/utils/abstract.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/backward_formals.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/backward_formals.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/utils/eval_typ.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index 9bf4563c8cd..4c77a147588 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -396,73 +396,12 @@ module type S = sig
val initialize_variable_using_type: init_kind -> varinfo -> t -> t
include Recycle with type t := t
-end
-
-
-(** Keys identify abstract domains through the type of their abstract values. *)
-type 'a key = 'a Structure.Key_Domain.key
-
-(** Describes the internal structure of a domain.
- Used internally to automatically generate efficient accessors from a
- generic abstract domain, which may be a combination of several domains,
- to a specific one. *)
-type 'a structure = 'a Structure.Key_Domain.structure =
- | Void : 'a structure
- | Leaf : 'a key -> 'a structure
- | Node : 'a structure * 'b structure -> ('a * 'b) structure
-
-(**
- For a simple 'leaf' domain, the structure should be:
- [let key = Structure.Key_Domain.create_key "name_of_the_domain";;
- let structure = Leaf key;;]
-
- Then, the key should be exported by the domain, to allow the use of the
- functions defined in the {!Interface} interface below.
-
- A compound domain may use the {!Node} constructor to provide a separate
- access to each of its parts.
-
- A domain can also use the {!Void} constructor to prevent access to itself.
-*)
-
-(** Structure of a domain. *)
-module type S_with_Structure = sig
- include S
-
- (** A structure matching the type of the domain. *)
- val structure : t structure
(** Category for the messages about the domain.
Must be created through {!Value_parameters.register_category}. *)
val log_category : Value_parameters.category
end
-(** External interface of a domain, with accessors.
- Automatically built by the functor {!Structure.Open}.
- When a generic domain is a combination of several domains, these functions
- allow interacting with its subparts. Note that their behavior is undefined
- if the overall domain contains several times the same domain. *)
-module type Interface = sig
- type t
-
- (** Tests whether a key belongs to the domain. *)
- val mem : 'a key -> bool
-
- (** For a key of type [k key]:
- - if the states of this domain (of type [t]) contain a part (of type [k])
- from the domain identified by the key,
- then [get key] returns an accessor for this part of a state.
- - otherwise, [get key] returns None. *)
- val get : 'a key -> (t -> 'a) option
-
- (** For a key of type [k key]:
- - if the states of this domain (of type [t]) contain a part (of type [k])
- from the domain identified by the key,
- then [set key d state] returns the state [state] in which this part
- has been replaced by [d].
- - otherwise, [set key _] is the identity function. *)
- val set : 'a key -> 'a -> t -> t
-end
(** Automatic storage of the states computed during the analysis. *)
module type Store = sig
@@ -487,7 +426,7 @@ end
(** Full implementation of domains. Automatically built by
{!Domain_builder.Complete} from an {!S_with_Structure} domain. *)
module type Internal = sig
- include S_with_Structure
+ include S
module Store: Store with type state := state
(** This function is called after the analysis. The argument is the state
@@ -497,11 +436,14 @@ module type Internal = sig
val post_analysis: t or_bottom -> unit
end
-(** Final interface of domains, as generated and used by Eva, with generic
- accessors for domains. *)
-module type External = sig
+type 't key = 't Structure.Key_Domain.key
+
+(** Signature for a leaf module of a domain. *)
+module type Leaf = sig
include Internal
- include Interface with type t := state
+
+ (** The key identifies the domain and the type [t] of its states. *)
+ val key: t key
end
diff --git a/src/plugins/value/domains/apron/apron_domain.ko.ml b/src/plugins/value/domains/apron/apron_domain.ko.ml
index 9ccb3680e29..cde2dc82ad6 100644
--- a/src/plugins/value/domains/apron/apron_domain.ko.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ko.ml
@@ -22,11 +22,14 @@
let ok = false
-module type S = Abstract_domain.Internal
+module type S = Abstract_domain.Leaf
with type value = Main_values.Interval.t
and type location = Precise_locs.precise_location
-module U = Unit_domain.Make (Main_values.Interval) (Main_locations.PLoc)
+module U = struct
+ include Unit_domain.Make (Main_values.Interval) (Main_locations.PLoc)
+ let key = Structure.Key_Domain.create_key "dummy_apron"
+end
module Octagon = U
module Box = U
@@ -34,14 +37,6 @@ module Polka_Loose = U
module Polka_Strict = U
module Polka_Equalities = U
-let dummy_key = Structure.Key_Domain.create_key "dummy_apron"
-let octagon_key = dummy_key
-let box_key = dummy_key
-let polka_loose_key = dummy_key
-let polka_strict_key = dummy_key
-let polka_equalities_key = dummy_key
-
-
(*
Local Variables:
compile-command: "make -C ../../../.."
diff --git a/src/plugins/value/domains/apron/apron_domain.mli b/src/plugins/value/domains/apron/apron_domain.mli
index 19c6611afb1..b330002eca9 100644
--- a/src/plugins/value/domains/apron/apron_domain.mli
+++ b/src/plugins/value/domains/apron/apron_domain.mli
@@ -28,7 +28,7 @@
val ok : bool
(** Signature of an Apron domain in Eva. *)
-module type S = Abstract_domain.Internal
+module type S = Abstract_domain.Leaf
with type value = Main_values.Interval.t
and type location = Precise_locs.precise_location
@@ -51,16 +51,6 @@ module Polka_Strict : S
(** Linear equalities. *)
module Polka_Equalities : S
-
-(** Domain keys for the Apron domains in Eva. *)
-
-val octagon_key : Octagon.t Abstract_domain.key
-val box_key : Box.t Abstract_domain.key
-val polka_loose_key : Polka_Loose.t Abstract_domain.key
-val polka_strict_key : Polka_Strict.t Abstract_domain.key
-val polka_equalities_key : Polka_Equalities.t Abstract_domain.key
-
-
(*
Local Variables:
compile-command: "make -C ../../../.."
diff --git a/src/plugins/value/domains/apron/apron_domain.ok.ml b/src/plugins/value/domains/apron/apron_domain.ok.ml
index e69f47ab862..160d5ced136 100644
--- a/src/plugins/value/domains/apron/apron_domain.ok.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ok.ml
@@ -32,7 +32,7 @@ let ok = true
let debug = false
-module type S = Abstract_domain.Internal
+module type S = Abstract_domain.Leaf
with type value = Main_values.Interval.t
and type location = Precise_locs.precise_location
@@ -362,7 +362,6 @@ module Make
type t
val manager: t Manager.t
val name: string
- val key: t Abstract1.t Abstract_domain.key
end)
= struct
@@ -371,8 +370,6 @@ module Make
type location = Precise_locs.precise_location
let man = Man.manager
-
- let structure = Abstract_domain.Leaf Man.key
let log_category = dkey
let empty_env = Environment.make [||] [||]
@@ -725,44 +722,32 @@ module Make
end
-let octagon_key = Structure.Key_Domain.create_key "apron-octagon"
-let box_key = Structure.Key_Domain.create_key "apron-box"
-let polka_loose_key = Structure.Key_Domain.create_key "polka-loose"
-let polka_strict_key = Structure.Key_Domain.create_key "polka-strict"
-let polka_equalities_key = Structure.Key_Domain.create_key "polka-equalities"
-
-
module Apron_Octagon = struct
type t = Oct.t
let manager = Oct.manager_alloc ()
let name = "Apron octagon domain"
- let key = octagon_key
end
module Apron_Box = struct
type t = Box.t
let manager = Box.manager_alloc ()
let name = "Apron box domain"
- let key = box_key
end
module Apron_Polka_Loose = struct
type t = Polka.loose Polka.t
let manager = Polka.manager_alloc_loose ()
let name = "Polka loose polyhedra domain"
- let key = polka_loose_key
end
module Apron_Polka_Strict = struct
type t = Polka.strict Polka.t
let manager = Polka.manager_alloc_strict ()
let name = "Polka strict polyhedra domain"
- let key = polka_strict_key
end
module Apron_Polka_Equalities = struct
type t = Polka.equalities Polka.t
let manager = Polka.manager_alloc_equalities ()
let name = "Polka linear equalities domain"
- let key = polka_equalities_key
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 841850c4fef..3c0579fa646 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -29,7 +29,7 @@ let extract get = match get key with
| None -> fun _ -> Cvalue.Model.top
| Some get -> function
| `Bottom -> Cvalue.Model.bottom
- | `Value state -> get state
+ | `Value state -> fst (get state)
module Model = struct
@@ -168,10 +168,6 @@ module State = struct
type state = Model.t * Locals_scoping.clobbered_set
- let structure =
- Abstract_domain.Node (Abstract_domain.Leaf key,
- Abstract_domain.Leaf Locals_scoping.key)
-
let log_category = Value_parameters.dkey_cvalue_domain
include Datatype.Make_with_collections (
@@ -193,6 +189,7 @@ module State = struct
end )
let name = "Cvalue domain"
+ let key = key
type value = Model.value
type location = Model.location
@@ -562,12 +559,12 @@ module Subpart = struct
let hash = Model.hash_subtree
let equal = Model.equal_subtree
end
-let distinct_subpart a b =
+let distinct_subpart (a, _) (b, _) =
if Model.equal a b then None
else
try Model.comp_prefixes a b; None
with Model.Found_prefix (p, s1, s2) -> Some (p, s1, s2)
-let find_subpart s prefix = Model.find_prefix s prefix
+let find_subpart (s, _) prefix = Model.find_prefix s prefix
(*
Local Variables:
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.mli b/src/plugins/value/domains/cvalue/cvalue_domain.mli
index 34436ded0ad..bd1284006ff 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.mli
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.mli
@@ -22,15 +22,14 @@
(** Main domain of the Value Analysis. *)
-module State : Abstract_domain.Internal
+module State : Abstract_domain.Leaf
with type value = Main_values.CVal.t
and type location = Main_locations.PLoc.location
-
-
-val key : Cvalue.Model.t Abstract_domain.key
+ and type state = Cvalue.Model.t * Locals_scoping.clobbered_set
val extract :
- (Cvalue.Model.t Abstract_domain.key -> ('state -> Cvalue.Model.t) option) ->
+ (State.t Structure.Key_Domain.key ->
+ ('state -> State.t) option) ->
'state Eval.or_bottom -> Cvalue.Model.t
val inject : Cvalue.Model.t -> State.t
@@ -42,8 +41,8 @@ val project : State.t -> Cvalue.Model.t
type prefix
module Subpart : Hashtbl.HashedType
val distinct_subpart :
- Cvalue.Model.t -> Cvalue.Model.t -> (prefix * Subpart.t * Subpart.t) option
-val find_subpart : Cvalue.Model.t -> prefix -> Subpart.t option
+ State.t -> State.t -> (prefix * Subpart.t * Subpart.t) option
+val find_subpart : State.t -> prefix -> Subpart.t option
diff --git a/src/plugins/value/domains/cvalue/locals_scoping.ml b/src/plugins/value/domains/cvalue/locals_scoping.ml
index 2059c345c71..0399ececdac 100644
--- a/src/plugins/value/domains/cvalue/locals_scoping.ml
+++ b/src/plugins/value/domains/cvalue/locals_scoping.ml
@@ -27,8 +27,6 @@ type clobbered_set = {
mutable clob: Base.SetLattice.t
}
-let key = Structure.Key_Domain.create_key "clobbered_set"
-
let structural_descr =
let open Structural_descr in
t_record [| Base.SetLattice.packed_descr |]
diff --git a/src/plugins/value/domains/cvalue/locals_scoping.mli b/src/plugins/value/domains/cvalue/locals_scoping.mli
index e0b8c5d181d..8f083545385 100644
--- a/src/plugins/value/domains/cvalue/locals_scoping.mli
+++ b/src/plugins/value/domains/cvalue/locals_scoping.mli
@@ -30,8 +30,6 @@ type clobbered_set = {
mutable clob: Base.SetLattice.t
}
-val key: clobbered_set Abstract_domain.key
-
val structural_descr: Structural_descr.t
val bottom: unit -> clobbered_set
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index b27b01329e1..7406f3753dd 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -22,7 +22,7 @@
module type InputDomain = sig
- include Abstract_domain.S_with_Structure
+ include Abstract_domain.S
val storage: unit -> bool
end
@@ -33,6 +33,9 @@ module Complete
include Domain
module Store = Domain_store.Make (Domain)
+ let key: Domain.t Structure.Key_Domain.key =
+ Structure.Key_Domain.create_key Domain.name
+
let post_analysis _state = ()
end
@@ -57,7 +60,6 @@ module Make_Minimal
include Domain
- let structure = Abstract_domain.Void
let log_category = Value_parameters.register_category ("d-" ^ name)
type value = Value.t
@@ -185,7 +187,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 structure = Abstract_domain.Void
let log_category = Value_parameters.register_category ("d-" ^ name)
type value = Cvalue.V.t
diff --git a/src/plugins/value/domains/domain_builder.mli b/src/plugins/value/domains/domain_builder.mli
index 7d3b426a606..1eddbb4b8b5 100644
--- a/src/plugins/value/domains/domain_builder.mli
+++ b/src/plugins/value/domains/domain_builder.mli
@@ -24,34 +24,34 @@
simplified interfaces. *)
module type InputDomain = sig
- include Abstract_domain.S_with_Structure
+ include Abstract_domain.S
val storage: unit -> bool
end
module Complete
(Domain: InputDomain)
- : Abstract_domain.Internal with type state = Domain.state
- and type value = Domain.value
- and type location = Domain.location
+ : Abstract_domain.Leaf with type state = Domain.state
+ and type value = Domain.value
+ and type location = Domain.location
module Complete_Minimal
(Value: Abstract_value.S)
(Location: Abstract_location.S)
(Domain: Simpler_domains.Minimal)
- : Abstract_domain.Internal with type value = Value.t
- and type location = Location.location
- and type state = Domain.t
+ : Abstract_domain.Leaf with type value = Value.t
+ and type location = Location.location
+ and type state = Domain.t
module Complete_Minimal_with_datatype
(Value: Abstract_value.S)
(Location: Abstract_location.S)
(Domain: Simpler_domains.Minimal_with_datatype)
- : Abstract_domain.Internal with type value = Value.t
- and type location = Location.location
- and type state = Domain.t
+ : Abstract_domain.Leaf with type value = Value.t
+ and type location = Location.location
+ and type state = Domain.t
module Complete_Simple_Cvalue
(Domain: Simpler_domains.Simple_Cvalue)
- : Abstract_domain.Internal with type value = Cvalue.V.t
- and type location = Precise_locs.precise_location
- and type state = Domain.t
+ : Abstract_domain.Leaf with type value = Cvalue.V.t
+ and type location = Precise_locs.precise_location
+ and type state = Domain.t
diff --git a/src/plugins/value/domains/domain_lift.ml b/src/plugins/value/domains/domain_lift.ml
index 02eaa96e98d..d53990a56cc 100644
--- a/src/plugins/value/domains/domain_lift.ml
+++ b/src/plugins/value/domains/domain_lift.ml
@@ -45,7 +45,6 @@ module Make
include (Domain : Datatype.S_with_collections with type t = Domain.t)
include (Domain : Abstract_domain.Lattice with type state = Domain.state)
- let structure = Domain.structure
let log_category = Domain.log_category
type value = Convert.extended_value
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index e596deec5d4..d35d7c7c791 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -51,8 +51,6 @@ module Make
(struct let module_name = name end)
type state = t
- let structure = Abstract_domain.Node (Left.structure, Right.structure)
-
let log_category = product_category
let top = Left.top, Right.top
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 7ccb02c9721..7186aaebe57 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -122,9 +122,8 @@ module Internal = struct
type state = t
let name = "Equality domain"
- let key = Structure.Key_Domain.create_key "equality_domain"
- let structure : t Abstract_domain.structure = Abstract_domain.Leaf key
let log_category = dkey
+ let key = Structure.Key_Domain.create_key "equality_domain"
type equalities = Equality.Set.t
let project (t, _, _) = t
@@ -180,13 +179,13 @@ module Store = Domain_store.Make (Internal)
(* ------------------------- Abstract Domain -------------------------------- *)
module Make
- (Value : Abstract_value.External)
+ (Value : Abstract.Value.External)
= struct
include Internal
module Store = Store
- let get_cvalue = Value.get Main_values.cvalue_key
+ let get_cvalue = Value.get Main_values.CVal.key
type value = Value.t
type location = Precise_locs.precise_location
@@ -218,7 +217,7 @@ module Make
let c = get v in
if Cvalue.V.is_imprecise c then
let c' = Cvalue.V.topify_with_origin Origin.top c in
- Value.set Main_values.cvalue_key c' v
+ Value.set Main_values.CVal.key c' v
else v
let coop_eval oracle equalities atom_src =
diff --git a/src/plugins/value/domains/equality/equality_domain.mli b/src/plugins/value/domains/equality/equality_domain.mli
index 6f6d0416541..1242e9d2e9c 100644
--- a/src/plugins/value/domains/equality/equality_domain.mli
+++ b/src/plugins/value/domains/equality/equality_domain.mli
@@ -31,10 +31,9 @@ type call_init_state =
| ISEmpty (** completely empty state, without impact on Memexec. *)
-module Make (Value : Abstract_value.External) : sig
- include Abstract_domain.Internal with type value = Value.t
- and type location = Precise_locs.precise_location
- val key : t Abstract_domain.key
+module Make (Value : Abstract.Value.External) : sig
+ include Abstract_domain.Leaf with type value = Value.t
+ and type location = Precise_locs.precise_location
val pretty_debug : Format.formatter -> t -> unit
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 1af31275192..e45fc726212 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1120,7 +1120,7 @@ end
let dkey = Value_parameters.register_category "d-gauges"
-module D_Impl : Abstract_domain.S_with_Structure
+module D_Impl : Abstract_domain.S
with type state = G.t
and type value = Cvalue.V.t
and type location = Precise_locs.precise_location
@@ -1132,8 +1132,6 @@ module D_Impl : Abstract_domain.S_with_Structure
include G
let name = "Gauges domain"
-
- let structure = Abstract_domain.Void
let log_category = dkey
let empty _ = G.empty
diff --git a/src/plugins/value/domains/gauges/gauges_domain.mli b/src/plugins/value/domains/gauges/gauges_domain.mli
index a1609d838a0..f51fdfbc660 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.mli
+++ b/src/plugins/value/domains/gauges/gauges_domain.mli
@@ -23,6 +23,6 @@
(** Gauges domain ("Arnaud Venet: The Gauge Domain: Scalable Analysis of
Linear Inequality Invariants. CAV 2012") *)
-module D: Abstract_domain.Internal
+module D: Abstract_domain.Leaf
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index 12ba3cd1528..1a5a4888c93 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -204,8 +204,6 @@ module Transfer = struct
end
-let key = Structure.Key_Domain.create_key "inout domain"
-
module Internal
(*: Domain_builder.InputDomain
with type state = inout
@@ -221,7 +219,7 @@ module Internal
include Abstract_domain.Lattice with type state := state
end)
- let structure : t Abstract_domain.structure = Abstract_domain.Leaf key
+ let name = "inout"
let log_category = Value_parameters.register_category "d-inout"
let enter_scope _kf _vars state = state
diff --git a/src/plugins/value/domains/inout_domain.mli b/src/plugins/value/domains/inout_domain.mli
index 0304f94f690..f759f59bfe6 100644
--- a/src/plugins/value/domains/inout_domain.mli
+++ b/src/plugins/value/domains/inout_domain.mli
@@ -22,8 +22,6 @@
(** Computation of inputs of outputs. *)
-module D: Abstract_domain.Internal
+module D: Abstract_domain.Leaf
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
-
-val key: D.t Abstract_domain.key
diff --git a/src/plugins/value/domains/numerors/numerors_domain.mli b/src/plugins/value/domains/numerors/numerors_domain.mli
index 00b7a2ea972..c00510fa309 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.mli
+++ b/src/plugins/value/domains/numerors/numerors_domain.mli
@@ -35,15 +35,15 @@ val ok: bool
numerors values on casts from integer to floating-point values.
Fails if numerors domain is not available. *)
val add_numerors_value:
- (module Abstract_value.Internal) -> (module Abstract_value.Internal)
+ (module Abstract.Value.Internal) -> (module Abstract.Value.Internal)
(* From a given abstract value product, creates the reduction function that
reduces numerors values by using cvalues. Returns the identity if the given
value product does not contain numerors and cvalue componants. *)
val reduce_error:
- (module Abstract_value.External with type t = 'v) -> ('v -> 'v)
+ (module Abstract.Value.External with type t = 'v) -> ('v -> 'v)
(** Returns the numerors domain module, if available. Fails otherwise. *)
val numerors_domain:
- unit -> (module Abstract_domain.Internal with type value = value
- and type location = location)
+ unit -> (module Abstract_domain.Leaf with type value = value
+ and type location = location)
diff --git a/src/plugins/value/domains/numerors/numerors_domain.ok.ml b/src/plugins/value/domains/numerors/numerors_domain.ok.ml
index cf8e73a78c4..8603b8643b0 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ok.ml
+++ b/src/plugins/value/domains/numerors/numerors_domain.ok.ml
@@ -27,7 +27,7 @@ open Cil_types
type value = Numerors_value.t
type location = Precise_locs.precise_location
-let value_key = Numerors_value.error_key
+let value_key = Numerors_value.key
let ok = true
@@ -87,12 +87,15 @@ module Numerors_Value = struct
]
end
-let add_numerors_value (module Value: Abstract_value.Internal) =
+let add_numerors_value (module Value: Abstract.Value.Internal) =
let module External_Value = Structure.Open (Structure.Key_Value) (Value) in
let module V = struct
include Value_product.Make (Value) (Numerors_value)
- let forward_cast = match External_Value.get Main_values.cvalue_key with
+ let structure =
+ Abstract.Value.(Node (Value.structure, Leaf Numerors_value.key))
+
+ let forward_cast = match External_Value.get Main_values.CVal.key with
| None -> forward_cast
| Some get_cvalue ->
fun ~src_type ~dst_type (value, num) ->
@@ -116,13 +119,13 @@ let add_numerors_value (module Value: Abstract_value.Internal) =
in
value', num
end in
- (module V: Abstract_value.Internal)
+ (module V: Abstract.Value.Internal)
-let reduce_error (type v) (module V: Abstract_value.External with type t = v) =
- match V.get Numerors_value.error_key, V.get Main_values.cvalue_key with
+let reduce_error (type v) (module V: Abstract.Value.External with type t = v) =
+ match V.get Numerors_value.key, V.get Main_values.CVal.key with
| Some get_error, Some get_cvalue ->
begin
- let set_error = V.set Numerors_value.error_key in
+ let set_error = V.set Numerors_value.key in
fun t ->
let cvalue = get_cvalue t in
try
@@ -159,5 +162,5 @@ end
let numerors_domain () =
Value_parameters.warning "The numerors domain is experimental.";
- (module Domain: Abstract_domain.Internal with type value = value
- and type location = location)
+ (module Domain: Abstract_domain.Leaf with type value = value
+ and type location = location)
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 8ab4ee60ca7..f491384582b 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -103,7 +103,6 @@ module Internal : Domain_builder.InputDomain
end)
let name = "Bitwise domain"
- let structure = Abstract_domain.Void
let log_category = dkey
let empty _ = Memory.empty_map
diff --git a/src/plugins/value/domains/offsm_domain.mli b/src/plugins/value/domains/offsm_domain.mli
index 4567fc14d3f..8833d4b88cb 100644
--- a/src/plugins/value/domains/offsm_domain.mli
+++ b/src/plugins/value/domains/offsm_domain.mli
@@ -20,6 +20,6 @@
(* *)
(**************************************************************************)
-module D : Abstract_domain.Internal
+module D : Abstract_domain.Leaf
with type value = Offsm_value.offsm_or_top
and type location = Precise_locs.precise_location
diff --git a/src/plugins/value/domains/printer_domain.mli b/src/plugins/value/domains/printer_domain.mli
index 5355cebbd9c..febfc6902d6 100644
--- a/src/plugins/value/domains/printer_domain.mli
+++ b/src/plugins/value/domains/printer_domain.mli
@@ -23,5 +23,5 @@
(** An abstract domain built on top of the Simpler_domains.Simple_Cvalue
interface that just prints the transfer functions called by the engine
during an analysis. *)
-include Abstract_domain.Internal with type value = Cvalue.V.t
- and type location = Precise_locs.precise_location
+include Abstract_domain.Leaf with type value = Cvalue.V.t
+ and type location = Precise_locs.precise_location
diff --git a/src/plugins/value/domains/sign_domain.mli b/src/plugins/value/domains/sign_domain.mli
index fafc9f18c67..b32803feb65 100644
--- a/src/plugins/value/domains/sign_domain.mli
+++ b/src/plugins/value/domains/sign_domain.mli
@@ -22,5 +22,5 @@
(** Abstraction of the sign of integer variables. *)
-include Abstract_domain.Internal with type value = Sign_value.t
- and type location = Precise_locs.precise_location
+include Abstract_domain.Leaf with type value = Sign_value.t
+ and type location = Precise_locs.precise_location
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index f312b589f11..ea175768582 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -188,9 +188,6 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
type value = Value.t
type location = Precise_locs.precise_location
- let key = Structure.Key_Domain.create_key (Info.name ^ " domain")
- let structure : t Abstract_domain.structure = Abstract_domain.Leaf key
-
let log_category = Value_parameters.register_category ("d-" ^ Info.name)
let widen _kf _stmt = widen
diff --git a/src/plugins/value/domains/simple_memory.mli b/src/plugins/value/domains/simple_memory.mli
index e45eef5cb3a..0ea8a003a60 100644
--- a/src/plugins/value/domains/simple_memory.mli
+++ b/src/plugins/value/domains/simple_memory.mli
@@ -106,8 +106,8 @@ module Make_Domain
(Value: Value)
: sig
- include Abstract_domain.Internal with type value = Value.t
- and type location = Precise_locs.precise_location
+ include Abstract_domain.Leaf with type value = Value.t
+ and type location = Precise_locs.precise_location
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 42db4cd7cb5..00220370476 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -472,7 +472,6 @@ module Internal : Domain_builder.InputDomain
end)
let name = "Symbolic locations domain"
- let structure = Abstract_domain.Void
let log_category = dkey
let empty _ = Memory.empty_map
diff --git a/src/plugins/value/domains/symbolic_locs.mli b/src/plugins/value/domains/symbolic_locs.mli
index 06cda3ce5eb..7cebf7b9f4c 100644
--- a/src/plugins/value/domains/symbolic_locs.mli
+++ b/src/plugins/value/domains/symbolic_locs.mli
@@ -23,6 +23,6 @@
(** Domain that store information on non-precise l-values such as
[t[i]] or [*p] when [i] or [p] is not exact. *)
-module D: Abstract_domain.Internal
+module D: Abstract_domain.Leaf
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 68f7b320300..f7d5946d2dd 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -846,8 +846,6 @@ let rec complete_graph (graph:Graph.t) =
) graph Graph.empty
-let key = Structure.Key_Domain.create_key "traces domain"
-
module Internal = struct
type nonrec state = state
type value = Cvalue.V.t
@@ -858,7 +856,6 @@ module Internal = struct
include Abstract_domain.Lattice with type state := state
end)
- let structure : t Abstract_domain.structure = Abstract_domain.Leaf key
let log_category = Value_parameters.register_category "d-traces"
type origin = unit
@@ -1271,8 +1268,7 @@ let output_dot filename state =
close_out out
module D = struct
- include Internal
- module Store = Domain_store.Make(Internal)
+ include Domain_builder.Complete (Internal)
let post_analysis state =
let return_stmt = Kernel_function.find_return (fst (Globals.entry_point ())) in
diff --git a/src/plugins/value/domains/traces_domain.mli b/src/plugins/value/domains/traces_domain.mli
index 7319b2f20bc..a1c57a5359d 100644
--- a/src/plugins/value/domains/traces_domain.mli
+++ b/src/plugins/value/domains/traces_domain.mli
@@ -71,7 +71,7 @@ val current: state -> loops
val globals: state -> Cil_types.varinfo list
val entry_formals: state -> Cil_types.varinfo list
-module D: Abstract_domain.Internal
+module D: Abstract_domain.Leaf
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
and type state = state
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index 4bb14526c7b..729932cbcb7 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -28,8 +28,8 @@ module Static = struct
type state = t
let name = "Unit domain"
- let structure = Abstract_domain.Void
let log_category = log_key
+ let structure = Abstract.Domain.Void
let top = ()
let is_included _ _ = true
diff --git a/src/plugins/value/domains/unit_domain.mli b/src/plugins/value/domains/unit_domain.mli
index 03a18359466..e1ed4495741 100644
--- a/src/plugins/value/domains/unit_domain.mli
+++ b/src/plugins/value/domains/unit_domain.mli
@@ -23,7 +23,7 @@
module Make
(Value: Abstract_value.S)
(Loc: Abstract_location.S)
- : Abstract_domain.Internal with type state = unit
+ : Abstract.Domain.Internal with type state = unit
and type value = Value.t
and type location = Loc.location
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 256fe3fd89b..5360df332a1 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -79,14 +79,14 @@ let legacy_config = {
}
module type Value = sig
- include Abstract_value.External
+ include Abstract.Value.External
val reduce : t -> t
end
module type S = sig
module Val : Value
- module Loc : Abstract_location.External with type value = Val.t
- module Dom : Abstract_domain.External with type value = Val.t
+ module Loc : Abstract.Location.External with type value = Val.t
+ module Dom : Abstract.Domain.External with type value = Val.t
and type location = Loc.location
end
@@ -103,13 +103,28 @@ end
(* -------------------------------------------------------------------------- *)
module type V = sig
- include Abstract_value.External
- val structure : t Abstract_value.structure
+ include Abstract.Value.External
+ val structure : t Abstract.Value.structure
end
-module CVal = struct
+module Internal_CVal = struct
include Main_values.CVal
- include Structure.Open (Structure.Key_Value) (Main_values.CVal)
+ let structure = Abstract.Value.Leaf key
+end
+
+module CVal = struct
+ include Internal_CVal
+ include Structure.Open (Structure.Key_Value) (Internal_CVal)
+end
+
+module Internal_PLoc = struct
+ include Main_locations.PLoc
+ let structure = Abstract.Location.Leaf key
+end
+
+module Internal_Cvalue_Domain = struct
+ include Cvalue_domain.State
+ let structure = Abstract.Domain.Leaf key
end
let has_apron config =
@@ -122,18 +137,20 @@ let has_apron config =
abstractions (if they are enabled). Do not display the intervals in the GUI
in this case. *)
let add_apron_value config value =
- let module Left = ((val value: Abstract_value.Internal)) in
+ let module Left = ((val value: Abstract.Value.Internal)) in
let module V = struct
include Value_product.Make (Left) (Main_values.Interval)
let pretty_typ =
if config.cvalue
then fun fmt typ (left, _right) -> Left.pretty_typ fmt typ left
else pretty_typ
+ let structure =
+ Abstract.Value.(Node (Left.structure, Leaf Main_values.Interval.key))
end in
- (module V: Abstract_value.Internal)
+ (module V: Abstract.Value.Internal)
let open_value_abstraction value =
- let module Value = (val value : Abstract_value.Internal) in
+ let module Value = (val value : Abstract.Value.Internal) in
(module struct
include Value
include Structure.Open (Structure.Key_Value) (Value)
@@ -142,14 +159,19 @@ let open_value_abstraction value =
let build_value config =
let value =
if config.bitwise
- then (module Offsm_value.CvalueOffsm : Abstract_value.Internal)
- else (module Main_values.CVal : Abstract_value.Internal)
+ then (module Offsm_value.CvalueOffsm : Abstract.Value.Internal)
+ else (module Internal_CVal : Abstract.Value.Internal)
in
let value =
if config.signs
then
- let module V = Value_product.Make ((val value)) (Sign_value) in
- (module V: Abstract_value.Internal)
+ let module Value = (val value) in
+ let module V = struct
+ include Value_product.Make (Value) (Sign_value)
+ let structure =
+ Abstract.Value.(Node (Value.structure, Leaf Sign_value.key))
+ end in
+ (module V: Abstract.Value.Internal)
else value
in
let value =
@@ -166,7 +188,7 @@ let build_value config =
(* Builds a module conversion from a generic external value to a key. *)
module Convert
- (Value : Abstract_value.External)
+ (Value : Abstract.Value.External)
(K : sig type v val key : v Abstract_value.key end)
= struct
type extended_value = Value.t
@@ -194,9 +216,9 @@ end
(* Abstractions needed for the analysis: value, location and domain. *)
module type Abstract = sig
module Val : V
- module Loc : Abstract_location.Internal with type value = Val.t
+ module Loc : Abstract.Location.Internal with type value = Val.t
and type location = Precise_locs.precise_location
- module Dom : Abstract_domain.Internal with type value = Val.t
+ module Dom : Abstract.Domain.Internal with type value = Val.t
and type location = Loc.location
end
@@ -205,13 +227,13 @@ let default_root_abstraction config =
then
(module struct
module Val = CVal
- module Loc = Main_locations.PLoc
- module Dom = Cvalue_domain.State
+ module Loc = Internal_PLoc
+ module Dom = Internal_Cvalue_Domain
end : Abstract)
else
(module struct
module Val = CVal
- module Loc = Main_locations.PLoc
+ module Loc = Internal_PLoc
module Dom = Unit_domain.Make (Val) (Loc)
end : Abstract)
@@ -219,20 +241,27 @@ let build_root_abstraction config value =
let module Val = (val value : V) in
let module K = struct
type v = Cvalue.V.t
- let key = Main_values.cvalue_key
+ let key = Main_values.CVal.key
end in
let module Conv = Convert (Val) (K) in
+ let module Loc = struct
+ include Location_lift.Make (Main_locations.PLoc) (Conv)
+ let structure = Abstract.Location.Leaf Internal_PLoc.key
+ end in
if config.cvalue
then
(module struct
module Val = Val
- module Loc = Location_lift.Make (Main_locations.PLoc) (Conv)
- module Dom = Domain_lift.Make (Cvalue_domain.State) (Conv)
+ module Loc = Loc
+ module Dom = struct
+ include Domain_lift.Make (Cvalue_domain.State) (Conv)
+ let structure = Abstract.Domain.Leaf Internal_Cvalue_Domain.key
+ end
end : Abstract)
else
(module struct
module Val = Val
- module Loc = Location_lift.Make (Main_locations.PLoc) (Conv)
+ module Loc = Loc
module Dom = Unit_domain.Make (Val) (Loc)
end : Abstract)
@@ -242,17 +271,22 @@ let build_root_abstraction config value =
(* -------------------------------------------------------------------------- *)
let add_apron_domain abstract apron =
- let module Abstract = (val abstract: Abstract) in
+ let module Acc = (val abstract: Abstract) in
let module K = struct
type v = Main_values.Interval.t
- let key = Main_values.interval_key
+ let key = Main_values.Interval.key
end in
- let module Conv = Convert (Abstract.Val) (K) in
- let module Apron = Domain_lift.Make ((val apron : Apron_domain.S)) (Conv) in
+ let module Conv = Convert (Acc.Val) (K) in
+ let module Apron = (val apron : Apron_domain.S) in
+ let structure = Abstract.Domain.Leaf Apron.key in
+ let module Apron = Domain_lift.Make (Apron) (Conv) in
(module struct
- module Val = Abstract.Val
- module Loc = Abstract.Loc
- module Dom = Domain_product.Make (Abstract.Val) (Abstract.Dom) (Apron)
+ module Val = Acc.Val
+ module Loc = Acc.Loc
+ module Dom = struct
+ include Domain_product.Make (Acc.Val) (Acc.Dom) (Apron)
+ let structure = Abstract.Domain.(Node (Acc.Dom.structure, structure))
+ end
end : Abstract)
let dkey_experimental = Value_parameters.register_category "experimental-ok"
@@ -273,32 +307,37 @@ let add_apron_domain abstractions apron =
module CvalueEquality = Equality_domain.Make (CVal)
-let add_generic_equalities (module Abstract : Abstract) =
- let module EqDom = Equality_domain.Make (Abstract.Val) in
- let module Dom = Domain_product.Make (Abstract.Val) (Abstract.Dom) (EqDom) in
+let add_generic_equalities (module Acc : Abstract) =
+ let module EqDom = Equality_domain.Make (Acc.Val) in
+ let module Dom = struct
+ include Domain_product.Make (Acc.Val) (Acc.Dom) (EqDom)
+ let structure = Abstract.Domain.(Node (Acc.Dom.structure, Leaf EqDom.key))
+ end in
(module struct
- module Val = Abstract.Val
- module Loc = Abstract.Loc
+ module Val = Acc.Val
+ module Loc = Acc.Loc
module Dom = Dom
end : Abstract)
-let add_equalities (type v) (module Abstract : Abstract with type Val.t = v) =
- match Abstract.Val.structure with
+let add_equalities (type v) (module Acc : Abstract with type Val.t = v) =
+ match Acc.Val.structure with
| Structure.Key_Value.Leaf key ->
begin
- match Structure.Key_Value.eq_type key Main_values.cvalue_key with
- | None -> add_generic_equalities (module Abstract)
+ match Structure.Key_Value.eq_type key Main_values.CVal.key with
+ | None -> add_generic_equalities (module Acc)
| Some Structure.Eq ->
- let module Dom =
- Domain_product.Make (Abstract.Val) (Abstract.Dom) (CvalueEquality)
- in
+ let module Dom = struct
+ include Domain_product.Make (Acc.Val) (Acc.Dom) (CvalueEquality)
+ let structure =
+ Abstract.Domain.(Node (Acc.Dom.structure, Leaf CvalueEquality.key))
+ end in
(module struct
- module Val = Abstract.Val
- module Loc = Abstract.Loc
+ module Val = Acc.Val
+ module Loc = Acc.Loc
module Dom = Dom
end : Abstract)
end
- | _ -> add_generic_equalities (module Abstract)
+ | _ -> add_generic_equalities (module Acc)
(* -------------------------------------------------------------------------- *)
@@ -306,17 +345,21 @@ let add_equalities (type v) (module Abstract : Abstract with type Val.t = v) =
(* -------------------------------------------------------------------------- *)
let add_offsm abstract =
- let module Abstract = (val abstract : Abstract) in
+ let module Acc = (val abstract : Abstract) in
let module K = struct
type v = Offsm_value.offsm_or_top
- let key = Offsm_value.offsm_key
+ let key = Offsm_value.Offsm.key
end in
- let module Conv = Convert (Abstract.Val) (K) in
+ let module Conv = Convert (Acc.Val) (K) in
let module Offsm = Domain_lift.Make (Offsm_domain.D) (Conv) in
- let module Dom = Domain_product.Make (Abstract.Val) (Abstract.Dom) (Offsm) in
+ let module Dom = struct
+ include Domain_product.Make (Acc.Val) (Acc.Dom) (Offsm)
+ let structure =
+ Abstract.Domain.(Node (Acc.Dom.structure, Leaf Offsm_domain.D.key))
+ end in
(module struct
- module Val = Abstract.Val
- module Loc = Abstract.Loc
+ module Val = Acc.Val
+ module Loc = Acc.Loc
module Dom = Dom
end : Abstract)
@@ -324,23 +367,27 @@ let add_offsm abstract =
(* Domains on standard locations and values *)
(* -------------------------------------------------------------------------- *)
-module type Standard_abstraction = Abstract_domain.Internal
+module type Standard_abstraction = Abstract_domain.Leaf
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
let add_standard_domain d abstract =
- let module Abstract = (val abstract : Abstract) in
+ let module Acc = (val abstract : Abstract) in
let module K = struct
type v = Cvalue.V.t
- let key = Main_values.cvalue_key
+ let key = Main_values.CVal.key
end in
- let module Conv = Convert (Abstract.Val) (K) in
+ let module Conv = Convert (Acc.Val) (K) in
let module D = (val d: Standard_abstraction) in
let module LD = Domain_lift.Make (D) (Conv) in
- let module Dom = Domain_product.Make (Abstract.Val)(Abstract.Dom)(LD) in
+ let module Dom = struct
+ include Domain_product.Make (Acc.Val)(Acc.Dom)(LD)
+ let structure =
+ Abstract.Domain.(Node (Acc.Dom.structure, Leaf D.key))
+ end in
(module struct
- module Val = Abstract.Val
- module Loc = Abstract.Loc
+ module Val = Acc.Val
+ module Loc = Acc.Loc
module Dom = Dom
end : Abstract)
@@ -381,17 +428,21 @@ let add_inout =
(* -------------------------------------------------------------------------- *)
let add_signs abstract =
- let module Abstract = (val abstract : Abstract) in
+ let module Acc = (val abstract : Abstract) in
let module K = struct
type v = Sign_value.t
- let key = Sign_value.sign_key
+ let key = Sign_value.key
end in
- let module Conv = Convert (Abstract.Val) (K) in
+ let module Conv = Convert (Acc.Val) (K) in
let module Sign = Domain_lift.Make (Sign_domain) (Conv) in
- let module Dom = Domain_product.Make (Abstract.Val) (Abstract.Dom) (Sign) in
+ let module Dom = struct
+ include Domain_product.Make (Acc.Val) (Acc.Dom) (Sign)
+ let structure =
+ Abstract.Domain.(Node (Acc.Dom.structure, Leaf Sign_domain.key))
+ end in
(module struct
- module Val = Abstract.Val
- module Loc = Abstract.Loc
+ module Val = Acc.Val
+ module Loc = Acc.Loc
module Dom = Dom
end : Abstract)
@@ -400,18 +451,22 @@ let add_signs abstract =
(* -------------------------------------------------------------------------- *)
let add_errors abstract =
- let module Abstract = (val abstract : Abstract) in
+ let module Acc = (val abstract : Abstract) in
let module K = struct
type v = Numerors_domain.value
let key = Numerors_domain.value_key
end in
- let module Conv = Convert (Abstract.Val) (K) in
+ let module Conv = Convert (Acc.Val) (K) in
let module Numerors = (val Numerors_domain.numerors_domain ()) in
let module Errors = Domain_lift.Make (Numerors) (Conv) in
- let module Dom = Domain_product.Make (Abstract.Val) (Abstract.Dom) (Errors) in
+ let module Dom = struct
+ include Domain_product.Make (Acc.Val) (Acc.Dom) (Errors)
+ let structure =
+ Abstract.Domain.(Node (Acc.Dom.structure, Leaf Numerors.key))
+ end in
(module struct
- module Val = Abstract.Val
- module Loc = Abstract.Loc
+ module Val = Acc.Val
+ module Loc = Acc.Loc
module Dom = Dom
end : Abstract)
@@ -439,7 +494,7 @@ let build_abstractions config =
let abstractions =
match V.structure with
| Structure.Key_Value.Leaf key
- when Structure.Key_Value.equal key Main_values.cvalue_key ->
+ when Structure.Key_Value.equal key Main_values.CVal.key ->
default_root_abstraction config
| _ -> build_root_abstraction config value
in
@@ -519,7 +574,7 @@ let build_abstractions config =
(* Add the reduce function to the value module. *)
-module Reduce (Value : Abstract_value.External) = struct
+module Reduce (Value : Abstract.Value.External) = struct
include Value
@@ -528,11 +583,11 @@ module Reduce (Value : Abstract_value.External) = struct
other. If the Cvalue is not a scalar do nothing, because we do not
currently use Apron for pointer offsets. *)
let reduce_apron_itv =
- match Value.get Main_values.interval_key, Value.get Main_values.cvalue_key with
+ match Value.get Main_values.Interval.key, Value.get Main_values.CVal.key with
| Some get_interval, Some get_cvalue ->
begin
- let set_cvalue = Value.set Main_values.cvalue_key in
- let set_interval = Value.set Main_values.interval_key in
+ let set_cvalue = Value.set Main_values.CVal.key in
+ let set_interval = Value.set Main_values.Interval.key in
fun t ->
match get_interval t with
| None -> begin
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index 996f0aaa039..15837823e65 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -53,7 +53,7 @@ val configure : unit -> config
module type Value = sig
- include Abstract_value.External
+ include Abstract.Value.External
val reduce : t -> t
end
@@ -61,8 +61,8 @@ end
abstractions.*)
module type S = sig
module Val : Value
- module Loc : Abstract_location.External with type value = Val.t
- module Dom : Abstract_domain.External with type value = Val.t
+ module Loc : Abstract.Location.External with type value = Val.t
+ module Dom : Abstract.Domain.External with type value = Val.t
and type location = Loc.location
end
@@ -78,7 +78,7 @@ module type Eva = sig
end
(** Type of abstractions that use the builtin types for values and locations *)
-module type Standard_abstraction = Abstract_domain.Internal
+module type Standard_abstraction = Abstract_domain.Leaf
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index d265352833e..4440415631b 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -149,17 +149,17 @@ module Make (Abstract: Abstractions.Eva) = struct
let initial_state = Init.initial_state
let get_cvalue =
- match Abstract.Dom.get Cvalue_domain.key with
+ match Abstract.Dom.get Cvalue_domain.State.key with
| None -> fun _ -> Cvalue.Model.top
- | Some get -> fun state -> get state
+ | Some get -> fun state -> Cvalue_domain.project (get state)
let get_cval =
- match Abstract.Val.get Main_values.cvalue_key with
+ match Abstract.Val.get Main_values.CVal.key with
| None -> fun _ -> assert false
| Some get -> fun value -> get value
let get_ploc =
- match Abstract.Loc.get Main_locations.ploc_key with
+ match Abstract.Loc.get Main_locations.PLoc.key with
| None -> fun _ -> assert false
| Some get -> fun location -> get location
@@ -312,17 +312,16 @@ module Make (Abstract: Abstractions.Eva) = struct
let cvalue_states, cacheable =
Builtins.apply_builtin builtin cvalue_call cvalue_state
in
- let insert (cvalue_state, clobbered_set) =
- Abstract.Dom.set Locals_scoping.key clobbered_set
- (Abstract.Dom.set Cvalue_domain.key cvalue_state final_state)
+ let insert cvalue_state =
+ Abstract.Dom.set Cvalue_domain.State.key cvalue_state final_state
in
let states = Bottom.bot_of_list (List.map insert cvalue_states) in
Transfer.{states; cacheable; builtin=true}
let compute_call =
- if Abstract.Dom.mem Cvalue_domain.key
- && Abstract.Val.mem Main_values.cvalue_key
- && Abstract.Loc.mem Main_locations.ploc_key
+ if Abstract.Dom.mem Cvalue_domain.State.key
+ && Abstract.Val.mem Main_values.CVal.key
+ && Abstract.Loc.mem Main_locations.PLoc.key
then compute_call_or_builtin
else compute_and_cache_call
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index cc4018b105a..b56d0062033 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -263,7 +263,7 @@ let indeterminate_copy lval result alarms =
module type Value = sig
- include Abstract_value.External
+ include Abstract.Value.External
val reduce : t -> t
end
diff --git a/src/plugins/value/engine/evaluation.mli b/src/plugins/value/engine/evaluation.mli
index ad8886669f2..f7febc17e42 100644
--- a/src/plugins/value/engine/evaluation.mli
+++ b/src/plugins/value/engine/evaluation.mli
@@ -104,7 +104,7 @@ module type S = sig
end
module type Value = sig
- include Abstract_value.External
+ include Abstract.Value.External
(** Inter-reduction of values. Useful when the value module is a reduced
product of several abstraction.
diff --git a/src/plugins/value/engine/initialization.ml b/src/plugins/value/engine/initialization.ml
index 317446467c2..6f15c07d5d6 100644
--- a/src/plugins/value/engine/initialization.ml
+++ b/src/plugins/value/engine/initialization.ml
@@ -80,7 +80,7 @@ let (>>>) t f = match t with
let counter = ref 0
module Make
- (Domain: Abstract_domain.External)
+ (Domain: Abstract.Domain.External)
(Eva: Evaluation.S with type state = Domain.state
and type loc = Domain.location)
(Transfer: Transfer_stmt.S with type state = Domain.t)
@@ -270,7 +270,7 @@ module Make
(* Use the values supplied in [actuals] for the formals of [kf], and
bind them in [state] *)
let add_supplied_main_formals kf actuals state =
- match Domain.get Cvalue_domain.key with
+ match Domain.get Cvalue_domain.State.key with
| None ->
Value_parameters.abort "Function Db.Value.fun_set_args cannot be used \
without the Cvalue domain"
@@ -278,7 +278,7 @@ module Make
let formals = Kernel_function.get_formals kf in
if (List.length formals) <> List.length actuals then
raise Db.Value.Incorrect_number_of_arguments;
- let cvalue_state = get_cvalue state in
+ let cvalue_state = Cvalue_domain.project (get_cvalue state) in
let add_actual state actual formal =
let actual = Eval_op.offsetmap_of_v ~typ:formal.vtype actual in
Cvalue.Model.add_base (Base.of_varinfo formal) actual state
@@ -286,8 +286,8 @@ module Make
let cvalue_state =
List.fold_left2 add_actual cvalue_state actuals formals
in
- let set_domain = Domain.set Cvalue_domain.key in
- set_domain cvalue_state state
+ let set_domain = Domain.set Cvalue_domain.State.key in
+ set_domain (Cvalue_domain.inject cvalue_state) state
let add_main_formals kf state =
match Db.Value.fun_get_args () with
@@ -354,7 +354,9 @@ module Make
let supplied_state () =
let cvalue_state = Db.Value.globals_state () in
if Cvalue.Model.is_reachable cvalue_state
- then `Value (Domain.set Cvalue_domain.key cvalue_state Domain.top)
+ then
+ let cvalue_state = Cvalue_domain.inject cvalue_state in
+ `Value (Domain.set Cvalue_domain.State.key cvalue_state Domain.top)
else `Bottom
let initial_state ~lib_entry =
diff --git a/src/plugins/value/engine/initialization.mli b/src/plugins/value/engine/initialization.mli
index d3bf03c164d..f87a4799a8d 100644
--- a/src/plugins/value/engine/initialization.mli
+++ b/src/plugins/value/engine/initialization.mli
@@ -44,7 +44,7 @@ module type S = sig
end
module Make
- (Domain: Abstract_domain.External)
+ (Domain: Abstract.Domain.External)
(Eva: Evaluation.S with type state = Domain.state
and type loc = Domain.location)
(Transfer: Transfer_stmt.S with type state = Domain.t)
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 541d61dd21f..0e83fb39280 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -433,10 +433,10 @@ module Make_Dataflow
edge_info.fireable <- true;
flow
- let get_cvalue = Domain.get Cvalue_domain.key
+ let get_cvalue = Domain.get Cvalue_domain.State.key
let gather_cvalues states =
match get_cvalue with
- | Some get -> List.map get states
+ | Some get -> List.map (fun s -> Cvalue_domain.project (get s)) states
| None -> []
let call_statement_callbacks (stmt : stmt) (f : flow) : unit =
diff --git a/src/plugins/value/engine/partition.ml b/src/plugins/value/engine/partition.ml
index 68686f72d14..644e3bf20b5 100644
--- a/src/plugins/value/engine/partition.ml
+++ b/src/plugins/value/engine/partition.ml
@@ -245,7 +245,7 @@ struct
all states"
in
(* Get the cvalue *)
- let cvalue = match Abstract.Val.get Main_values.cvalue_key with
+ let cvalue = match Abstract.Val.get Main_values.CVal.key with
| Some get_cvalue -> get_cvalue value
| None -> fail ~exp "partitioning is disabled when the CValue domain is \
not active"
@@ -325,7 +325,7 @@ struct
(* --- Applying partitioning actions onto flows --------------------------- *)
- let stamp_by_value = match Abstract.Val.get Main_values.cvalue_key with
+ let stamp_by_value = match Abstract.Val.get Main_values.CVal.key with
| None -> fun _ _ _ -> None
| Some get -> fun expr expected_values state ->
let typ = Cil.typeOf expr in
diff --git a/src/plugins/value/engine/partitioning_index.ml b/src/plugins/value/engine/partitioning_index.ml
index 08a2f449cf0..af420297323 100644
--- a/src/plugins/value/engine/partitioning_index.ml
+++ b/src/plugins/value/engine/partitioning_index.ml
@@ -23,7 +23,8 @@
module type Domain = sig
include Abstract_domain.Lattice
include Datatype.S_with_collections with type t = state
- include Abstract_domain.Interface with type t := state
+ include Abstract.Interface with type t := state
+ and type 'a key := 'a Abstract_domain.key
end
(** Partition of the abstract states, computed for each node by the
@@ -45,12 +46,12 @@ module Make
(* Optimizations relying on specific features of the cvalue domain. *)
- let distinct_subpart = match Domain.get Cvalue_domain.key with
+ let distinct_subpart = match Domain.get Cvalue_domain.State.key with
| None -> fun _ _ -> None
| Some get ->
fun s1 s2 -> Cvalue_domain.distinct_subpart (get s1) (get s2)
- let find_subpart = match Domain.get Cvalue_domain.key with
+ let find_subpart = match Domain.get Cvalue_domain.State.key with
| None -> fun _ _ -> None
| Some get ->
fun state prefix -> Cvalue_domain.find_subpart (get state) prefix
diff --git a/src/plugins/value/engine/partitioning_index.mli b/src/plugins/value/engine/partitioning_index.mli
index b4488a2eef7..9a72e4b44bb 100644
--- a/src/plugins/value/engine/partitioning_index.mli
+++ b/src/plugins/value/engine/partitioning_index.mli
@@ -33,7 +33,8 @@
module type Domain = sig
include Abstract_domain.Lattice
include Datatype.S_with_collections with type t = state
- include Abstract_domain.Interface with type t := state
+ include Abstract.Interface with type t := state
+ and type 'a key := 'a Abstract_domain.key
end
module Make (Domain: Domain) : sig
diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index ae1efe494c8..3d0e928ef9f 100644
--- a/src/plugins/value/engine/subdivided_evaluation.ml
+++ b/src/plugins/value/engine/subdivided_evaluation.ml
@@ -368,7 +368,7 @@ module type Forward_Evaluation = sig
end
module Make
- (Value : Abstract_value.External)
+ (Value : Abstract.Value.External)
(Loc : Abstract_location.S with type value = Value.t)
(Valuation: Valuation with type value = Value.t
and type loc = Loc.location)
@@ -379,15 +379,15 @@ module Make
(* Values are converted to {!Cvalue.V.t}, because those are
currently the only values on which we can split. *)
- let get_cval = match Value.get Main_values.cvalue_key with
+ let get_cval = match Value.get Main_values.CVal.key with
| Some get -> get
| None -> fun _ -> Cvalue.V.top
let set_cval =
- let set = Value.set Main_values.cvalue_key in
+ let set = Value.set Main_values.CVal.key in
fun cval v -> set cval v
- let activated = Value.mem Main_values.cvalue_key
+ let activated = Value.mem Main_values.CVal.key
module Clear = Clear_Valuation (Valuation)
diff --git a/src/plugins/value/engine/subdivided_evaluation.mli b/src/plugins/value/engine/subdivided_evaluation.mli
index 745624c4575..71d582bb70d 100644
--- a/src/plugins/value/engine/subdivided_evaluation.mli
+++ b/src/plugins/value/engine/subdivided_evaluation.mli
@@ -36,7 +36,7 @@ module type Forward_Evaluation = sig
end
module Make
- (Value : Abstract_value.External)
+ (Value : Abstract.Value.External)
(Loc: Abstract_location.S with type value = Value.t)
(Valuation: Eval.Valuation with type value = Value.t
and type loc = Loc.location)
diff --git a/src/plugins/value/engine/transfer_specification.ml b/src/plugins/value/engine/transfer_specification.ml
index d5438b227de..69171aaeec7 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -227,14 +227,14 @@ module Make
(* Extraction of the precise location and of the cvalue domain:
needed to evaluate the location of an assigns clause. *)
- let get_ploc = match Location.get Main_locations.ploc_key with
+ let get_ploc = match Location.get Main_locations.PLoc.key with
| None -> fun _ -> Main_locations.PLoc.top
| Some get -> get
- let set_ploc = Location.set Main_locations.ploc_key
+ let set_ploc = Location.set Main_locations.PLoc.key
let set_location loc = set_ploc (Main_locations.PLoc.make loc)
- let get_cvalue_state = match Domain.get Cvalue_domain.key with
+ let get_cvalue_state = match Domain.get Cvalue_domain.State.key with
| None -> fun _ -> Cvalue.Model.top
- | Some get -> get
+ | Some get -> fun s -> Cvalue_domain.project (get s)
let make_env state = Eval_terms.env_assigns (get_cvalue_state state)
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index e7be6f8f582..c0f99adcbda 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -318,7 +318,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* ------------------- Retro propagation on formals ----------------------- *)
- let get_precise_location = Location.get Main_locations.ploc_key
+ let get_precise_location = Location.get Main_locations.PLoc.key
(* [is_safe_argument valuation expr] is true iff the expression [expr] could
not have been written during the last call.
@@ -559,9 +559,9 @@ module Make (Abstract: Abstractions.Eva) = struct
(* ----------------- show_each and dump_each directives ------------------- *)
- let extract_cvalue = match Domain.get Cvalue_domain.key with
+ let extract_cvalue = match Domain.get Cvalue_domain.State.key with
| None -> fun _ -> Cvalue.Model.top
- | Some get -> get
+ | Some get -> fun s -> Cvalue_domain.project (get s)
(* The product of domains formats the printing of each leaf domains, by
checking their log_category and adding their name before the dump. If the
@@ -609,7 +609,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* For non scalar expressions, prints the offsetmap of the cvalue domain. *)
let show_offsm =
- match Domain.get Cvalue_domain.key, Location.get Main_locations.ploc_key with
+ match Domain.get Cvalue_domain.State.key, Location.get Main_locations.PLoc.key with
| None, _ | _, None ->
fun fmt _ _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
| Some get_cvalue, Some get_ploc ->
@@ -622,7 +622,7 @@ module Make (Abstract: Abstractions.Eva) = struct
fst (Eval.lvaluate ~for_writing:false state lval)
>>- fun (_, loc, _) ->
let ploc = get_ploc loc
- and cvalue_state = get_cvalue state in
+ and cvalue_state = Cvalue_domain.project (get_cvalue state) in
Eval_op.offsetmap_of_loc ploc cvalue_state
in
let typ = Cil.typeOf expr in
@@ -634,7 +634,7 @@ module Make (Abstract: Abstractions.Eva) = struct
(* For scalar expressions, prints the cvalue component of their values. *)
let show_value =
- match Value.get Main_values.cvalue_key with
+ match Value.get Main_values.CVal.key with
| None -> fun fmt _ _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
| Some get_cval ->
fun fmt expr state ->
diff --git a/src/plugins/value/gui_files/gui_eval.ml b/src/plugins/value/gui_files/gui_eval.ml
index 108079350d9..2c64ede8741 100644
--- a/src/plugins/value/gui_files/gui_eval.ml
+++ b/src/plugins/value/gui_files/gui_eval.ml
@@ -144,12 +144,12 @@ module Make (X: Analysis.S) = struct
module Analysis = X
let get_cvalue_state =
- match X.Dom.get Cvalue_domain.key with
+ match X.Dom.get Cvalue_domain.State.key with
| None -> fun _ -> Cvalue.Model.top
- | Some get -> fun state -> get state
+ | Some get -> fun state -> Cvalue_domain.project (get state)
let get_precise_loc =
- match X.Loc.get Main_locations.ploc_key with
+ match X.Loc.get Main_locations.PLoc.key with
| None -> fun _ -> Precise_locs.loc_top
| Some get -> fun loc -> get loc
diff --git a/src/plugins/value/gui_files/gui_types.ml b/src/plugins/value/gui_files/gui_types.ml
index 683fa039860..f4fad0001bc 100644
--- a/src/plugins/value/gui_files/gui_types.ml
+++ b/src/plugins/value/gui_files/gui_types.ml
@@ -167,8 +167,8 @@ module Make (V: Abstractions.Value) = struct
| GA_After r1, GA_After r2 -> equal_gui_res r1 r2
| (GA_After _ | GA_NA | GA_Unchanged | GA_Bottom), _ -> false
- let get_cvalue = V.get Main_values.cvalue_key
- let from_cvalue v = V.set Main_values.cvalue_key v V.top
+ let get_cvalue = V.get Main_values.CVal.key
+ let from_cvalue v = V.set Main_values.CVal.key v V.top
let var_of_base base acc =
try
diff --git a/src/plugins/value/register.ml b/src/plugins/value/register.ml
index b7198f21219..d3103749d06 100644
--- a/src/plugins/value/register.ml
+++ b/src/plugins/value/register.ml
@@ -169,9 +169,14 @@ let () =
open Eval
-module Val = struct
+module CVal = struct
include Main_values.CVal
- include Structure.Open (Structure.Key_Value) (Main_values.CVal)
+ let structure = Abstract.Value.Leaf key
+end
+
+module Val = struct
+ include CVal
+ include Structure.Open (Structure.Key_Value) (CVal)
let reduce t = t
end
diff --git a/src/plugins/value/utils/abstract.ml b/src/plugins/value/utils/abstract.ml
new file mode 100644
index 00000000000..54cf436f968
--- /dev/null
+++ b/src/plugins/value/utils/abstract.ml
@@ -0,0 +1,75 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** External interface of an abstraction, built by {!Structure.Open}. *)
+module type Interface = sig
+ type t
+ type 'a key
+ val mem : 'a key -> bool
+ val get : 'a key -> (t -> 'a) option
+ val set : 'a key -> 'a -> t -> t
+end
+
+module Value = struct
+ include Structure.Key_Value
+
+ module type Internal = sig
+ include Abstract_value.S
+ val structure: t structure
+ end
+
+ module type External = sig
+ include Internal
+ include Structure.External with type t := t
+ and type 'a key := 'a key
+ end
+end
+
+module Location = struct
+ include Structure.Key_Location
+
+ module type Internal = sig
+ include Abstract_location.S
+ val structure: location structure
+ end
+
+ module type External = sig
+ include Internal
+ include Structure.External with type t := location
+ and type 'a key := 'a key
+ end
+end
+
+module Domain = struct
+ include Structure.Key_Domain
+
+ module type Internal = sig
+ include Abstract_domain.Internal
+ val structure: t structure
+ end
+
+ module type External = sig
+ include Internal
+ include Structure.External with type t := t
+ and type 'a key := 'a key
+ end
+end
diff --git a/src/plugins/value/utils/abstract.mli b/src/plugins/value/utils/abstract.mli
new file mode 100644
index 00000000000..ad5037857fb
--- /dev/null
+++ b/src/plugins/value/utils/abstract.mli
@@ -0,0 +1,113 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2019 *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+(** Internal and External signature of abstractions used in the Eva engine. *)
+
+(** Internal modules contains a [structure] value that describes the internal
+ structure of the abstraction. This structure is used to automatically
+ generate efficient accessors from a generic compound abstraction to specific
+ leaf abstractions. *)
+
+(** External modules export direct accessors to their leaf components.
+ When a generic abstraction is a product of several specific abstractions,
+ they allow interacting with each leaf abstraction identified by a key.
+ Note that their behavior is undefined if an abstraction contains
+ several times the same leaf module. *)
+
+(** External interface of an abstraction, built by {!Structure.Open}. *)
+module type Interface = sig
+ type t
+ type 'a key
+
+ (** Tests whether a key belongs to the module. *)
+ val mem : 'a key -> bool
+
+ (** For a key of type [k key]:
+ - if the values of type [t] contain a subpart of type [k] from a module
+ identified by the key, then [get key] returns an accessor for it.
+ - otherwise, [get key] returns None. *)
+ val get : 'a key -> (t -> 'a) option
+
+ (** For a key of type [k key]:
+ - if the values of type [t] contain a subpart of type [k] from a module
+ identified by the key, then [set key v t] returns the value [t] in which
+ this subpart has been replaced by [v].
+ - otherwise, [set key _] is the identity function. *)
+ val set : 'a key -> 'a -> t -> t
+end
+
+(** Key and structure for abstract values.
+ See {structure.mli} for more details. *)
+module Value : sig
+ include Structure.Shape
+ with type 'a key = 'a Structure.Key_Value.key
+ and type 'a structure = 'a Structure.Key_Value.structure
+
+ module type Internal = sig
+ include Abstract_value.S
+ val structure: t structure
+ end
+
+ module type External = sig
+ include Internal
+ include Interface with type t := t
+ and type 'a key := 'a key
+ end
+end
+
+(** Key and structure for abstract locations.
+ See {structure.mli} for more details. *)
+module Location : sig
+ include Structure.Shape
+ with type 'a key = 'a Structure.Key_Location.key
+ and type 'a structure = 'a Structure.Key_Location.structure
+
+ module type Internal = sig
+ include Abstract_location.S
+ val structure: location structure
+ end
+
+ module type External = sig
+ include Internal
+ include Interface with type t := location
+ and type 'a key := 'a key
+ end
+end
+
+(** Key and structure for abstract domains.
+ See {structure.mli} for more details. *)
+module Domain : sig
+ include Structure.Shape
+ with type 'a key = 'a Structure.Key_Domain.key
+ and type 'a structure = 'a Structure.Key_Domain.structure
+
+ module type Internal = sig
+ include Abstract_domain.Internal
+ val structure: t structure
+ end
+
+ module type External = sig
+ include Internal
+ include Interface with type t := t
+ and type 'a key := 'a key
+ end
+end
diff --git a/src/plugins/value/values/abstract_location.mli b/src/plugins/value/values/abstract_location.mli
index 41990872759..6242ecc18d1 100644
--- a/src/plugins/value/values/abstract_location.mli
+++ b/src/plugins/value/values/abstract_location.mli
@@ -119,21 +119,14 @@ module type S = sig
typ -> index:value -> remaining:offset -> offset -> (value * offset) or_bottom
end
-(** Key and structure for locations. See {structure.mli},
- and {domain.mli} where the mechanism is explained in detail.*)
+type 'loc key = 'loc Structure.Key_Location.key
-type 'a key = 'a Structure.Key_Location.key
-type 'a structure = 'a Structure.Key_Location.structure
-
-module type Internal = sig
+(** Signature for a leaf module of abstract locations. *)
+module type Leaf = sig
include S
- val structure : location structure
-end
-module type External = sig
- include S
- include Structure.External with type t := location
- and type 'a key := 'a key
+ (** The key identifies the module and the type [t] of abstract locations. *)
+ val key: location key
end
(*
diff --git a/src/plugins/value/values/abstract_value.mli b/src/plugins/value/values/abstract_value.mli
index 25fab072de6..c6efd632718 100644
--- a/src/plugins/value/values/abstract_value.mli
+++ b/src/plugins/value/values/abstract_value.mli
@@ -181,21 +181,14 @@ module type S = sig
end
-(** Key and structure for values. See {structure.mli},
- and {domain.mli} where the mechanism is explained in detail.*)
+type 'v key = 'v Structure.Key_Value.key
-type 'a key = 'a Structure.Key_Value.key
-type 'a structure = 'a Structure.Key_Value.structure
-
-module type Internal = sig
+(** Signature for a leaf module of abstract values. *)
+module type Leaf = sig
include S
- val structure : t structure
-end
-module type External = sig
- include S
- include Structure.External with type t := t
- and type 'a key := 'a key
+ (** The key identifies the module and the type [t] of abstract values. *)
+ val key: t key
end
diff --git a/src/plugins/value/values/location_lift.ml b/src/plugins/value/values/location_lift.ml
index ce5ae27c864..4ae36f3622c 100644
--- a/src/plugins/value/values/location_lift.ml
+++ b/src/plugins/value/values/location_lift.ml
@@ -32,12 +32,12 @@ module type Conversion = sig
end
module Make
- (Loc: Abstract_location.Internal)
+ (Loc: Abstract_location.S)
(Convert : Conversion with type internal_value := Loc.value)
= struct
(* Import most of [Loc] *)
- include (Loc: Abstract_location.Internal
+ include (Loc: Abstract_location.S
with type value := Loc.value (* we are converting this type *)
and type location = Loc.location
and type offset = Loc.offset)
diff --git a/src/plugins/value/values/location_lift.mli b/src/plugins/value/values/location_lift.mli
index 1eb2d98d38c..602fbcee455 100644
--- a/src/plugins/value/values/location_lift.mli
+++ b/src/plugins/value/values/location_lift.mli
@@ -30,11 +30,11 @@ module type Conversion = sig
end
module Make
- (Loc: Abstract_location.Internal)
+ (Loc: Abstract_location.S)
(Convert : Conversion with type internal_value := Loc.value)
- : Abstract_location.Internal with type location = Loc.location
- and type offset = Loc.offset
- and type value = Convert.extended_value
+ : Abstract_location.S with type location = Loc.location
+ and type offset = Loc.offset
+ and type value = Convert.extended_value
(*
diff --git a/src/plugins/value/values/main_locations.ml b/src/plugins/value/values/main_locations.ml
index f98119eab16..8722ef35172 100644
--- a/src/plugins/value/values/main_locations.ml
+++ b/src/plugins/value/values/main_locations.ml
@@ -22,8 +22,6 @@
open Cil_types
-let ploc_key = Structure.Key_Location.create_key "precise_locs"
-
module PLoc = struct
type value = Cvalue.V.t
@@ -32,7 +30,7 @@ module PLoc = struct
| Precise of Precise_locs.precise_offset
| Imprecise of Cvalue.V.t (* when the offset contains addresses *)
- let structure = Structure.Key_Location.Leaf ploc_key
+ let key = Structure.Key_Location.create_key "precise_locs"
let equal_loc = Precise_locs.equal_loc
let equal_offset o1 o2 = match o1, o2 with
diff --git a/src/plugins/value/values/main_locations.mli b/src/plugins/value/values/main_locations.mli
index 28d11c16b76..7701838d407 100644
--- a/src/plugins/value/values/main_locations.mli
+++ b/src/plugins/value/values/main_locations.mli
@@ -25,7 +25,7 @@
(** Abstract locations built over Precise_locs. *)
module PLoc : sig
- include Abstract_location.Internal
+ include Abstract_location.Leaf
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
@@ -33,10 +33,6 @@ module PLoc : sig
end
-(** Key for precise locs. *)
-val ploc_key : PLoc.location Abstract_location.key
-
-
(*
Local Variables:
compile-command: "make -C ../../../.."
diff --git a/src/plugins/value/values/main_values.ml b/src/plugins/value/values/main_values.ml
index f5bec06d977..83b93bbfb63 100644
--- a/src/plugins/value/values/main_values.ml
+++ b/src/plugins/value/values/main_values.ml
@@ -22,12 +22,10 @@
open Cil_types
-let cvalue_key = Structure.Key_Value.create_key "cvalue"
-
module CVal = struct
include Cvalue.V
- let structure = Structure.Key_Value.Leaf cvalue_key
+ let key = Structure.Key_Value.create_key "cvalue"
let zero = Cvalue.V.singleton_zero
let one = Cvalue.V.singleton_one
@@ -135,12 +133,10 @@ module CVal = struct
with Abstract_interp.Error_Top -> `Top, true
end
-let interval_key = Structure.Key_Value.create_key "interval"
-
module Interval = struct
include Datatype.Option (Ival)
- let structure = Structure.Key_Value.Leaf interval_key
+ let key = Structure.Key_Value.create_key "interval"
let pretty_typ _ = pretty
diff --git a/src/plugins/value/values/main_values.mli b/src/plugins/value/values/main_values.mli
index fd148fcfcc5..4923f3182ed 100644
--- a/src/plugins/value/values/main_values.mli
+++ b/src/plugins/value/values/main_values.mli
@@ -23,17 +23,11 @@
(** Main numeric values of Eva. *)
(** Abstract values built over Cvalue.V *)
-module CVal : Abstract_value.Internal with type t = Cvalue.V.t
-
-(** Key for cvalues. *)
-val cvalue_key : CVal.t Abstract_value.key
+module CVal : Abstract_value.Leaf with type t = Cvalue.V.t
(** Dummy interval: no forward nor backward propagations.
[None] is top. *)
-module Interval : Abstract_value.Internal with type t = Ival.t option
-
-(** Key for intervals. *)
-val interval_key : Interval.t Abstract_value.key
+module Interval : Abstract_value.Leaf with type t = Ival.t option
(*
Local Variables:
diff --git a/src/plugins/value/values/numerors/numerors_value.ml b/src/plugins/value/values/numerors/numerors_value.ml
index 8fa47dc923f..6ef7042aa69 100644
--- a/src/plugins/value/values/numerors/numerors_value.ml
+++ b/src/plugins/value/values/numerors/numerors_value.ml
@@ -116,8 +116,7 @@ end
include Datatype.Make(T)
let pretty_debug = pretty
let pretty_typ _ = pretty
-let error_key = Structure.Key_Value.create_key "numerors_values"
-let structure = Structure.Key_Value.Leaf error_key
+let key = Structure.Key_Value.create_key "numerors_values"
(*-----------------------------------------------------------------------------
diff --git a/src/plugins/value/values/numerors/numerors_value.mli b/src/plugins/value/values/numerors/numerors_value.mli
index 44da21eca97..3c87147b3e3 100644
--- a/src/plugins/value/values/numerors/numerors_value.mli
+++ b/src/plugins/value/values/numerors/numerors_value.mli
@@ -20,15 +20,13 @@
(* *)
(**************************************************************************)
-include Abstract_value.Internal
+include Abstract_value.Leaf
val pretty_debug : t Pretty_utils.formatter
(** Reduction of an error value according to a floating-point interval. *)
val reduce: Fval.t -> t -> t Eval.or_bottom
-val error_key : t Structure.Key_Value.key
-
val set_absolute_to_top : t -> t
val set_relative_to_top : t -> t
diff --git a/src/plugins/value/values/offsm_value.ml b/src/plugins/value/values/offsm_value.ml
index a447493695d..2a6bab76fb2 100644
--- a/src/plugins/value/values/offsm_value.ml
+++ b/src/plugins/value/values/offsm_value.ml
@@ -381,12 +381,10 @@ module Datatype_Offsm_or_top = Datatype.Make_with_collections(struct
end)
-let offsm_key = Structure.Key_Value.create_key "offsetmap_value"
-
-module Offsm : Abstract_value.Internal with type t = offsm_or_top = struct
+module Offsm : Abstract_value.Leaf with type t = offsm_or_top = struct
include Datatype_Offsm_or_top
- let structure = Structure.Key_Value.Leaf offsm_key
+ let key = Structure.Key_Value.create_key "offsetmap_value"
let pretty_typ typ fmt = function
| Top as o -> pretty fmt o
@@ -480,10 +478,13 @@ module Offsm : Abstract_value.Internal with type t = offsm_or_top = struct
end
-module CvalueOffsm : Abstract_value.Internal with type t = V.t * offsm_or_top
+module CvalueOffsm : Abstract.Value.Internal with type t = V.t * offsm_or_top
= struct
include Value_product.Make (Main_values.CVal) (Offsm)
+ let structure =
+ Abstract.Value.(Node (Leaf Main_values.CVal.key, Leaf Offsm.key))
+
let size typ = Integer.of_int (Cil.bitsSizeOf typ)
(* Extract an offsetmap from a pair, by converting the value when needed. *)
diff --git a/src/plugins/value/values/offsm_value.mli b/src/plugins/value/values/offsm_value.mli
index 088bf7f0843..6465583c14e 100644
--- a/src/plugins/value/values/offsm_value.mli
+++ b/src/plugins/value/values/offsm_value.mli
@@ -22,13 +22,10 @@
type offsm_or_top = O of Cvalue.V_Offsetmap.t | Top
-val offsm_key : offsm_or_top Structure.Key_Value.key
-
val cast :
old_size: Integer.t -> new_size: Integer.t -> signed: bool ->
Cvalue.V_Offsetmap.t -> Cvalue.V_Offsetmap.t
+module Offsm : Abstract_value.Leaf with type t = offsm_or_top
-module Offsm : Abstract_value.Internal with type t = offsm_or_top
-
-module CvalueOffsm : Abstract_value.Internal with type t = Cvalue.V.t * offsm_or_top
+module CvalueOffsm : Abstract.Value.Internal with type t = Cvalue.V.t * offsm_or_top
diff --git a/src/plugins/value/values/sign_value.ml b/src/plugins/value/values/sign_value.ml
index 211ce3cd5b2..66ebbb989c5 100644
--- a/src/plugins/value/values/sign_value.ml
+++ b/src/plugins/value/values/sign_value.ml
@@ -271,5 +271,4 @@ let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ = `Value None
(** {2 Misc} *)
(* Eva boilerplate, used to retrieve the domain. *)
-let sign_key = Structure.Key_Value.create_key "sign_values"
-let structure = Structure.Key_Value.Leaf sign_key
+let key = Structure.Key_Value.create_key "sign_values"
diff --git a/src/plugins/value/values/sign_value.mli b/src/plugins/value/values/sign_value.mli
index 9a71c60d69c..44b761fb982 100644
--- a/src/plugins/value/values/sign_value.mli
+++ b/src/plugins/value/values/sign_value.mli
@@ -22,8 +22,6 @@
(** Sign domain: abstraction of integer numerical values by their signs. *)
-include Abstract_value.Internal
+include Abstract_value.Leaf
val pretty_debug: t Pretty_utils.formatter
-
-val sign_key : t Structure.Key_Value.key
diff --git a/src/plugins/value/values/value_product.ml b/src/plugins/value/values/value_product.ml
index 131d47bfa68..5a088c52838 100644
--- a/src/plugins/value/values/value_product.ml
+++ b/src/plugins/value/values/value_product.ml
@@ -23,14 +23,12 @@
open Eval
module Make
- (Left: Abstract_value.Internal)
- (Right: Abstract_value.Internal)
+ (Left: Abstract_value.S)
+ (Right: Abstract_value.S)
= struct
include Datatype.Pair (Left) (Right)
- let structure = Structure.Key_Value.Node (Left.structure, Right.structure)
-
let pretty_typ typ =
Pretty_utils.pp_pair ~pre:"@[" ~sep:",@ " ~suf:"@]"
(Left.pretty_typ typ) (Right.pretty_typ typ)
diff --git a/src/plugins/value/values/value_product.mli b/src/plugins/value/values/value_product.mli
index f6369ee2efd..c24505d85e3 100644
--- a/src/plugins/value/values/value_product.mli
+++ b/src/plugins/value/values/value_product.mli
@@ -23,9 +23,9 @@
(** Cartesian product of two value abstractions. *)
module Make
- (Left: Abstract_value.Internal)
- (Right: Abstract_value.Internal)
- : Abstract_value.Internal with type t = Left.t * Right.t
+ (Left: Abstract_value.S)
+ (Right: Abstract_value.S)
+ : Abstract_value.S with type t = Left.t * Right.t
(*
--
GitLab