Commit e342fcf1 authored by David Bühler's avatar David Bühler
Browse files

[Eva] New file abstract defining the Internal and External module types.

These module definitions were previously in abstract_value, abstract_location
and abstract_domain. They are now grouped in this new file for the three
abstractions.
These module types should only be useful for the engine, and need not to be
visible in the implementation of the various abstractions.

New module type Leaf in abstract_value, abstract_location and abstract_domain
with the key identifying the module. The internal structure is no longer needed
in these abstractions, and is instead built by the engine from this key.

Keys are no longer exported outside the modules.
For abstract domains, the key is automatically created by the functor
Domain_builder.Complete from the domain name.

Many changes throughout the analyzer:
- in the engine, Abstract_value.{Internal|External} becomes
  Abstract.Value.{Internal|External}.
- in the abstractions, Abstract_value.Internal becomes Abstract_value.Leaf.
parent 154083e6
......@@ -878,7 +878,7 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
slevel/per_stmt_slevel \
utils/library_functions \
utils/eval_typ utils/backward_formals \
alarmset eval utils/structure \
alarmset eval utils/structure utils/abstract \
values/value_product values/location_lift \
values/cvalue_forward values/cvalue_backward \
values/main_values values/main_locations \
......
......@@ -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
......
......@@ -396,73 +396,12 @@ module type S = sig
val initialize_variable_using_type: init_kind -> varinfo -> t -> t
include Recycle with type t := t
end
(** Keys identify abstract domains through the type of their abstract values. *)
type 'a key = 'a Structure.Key_Domain.key
(** Describes the internal structure of a domain.
Used internally to automatically generate efficient accessors from a
generic abstract domain, which may be a combination of several domains,
to a specific one. *)
type 'a structure = 'a Structure.Key_Domain.structure =
| Void : 'a structure
| Leaf : 'a key -> 'a structure
| Node : 'a structure * 'b structure -> ('a * 'b) structure
(**
For a simple 'leaf' domain, the structure should be:
[let key = Structure.Key_Domain.create_key "name_of_the_domain";;
let structure = Leaf key;;]
Then, the key should be exported by the domain, to allow the use of the
functions defined in the {!Interface} interface below.
A compound domain may use the {!Node} constructor to provide a separate
access to each of its parts.
A domain can also use the {!Void} constructor to prevent access to itself.
*)
(** Structure of a domain. *)
module type S_with_Structure = sig
include S
(** A structure matching the type of the domain. *)
val structure : t structure
(** Category for the messages about the domain.
Must be created through {!Value_parameters.register_category}. *)
val log_category : Value_parameters.category
end
(** External interface of a domain, with accessors.
Automatically built by the functor {!Structure.Open}.
When a generic domain is a combination of several domains, these functions
allow interacting with its subparts. Note that their behavior is undefined
if the overall domain contains several times the same domain. *)
module type Interface = sig
type t
(** Tests whether a key belongs to the domain. *)
val mem : 'a key -> bool
(** For a key of type [k key]:
- if the states of this domain (of type [t]) contain a part (of type [k])
from the domain identified by the key,
then [get key] returns an accessor for this part of a state.
- otherwise, [get key] returns None. *)
val get : 'a key -> (t -> 'a) option
(** For a key of type [k key]:
- if the states of this domain (of type [t]) contain a part (of type [k])
from the domain identified by the key,
then [set key d state] returns the state [state] in which this part
has been replaced by [d].
- otherwise, [set key _] is the identity function. *)
val set : 'a key -> 'a -> t -> t
end
(** Automatic storage of the states computed during the analysis. *)
module type Store = sig
......@@ -487,7 +426,7 @@ end
(** Full implementation of domains. Automatically built by
{!Domain_builder.Complete} from an {!S_with_Structure} domain. *)
module type Internal = sig
include S_with_Structure
include S
module Store: Store with type state := state
(** This function is called after the analysis. The argument is the state
......@@ -497,11 +436,14 @@ module type Internal = sig
val post_analysis: t or_bottom -> unit
end
(** Final interface of domains, as generated and used by Eva, with generic
accessors for domains. *)
module type External = sig
type 't key = 't Structure.Key_Domain.key
(** Signature for a leaf module of a domain. *)
module type Leaf = sig
include Internal
include Interface with type t := state
(** The key identifies the domain and the type [t] of its states. *)
val key: t key
end
......
......@@ -22,11 +22,14 @@
let ok = false
module type S = Abstract_domain.Internal
module type S = Abstract_domain.Leaf
with type value = Main_values.Interval.t
and type location = Precise_locs.precise_location
module U = Unit_domain.Make (Main_values.Interval) (Main_locations.PLoc)
module U = struct
include Unit_domain.Make (Main_values.Interval) (Main_locations.PLoc)
let key = Structure.Key_Domain.create_key "dummy_apron"
end
module Octagon = U
module Box = U
......@@ -34,14 +37,6 @@ module Polka_Loose = U
module Polka_Strict = U
module Polka_Equalities = U
let dummy_key = Structure.Key_Domain.create_key "dummy_apron"
let octagon_key = dummy_key
let box_key = dummy_key
let polka_loose_key = dummy_key
let polka_strict_key = dummy_key
let polka_equalities_key = dummy_key
(*
Local Variables:
compile-command: "make -C ../../../.."
......
......@@ -28,7 +28,7 @@
val ok : bool
(** Signature of an Apron domain in Eva. *)
module type S = Abstract_domain.Internal
module type S = Abstract_domain.Leaf
with type value = Main_values.Interval.t
and type location = Precise_locs.precise_location
......@@ -51,16 +51,6 @@ module Polka_Strict : S
(** Linear equalities. *)
module Polka_Equalities : S
(** Domain keys for the Apron domains in Eva. *)
val octagon_key : Octagon.t Abstract_domain.key
val box_key : Box.t Abstract_domain.key
val polka_loose_key : Polka_Loose.t Abstract_domain.key
val polka_strict_key : Polka_Strict.t Abstract_domain.key
val polka_equalities_key : Polka_Equalities.t Abstract_domain.key
(*
Local Variables:
compile-command: "make -C ../../../.."
......
......@@ -32,7 +32,7 @@ let ok = true
let debug = false
module type S = Abstract_domain.Internal
module type S = Abstract_domain.Leaf
with type value = Main_values.Interval.t
and type location = Precise_locs.precise_location
......@@ -362,7 +362,6 @@ module Make
type t
val manager: t Manager.t
val name: string
val key: t Abstract1.t Abstract_domain.key
end)
= struct
......@@ -371,8 +370,6 @@ module Make
type location = Precise_locs.precise_location
let man = Man.manager
let structure = Abstract_domain.Leaf Man.key
let log_category = dkey
let empty_env = Environment.make [||] [||]
......@@ -725,44 +722,32 @@ module Make
end
let octagon_key = Structure.Key_Domain.create_key "apron-octagon"
let box_key = Structure.Key_Domain.create_key "apron-box"
let polka_loose_key = Structure.Key_Domain.create_key "polka-loose"
let polka_strict_key = Structure.Key_Domain.create_key "polka-strict"
let polka_equalities_key = Structure.Key_Domain.create_key "polka-equalities"
module Apron_Octagon = struct
type t = Oct.t
let manager = Oct.manager_alloc ()
let name = "Apron octagon domain"
let key = octagon_key
end
module Apron_Box = struct
type t = Box.t
let manager = Box.manager_alloc ()
let name = "Apron box domain"
let key = box_key
end
module Apron_Polka_Loose = struct
type t = Polka.loose Polka.t
let manager = Polka.manager_alloc_loose ()
let name = "Polka loose polyhedra domain"
let key = polka_loose_key
end
module Apron_Polka_Strict = struct
type t = Polka.strict Polka.t
let manager = Polka.manager_alloc_strict ()
let name = "Polka strict polyhedra domain"
let key = polka_strict_key
end
module Apron_Polka_Equalities = struct
type t = Polka.equalities Polka.t
let manager = Polka.manager_alloc_equalities ()
let name = "Polka linear equalities domain"
let key = polka_equalities_key
end
(** Apron manager allocation changes the rounding mode. *)
......
......@@ -29,7 +29,7 @@ let extract get = match get key with
| None -> fun _ -> Cvalue.Model.top
| Some get -> function
| `Bottom -> Cvalue.Model.bottom
| `Value state -> get state
| `Value state -> fst (get state)
module Model = struct
......@@ -168,10 +168,6 @@ module State = struct
type state = Model.t * Locals_scoping.clobbered_set
let structure =
Abstract_domain.Node (Abstract_domain.Leaf key,
Abstract_domain.Leaf Locals_scoping.key)
let log_category = Value_parameters.dkey_cvalue_domain
include Datatype.Make_with_collections (
......@@ -193,6 +189,7 @@ module State = struct
end )
let name = "Cvalue domain"
let key = key
type value = Model.value
type location = Model.location
......@@ -562,12 +559,12 @@ module Subpart = struct
let hash = Model.hash_subtree
let equal = Model.equal_subtree
end
let distinct_subpart a b =
let distinct_subpart (a, _) (b, _) =
if Model.equal a b then None
else
try Model.comp_prefixes a b; None
with Model.Found_prefix (p, s1, s2) -> Some (p, s1, s2)
let find_subpart s prefix = Model.find_prefix s prefix
let find_subpart (s, _) prefix = Model.find_prefix s prefix
(*
Local Variables:
......
......@@ -22,15 +22,14 @@
(** Main domain of the Value Analysis. *)
module State : Abstract_domain.Internal
module State : Abstract_domain.Leaf
with type value = Main_values.CVal.t
and type location = Main_locations.PLoc.location
val key : Cvalue.Model.t Abstract_domain.key
and type state = Cvalue.Model.t * Locals_scoping.clobbered_set
val extract :
(Cvalue.Model.t Abstract_domain.key -> ('state -> Cvalue.Model.t) option) ->
(State.t Structure.Key_Domain.key ->
('state -> State.t) option) ->
'state Eval.or_bottom -> Cvalue.Model.t
val inject : Cvalue.Model.t -> State.t
......@@ -42,8 +41,8 @@ val project : State.t -> Cvalue.Model.t
type prefix
module Subpart : Hashtbl.HashedType
val distinct_subpart :
Cvalue.Model.t -> Cvalue.Model.t -> (prefix * Subpart.t * Subpart.t) option
val find_subpart : Cvalue.Model.t -> prefix -> Subpart.t option
State.t -> State.t -> (prefix * Subpart.t * Subpart.t) option
val find_subpart : State.t -> prefix -> Subpart.t option
......
......@@ -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 |]
......
......@@ -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
......
......@@ -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
......
......@@ -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
......@@ -45,7 +45,6 @@ module Make
include (Domain : Datatype.S_with_collections with type t = Domain.t)
include (Domain : Abstract_domain.Lattice with type state = Domain.state)
let structure = Domain.structure
let log_category = Domain.log_category
type value = Convert.extended_value
......
......@@ -51,8 +51,6 @@ module Make
(struct let module_name = name end)
type state = t
let structure = Abstract_domain.Node (Left.structure, Right.structure)
let log_category = product_category
let top = Left.top, Right.top
......
......@@ -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 =
......
......@@ -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
......
......@@ -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
......
......@@ -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
......@@ -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
......
......@@ -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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment