From 0e685069f3f676939e0af77c3589e490df52c28e Mon Sep 17 00:00:00 2001
From: Maxime Jacquemin <maxime2.jacquemin@gmail.com>
Date: Mon, 20 Feb 2023 18:56:31 +0100
Subject: [PATCH] [Eva] Abstractions: final steps to handle multiple locations.
Abstractions.ml should be done; now we have to fix everything else (in the
next commits).
---
src/plugins/eva/engine/abstractions.ml | 870 ++++++------------------
src/plugins/eva/engine/abstractions.mli | 130 ++++
2 files changed, 321 insertions(+), 679 deletions(-)
diff --git a/src/plugins/eva/engine/abstractions.ml b/src/plugins/eva/engine/abstractions.ml
index cf62ec9304b..20d2b3c3a4b 100644
--- a/src/plugins/eva/engine/abstractions.ml
+++ b/src/plugins/eva/engine/abstractions.ml
@@ -86,7 +86,6 @@ module Value = struct
updating the structure. *)
let add : type v. v registered -> structured -> structured =
fun (key, input) structured ->
- let open Abstract.Value in
let module Interactive = (val make_interactive structured) in
if not (Interactive.mem key) then
(module struct
@@ -99,13 +98,11 @@ module Value = struct
(* The minimal value abstraction to use. It contains the CValue abstraction,
configured depending of the bitwise *)
- let init (is_bitwise : bool) : structured =
- if not is_bitwise then
- (module struct
- include Main_values.CVal
- let structure = Abstract.Value.Leaf (key, (module Main_values.CVal))
- end)
- else (module Offsm_value.CvalueOffsm)
+ let init : structured =
+ (module struct
+ include Main_values.CVal
+ let structure = Abstract.Value.Leaf (key, (module Main_values.CVal))
+ end)
(* When building the complete abstraction, we need to trick locations and
@@ -116,7 +113,6 @@ module Value = struct
This functor is responsible of building such conversion operations. *)
module type From = sig type value val structure : value structure end
module Converter (From : From) (To : Interactive) = struct
- type internal = From.value
type extended = To.t
let structure = From.structure
@@ -207,6 +203,13 @@ module Location = struct
| Last registered -> folder registered acc
| hd :: tl -> fold { folder } tl (folder hd acc)
+ let rec fold_values : type v. 'a Value.folder -> v dependencies -> 'a -> 'a =
+ fun folder dependencies acc ->
+ match dependencies with
+ | Last (module R) -> Value.fold folder R.dependencies acc
+ | (module R) :: tl ->
+ fold_values folder tl (Value.fold folder R.dependencies acc)
+
(* As for the value abstraction, building the location abstraction consists
of structuring the needed registered locations and then adding the needed
@@ -229,30 +232,31 @@ module Location = struct
type 'v structured = (module Structured with type value = 'v)
type 'v interactive = (module Interactive with type value = 'v)
- let init : type v. (module Value.Interactive with type t = v) -> v structured =
- fun (module Interactive) ->
- let module CVal = Main_values.CVal in
- let leaf = Abstract.Value.Leaf (CVal.key, (module CVal)) in
- let module From = struct type value = CVal.t let structure = leaf end in
- let module Converter = Value.Converter (From) (Interactive) in
- let module Loc = Location_lift.Make (Main_locations.PLoc) (Converter) in
- (module struct
- type value = v
- module Value = Interactive
- module Location = Loc
- end)
+ (* Initial location builder *)
+ module Init (V : Value.Interactive) : Structured with type value = V.t =
+ struct
+ module CVal = Main_values.CVal
+ let leaf = Abstract.Value.Leaf (CVal.key, (module CVal))
+ module From = struct type value = CVal.t let structure = leaf end
+ module Converter = Value.Converter (From) (V)
+
+ type value = V.t
+ module Value = V
+ module Location = Location_lift.Make (Main_locations.PLoc) (Converter)
+ end
(* Making a structured value interactive simply consists of adding the
needed operations using the Structure.Open functor.*)
- let make_interactive (module Structured : Structured) =
- (module struct
- include Structured.Location
- include Structure.Open (Abstract.Location) (struct
+ let make_interactive : type v. v structured -> v interactive =
+ fun (module Structured) ->
+ (module struct
include Structured.Location
- type t = location
+ include Structure.Open (Abstract.Location) (struct
+ include Structured.Location
+ type t = location
+ end)
end)
- end : Interactive)
(* Adding a registered location into a structured one is done in three steps:
1. Computing the values dependencies structure.
@@ -303,7 +307,6 @@ module Location = struct
responsible of building such conversion operations. *)
module type From = sig type location val structure : location structure end
module Converter (From : From) (To : Interactive) = struct
- type internal = From.location
type extended = To.location
let structure = From.structure
@@ -389,8 +392,12 @@ module Domain = struct
<location>. *)
module type Domain = sig
type location
- module Make (V : Value.Interactive) :
- Abstract_domain.Leaf with type value = V.t and type location = location
+ module Make (V : Value.Interactive) : sig
+ include Abstract_domain.S
+ with type value = V.t
+ and type location = location
+ val key : state key
+ end
end
type 'l domain = (module Domain with type location = 'l)
@@ -445,10 +452,40 @@ module Domain = struct
| RegisteredDomain : 's Leaf.registered -> registered
| RegisteredFunctor : Functor.registered -> registered
- let register = function
+ type 't with_info =
+ { name : string
+ ; experimental : bool
+ ; priority : int
+ ; abstraction : 't
+ }
+
+ type 't with_mode = 't * Domain_mode.t option
+
+
+ let static_domains = ref []
+ let dynamic_domains = ref []
+
+ let register_domain_option ~name ~experimental ~descr =
+ let descr = if experimental then "Experimental. " ^ descr else descr in
+ Parameters.register_domain ~name ~descr
+
+ let register_abstraction = function
| Domain register -> RegisteredDomain (Leaf.register register)
| Functor register -> RegisteredFunctor (Functor.register register)
+ let register ~name ~descr ?(experimental=false) ?(priority=0) register =
+ register_domain_option ~name ~descr ~experimental ;
+ let abstraction = register_abstraction register in
+ let registered = { name ; experimental ; priority ; abstraction } in
+ static_domains := registered :: !static_domains ;
+ abstraction
+
+ let dynamic_register ~name ~descr ?(experimental=false) ?(priority=0) make =
+ register_domain_option ~name ~descr ~experimental ;
+ let make () = make () |> register_abstraction in
+ let make () = { name ; experimental ; priority ; abstraction = make () } in
+ dynamic_domains := (name, make) :: !dynamic_domains
+
(* Building the domain abstraction consists of structuring the requested
registered domains. To do so, we need to keep track of the values and
@@ -487,13 +524,16 @@ module Domain = struct
(* Adding a registered domain into a structured one consists of performing a
lifting of the registered one if needed before performing the product,
configuring the name and restricting the domain depending of the mode. *)
- let add (type v l) dname mode registered (structured : (v, l) structured) =
+ let add (type v l) (registered, mode) (structured : (v, l) structured) =
+ let wkey = Self.wkey_experimental in
+ let { experimental = exp ; name } = registered in
+ if exp then Self.warning ~wkey "The %s domain is experimental" name ;
let module Structured = (val structured) in
let module Loc = Structured.Location in
let module Val = Structured.Value in
let module Dom = Structured.Domain in
let domain : (v, l) structured_domain =
- match registered with
+ match registered.abstraction with
| RegisteredFunctor (module Functor) ->
let locs = Location.outline Functor.locations in
let eq_loc = Location.dec_eq locs Loc.structure in
@@ -538,7 +578,7 @@ module Domain = struct
module Store = struct
include Store
let register_global_state storage state =
- let no_results = Parameters.NoResultsDomains.mem dname in
+ let no_results = Parameters.NoResultsDomains.mem registered.name in
register_global_state (storage && not no_results) state
end
end in
@@ -564,640 +604,147 @@ module Domain = struct
end : Structured with type value = v and type location = l)
-
-
-
-
-
-
-end
-
-
-
-
-(* --- Registration types --------------------------------------------------- *)
-
-type 'v value =
- | Single of (module Abstract_value.Leaf with type t = 'v)
- | Struct of 'v Abstract.Value.structure
-
-type 'l location =
- | SingleLoc of (module Abstract_location.Leaf with type location = 'l)
- | StructLoc of 'l Abstract.Location.structure
-
-type ('v, 'l) leaf_domain =
- (module Abstract_domain.Leaf with type location = 'l and type value = 'v)
-
-module type Functor_value = sig
- type l
- module Make (V: Abstract.Value.External) :
- (Abstract_domain.Leaf with type value = V.t and type location = l)
+ (* Build a complete abstraction based on a list of registered domains and a
+ value initial configuration. *)
+ let build domains : (module Structured) =
+ let values =
+ let add_value = Value.{ folder = add } in
+ let add_values values (registered, _) =
+ match registered.abstraction with
+ | RegisteredDomain (module Domain) ->
+ Value.fold add_value Domain.values values |>
+ Location.fold_values add_value Domain.locations
+ | RegisteredFunctor (module F) ->
+ Location.fold_values add_value F.locations values
+ in
+ List.fold_left add_values Value.init domains |>
+ Value.make_interactive
+ in
+ let module V = (val values) in
+ let locations =
+ let init : V.t Location.structured = (module Location.Init (V)) in
+ let add_loc = Location.{ folder = add } in
+ let add_locations locs (registered, _) =
+ match registered.abstraction with
+ | RegisteredDomain (module D) -> Location.fold add_loc D.locations locs
+ | RegisteredFunctor (module D) -> Location.fold add_loc D.locations locs
+ in
+ List.fold_left add_locations init domains |>
+ Location.make_interactive
+ in
+ let module L = (val locations) in
+ let domain : (V.t, L.location) structured_domain =
+ (module Unit_domain.Make (V) (L))
+ in
+ let structured : (V.t, L.location) structured = (module struct
+ type value = V.t
+ type location = L.location
+ module Value = V
+ module Location = L
+ module Domain = (val domain)
+ end) in
+ let structured = List.fold_left (fun s d -> add d s) structured domains in
+ let module Structured : Structured = (val structured) in
+ (module Structured)
end
-type ('v, 'l) domain =
- | Domain : ('v, 'l) leaf_domain -> ('v, 'l) domain
- | FunctorValue : (module Functor_value with type l = 'l) -> (_, 'l) domain
-
-type ('v, 'l) abstraction =
- { values: 'v value
- ; location: 'l location
- ; domain : ('v, 'l) domain
- }
-
-type 't with_info =
- { name: string
- ; experimental: bool
- ; priority: int
- ; abstraction: 't
- }
-
-type flag = Flag: ('v, 'l) abstraction with_info -> flag
-
-
-type ('a, 'b) dec_eq = ('a, 'b) Structure.eq option
-
-
-
-(* --- Config and registration ---------------------------------------------- *)
-
-module Config = struct
- module OptMode = Datatype.Option (Domain_mode)
- module Element = struct
- type t = flag * Domain_mode.t option
-
- (* Flags are sorted by increasing priority order, and then by name. *)
- let compare (Flag f1, mode1) (Flag f2, mode2) =
- let c = Datatype.Int.compare f1.priority f2.priority in
- if c <> 0 then c else
- let c = Datatype.String.compare f1.name f2.name in
- if c <> 0 then c else
- OptMode.compare mode1 mode2
- end
-
- include Set.Make (Element)
- let mem (Flag domain) =
- exists (fun (Flag flag, _mode) -> flag.name = domain.name)
- let abstractions = ref []
- let dynamic_abstractions = ref []
+(* --- Configuration -------------------------------------------------------- *)
- let register_domain_option ~name ~experimental ~descr =
- let descr = if experimental then "Experimental. " ^ descr else descr in
- Parameters.register_domain ~name ~descr
+module Configuration = struct
+ module Mode = Datatype.Option (Domain_mode)
- let register ~name ~descr ?(experimental=false) ?(priority=0) abstraction =
- register_domain_option ~name ~experimental ~descr;
- let flag = Flag { name; experimental; priority; abstraction } in
- abstractions := flag :: !abstractions;
- flag
-
- let dynamic_register ~name ~descr ?(experimental=false) ?(priority=0) make =
- register_domain_option ~name ~experimental ~descr;
- let make' () : flag =
- Flag { name; experimental; priority; abstraction = make () }
- in
- dynamic_abstractions := (name,make') :: !dynamic_abstractions
+ include Set.Make (struct
+ open Domain
+ type t = registered with_info with_mode
+ let compare (d1, m1) (d2, m2) =
+ let c = Datatype.Int.compare d1.priority d2.priority in
+ if c = 0 then
+ let c = Datatype.String.compare d1.name d2.name in
+ if c = 0 then Mode.compare m1 m2 else c
+ else c
+ end)
let configure () =
- let add_main_mode mode =
- let main, _ = Globals.entry_point () in
- (main, Domain_mode.Mode.all) :: mode
- in
- let add config (name, make) =
+ let find = Parameters.DomainsFunction.find in
+ let find name = try Some (find name) with Not_found -> None in
+ let main = Globals.entry_point () |> fst in
+ let add_main_mode modes = (main, Domain_mode.Mode.all) :: modes in
+ let dynamic (name, make) config =
let enabled = Parameters.Domains.mem name in
- try
- let mode = Parameters.DomainsFunction.find name in
- let mode = if enabled then add_main_mode mode else mode in
- add (make (), Some mode) config
- with Not_found ->
- if enabled then add (make (), None) config else config
+ let enable modes = if enabled then add_main_mode modes else modes in
+ match find name with
+ | None -> if enabled then add (make (), None) config else config
+ | Some modes -> add (make (), Some (enable modes)) config
in
- let aux config (Flag domain as flag) =
- add config (domain.name, (fun () -> flag))
- in
- let config = List.fold_left aux empty !abstractions in
- List.fold_left add config !dynamic_abstractions
-
- (* --- Register default abstractions -------------------------------------- *)
-
- let create_domain ?experimental priority name descr values location domain =
- let values = Single values in
- let location = SingleLoc location in
- let domain = Domain domain in
- let abstraction = { values ; location ; domain } in
- register ~name ~descr ~priority ?experimental abstraction
-
- (* Register standard domains over cvalues. *)
- let make ?experimental rank name descr =
- create_domain ?experimental rank name descr
- (module Main_values.CVal) (module Main_locations.PLoc)
-
- let cvalue =
- make 9 "cvalue"
- "Main analysis domain, enabled by default. Should not be disabled."
- (module Cvalue_domain.State)
-
- let symbolic_locations =
- make 7 "symbolic-locations"
- "Infers values of symbolic locations represented by imprecise lvalues, \
- such as t[i] or *p when the possible values of [i] or [p] are imprecise."
- (module Symbolic_locs.D)
-
- (* TODO: Location handling in equality functor *)
- let equality =
- let descr = "Infers equalities between syntactic C expressions. \
- Makes the analysis less dependent on temporary variables and \
- intermediate computations."
- and abstraction =
- { values = Struct Abstract.Value.Unit;
- location = SingleLoc (module Main_locations.PLoc);
- domain = FunctorValue (module struct
- type l = Main_locations.PLoc.location
- module Make = Equality_domain.Make
- end); }
- in
- register ~name:"equality" ~descr ~priority:8 abstraction
-
- let gauges =
- make 6 "gauges"
- "Infers linear inequalities between the variables modified within a loop \
- and a special loop counter."
- (module Gauges_domain.D)
-
- let octagon =
- make 6 "octagon"
- "Infers relations between scalar variables of the form b ≤ ±X ± Y ≤ e, \
- where X, Y are program variables and b, e are constants."
- (module Octagons)
-
- let bitwise =
- create_domain 3 "bitwise"
- "Infers bitwise information to interpret more precisely bitwise operators."
- (module Offsm_value.Offsm) (module Main_locations.PLoc) (module Offsm_domain.D)
-
- let sign =
- create_domain 4 "sign"
- "Infers the sign of program variables."
- (module Sign_value) (module Main_locations.PLoc) (module Sign_domain)
-
- let inout = make 5 "inout" ~experimental:true
- "Infers the inputs and outputs of each function."
- (module Inout_domain.D)
-
- let traces =
- make 2 "traces" ~experimental:true
- "Builds an over-approximation of all the traces that lead \
- to a statement."
- (module Traces_domain.D)
-
- let printer =
- make 2 "printer"
- "Debug domain, only useful for developers. Prints the transfer functions \
- used during the analysis."
- (module Printer_domain)
-
- (* --- Default and legacy configurations ---------------------------------- *)
-
- let default = configure ()
- let legacy = singleton (cvalue, None)
+ let static d = dynamic (d.Domain.name, fun () -> d) in
+ let fold f xs acc = List.fold_left (fun acc x -> f x acc) acc xs in
+ fold static !Domain.static_domains empty |>
+ fold dynamic !Domain.dynamic_domains
end
-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 Internal_Value = struct
- open Abstract.Value
-
- let eq_value : type a b. a structure -> b value -> (a, b) dec_eq =
- fun structure -> function
- | Struct s -> eq_structure structure s
- | Single (module V) ->
- match structure with
- | Leaf (key, _) -> eq_type key V.key
- | _ -> None
- 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 void_value () =
- Self.fatal "Cannot register a value module from a Void structure."
-
- let add_value_structure value internal =
- let rec aux: type v. (module Internal) -> v structure -> (module Internal) =
- fun value -> function
- | Option (s, _) -> aux value s
- | Leaf (key, v) -> add_value_leaf value (V (key, v))
- | Node (s1, s2) -> aux (aux value s1) s2
- | Unit -> value
- | Void -> void_value ()
- in
- aux value internal
+(* --- Value reduced product ----------------------------------------------- *)
- let build_values config initial_value =
- let build (Flag flag, _) acc =
- match flag.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 type Struct = sig type v val s : v value end
-
- module Convert (Value: Abstract.Value.External) (Struct: Struct) = struct
- type extended = Value.t
-
- let structure =
- match Struct.s with
- | Single (module V) -> Abstract.Value.Leaf (V.key, (module V))
- | Struct s -> s
-
- let replace =
- 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)
- | Option (s, default) -> fun v -> set s (Option.value ~default v)
- | Unit -> fun () value -> value
- | Void -> void_value ()
- in
- set structure
-
- let extend v = replace v Value.top
-
- let restrict =
- let rec get: type v. v structure -> Value.t -> v = function
- | Leaf (key, _) -> Option.get (Value.get key)
- | Node (s1, s2) ->
- let get1 = get s1 and get2 = get s2 in
- fun v -> get1 v, get2 v
- | Option (s, _) -> fun v -> Some (get s v)
- | Unit -> fun _ -> ()
- | Void -> void_value ()
- in
- get structure
+module Reducer = struct
+ module type S = sig
+ include Abstract.Value.External
+ val reduce : t -> t
end
-end
-
+ type 'a key = 'a Value.key
+ type ('a, 'b) reducer = 'a -> 'b -> 'a * 'b
+ type action = Action : 'a key * 'b key * ('a, 'b) reducer -> action
-(* --- Building value abstractions ------------------------------------------ *)
+ let actions = ref []
-module Leaf_Location (Loc: Abstract_location.Leaf) = struct
- include Loc
- let structure = Abstract.Location.Leaf (Loc.key, (module Loc))
-end
+ let register left right reducer =
+ actions := (Action (left, right, reducer)) :: !actions
-module Internal_Loc = struct
- open Abstract.Location
+ module Make (Value : Abstract.Value.External) = struct
+ include Value
- let eq_loc : type a b. a structure -> b location -> (a, b) dec_eq =
- fun structure -> function
- | StructLoc s -> eq_structure structure s
- | SingleLoc (module L) ->
- match structure with
- | Leaf (key, _) -> eq_type key L.key
- | _ -> None
+ let make_reduction acc (Action (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 = f (get1 v) (get2 v) in
+ let reducer v = let v1, v2 = reduce v in set1 v1 (set2 v2 v) in
+ reducer :: acc
+ | _, _ -> acc
- type loc_key_module = L : 'l key * 'l data -> loc_key_module
-
- let open_loc_abstraction (module Loc : Internal) =
- (module struct
- include Loc
- include Structure.Open (Abstract.Location) (struct
- include Loc
- type t = location
- end)
- end : Abstract.Location.External)
-
- (* TODO: Location product ? *)
- let add_loc_leaf loc (L (key, _l)) =
- let module Loc = (val open_loc_abstraction loc) in
- if Loc.mem key then loc else
- (* (module struct *)
- (* include Location_product.Make (Loc) (val l) *)
- (* let structure = Node (Loc.structure, Leaf (key, l)) *)
- (* end) *)
- assert false
-
- let void_loc () =
- Self.fatal "Cannot register a location module from a Void structure."
-
- let add_loc_structure loc internal =
- let rec aux: type l. (module Internal) -> l structure -> (module Internal) =
- fun loc -> function
- | Option (s, _) -> aux loc s
- | Leaf (key, v) -> add_loc_leaf loc (L (key, v))
- | Node (s1, s2) -> aux (aux loc s1) s2
- | Unit -> loc
- | Void -> void_loc ()
- in
- aux loc internal
-
- let build_locs config initial_loc =
- let build (Flag flag, _) acc =
- match flag.abstraction.location with
- | StructLoc structure -> add_loc_structure acc structure
- | SingleLoc (module L) -> add_loc_leaf acc (L (L.key, (module L)))
- in
- Config.fold build config initial_loc |> open_loc_abstraction
-
- module type Struct = sig type l val s : l location end
-
- module Convert (Loc: Abstract.Location.External) (Struct: Struct) = struct
- type extended = Loc.location
-
- let structure =
- match Struct.s with
- | SingleLoc (module L) -> Abstract.Location.Leaf (L.key, (module L))
- | StructLoc s -> s
-
- let replace =
- let rec set: type l. l structure -> l -> Loc.location -> Loc.location = function
- | Leaf (key, _) -> Loc.set key
- | Node (s1, s2) ->
- let set1 = set s1 and set2 = set s2 in
- fun (l1, l2) loc -> set1 l1 (set2 l2 loc)
- | Option (s, default) -> fun l -> set s (Option.value ~default l)
- | Unit -> fun () loc -> loc
- | Void -> void_loc ()
- in
- set structure
-
- let extend l = replace l Loc.top
-
- let restrict =
- let rec get: type l. l structure -> Loc.location -> l = function
- | Leaf (key, _) -> Option.get (Loc.get key)
- | Node (s1, s2) ->
- let get1 = get s1 and get2 = get s2 in
- fun l -> get1 l, get2 l
- | Option (s, _) -> fun l -> Some (get s l)
- | Unit -> fun _ -> ()
- | Void -> void_loc ()
- in
- get structure
+ let reduce =
+ let list = List.fold_left make_reduction [] !actions in
+ fun v -> List.fold_left (fun v reduce -> reduce v) v list
end
end
-(* --- Building domain abstractions ----------------------------------------- *)
-
-module type Acc = sig
- module Val : Abstract.Value.External
- module Loc : Abstract.Location.External
- with type value = Val.t
- module Dom : Abstract.Domain.Internal
- with type value = Val.t and type location = Loc.location
-end
-
-module Leaf_Domain (D: Abstract_domain.Leaf) = struct
- include D
- let structure = Abstract.Domain.Leaf (D.key, (module D))
-end
-
-
-module type Typ = sig type t end
-let conversion_id (type t) (module T: Typ with type t = t) =
- (module struct
- type extended = T.t
- type internal = T.t
- let extend x = x
- let restrict x = x
- end: Domain_lift.Conversion with type extended = t and type internal = t)
-
-type ('v, 'l) internal_domain =
- (module Abstract.Domain.Internal with type value = 'v and type location = 'l)
-
-let add_domain (type v) (type l) dname mode (abstraction: (v, l) abstraction) (module Acc: Acc) =
- let domain : (Acc.Val.t, Acc.Loc.location) internal_domain =
- let eq_loc = Internal_Loc.eq_loc Acc.Loc.structure abstraction.location in
- match abstraction.domain with
- | FunctorValue (module Functor) ->
- let module Domain = Leaf_Domain (Functor.Make (Acc.Val)) in
- begin match eq_loc with
- | Some Structure.Eq -> (module Domain)
- | None ->
- let module ConvertVal = (val conversion_id (module Acc.Val)) in
- let module ConvertLoc = Internal_Loc.Convert (Acc.Loc) (struct
- type l = Domain.location
- let s = abstraction.location
- end) in
- (module Domain_lift.Make (Domain) (ConvertVal) (ConvertLoc))
- end
- | Domain (module Domain) ->
- let eq_value = Internal_Value.eq_value Acc.Val.structure abstraction.values in
- match eq_value, eq_loc with
- | Some Structure.Eq, Some Structure.Eq -> (module Leaf_Domain (Domain))
- | Some Structure.Eq, None ->
- let module ConvertVal = (val conversion_id (module Acc.Val)) in
- let module ConvertLoc = Internal_Loc.Convert (Acc.Loc) (struct
- type l = Domain.location
- let s = abstraction.location
- end) in
- (module Domain_lift.Make (Domain) (ConvertVal) (ConvertLoc))
- | None, Some Structure.Eq ->
- let module ConvertVal = Internal_Value.Convert (Acc.Val) (struct
- type v = Domain.value
- let s = abstraction.values
- end) in
- let module LocTyp = struct type t = Acc.Loc.location end in
- let module ConvertLoc = (val conversion_id (module LocTyp)) in
- (module Domain_lift.Make (Domain) (ConvertVal) (ConvertLoc))
- | None, None ->
- let module ConvertVal = Internal_Value.Convert (Acc.Val) (struct
- type v = Domain.value
- let s = abstraction.values
- end) in
- let module ConvertLoc = Internal_Loc.Convert (Acc.Loc) (struct
- type l = Domain.location
- let s = abstraction.location
- end) in
- (module Domain_lift.Make (Domain) (ConvertVal) (ConvertLoc))
- in
- (* Set the name of the domain. *)
- let module Domain = struct
- include (val domain)
- module Store = struct
- include Store
- let register_global_state storage state =
- let no_results = Parameters.NoResultsDomains.mem dname in
- register_global_state (storage && not no_results) state
- end
- end in
- (* Restricts the domain according to [mode]. *)
- let domain : (Acc.Val.t, Acc.Loc.location) internal_domain =
- match mode with
- | None -> (module Domain)
- | Some kf_modes ->
- let module Scope = struct let functions = kf_modes end in
- let module Domain =
- Domain_builder.Restrict
- (Acc.Val)
- (Domain)
- (Scope)
- in
- (module Domain)
- in
- let domain : (Acc.Val.t, Acc.Loc.location) internal_domain =
- 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
- (module struct
- module Val = Acc.Val
- module Loc = Acc.Loc
- module Dom = (val domain)
- end : Acc)
-
-let warn_experimental flag =
- if flag.experimental then
- Self.(warning ~wkey:wkey_experimental
- "The %s domain is experimental." flag.name)
-
-let build_domain config abstract =
- let build (Flag flag, mode) acc =
- warn_experimental flag;
- add_domain flag.name mode flag.abstraction acc
- in
- (* Domains in the [config] are sorted by increasing priority: domains with
- higher priority are added last: they will be at the top of the domains
- tree, and thus will be processed first during the analysis. *)
- Config.fold build config abstract
-
-
-
-(* --- Value reduced product ----------------------------------------------- *)
-
-module type Value = sig
- include Abstract.Value.External
- val reduce : t -> t
-end
+(* --- Finalizing abstractions build ---------------------------------------- *)
module type S = sig
- module Val : Value
- module Loc : Abstract.Location.External
- with type value = Val.t
+ module Val : Reducer.S
+ 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 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
-
-
-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
-
-let value_reduced_product = ref []
-
-let register_value_reduction reduced_product =
- value_reduced_product := (R reduced_product) :: !value_reduced_product
-
-(* 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
- | Some ival ->
- try
- let ival' = Cvalue.V.project_ival cvalue in
- if Ival.is_int ival'
- then
- let reduced_ival = Ival.narrow ival ival' in
- let cvalue = Cvalue.V.inject_ival reduced_ival in
- cvalue, Some reduced_ival
- else cvalue, Some 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
-
- 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
+module Hooks = struct
+ let hooks = ref []
+ type hook = (module S) -> (module S)
+ let register (f : hook) = hooks := f :: !hooks
+ let apply abst = List.fold_left (fun acc f -> f acc) abst !hooks
end
-
-
-(* --- Final hook ----------------------------------------------------------- *)
-
-let final_hooks = ref []
-
-let register_hook f =
- final_hooks := f :: !final_hooks
-
-let apply_final_hooks abstractions =
- List.fold_left (fun acc f -> f acc) abstractions !final_hooks
-
-
-
-(* --- 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 Open (Structured : Domain.Structured) : S = struct
+ module Val = Reducer.Make (Structured.Value)
+ module Loc = Structured.Location
module Dom = struct
- include Acc.Dom
- include Structure.Open (Abstract.Domain) (Acc.Dom)
+ include Structured.Domain
+ include Structure.Open (Abstract.Domain) (Structured.Domain)
let get_cvalue = match get Cvalue_domain.State.key with
| None -> None
@@ -1213,53 +760,18 @@ module Open (Acc: Acc) : S = struct
end
end
-module CVal = Leaf_Value (Main_values.CVal)
-
-let unit_acc (type v)
- (module Value: Abstract.Value.External with type t = v)
- (module Loc: Abstract.Location.External with type value = v) =
- (module struct
- module Val = Value
- module Loc = Loc
- module Dom = Unit_domain.Make (Val) (Loc)
- end: Acc)
-
-(* let unit_acc (module Value: Abstract.Value.External) = *)
-(* let loc : (module Abstract.Location.Internal 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 = Value *)
-(* module Loc = (val loc) *)
-(* module Dom = Unit_domain.Make (Val) (Loc) *)
-(* end : Acc) *)
-
-let build_abstractions config =
- let initial_loc = (module Main_locations.PLoc: Abstract.Location.Internal) in
- 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 loc = Internal_Loc.build_locs config initial_loc in
- let acc = unit_acc value loc in
- build_domain config acc
-
-let configure = Config.configure
+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 make config =
- let abstractions = build_abstractions config in
- let abstractions = (module Open (val abstractions): S) in
- apply_final_hooks abstractions
+ let abstractions = Configuration.elements config |> Domain.build in
+ let abstractions = (module Open (val abstractions) : S) in
+ Hooks.apply abstractions
-module Default = (val make Config.default)
-module Legacy = (val make Config.legacy)
+module Default = (val make (Configuration.configure ()))
diff --git a/src/plugins/eva/engine/abstractions.mli b/src/plugins/eva/engine/abstractions.mli
index be3c32e0515..755e771a050 100644
--- a/src/plugins/eva/engine/abstractions.mli
+++ b/src/plugins/eva/engine/abstractions.mli
@@ -20,6 +20,134 @@
(* *)
(**************************************************************************)
+
+
+module Value : sig
+ type 'v key = 'v Abstract.Value.key
+ type 'v value = (module Abstract_value.S with type t = 'v)
+
+ type 'v registered
+ type 'v register = { key : 'v key ; value : 'v value }
+ val register : 'v register -> 'v registered
+
+ type 'v dependencies =
+ | Last : 'v registered -> 'v dependencies
+ | (::) : 'a registered * 'b dependencies -> ('a * 'b) dependencies
+end
+
+
+
+module Location : sig
+ type 'l key = 'l Abstract.Location.key
+ type ('v, 'l) location =
+ (module Abstract_location.S with type value = 'v and type location = 'l)
+
+ type 'l registered
+ type ('v, 'l) register =
+ { key : 'l key
+ ; location : ('v, 'l) location
+ ; dependencies : 'v Value.dependencies
+ }
+
+ val register : ('v, 'l) register -> 'l registered
+
+ type 'l dependencies =
+ | Last : 'l registered -> 'l dependencies
+ | (::) : 'a registered * 'b dependencies -> ('a * 'b) dependencies
+end
+
+
+
+module Domain : sig
+ type 's key = 's Abstract.Domain.key
+
+ module Leaf : sig
+ type ('v, 'l, 's) domain =
+ (module Abstract_domain.S
+ with type value = 'v and type location = 'l and type state = 's)
+
+ type ('v, 'l, 's) register =
+ { key : 's key
+ ; domain : ('v, 'l, 's) domain
+ ; values : 'v Value.dependencies
+ ; locations : 'l Location.dependencies
+ }
+ end
+
+ module Functor : sig
+ module type Domain = sig
+ type location
+ module Make (V : Abstract.Value.External) : sig
+ include Abstract_domain.S
+ with type value = V.t and type location = location
+ val key : state key
+ end
+ end
+
+ type 'l domain = (module Domain with type location = 'l)
+
+ type 'l register =
+ { domain : 'l domain
+ ; locations : 'l Location.dependencies
+ }
+ end
+
+ type registered
+ type register =
+ | Domain : ('v, 'l, 's) Leaf.register -> register
+ | Functor : 'l Functor.register -> register
+
+ val register :
+ name:string -> descr:string -> ?experimental:bool -> ?priority:int ->
+ register -> registered
+
+ val dynamic_register :
+ name:string -> descr:string -> ?experimental:bool -> ?priority:int ->
+ (unit -> register) -> unit
+end
+
+
+
+module Reducer : sig
+ module type S = sig
+ include Abstract.Value.External
+ val reduce : t -> t
+ end
+
+ type 'a key = 'a Value.key
+ type ('a, 'b) reducer = 'a -> 'b -> 'a * 'b
+
+ val register : 'a key -> 'b key -> ('a, 'b) reducer -> unit
+end
+
+
+
+module type S = sig
+ module Val : Reducer.S
+ 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 Hooks : sig
+ type hook = (module S) -> (module S)
+ val register : hook -> unit
+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
+end
+
+module Default : S
+
+
+(*
+
(** Registration and building of the analysis abstractions. *)
(** {2 Registration of abstractions.} *)
@@ -179,3 +307,5 @@ val make: Config.t -> (module S)
module Legacy : S
module Default : S
+
+*)
--
GitLab