diff --git a/Makefile b/Makefile
index ce5d740b6d4f2ffd7428765694e2e42949dd6b68..a4ba43c60ea3355165bafcb0f4fbabaec98098e3 100644
--- a/Makefile
+++ b/Makefile
@@ -821,52 +821,29 @@ PLUGIN_TESTS_DIRS+=value/traces
# Files for the binding to Apron domains. Only available if Apron is available.
ifeq ($(HAS_APRON),yes)
PLUGIN_REQUIRES+= apron.octMPQ apron.boxMPQ apron.polkaMPQ apron.apron gmp
-src/plugins/value/domains/apron/apron_domain.ml: \
- src/plugins/value/domains/apron/apron_domain.ok.ml \
- share/Makefile.config
- $(CP_IF_DIFF) $< $@
- $(CHMOD_RO) $@
+APRON_CMO:= domains/apron/apron_domain
else
-src/plugins/value/domains/apron/apron_domain.ml: \
- src/plugins/value/domains/apron/apron_domain.ko.ml \
- share/Makefile.config
- $(CP_IF_DIFF) $< $@
- $(CHMOD_RO) $@
-endif
-PLUGIN_GENERATED+= src/plugins/value/domains/apron/apron_domain.ml
+APRON_CMO:=
PLUGIN_DISTRIB_EXTERNAL+= \
- domains/apron/apron_domain.ok.ml domains/apron/apron_domain.ko.ml
+ domains/apron/apron_domain.ml domains/apron/apron_domain.mli
+endif
# Files for the numerors domain. Only available is MPFR is available.
NUMERORS_FILES:= \
values/numerors/numerors_utils values/numerors/numerors_float \
values/numerors/numerors_interval values/numerors/numerors_arithmetics \
- values/numerors/numerors_value
+ values/numerors/numerors_value domains/numerors/numerors_domain
ifeq ($(HAS_MPFR),yes)
PLUGIN_REQUIRES+= gmp
PLUGIN_TESTS_DIRS+=value/numerors
NUMERORS_CMO:= $(NUMERORS_FILES)
-src/plugins/value/domains/numerors/numerors_domain.ml: \
- src/plugins/value/domains/numerors/numerors_domain.ok.ml \
- share/Makefile.config
- $(CP_IF_DIFF) $< $@
- $(CHMOD_RO) $@
else
# Do not compile numerors files, but include them in the distributed files.
NUMERORS_CMO:=
PLUGIN_DISTRIB_EXTERNAL+= $(addsuffix .ml,$(NUMERORS_FILES))
PLUGIN_DISTRIB_EXTERNAL+= $(addsuffix .mli,$(NUMERORS_FILES))
-src/plugins/value/domains/numerors/numerors_domain.ml: \
- src/plugins/value/domains/numerors/numerors_domain.ko.ml \
- share/Makefile.config
- $(CP_IF_DIFF) $< $@
- $(CHMOD_RO) $@
endif
-PLUGIN_GENERATED+= src/plugins/value/domains/numerors/numerors_domain.ml
-PLUGIN_DISTRIB_EXTERNAL+= \
- domains/numerors/numerors_domain.ok.ml \
- domains/numerors/numerors_domain.ko.ml
# General rules for ordering files within PLUGIN_CMO:
# - try to keep the legacy Value before Eva
@@ -878,7 +855,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 \
@@ -890,13 +867,11 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
domains/traces_domain \
domains/simple_memory \
domains/gauges/gauges_domain \
- domains/apron/apron_domain \
domains/hcexprs \
domains/equality/equality domains/equality/equality_domain \
domains/offsm_domain \
domains/symbolic_locs \
domains/sign_domain \
- $(NUMERORS_CMO) domains/numerors/numerors_domain \
domains/cvalue/warn domains/cvalue/locals_scoping \
domains/cvalue/cvalue_offsetmap \
utils/value_results \
@@ -918,7 +893,8 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
engine/partition engine/partitioning_parameters engine/trace_partitioning \
engine/iterator \
engine/initialization \
- engine/compute_functions engine/analysis register
+ engine/compute_functions engine/analysis register \
+ $(APRON_CMO) $(NUMERORS_CMO)
PLUGIN_CMI:= values/abstract_value values/abstract_location \
domains/abstract_domain domains/simpler_domains
PLUGIN_DEPENDENCIES:=Callgraph LoopAnalysis RteGen
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 9ddb17082d70603ad752fecbcb7898de4d857cf4..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.k
-
-(** 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
deleted file mode 100644
index 9ccb3680e2919874b7ad15a85c8b3c597e39083d..0000000000000000000000000000000000000000
--- a/src/plugins/value/domains/apron/apron_domain.ko.ml
+++ /dev/null
@@ -1,49 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-let ok = false
-
-module type S = Abstract_domain.Internal
- 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 Octagon = U
-module Box = U
-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 ../../../.."
-End:
-*)
diff --git a/src/plugins/value/domains/apron/apron_domain.ok.ml b/src/plugins/value/domains/apron/apron_domain.ml
similarity index 95%
rename from src/plugins/value/domains/apron/apron_domain.ok.ml
rename to src/plugins/value/domains/apron/apron_domain.ml
index e69f47ab8625886339479d8da73957603665d6aa..15035124c408a28ef47136b8b728305bdab97c97 100644
--- a/src/plugins/value/domains/apron/apron_domain.ok.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -20,22 +20,14 @@
(* *)
(**************************************************************************)
-#24 "src/plugins/value/domains/apron/apron_domain.ok.ml"
-
open Cil_types
open Eval
open Apron
let dkey = Value_parameters.register_category "d-apron"
-let ok = true
-
let debug = false
-module type S = Abstract_domain.Internal
- with type value = Main_values.Interval.t
- and type location = Precise_locs.precise_location
-
let abort exclog =
let open Manager in
Value_parameters.fatal
@@ -357,22 +349,19 @@ let ival_to_interval = function
(* Abstract Domain Functor *)
(* -------------------------------------------------------------------------- *)
-module Make
- (Man: sig
- type t
- val manager: t Manager.t
- val name: string
- val key: t Abstract1.t Abstract_domain.key
- end)
-= struct
+module type Input = sig
+ type t
+ val manager: t Manager.t
+ val name: string
+end
+
+module Make (Man : Input) = struct
type state = Man.t Abstract1.t
type value = Main_values.Interval.t
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,54 +714,52 @@ 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. *)
let () = Floating_point.set_round_nearest_even ()
-module Octagon = Domain_builder.Complete (Make (Apron_Octagon))
-module Box = Domain_builder.Complete (Make (Apron_Box))
-module Polka_Loose = Domain_builder.Complete (Make (Apron_Polka_Loose))
-module Polka_Strict = Domain_builder.Complete (Make (Apron_Polka_Strict))
-module Polka_Equalities = Domain_builder.Complete (Make (Apron_Polka_Equalities))
+let make name enable (module Man: Input) =
+ let module Domain = Domain_builder.Complete (Make (Man)) in
+ let open Abstractions in
+ register ~enable { name; priority = 1;
+ values = Single (module Main_values.Interval);
+ domain = Domain (module Domain); }
+
+let () =
+ let open Value_parameters in
+ make "apron octagons" ApronOctagon.get (module Apron_Octagon);
+ make "apron box" ApronBox.get (module Apron_Box);
+ make "polka loose" PolkaLoose.get (module Apron_Polka_Loose);
+ make "polka strict" PolkaStrict.get (module Apron_Polka_Strict);
+ make "polka equalities" PolkaEqualities.get (module Apron_Polka_Equalities);
+ register_apron ()
(*
diff --git a/src/plugins/value/domains/apron/apron_domain.mli b/src/plugins/value/domains/apron/apron_domain.mli
index 19c6611afb1159e90e569e04971eec187da1bbab..5d86a35d509779c5d55ddf1de342b5f592f297fa 100644
--- a/src/plugins/value/domains/apron/apron_domain.mli
+++ b/src/plugins/value/domains/apron/apron_domain.mli
@@ -24,43 +24,6 @@
the APRON library: http://apron.cri.ensmp.fr/library
For now, this binding only processes scalar integer variables. *)
-(** Are apron domains available? *)
-val ok : bool
-
-(** Signature of an Apron domain in Eva. *)
-module type S = Abstract_domain.Internal
- with type value = Main_values.Interval.t
- and type location = Precise_locs.precise_location
-
-
-(** Apron domains available for Eva. *)
-
-(** Octagons abstract domain. *)
-module Octagon : S
-
-(** Intervals abstract domain. *)
-module Box : S
-
-(** Loose polyhedra of the NewPolka library.
- Cannot have strict inequality constraints. Algorithmically more efficient. *)
-module Polka_Loose : S
-
-(** Strict polyhedra of the NewPolka library. *)
-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/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index 841850c4fefb3bc6b3bc6b678eefa8887bf517fa..019f87cc0ee61fa5f2fb0ab04a5b43ce16e56256 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -22,15 +22,8 @@
open Eval
-let key = Structure.Key_Domain.create_key "cvalue_domain"
let dkey_card = Value_parameters.register_category "cardinal"
-let extract get = match get key with
- | None -> fun _ -> Cvalue.Model.top
- | Some get -> function
- | `Bottom -> Cvalue.Model.bottom
- | `Value state -> get state
-
module Model = struct
include Cvalue.Model
@@ -168,10 +161,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 +182,7 @@ module State = struct
end )
let name = "Cvalue domain"
+ let key = Structure.Key_Domain.create_key "cvalue_domain"
type value = Model.value
type location = Model.location
@@ -552,9 +542,6 @@ end
let () = Db.Value.display := (fun fmt kf -> State.display ~fmt kf)
-let inject cvalue_model = cvalue_model, Locals_scoping.bottom ()
-let project (state, _) = state
-
type prefix = Hptmap.prefix
module Subpart = struct
@@ -562,12 +549,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..cf750b4e60f4caad41803517a7d468d98c6b948b 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.mli
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.mli
@@ -22,28 +22,18 @@
(** 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
-
-val extract :
- (Cvalue.Model.t Abstract_domain.key -> ('state -> Cvalue.Model.t) option) ->
- 'state Eval.or_bottom -> Cvalue.Model.t
-
-val inject : Cvalue.Model.t -> State.t
-val project : State.t -> Cvalue.Model.t
-
+ and type state = Cvalue.Model.t * Locals_scoping.clobbered_set
(** Specific functions for partitioning optimizations. *)
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..0256e97c80d334675f3171ec8e0e2dfb1eb4ae86 100644
--- a/src/plugins/value/domains/domain_lift.ml
+++ b/src/plugins/value/domains/domain_lift.ml
@@ -37,7 +37,7 @@ end
module Make
- (Domain: Abstract_domain.Internal)
+ (Domain: Abstract_domain.Leaf)
(Convert : Conversion with type internal_value := Domain.value
and type internal_location := Domain.location)
= struct
@@ -45,7 +45,8 @@ 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 structure = Abstract.Domain.Leaf (Domain.key, (module Domain))
+
let log_category = Domain.log_category
type value = Convert.extended_value
diff --git a/src/plugins/value/domains/domain_lift.mli b/src/plugins/value/domains/domain_lift.mli
index 9e16a8a292ee65d5fd7ff670ac2e9228b9180ba1..9ed356565906f71c2c7aace94cb44fc0e9f5ad9b 100644
--- a/src/plugins/value/domains/domain_lift.mli
+++ b/src/plugins/value/domains/domain_lift.mli
@@ -36,10 +36,10 @@ end
module Make
- (Domain: Abstract_domain.Internal)
+ (Domain: Abstract_domain.Leaf)
(Convert : Conversion with type internal_value := Domain.value
and type internal_location := Domain.location)
- : Abstract_domain.Internal with type state = Domain.state
+ : Abstract.Domain.Internal with type state = Domain.state
and type value = Convert.extended_value
and type location = Convert.extended_location
and type origin = Domain.origin
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index e596deec5d4fb9c3ec0864d3e1db015137fa16de..1985b6c173ad631b55d0401c0bf67494861cf831 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -28,8 +28,8 @@ let product_category = Value_parameters.register_category "domain_product"
module Make
(Value: Abstract_value.S)
- (Left: Abstract_domain.Internal with type value = Value.t)
- (Right: Abstract_domain.Internal with type value = Left.value
+ (Left: Abstract.Domain.Internal with type value = Value.t)
+ (Right: Abstract.Domain.Internal with type value = Left.value
and type location = Left.location)
= struct
@@ -51,7 +51,7 @@ module Make
(struct let module_name = name end)
type state = t
- let structure = Abstract_domain.Node (Left.structure, Right.structure)
+ let structure = Abstract.Domain.Node (Left.structure, Right.structure)
let log_category = product_category
diff --git a/src/plugins/value/domains/domain_product.mli b/src/plugins/value/domains/domain_product.mli
index c883a94ba8d1cb26816c742f8c8bf9a5bbe8532c..859988e255221878be47fd1ef9fc7836ca81e6a6 100644
--- a/src/plugins/value/domains/domain_product.mli
+++ b/src/plugins/value/domains/domain_product.mli
@@ -24,10 +24,10 @@ val product_category: Value_parameters.category
module Make
(Value: Abstract_value.S)
- (Left: Abstract_domain.Internal with type value = Value.t)
- (Right: Abstract_domain.Internal with type value = Left.value
+ (Left: Abstract.Domain.Internal with type value = Value.t)
+ (Right: Abstract.Domain.Internal with type value = Left.value
and type location = Left.location)
- : Abstract_domain.Internal with type value = Value.t
+ : Abstract.Domain.Internal with type value = Value.t
and type location = Left.location
and type state = Left.state * Right.state
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.ko.ml b/src/plugins/value/domains/numerors/numerors_domain.ko.ml
deleted file mode 100644
index eb6bc8b9a4fd68b544826004a66bc62dc4b3f43d..0000000000000000000000000000000000000000
--- a/src/plugins/value/domains/numerors/numerors_domain.ko.ml
+++ /dev/null
@@ -1,39 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-#24 "src/plugins/value/domains/numerors/numerors_domain.ko.ml"
-
-type value
-type location = Precise_locs.precise_location
-let value_key = Structure.Key_Value.create_key "dummy_numerors_values"
-
-let ok = false
-
-let abort () =
- Value_parameters.abort
- "The numerors domain has been requested but is not available, as Frama-C \
- did not found the MPFR library. The analysis is aborted."
-
-let add_numerors_value _ = abort ()
-let numerors_domain = abort
-
-let reduce_error _ = fun v -> v
diff --git a/src/plugins/value/domains/numerors/numerors_domain.ok.ml b/src/plugins/value/domains/numerors/numerors_domain.ml
similarity index 57%
rename from src/plugins/value/domains/numerors/numerors_domain.ok.ml
rename to src/plugins/value/domains/numerors/numerors_domain.ml
index cf8e73a78c435b8f993f61ab80c07057b10d60d4..6295adc0eed64e7d4495b8c1dc62ed8aba6ec0cf 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ok.ml
+++ b/src/plugins/value/domains/numerors/numerors_domain.ml
@@ -20,17 +20,10 @@
(* *)
(**************************************************************************)
-#24 "src/plugins/value/domains/numerors/numerors_domain.ok.ml"
-
open Eval
open Cil_types
-type value = Numerors_value.t
-type location = Precise_locs.precise_location
-let value_key = Numerors_value.error_key
-
-let ok = true
-
+(* The numerors values, plus some builtin functions. *)
module Numerors_Value = struct
include Numerors_value
@@ -87,61 +80,7 @@ module Numerors_Value = struct
]
end
-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
- | None -> forward_cast
- | Some get_cvalue ->
- fun ~src_type ~dst_type (value, num) ->
- forward_cast ~src_type ~dst_type (value, num) >>-: fun (value', num) ->
- let num = match src_type, dst_type with
- | Eval_typ.TSInt _, Eval_typ.TSFloat fkind ->
- begin
- try
- let cvalue = get_cvalue value in
- let ival = Cvalue.V.project_ival cvalue in
- match Ival.min_and_max ival with
- | Some min, Some max ->
- let min, max = Integer.to_int min, Integer.to_int max in
- let prec = Numerors_utils.Precisions.of_fkind fkind in
- Numerors_value.of_ints ~prec min max
- | _, _ -> num
- (* Integer.to_int may fail for too big integers. *)
- with Cvalue.V.Not_based_on_null | Z.Overflow -> num
- end
- | _, _ -> num
- in
- value', num
- end in
- (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
- | Some get_error, Some get_cvalue ->
- begin
- let set_error = V.set Numerors_value.error_key in
- fun t ->
- let cvalue = get_cvalue t in
- try
- let ival = Cvalue.V.project_ival cvalue in
- match ival with
- | Ival.Float fval ->
- begin
- let error = get_error t in
- let error = Numerors_value.reduce fval error in
- match error with
- | `Value error -> set_error error t
- | `Bottom -> t (* TODO: we should be able to reduce to bottom. *)
- end
- | _ -> t
- with Cvalue.V.Not_based_on_null -> t
- end
- | _, _ -> fun x -> x
-
-
+(* The numerors domain: a simple memory over the numerors value. *)
module Domain = struct
module Name = struct let name = "numerors" end
include Simple_memory.Make_Domain (Name) (Numerors_Value)
@@ -157,7 +96,72 @@ module Domain = struct
| _, _ -> ()
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)
+(* Reduced product between the cvalue values and the numerors values. *)
+let reduce_error cvalue error =
+ try
+ let ival = Cvalue.V.project_ival cvalue in
+ match ival with
+ | Ival.Float fval ->
+ begin
+ match Numerors_value.reduce fval error with
+ | `Value error -> cvalue, error
+ | `Bottom -> cvalue, error (* TODO: we should be able to reduce to bottom. *)
+ end
+ | _ -> cvalue, error
+ with Cvalue.V.Not_based_on_null -> cvalue, error
+
+(* Reduction of the numerors value resulting from a cast from int to float type,
+ using the cvalue component of value abstractions. *)
+let reduce_cast (module Abstract: Abstractions.S) =
+ let module Val = struct
+ include Abstract.Val
+
+ (* Redefines the [forward_cast] function of the value component. *)
+ let forward_cast =
+ (* If cvalue or numerors do not belong to the abstraction, no reduction:
+ the [forward_cast] function is unchanged. *)
+ match get Main_values.CVal.key, mem Numerors_value.key with
+ | None, _ | _, false -> forward_cast
+ | Some get_cvalue, true ->
+ (* Otherwise, applies the [forward_cast] function, but updates the
+ numerors component of the result. *)
+ fun ~src_type ~dst_type value ->
+ forward_cast ~src_type ~dst_type value >>-: fun result ->
+ match src_type, dst_type with
+ | Eval_typ.TSInt _, Eval_typ.TSFloat fkind ->
+ begin
+ try
+ let cvalue = get_cvalue value in
+ let ival = Cvalue.V.project_ival cvalue in
+ match Ival.min_and_max ival with
+ | Some min, Some max ->
+ let min, max = Integer.to_int min, Integer.to_int max in
+ let prec = Numerors_utils.Precisions.of_fkind fkind in
+ let num = Numerors_value.of_ints ~prec min max in
+ set Numerors_value.key num result
+ | _, _ -> result
+ (* Integer.to_int may fail for too big integers. *)
+ with Cvalue.V.Not_based_on_null | Z.Overflow -> result
+ end
+ | _, _ -> result
+ end in
+ (module struct
+ module Val = Val
+ module Loc = Abstract.Loc
+ module Dom = Abstract.Dom
+ end: Abstractions.S)
+
+(* Register the domain as an Eva abstractions. *)
+let () =
+ let open Abstractions in
+ let domain =
+ { name = "numerors";
+ priority = 0;
+ values = Single (module Numerors_value);
+ domain = Domain (module Domain); }
+ in
+ let reduced_product = Main_values.CVal.key, Numerors_value.key, reduce_error in
+ register ~enable:Value_parameters.NumerorsDomain.get domain;
+ register_value_reduction reduced_product;
+ register_hook reduce_cast;
+ Value_parameters.register_numerors ()
diff --git a/src/plugins/value/domains/numerors/numerors_domain.mli b/src/plugins/value/domains/numerors/numerors_domain.mli
index d08ef39909623588ccb4c7582daf7c7a05bdce2a..6fcd35b31eed7cff62e5bdbbda30383c54f47cfc 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.mli
+++ b/src/plugins/value/domains/numerors/numerors_domain.mli
@@ -20,30 +20,7 @@
(* *)
(**************************************************************************)
-type value
-type location = Precise_locs.precise_location
-val value_key : value Structure.Key_Value.k
-
-(** True if the numerors domain is available;
- False if the MPFR library has not been found. *)
-val ok: bool
-
-(** Functions used by the engine to build numerors abstractions. *)
-
-(** Builds the product between a given value module and the numerors value
- module. If the given value module contains Cvalue, uses cvalues to reduce
- 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)
-
-(* 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)
-
-(** 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)
+(** Numerors domain: computes over-approximations of the rounding errors bounds
+ of floating-point computations.
+ Nothing is exported: the domain is registered as an analysis abstraction
+ in the Eva engine, enabled by the -eva-numerors-domain option. *)
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..e78644f8c489b4125db88289516e89dec38bc0f3 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.Unit
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..5781d60bf7672faf0129790ab98f89cde419dd68 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -20,583 +20,424 @@
(* *)
(**************************************************************************)
-(* Configuration of the abstract domain. *)
-
-type config = {
- cvalue : bool;
- equalities : bool;
- symbolic_locs : bool;
- bitwise : bool;
- gauges : bool;
- apron_oct : bool;
- apron_box : bool;
- polka_loose : bool;
- polka_strict : bool;
- polka_equalities : bool;
- inout: bool;
- signs: bool;
- printer: bool;
- numerors: bool;
- traces: bool;
-}
-
-let configure () = {
- cvalue = Value_parameters.CvalueDomain.get ();
- equalities = Value_parameters.EqualityDomain.get ();
- symbolic_locs = Value_parameters.SymbolicLocsDomain.get ();
- bitwise = Value_parameters.BitwiseOffsmDomain.get ();
- gauges = Value_parameters.GaugesDomain.get ();
- apron_oct = Value_parameters.ApronOctagon.get ();
- apron_box = Value_parameters.ApronBox.get ();
- polka_loose = Value_parameters.PolkaLoose.get ();
- polka_strict = Value_parameters.PolkaStrict.get ();
- polka_equalities = Value_parameters.PolkaEqualities.get ();
- inout = Value_parameters.InoutDomain.get ();
- signs = Value_parameters.SignDomain.get ();
- printer = Value_parameters.PrinterDomain.get ();
- numerors = Value_parameters.NumerorsDomain.get ();
- traces = Value_parameters.TracesDomain.get ();
-}
-
-let default_config = configure ()
-
-let legacy_config = {
- cvalue = true;
- equalities = false;
- symbolic_locs = false;
- bitwise = false;
- gauges = false;
- apron_oct = false;
- apron_box = false;
- polka_loose = false;
- polka_strict = false;
- polka_equalities = false;
- inout = false;
- signs = false;
- printer = false;
- numerors = false;
- traces = false;
-}
+(* --- Registration types --------------------------------------------------- *)
-module type Value = sig
- include Abstract_value.External
- val reduce : t -> t
+type 'v value =
+ | Single of (module Abstract_value.Leaf with type t = 'v)
+ | Struct of 'v Abstract.Value.structure
+
+type precise_loc = Precise_locs.precise_location
+
+module type leaf_domain = Abstract_domain.Leaf with type location = precise_loc
+
+module type domain_functor =
+ functor (Value: Abstract.Value.External) ->
+ (leaf_domain with type value = Value.t)
+
+type 'v domain =
+ | Domain: (module leaf_domain with type value = 'v) -> 'v domain
+ | Functor: (module domain_functor) -> _ domain
+
+type 'v abstraction =
+ { name: string;
+ priority: int;
+ values: 'v value;
+ domain: 'v domain; }
+
+(* --- Config and registration ---------------------------------------------- *)
+
+module Config = struct
+ type flag = Flag: 'v abstraction -> flag
+
+ module Flag = struct
+ type t = flag
+
+ (* Flags are sorted by increasing priority order, and then by name. *)
+ let compare (Flag f1) (Flag f2) =
+ let c = Datatype.Int.compare f1.priority f2.priority in
+ if c <> 0 then c else Datatype.String.compare f1.name f2.name
+ end
+
+ include Set.Make (Flag)
+
+ type dynamic = Dynamic: (unit -> 'a option) * ('a -> 'v abstraction) -> dynamic
+
+ let abstractions = ref []
+ let dynamic_abstractions : dynamic list ref = ref []
+
+ let register ~enable abstraction =
+ abstractions := (enable, Flag abstraction) :: !abstractions
+
+ let dynamic_register ~configure ~make =
+ dynamic_abstractions := Dynamic (configure, make) :: !dynamic_abstractions
+
+ let configure () =
+ let aux config (enable, flag) =
+ if enable () then add flag config else config
+ in
+ let config = List.fold_left aux empty !abstractions in
+ let aux config (Dynamic (configure, make)) =
+ match configure () with
+ | None -> config
+ | Some c -> add (Flag (make c)) config
+ in
+ List.fold_left aux config !dynamic_abstractions
+
+ (* --- Register default abstractions -------------------------------------- *)
+
+ let create ~enable abstract = register ~enable abstract; Flag abstract
+ let create_domain priority name enable values domain =
+ create ~enable
+ { name; priority; values = Single values; domain = Domain domain }
+
+ open Value_parameters
+
+ (* Register standard domains over cvalues. *)
+ let make rank name enable =
+ create_domain rank name enable (module Main_values.CVal)
+
+ let cvalue = make 9 "cvalue" CvalueDomain.get (module Cvalue_domain.State)
+ let gauges = make 6 "gauges" GaugesDomain.get (module Gauges_domain.D)
+ let inout = make 5 "inout" InoutDomain.get (module Inout_domain.D)
+ let traces = make 2 "traces" TracesDomain.get (module Traces_domain.D)
+ let printer = make 2 "printer" PrinterDomain.get (module Printer_domain)
+ let symbolic_locations =
+ make 7 "symbolic_locations" SymbolicLocsDomain.get (module Symbolic_locs.D)
+
+ let sign =
+ create_domain 4 "sign" SignDomain.get
+ (module Sign_value) (module Sign_domain)
+
+ let bitwise =
+ create_domain 3 "bitwise" BitwiseOffsmDomain.get
+ (module Offsm_value.Offsm) (module Offsm_domain.D)
+
+ let equality_domain =
+ { name = "equality";
+ priority = 8;
+ values = Struct Abstract.Value.Unit;
+ domain = Functor (module Equality_domain.Make); }
+ let equality = create ~enable:EqualityDomain.get equality_domain
+
+ (* --- Default and legacy configurations ---------------------------------- *)
+
+ let default = configure ()
+ let legacy = singleton cvalue
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
- and type location = Loc.location
+let register = Config.register
+let dynamic_register = Config.dynamic_register
+
+(* --- Building value abstractions ------------------------------------------ *)
+
+module Leaf_Value (V: Abstract_value.Leaf) = struct
+ include V
+ let structure = Abstract.Value.Leaf (V.key, (module V))
end
-module type Eva = sig
- include S
- module Eval: Evaluation.S with type state = Dom.t
- and type value = Val.t
- and type loc = Loc.location
- and type origin = Dom.origin
+module Leaf_Location (Loc: Abstract_location.Leaf) = struct
+ include Loc
+ let structure = Abstract.Location.Leaf (Loc.key, (module Loc))
end
-(* -------------------------------------------------------------------------- *)
-(* Value Abstraction *)
-(* -------------------------------------------------------------------------- *)
+module Leaf_Domain (D: Abstract_domain.Leaf) = struct
+ include D
+ let structure = Abstract.Domain.Leaf (D.key, (module D))
+end
-module type V = sig
- include Abstract_value.External
- val structure : t Abstract_value.structure
+module type Acc = sig
+ module Val : Abstract.Value.External
+ module Loc : Abstract.Location.Internal with type value = Val.t
+ and type location = precise_loc
+ module Dom : Abstract.Domain.Internal with type value = Val.t
+ and type location = Loc.location
end
-module CVal = struct
- include Main_values.CVal
- include Structure.Open (Structure.Key_Value) (Main_values.CVal)
+module Internal_Value = struct
+ open Abstract.Value
+
+ type value_key_module = V : 'v key * 'v data -> value_key_module
+
+ let open_value_abstraction (module Value : Internal) =
+ (module struct
+ include Value
+ include Structure.Open (Abstract.Value) (Value)
+ end : Abstract.Value.External)
+
+ let add_value_leaf value (V (key, v)) =
+ let module Value = (val open_value_abstraction value) in
+ if Value.mem key then value else
+ (module struct
+ include Value_product.Make (Value) (val v)
+ let structure = Node (Value.structure, Leaf (key, v))
+ end)
+
+ let add_value_structure value internal =
+ let rec aux: type v. (module Internal) -> v structure -> (module Internal) =
+ fun value -> function
+ | Leaf (key, v) -> add_value_leaf value (V (key, v))
+ | Node (s1, s2) -> aux (aux value s1) s2
+ | Unit -> value
+ in
+ aux value internal
+
+ let build_values config initial_value =
+ let build (Config.Flag abstraction) acc =
+ match abstraction.values with
+ | Struct structure -> add_value_structure acc structure
+ | Single (module V) -> add_value_leaf acc (V (V.key, (module V)))
+ in
+ let value = Config.fold build config initial_value in
+ open_value_abstraction value
+
+
+ module Convert
+ (Value: Abstract.Value.External)
+ (Struct: sig type v val s : v value end)
+ = struct
+
+ let structure = match Struct.s with
+ | Single (module V) -> Abstract.Value.Leaf (V.key, (module V))
+ | Struct s -> s
+
+ type extended_value = Value.t
+
+ let replace_val =
+ let rec set: type v. v structure -> v -> Value.t -> Value.t =
+ function
+ | Leaf (key, _) -> Value.set key
+ | Node (s1, s2) ->
+ let set1 = set s1 and set2 = set s2 in
+ fun (v1, v2) value -> set1 v1 (set2 v2 value)
+ | Unit -> fun () value -> value
+ in
+ set structure
+
+ let extend_val v = replace_val v Value.top
+
+ let restrict_val =
+ let rec get: type v. v structure -> Value.t -> v = function
+ | Leaf (key, _) -> Extlib.the (Value.get key)
+ | Node (s1, s2) ->
+ let get1 = get s1 and get2 = get s2 in
+ fun v -> get1 v, get2 v
+ | Unit -> fun _ -> ()
+ in
+ get structure
+
+ type extended_location = Main_locations.PLoc.location
+
+ let restrict_loc = fun x -> x
+ let extend_loc = fun x -> x
+ end
end
-let has_apron config =
- config.apron_oct || config.apron_box || config.polka_equalities
- || config.polka_loose || config.polka_strict
-
-(* The apron domains relies on a specific interval abstraction to communicate
- with other domains. This function adds the intervals to the current [value]
- abstraction. These intervals carry the same information as the cvalue
- 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 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
- end in
- (module V: Abstract_value.Internal)
-
-let open_value_abstraction value =
- let module Value = (val value : Abstract_value.Internal) in
- (module struct
- include Value
- include Structure.Open (Structure.Key_Value) (Value)
- end : V)
-
-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)
- in
- let value =
- if config.signs
- then
- let module V = Value_product.Make ((val value)) (Sign_value) in
- (module V: Abstract_value.Internal)
- else value
- in
- let value =
- if config.numerors
- then Numerors_domain.add_numerors_value value
- else value
+(* --- Building domain abstractions ----------------------------------------- *)
+
+module type internal_loc =
+ Abstract.Location.Internal with type location = precise_loc
+module type internal_domain =
+ Abstract.Domain.Internal with type location = precise_loc
+
+let eq_value:
+ type a b. a Abstract.Value.structure -> b value -> (a,b) Structure.eq option
+ = fun structure -> function
+ | Struct s -> Abstract.Value.eq_structure structure s
+ | Single (module V) ->
+ match structure with
+ | Abstract.Value.Leaf (key, _) -> Abstract.Value.eq_type key V.key
+ | _ -> None
+
+let add_domain (type v) (abstraction: v abstraction) (module Acc: Acc) =
+ let domain : (module internal_domain with type value = Acc.Val.t) =
+ match abstraction.domain with
+ | Functor make ->
+ let module Make = (val make: domain_functor) in
+ (module Leaf_Domain (Make (Acc.Val)))
+ | Domain domain ->
+ match eq_value Acc.Val.structure abstraction.values with
+ | Some Structure.Eq ->
+ let module Domain = (val domain) in
+ (module Leaf_Domain (Domain))
+ | None ->
+ let module Domain = (val domain : leaf_domain with type value = v) in
+ let module Struct = struct
+ type v = Domain.value
+ let s = abstraction.values
+ end in
+ let module Convert = Internal_Value.Convert (Acc.Val) (Struct) in
+ (module Domain_lift.Make (Domain) (Convert))
in
- let value =
- if has_apron config
- then add_apron_value config value
- else value
+ let domain : (module internal_domain with type value = Acc.Val.t) =
+ match Abstract.Domain.(eq_structure Acc.Dom.structure Unit) with
+ | Some _ -> domain
+ | None ->
+ (* The new [domain] becomes the left leaf of the domain product, and will
+ be processed before the domains from [Acc.Dom] during the analysis. *)
+ (module Domain_product.Make (Acc.Val) ((val domain)) (Acc.Dom))
in
- open_value_abstraction value
-
-(* Builds a module conversion from a generic external value to a key. *)
-module Convert
- (Value : Abstract_value.External)
- (K : sig type v val key : v Abstract_value.key end)
-= struct
- type extended_value = Value.t
- type extended_location = Main_locations.PLoc.location
+ (module struct
+ module Val = Acc.Val
+ module Loc = Acc.Loc
+ module Dom = (val domain)
+ end : Acc)
- let extend_val =
- let set = Value.set K.key in
- fun v -> set v Value.top
+let build_domain config abstract =
+ let build (Config.Flag abstraction) acc = add_domain abstraction acc in
+ (* Domains in the [config] are sorted by increasing priority: domains with
+ higher priority are added last: they will be at the top of the domains
+ tree, and thus will be processed first during the analysis. *)
+ Config.fold build config abstract
- let replace_val = Value.set K.key
- let restrict_val = match Value.get K.key with
- | None -> assert false
- | Some get -> get
+(* --- Value reduced product ----------------------------------------------- *)
- let restrict_loc = fun x -> x
- let extend_loc = fun x -> x
+module type Value = sig
+ include Abstract.Value.External
+ val reduce : t -> t
end
-
-(* -------------------------------------------------------------------------- *)
-(* Cvalue Domain *)
-(* -------------------------------------------------------------------------- *)
-
-(* 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
- and type location = Precise_locs.precise_location
- module Dom : Abstract_domain.Internal with type value = Val.t
+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
and type location = Loc.location
end
-let default_root_abstraction config =
- if config.cvalue
- then
- (module struct
- module Val = CVal
- module Loc = Main_locations.PLoc
- module Dom = Cvalue_domain.State
- end : Abstract)
- else
- (module struct
- module Val = CVal
- module Loc = Main_locations.PLoc
- module Dom = Unit_domain.Make (Val) (Loc)
- end : Abstract)
-
-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
- end in
- let module Conv = Convert (Val) (K) 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)
- end : Abstract)
- else
- (module struct
- module Val = Val
- module Loc = Location_lift.Make (Main_locations.PLoc) (Conv)
- module Dom = Unit_domain.Make (Val) (Loc)
- end : Abstract)
-
-
-(* -------------------------------------------------------------------------- *)
-(* Apron Domains *)
-(* -------------------------------------------------------------------------- *)
-
-let add_apron_domain abstract apron =
- let module Abstract = (val abstract: Abstract) in
- let module K = struct
- type v = Main_values.Interval.t
- 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
- (module struct
- module Val = Abstract.Val
- module Loc = Abstract.Loc
- module Dom = Domain_product.Make (Abstract.Val) (Abstract.Dom) (Apron)
- end : Abstract)
+module type Eva = sig
+ include S
+ module Eval: Evaluation.S with type state = Dom.t
+ and type value = Val.t
+ and type loc = Loc.location
+ and type origin = Dom.origin
+end
-let dkey_experimental = Value_parameters.register_category "experimental-ok"
-let add_apron_domain abstractions apron =
- if not (Value_parameters.is_debug_key_enabled dkey_experimental) then
- Value_parameters.warning "The Apron domains binding is experimental.";
- if Apron_domain.ok
- then add_apron_domain abstractions apron
- else
- Value_parameters.abort
- "Apron domain requested but apron binding not available: analysis aborted."
+type ('a, 'b) value_reduced_product =
+ 'a Abstract.Value.key * 'b Abstract.Value.key * ('a -> 'b -> 'a * 'b)
+type v_reduced_product = R: ('a, 'b) value_reduced_product -> v_reduced_product
-(* -------------------------------------------------------------------------- *)
-(* Equality Domain *)
-(* -------------------------------------------------------------------------- *)
+let value_reduced_product = ref []
-module CvalueEquality = Equality_domain.Make (CVal)
+let register_value_reduction reduced_product =
+ value_reduced_product := (R reduced_product) :: !value_reduced_product
-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
- (module struct
- module Val = Abstract.Val
- module Loc = Abstract.Loc
- module Dom = Dom
- end : Abstract)
-
-let add_equalities (type v) (module Abstract : Abstract with type Val.t = v) =
- match Abstract.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)
- | Some Structure.Eq ->
- let module Dom =
- Domain_product.Make (Abstract.Val) (Abstract.Dom) (CvalueEquality)
- in
- (module struct
- module Val = Abstract.Val
- module Loc = Abstract.Loc
- module Dom = Dom
- end : Abstract)
+(* When the value abstraction contains both a cvalue and an interval
+ component (coming currently from an Apron domain), reduce them from each
+ other. If the Cvalue is not a scalar do nothing, because we do not
+ currently use Apron for pointer offsets. *)
+let reduce_apron_itv cvalue ival =
+ match ival with
+ | None -> begin
+ try cvalue, Some (Cvalue.V.project_ival cvalue)
+ with Cvalue.V.Not_based_on_null -> cvalue, ival
end
- | _ -> add_generic_equalities (module Abstract)
-
-
-(* -------------------------------------------------------------------------- *)
-(* Offsetmap Domain *)
-(* -------------------------------------------------------------------------- *)
-
-let add_offsm abstract =
- let module Abstract = (val abstract : Abstract) in
- let module K = struct
- type v = Offsm_value.offsm_or_top
- let key = Offsm_value.offsm_key
- end in
- let module Conv = Convert (Abstract.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
- (module struct
- module Val = Abstract.Val
- module Loc = Abstract.Loc
- module Dom = Dom
- end : Abstract)
-
-(* -------------------------------------------------------------------------- *)
-(* Domains on standard locations and values *)
-(* -------------------------------------------------------------------------- *)
-
-module type Standard_abstraction = Abstract_domain.Internal
- 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 K = struct
- type v = Cvalue.V.t
- let key = Main_values.cvalue_key
- end in
- let module Conv = Convert (Abstract.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
- (module struct
- module Val = Abstract.Val
- module Loc = Abstract.Loc
- module Dom = Dom
- end : Abstract)
-
-(* List of abstractions registered by other plugins *)
-let dynamic_abstractions = ref []
-
-let add_dynamic_abstractions abstract =
- List.fold_left
- (fun d abstract -> add_standard_domain abstract d)
- abstract !dynamic_abstractions
-
-let register_dynamic_abstraction d =
- dynamic_abstractions := d :: !dynamic_abstractions
-
-(* --------------------------------------------------------------------------*)
-(* Symbolic locations *)
-(* --------------------------------------------------------------------------*)
-
-let add_symbolic_locs =
- add_standard_domain (module Symbolic_locs.D)
-
-(* -------------------------------------------------------------------------- *)
-(* Gauges *)
-(* -------------------------------------------------------------------------- *)
-
-let add_gauges =
- add_standard_domain (module Gauges_domain.D)
-
-(* -------------------------------------------------------------------------- *)
-(* Inout *)
-(* -------------------------------------------------------------------------- *)
-
-let add_inout =
- add_standard_domain (module Inout_domain.D)
-
-(* -------------------------------------------------------------------------- *)
-(* Sign Domain *)
-(* -------------------------------------------------------------------------- *)
-
-let add_signs abstract =
- let module Abstract = (val abstract : Abstract) in
- let module K = struct
- type v = Sign_value.t
- let key = Sign_value.sign_key
- end in
- let module Conv = Convert (Abstract.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
- (module struct
- module Val = Abstract.Val
- module Loc = Abstract.Loc
- module Dom = Dom
- end : Abstract)
-
-(* -------------------------------------------------------------------------- *)
-(* Numerors Domain *)
-(* -------------------------------------------------------------------------- *)
-
-let add_errors abstract =
- let module Abstract = (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 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
- (module struct
- module Val = Abstract.Val
- module Loc = Abstract.Loc
- module Dom = Dom
- end : Abstract)
+ | Some ival ->
+ try
+ let ival' = Cvalue.V.project_ival cvalue in
+ (match ival' with
+ | Ival.Float _ -> raise Cvalue.V.Not_based_on_null
+ | _ -> ());
+ let reduced_ival = Ival.narrow ival ival' in
+ let cvalue = Cvalue.V.inject_ival reduced_ival in
+ cvalue, Some reduced_ival
+ with Cvalue.V.Not_based_on_null -> cvalue, Some ival
+
+let () =
+ register_value_reduction
+ (Main_values.CVal.key, Main_values.Interval.key, reduce_apron_itv)
+
+module Reduce (Value : Abstract.Value.External) = struct
+ include Value
-(* -------------------------------------------------------------------------- *)
-(* Traces *)
-(* -------------------------------------------------------------------------- *)
+ let make_reduction acc (R (key1, key2, f)) =
+ match Value.get key1, Value.get key2 with
+ | Some get1, Some get2 ->
+ let set1 = Value.set key1
+ and set2 = Value.set key2 in
+ let reduce v = let v1, v2 = f (get1 v) (get2 v) in set1 v1 (set2 v2 v) in
+ reduce :: acc
+ | _, _ -> acc
+
+ let reduce =
+ let list = List.fold_left make_reduction [] !value_reduced_product in
+ fun v -> List.fold_left (fun v reduce -> reduce v) v list
+end
-let add_traces =
- add_standard_domain (module Traces_domain.D)
+(* --- Final hook ----------------------------------------------------------- *)
-(* -------------------------------------------------------------------------- *)
-(* Printer *)
-(* -------------------------------------------------------------------------- *)
+let final_hooks = ref []
-let add_printer =
- add_standard_domain (module Printer_domain)
+let register_hook f =
+ final_hooks := f :: !final_hooks
-(* -------------------------------------------------------------------------- *)
-(* Build Abstractions *)
-(* -------------------------------------------------------------------------- *)
+let apply_final_hooks abstractions =
+ List.fold_left (fun acc f -> f acc) abstractions !final_hooks
-let build_abstractions config =
- let value = build_value config in
- let module V = (val value : V) in
- let abstractions =
- match V.structure with
- | Structure.Key_Value.Leaf key
- when Structure.Key_Value.equal key Main_values.cvalue_key ->
- default_root_abstraction config
- | _ -> build_root_abstraction config value
- in
- let abstractions =
- if config.apron_oct
- then add_apron_domain abstractions (module Apron_domain.Octagon)
- else abstractions
- in
- let abstractions =
- if config.apron_box
- then add_apron_domain abstractions (module Apron_domain.Box)
- else abstractions
- in
- let abstractions =
- if config.polka_loose
- then add_apron_domain abstractions (module Apron_domain.Polka_Loose)
- else abstractions
- in
- let abstractions =
- if config.polka_strict
- then add_apron_domain abstractions (module Apron_domain.Polka_Strict)
- else abstractions
- in
- let abstractions =
- if config.polka_equalities
- then add_apron_domain abstractions (module Apron_domain.Polka_Equalities)
- else abstractions
- in
- let module A = (val abstractions : Abstract) in
- let abstractions =
- if config.equalities
- then add_equalities (module A)
- else abstractions
- in
- let abstractions =
- if config.symbolic_locs
- then add_symbolic_locs abstractions
- else abstractions
- in
- let abstractions =
- if config.bitwise
- then add_offsm abstractions
- else abstractions
- in
- let abstractions =
- if config.gauges
- then add_gauges abstractions
- else abstractions
- in
- let abstractions =
- if config.inout
- then add_inout abstractions
- else abstractions
- in
- let abstractions =
- if config.signs
- then add_signs abstractions
- else abstractions
- in
- let abstractions =
- if config.numerors
- then add_errors abstractions
- else abstractions
- in
- let abstractions =
- if config.printer
- then add_printer abstractions
- else abstractions
- in
- let abstractions =
- if config.traces
- then add_traces abstractions
- else abstractions
- in
- let abstractions = add_dynamic_abstractions abstractions in
- abstractions
+(* --- Building abstractions ------------------------------------------------ *)
+module Open (Acc: Acc) : S = struct
+ module Val = Reduce (Acc.Val)
+ module Loc = struct
+ include Acc.Loc
+ include Structure.Open (Abstract.Location)
+ (struct include Acc.Loc type t = location end)
+ end
+ module Dom = struct
+ include Acc.Dom
+ include Structure.Open (Abstract.Domain) (Acc.Dom)
-(* Add the reduce function to the value module. *)
-module Reduce (Value : Abstract_value.External) = struct
+ let get_cvalue = match get Cvalue_domain.State.key with
+ | None -> None
+ | Some get -> Some (fun s -> fst (get s))
- include Value
+ let get_cvalue_or_top = match get Cvalue_domain.State.key with
+ | None -> fun _ -> Cvalue.Model.top
+ | Some get -> fun s -> fst (get s)
- (* When the value abstraction contains both a cvalue and an interval
- component (coming currently from an Apron domain), reduce them from each
- 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
- | 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
- fun t ->
- match get_interval t with
- | None -> begin
- let cvalue = get_cvalue t in
- try
- let ival = Cvalue.V.project_ival cvalue in
- set_interval (Some ival) t
- with Cvalue.V.Not_based_on_null -> t
- end
- | Some ival ->
- let cvalue = get_cvalue t in
- try
- let ival' = Cvalue.V.project_ival cvalue in
- (match ival' with
- | Ival.Float _ -> raise Cvalue.V.Not_based_on_null
- | _ -> ());
- let reduced_ival = Ival.narrow ival ival' in
- let cvalue = Cvalue.V.inject_ival reduced_ival in
- set_interval (Some reduced_ival) (set_cvalue cvalue t)
- with Cvalue.V.Not_based_on_null -> t
- end
- | _, _ -> fun x -> x
-
- let reduce_error = Numerors_domain.reduce_error (module Value)
-
- let reduce t = reduce_apron_itv (reduce_error t)
+ let get_cvalue_or_bottom = function
+ | `Bottom -> Cvalue.Model.bottom
+ | `Value state -> get_cvalue_or_top state
+ end
end
-let open_abstractions abstraction =
- let module Abstract = (val abstraction : Abstract) in
- let module Val = Reduce (Abstract.Val) in
- let module Loc = struct
- include Abstract.Loc
- include Structure.Open
- (Structure.Key_Location)
- (struct include Abstract.Loc type t = location end)
- end in
- let module Domain = struct
- include Abstract.Dom
- include Structure.Open (Structure.Key_Domain) (Abstract.Dom)
- end in
+module CVal = Leaf_Value (Main_values.CVal)
+
+let unit_acc (module Value: Abstract.Value.External) =
+ let loc : (module internal_loc with type value = Value.t) =
+ match Abstract.Value.eq_structure Value.structure CVal.structure with
+ | Some Structure.Eq -> (module Leaf_Location (Main_locations.PLoc))
+ | _ ->
+ let module Struct = struct
+ type v = Cvalue.V.t
+ let s = Single (module Main_values.CVal)
+ end in
+ let module Conv = Internal_Value.Convert (Value) (Struct) in
+ (module Location_lift.Make (Main_locations.PLoc) (Conv))
+ in
(module struct
- module Val = Val
- module Loc = Loc
- module Dom = Domain
- end : S)
+ module Val = Value
+ module Loc = (val loc)
+ module Dom = Unit_domain.Make (Val) (Loc)
+ end : Acc)
+
+let build_abstractions config =
+ let initial_value : (module Abstract.Value.Internal) =
+ if Config.mem Config.bitwise config
+ then (module Offsm_value.CvalueOffsm)
+ else (module CVal)
+ in
+ let value = Internal_Value.build_values config initial_value in
+ let acc = unit_acc value in
+ build_domain config acc
+let configure = Config.configure
let make config =
let abstractions = build_abstractions config in
- open_abstractions abstractions
-
-
-(* -------------------------------------------------------------------------- *)
-(* Default and Legacy Abstractions *)
-(* -------------------------------------------------------------------------- *)
-
-module Legacy = (val make legacy_config)
-module Default = (val make default_config)
-
-
+ let abstractions = (module Open (val abstractions): S) in
+ apply_final_hooks abstractions
-(*
-Local Variables:
-compile-command: "make -C ../../../.."
-End:
-*)
+module Default = (val make Config.default)
+module Legacy = (val make Config.legacy)
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index 996f0aaa0392ad6ab229d4cd1f1429419530bd06..4c2909dbb757e52966e0dab66ec42e86473b87b2 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -20,55 +20,90 @@
(* *)
(**************************************************************************)
-(** Constructions of the abstractions used by Eva. *)
-
-(** Configuration of the abstract domain. *)
-type config = {
- cvalue : bool;
- equalities : bool;
- symbolic_locs : bool;
- bitwise : bool;
- gauges: bool;
- apron_oct : bool;
- apron_box : bool;
- polka_loose : bool;
- polka_strict : bool;
- polka_equalities : bool;
- inout: bool;
- signs: bool;
- printer: bool;
- numerors: bool;
- traces: bool;
-}
-
-(** Default configuration of Eva. *)
-val default_config : config
-
-(** Legacy configuration of Eva, with only the cvalue domain enabled.
- May be the default config as well. *)
-val legacy_config : config
-
-(** Build a configuration according to the analysis parameters. *)
-val configure : unit -> config
+(** Registration and building of the analysis abstractions. *)
+(** {2 Registration of abstractions.} *)
+(** Dynamic registration of the abstractions to be used in an Eva analysis:
+ - value abstractions, detailled in the {Abstract_value} signature;
+ - location abstractions, detailled in the {Abstract_location} signature;
+ - state abstractions, or abstract domains, detailled in {Abstract_domain}.
+*)
+
+(** Module types of value abstractions: either a single leaf module, or
+ a compound of several modules described by a structure. *)
+type 'v value =
+ | Single of (module Abstract_value.Leaf with type t = 'v)
+ | Struct of 'v Abstract.Value.structure
+
+(** For the moment, all domains must use [precise_loc] as their location
+ abstraction, and no new location abstraction can be registered for an
+ analysis.
+ If you need to build a new location abstraction, please contact us. *)
+type precise_loc = Precise_locs.precise_location
+
+(** Module type of a leaf domain over precise_loc abstraction. *)
+module type leaf_domain = Abstract_domain.Leaf with type location = precise_loc
+
+(** Module type of a functor building a leaf domain from a value abstraction.
+ The resulting domain must use the input value as value abstraction. *)
+module type domain_functor = functor
+ (Value: Abstract.Value.External) -> (leaf_domain with type value = Value.t)
+
+(** Type of domain to be registered: either a leaf module with ['v] as value
+ abstraction, or a functor building a domain from any value abstraction. *)
+type 'v domain =
+ | Domain: (module leaf_domain with type value = 'v) -> 'v domain
+ | Functor: (module domain_functor) -> _ domain
+
+(** Abstraction to be registered. The name of each abstraction must be unique.
+ The priority can be any integer; domains with higher priority are always
+ processed first. The domains currently provided by Eva have priority ranging
+ between 1 and 19, so a priority of 0 (respectively 20) ensures that a new
+ domain is processed after (respectively before) the classic Eva domains. *)
+type 'v abstraction =
+ { name: string; (** Name of the abstraction. Must be unique. *)
+ priority: int; (** Domains with higher priority are processed first. *)
+ values: 'v value; (** The value abstraction. *)
+ domain: 'v domain; (** The domain over the value abstraction. *)
+ }
+
+(** Register an abstraction. The abstraction is used in an Eva analysis only if
+ [enable ()] returns true at the start of the analysis. *)
+val register: enable:(unit -> bool) -> 'v abstraction -> unit
+
+(** Register a dynamic abstraction: the abstraction is built by applying
+ [make (configure ())] at the start of each analysis. *)
+val dynamic_register:
+ configure:(unit -> 'a option) -> make:('a -> 'v abstraction) -> unit
+
+(** Value reduced product between two value abstractions, identified by their
+ keys. *)
+type ('a, 'b) value_reduced_product =
+ 'a Abstract.Value.key * 'b Abstract.Value.key * ('a -> 'b -> 'a * 'b)
+
+(** Register a reduction function for a value reduced product. *)
+val register_value_reduction: ('a, 'b) value_reduced_product -> unit
+
+
+(** {2 Types used in the engine.} *)
+
+(** The external signature of value abstractions, plus the reduction function
+ of the reduced product. *)
module type Value = sig
- include Abstract_value.External
+ include Abstract.Value.External
val reduce : t -> t
end
-(** Types of the abstractions of the analysis: value, location and state
- abstractions.*)
+(** The three abstractions used in an Eva analysis. *)
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
-(** Module gathering:
- - the analysis abstractions: value, location and state abstractions;
- - the evaluation functions for these abstractions. *)
+(** The three abstractions plus an evaluation engine for these abstractions. *)
module type Eva = sig
include S
module Eval: Evaluation.S with type state = Dom.t
@@ -77,26 +112,45 @@ module type Eva = sig
and type origin = Dom.origin
end
-(** Type of abstractions that use the builtin types for values and locations *)
-module type Standard_abstraction = Abstract_domain.Internal
- with type value = Cvalue.V.t
- and type location = Precise_locs.precise_location
+(** Register a hook modifying the three abstractions after their building by
+ the engine, before the start of each analysis. *)
+val register_hook: ((module S) -> (module S)) -> unit
-val register_dynamic_abstraction: (module Standard_abstraction) -> unit
+(** {2 Configuration of an analysis.} *)
-(** Builds the abstractions according to a configuration. *)
-val make : config -> (module S)
+(** Configuration defining the abstractions to be used in an analysis. *)
+module Config : sig
+ (** Flag for an abstraction. *)
+ type flag = Flag: 'v abstraction -> flag
+ (** A configuration is a set of flags, i.e. a set of enabled abstractions. *)
+ include Set.S with type elt = flag
-(** Two abstractions are instantiated at compile time: default and legacy
- (which may be the same). *)
+ (** Flags for the standard domains currently provided in Eva. *)
-module Legacy : S
-module Default : S
+ val cvalue: flag
+ val equality: flag
+ val symbolic_locations: flag
+ val gauges: flag
+ val bitwise: flag
+ val inout: flag
+ val sign: flag
+ val traces: flag
+ val printer: flag
+ val default: t (** The default configuration of Eva. *)
+ val legacy: t (** The configuration corresponding to the old "Value" analysis,
+ with only the cvalue domain enabled. *)
+end
-(*
-Local Variables:
-compile-command: "make -C ../../../.."
-End:
-*)
+(** Creates the configuration according to the analysis parameters. *)
+val configure: unit -> Config.t
+
+(** Builds the abstractions according to a configuration. *)
+val make: Config.t -> (module S)
+
+(** Two abstractions are instantiated at compile time for the default and legacy
+ configurations (which may be the same). *)
+
+module Legacy : S
+module Default : S
diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index fd3cf68003bf90f49e026ed3028488d18cf19c72..ee1b5680eeac44e2ad88489209edf6dbbb7fceb6 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -102,7 +102,7 @@ module Legacy = Make (Abstractions.Legacy)
module Default =
(val
- (if Abstractions.default_config = Abstractions.legacy_config
+ (if Abstractions.Config.(equal default legacy)
then (module Legacy)
else (module Make (Abstractions.Default)))
: Analyzer)
@@ -112,7 +112,7 @@ module Default =
the parameters of Eva regarding the abstractions used in the analysis) and
the current Analyzer module. *)
let ref_analyzer =
- ref (Abstractions.default_config, (module Default : Analyzer))
+ ref (Abstractions.Config.default, (module Default : Analyzer))
(* Returns the current Analyzer module. *)
let current_analyzer () = (module (val (snd !ref_analyzer)): S)
@@ -133,14 +133,14 @@ let set_current_analyzer config (analyzer: (module Analyzer)) =
let cvalue_initial_state () =
let module A = (val snd !ref_analyzer) in
let _, lib_entry = Globals.entry_point () in
- Cvalue_domain.extract A.Dom.get (A.initial_state ~lib_entry)
+ A.Dom.get_cvalue_or_bottom (A.initial_state ~lib_entry)
(* Builds the Analyzer module corresponding to a given configuration,
and sets it as the current analyzer. *)
let make_analyzer config =
let analyzer =
- if config = Abstractions.legacy_config then (module Legacy: Analyzer)
- else if config = Abstractions.default_config then (module Default)
+ if Abstractions.Config.(equal config legacy) then (module Legacy: Analyzer)
+ else if Abstractions.Config.(equal config default) then (module Default)
else
let module Abstract = (val Abstractions.make config) in
let module Analyzer = Make (Abstract) in
@@ -153,7 +153,7 @@ let reset_analyzer () =
let config = Abstractions.configure () in
(* If the configuration has not changed, do not reset the Analyzer but uses
the reference instead. *)
- if config <> fst !ref_analyzer
+ if not (Abstractions.Config.equal config (fst !ref_analyzer))
then make_analyzer config
(* Builds the analyzer if needed, and run the analysis. *)
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index d265352833e4dbbf7b2d88c7ed8483849670c57d..21a9876322a1e7dfe27fdc0a8c9d0dc8803ce778 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -148,18 +148,13 @@ module Make (Abstract: Abstractions.Eva) = struct
let initial_state = Init.initial_state
- let get_cvalue =
- match Abstract.Dom.get Cvalue_domain.key with
- | None -> fun _ -> Cvalue.Model.top
- | Some get -> fun state -> 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
@@ -191,7 +186,7 @@ module Make (Abstract: Abstractions.Eva) = struct
then `Spec (Annotations.funspec kf)
else `Def def
in
- let cvalue_state = get_cvalue state in
+ let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
let resulting_states, cacheable = match use_spec with
| `Spec spec ->
Db.Value.Call_Type_Value_Callbacks.apply
@@ -237,9 +232,9 @@ module Make (Abstract: Abstractions.Eva) = struct
in
call_result
| Some (states, i) ->
- let stack_with_call = Value_util.call_stack () in
- Db.Value.Call_Type_Value_Callbacks.apply
- (`Memexec, get_cvalue init_state, stack_with_call);
+ let stack = Value_util.call_stack () in
+ let cvalue = Abstract.Dom.get_cvalue_or_top init_state in
+ Db.Value.Call_Type_Value_Callbacks.apply (`Memexec, cvalue, stack);
(* Evaluate the preconditions of kf, to update the statuses
at this call. *)
let spec = Annotations.funspec call.kf in
@@ -300,7 +295,7 @@ module Make (Abstract: Abstractions.Eva) = struct
in
Locations.Location_Bytes.do_track_garbled_mix true;
let final_state = states >>- join_states in
- let cvalue_state = get_cvalue state in
+ let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
match final_state with
| `Bottom ->
let cs = Value_util.call_stack () in
@@ -312,17 +307,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
@@ -330,7 +324,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let store_initial_state kf init_state =
Abstract.Dom.Store.register_initial_state (Value_util.call_stack ()) init_state;
- let cvalue_state = get_cvalue init_state in
+ let cvalue_state = Abstract.Dom.get_cvalue_or_top init_state in
Db.Value.Call_Value_Callbacks.apply (cvalue_state, [kf, Kglobal])
let compute kf init_state =
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..fd124a687b6a27f5c823130697fcad9ca2042a7a 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,10 +270,9 @@ 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
- | None ->
- Value_parameters.abort "Function Db.Value.fun_set_args cannot be used \
- without the Cvalue domain"
+ match Domain.get_cvalue with
+ | None -> Value_parameters.abort "Function Db.Value.fun_set_args cannot be \
+ used without the Cvalue domain"
| Some get_cvalue ->
let formals = Kernel_function.get_formals kf in
if (List.length formals) <> List.length actuals then
@@ -286,8 +285,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_state, Locals_scoping.bottom ()) state
let add_main_formals kf state =
match Db.Value.fun_get_args () with
@@ -354,7 +353,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_state, Locals_scoping.bottom () in
+ `Value (Domain.set Cvalue_domain.State.key cvalue_state Domain.top)
else `Bottom
let initial_state ~lib_entry =
@@ -363,7 +364,7 @@ module Make
else global_state ~lib_entry
let print_initial_cvalue_state state =
- let cvalue_state = Cvalue_domain.extract Domain.get state in
+ let cvalue_state = Domain.get_cvalue_or_bottom state in
(* Do not show variables from the frama-c libc specifications. *)
let print_base base =
try
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..bae4fbcc7b35ec5ec246816cd8ab55f9f6bcfe47 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -433,9 +433,7 @@ module Make_Dataflow
edge_info.fireable <- true;
flow
- let get_cvalue = Domain.get Cvalue_domain.key
- let gather_cvalues states =
- match get_cvalue with
+ let gather_cvalues states = match Domain.get_cvalue with
| Some get -> List.map get states
| None -> []
@@ -633,9 +631,6 @@ module Make_Dataflow
G.iter_edges_e fill graph;
Db.Value.merge_conditions table
- let extract_cvalue (state : state) : 'a =
- Cvalue_domain.extract Domain.get (`Value state)
-
let is_instr s = match s.skind with Instr _ -> true | _ -> false
let states_after_stmt states_before states_after =
@@ -676,7 +671,7 @@ module Make_Dataflow
then VertexTable.memo merged_states v get_smashed_store
else `Bottom
and lift_to_cvalues table =
- StmtTable.map (fun _ s -> extract_cvalue s) (Lazy.force table)
+ StmtTable.map (fun _ s -> Domain.get_cvalue_or_top s) (Lazy.force table)
in
let merged_pre_states = lazy
(StmtTable.map' (fun s (v,_) -> get_merged_states ~all:true s v) automaton.stmt_table)
@@ -691,7 +686,7 @@ module Make_Dataflow
(StmtTable.map (fun _stmt (v,_) ->
let store = get_vertex_store v in
let states = Partition.expanded store in
- List.map (fun x -> extract_cvalue x) states)
+ List.map (fun x -> Domain.get_cvalue_or_top x) states)
automaton.stmt_table)
in
let merged_pre_cvalues = lazy (lift_to_cvalues merged_pre_states)
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..e15091974e5c8cdc7de19f10e67d858ec9a6babc 100644
--- a/src/plugins/value/engine/transfer_specification.ml
+++ b/src/plugins/value/engine/transfer_specification.ml
@@ -227,16 +227,13 @@ 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
- | None -> fun _ -> Cvalue.Model.top
- | Some get -> get
- let make_env state = Eval_terms.env_assigns (get_cvalue_state state)
+ let make_env state = Eval_terms.env_assigns (Domain.get_cvalue_or_top state)
let is_result = function
| Assigns (term, _)
@@ -299,7 +296,7 @@ module Make
end
in
let check_one_state state =
- let cvalue_state = get_cvalue_state state in
+ let cvalue_state = Domain.get_cvalue_or_top state in
List.iter (check_one_assign cvalue_state) assigns
in
States.iter check_one_state states
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index e7be6f8f5827d5e2172721c25c0a7529cc7e321a..514e4ea789c0db62b5c02857c3417d66e9128ee5 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,10 +559,6 @@ module Make (Abstract: Abstractions.Eva) = struct
(* ----------------- show_each and dump_each directives ------------------- *)
- let extract_cvalue = match Domain.get Cvalue_domain.key with
- | None -> fun _ -> Cvalue.Model.top
- | Some get -> get
-
(* 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
domain is not a product, this needs to be done here. *)
@@ -609,7 +605,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, Location.get Main_locations.PLoc.key with
| None, _ | _, None ->
fun fmt _ _ -> Format.fprintf fmt "%s" (Unicode.top_string ())
| Some get_cvalue, Some get_ploc ->
@@ -621,9 +617,7 @@ module Make (Abstract: Abstractions.Eva) = struct
let offsm =
fst (Eval.lvaluate ~for_writing:false state lval)
>>- fun (_, loc, _) ->
- let ploc = get_ploc loc
- and cvalue_state = get_cvalue state in
- Eval_op.offsetmap_of_loc ploc cvalue_state
+ Eval_op.offsetmap_of_loc (get_ploc loc) (get_cvalue state)
in
let typ = Cil.typeOf expr in
(Bottom.pretty (Eval_op.pretty_offsetmap typ)) fmt offsm
@@ -634,7 +628,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 ->
@@ -707,7 +701,7 @@ module Make (Abstract: Abstractions.Eva) = struct
{Cvalue_transfer.start_call}. *)
let apply_cvalue_callback kf ki_call state =
let stack_with_call = (kf, ki_call) :: Value_util.call_stack () in
- let cvalue_state = extract_cvalue state in
+ let cvalue_state = Domain.get_cvalue_or_top state in
Db.Value.Call_Value_Callbacks.apply (cvalue_state, stack_with_call);
Db.Value.merge_initial_state (Value_util.call_stack ()) cvalue_state;
let result =
diff --git a/src/plugins/value/gui_files/gui_eval.ml b/src/plugins/value/gui_files/gui_eval.ml
index 108079350d90481f0a0ec71c200f2a62b0d93443..8239f3974fe81a150ebdeaa53a488ec29935eb31 100644
--- a/src/plugins/value/gui_files/gui_eval.ml
+++ b/src/plugins/value/gui_files/gui_eval.ml
@@ -143,13 +143,8 @@ module Make (X: Analysis.S) = struct
module Analysis = X
- let get_cvalue_state =
- match X.Dom.get Cvalue_domain.key with
- | None -> fun _ -> Cvalue.Model.top
- | Some get -> fun state -> 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
@@ -210,7 +205,7 @@ module Make (X: Analysis.S) = struct
let lval_to_offsetmap state lv =
let loc, alarms = X.eval_lval_to_loc state lv in
let ok = Alarmset.is_empty alarms in
- let state = get_cvalue_state state in
+ let state = X.Dom.get_cvalue_or_top state in
let aux loc (acc_res, acc_ok) =
let res, ok =
match lv with (* catch simplest pattern *)
@@ -273,7 +268,7 @@ module Make (X: Analysis.S) = struct
}
let null_to_offsetmap state (_:unit) =
- let state = get_cvalue_state state in
+ let state = X.Dom.get_cvalue_or_top state in
match Cvalue.Model.find_base_or_default Base.null state with
| `Bottom -> GO_InvalidLoc, false, false
| `Top -> GO_Top, false, false
@@ -335,17 +330,17 @@ module Make (X: Analysis.S) = struct
let env_here kf here callstack =
let pre = pre_kf kf callstack in
- let here = get_cvalue_state here in
+ let here = X.Dom.get_cvalue_or_top here in
let c_labels = Eval_annots.c_labels kf callstack in
Eval_terms.env_annot ~c_labels ~pre ~here ()
let env_pre _kf here _callstack =
- let here = get_cvalue_state here in
+ let here = X.Dom.get_cvalue_or_top here in
Eval_terms.env_pre_f ~pre:here ()
let env_post kf post callstack =
let pre = pre_kf kf callstack in
- let post = get_cvalue_state post in
+ let post = X.Dom.get_cvalue_or_top post in
let result =
if !Db.Value.use_spec_instead_of_definition kf then
None
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..f8617e5ad4eb5c0b021ed543a5102af398231f72 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, (module Main_values.CVal))
+end
+
+module Val = struct
+ include CVal
+ include Structure.Open (Abstract.Value) (CVal)
let reduce t = t
end
@@ -183,6 +188,8 @@ module Eva =
module Transfer = Cvalue_domain.State.Transfer (Eva.Valuation)
+let inject_cvalue state = state, Locals_scoping.bottom ()
+
let bot_value = function
| `Bottom -> Cvalue.V.bottom
| `Value v -> v
@@ -192,7 +199,7 @@ let bot_state = function
| `Value s -> s
let update valuation state =
- bot_state (Transfer.update valuation state >>-: Cvalue_domain.project)
+ bot_state (Transfer.update valuation state >>-: fst)
let rec eval_deps state e =
match e.enode with
@@ -231,7 +238,7 @@ let notify_opt with_alarms alarms =
Extlib.may (fun mode -> Alarmset.notify mode alarms) with_alarms
let eval_expr_with_valuation ?with_alarms deps state expr=
- let state = Cvalue_domain.inject state in
+ let state = inject_cvalue state in
let deps = match deps with
| None -> None
| Some deps ->
@@ -251,7 +258,7 @@ let eval_expr_with_valuation ?with_alarms deps state expr=
module Eval = struct
let eval_expr ?with_alarms state expr =
- let state = Cvalue_domain.inject state in
+ let state = inject_cvalue state in
let eval, alarms = Eva.evaluate ~reduction:false state expr in
notify_opt with_alarms alarms;
bot_value (eval >>-: snd)
@@ -273,7 +280,7 @@ module Eval = struct
let reduce_by_cond state expr positive =
- let state = Cvalue_domain.inject state in
+ let state = inject_cvalue state in
let eval, _alarms =
Eva.reduce state expr positive
in
@@ -284,7 +291,7 @@ module Eval = struct
if not (Cvalue.Model.is_reachable state)
then state, deps, Precise_locs.loc_bottom, (Cil.typeOfLval lval)
else
- let state = Cvalue_domain.inject state in
+ let state = inject_cvalue state in
let deps = match deps with
| None -> None
| Some deps ->
@@ -333,7 +340,7 @@ module Eval = struct
let resolv_func_vinfo ?with_alarms deps state funcexp =
let open Cil_types in
- let state = Cvalue_domain.inject state in
+ let state = inject_cvalue state in
let deps = match funcexp.enode with
| Lval (Var _, NoOffset) -> deps
| Lval (Mem v, _) ->
diff --git a/src/plugins/value/utils/abstract.ml b/src/plugins/value/utils/abstract.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e5153a5241bcbd0682795eb13ee79fbe48976499
--- /dev/null
+++ b/src/plugins/value/utils/abstract.ml
@@ -0,0 +1,94 @@
+(**************************************************************************)
+(* *)
+(* 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
+
+ module V = struct
+ type 'a t = (module Abstract_value.S with type t = 'a)
+ end
+
+ include Structure.Shape (Structure.Key_Value) (V)
+
+ 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
+
+ module L = struct
+ type 'a t = (module Abstract_location.S with type location = 'a)
+ end
+
+ include Structure.Shape (Structure.Key_Location) (L)
+
+ 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
+
+ module D = struct
+ type 'a t = (module Abstract_domain.Internal with type state = 'a)
+ end
+
+ include Structure.Shape (Structure.Key_Domain) (D)
+
+ 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
+
+ val get_cvalue: (t -> Cvalue.Model.t) option
+ val get_cvalue_or_top: t -> Cvalue.Model.t
+ val get_cvalue_or_bottom: t Bottom.or_bottom -> Cvalue.Model.t
+ end
+end
diff --git a/src/plugins/value/utils/abstract.mli b/src/plugins/value/utils/abstract.mli
new file mode 100644
index 0000000000000000000000000000000000000000..3e797f8eddba95cddfa69765f3097ac7a3081ffa
--- /dev/null
+++ b/src/plugins/value/utils/abstract.mli
@@ -0,0 +1,118 @@
+(**************************************************************************)
+(* *)
+(* 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 data = (module Abstract_value.S with type t = 'a)
+
+ 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 data = (module Abstract_location.S with type location = 'a)
+
+ 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 data = (module Abstract_domain.Internal with type state = 'a)
+
+ 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
+
+ (** Special accessors for the main cvalue domain. *)
+ val get_cvalue: (t -> Cvalue.Model.t) option
+ val get_cvalue_or_top: t -> Cvalue.Model.t
+ val get_cvalue_or_bottom: t Bottom.or_bottom -> Cvalue.Model.t
+ end
+end
diff --git a/src/plugins/value/utils/structure.ml b/src/plugins/value/utils/structure.ml
index 30f4b3c38637a85fc888f4e7541ed9cf7b89f51d..c6dd04ab1c1280da7ee2927723be8bf6493c7f85 100644
--- a/src/plugins/value/utils/structure.ml
+++ b/src/plugins/value/utils/structure.ml
@@ -24,32 +24,22 @@
type (_,_) eq = Eq : ('a,'a) eq
module type Key = sig
- type 'a k
-
- val create_key: string -> 'a k
- val eq_type : 'a k -> 'b k -> ('a, 'b) eq option
+ type 'a key
- val print: 'a k Pretty_utils.formatter
- val compare: 'a k -> 'b k -> int
- val equal: 'a k -> 'b k -> bool
- val hash : 'a k -> int
- val tag: 'a k -> int
-end
+ val create_key: string -> 'a key
+ val eq_type : 'a key -> 'b key -> ('a, 'b) eq option
-module type Shape = sig
- include Key
-
- type 'a structure =
- | Void : 'a structure
- | Leaf : 'a k -> 'a structure
- | Node : 'a structure * 'b structure -> ('a * 'b) structure
+ val print: 'a key Pretty_utils.formatter
+ val compare: 'a key -> 'b key -> int
+ val equal: 'a key -> 'b key -> bool
+ val hash : 'a key -> int
+ val tag: 'a key -> int
end
-
module Make (X : sig end) = struct
- type 'a k = { tag: int;
- name: string }
+ type 'a key = { tag: int;
+ name: string }
let c = ref (-1)
let id () = incr c; !c
@@ -57,7 +47,7 @@ module Make (X : sig end) = struct
let create_key name = { tag = id (); name }
let equal x y = x.tag = y.tag
- let eq_type : type a b. a k -> b k -> (a,b) eq option = fun a b ->
+ let eq_type : type a b. a key -> b key -> (a,b) eq option = fun a b ->
if equal a b
then Some ((Obj.magic (Eq : (a,a) eq)) : (a,b) eq)
else None
@@ -67,17 +57,46 @@ module Make (X : sig end) = struct
let tag x = x.tag
let print fmt x = Format.pp_print_string fmt x.name
-
- type 'a structure =
- | Void : 'a structure
- | Leaf : 'a k -> 'a structure
- | Node : 'a structure * 'b structure -> ('a * 'b) structure
end
module Key_Value = Make (struct end)
module Key_Location = Make (struct end)
module Key_Domain = Make (struct end)
+module type Shape = sig
+ include Key
+ type 'a data
+
+ type 'a structure =
+ | Unit : unit structure
+ | Leaf : 'a key * 'a data -> 'a structure
+ | Node : 'a structure * 'b structure -> ('a * 'b) structure
+
+ val eq_structure: 'a structure -> 'b structure -> ('a, 'b) eq option
+end
+
+module Shape (Key: Key) (Data: sig type 'a t end) = struct
+ include Key
+ type 'a data = 'a Data.t
+
+ type 'a structure =
+ | Unit : unit structure
+ | Leaf : 'a key * 'a data -> 'a structure
+ | Node : 'a structure * 'b structure -> ('a * 'b) structure
+
+ let rec eq_structure : type a b. a structure -> b structure -> (a, b) eq option
+ = fun a b ->
+ match a, b with
+ | Leaf (key1, _), Leaf (key2, _) -> Key.eq_type key1 key2
+ | Node (l1, r1), Node (l2, r2) ->
+ begin
+ match eq_structure l1 l2, eq_structure r1 r2 with
+ | Some Eq, Some Eq -> Some Eq
+ | _, _ -> None
+ end
+ | Unit, Unit -> Some Eq
+ | _, _ -> None
+end
module type Internal = sig
type t
@@ -93,7 +112,6 @@ module type External = sig
val set : 'a key -> 'a -> t -> t
end
-
module Open
(Shape : Shape)
(M : sig type t val structure : t Shape.structure end)
@@ -110,15 +128,15 @@ module Open
open Shape
- let rec mem : type a. 'v Shape.k -> a structure -> bool = fun key -> function
- | Void -> false
- | Leaf k -> Shape.equal key k
+ let rec mem : type a. 'v Shape.key -> a structure -> bool = fun key -> function
+ | Unit -> false
+ | Leaf (k, _) -> Shape.equal key k
| Node (left, right) -> mem key left || mem key right
let mem key = mem key M.structure
- type ('a, 'b) get = 'b Shape.k * ('a -> 'b)
+ type ('a, 'b) get = 'b Shape.key * ('a -> 'b)
type 'a getter = Get : ('a, 'b) get -> 'a getter
@@ -130,15 +148,15 @@ module Open
let lift_get f (Get (key, get)) = Get (key, fun t -> get (f t))
let rec compute_getters : type a. a structure -> (a getter) KMap.t = function
- | Void -> KMap.empty
- | Leaf key -> KMap.singleton key (Get (key, fun (t : a) -> t))
+ | Unit -> KMap.empty
+ | Leaf (key, _) -> KMap.singleton key (Get (key, fun (t : a) -> t))
| Node (left, right) ->
let l = compute_getters left and r = compute_getters right in
let l = KMap.map (lift_get fst) l and r = KMap.map (lift_get snd) r in
KMap.merge merge l r
let getters = compute_getters M.structure
- let get (type a) (key: a Shape.k) : (M.t -> a) option =
+ let get (type a) (key: a Shape.key) : (M.t -> a) option =
match KMap.find key getters with
| None -> None
| Some (Get (k, get)) -> match Shape.eq_type key k with
@@ -146,15 +164,15 @@ module Open
| Some Eq -> Some get
- type ('a, 'b) set = 'b Shape.k * ('b -> 'a -> 'a)
+ type ('a, 'b) set = 'b Shape.key * ('b -> 'a -> 'a)
type 'a setter = Set : ('a, 'b) set -> 'a setter
let lift_set f (Set (key, set)) = Set (key, fun v b -> f (fun a -> set v a) b)
let rec compute_setters : type a. a structure -> (a setter) KMap.t = function
- | Void -> KMap.empty
- | Leaf key -> KMap.singleton key (Set (key, fun v _t -> v))
+ | Unit -> KMap.empty
+ | Leaf (key, _) -> KMap.singleton key (Set (key, fun v _t -> v))
| Node (left, right) ->
let l = compute_setters left and r = compute_setters right in
let l = KMap.map (lift_set (fun set (l, r) -> set l, r)) l
@@ -162,7 +180,7 @@ module Open
KMap.merge merge l r
let setters = compute_setters M.structure
- let set (type a) (key: a Shape.k) : (a -> M.t -> M.t) =
+ let set (type a) (key: a Shape.key) : (a -> M.t -> M.t) =
match KMap.find key setters with
| None -> fun _ t -> t
| Some (Set (k, set)) -> match Shape.eq_type key k with
diff --git a/src/plugins/value/utils/structure.mli b/src/plugins/value/utils/structure.mli
index 9d52978f6930c2a52e2231c8bb41468ce4ca24e6..c04eb8cda7bb222f5b24d2bdfc1a63de1e6214f5 100644
--- a/src/plugins/value/utils/structure.mli
+++ b/src/plugins/value/utils/structure.mli
@@ -29,43 +29,48 @@ type (_,_) eq = Eq : ('a,'a) eq
(** Keys identifying datatypes. *)
module type Key = sig
- type 'a k
+ type 'a key
- val create_key: string -> 'a k
- val eq_type : 'a k -> 'b k -> ('a, 'b) eq option
+ val create_key: string -> 'a key
+ val eq_type : 'a key -> 'b key -> ('a, 'b) eq option
- val print: 'a k Pretty_utils.formatter
- val compare: 'a k -> 'b k -> int
- val equal: 'a k -> 'b k -> bool
- val hash : 'a k -> int
- val tag: 'a k -> int
+ val print: 'a key Pretty_utils.formatter
+ val compare: 'a key -> 'b key -> int
+ val equal: 'a key -> 'b key -> bool
+ val hash : 'a key -> int
+ val tag: 'a key -> int
end
+module Make (X : sig end) : Key
+
+(** Keys module for the abstract values of Eva. *)
+module Key_Value : Key
+
+(** Keys module for the abstract locations of Eva. *)
+module Key_Location : Key
+
+(** Keys module for the abstract domains of Eva. *)
+module Key_Domain : Key
+
(** A Key module with its structure type. *)
module type Shape = sig
include Key
+ type 'a data
(** The gadt, based on keys giving the type of each node.
Describes the internal structure of a data type.
Used internally to automatically generate efficient accessors of its nodes. *)
type 'a structure =
- | Void : 'a structure
- | Leaf : 'a k -> 'a structure
+ | Unit : unit structure
+ | Leaf : 'a key * 'a data -> 'a structure
| Node : 'a structure * 'b structure -> ('a * 'b) structure
-end
-module Make (X : sig end) : Shape
-
-
-(** Keys module for the abstract values of Eva. *)
-module Key_Value : Shape
-
-(** Keys module for the abstract locations of Eva. *)
-module Key_Location : Shape
-
-(** Keys module for the abstract domains of Eva. *)
-module Key_Domain : Shape
+ val eq_structure: 'a structure -> 'b structure -> ('a, 'b) eq option
+end
+module Shape (Key: Key) (Data: sig type 'a t end) :
+ Shape with type 'a key = 'a Key.key
+ and type 'a data = 'a Data.t
(** Internal view of the tree, with the structure. *)
module type Internal = sig
@@ -92,4 +97,4 @@ module Open
(Shape : Shape)
(Data : Internal with type 'a structure := 'a Shape.structure)
: External with type t := Data.t
- and type 'a key := 'a Shape.k
+ and type 'a key := 'a Shape.key
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 118115fa8b539e80b95d1a8c038cfc2ce675b067..1de1430a7c101b4894bd7aa0176476f575738ee8 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -77,6 +77,8 @@ let dkey_incompatible_states = register_category "incompatible-states"
let dkey_iterator = register_category "iterator"
let dkey_callbacks = register_category "callbacks"
let dkey_widening = register_category "widening"
+let dkey_experimental = register_category "experimental-ok"
+
let () =
let activate dkey = add_debug_keys dkey in
@@ -172,6 +174,18 @@ module BitwiseOffsmDomain = Domain_Parameter
let default = false
end)
+let numerors_available = ref false
+let register_numerors () = numerors_available := true
+
+let numerors_hook _ _ =
+ if not !numerors_available
+ then
+ abort
+ "The numerors domain has been requested but is not available,@ \
+ as Frama-C did not found the MPFR library. The analysis is aborted."
+ else if not (is_debug_key_enabled dkey_experimental) then
+ warning "The numerors domain is experimental.";
+
module NumerorsDomain = Domain_Parameter
(struct
let option_name = "-eva-numerors-domain"
@@ -180,16 +194,28 @@ module NumerorsDomain = Domain_Parameter
computations"
let default = false
end)
+let () = NumerorsDomain.add_set_hook numerors_hook
let apron_help = "Experimental binding of the numerical domains provided \
by the APRON library: http://apron.cri.ensmp.fr/library \n"
+let apron_available = ref false
+let register_apron () = apron_available := true
+
+let apron_hook _ _ =
+ if not !apron_available
+ then
+ abort "an Apron domain is requested but the apron binding is not available."
+ else if not (is_debug_key_enabled dkey_experimental) then
+ warning "The Apron domains binding is experimental.";
+
module ApronOctagon = Domain_Parameter
(struct
let option_name = "-eva-apron-oct"
let help = apron_help ^ "Use the octagon domain of apron."
let default = false
end)
+let () = ApronOctagon.add_set_hook apron_hook
module ApronBox = Domain_Parameter
(struct
@@ -197,6 +223,7 @@ module ApronBox = Domain_Parameter
let help = apron_help ^ "Use the box domain of apron."
let default = false
end)
+let () = ApronBox.add_set_hook apron_hook
module PolkaLoose = Domain_Parameter
(struct
@@ -204,6 +231,7 @@ module PolkaLoose = Domain_Parameter
let help = apron_help ^ "Use the loose polyhedra domain of apron."
let default = false
end)
+let () = PolkaLoose.add_set_hook apron_hook
module PolkaStrict = Domain_Parameter
(struct
@@ -211,6 +239,7 @@ module PolkaStrict = Domain_Parameter
let help = apron_help ^ "Use the strict polyhedra domain of apron."
let default = false
end)
+let () = PolkaStrict.add_set_hook apron_hook
module PolkaEqualities = Domain_Parameter
(struct
@@ -218,6 +247,7 @@ module PolkaEqualities = Domain_Parameter
let help = apron_help ^ "Use the linear equalities domain of apron."
let default = false
end)
+let () = PolkaEqualities.add_set_hook apron_hook
module InoutDomain = Domain_Parameter
(struct
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index dc958517ee46ca0c0430e3ee513b75662d9b88c9..3e0fb860496b052159093bf18d4239e97379081a 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -234,6 +234,11 @@ val dkey_callbacks : category
val dkey_widening : category
+(** Notifies that the binding to Apron domains is available. *)
+val register_apron: unit -> unit
+
+(** Notifies that the numerors domain is available. *)
+val register_numerors: unit -> unit
(*
Local Variables:
diff --git a/src/plugins/value/values/abstract_location.mli b/src/plugins/value/values/abstract_location.mli
index 2c7266aa87353cdcf86e012121bc23f026d2d010..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.k
-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 28fec80b0e53acad4535b0655b86601a5e0b690d..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.k
-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..f02568133bbbfd282a44abb8b20cf7f70f5e51af 100644
--- a/src/plugins/value/values/location_lift.ml
+++ b/src/plugins/value/values/location_lift.ml
@@ -32,17 +32,19 @@ module type Conversion = sig
end
module Make
- (Loc: Abstract_location.Internal)
+ (Loc: Abstract_location.Leaf)
(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)
type value = Convert.extended_value
+ let structure = Abstract.Location.Leaf (Loc.key, (module Loc))
+
(* Now lift the functions that contain {!value} in their type. *)
let to_value loc = Convert.extend_val (Loc.to_value loc)
diff --git a/src/plugins/value/values/location_lift.mli b/src/plugins/value/values/location_lift.mli
index 1eb2d98d38c1da61d05b0891f7e6f88cda650e87..cd5b46cafaf7143981d76060b05f4be48b656f4d 100644
--- a/src/plugins/value/values/location_lift.mli
+++ b/src/plugins/value/values/location_lift.mli
@@ -30,9 +30,9 @@ module type Conversion = sig
end
module Make
- (Loc: Abstract_location.Internal)
+ (Loc: Abstract_location.Leaf)
(Convert : Conversion with type internal_value := Loc.value)
- : Abstract_location.Internal with type location = Loc.location
+ : Abstract.Location.Internal 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 d73b689cd75ca60a4fe10a2cb2eaad9bc625d97a..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.k
-
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..1465804854fcd34cab00ffe0d572657ea2951c7b 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,14 @@ 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, (module Main_values.CVal)),
+ Leaf (Offsm.key, (module Offsm))))
+
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 1ad67480937996b32bffb54068b50d30ec4ef640..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.k
-
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 14deeda643e120747070f6106980b9acb1d5494f..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.k
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
(*