diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 5f683ec3aac7447bb9548056c53a03f26685449c..7ddec87ce11c0f34b1fd06245e68bab3f115557c 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -181,7 +181,7 @@ end
module Deps: sig
(** Memory dependencies of an expression. *)
- type t = Function_Froms.Deps.deps = {
+ type t = {
data: Locations.Zone.t;
(** Memory zone directly required to evaluate the given expression. *)
indirect: Locations.Zone.t;
@@ -634,6 +634,138 @@ module Eval: sig
callers, can be cached. *)
end
+module Froms: sig
+
+ module DepsOrUnassigned : sig
+
+ type deps_or_unassigned =
+ | DepsBottom (** Bottom of the lattice, never bound inside a memory state
+ at a valid location. (May appear for bases for which the
+ validity does not start at 0, currently only NULL.) *)
+ | Unassigned (** Location has never been assigned *)
+ | AssignedFrom of Deps.t (** Location guaranteed to have been overwritten,
+ its contents depend on the [Deps.t] value *)
+ | MaybeAssignedFrom of Deps.t (** Location may or may not have been
+ overwritten *)
+ (** The lattice is [DepsBottom <= Unassigned], [DepsBottom <= AssignedFrom z],
+ [Unassigned <= MaybeAssignedFrom] and
+ [AssignedFrom z <= MaybeAssignedFrom z]. *)
+
+ include Lmap_bitwise.With_default with type t = deps_or_unassigned
+
+ val subst: (Deps.t -> Deps.t) -> t -> t
+
+ val extract_data: t -> Locations.Zone.t
+ val extract_indirect: t -> Locations.Zone.t
+
+ val may_be_unassigned: t -> bool
+
+ val compose: t -> t -> t
+ (** [compose d1 d2] is the sequential composition of [d1] after [d2], ie.
+ the dependencies needed to execute [d1] after having executed [d2].
+ It is computed as [d1] if [d1 = AssignedFrom _] (as executing [d1]
+ completely overwrites what [d2] wrote), and as a partial join between
+ [d1] and [d2] in the other cases. *)
+
+ val pretty_precise : Format.formatter -> t -> unit
+
+ val to_zone: t -> Locations.Zone.t
+ val to_deps: t -> Deps.t
+ end
+
+ module Memory : sig
+ include Lmap_bitwise.Location_map_bitwise with type v = DepsOrUnassigned.t
+
+ (** Prints the detail of address and data dependencies, as opposed to [pretty]
+ that prints the backwards-compatible union of them *)
+ val pretty_ind_data : Format.formatter -> t -> unit
+
+ val find: t -> Locations.Zone.t -> Locations.Zone.t
+ (** Imprecise version of find, in which data and indirect dependencies are
+ not distinguished *)
+
+ val find_precise: t -> Locations.Zone.t -> Deps.t
+ (** Precise version of find *)
+
+ val add_binding: exact:bool -> t -> Locations.Zone.t -> Deps.t -> t
+ val add_binding_loc: exact:bool -> t -> Locations.location -> Deps.t -> t
+ val add_binding_precise_loc:
+ exact:bool -> Locations.access -> t ->
+ Precise_locs.precise_location -> Deps.t -> t
+ val bind_var: Cil_types.varinfo -> Deps.t -> t -> t
+ val unbind_var: Cil_types.varinfo -> t -> t
+
+ val map: (DepsOrUnassigned.t -> DepsOrUnassigned.t) -> t -> t
+
+ val compose: t -> t -> t
+ (** Sequential composition. See {!DepsOrUnassigned.compose}. *)
+
+ val substitute: t -> Deps.t -> Deps.t
+ (** [substitute m d] applies [m] to [d] so that any dependency in [d] is
+ expressed using the dependencies already present in [m]. For example,
+ [substitute 'x From y' 'x'] returns ['y']. *)
+
+
+ (** Dependencies for [\result]. *)
+
+ type return = Deps.t
+ (* Currently, this type is equal to [Deps.t]. However, some of the functions
+ below are more precise, and will be more useful when 'return' are
+ represented by a precise offsetmap. *)
+
+ (** Default value to use for storing the dependencies of [\result] *)
+ val default_return: return
+
+ (** Completely imprecise return *)
+ val top_return: return
+
+ (** Completely imprecise return of the given size *)
+ val top_return_size: Int_Base.t -> return
+
+ (** Add some dependencies to [\result], between bits [start] and
+ [start+size-1], to the [Deps.t] value; default value for [start] is 0.
+ If [m] is specified, the dependencies are added to it. Otherwise,
+ {!default_return} is used. *)
+ val add_to_return:
+ ?start:int -> size:Int_Base.t -> ?m:return -> Deps.t -> return
+
+ val collapse_return: return -> Deps.t
+ end
+
+
+
+ type t = {
+ deps_return : Memory.return
+ (** Dependencies for the returned value *);
+ deps_table : Memory.t
+ (** Dependencies on all the zones modified by the function *);
+ }
+
+ include Datatype.S with type t := t
+
+ val join: t -> t -> t
+
+ val top: t
+
+ (** Display dependencies of a function, using the function's type to improve
+ readability *)
+ val pretty_with_type: Cil_types.typ -> t Pretty_utils.formatter
+
+ (** Display dependencies of a function, using the function's type to improve
+ readability, separating direct and indirect dependencies *)
+ val pretty_with_type_indirect: Cil_types.typ -> t Pretty_utils.formatter
+
+ (** Extract the left part of a from result, ie. the zones that are written *)
+ val outputs: t -> Locations.Zone.t
+
+ (** Extract the right part of a from result, ie. the zones on which the
+ written zones depend. If [include_self] is true, and the from is
+ of the form [x FROM y (and SELF)], [x] is added to the result;
+ default value is [false]. *)
+ val inputs: ?include_self:bool -> t -> Locations.Zone.t
+
+end
+
module Builtins: sig
(** Eva analysis builtins for the cvalue domain, more efficient than their
@@ -658,7 +790,7 @@ module Builtins: sig
c_clobbered: Base.SetLattice.t;
(** An over-approximation of the bases in which addresses of local variables
might have been written *)
- c_from: (Function_Froms.froms * Locations.Zone.t) option;
+ c_from: (Froms.t * Locations.Zone.t) option;
(** If not None, the froms of the function, and its sure outputs;
i.e. the dependencies of the result and of each zone written to. *)
}
@@ -709,7 +841,7 @@ module Cvalue_callbacks: sig
(** If not None, the froms of the function, and its sure outputs;
i.e. the dependencies of the result, and the dependencies
of each zone written to. *)
- type call_froms = (Function_Froms.froms * Locations.Zone.t) option
+ type call_froms = (Froms.t * Locations.Zone.t) option
type analysis_kind =
[ `Builtin (** A cvalue builtin is used to interpret the function. *)
@@ -804,7 +936,7 @@ module Logic_inout: sig
and compare them with the given froms (computed by the from plugin).
Emits warnings if needed, and sets statuses to the assigns clauses. *)
val verify_assigns:
- Cil_types.kernel_function -> pre:Cvalue.Model.t -> Function_Froms.froms -> unit
+ Cil_types.kernel_function -> pre:Cvalue.Model.t -> Froms.t -> unit
(** [accept_base ~formals ~locals kf b] returns [true] if and only if [b] is:
diff --git a/src/plugins/eva/domains/cvalue/builtins.ml b/src/plugins/eva/domains/cvalue/builtins.ml
index b128b35eed8387cf041c595f1438392a8f0bc3e9..8990420a0c8c70c1f671d24d1674b51c6a7254af 100644
--- a/src/plugins/eva/domains/cvalue/builtins.ml
+++ b/src/plugins/eva/domains/cvalue/builtins.ml
@@ -31,7 +31,7 @@ type cacheable = Eval.cacheable = Cacheable | NoCache | NoCacheCallers
type full_result = {
c_values: (Cvalue.V.t option * Cvalue.Model.t) list;
c_clobbered: Base.SetLattice.t;
- c_from: (Function_Froms.froms * Locations.Zone.t) option;
+ c_from: (Froms.t * Locations.Zone.t) option;
}
type call_result =
diff --git a/src/plugins/eva/domains/cvalue/builtins.mli b/src/plugins/eva/domains/cvalue/builtins.mli
index 1d25c32aff6cc28b5391b25368b0c3a52dce20dc..a95ff2ce8e76dbb1b0dfc6ec571e3112838d5051 100644
--- a/src/plugins/eva/domains/cvalue/builtins.mli
+++ b/src/plugins/eva/domains/cvalue/builtins.mli
@@ -44,7 +44,7 @@ type full_result = {
c_clobbered: Base.SetLattice.t;
(** An over-approximation of the bases in which addresses of local variables
might have been written *)
- c_from: (Function_Froms.froms * Locations.Zone.t) option;
+ c_from: (Froms.t * Locations.Zone.t) option;
(** If not None, the froms of the function, and its sure outputs;
i.e. the dependencies of the result and of each zone written to. *)
}
diff --git a/src/plugins/eva/domains/cvalue/builtins_malloc.ml b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
index 77b26cbe8cc5bcb6e6cd6812c283f612ecb56eed..3d5c3245d70535aa716a310b4e10168fe248b4ce 100644
--- a/src/plugins/eva/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
@@ -579,9 +579,8 @@ let free ~exact bases state =
Locals_scoping.make_escaping ~exact ~escaping ~on_escaping ~within state
in
let from_changed =
- let open Function_Froms in
- let m = Memory.(add_binding ~exact empty !changed Deps.bottom) in
- { deps_table = m; deps_return = Deps.bottom }
+ let m = Froms.Memory.(add_binding ~exact empty !changed Deps.bottom) in
+ Froms.{ deps_table = m; deps_return = Deps.bottom }
in
state, (from_changed, if exact then !changed else Zone.bottom)
diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index c9d89b45120c756e9139086caca3a70f1b5a30c4..182171223f8e100043181004e3aaa2745e6731ca 100644
--- a/src/plugins/eva/domains/cvalue/builtins_memory.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_memory.ml
@@ -74,7 +74,7 @@ let frama_c_offset _state = function
let () = register_builtin "Frama_C_offset" frama_c_offset
-exception Memcpy_result of (Cvalue.Model.t * Function_Froms.froms * Zone.t)
+exception Memcpy_result of (Cvalue.Model.t * Froms.t * Zone.t)
exception Indeterminate of V_Or_Uninitialized.t
@@ -97,11 +97,10 @@ let memcpy_check_indeterminate_offsetmap offsm =
(* Create a dependency [\from arg_n] where n is the nth argument of the
currently called function. *)
let deps_nth_arg n =
- let open Function_Froms in
let kf = Callstack.top_kf (Eva_utils.current_call_stack ()) in
try
let vi = List.nth (Kernel_function.get_formals kf) n in
- Deps.add_data_dep Deps.bottom (Locations.zone_of_varinfo vi)
+ Deps.add_data Deps.bottom (Locations.zone_of_varinfo vi)
with Failure _ -> Kernel.fatal "%d arguments expected" n
@@ -126,7 +125,7 @@ let frama_c_memcpy name state actuals =
in
let deps_return = deps_nth_arg 0 in
let empty_cfrom =
- Function_Froms.({ deps_table = Memory.empty; deps_return })
+ Froms.{ deps_table = Memory.empty; deps_return }
in
let precise_copy state =
(* First step: copy the bytes we are sure to copy *)
@@ -155,15 +154,15 @@ let frama_c_memcpy name state actuals =
imprecision of the value analysis here. *)
let exact = Location_Bits.cardinal_zero_or_one dst_bits in
let deps_table =
- Function_Froms.Memory.add_binding ~exact
- Function_Froms.Memory.empty zone_dst deps in
+ Froms.Memory.add_binding ~exact Froms.Memory.empty zone_dst deps
+ in
let sure_zone = if exact then zone_dst else Zone.bottom in
(deps_table, sure_zone)
in
new_state, deps_table, sure_zone
end
else (* Nothing certain can be copied *)
- (state, Function_Froms.Memory.empty, Zone.bottom)
+ (state, Froms.Memory.empty, Zone.bottom)
in
let imprecise_copy new_state precise_deps_table sure_zone =
(* Second step. Size is imprecise, we will now copy some bits
@@ -193,11 +192,10 @@ let frama_c_memcpy name state actuals =
let zone_src = enumerate_valid_bits Locations.Read loc_src in
let zone_dst = enumerate_valid_bits Locations.Write loc_dst in
let deps = Deps.data zone_src in
- let open Function_Froms in
let deps_table =
- Memory.add_binding ~exact:false precise_deps_table zone_dst deps
+ Froms.Memory.add_binding ~exact:false precise_deps_table zone_dst deps
in
- { deps_table; deps_return }
+ Froms.{ deps_table; deps_return }
in
try
(* We try to iter on all the slices inside the value of slice.
@@ -274,9 +272,10 @@ let frama_c_memcpy name state actuals =
raise (Memcpy_result (state, empty_cfrom, Zone.bottom));
let (precise_state,precise_deps_table,sure_zone) = precise_copy state in
if Option.fold ~none:false ~some:(Int.equal min) max then
- (let open Function_Froms in
- let c_from = { deps_table = precise_deps_table; deps_return } in
- raise (Memcpy_result (precise_state, c_from, sure_zone)));
+ begin
+ let c_from = Froms.{ deps_table = precise_deps_table; deps_return } in
+ raise (Memcpy_result (precise_state, c_from, sure_zone))
+ end;
imprecise_copy precise_state precise_deps_table sure_zone
with
| Memcpy_result (new_state,c_from,sure_zone) ->
@@ -361,16 +360,16 @@ let frama_c_memset_imprecise state dst_lval dst v size =
with Not_found -> (new_state,Zone.bottom) (* from find_lonely_key + explicit raise *)
in
let c_from =
- let open Function_Froms in
let value_dep = deps_nth_arg 1 in
+ let empty = Froms.Memory.empty in
let deps_table =
- Memory.add_binding ~exact:false Memory.empty over_zone value_dep
+ Froms.Memory.add_binding ~exact:false empty over_zone value_dep
in
let deps_table =
- Memory.add_binding ~exact:true deps_table sure_zone value_dep
+ Froms.Memory.add_binding ~exact:true deps_table sure_zone value_dep
in
let deps_return = deps_nth_arg 0 in
- { deps_table; deps_return }
+ Froms.{ deps_table; deps_return }
in
Builtins.Full
{ Builtins.c_values = [Some dst, new_state'];
@@ -573,15 +572,14 @@ let frama_c_memset_precise state dst_lval dst v (exp_size, size) =
let dst_loc = Locations.loc_bytes_to_loc_bits dst in
let (c_from,dst_zone) =
let input = deps_nth_arg 1 in
- let open Function_Froms in
let size_bits = Integer.mul size (Bit_utils.sizeofchar ())in
let dst_location = Locations.make_loc dst_loc (Int_Base.Value size_bits) in
let dst_zone = Locations.(enumerate_valid_bits Write dst_location) in
let deps_table =
- Function_Froms.Memory.add_binding ~exact:true
- Function_Froms.Memory.empty dst_zone input in
+ Froms.Memory.add_binding ~exact:true Froms.Memory.empty dst_zone input
+ in
let deps_return = deps_nth_arg 0 in
- let c_from = { deps_table; deps_return } in
+ let c_from = Froms.{ deps_table; deps_return } in
c_from,dst_zone
in
let _ = c_from in
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index 72c9794026a8ffa276dce764e63e3420a14e35ea..a828561d21824a349f0f222e217576eeceb50f34 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -113,7 +113,8 @@
(deps
gen-api.sh Eva.header
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/eva_annotations.mli eval.mli types/froms.mli
+ domains/cvalue/builtins.mli utils/cvalue_callbacks.mli legacy/logic_inout.mli
+ utils/eva_results.mli
utils/unit_tests.mli)
(action (run bash %{deps})))
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 88b6280b2e75a83b72bf2a90b23921754ba17269..7e02649b28a12c7f8526a6eea4732484e09ddde9 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -35,7 +35,7 @@ let clear_caches () =
Cvalue.Model.clear_caches ();
Locations.Location_Bytes.clear_caches ();
Locations.Zone.clear_caches ();
- Function_Froms.Memory.clear_caches ()
+ Froms.Memory.clear_caches ()
let () = State.add_hook_on_update Self.state clear_caches
diff --git a/src/plugins/eva/gui/gui_eval.ml b/src/plugins/eva/gui/gui_eval.ml
index 3205c66f1626cdcf9cfbafd72be6a11af0af5b2c..bee771c2d1f03c870818a8f36f27e766dfa7969a 100644
--- a/src/plugins/eva/gui/gui_eval.ml
+++ b/src/plugins/eva/gui/gui_eval.ml
@@ -86,7 +86,7 @@ let clear_caches () =
Cvalue.Model.clear_caches ();
Locations.Location_Bytes.clear_caches ();
Locations.Zone.clear_caches ();
- Function_Froms.Memory.clear_caches ()
+ Froms.Memory.clear_caches ()
module type S = sig
module Analysis : Analysis.S
diff --git a/src/plugins/eva/legacy/logic_inout.ml b/src/plugins/eva/legacy/logic_inout.ml
index e1239bd8a790afd2dc0b7c0f75b064666f05aa2b..4c1a07385881578a2b1fbcec1fd9ab11f7ccb533 100644
--- a/src/plugins/eva/legacy/logic_inout.ml
+++ b/src/plugins/eva/legacy/logic_inout.ml
@@ -150,11 +150,10 @@ let eval_assigns_from pre_state it =
let check_from pre_state asgn assigns_zone from found_froms =
let open Locations in
let found_deps =
- let open Function_Froms in
if Logic_utils.is_result asgn.it_content then
- found_froms.deps_return
+ found_froms.Froms.deps_return
else
- Memory.find_precise found_froms.deps_table assigns_zone
+ Froms.Memory.find_precise found_froms.deps_table assigns_zone
in
let (indirect_deps,direct_deps) =
let filter x = List.mem "indirect" x.it_content.term_name in
@@ -214,7 +213,7 @@ let check_fct_assigns kf ab ~pre_state found_froms =
let behaviors = Annotations.behaviors kf in
(* Under-approximation of the union. *)
let link zones = List.fold_left Zone.link Zone.bottom zones in
- let outputs = Function_Froms.outputs found_froms in
+ let outputs = Froms.outputs found_froms in
let check_for_behavior b =
let activity = Active_behaviors.is_active ab b in
match activity with
diff --git a/src/plugins/eva/legacy/logic_inout.mli b/src/plugins/eva/legacy/logic_inout.mli
index ddec2c39239451d647383b453d55c3800a534a7c..d55e8ccd6ef71ddd0c035f61a2dba75f8467d227 100644
--- a/src/plugins/eva/legacy/logic_inout.mli
+++ b/src/plugins/eva/legacy/logic_inout.mli
@@ -66,7 +66,7 @@ val assigns_tlval_to_zones:
and compare them with the given froms (computed by the from plugin).
Emits warnings if needed, and sets statuses to the assigns clauses. *)
val verify_assigns:
- Cil_types.kernel_function -> pre:Cvalue.Model.t -> Function_Froms.froms -> unit
+ Cil_types.kernel_function -> pre:Cvalue.Model.t -> Froms.t -> unit
(** [accept_base ~formals ~locals kf b] returns [true] if and only if [b] is:
diff --git a/src/plugins/eva/types/deps.ml b/src/plugins/eva/types/deps.ml
index bfd9904fecca0b2be9dbbaa825a663f56526bd64..2f6bad3f7a3fd2b6929de54743354bf3c206498f 100644
--- a/src/plugins/eva/types/deps.ml
+++ b/src/plugins/eva/types/deps.ml
@@ -22,7 +22,7 @@
module Zone = Locations.Zone
-type deps = Function_Froms.Deps.deps = {
+type deps = {
data: Zone.t;
indirect: Zone.t;
}
diff --git a/src/plugins/eva/types/deps.mli b/src/plugins/eva/types/deps.mli
index e63413d1d8757e52e986f39415ffc34526595403..a30399e8e540450f5be762e719d3ffd86db01176 100644
--- a/src/plugins/eva/types/deps.mli
+++ b/src/plugins/eva/types/deps.mli
@@ -23,7 +23,7 @@
[@@@ api_start]
(** Memory dependencies of an expression. *)
-type t = Function_Froms.Deps.deps = {
+type t = {
data: Locations.Zone.t;
(** Memory zone directly required to evaluate the given expression. *)
indirect: Locations.Zone.t;
diff --git a/src/kernel_services/abstract_interp/function_Froms.ml b/src/plugins/eva/types/froms.ml
similarity index 84%
rename from src/kernel_services/abstract_interp/function_Froms.ml
rename to src/plugins/eva/types/froms.ml
index f6f2f5e8a931121cbb58b2d66caf6c5fdaa4e3e5..d9adc49442dd575a1fd27fab4db657b782e907a0 100644
--- a/src/kernel_services/abstract_interp/function_Froms.ml
+++ b/src/plugins/eva/types/froms.ml
@@ -22,107 +22,6 @@
open Locations
-module Deps =
-struct
-
- type deps = {
- data: Zone.t;
- indirect: Zone.t;
- }
-
- let to_zone {data; indirect} = Zone.join data indirect
-
- module DatatypeFromDeps = Datatype.Make(struct
- type t = deps
-
- let name = "Function_Froms.Deps.from_deps"
-
- let hash fd =
- Zone.hash fd.data + 37 * Zone.hash fd.indirect
-
- let compare fd1 fd2 =
- let c = Zone.compare fd1.data fd2.data in
- if c <> 0 then c
- else Zone.compare fd1.indirect fd2.indirect
-
- let equal = Datatype.from_compare
-
- let pretty fmt d = Zone.pretty fmt (to_zone d)
-
- let reprs =
- List.map (fun z -> {data = z; indirect = z}) Zone.reprs
-
- let structural_descr =
- Structural_descr.t_record [| Zone.packed_descr; Zone.packed_descr; |]
- let rehash = Datatype.identity
-
- let mem_project = Datatype.never_any_project
-
- let copy = Datatype.undefined
- end)
-
- include DatatypeFromDeps
-
- let pretty_precise fmt {data; indirect} =
- let bottom_data = Zone.is_bottom data in
- let bottom_indirect = Zone.is_bottom indirect in
- match bottom_indirect, bottom_data with
- | true, true ->
- Format.fprintf fmt "\\nothing"
- | true, false ->
- Format.fprintf fmt "direct: %a"
- Zone.pretty data
- | false, true ->
- Format.fprintf fmt "indirect: %a"
- Zone.pretty indirect
- | false, false ->
- Format.fprintf fmt "indirect: %a; direct: %a"
- Zone.pretty indirect
- Zone.pretty data
-
- let from_data_deps z = { data = z; indirect = Zone.bottom }
- let from_indirect_deps z = { data = Zone.bottom; indirect = z }
-
- let bottom = {
- data = Zone.bottom;
- indirect = Zone.bottom;
- }
-
- let top = {
- data = Zone.top;
- indirect = Zone.top;
- }
-
- let is_included fd1 fd2 =
- Zone.is_included fd1.data fd2.data &&
- Zone.is_included fd1.indirect fd2.indirect
-
- let join fd1 fd2 =
- if fd1 == bottom then fd2
- else if fd2 == bottom then fd1
- else {
- data = Zone.join fd1.data fd2.data;
- indirect = Zone.join fd1.indirect fd2.indirect
- }
-
- let narrow fd1 fd2 = {
- data = Zone.narrow fd1.data fd2.data;
- indirect = Zone.narrow fd1.indirect fd2.indirect
- }
-
- let add_data_dep fd data =
- { fd with data = Zone.join fd.data data }
-
- let add_indirect_dep fd indirect =
- { fd with indirect = Zone.join fd.indirect indirect }
-
- let map f fd = {
- data = f fd.data;
- indirect = f fd.indirect;
- }
-
-end
-
module DepsOrUnassigned = struct
type deps_or_unassigned =
@@ -310,7 +209,7 @@ module Memory = struct
(** Once the base is known, we can obtain something of type [Deps.t] *)
let convert_find_offsm base fp =
let z = Zone.inject base fp.fo_itvs in
- Deps.add_data_dep fp.fo_deps z
+ Deps.add_data fp.fo_deps z
let empty_find_offsm = {
fo_itvs = Int_Intervals.bottom;
@@ -354,7 +253,7 @@ module Memory = struct
let conv = convert_find_offsm in
(* We are querying a zone for which no dependency is stored. Hence, every
base is implicitly bound to [Unassigned]. *)
- let empty_map z = Deps.from_data_deps z in
+ let empty_map z = Deps.data z in
let join = Deps.join in
let empty = Deps.bottom in
(* Partial application is important *)
@@ -418,7 +317,7 @@ module Memory = struct
does the recursive descent. *)
let substitute_data_deps =
(* Nothing left to substitute, return z unchanged *)
- let empty_right z = Deps.from_data_deps z in
+ let empty_right z = Deps.data z in
(* Zone to substitute is empty *)
let empty_left _ = Deps.bottom in
(* [b] is in the zone and substituted. Rewrite appropriately *)
@@ -505,7 +404,7 @@ module Memory = struct
end
-type froms =
+type t =
{ deps_return : Memory.return;
deps_table : Memory.t }
@@ -600,31 +499,33 @@ let equal
{ deps_return = dr' ; deps_table = dt' } =
Memory.equal dt dt'&& Deps.equal dr dr'
-include Datatype.Make
- (struct
- type t = froms
- let reprs =
- List.fold_left
- (fun acc o ->
- List.fold_left
- (fun acc m -> { deps_return = o; deps_table = m } :: acc)
- acc
- Memory.reprs)
- []
- Deps.reprs
- let structural_descr =
- Structural_descr.t_record
- [| Deps.packed_descr;
- Memory.packed_descr |]
- let name = "Function_Froms"
- let hash = hash
- let compare = Datatype.undefined
- let equal = equal
- let pretty = pretty
- let rehash = Datatype.identity
- let copy = Datatype.undefined
- let mem_project = Datatype.never_any_project
- end)
+include
+ (Datatype.Make
+ (struct
+ type nonrec t = t
+ let reprs =
+ List.fold_left
+ (fun acc o ->
+ List.fold_left
+ (fun acc m -> { deps_return = o; deps_table = m } :: acc)
+ acc
+ Memory.reprs)
+ []
+ Deps.reprs
+ let structural_descr =
+ Structural_descr.t_record
+ [| Deps.packed_descr;
+ Memory.packed_descr |]
+ let name = "Function_Froms"
+ let hash = hash
+ let compare = Datatype.undefined
+ let equal = equal
+ let pretty = pretty
+ let rehash = Datatype.identity
+ let copy = Datatype.undefined
+ let mem_project = Datatype.never_any_project
+ end)
+ : Datatype.S with type t := t)
(*
Local Variables:
diff --git a/src/kernel_services/abstract_interp/function_Froms.mli b/src/plugins/eva/types/froms.mli
similarity index 85%
rename from src/kernel_services/abstract_interp/function_Froms.mli
rename to src/plugins/eva/types/froms.mli
index 141bfc5f9a5266c16d87476242410a5f7f679f83..b90b41363da6acbdb0d9e5704471375c5045dc28 100644
--- a/src/kernel_services/abstract_interp/function_Froms.mli
+++ b/src/plugins/eva/types/froms.mli
@@ -22,34 +22,7 @@
(** Datastructures and common operations for the results of the From plugin. *)
-module Deps : sig
-
- type deps = {
- data: Locations.Zone.t;
- indirect: Locations.Zone.t;
- }
-
- val bottom: deps
- val top: deps
- val is_included: deps -> deps -> bool
- val join: deps -> deps -> deps
- val narrow: deps -> deps -> deps
- val to_zone: deps -> Locations.Zone.t
-
- val add_data_dep: deps -> Locations.Zone.t -> deps
- val add_indirect_dep: deps -> Locations.Zone.t -> deps
-
-
- val from_data_deps: Locations.Zone.t -> deps
- val from_indirect_deps: Locations.Zone.t -> deps
-
- val map: (Locations.Zone.t -> Locations.Zone.t) -> deps -> deps
-
- include Datatype.S with type t = deps
-
- val pretty_precise : Format.formatter -> t -> unit
-end
-
+[@@@ api_start]
module DepsOrUnassigned : sig
@@ -85,7 +58,7 @@ module DepsOrUnassigned : sig
val pretty_precise : Format.formatter -> t -> unit
val to_zone: t -> Locations.Zone.t
- val to_deps: t -> Deps.deps
+ val to_deps: t -> Deps.t
end
module Memory : sig
@@ -149,35 +122,37 @@ end
-type froms = {
+type t = {
deps_return : Memory.return
(** Dependencies for the returned value *);
deps_table : Memory.t
(** Dependencies on all the zones modified by the function *);
}
-include Datatype.S with type t = froms
+include Datatype.S with type t := t
-val join: froms -> froms -> froms
+val join: t -> t -> t
-val top: froms
+val top: t
(** Display dependencies of a function, using the function's type to improve
readability *)
-val pretty_with_type: Cil_types.typ -> froms Pretty_utils.formatter
+val pretty_with_type: Cil_types.typ -> t Pretty_utils.formatter
(** Display dependencies of a function, using the function's type to improve
readability, separating direct and indirect dependencies *)
-val pretty_with_type_indirect: Cil_types.typ -> froms Pretty_utils.formatter
+val pretty_with_type_indirect: Cil_types.typ -> t Pretty_utils.formatter
(** Extract the left part of a from result, ie. the zones that are written *)
-val outputs: froms -> Locations.Zone.t
+val outputs: t -> Locations.Zone.t
(** Extract the right part of a from result, ie. the zones on which the
written zones depend. If [include_self] is true, and the from is
of the form [x FROM y (and SELF)], [x] is added to the result;
default value is [false]. *)
-val inputs: ?include_self:bool -> froms -> Locations.Zone.t
+val inputs: ?include_self:bool -> t -> Locations.Zone.t
+
+[@@@ api_end]
(*
Local Variables:
diff --git a/src/plugins/eva/utils/cvalue_callbacks.ml b/src/plugins/eva/utils/cvalue_callbacks.ml
index d4101a12b9c2de6f3a289deef62458ba3a3ef6c6..66b713cce3ab8097787ba1864d1782049ea2cb57 100644
--- a/src/plugins/eva/utils/cvalue_callbacks.ml
+++ b/src/plugins/eva/utils/cvalue_callbacks.ml
@@ -41,7 +41,7 @@ let register_call_hook f =
let apply_call_hooks callstack kf state kind =
Call.apply (callstack, kf, state, kind)
-type call_froms = (Function_Froms.froms * Locations.Zone.t) option
+type call_froms = (Froms.t * Locations.Zone.t) option
type state_by_stmt = (state Cil_datatype.Stmt.Hashtbl.t) Lazy.t
type results = { before_stmts: state_by_stmt; after_stmts: state_by_stmt }
diff --git a/src/plugins/eva/utils/cvalue_callbacks.mli b/src/plugins/eva/utils/cvalue_callbacks.mli
index baa6dc0942ac19de3ec39a0ce11584b893626fe8..d48fb793c6b79cbc0ea96f37d6d9cad43c1c6040 100644
--- a/src/plugins/eva/utils/cvalue_callbacks.mli
+++ b/src/plugins/eva/utils/cvalue_callbacks.mli
@@ -33,7 +33,7 @@ type state = Cvalue.Model.t
(** If not None, the froms of the function, and its sure outputs;
i.e. the dependencies of the result, and the dependencies
of each zone written to. *)
-type call_froms = (Function_Froms.froms * Locations.Zone.t) option
+type call_froms = (Froms.t * Locations.Zone.t) option
type analysis_kind =
[ `Builtin (** A cvalue builtin is used to interpret the function. *)
diff --git a/src/plugins/eva/utils/private.ml b/src/plugins/eva/utils/private.ml
index e4a368655a9c996dcafcb0369e4ba346cfa6549b..564056180ee41b2d2b1173113daeb53e2075a37b 100644
--- a/src/plugins/eva/utils/private.ml
+++ b/src/plugins/eva/utils/private.ml
@@ -40,6 +40,7 @@ module Eval_annots = Eval_annots
module Eval_op = Eval_op
module Eval_terms = Eval_terms
module Eval_typ = Eval_typ
+module Froms = Froms
module Function_calls = Function_calls
module Logic_inout = Logic_inout
module Main_locations = Main_locations
diff --git a/src/plugins/eva/utils/private.mli b/src/plugins/eva/utils/private.mli
index f70377152869169e4763bef80aca6d553384f555..1a614467fd16d849f0091a1781d113ce5219a8d8 100644
--- a/src/plugins/eva/utils/private.mli
+++ b/src/plugins/eva/utils/private.mli
@@ -44,6 +44,7 @@ module Eval_annots = Eval_annots
module Eval_op = Eval_op
module Eval_terms = Eval_terms
module Eval_typ = Eval_typ
+module Froms = Froms
module Function_calls = Function_calls
module Logic_inout = Logic_inout
module Main_locations = Main_locations
diff --git a/src/plugins/from/From.ml b/src/plugins/from/From.ml
index 03c99df40462fd32d23c0c3d9794b283fc074559..4073b6e66775afbb55bd718bfb42b3b8b4a33c49 100644
--- a/src/plugins/from/From.ml
+++ b/src/plugins/from/From.ml
@@ -27,7 +27,7 @@ let is_computed = Functionwise.is_computed
let get = Functionwise.get
let pretty = Functionwise.pretty
-let access zone mem = Function_Froms.Memory.find mem zone
+let access zone mem = Eva.Froms.Memory.find mem zone
let display fmt = From_register.display (Some fmt)
diff --git a/src/plugins/from/From.mli b/src/plugins/from/From.mli
index ac8e62ad0c26771c22e8f1ccf023d03be617a62f..dfc0e8c32390c22edba090136edc55fdeec0bee5 100644
--- a/src/plugins/from/From.mli
+++ b/src/plugins/from/From.mli
@@ -28,8 +28,8 @@ val is_computed : kernel_function -> bool
val compute : kernel_function -> unit
val compute_all : unit -> unit
-val get : Cil_types.kernel_function -> Function_Froms.froms
-val access : Locations.Zone.t -> Function_Froms.Memory.t -> Locations.Zone.t
+val get : Cil_types.kernel_function -> Eva.Froms.t
+val access : Locations.Zone.t -> Eva.Froms.Memory.t -> Locations.Zone.t
val self : State.t
@@ -42,6 +42,6 @@ val display : Format.formatter -> unit
val compute_all_calldeps : unit -> unit
module Callwise : sig
- val iter : (Cil_types.kinstr -> Function_Froms.froms -> unit) -> unit
- val find : Cil_types.kinstr -> Function_Froms.froms
+ val iter : (Cil_types.kinstr -> Eva.Froms.t -> unit) -> unit
+ val find : Cil_types.kinstr -> Eva.Froms.t
end
diff --git a/src/plugins/from/callwise.ml b/src/plugins/from/callwise.ml
index 0e5d37b4d35d0d8aaf6bd1613548ee7cd526d7d2..d909206a8493e0e8c078625e8bc4d42b02946187 100644
--- a/src/plugins/from/callwise.ml
+++ b/src/plugins/from/callwise.ml
@@ -25,7 +25,7 @@ open Cil_datatype
module Tbl =
Cil_state_builder.Kinstr_hashtbl
- (Function_Froms)
+ (Eva.Froms)
(struct
let name = "Callwise dependencies"
let size = 17
@@ -36,7 +36,7 @@ let () = From_parameters.ForceCallDeps.set_output_dependencies [Tbl.self]
let merge_call_froms table callsite froms =
try
let current = Kinstr.Hashtbl.find table callsite in
- let new_froms = Function_Froms.join froms current in
+ let new_froms = Eva.Froms.join froms current in
Kinstr.Hashtbl.replace table callsite new_froms
with Not_found ->
Kinstr.Hashtbl.add table callsite froms
@@ -44,7 +44,7 @@ let merge_call_froms table callsite froms =
(** State for the analysis of one function call *)
type from_state = {
current_function: Kernel_function.t (** Function being analyzed *);
- table_for_calls: Function_Froms.t Kinstr.Hashtbl.t
+ table_for_calls: Eva.Froms.t Kinstr.Hashtbl.t
(** State of the From plugin for each statement containing a function call
in the body of [current_function]. Updated incrementally each time
Value analyses such a statement *);
@@ -59,7 +59,7 @@ let call_froms_stack : from_state list ref = ref []
let record_callwise_dependencies_in_db call_site froms =
try
let previous = Tbl.find call_site in
- Tbl.replace call_site (Function_Froms.join previous froms)
+ Tbl.replace call_site (Eva.Froms.join previous froms)
with Not_found -> Tbl.add call_site froms
let call_for_individual_froms _callstack current_function _state call_type =
@@ -97,7 +97,7 @@ let end_record callstack froms =
module MemExec =
State_builder.Hashtbl
(Datatype.Int.Hashtbl)
- (Function_Froms)
+ (Eva.Froms)
(struct
let size = 17
let dependencies = [Tbl.self]
@@ -135,7 +135,7 @@ let record_for_individual_froms callstack kf pre_state value_res =
let froms =
if Eva.Analysis.save_results kf
then compute_call_from_value_states kf (Lazy.force before_stmts)
- else Function_Froms.top
+ else Eva.Froms.top
in
if From_parameters.VerifyAssigns.get () then
Eva.Logic_inout.verify_assigns kf ~pre:pre_state froms;
diff --git a/src/plugins/from/callwise.mli b/src/plugins/from/callwise.mli
index 6fa25e4f741c7f6803d63cdfd1795f81423afdee..2cdb2cb3e7ddbda80336cd881940a84ef65d52bd 100644
--- a/src/plugins/from/callwise.mli
+++ b/src/plugins/from/callwise.mli
@@ -25,5 +25,5 @@
precise than the functionwise results. *)
val compute_all_calldeps : unit -> unit
-val iter : (Cil_types.kinstr -> Function_Froms.froms -> unit) -> unit
-val find : Cil_types.kinstr -> Function_Froms.froms
+val iter : (Cil_types.kinstr -> Eva.Froms.t -> unit) -> unit
+val find : Cil_types.kinstr -> Eva.Froms.t
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 4c662872580ba2732f0583f403dda70ffe646c7a..f9668845e4102fe41b0da3e82f972881ed477d43 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -33,16 +33,16 @@ module Record_From_Callbacks =
(struct
type t =
(Kernel_function.t Stack.t) *
- Function_Froms.Memory.t Stmt.Hashtbl.t *
- (Kernel_function.t * Function_Froms.Memory.t) list Stmt.Hashtbl.t
+ Eva.Froms.Memory.t Stmt.Hashtbl.t *
+ (Kernel_function.t * Eva.Froms.Memory.t) list Stmt.Hashtbl.t
end)
module type To_Use =
sig
- val get_from_call : kernel_function -> stmt -> Function_Froms.t
+ val get_from_call : kernel_function -> stmt -> Eva.Froms.t
val stmt_request : stmt -> Eva.Results.request
val keep_base : kernel_function -> Base.t -> bool
- val cleanup_and_save : kernel_function -> Function_Froms.t -> Function_Froms.t
+ val cleanup_and_save : kernel_function -> Eva.Froms.t -> Eva.Froms.t
end
let compute_using_prototype_for_state state kf assigns =
@@ -53,7 +53,7 @@ let compute_using_prototype_for_state state kf assigns =
From_parameters.warning "@[no assigns clauses@ for function %a.@]@ \
Results will be imprecise."
Kernel_function.pretty kf;
- Function_Froms.Memory.(top_return, top)
+ Eva.Froms.Memory.(top_return, top)
| Writes assigns ->
let (rt_typ,_,_,_) = splitFunctionTypeVI varinfo in
let input_zone out ins =
@@ -75,9 +75,9 @@ let compute_using_prototype_for_state state kf assigns =
(* assign clauses do not let us specify address
dependencies for now, so we assume it is all data
dependencies *)
- let input_deps = Function_Froms.Deps.from_data_deps input_zone in
+ let input_deps = Eva.Deps.data input_zone in
(* Weak update of the over-approximation of the zones assigned *)
- let acc = Function_Froms.Memory.add_binding ~exact:false
+ let acc = Eva.Froms.Memory.add_binding ~exact:false
acc output.over input_deps in
(* Now, perform a strong update on the zones that are guaranteed
to be assigned (under-approximation) AND that do not depend
@@ -90,7 +90,7 @@ let compute_using_prototype_for_state state kf assigns =
Zone.(if equal top input_zone then bottom
else diff output.under input_zone)
in
- let acc = Function_Froms.Memory.add_binding ~exact:true
+ let acc = Eva.Froms.Memory.add_binding ~exact:true
acc sure_out_zone input_deps in
acc
@@ -99,15 +99,15 @@ let compute_using_prototype_for_state state kf assigns =
let zone_from = input_zone out from in
(* assign clauses do not let us specify address dependencies for
now, so we assume it is all data dependencies *)
- let inputs_deps = Function_Froms.Deps.from_data_deps zone_from in
+ let inputs_deps = Eva.Deps.data zone_from in
try
let coffs = Logic_to_c.loc_to_offset out.it_content in
List.fold_left
(fun acc coff ->
let (base,width) = bitsOffset rt_typ coff in
let size = Int_Base.inject (Int.of_int width) in
- Function_Froms.Memory.(add_to_return
- ~start:base ~size ~m:acc inputs_deps)
+ Eva.Froms.Memory.add_to_return
+ ~start:base ~size ~m:acc inputs_deps
)
acc coffs
with Logic_to_c.No_conversion | SizeOfError _ ->
@@ -115,7 +115,7 @@ let compute_using_prototype_for_state state kf assigns =
"Unable to extract a proper offset. \
Using FROM for the whole \\result";
let size = Bit_utils.sizeof rt_typ in
- Function_Froms.(Memory.add_to_return ~size ~m:acc inputs_deps)
+ Eva.Froms.Memory.add_to_return ~size ~m:acc inputs_deps
in
let return_assigns, other_assigns =
List.fold_left
@@ -127,19 +127,19 @@ let compute_using_prototype_for_state state kf assigns =
let return_assigns =
match return_assigns with
| [] when Cil.isVoidType rt_typ ->
- Function_Froms.Memory.default_return
+ Eva.Froms.Memory.default_return
| [] -> (* \from unspecified. *)
let size = Bit_utils.sizeof rt_typ in
- Function_Froms.Memory.top_return_size size
+ Eva.Froms.Memory.top_return_size size
| _ ->
List.fold_left treat_ret_assign
- Function_Froms.Memory.default_return return_assigns
+ Eva.Froms.Memory.default_return return_assigns
in
return_assigns,
List.fold_left
- treat_assign Function_Froms.Memory.empty other_assigns
+ treat_assign Eva.Froms.Memory.empty other_assigns
in
- { deps_return = return_deps; Function_Froms.deps_table = deps }
+ Eva.Froms.{ deps_return = return_deps; deps_table = deps }
module ZoneStmtMap = struct
include
@@ -164,7 +164,7 @@ struct
the statement that gave rise to the dependency. *)
additional_deps : Zone.t;
(** Union of the sets in {!additional_deps_table} *)
- deps_table : Function_Froms.Memory.t
+ deps_table : Eva.Froms.Memory.t
(** dependency table *)
}
@@ -181,7 +181,7 @@ struct
depending directly on an indirect dependency -> indirect,
depending indirectly on a direct dependency -> indirect *)
let merge_deps f deps =
- let open Function_Froms.Deps in
+ let open Eva.Deps in
let ind = f deps.indirect in
let data = f deps.data in
let ind = Zone.join data.indirect (to_zone ind) in
@@ -202,7 +202,7 @@ struct
let aux_local acc vi =
Cil.CurrentLoc.set vi.vdecl;
(* Consider that local are initialized to a constant value *)
- Function_Froms.Memory.bind_var vi Function_Froms.Deps.bottom acc
+ Eva.Froms.Memory.bind_var vi Eva.Deps.bottom acc
in
let loc = Cil.CurrentLoc.get () in
@@ -212,7 +212,7 @@ struct
let unbind_locals m b =
let aux_local acc vi =
- Function_Froms.Memory.unbind_var vi acc
+ Eva.Froms.Memory.unbind_var vi acc
in
List.fold_left aux_local m b.blocals
@@ -221,7 +221,7 @@ struct
let request = To_Use.stmt_request stmt in
let pre_trans = Eva.Results.expr_dependencies expr request in
merge_deps
- (fun d -> Function_Froms.Memory.find_precise deps_tbl d) pre_trans
+ (fun d -> Eva.Froms.Memory.find_precise deps_tbl d) pre_trans
let lval_to_zone_with_deps stmt lv =
let request = To_Use.stmt_request stmt in
@@ -238,12 +238,12 @@ struct
let empty_from =
{ additional_deps_table = ZoneStmtMap.empty;
additional_deps = Zone.bottom;
- deps_table = Function_Froms.Memory.empty }
+ deps_table = Eva.Froms.Memory.empty }
let bottom_from =
{ additional_deps_table = ZoneStmtMap.empty;
additional_deps = Zone.bottom;
- deps_table = Function_Froms.Memory.bottom }
+ deps_table = Eva.Froms.Memory.bottom }
module Computer = struct
@@ -253,11 +253,11 @@ struct
let callwise_states_with_formals = Stmt.Hashtbl.create 7
let substitute call_site_froms extra_loc deps =
- let subst_deps = Function_Froms.Memory.substitute call_site_froms deps in
- Function_Froms.Deps.add_indirect_dep subst_deps extra_loc
+ let subst_deps = Eva.Froms.Memory.substitute call_site_froms deps in
+ Eva.Deps.add_indirect subst_deps extra_loc
let display_one_from fmt v =
- Function_Froms.Memory.pretty fmt v.deps_table;
+ Eva.Froms.Memory.pretty fmt v.deps_table;
Format.fprintf fmt "Additional Variable Map : %a@\n"
ZoneStmtMap.pretty v.additional_deps_table;
Format.fprintf fmt
@@ -270,7 +270,7 @@ struct
let transfer_conditional_exp s exp state =
let additional = find s state.deps_table exp in
- let additional = Function_Froms.Deps.to_zone additional in
+ let additional = Eva.Deps.to_zone additional in
{state with
additional_deps_table =
ZoneStmtMap.add s additional state.additional_deps_table;
@@ -291,10 +291,10 @@ struct
m, new_z, false
in
let map =
- Function_Froms.Memory.join new_.deps_table old.deps_table
+ Eva.Froms.Memory.join new_.deps_table old.deps_table
in
let included' =
- Function_Froms.Memory.is_included new_.deps_table old.deps_table
+ Eva.Froms.Memory.is_included new_.deps_table old.deps_table
in
{ deps_table = map;
additional_deps_table = additional_map;
@@ -314,12 +314,12 @@ struct
let deps, loc, exact =
lval_to_precise_loc_with_deps stmt ~for_writing:(not init) lv
in
- let deps_of_deps = Function_Froms.Memory.find state.deps_table deps in
+ let deps_of_deps = Eva.Froms.Memory.find state.deps_table deps in
let all_indirect = Zone.join state.additional_deps deps_of_deps in
- let deps = Function_Froms.Deps.add_indirect_dep deps_right all_indirect in
+ let deps = Eva.Deps.add_indirect deps_right all_indirect in
let access = if init then Read else Write in
{ state with deps_table =
- Function_Froms.Memory.add_binding_precise_loc
+ Eva.Froms.Memory.add_binding_precise_loc
~exact access state.deps_table loc deps }
let transfer_call stmt dest f args _loc state =
@@ -328,9 +328,7 @@ struct
let called_vinfos = Eva.Results.(eval_callee f request |> default []) in
let f_deps = Eva.Results.expr_deps f request in
(* dependencies for the evaluation of [f] *)
- let f_deps =
- Function_Froms.Memory.find state.deps_table f_deps
- in
+ let f_deps = Eva.Froms.Memory.find state.deps_table f_deps in
let additional_deps =
Zone.join
state.additional_deps
@@ -350,8 +348,8 @@ struct
state
else
let froms_call = To_Use.get_from_call kf stmt in
- let froms_call_table = froms_call.Function_Froms.deps_table in
- if Function_Froms.Memory.is_bottom froms_call_table then
+ let froms_call_table = froms_call.Eva.Froms.deps_table in
+ if Eva.Froms.Memory.is_bottom froms_call_table then
bottom_from
else
let formal_args = Kernel_function.get_formals kf in
@@ -360,7 +358,7 @@ struct
List.iter2
(fun vi from ->
state_with_formals :=
- Function_Froms.Memory.bind_var
+ Eva.Froms.Memory.bind_var
vi from !state_with_formals;
) formal_args args_froms;
with Invalid_argument _ ->
@@ -381,7 +379,7 @@ struct
but before the result assignment *)
let deps_after_call =
let before_call = state.deps_table in
- let open Function_Froms in
+ let open Eva.Froms in
let subst d = DepsOrUnassigned.subst subst_before_call d in
let call_substituted = Memory.map subst froms_call_table in
Memory.compose call_substituted before_call
@@ -392,7 +390,7 @@ struct
match dest with
| None -> state
| Some lv ->
- let return_from = froms_call.Function_Froms.deps_return in
+ let return_from = froms_call.Eva.Froms.deps_return in
let deps_ret = subst_before_call return_from in
let init = Cil.is_mutable_or_initialized lv in
transfer_assign stmt ~init lv deps_ret state
@@ -404,7 +402,7 @@ struct
| Some acc_memory ->
Some
{state with
- deps_table = Function_Froms.Memory.join
+ deps_table = Eva.Froms.Memory.join
p.deps_table
acc_memory.deps_table}
in
@@ -452,7 +450,7 @@ struct
(* If implicit zero-initializers have been skipped, also mark
the entire array as initialized from no dependency (nothing
is read by the implicit zero-initializers). *)
- transfer_assign stmt ~init:true lv Function_Froms.Deps.bottom r
+ transfer_assign stmt ~init:true lv Eva.Deps.bottom r
in
aux (Cil.var v) i state
| Call (lvaloption,funcexp,argl,loc) ->
@@ -521,7 +519,7 @@ struct
(* Filter out unreachable values. *)
let transfer_stmt s d =
if Eva.Results.is_reachable s &&
- not (Function_Froms.Memory.is_bottom d.deps_table)
+ not (Eva.Froms.Memory.is_bottom d.deps_table)
then transfer_stmt s d
else []
@@ -552,25 +550,25 @@ struct
(match return.skind with
| Return (Some ({enode = Lval v}),_) ->
let zone = lval_to_zone_with_deps return v in
- let deps = Function_Froms.Memory.find_precise state.deps_table zone in
+ let deps = Eva.Froms.Memory.find_precise state.deps_table zone in
let size = Bit_utils.sizeof (Cil.typeOfLval v) in
- Function_Froms.(Memory.add_to_return ~size deps)
+ Eva.Froms.Memory.add_to_return ~size deps
| Return (None,_) ->
- Function_Froms.Memory.default_return
+ Eva.Froms.Memory.default_return
| _ -> assert false)
in
let accept = To_Use.keep_base kf in
let deps_table =
- Function_Froms.Memory.filter_base accept state.deps_table
+ Eva.Froms.Memory.filter_base accept state.deps_table
in
- { deps_return = deps_return;
- Function_Froms.deps_table = deps_table }
+ Eva.Froms.{ deps_return = deps_return;
+ deps_table = deps_table }
let compute_using_cfg kf =
match kf.fundec with
| Declaration _ -> assert false
| Definition (f,_) ->
- if not (Eva.Analysis.save_results kf) then Function_Froms.top
+ if not (Eva.Analysis.save_results kf) then Eva.Froms.top
else
try
Stack.iter (fun g -> if kf == g then raise Exit) call_stack;
@@ -615,16 +613,15 @@ struct
From_parameters.result
"Non-terminating function %a (no dependencies)"
Kernel_function.pretty kf;
- { Function_Froms.deps_return =
- Function_Froms.Memory.default_return;
- deps_table = Function_Froms.Memory.bottom }
+ Eva.Froms.{ deps_return = Eva.Froms.Memory.default_return;
+ deps_table = Eva.Froms.Memory.bottom }
end
in
last_from
with Exit (* Recursive call *) ->
- { Function_Froms.deps_return = Function_Froms.Memory.default_return;
- deps_table = Function_Froms.Memory.empty }
+ { deps_return = Eva.Froms.Memory.default_return;
+ deps_table = Eva.Froms.Memory.empty }
let compute_using_prototype kf =
let state = Eva.Results.(at_start_of kf |> get_cvalue_model) in
diff --git a/src/plugins/from/from_compute.mli b/src/plugins/from/from_compute.mli
index 9beabb6c488608a4c1efd485a7b0d775dbff2859..2d9f43e4bb4b8d705098e97d1915feff95e8f00c 100644
--- a/src/plugins/from/from_compute.mli
+++ b/src/plugins/from/from_compute.mli
@@ -30,7 +30,7 @@ open Cil_types
module type To_Use =
sig
(** How to find the Froms for a given call during the analysis. *)
- val get_from_call : kernel_function -> stmt -> Function_Froms.t
+ val get_from_call : kernel_function -> stmt -> Eva.Froms.t
(** The Eva request that can be used to evaluate expressions at a given
statement through the Eva public API. *)
@@ -43,7 +43,7 @@ sig
(** Clean the given from (that have been computed for the given function),
optionally save them, and return the cleaned result. *)
- val cleanup_and_save : kernel_function -> Function_Froms.t -> Function_Froms.t
+ val cleanup_and_save : kernel_function -> Eva.Froms.t -> Eva.Froms.t
end
(** Function that compute the Froms from a given prototype, called
@@ -52,14 +52,14 @@ val compute_using_prototype_for_state :
Cvalue.Model.t ->
Kernel_function.t ->
assigns ->
- Function_Froms.froms
+ Eva.Froms.t
(** Functor computing the functional dependencies, according to the three
modules above. *)
module Make (_: To_Use) : sig
(** Compute the dependencies of the given function, and return them *)
- val compute_and_return : Kernel_function.t -> Function_Froms.t
+ val compute_and_return : Kernel_function.t -> Eva.Froms.t
(** Compute the dependencies of the given function *)
val compute : Kernel_function.t -> unit
diff --git a/src/plugins/from/from_register.ml b/src/plugins/from/from_register.ml
index df9beea20f8bd31766c25136d413db7fb06a2b9f..1ad6000d2d117c58b8d996fa7564e2649b75f939 100644
--- a/src/plugins/from/from_register.ml
+++ b/src/plugins/from/from_register.ml
@@ -24,7 +24,7 @@ open Cil_types
let pretty_with_indirect fmt v =
let deps = Functionwise.get v in
- Function_Froms.pretty_with_type_indirect (Kernel_function.get_type v) fmt deps
+ Eva.Froms.pretty_with_type_indirect (Kernel_function.get_type v) fmt deps
let display fmtopt =
Option.iter (fun fmt -> Format.fprintf fmt "@[<v>") fmtopt;
@@ -138,8 +138,8 @@ let print_calldeps () =
From_parameters.printf ~header
"@[ %a@]"
((if From_parameters.ShowIndirectDeps.get ()
- then Function_Froms.pretty_with_type_indirect
- else Function_Froms.pretty_with_type) typ)
+ then Eva.Froms.pretty_with_type_indirect
+ else Eva.Froms.pretty_with_type) typ)
d);
From_parameters.feedback "====== END OF CALLWISE DEPENDENCIES ======"
diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml
index 484fbdba5b54ddcd4643bbba1f7f7e62d396d3e6..91991c3ccc1d32a82652223613812edd92496fea 100644
--- a/src/plugins/from/functionwise.ml
+++ b/src/plugins/from/functionwise.ml
@@ -25,7 +25,7 @@ open Locations
module Tbl =
Kernel_function.Make_Table
- (Function_Froms)
+ (Eva.Froms)
(struct
let name = "Functionwise dependencies"
let size = 17
@@ -53,7 +53,7 @@ module To_Use = struct
Eva.Logic_inout.accept_base ~formals:false ~locals:false kf
let cleanup kf froms =
- if Function_Froms.Memory.is_bottom froms.Function_Froms.deps_table
+ if Eva.Froms.Memory.is_bottom froms.Eva.Froms.deps_table
then froms
else
let accept_base =
@@ -75,11 +75,10 @@ module To_Use = struct
zone_substitution x
with Abstract_interp.Error_Top -> Zone.top
in
- let map_zone = Function_Froms.Deps.map zone_substitution in
- let subst = Function_Froms.DepsOrUnassigned.subst map_zone in
- let open Function_Froms in
- { deps_table = Memory.map subst froms.deps_table;
- deps_return = Deps.map zone_substitution froms.deps_return;
+ let map_zone = Eva.Deps.map zone_substitution in
+ let subst = Eva.Froms.DepsOrUnassigned.subst map_zone in
+ { deps_table = Eva.Froms.Memory.map subst froms.deps_table;
+ deps_return = Eva.Deps.map zone_substitution froms.deps_return;
}
let cleanup_and_save kf froms =
@@ -111,7 +110,7 @@ let is_computed = Tbl.mem
let get = To_Use.memo
let pretty fmt v =
- Function_Froms.pretty_with_type (Kernel_function.get_type v) fmt (get v)
+ Eva.Froms.pretty_with_type (Kernel_function.get_type v) fmt (get v)
(*
Local Variables:
diff --git a/src/plugins/from/functionwise.mli b/src/plugins/from/functionwise.mli
index 2f81e01120c45eb4fb58e1d242dd885c6f760136..aee21d2668d2b74d8e9090a1c16eabf71f305441 100644
--- a/src/plugins/from/functionwise.mli
+++ b/src/plugins/from/functionwise.mli
@@ -29,5 +29,5 @@ val self : State.t
val compute : kernel_function -> unit
val compute_all : unit -> unit
val is_computed : kernel_function -> bool
-val get : Cil_types.kernel_function -> Function_Froms.froms
+val get : Cil_types.kernel_function -> Eva.Froms.t
val pretty : Format.formatter -> kernel_function -> unit
diff --git a/src/plugins/inout/operational_inputs.ml b/src/plugins/inout/operational_inputs.ml
index d12bc75efab318688cbc438b023c28003b81d836..03c8aca99b100baf8c42109d3bb206f14e24fa07 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -515,25 +515,23 @@ let get_external_aux ?stmt kf =
else !ref_get_external kf
let extract_inout_from_froms froms =
- let open Function_Froms in
- let {deps_return; deps_table } = froms in
- let in_return = Deps.to_zone deps_return in
+ let Eva.Froms.{ deps_return; deps_table } = froms in
+ let in_return = Eva.Deps.to_zone deps_return in
let in_, out_ =
match deps_table with
- | Memory.Top -> Zone.top, Zone.top
- | Memory.Bottom -> Zone.bottom, Zone.bottom
- | Memory.Map m ->
+ | Top -> Zone.top, Zone.top
+ | Bottom -> Zone.bottom, Zone.bottom
+ | Map m ->
let aux_from out in_ (acc_in,acc_out as acc) =
- let open DepsOrUnassigned in
(* Skip zones fully unassigned, they are not really port of the
dependencies, but just present in the offsetmap to avoid "holes" *)
- match in_ with
+ match (in_ : Eva.Froms.DepsOrUnassigned.t) with
| DepsBottom | Unassigned -> acc
| AssignedFrom in_ | MaybeAssignedFrom in_ ->
- Zone.join acc_in (Deps.to_zone in_),
+ Zone.join acc_in (Eva.Deps.to_zone in_),
Zone.join acc_out out
in
- Memory.fold aux_from m (Zone.bottom, Zone.bottom)
+ Eva.Froms.Memory.fold aux_from m (Zone.bottom, Zone.bottom)
in
(Zone.join in_return in_), out_
diff --git a/src/plugins/pdg/build.ml b/src/plugins/pdg/build.ml
index 6db271d345e2405a1761dc0f0ea9be74ad26a0d8..3fb17f29435fdf84a85e684d9e8be70c5448a377 100644
--- a/src/plugins/pdg/build.ml
+++ b/src/plugins/pdg/build.ml
@@ -566,7 +566,7 @@ let finalize_pdg pdg from_opt =
(* TODO : also add the nodes for the other from ! *)
let state = match last_state with Some s -> s | None -> assert false in
let process_out out deps s =
- let open Function_Froms.DepsOrUnassigned in
+ let open Eva.Froms.DepsOrUnassigned in
if (equal Unassigned deps)
then s
else
@@ -574,24 +574,24 @@ let finalize_pdg pdg from_opt =
let default = may_be_unassigned deps in
add_from pdg state s out (default, from_out)
in
- let from_table = froms.Function_Froms.deps_table in
+ let from_table = froms.Eva.Froms.deps_table in
let new_state =
- if Function_Froms.Memory.is_bottom from_table then
+ if Eva.Froms.Memory.is_bottom from_table then
Pdg_state.bottom
else
let new_state =
match from_table with
- | Function_Froms.Memory.Top ->
+ | Top ->
process_out
- Locations.Zone.top Function_Froms.DepsOrUnassigned.top state
- | Function_Froms.Memory.Map m ->
- Function_Froms.Memory.fold_fuse_same process_out m state
- | Function_Froms.Memory.Bottom -> assert false (* checked above *)
+ Locations.Zone.top Eva.Froms.DepsOrUnassigned.top state
+ | Map m ->
+ Eva.Froms.Memory.fold_fuse_same process_out m state
+ | Bottom -> assert false (* checked above *)
in
if not (Kernel_function.returns_void pdg.fct) then begin
- let from0 = froms.Function_Froms.deps_return in
- let deps_ret = Function_Froms.Memory.collapse_return from0 in
- let deps_ret = Function_Froms.Deps.to_zone deps_ret in
+ let from0 = froms.Eva.Froms.deps_return in
+ let deps_ret = Eva.Froms.Memory.collapse_return from0 in
+ let deps_ret = Eva.Deps.to_zone deps_ret in
ignore
(create_fun_output_node pdg (Some new_state) deps_ret)
end;
@@ -651,46 +651,45 @@ let call_outputs pdg state_before_call state_with_inputs stmt
lvaloption froms fct_dpds =
(* obtain inputs from state_with_inputs
to avoid mixing in and out *)
- let froms_deps_return = froms.Function_Froms.deps_return in
- let from_table = froms.Function_Froms.deps_table in
+ let froms_deps_return = froms.Eva.Froms.deps_return in
+ let from_table = froms.Eva.Froms.deps_table in
let print_outputs fmt =
Format.fprintf fmt "call outputs : %a"
- Function_Froms.Memory.pretty from_table;
+ Eva.Froms.Memory.pretty from_table;
if not (lvaloption = None) then
Format.fprintf fmt "\t and \\result %a@."
- Function_Froms.Deps.pretty froms_deps_return
+ Eva.Deps.pretty froms_deps_return
in
debug "%t" print_outputs;
let process_out out deps state =
- if Function_Froms.DepsOrUnassigned.(equal Unassigned deps) then
+ if Eva.Froms.DepsOrUnassigned.(equal Unassigned deps) then
state
else
- let from_out = Function_Froms.DepsOrUnassigned.to_zone deps in
- let default = Function_Froms.DepsOrUnassigned.may_be_unassigned deps in
+ let from_out = Eva.Froms.DepsOrUnassigned.to_zone deps in
+ let default = Eva.Froms.DepsOrUnassigned.may_be_unassigned deps in
process_call_output
pdg state_with_inputs state stmt out default from_out fct_dpds
in
- if Function_Froms.Memory.is_bottom from_table then
+ if Eva.Froms.Memory.is_bottom from_table then
Pdg_state.bottom
else
let state_with_outputs =
- let open Function_Froms in
match from_table with
- | Memory.Top ->
+ | Top ->
process_out
- Locations.Zone.top DepsOrUnassigned.top state_before_call
- | Memory.Bottom -> assert false (* checked above *)
- | Memory.Map m ->
- Memory.fold_fuse_same process_out m state_before_call
+ Locations.Zone.top Eva.Froms.DepsOrUnassigned.top state_before_call
+ | Bottom -> assert false (* checked above *)
+ | Map m ->
+ Eva.Froms.Memory.fold_fuse_same process_out m state_before_call
in
match lvaloption with
| None -> state_with_outputs
| Some lval ->
let r_dpds =
- Function_Froms.Memory.collapse_return froms_deps_return
+ Eva.Froms.Memory.collapse_return froms_deps_return
in
- let r_dpds = Function_Froms.Deps.to_zone r_dpds in
+ let r_dpds = Eva.Deps.to_zone r_dpds in
let (l_loc, exact, l_dpds, l_decl) = get_lval_infos lval stmt in
process_call_return
pdg
diff --git a/src/plugins/scope/zones.ml b/src/plugins/scope/zones.ml
index 03a5d675411bf205295840b9b9102a57a8931f6f..3bf6e3bfd52905d30f1cdb0154ac410664a8b1fc 100644
--- a/src/plugins/scope/zones.ml
+++ b/src/plugins/scope/zones.ml
@@ -79,9 +79,9 @@ let process_call_res data stmt lvaloption froms =
let data = match lvaloption with
| None -> false, data
| Some lval ->
- let ret_dpds = froms.Function_Froms.deps_return in
- let r_dpds = Function_Froms.Memory.collapse_return ret_dpds in
- let r_dpds = Function_Froms.Deps.to_zone r_dpds in
+ let ret_dpds = froms.Eva.Froms.deps_return in
+ let r_dpds = Eva.Froms.Memory.collapse_return ret_dpds in
+ let r_dpds = Eva.Deps.to_zone r_dpds in
let l_dpds, exact, l_zone =
get_lval_zones ~for_writing:true stmt lval in
compute_new_data data l_zone l_dpds exact r_dpds
@@ -92,10 +92,10 @@ let process_call_res data stmt lvaloption froms =
* Moreover, we need to add the part of [data_after] that has not been
* modified for sure. *)
let process_froms data_after froms =
- let from_table = froms.Function_Froms.deps_table in
+ let from_table = froms.Eva.Froms.deps_table in
let process_out_call out deps (to_prop, used, new_data) =
- let out_dpds = Function_Froms.DepsOrUnassigned.to_zone deps in
- let default = Function_Froms.DepsOrUnassigned.may_be_unassigned deps in
+ let out_dpds = Eva.Froms.DepsOrUnassigned.to_zone deps in
+ let default = Eva.Froms.DepsOrUnassigned.may_be_unassigned deps in
let exact = not default in
(* be careful to compare out with data_after and not new_data *)
if (Data.intersects data_after out) then
@@ -113,12 +113,12 @@ let process_froms data_after froms =
let used = false in (* is the call needed ? *)
let to_prop, used, new_data =
match from_table with
- | Function_Froms.Memory.Bottom -> to_prop, used, new_data
- | Function_Froms.Memory.Top ->
- let v = Function_Froms.DepsOrUnassigned.top in
+ | Bottom -> to_prop, used, new_data
+ | Top ->
+ let v = Eva.Froms.DepsOrUnassigned.top in
process_out_call Locations.Zone.top v (to_prop, used, new_data)
- | Function_Froms.Memory.Map m ->
- Function_Froms.Memory.fold process_out_call m (to_prop, used, new_data)
+ | Map m ->
+ Eva.Froms.Memory.fold process_out_call m (to_prop, used, new_data)
in let data = Data.merge to_prop new_data in
(used, data)