diff --git a/Makefile b/Makefile
index 977133d5e9174b99399ca09663454ca41ffe7830..9e3ac8f0cafacd58b0c57683ce897f7783cb62fa 100644
--- a/Makefile
+++ b/Makefile
@@ -861,7 +861,7 @@ endif
# General rules for ordering files within PLUGIN_CMO:
# - try to keep the legacy Value before Eva
-PLUGIN_CMO:= partitioning/split_strategy value_parameters \
+PLUGIN_CMO:= partitioning/split_strategy domains/domain_mode value_parameters \
utils/value_perf utils/eva_annotations \
utils/value_util utils/red_statuses \
utils/mark_noresults \
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 2ada5971dd26cf43899de59b063ce5ae0a7d88f5..9c669cda9390d35e43e048e6019ba9aa82c09c84 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1224,6 +1224,8 @@ src/plugins/value/domains/cvalue/locals_scoping.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/cvalue/locals_scoping.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/cvalue/warn.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/cvalue/warn.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/domain_mode.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/value/domains/domain_mode.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/domain_builder.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/domain_builder.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/value/domains/domain_lift.ml: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index b8b6ee7d87af66a98e082b94a747271b4aafaf24..876e52a7428012dde40a3c9d51b2a4a1e8ad0563 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -254,45 +254,29 @@ end
(* -------------------------------------------------------------------------- *)
-type permission = { read: bool; write: bool; }
-type mode = { current: permission; calls: permission; }
-
-module Mode = struct
-
- let all =
- let p = { read = true; write = true } in
- { current = p; calls = p; }
-
-
- include Datatype.Make_with_collections
- (struct
- include Datatype.Serializable_undefined
- type t = mode
- let name = "Domain_builder.Restrict_State"
- let reprs = [ all ]
- let compare _ _ = 0
- let equal _ _ = true
- let hash _ = 0
- end)
-
- let merge f m1 m2 =
- let merge_perm p1 p2 =
- { read = f p1.read p2.read;
- write = f p1.write p2.write; }
- in
- { current = merge_perm m1.current m2.current;
- calls = merge_perm m1.calls m2.calls; }
-
- let join = merge (&&)
- let narrow = merge (||)
-end
-
module Restrict
(Value: Abstract_value.S)
(Domain: Abstract.Domain.Internal with type value = Value.t)
- (Scope: sig val functions: (Kernel_function.t * mode) list end)
+ (Scope: sig val functions: Domain_mode.function_mode list end)
= struct
+ open Domain_mode
+
+ module Mode = struct
+ include Mode
+
+ let merge f m1 m2 =
+ let merge_perm p1 p2 =
+ { read = f p1.read p2.read;
+ write = f p1.write p2.write; }
+ in
+ { current = merge_perm m1.current m2.current;
+ calls = merge_perm m1.calls m2.calls; }
+
+ let join = merge (&&)
+ let narrow = merge (||)
+ end
+
let functions_map =
List.fold_left
(fun map (kf, mode) -> Kernel_function.Map.add kf mode map)
diff --git a/src/plugins/value/domains/domain_builder.mli b/src/plugins/value/domains/domain_builder.mli
index f63aa2e6ded7d83ca69f3557686c92cd2e09ce61..718c0c5febdfddf28f144850e7d09c4d7f588087 100644
--- a/src/plugins/value/domains/domain_builder.mli
+++ b/src/plugins/value/domains/domain_builder.mli
@@ -56,17 +56,9 @@ module Complete_Simple_Cvalue
and type location = Precise_locs.precise_location
and type state = Domain.t
-
-type permission = { read: bool; write: bool; }
-type mode = { current: permission; calls: permission; }
-
-module Mode : sig
- val all: mode
-end
-
module Restrict
(Value: Abstract_value.S)
(Domain: Abstract.Domain.Internal with type value = Value.t)
- (Scope: sig val functions: (Kernel_function.t * mode) list end)
+ (Scope: sig val functions: Domain_mode.function_mode list end)
: Abstract.Domain.Internal with type value = Value.t
and type location = Domain.location
diff --git a/src/plugins/value/domains/domain_mode.ml b/src/plugins/value/domains/domain_mode.ml
new file mode 100644
index 0000000000000000000000000000000000000000..4363dba60257b8e84b8cc47c7b796e82b1db34d4
--- /dev/null
+++ b/src/plugins/value/domains/domain_mode.ml
@@ -0,0 +1,96 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+type permission = { read: bool; write: bool; }
+type mode = { current: permission; calls: permission; }
+
+type function_mode = Kernel_function.t * mode
+
+module Mode = struct
+ let all_permission = { read = true; write = true; }
+ let no_permission = { read = false; write = false; }
+
+ let default = { current = all_permission; calls = no_permission; }
+ let all = { current = all_permission; calls = all_permission; }
+ let none = { current = no_permission; calls = no_permission; }
+
+ include Datatype.Make_with_collections
+ (struct
+ include Datatype.Serializable_undefined
+ type t = mode
+ let name = "Domain_mode.Mode"
+ let reprs = [ default ]
+ let compare = Transitioning.Stdlib.compare
+ let equal = Datatype.from_compare
+ let hash = Hashtbl.hash
+ end)
+
+ let check str =
+ String.iter
+ (fun c ->
+ if Char.lowercase_ascii c <> 'r' && Char.lowercase_ascii c <> 'w'
+ then raise (Invalid_argument ("invalid mode " ^ str)))
+ str
+
+ let of_string str =
+ check str;
+ let calls =
+ { read = String.contains str 'R';
+ write = String.contains str 'W'; }
+ and current =
+ { read = String.contains str 'r';
+ write = String.contains str 'w'; }
+ in
+ { current; calls; }
+
+ let to_string t =
+ let string_if c b = if b then c else "" in
+ string_if "r" t.current.read ^ string_if "w" t.current.write ^
+ string_if "R" t.calls.read ^ string_if "W" t.calls.write
+end
+
+module Function_Mode = struct
+ include Datatype.Pair (Kernel_function) (Mode)
+ type key = string
+
+ let of_string ~key ~prev:_ str =
+ match str with
+ | None -> raise (Invalid_argument ("no value bound to " ^ key))
+ | Some str ->
+ let get_function str =
+ try Globals.Functions.find_by_name str
+ with Not_found -> raise (Invalid_argument ("no function " ^ str))
+ in
+ match String.split_on_char '-' str with
+ | [ kf; "" ] -> Some (get_function kf, Mode.none)
+ | _ ->
+ match String.split_on_char '+' str with
+ | [ kf ] -> Some (get_function kf, Mode.default)
+ | [ kf; "" ] -> Some (get_function kf, Mode.all)
+ | [ kf; mode ] -> Some (get_function kf, Mode.of_string mode)
+ | _ -> raise (Invalid_argument ("invalid argument " ^ str))
+
+ let to_string ~key:_ = function
+ | None -> None
+ | Some (kf, mode) ->
+ Some (Kernel_function.get_name kf ^ "+" ^ Mode.to_string mode)
+end
diff --git a/src/plugins/value/domains/domain_mode.mli b/src/plugins/value/domains/domain_mode.mli
new file mode 100644
index 0000000000000000000000000000000000000000..b56b75e73890cc55c0c916d499863e6060a7f891
--- /dev/null
+++ b/src/plugins/value/domains/domain_mode.mli
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+type permission = { read: bool; write: bool; }
+type mode = { current: permission; calls: permission; }
+
+module Mode : sig
+ include Datatype.S_with_collections with type t = mode
+ val all: t
+end
+
+type function_mode = Kernel_function.t * mode
+
+module Function_Mode:
+ Parameter_sig.Multiple_value_datatype with type key = string
+ and type t = function_mode
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 7c7e4524ac864fd00f7c1fe4af6d68daec1ed9ce..c231134e548eea4fea2d86a977f73a8a0a5d5097 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -85,12 +85,14 @@ module Config = struct
let configure () =
let aux config (Flag domain as flag) =
if Value_parameters.Domains.mem domain.name
+ || Value_parameters.DomainsFunction.mem domain.name
then add flag config
else config
in
let config = List.fold_left aux empty !abstractions in
let aux config (Dynamic { name; experimental; priority; abstraction; }) =
if Value_parameters.Domains.mem name
+ || Value_parameters.DomainsFunction.mem name
then
let abstraction = abstraction () in
let flag = Flag { name; experimental; priority; abstraction; } in
@@ -307,7 +309,7 @@ let eq_value:
| Abstract.Value.Leaf (key, _) -> Abstract.Value.eq_type key V.key
| _ -> None
-let add_domain (type v) (abstraction: v abstraction) (module Acc: Acc) =
+let add_domain (type v) name (abstraction: v abstraction) (module Acc: Acc) =
let domain : (module internal_domain with type value = Acc.Val.t) =
match abstraction.domain with
| Functor make ->
@@ -327,6 +329,19 @@ let add_domain (type v) (abstraction: v abstraction) (module Acc: Acc) =
let module Convert = Internal_Value.Convert (Acc.Val) (Struct) in
(module Domain_lift.Make (Domain) (Convert))
in
+ let domain : (module internal_domain with type value = Acc.Val.t) =
+ try
+ let kf_modes = Value_parameters.DomainsFunction.find name in
+ let module Scope = struct let functions = kf_modes end in
+ let module Domain =
+ Domain_builder.Restrict
+ (Acc.Val)
+ ((val domain))
+ (Scope)
+ in
+ (module Domain)
+ with Not_found -> domain
+ in
let domain : (module internal_domain with type value = Acc.Val.t) =
match Abstract.Domain.(eq_structure Acc.Dom.structure Unit) with
| Some _ -> domain
@@ -349,7 +364,7 @@ let warn_experimental flag =
let build_domain config abstract =
let build (Flag flag) acc =
warn_experimental flag;
- add_domain flag.abstraction acc
+ add_domain flag.name 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
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 70311f618f178f9f657a7a05ea338807f30a14d1..bbe2cb24f8be0976029f6d00fac8af91f560821c 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -213,9 +213,31 @@ let () =
Domains.add_set_hook
(fun _old domains -> Datatype.String.Set.iter check_domain domains)
+let () = Parameter_customize.set_group domains
+module DomainsFunction =
+ String_multiple_map
+ (struct
+ include Domain_mode.Function_Mode
+ let of_string ~key ~prev str =
+ check_domain key;
+ try of_string ~key ~prev str
+ with Invalid_argument msg -> raise (Cannot_build msg)
+ end)
+ (struct
+ let option_name = "-eva-domains-function"
+ let help = "Enables a domain only for the given functions. \
+ <d:f+> enables the domain [d] from function [f] \
+ (the domain is enabled in all functions called from [f]). \
+ <d:f-> disables the domain [d] from function [f]."
+ let arg_name = "d:f"
+ let default = Datatype.String.Map.empty
+ end)
+let () = add_precision_dep DomainsFunction.parameter
+
(* Set of parameters defining the abstractions used in an Eva analysis. *)
let parameters_abstractions =
- ref (Typed_parameter.Set.singleton Domains.parameter)
+ ref (Typed_parameter.Set.of_list
+ [Domains.parameter; DomainsFunction.parameter])
let () = Parameter_customize.set_group domains
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 8c338bbc48c349b742d7af40e1ae39b0e4a580b8..828113a3c87ef0927de1d90ebda9ca0fe3ee5ca0 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -29,6 +29,9 @@ module OracleDepth: Parameter_sig.Int
module ReductionDepth: Parameter_sig.Int
module Domains: Parameter_sig.String_set
+module DomainsFunction: Parameter_sig.Multiple_map
+ with type key = string
+ and type value = Domain_mode.function_mode
module EqualityCall: Parameter_sig.String
module EqualityCallFunction: