Skip to content
Snippets Groups Projects
Commit 9772805f authored by David Bühler's avatar David Bühler
Browse files

[Eva] Dynamic registration of abstractions (values and domains). 

Complete rewrite of abstraction.ml, with even more first class modules and GADT.
All current abstract values and domains are registered with this generic
mecanism in abstractions.ml, except the Apron binding and the Numerors domain.

The configuration is now the set of abstractions that should be instantiated.
parent a5d0d5ad
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/plugins/value/engine/abstractions.ml
+ 341
− 575
View file @ 9772805f
......@@ -20,638 +20,404 @@
(* *)
(**************************************************************************)
(* 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
end
type 'v value =
| Single of (module Abstract_value.Leaf with type t = 'v)
| Struct of 'v Abstract.Value.structure
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
type precise_loc = Precise_locs.precise_location
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 type leaf_domain = Abstract_domain.Leaf with type location = precise_loc
(* -------------------------------------------------------------------------- *)
(* Value Abstraction *)
(* -------------------------------------------------------------------------- *)
module type domain_functor =
functor (Value: Abstract.Value.External) ->
(leaf_domain with type value = Value.t)
module type V = sig
include Abstract.Value.External
val structure : t Abstract.Value.structure
end
type 'v domain =
| Domain: (module leaf_domain with type value = 'v) -> 'v domain
| Functor: (module domain_functor) -> _ domain
module Internal_CVal = struct
include Main_values.CVal
let structure = Abstract.Value.Leaf key
end
type 'v abstraction =
{ name: string;
values: 'v value;
domain: 'v domain; }
module CVal = struct
include Internal_CVal
include Structure.Open (Abstract.Value) (Internal_CVal)
end
(* --- Config and registration ---------------------------------------------- *)
module Internal_PLoc = struct
include Main_locations.PLoc
let structure = Abstract.Location.Leaf key
end
module Config = struct
type flag = Flag: 'v abstraction -> flag
module Internal_Cvalue_Domain = struct
include Cvalue_domain.State
let structure = Abstract.Domain.Leaf key
end
module Flag = struct
type t = flag
let compare (Flag f1) (Flag f2) = Datatype.String.compare f1.name f2.name
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
let structure =
Abstract.Value.(Node (Left.structure, Leaf Main_values.Interval.key))
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 (Abstract.Value) (Value)
end : V)
let build_value config =
let value =
if config.bitwise
then (module Offsm_value.CvalueOffsm : Abstract.Value.Internal)
else (module Internal_CVal : Abstract.Value.Internal)
in
let value =
if config.signs
then
let module Value = (val value) in
let module V = struct
include Value_product.Make (Value) (Sign_value)
let structure =
Abstract.Value.(Node (Value.structure, Leaf Sign_value.key))
end in
(module V: Abstract.Value.Internal)
else value
in
let value =
if config.numerors
then Numerors_domain.add_numerors_value value
else value
in
let value =
if has_apron config
then add_apron_value config value
else value
in
open_value_abstraction value
include Set.Make (Flag)
(* 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
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 extend_val =
let set = Value.set K.key in
fun v -> set v Value.top
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
let replace_val = Value.set K.key
(* --- Register default abstractions -------------------------------------- *)
let restrict_val = match Value.get K.key with
| None -> assert false
| Some get -> get
let create ~enable abstract = register ~enable abstract; Flag abstract
let create_domain name enable values domain =
create ~enable { name; values = Single values; domain = Domain domain }
let restrict_loc = fun x -> x
let extend_loc = fun x -> x
open Value_parameters
(* Register standard domains over cvalues. *)
let make name enable = create_domain name enable (module Main_values.CVal)
let cvalue = make "cvalue" CvalueDomain.get (module Cvalue_domain.State)
let gauges = make "gauges" GaugesDomain.get (module Gauges_domain.D)
let inout = make "inout" InoutDomain.get (module Inout_domain.D)
let printer = make "printer" PrinterDomain.get (module Printer_domain)
let symbolic_locations =
make "symbolic_locations" SymbolicLocsDomain.get (module Symbolic_locs.D)
let sign =
create_domain "sign" SignDomain.get (module Sign_value) (module Sign_domain)
let bitwise =
create_domain "bitwise" BitwiseOffsmDomain.get
(module Offsm_value.Offsm) (module Offsm_domain.D)
let equality_domain =
{ name = "equality";
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
let register = Config.register
let dynamic_register = Config.dynamic_register
(* --- Building value abstractions ------------------------------------------ *)
(* -------------------------------------------------------------------------- *)
(* Cvalue Domain *)
(* -------------------------------------------------------------------------- *)
module Leaf_Value (V: Abstract_value.Leaf) = struct
include V
let structure = Abstract.Value.Leaf (V.key, (module V))
end
module Leaf_Domain (D: Abstract_domain.Leaf) = struct
include D
let structure = Abstract.Domain.Leaf (D.key, (module D))
end
(* Abstractions needed for the analysis: value, location and domain. *)
module type Abstract = sig
module Val : V
module type Acc = sig
module Val : Abstract.Value.External
module Loc : Abstract.Location.Internal with type value = Val.t
and type location = Precise_locs.precise_location
and type location = precise_loc
module Dom : Abstract.Domain.Internal 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 = Internal_PLoc
module Dom = Internal_Cvalue_Domain
end : Abstract)
else
(module struct
module Val = CVal
module Loc = Internal_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.CVal.key
end in
let module Conv = Convert (Val) (K) in
let module Loc = struct
include Location_lift.Make (Main_locations.PLoc) (Conv)
let structure = Abstract.Location.Leaf Internal_PLoc.key
end in
if config.cvalue
then
(module struct
module Val = Val
module Loc = Loc
module Dom = struct
include Domain_lift.Make (Cvalue_domain.State) (Conv)
let structure = Abstract.Domain.Leaf Internal_Cvalue_Domain.key
end
end : Abstract)
else
module 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
module Val = Val
module Loc = Loc
module Dom = Unit_domain.Make (Val) (Loc)
end : Abstract)
(* -------------------------------------------------------------------------- *)
(* Apron Domains *)
(* -------------------------------------------------------------------------- *)
let add_apron_domain abstract apron =
let module Acc = (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 (Acc.Val) (K) in
let module Apron = (val apron : Apron_domain.S) in
let structure = Abstract.Domain.Leaf Apron.key in
let module Apron = Domain_lift.Make (Apron) (Conv) in
(module struct
module Val = Acc.Val
module Loc = Acc.Loc
module Dom = struct
include Domain_product.Make (Acc.Val) (Acc.Dom) (Apron)
let structure = Abstract.Domain.(Node (Acc.Dom.structure, structure))
end
end : Abstract)
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
end
end
let dkey_experimental = Value_parameters.register_category "experimental-ok"
(* --- Building domain abstractions ----------------------------------------- *)
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."
module Lift_Domain
(Value: Abstract.Value.External)
(Domain: Abstract_domain.Leaf with type location = precise_loc)
(Struct: sig type v = Domain.value val s : v value end)
= struct
module Convert = struct
include Internal_Value.Convert (Value) (Struct)
(* -------------------------------------------------------------------------- *)
(* Equality Domain *)
(* -------------------------------------------------------------------------- *)
type extended_location = Main_locations.PLoc.location
module CvalueEquality = Equality_domain.Make (CVal)
let restrict_loc = fun x -> x
let extend_loc = fun x -> x
end
let add_generic_equalities (module Acc : Abstract) =
let module EqDom = Equality_domain.Make (Acc.Val) in
let module Dom = struct
include Domain_product.Make (Acc.Val) (Acc.Dom) (EqDom)
let structure = Abstract.Domain.(Node (Acc.Dom.structure, Leaf EqDom.key))
end in
(module struct
module Val = Acc.Val
module Loc = Acc.Loc
module Dom = Dom
end : Abstract)
let add_equalities (type v) (module Acc : Abstract with type Val.t = v) =
match Acc.Val.structure with
| Abstract.Value.Leaf key ->
begin
match Structure.Key_Value.eq_type key Main_values.CVal.key with
| None -> add_generic_equalities (module Acc)
| Some Structure.Eq ->
let module Dom = struct
include Domain_product.Make (Acc.Val) (Acc.Dom) (CvalueEquality)
let structure =
Abstract.Domain.(Node (Acc.Dom.structure, Leaf CvalueEquality.key))
include Domain_lift.Make (Domain) (Convert)
let key = Domain.key
end
module type internal_domain =
Abstract.Domain.Internal with type location = Precise_locs.precise_location
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) acc =
let module Acc = (val acc: Acc) in
let new_domain : (module leaf_domain with type value = Acc.Val.t) =
match abstraction.domain with
| Functor make ->
let module Make = (val make: domain_functor) in
(module Make (Acc.Val))
| Domain domain ->
match eq_value Acc.Val.structure abstraction.values with
| Some Structure.Eq -> domain
| None ->
let module Dom = (val domain : leaf_domain with type value = v) in
let module Struct = struct
type v = Dom.value
let s = abstraction.values
end in
(module struct
module Val = Acc.Val
module Loc = Acc.Loc
module Dom = Dom
end : Abstract)
end
| _ -> add_generic_equalities (module Acc)
(* -------------------------------------------------------------------------- *)
(* Offsetmap Domain *)
(* -------------------------------------------------------------------------- *)
let add_offsm abstract =
let module Acc = (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 (Acc.Val) (K) in
let module Offsm = Domain_lift.Make (Offsm_domain.D) (Conv) in
let module Dom = struct
include Domain_product.Make (Acc.Val) (Acc.Dom) (Offsm)
let structure =
Abstract.Domain.(Node (Acc.Dom.structure, Leaf Offsm_domain.D.key))
end in
(module Lift_Domain (Acc.Val) (Dom) (Struct))
in
let module Domain = (val new_domain) in
let module Domain = Leaf_Domain (Domain) in
let domain : (module internal_domain with type value = Acc.Val.t) =
match Acc.Dom.structure with
| Abstract.Domain.Unit -> (module Domain)
| s ->
(module struct
include Domain_product.Make (Acc.Val) (Acc.Dom) (Domain)
let structure = Abstract.Domain.Node (s, Domain.structure)
end)
in
(module struct
module Val = Acc.Val
module Loc = Acc.Loc
module Dom = Dom
end : Abstract)
module Dom = (val domain)
end : Acc)
(* -------------------------------------------------------------------------- *)
(* Domains on standard locations and values *)
(* -------------------------------------------------------------------------- *)
let build_domain config abstract =
let build (Config.Flag abstraction) acc = add_domain abstraction acc in
Config.fold build config abstract
module type Standard_abstraction = Abstract_domain.Leaf
with type value = Cvalue.V.t
and type location = Precise_locs.precise_location
let add_standard_domain d abstract =
let module Acc = (val abstract : Abstract) in
let module K = struct
type v = Cvalue.V.t
let key = Main_values.CVal.key
end in
let module Conv = Convert (Acc.Val) (K) in
let module D = (val d: Standard_abstraction) in
let module LD = Domain_lift.Make (D) (Conv) in
let module Dom = struct
include Domain_product.Make (Acc.Val)(Acc.Dom)(LD)
let structure =
Abstract.Domain.(Node (Acc.Dom.structure, Leaf D.key))
end in
(module struct
module Val = Acc.Val
module Loc = Acc.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 Acc = (val abstract : Abstract) in
let module K = struct
type v = Sign_value.t
let key = Sign_value.key
end in
let module Conv = Convert (Acc.Val) (K) in
let module Sign = Domain_lift.Make (Sign_domain) (Conv) in
let module Dom = struct
include Domain_product.Make (Acc.Val) (Acc.Dom) (Sign)
let structure =
Abstract.Domain.(Node (Acc.Dom.structure, Leaf Sign_domain.key))
end in
(module struct
module Val = Acc.Val
module Loc = Acc.Loc
module Dom = Dom
end : Abstract)
(* -------------------------------------------------------------------------- *)
(* Numerors Domain *)
(* -------------------------------------------------------------------------- *)
let add_errors abstract =
let module Acc = (val abstract : Abstract) in
let module K = struct
type v = Numerors_domain.value
let key = Numerors_domain.value_key
end in
let module Conv = Convert (Acc.Val) (K) in
let module Numerors = (val Numerors_domain.numerors_domain ()) in
let module Errors = Domain_lift.Make (Numerors) (Conv) in
let module Dom = struct
include Domain_product.Make (Acc.Val) (Acc.Dom) (Errors)
let structure =
Abstract.Domain.(Node (Acc.Dom.structure, Leaf Numerors.key))
end in
(module struct
module Val = Acc.Val
module Loc = Acc.Loc
module Dom = Dom
end : Abstract)
(* --- Value reduced product ----------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* Traces *)
(* -------------------------------------------------------------------------- *)
module type Value = sig
include Abstract.Value.External
val reduce : t -> t
end
let add_traces =
add_standard_domain (module Traces_domain.D)
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
(* -------------------------------------------------------------------------- *)
(* Printer *)
(* -------------------------------------------------------------------------- *)
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 add_printer =
add_standard_domain (module Printer_domain)
(* -------------------------------------------------------------------------- *)
(* Build Abstractions *)
(* -------------------------------------------------------------------------- *)
type ('a, 'b) value_reduced_product =
'a Abstract.Value.key * 'b Abstract.Value.key * ('a -> 'b -> 'a * 'b)
let build_abstractions config =
let value = build_value config in
let module V = (val value : V) in
let abstractions =
match V.structure with
| Abstract.Value.Leaf key
when Structure.Key_Value.equal key Main_values.CVal.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
type v_reduced_product = R: ('a, 'b) value_reduced_product -> v_reduced_product
let value_reduced_product = ref []
(* Add the reduce function to the value module. *)
module Reduce (Value : Abstract.Value.External) = struct
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
let ival = Cvalue.V.project_ival cvalue in
cvalue, (Some ival)
with Cvalue.V.Not_based_on_null -> cvalue, ival
end
| 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
(* 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.CVal.key with
| Some get_interval, Some get_cvalue ->
begin
let set_cvalue = Value.set Main_values.CVal.key in
let set_interval = Value.set Main_values.Interval.key in
fun t ->
match get_interval t with
| None -> begin
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 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 open_abstractions abstraction =
let module Acc = (val abstraction : Abstract) in
let module Val = Reduce (Acc.Val) in
let module Loc = struct
(* --- 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)
include Structure.Open (Abstract.Location)
(struct include Acc.Loc type t = location end)
end in
let module Domain = struct
end
module Dom = struct
include Acc.Dom
include Structure.Open (Abstract.Domain) (Acc.Dom)
end in
(module struct
module Val = Val
module Loc = Loc
module Dom = Domain
end : S)
let make config =
let abstractions = build_abstractions config in
open_abstractions abstractions
end
end
(* -------------------------------------------------------------------------- *)
(* Default and Legacy Abstractions *)
(* -------------------------------------------------------------------------- *)
module Unit_Acc (Value: Abstract.Value.External) : Acc = struct
module PLoc = Main_locations.PLoc
module Struct = struct
type v = Cvalue.V.t
let s = Single (module Main_values.CVal)
end
module Conv = Internal_Value.Convert (Value) (Struct)
module Val = Value
module Loc = struct
include Location_lift.Make (PLoc) (Conv)
let structure = Abstract.Location.Leaf (PLoc.key, (module PLoc))
end
module Dom = Unit_domain.Make (Value) (Loc)
end
module Legacy = (val make legacy_config)
module Default = (val make default_config)
let build_abstractions config =
let initial_value : (module Abstract.Value.Internal) =
if Config.mem Config.bitwise config
then (module Offsm_value.CvalueOffsm)
else (module Leaf_Value (Main_values.CVal))
in
let value = Internal_Value.build_values config initial_value in
let acc = (module Unit_Acc (val value): Acc) in
build_domain config acc
let configure = Config.configure
let make config =
let abstractions = build_abstractions config in
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)
src/plugins/value/engine/abstractions.mli
+ 99
− 51
View file @ 9772805f
......@@ -20,45 +20,77 @@
(* *)
(**************************************************************************)
(** 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. *)
type 'v abstraction =
{ name: string; (** Name of the abstraction. Must be unique. *)
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
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
......@@ -66,9 +98,7 @@ module type S = sig
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 +107,44 @@ 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.Leaf
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 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
src/plugins/value/engine/analysis.ml
+ 5
− 5
View file @ 9772805f
......@@ -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)
......@@ -139,8 +139,8 @@ let cvalue_initial_state () =
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. *)
......
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