diff --git a/Makefile b/Makefile
index ce5d740b6d4f2ffd7428765694e2e42949dd6b68..334437fc823b2fda73ba2f525a1d0abe5a13e074 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 f5f65ba9305df53bb4a95afcc297f6bfe441ab7a..b66be1d6251f0bfde9c04b103943158952b9c1c6 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 9bf4563c8cd4e13948555f4446989e91b8c2687d..4c77a1475887504958c8884cd540d0bdf5697822 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 9ccb3680e2919874b7ad15a85c8b3c597e39083d..cde2dc82ad67131375f9493d47384e256eb708d1 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 19c6611afb1159e90e569e04971eec187da1bbab..b330002eca963b2f27dc42381dd90b7ae6379d5f 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 e69f47ab8625886339479d8da73957603665d6aa..160d5ced13653b530c18a30a634a301484a5f957 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 841850c4fefb3bc6b3bc6b678eefa8887bf517fa..3c0579fa6462ea7496f28af5b5ebc819b84f0cec 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 34436ded0ad5db8a2d0b97d157f0d802891256a4..bd1284006ff3f389db475654aee11f3e21604cf4 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 2059c345c71b2421ed931990f7471fccdfa83ad5..0399ececdacea419c547292619239e0b51aceea7 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 e0b8c5d181d57181580186b48c8a832594d15550..8f0835453855fa211165d61038556ce98f03a81d 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 b27b01329e10386ad60dee893ca52c897b1d10a5..7406f3753ddcdd15481c6defa1d9e2a36c403c12 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 7d3b426a606878abe05699292d827739fcec4948..1eddbb4b8b52625248ac77e374a6af904047cdf5 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 02eaa96e98d63b5f8cccfe3bfa8463d6565ef361..d53990a56ccd8c1449c45704adea367eac5b0f35 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 e596deec5d4fb9c3ec0864d3e1db015137fa16de..d35d7c7c7911e44930051c246e6e599cacec7c37 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 7ccb02c97211ab9dfbf100b5cf16abd9c45358d0..7186aaebe57942d239821101d28e1f9770848930 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 6f6d041654125ff27303bcd95cd853297b8ba836..1242e9d2e9cc9af841e56d5ffcad96c5c0595747 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 1af3127519259cc44ffd7db880c28f39dc8983da..e45fc726212b250492260e4c551bc5c1bed3dea4 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 a1609d838a046745346cd36f02e063314057b88a..f51fdfbc660171bd5485c37869384790319e43e1 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 12ba3cd152852bbd7ea98e40b0921ae2110bc5a6..1a5a4888c93f0f23d46045a7048f47755e2075b2 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 0304f94f6900c3178afd03ca5c1d3534896a70a6..f759f59bfe6bff258657a4623bfdec01048222e4 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 00b7a2ea9727b69b5353a6f10faf09750e7667cf..c00510fa3097c46ce53ddc5288b6bb2e0f618641 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 cf8e73a78c435b8f993f61ab80c07057b10d60d4..8603b8643b06d45928d41616d7db798b65d68bef 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 8ab4ee60ca741522d565be563559c1224d23022d..f491384582b905f2aba39ffa65dc80f073344669 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 4567fc14d3f21c1ad2db640e9264fe6ec387e4cb..8833d4b88cb93b0134e3239aa139a3c6a34585a5 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 5355cebbd9cbf82b76690098e670e0af76855c9c..febfc6902d6a8cdf0d0bee4a199bbdadd5cc094d 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 fafc9f18c67cf1cd72ee5d88375dfce1631f8fe6..b32803feb652aad71ea799b02aff6a7c733f6b40 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 f312b589f11a835903ac4080566ce7f14b81df3a..ea1757685829577ec77aa94c1c1de8ff79dc8ce2 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 e45eef5cb3a61dcb648a8934330ceabd2d36552f..0ea8a003a607d3271ff50d8c4909948c933b520b 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 42db4cd7cb58a9c6b6cd3cd75b24f28ab2bd0149..00220370476099169b87412b86f2b397e6574c2f 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 06cda3ce5eb47f2d1ac33fdfe85205c3dbb1afbb..7cebf7b9f4cb6083bf3625b520be6bf5c1e30ae1 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 68f7b320300808fd20c819154f7fcd6d4b8e4705..f7d5946d2dd0477f135ef6c82b6f6190410c1156 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 7319b2f20bc6c107e0e135a976e75355c26e0a7c..a1c57a5359d505bcb8ba41a06b9ab4d7003f649f 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 4bb14526c7b277ba0348fd36954e862c6d997ab4..729932cbcb7a79c002c3134b0ccbdad052e6c9ad 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 03a18359466383b2b457973f30e5d872e498228f..e1ed4495741e0e69942ef91292998f274f08b9c9 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 256fe3fd89b4c89ca13976f788b4c4ecccde0aca..5360df332a1ad973cdeed1d0a09c8a6c7372fc9e 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 996f0aaa0392ad6ab229d4cd1f1429419530bd06..15837823e65ac26836451b1a26c528b025cde2f5 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 d265352833e4dbbf7b2d88c7ed8483849670c57d..4440415631b5dd90793189134a401c3e655e9dfa 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 cc4018b105ace85d2ef41e338aede20e702b64bf..b56d00620330f489f0e440f296aa0e575f5b6465 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 ad8886669f22c25f17b0a08d404ba0c81efd8cec..f7febc17e4242c9d2b6f01189995ec86afcdfecc 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 317446467c2dcd3b4e657f30019dc3407b098146..6f15c07d5d656a644e39895b095726493790376a 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 d3bf03c164d12c1a524f8efffead3446eb2b17eb..f87a4799a8dabf85382536a3faf4beb8eb9deab9 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 541d61dd21f62783f1efeb762824b51b4bb54b27..0e83fb39280cd62436229a5d74a6b8cd5ff5def8 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 68686f72d14cc2cfa28af182e0714db28e980b5b..644e3bf20b5a617f34df40a686b12dadabab3bf4 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 08a2f449cf02a90603131b2b7dca16623c10df5e..af4202973238a17d341109ddadd4f1ede3fe9319 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 b4488a2eef755c6056994295834de7d54afba023..9a72e4b44bb7cde362196aebea23713899381e18 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 ae1efe494c8c2dd823b6c5a7dd6b428795ecf024..3d0e928ef9f2da8cd8a22afc259eef4c4c6a90e3 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 745624c457517ac366c4f7734bd7960c9bb6d3d7..71d582bb70d8a4e1f6bda7d6d77b88051d08f994 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 d5438b227de994181748fcdadfd7c43f3a49b05b..69171aaeec78721bd2c156951fea6e5d791df366 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 e7be6f8f5827d5e2172721c25c0a7529cc7e321a..c0f99adcbda13fd6af6563f097ae04be9534acee 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 108079350d90481f0a0ec71c200f2a62b0d93443..2c64ede8741331662b1b3085078c4ba5e77364af 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 683fa0398606aed22d2fafb21e85f26d2de82070..f4fad0001bcf153f14c432216195984d1da38804 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 b7198f212195417767e50c26497c272c0026b8c5..d3103749d06ab0fc0e6819ac4ff21ffb6392ead5 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 0000000000000000000000000000000000000000..54cf436f968546860044cf4e9c28629428996dff
--- /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 0000000000000000000000000000000000000000..ad5037857fb279840fcab7c6a6b9d6d5e8a97f9b
--- /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 419908727596f04383abf22f2f13354e1a835945..6242ecc18d1f1b3df5d183dbccc6b59aeeb41cf2 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 25fab072de6d37a28cf0644e15e32c0278ae8c2e..c6efd63271876b27d54960adc4f32e5697b3d139 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 ce5ae27c8641259ef90652d9d36dffffee6ad2bf..4ae36f3622c5bc5bc304ea335a19104bea4efaf1 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 1eb2d98d38c1da61d05b0891f7e6f88cda650e87..602fbcee4551820ff7cc505da2f0ff4892dbc75f 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 f98119eab16be0479dd44dbd92e7c66bb668296d..8722ef3517205bc1e9d53b74c754e44cc6a87292 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 28d11c16b762f742bdcc3364c4d01de67d6ca0c3..7701838d407cb735e23a76bd8de2a1f74bdb558a 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 f5bec06d977060be6fd796cedaea8bfde736f059..83b93bbfb6321503ef84c4d54421936a7e2cd2b1 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 fd148fcfcc5208e58353e0a847249b4d715a3c14..4923f3182ed2e685eaefa4653bae7a840b9b0fb8 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 8fa47dc923f6337a7a09483991e497cb2d08da7f..6ef7042aa6964c78ea5a70bfac37a58a5fb76955 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 44da21eca973d30b54965cbce4a673f9ac225036..3c87147b3e30abae9d15aa503bf164147ddaf18c 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 a447493695dcb04a94297946066499e67a8c077c..2a6bab76fb2ec98089ab153e3c13a1ad57cddf81 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 088bf7f0843f70bdd215e1389d1c4bcc465f263e..6465583c14eac05255723276ac81be8d94f5cafb 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 211ce3cd5b2891d14d9a44a6e6f5862aed9eb762..66ebbb989c5bd9fd1fe05f9c2d258e59e66feaff 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 9a71c60d69cd2689f9435f505c51952355f3805c..44b761fb982e26370f6bc2f85c71e0618c85150b 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 131d47bfa680cd438e8146e4de79bcf1a3b99d29..5a088c5283873e658f87f003c5766d010bf1dda8 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 f6369ee2efd75c5241cb13ca4243de875428f610..c24505d85e3f7e748301f1d05570e6df56b137d5 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
(*