diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli index 7ee21c551d305b60cadca7ec6460b7d37f67b24b..5783238d0d87d5c6ba5bf5848dd08b4db256046a 100644 --- a/src/plugins/eva/Eva.mli +++ b/src/plugins/eva/Eva.mli @@ -178,6 +178,47 @@ module Callstack: sig end +module Deps: sig + + (** Memory dependencies of an expression. *) + type t = Function_Froms.Deps.deps = { + data: Locations.Zone.t; + (** Memory zone directly required to evaluate the given expression. *) + indirect: Locations.Zone.t; + (** Memory zone read to compute data addresses. *) + } + + include Datatype.S with type t := t + + val pretty_debug: Format.formatter -> t -> unit + + (* Constructors *) + + val top : t + val bottom : t + val data : Locations.Zone.t -> t + val indirect : Locations.Zone.t -> t + + (* Conversion *) + + val to_zone : t -> Locations.Zone.t + + (* Mutators *) + + val add_data : t -> Locations.Zone.t -> t + val add_indirect : t -> Locations.Zone.t -> t + + (* Map *) + + val map : (Locations.Zone.t -> Locations.Zone.t) -> t -> t + + (* Lattice operators *) + + val is_included : t -> t -> bool + val join : t -> t -> t + val narrow : t -> t -> t +end + module Results: sig (** Eva's result API is a new interface to access the results of an analysis, @@ -335,14 +376,6 @@ module Results: sig evaluate the given lvalue, excluding the lvalue zone itself. *) val address_deps : Cil_types.lval -> request -> Locations.Zone.t - (** Memory dependencies of an expression. *) - type deps = Function_Froms.Deps.deps = { - data: Locations.Zone.t; - (** Memory zone directly required to evaluate the given expression. *) - indirect: Locations.Zone.t; - (** Memory zone read to compute data addresses. *) - } - (** Taint of a memory zone, according to the taint domain. *) type taint = | Direct @@ -361,7 +394,7 @@ module Results: sig (** Computes (an overapproximation of) the memory dependencies of an expression. *) - val expr_dependencies : Cil_types.exp -> request -> deps + val expr_dependencies : Cil_types.exp -> request -> Deps.t (** Evaluation *) diff --git a/src/plugins/eva/api/general_requests.ml b/src/plugins/eva/api/general_requests.ml index 3015cbcf1564ee2332cac2973c08abf0289588dd..3666a0c4345da0dbe0554481a50459fd1dd98453 100644 --- a/src/plugins/eva/api/general_requests.ml +++ b/src/plugins/eva/api/general_requests.ml @@ -327,7 +327,7 @@ module EvaTaints = struct let evaluate expr request = let (let+) = Option.bind in - let { data ; indirect } = expr_dependencies expr request in + let Deps.{ data ; indirect } = expr_dependencies expr request in let+ data = is_tainted data request |> Result.to_option in let+ indirect = is_tainted indirect request |> Result.to_option in Some (data, indirect) diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune index 66e75d5fb6c5738a5fac9570a71e8c8c1743dce1..72c9794026a8ffa276dce764e63e3420a14e35ea 100644 --- a/src/plugins/eva/dune +++ b/src/plugins/eva/dune @@ -112,7 +112,7 @@ (mode (promote (only Eva.mli))) (deps gen-api.sh Eva.header - engine/analysis.mli types/callstack.mli utils/results.mli parameters.mli + engine/analysis.mli types/callstack.mli types/deps.mli utils/results.mli parameters.mli utils/eva_annotations.mli eval.mli domains/cvalue/builtins.mli utils/cvalue_callbacks.mli legacy/logic_inout.mli utils/eva_results.mli utils/unit_tests.mli) diff --git a/src/plugins/eva/types/deps.mli b/src/plugins/eva/types/deps.mli index 9c3682e139c54655ba598634722c346a47839174..922e8e622ad8090b54aabbb30c29012b58791453 100644 --- a/src/plugins/eva/types/deps.mli +++ b/src/plugins/eva/types/deps.mli @@ -20,6 +20,8 @@ (* *) (**************************************************************************) +[@@@ api_start] + (** Memory dependencies of an expression. *) type t = Function_Froms.Deps.deps = { data: Locations.Zone.t; @@ -57,3 +59,4 @@ val map : (Locations.Zone.t -> Locations.Zone.t) -> t -> t val is_included : t -> t -> bool val join : t -> t -> t val narrow : t -> t -> t +[@@@ api_end] diff --git a/src/plugins/eva/utils/results.ml b/src/plugins/eva/utils/results.ml index 297a2b22d2edf20faaac55e7e7c4e5a6443e824d..0df27562e45c83d92c131f8e32b81caa27d8889e 100644 --- a/src/plugins/eva/utils/results.ml +++ b/src/plugins/eva/utils/results.ml @@ -733,11 +733,6 @@ let address_deps lval request = let lval_to_loc lv = eval_address lv request |> as_precise_loc in Eva_utils.indirect_zone_of_lval lval_to_loc lval -type deps = Function_Froms.Deps.deps = { - data: Locations.Zone.t; - indirect: Locations.Zone.t; -} - let expr_dependencies expr request = let lval_to_loc lv = eval_address lv request |> as_precise_loc in Eva_utils.deps_of_expr lval_to_loc expr diff --git a/src/plugins/eva/utils/results.mli b/src/plugins/eva/utils/results.mli index b091f95830f1e2c6846970a94b84bbafc81e4072..c68373ebcb4157a8312dfefb59b6f0467863d320 100644 --- a/src/plugins/eva/utils/results.mli +++ b/src/plugins/eva/utils/results.mli @@ -177,14 +177,6 @@ val lval_deps : Cil_types.lval -> request -> Locations.Zone.t evaluate the given lvalue, excluding the lvalue zone itself. *) val address_deps : Cil_types.lval -> request -> Locations.Zone.t -(** Memory dependencies of an expression. *) -type deps = Function_Froms.Deps.deps = { - data: Locations.Zone.t; - (** Memory zone directly required to evaluate the given expression. *) - indirect: Locations.Zone.t; - (** Memory zone read to compute data addresses. *) -} - (** Taint of a memory zone, according to the taint domain. *) type taint = | Direct @@ -203,7 +195,7 @@ val is_tainted : Locations.Zone.t -> request -> (taint, error) Result.t (** Computes (an overapproximation of) the memory dependencies of an expression. *) -val expr_dependencies : Cil_types.exp -> request -> deps +val expr_dependencies : Cil_types.exp -> request -> Deps.t (** Evaluation *)