Commit 248be1c3 authored by David Bühler's avatar David Bühler Committed by Andre Maroneze
Browse files

[Eva] New option -eva-domains-function to enable domains on specific functions.

parent bf4350cc
......@@ -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 \
......
......@@ -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
......
......@@ -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)
......
......@@ -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
(**************************************************************************)
(* *)
(* 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
(**************************************************************************)
(* *)
(* 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
......@@ -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
......
......@@ -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
......
......@@ -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:
......
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