diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 096efee25f75d711296b3d0da3e2202a85933d8e..8505cb0590433c6802109df4633c4a20d9998d4b 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -634,7 +634,7 @@ module Eval: sig
callers, can be cached. *)
end
-module Froms: sig
+module Assigns: sig
module DepsOrUnassigned : sig
@@ -678,9 +678,9 @@ module Froms: sig
end
type t = {
- deps_return : Deps.t
+ return : Deps.t
(** Dependencies for the returned value *);
- deps_table : Memory.t
+ memory : Memory.t
(** Dependencies on all the zones modified by the function *);
}
@@ -715,7 +715,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: (Froms.t * Locations.Zone.t) option;
+ c_assigns: (Assigns.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. *)
}
@@ -766,7 +766,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 = (Froms.t * Locations.Zone.t) option
+ type call_assigns = (Assigns.t * Locations.Zone.t) option
type analysis_kind =
[ `Builtin (** A cvalue builtin is used to interpret the function. *)
@@ -791,7 +791,7 @@ module Cvalue_callbacks: sig
(** Results of a function call. *)
type call_results =
- [ `Builtin of state list * call_froms
+ [ `Builtin of state list * call_assigns
(** List of cvalue states at the end of the builtin. *)
| `Spec of state list
(** List of cvalue states at the end of the call. *)
@@ -861,7 +861,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 -> Froms.t -> unit
+ Cil_types.kernel_function -> pre:Cvalue.Model.t -> Assigns.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 8990420a0c8c70c1f671d24d1674b51c6a7254af..493a62a052b953e553871f1d6d1dbdf50ca7bd05 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: (Froms.t * Locations.Zone.t) option;
+ c_assigns: (Assigns.t * Locations.Zone.t) option;
}
type call_result =
@@ -276,7 +276,7 @@ let apply_builtin (builtin:builtin) call ~pre ~post =
let states = process_result call post call_result in
let froms =
match call_result with
- | Full result -> result.c_from
+ | Full result -> result.c_assigns
| States _ | Result _ -> None
in
let result = `Builtin (List.map fst states, froms) in
diff --git a/src/plugins/eva/domains/cvalue/builtins.mli b/src/plugins/eva/domains/cvalue/builtins.mli
index a95ff2ce8e76dbb1b0dfc6ec571e3112838d5051..e090c1daa38b1048df9d24ec3c05ec3f578811cd 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: (Froms.t * Locations.Zone.t) option;
+ c_assigns: (Assigns.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 3d5c3245d70535aa716a310b4e10168fe248b4ce..14364066d2fa108a24be87f005c2e0a6bce40756 100644
--- a/src/plugins/eva/domains/cvalue/builtins_malloc.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_malloc.ml
@@ -489,7 +489,7 @@ let register_malloc ?replace name ?returns_null prefix region =
let ret = V.inject new_base Ival.zero in
let c_values = wrap_fallible_alloc ?returns_null ret state new_state in
let c_clobbered = Base.SetLattice.bottom in
- Builtins.Full { c_values; c_clobbered; c_from = None; }
+ Builtins.Full { c_values; c_clobbered; c_assigns = None; }
in
let name = "Frama_C_" ^ name in
let typ () = Cil.voidPtrType, [Cil.theMachine.Cil.typeOfSizeOf] in
@@ -541,7 +541,7 @@ let calloc_builtin state args =
wrap_fallible_alloc ?returns_null ret state new_state
in
let c_clobbered = Base.SetLattice.bottom in
- Builtins.Full { c_values; c_clobbered; c_from = None; }
+ Builtins.Full { c_values; c_clobbered; c_assigns = None; }
let () =
let name = "Frama_C_calloc" in
@@ -579,8 +579,8 @@ let free ~exact bases state =
Locals_scoping.make_escaping ~exact ~escaping ~on_escaping ~within state
in
let from_changed =
- let m = Froms.Memory.(add_binding ~exact empty !changed Deps.bottom) in
- Froms.{ deps_table = m; deps_return = Deps.bottom }
+ let m = Assigns.Memory.(add_binding ~exact empty !changed Deps.bottom) in
+ Assigns.{ memory = m; return = Deps.bottom }
in
state, (from_changed, if exact then !changed else Zone.bottom)
@@ -645,12 +645,12 @@ let frama_c_free state actuals =
let bases_to_remove, card_to_remove, _null = resolve_bases_to_free arg in
let c_clobbered = Base.SetLattice.bottom in
if card_to_remove = 0 then
- Builtins.Full { c_values = []; c_clobbered; c_from = None; }
+ Builtins.Full { c_values = []; c_clobbered; c_assigns = None; }
else
let strong = card_to_remove <= 1 in
let state, changed = free_aux state ~strong bases_to_remove in
let c_values = [None, state] in
- Builtins.Full { c_values; c_clobbered; c_from = Some changed; }
+ Builtins.Full { c_values; c_clobbered; c_assigns = Some changed; }
| _ -> raise (Builtins.Invalid_nb_of_args 1)
let () =
@@ -666,7 +666,7 @@ let frama_c_vla_free state actuals =
let state, changed = free_aux state ~strong:true bases_to_remove in
let c_values = [None, state] in
let c_clobbered = Base.SetLattice.bottom in
- Builtins.Full { c_values; c_clobbered; c_from = Some changed; }
+ Builtins.Full { c_values; c_clobbered; c_assigns = Some changed; }
| _ -> raise (Builtins.Invalid_nb_of_args 1)
let () =
@@ -823,10 +823,10 @@ let realloc_builtin_aux state ptr size =
let new_state, changed = free_aux new_state ~strong bases in
let c_values = wrap_fallible_alloc ret state new_state in
let c_clobbered = Builtins.clobbered_set_from_ret new_state ret in
- Builtins.Full { c_values; c_clobbered; c_from = Some changed; }
+ Builtins.Full { c_values; c_clobbered; c_assigns = Some changed; }
else (* Invalid call. *)
let c_clobbered = Base.SetLattice.bottom in
- Builtins.Full { c_values = []; c_clobbered; c_from = None; }
+ Builtins.Full { c_values = []; c_clobbered; c_assigns = None; }
let realloc_builtin state args =
let ptr, size =
@@ -914,7 +914,7 @@ let check_leaked_malloced_bases state _ =
Base.pretty base)
alloced_bases;
let c_clobbered = Base.SetLattice.bottom in
- Builtins.Full { c_values = [None,state]; c_clobbered; c_from = None; }
+ Builtins.Full { c_values = [None,state]; c_clobbered; c_assigns = None; }
let () =
Builtins.register_builtin "Frama_C_check_leak" NoCacheCallers
diff --git a/src/plugins/eva/domains/cvalue/builtins_memory.ml b/src/plugins/eva/domains/cvalue/builtins_memory.ml
index 182171223f8e100043181004e3aaa2745e6731ca..f466617f59030c0b0438385e1b94fa5fb7784450 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 * Froms.t * Zone.t)
+exception Memcpy_result of (Cvalue.Model.t * Assigns.t * Zone.t)
exception Indeterminate of V_Or_Uninitialized.t
@@ -125,7 +125,7 @@ let frama_c_memcpy name state actuals =
in
let deps_return = deps_nth_arg 0 in
let empty_cfrom =
- Froms.{ deps_table = Memory.empty; deps_return }
+ Assigns.{ memory = Memory.empty; return = deps_return }
in
let precise_copy state =
(* First step: copy the bytes we are sure to copy *)
@@ -154,7 +154,8 @@ 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 =
- Froms.Memory.add_binding ~exact Froms.Memory.empty zone_dst deps
+ Assigns.Memory.add_binding ~exact
+ Assigns.Memory.empty zone_dst deps
in
let sure_zone = if exact then zone_dst else Zone.bottom in
(deps_table, sure_zone)
@@ -162,9 +163,9 @@ let frama_c_memcpy name state actuals =
new_state, deps_table, sure_zone
end
else (* Nothing certain can be copied *)
- (state, Froms.Memory.empty, Zone.bottom)
+ (state, Assigns.Memory.empty, Zone.bottom)
in
- let imprecise_copy new_state precise_deps_table sure_zone =
+ let imprecise_copy new_state precise_assigns sure_zone =
(* Second step. Size is imprecise, we will now copy some bits
that we are not sure to copy *)
let size_min_ival = Ival.inject_singleton size_min in
@@ -192,10 +193,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 deps_table =
- Froms.Memory.add_binding ~exact:false precise_deps_table zone_dst deps
+ let memory =
+ Assigns.Memory.add_binding ~exact:false precise_assigns zone_dst deps
in
- Froms.{ deps_table; deps_return }
+ Assigns.{ memory; return = deps_return }
in
try
(* We try to iter on all the slices inside the value of slice.
@@ -270,27 +271,29 @@ let frama_c_memcpy name state actuals =
try
if Ival.is_zero size then
raise (Memcpy_result (state, empty_cfrom, Zone.bottom));
- let (precise_state,precise_deps_table,sure_zone) = precise_copy state in
+ let (precise_state,precise_assigns,sure_zone) = precise_copy state in
if Option.fold ~none:false ~some:(Int.equal min) max then
begin
- let c_from = Froms.{ deps_table = precise_deps_table; deps_return } in
- raise (Memcpy_result (precise_state, c_from, sure_zone))
+ let c_assigns =
+ Assigns.{ memory = precise_assigns; return = deps_return }
+ in
+ raise (Memcpy_result (precise_state, c_assigns, sure_zone))
end;
- imprecise_copy precise_state precise_deps_table sure_zone
+ imprecise_copy precise_state precise_assigns sure_zone
with
- | Memcpy_result (new_state,c_from,sure_zone) ->
+ | Memcpy_result (new_state,c_assigns,sure_zone) ->
if Model.is_reachable new_state then
(* Copy at least partially succeeded (with perhaps an
alarm for some of the sizes *)
Builtins.Full
{ Builtins.c_values = [Some dst_bytes, new_state];
c_clobbered = Builtins.clobbered_set_from_ret new_state dst_bytes;
- c_from = Some (c_from, sure_zone); }
+ c_assigns = Some (c_assigns, sure_zone); }
else
Builtins.Full
{ Builtins.c_values = [ None, Cvalue.Model.bottom];
c_clobbered = Base.SetLattice.bottom;
- c_from = Some (c_from, sure_zone); }
+ c_assigns = Some (c_assigns, sure_zone); }
in
match actuals with
| [dst; src; size] -> compute dst src size
@@ -359,22 +362,22 @@ let frama_c_memset_imprecise state dst_lval dst v size =
(new_state,Zone.bottom)
with Not_found -> (new_state,Zone.bottom) (* from find_lonely_key + explicit raise *)
in
- let c_from =
+ let c_assigns =
let value_dep = deps_nth_arg 1 in
- let empty = Froms.Memory.empty in
- let deps_table =
- Froms.Memory.add_binding ~exact:false empty over_zone value_dep
+ let memory = Assigns.Memory.empty in
+ let memory =
+ Assigns.Memory.add_binding ~exact:false memory over_zone value_dep
in
- let deps_table =
- Froms.Memory.add_binding ~exact:true deps_table sure_zone value_dep
+ let memory =
+ Assigns.Memory.add_binding ~exact:true memory sure_zone value_dep
in
let deps_return = deps_nth_arg 0 in
- Froms.{ deps_table; deps_return }
+ Assigns.{ memory; return = deps_return }
in
Builtins.Full
{ Builtins.c_values = [Some dst, new_state'];
c_clobbered = Base.SetLattice.bottom;
- c_from = Some (c_from,sure_zone); }
+ c_assigns = Some (c_assigns,sure_zone); }
(* let () = register_builtin "Frama_C_memset" frama_c_memset_imprecise *)
(* Type that describes why the 'precise memset' builtin may fail. *)
@@ -575,11 +578,12 @@ let frama_c_memset_precise state dst_lval dst v (exp_size, size) =
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 =
- Froms.Memory.add_binding ~exact:true Froms.Memory.empty dst_zone input
+ let memory =
+ Assigns.Memory.add_binding ~exact:true
+ Assigns.Memory.empty dst_zone input
in
- let deps_return = deps_nth_arg 0 in
- let c_from = Froms.{ deps_table; deps_return } in
+ let return = deps_nth_arg 0 in
+ let c_from = Assigns.{ memory; return } in
c_from,dst_zone
in
let _ = c_from in
@@ -592,7 +596,7 @@ let frama_c_memset_precise state dst_lval dst v (exp_size, size) =
Builtins.Full
{ Builtins.c_values = [Some dst, state'];
c_clobbered = Base.SetLattice.bottom;
- c_from = Some (c_from,dst_zone); }
+ c_assigns = Some (c_from,dst_zone); }
with
| Bit_utils.NoMatchingOffset -> raise (ImpreciseMemset SizeMismatch)
| Base.Not_a_C_variable -> raise (ImpreciseMemset NoTypeForDest)
diff --git a/src/plugins/eva/dune b/src/plugins/eva/dune
index a828561d21824a349f0f222e217576eeceb50f34..ee102c636e8dba81c0523c333d5ca81ca3984577 100644
--- a/src/plugins/eva/dune
+++ b/src/plugins/eva/dune
@@ -113,7 +113,7 @@
(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 types/froms.mli
+ utils/eva_annotations.mli eval.mli types/assigns.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/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 7e02649b28a12c7f8526a6eea4732484e09ddde9..90a70b081ad5d1f6cfe4b9528a9c50647ef4c3f7 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 ();
- Froms.Memory.clear_caches ()
+ Assigns.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 bee771c2d1f03c870818a8f36f27e766dfa7969a..1aec39065f79ef1fcdf4165fe164b86098694e2d 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 ();
- Froms.Memory.clear_caches ()
+ Assigns.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 4c1a07385881578a2b1fbcec1fd9ab11f7ccb533..7f6db6d4f75c48e434e26205b43ee000b084f9e7 100644
--- a/src/plugins/eva/legacy/logic_inout.ml
+++ b/src/plugins/eva/legacy/logic_inout.ml
@@ -147,13 +147,13 @@ let eval_assigns_from pre_state it =
(** Compute the validity status for [from] in [pre_state], assuming the
entire clause is [assigns asgn \from from]. The inferred dependencies
are [found_froms], while [asgn] evaluates to [assigns_zone]. *)
-let check_from pre_state asgn assigns_zone from found_froms =
+let check_from pre_state asgn assigns_zone from found_assigns =
let open Locations in
let found_deps =
if Logic_utils.is_result asgn.it_content then
- found_froms.Froms.deps_return
+ found_assigns.Assigns.return
else
- Froms.Memory.find_precise found_froms.deps_table assigns_zone
+ Assigns.Memory.find_precise found_assigns.memory assigns_zone
in
let (indirect_deps,direct_deps) =
let filter x = List.mem "indirect" x.it_content.term_name in
@@ -213,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 = Froms.outputs found_froms in
+ let outputs = Assigns.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 d55e8ccd6ef71ddd0c035f61a2dba75f8467d227..acc64743f80292fac05f08746c652c4ccc673bc5 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 -> Froms.t -> unit
+ Cil_types.kernel_function -> pre:Cvalue.Model.t -> Assigns.t -> unit
(** [accept_base ~formals ~locals kf b] returns [true] if and only if [b] is:
diff --git a/src/plugins/eva/types/assigns.ml b/src/plugins/eva/types/assigns.ml
index 643e847c4112fa2c98e8e9c4324258658e3ff91a..f1a4fd3e43021c4e227c14eae6718cc0528fb3ef 100644
--- a/src/plugins/eva/types/assigns.ml
+++ b/src/plugins/eva/types/assigns.ml
@@ -193,33 +193,35 @@ end
module Datatype_Input = struct
include Datatype.Serializable_undefined
type t = {
- deps_return : Deps.t;
- deps_table : Memory.t
+ return : Deps.t;
+ memory : Memory.t
}
[@@deriving eq,ord]
let name = "Eva.Froms"
let top = {
- deps_return = Deps.top;
- deps_table = Memory.top;
+ return = Deps.top;
+ memory = Memory.top;
}
let reprs = [ top ]
- let hash froms =
- Hashtbl.hash (Memory.hash froms.deps_table, Deps.hash froms.deps_return)
- let pretty fmt { deps_return = r ; deps_table = t } =
+ let hash assigns =
+ Hashtbl.hash (Memory.hash assigns.memory, Deps.hash assigns.return)
+ let pretty fmt assigns =
Format.fprintf fmt "%a@\n\\result FROM @[%a@]@\n"
- Memory.pretty t
- Deps.pretty r
+ Memory.pretty assigns.memory
+ Deps.pretty assigns.return
end
include Datatype.Make (Datatype_Input)
include Datatype_Input
let join x y =
- { deps_return = Deps.join x.deps_return y.deps_return ;
- deps_table = Memory.join x.deps_table y.deps_table }
+ {
+ return = Deps.join x.return y.return;
+ memory = Memory.join x.memory y.memory;
+ }
-let outputs { deps_table = t } =
- match t with
+let outputs assigns =
+ match assigns.memory with
| Memory.Top -> Locations.Zone.top
| Memory.Bottom -> Locations.Zone.bottom
| Memory.Map m ->
diff --git a/src/plugins/eva/types/froms.mli b/src/plugins/eva/types/assigns.mli
similarity index 98%
rename from src/plugins/eva/types/froms.mli
rename to src/plugins/eva/types/assigns.mli
index a1935da3f66f11156367ab5536b201cff33f1f60..2875fbf0dc3a54e01e7feab400950478fa4f82bb 100644
--- a/src/plugins/eva/types/froms.mli
+++ b/src/plugins/eva/types/assigns.mli
@@ -66,9 +66,9 @@ module Memory : sig
end
type t = {
- deps_return : Deps.t
+ return : Deps.t
(** Dependencies for the returned value *);
- deps_table : Memory.t
+ memory : Memory.t
(** Dependencies on all the zones modified by the function *);
}
diff --git a/src/plugins/eva/types/froms.ml b/src/plugins/eva/types/froms.ml
deleted file mode 100644
index a79c103c59894e2626a152cf3e583135d44c1782..0000000000000000000000000000000000000000
--- a/src/plugins/eva/types/froms.ml
+++ /dev/null
@@ -1,242 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2023 *)
-(* 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). *)
-(* *)
-(**************************************************************************)
-
-module DepsOrUnassigned = struct
- module Datatype_Input = struct
- include Datatype.Serializable_undefined
-
- type t =
- | DepsBottom
- | Unassigned
- | AssignedFrom of Deps.t
- | MaybeAssignedFrom of Deps.t
- [@@deriving eq,ord]
- let name = "Eva.Froms.DepsOrUnassigned"
-
- let pretty fmt = function
- | DepsBottom -> Format.pp_print_string fmt "DEPS_BOTTOM"
- | Unassigned -> Format.pp_print_string fmt "UNASSIGNED"
- | AssignedFrom fd -> Deps.pretty_precise fmt fd
- | MaybeAssignedFrom fd ->
- Format.fprintf fmt "%a (or UNASSIGNED)" Deps.pretty_precise fd
-
- let hash = function
- | DepsBottom -> 1
- | Unassigned -> 2
- | AssignedFrom fd -> Hashtbl.hash (3, Deps.hash fd)
- | MaybeAssignedFrom fd -> Hashtbl.hash (4, Deps.hash fd)
-
- let reprs = Unassigned :: List.map (fun r -> AssignedFrom r) Deps.reprs
- end
-
- include Datatype.Make (Datatype_Input)
- include Datatype_Input
-
- let join d1 d2 = match d1, d2 with
- | DepsBottom, d | d, DepsBottom -> d
- | Unassigned, Unassigned -> Unassigned
- | Unassigned, AssignedFrom fd | AssignedFrom fd, Unassigned ->
- MaybeAssignedFrom fd
- | Unassigned, (MaybeAssignedFrom _ as d)
- | (MaybeAssignedFrom _ as d), Unassigned ->
- d
- | AssignedFrom fd1, AssignedFrom fd2 ->
- AssignedFrom (Deps.join fd1 fd2)
- | AssignedFrom fd1, MaybeAssignedFrom fd2
- | MaybeAssignedFrom fd1, AssignedFrom fd2
- | MaybeAssignedFrom fd1, MaybeAssignedFrom fd2 ->
- MaybeAssignedFrom (Deps.join fd1 fd2)
-
- let narrow _ _ = assert false (* not used yet *)
-
- let is_included d1 d2 = match d1, d2 with
- | DepsBottom, (DepsBottom | Unassigned | AssignedFrom _ |
- MaybeAssignedFrom _)
- | Unassigned, (Unassigned | AssignedFrom _ | MaybeAssignedFrom _) ->
- true
- | MaybeAssignedFrom fd1, (AssignedFrom fd2 | MaybeAssignedFrom fd2)
- | AssignedFrom fd1, AssignedFrom fd2 ->
- Deps.is_included fd1 fd2
- | (Unassigned | AssignedFrom _ | MaybeAssignedFrom _), DepsBottom
- | (AssignedFrom _ | MaybeAssignedFrom _), Unassigned
- | AssignedFrom _, MaybeAssignedFrom _ ->
- false
-
- let bottom = DepsBottom
- let top = MaybeAssignedFrom Deps.top
- let default = Unassigned
-
- let to_zone = function
- | DepsBottom | Unassigned -> Locations.Zone.bottom
- | AssignedFrom fd | MaybeAssignedFrom fd -> Deps.to_zone fd
-
- let may_be_unassigned = function
- | DepsBottom | AssignedFrom _ -> false
- | Unassigned | MaybeAssignedFrom _ -> true
-end
-
-module Memory = struct
- (* A From table is internally represented as a Lmap of [DepsOrUnassigned].
- However, the API mostly hides this fact, and exports access functions
- that take or return [Deps.t] values. This way, the user needs not
- understand the subtleties of DepsBottom/Unassigned/MaybeAssigned. *)
-
- include Lmap_bitwise.Make_bitwise(DepsOrUnassigned)
-
- let add_binding_precise_loc ~exact access m loc v =
- let aux_one_loc loc m =
- let loc = Locations.valid_part access loc in
- add_binding_loc ~exact m loc (DepsOrUnassigned.AssignedFrom v)
- in
- Precise_locs.fold aux_one_loc loc m
-
- let add_binding ~exact m z v =
- add_binding ~exact m z (DepsOrUnassigned.AssignedFrom v)
-
- let add_binding_loc ~exact m loc v =
- add_binding_loc ~exact m loc (DepsOrUnassigned.AssignedFrom v)
-
- (* This is the auxiliary datastructure used to write the function [find].
- When we iterate over a offsetmap of value [DepsOrUnassigned], we obtain
- two things: (1) some dependencies; (2) some intervals that may have not
- been assigned, and that will appear as data dependencies (once we know
- the base we are iterating on). *)
- type find_offsm = {
- fo_itvs: Int_Intervals.t;
- fo_deps: Deps.t;
- }
-
- (* Once the base is known, we can obtain something of type [Deps.t] *)
- let convert_find_offsm base fp =
- let z = Locations.Zone.inject base fp.fo_itvs in
- Deps.add_data fp.fo_deps z
-
- let empty_find_offsm = {
- fo_itvs = Int_Intervals.bottom;
- fo_deps = Deps.bottom;
- }
-
- let join_find_offsm fp1 fp2 =
- if fp1 == empty_find_offsm then fp2
- else if fp2 == empty_find_offsm then fp1
- else {
- fo_itvs = Int_Intervals.join fp1.fo_itvs fp2.fo_itvs;
- fo_deps = Deps.join fp1.fo_deps fp2.fo_deps;
- }
-
- (* Auxiliary function that collects the dependencies on some intervals of
- an offsetmap. *)
- let find_precise_offsetmap : Int_Intervals.t -> LOffset.t -> find_offsm =
- let cache = Hptmap_sig.PersistentCache "Eva.Froms.Memory.find_precise" in
- let aux_find_offsm ib ie v =
- (* If the interval can be unassigned, we collect its bound. We also
- return the dependencies stored at this interval. *)
- let default, v = match v with
- | DepsOrUnassigned.DepsBottom -> false, Deps.bottom
- | DepsOrUnassigned.Unassigned -> true, Deps.bottom
- | DepsOrUnassigned.MaybeAssignedFrom v -> true, v
- | DepsOrUnassigned.AssignedFrom v -> false, v
- in
- { fo_itvs =
- if default
- then Int_Intervals.inject_bounds ib ie
- else Int_Intervals.bottom;
- fo_deps = v }
- in
- (* Partial application is important *)
- LOffset.fold_join_itvs
- ~cache aux_find_offsm join_find_offsm empty_find_offsm
-
- (* Collecting dependencies on a given zone. *)
- let find_precise : t -> Locations.Zone.t -> Deps.t =
- let both = find_precise_offsetmap in
- 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.data z in
- let join = Deps.join in
- let empty = Deps.bottom in
- (* Partial application is important *)
- let f = fold_join_zone ~both ~conv ~empty_map ~join ~empty in
- fun m z ->
- match m with
- | Top -> Deps.top
- | Bottom -> Deps.bottom
- | Map m -> try f z m with Abstract_interp.Error_Top -> Deps.top
-
- let find_precise_loffset loffset base itv =
- let fo = find_precise_offsetmap itv loffset in
- convert_find_offsm base fo
-
- let find z m = Deps.to_zone (find_precise z m)
-end
-
-type t =
- { deps_return : Deps.t;
- deps_table : Memory.t }
-
-let top = {
- deps_return = Deps.top;
- deps_table = Memory.top;
-}
-
-let join x y =
- { deps_return = Deps.join x.deps_return y.deps_return ;
- deps_table = Memory.join x.deps_table y.deps_table }
-
-let outputs { deps_table = t } =
- match t with
- | Memory.Top -> Locations.Zone.top
- | Memory.Bottom -> Locations.Zone.bottom
- | Memory.Map m ->
- Memory.fold
- (fun z v acc ->
- let open DepsOrUnassigned in
- match v with
- | DepsBottom | Unassigned -> acc
- | AssignedFrom _ | MaybeAssignedFrom _ -> Locations.Zone.join z acc)
- m Locations.Zone.bottom
-
-module Datatype_Input = struct
- include Datatype.Serializable_undefined
- type nonrec t = t
- let name = "Eva.Froms"
-
- let reprs = [ top ]
- let structural_descr =
- Structural_descr.t_record [| Deps.packed_descr; Memory.packed_descr |]
-
- let equal
- { deps_return = dr ; deps_table = dt }
- { deps_return = dr' ; deps_table = dt' } =
- Memory.equal dt dt'&& Deps.equal dr dr'
-
- let hash { deps_return = dr ; deps_table = dt } =
- Memory.hash dt + 197 * Deps.hash dr
-
- let pretty fmt { deps_return = r ; deps_table = t } =
- Format.fprintf fmt "%a@\n\\result FROM @[%a@]@\n"
- Memory.pretty t
- Deps.pretty r
-end
-
-include (Datatype.Make (Datatype_Input) : Datatype.S with type t := t)
diff --git a/src/plugins/eva/utils/cvalue_callbacks.ml b/src/plugins/eva/utils/cvalue_callbacks.ml
index 66b713cce3ab8097787ba1864d1782049ea2cb57..99461fbbeb8ba04c86f57163a4a90380d8f25a1b 100644
--- a/src/plugins/eva/utils/cvalue_callbacks.ml
+++ b/src/plugins/eva/utils/cvalue_callbacks.ml
@@ -41,13 +41,13 @@ let register_call_hook f =
let apply_call_hooks callstack kf state kind =
Call.apply (callstack, kf, state, kind)
-type call_froms = (Froms.t * Locations.Zone.t) option
+type call_assigns = (Assigns.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 }
type call_results =
- [ `Builtin of state list * call_froms
+ [ `Builtin of state list * call_assigns
| `Spec of state list
| `Body of results * int
| `Reuse of int
diff --git a/src/plugins/eva/utils/cvalue_callbacks.mli b/src/plugins/eva/utils/cvalue_callbacks.mli
index d48fb793c6b79cbc0ea96f37d6d9cad43c1c6040..d5ab270851db90adb36aa953bed8121c1f9ec286 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 = (Froms.t * Locations.Zone.t) option
+type call_assigns = (Assigns.t * Locations.Zone.t) option
type analysis_kind =
[ `Builtin (** A cvalue builtin is used to interpret the function. *)
@@ -58,7 +58,7 @@ type results = { before_stmts: state_by_stmt; after_stmts: state_by_stmt }
(** Results of a function call. *)
type call_results =
- [ `Builtin of state list * call_froms
+ [ `Builtin of state list * call_assigns
(** List of cvalue states at the end of the builtin. *)
| `Spec of state list
(** List of cvalue states at the end of the call. *)
diff --git a/src/plugins/eva/utils/private.ml b/src/plugins/eva/utils/private.ml
index 564056180ee41b2d2b1173113daeb53e2075a37b..2a103740752b240773be661b721e6142729470cc 100644
--- a/src/plugins/eva/utils/private.ml
+++ b/src/plugins/eva/utils/private.ml
@@ -28,6 +28,7 @@ module Abstractions = Abstractions
module Active_behaviors = Active_behaviors
module Alarmset = Alarmset
module Analysis = Analysis
+module Assigns = Assigns
module Callstack = Callstack
module Cvalue_domain = Cvalue_domain
module Cvalue_results = Cvalue_results
@@ -40,7 +41,6 @@ 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 1a614467fd16d849f0091a1781d113ce5219a8d8..eb7491b3c9617d5c9f9e8029b9d5106d13bf2f5c 100644
--- a/src/plugins/eva/utils/private.mli
+++ b/src/plugins/eva/utils/private.mli
@@ -32,6 +32,7 @@ module Abstractions = Abstractions
module Active_behaviors = Active_behaviors
module Alarmset = Alarmset
module Analysis = Analysis
+module Assigns = Assigns
module Callstack = Callstack
module Cvalue_domain = Cvalue_domain
module Cvalue_results = Cvalue_results
@@ -44,7 +45,6 @@ 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 4073b6e66775afbb55bd718bfb42b3b8b4a33c49..a2bbb575037a34ebd51051c1406eee5d305a44b5 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 = Eva.Froms.Memory.find mem zone
+let access zone mem = Eva.Assigns.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 dfc0e8c32390c22edba090136edc55fdeec0bee5..ac0db406d4db28374a7cea5b28c4486c54885a05 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 -> Eva.Froms.t
-val access : Locations.Zone.t -> Eva.Froms.Memory.t -> Locations.Zone.t
+val get : Cil_types.kernel_function -> Eva.Assigns.t
+val access : Locations.Zone.t -> Eva.Assigns.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 -> Eva.Froms.t -> unit) -> unit
- val find : Cil_types.kinstr -> Eva.Froms.t
+ val iter : (Cil_types.kinstr -> Eva.Assigns.t -> unit) -> unit
+ val find : Cil_types.kinstr -> Eva.Assigns.t
end
diff --git a/src/plugins/from/callwise.ml b/src/plugins/from/callwise.ml
index d909206a8493e0e8c078625e8bc4d42b02946187..1d70d24bb671bb6e53819735614723cf564333ac 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
- (Eva.Froms)
+ (Eva.Assigns)
(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 = Eva.Froms.join froms current in
+ let new_froms = Eva.Assigns.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: Eva.Froms.t Kinstr.Hashtbl.t
+ table_for_calls: Eva.Assigns.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 (Eva.Froms.join previous froms)
+ Tbl.replace call_site (Eva.Assigns.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)
- (Eva.Froms)
+ (Eva.Assigns)
(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 Eva.Froms.top
+ else Eva.Assigns.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 2cdb2cb3e7ddbda80336cd881940a84ef65d52bd..ad682a4d569ca6c75efea339479e358348a738aa 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 -> Eva.Froms.t -> unit) -> unit
-val find : Cil_types.kinstr -> Eva.Froms.t
+val iter : (Cil_types.kinstr -> Eva.Assigns.t -> unit) -> unit
+val find : Cil_types.kinstr -> Eva.Assigns.t
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 9a6996e3d358c791601b833bb58071b796e3743f..9a063c21cea44ee5b54938be5b28d21a1fcf8f1b 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) *
- Eva.Froms.Memory.t Stmt.Hashtbl.t *
- (Kernel_function.t * Eva.Froms.Memory.t) list Stmt.Hashtbl.t
+ Eva.Assigns.Memory.t Stmt.Hashtbl.t *
+ (Kernel_function.t * Eva.Assigns.Memory.t) list Stmt.Hashtbl.t
end)
module type To_Use =
sig
- val get_from_call : kernel_function -> stmt -> Eva.Froms.t
+ val get_from_call : kernel_function -> stmt -> Eva.Assigns.t
val stmt_request : stmt -> Eva.Results.request
val keep_base : kernel_function -> Base.t -> bool
- val cleanup_and_save : kernel_function -> Eva.Froms.t -> Eva.Froms.t
+ val cleanup_and_save : kernel_function -> Eva.Assigns.t -> Eva.Assigns.t
end
let compute_using_prototype_for_state state kf assigns =
@@ -77,7 +77,7 @@ let compute_using_prototype_for_state state kf assigns =
dependencies *)
let input_deps = Eva.Deps.data input_zone in
(* Weak update of the over-approximation of the zones assigned *)
- let acc = Eva.Froms.Memory.add_binding ~exact:false
+ let acc = Eva.Assigns.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 = Eva.Froms.Memory.add_binding ~exact:true
+ let acc = Eva.Assigns.Memory.add_binding ~exact:true
acc sure_out_zone input_deps in
acc
@@ -137,9 +137,9 @@ let compute_using_prototype_for_state state kf assigns =
in
return_assigns,
List.fold_left
- treat_assign Eva.Froms.Memory.empty other_assigns
+ treat_assign Eva.Assigns.Memory.empty other_assigns
in
- Eva.Froms.{ deps_return = return_deps; deps_table = deps }
+ Eva.Assigns.{ return = return_deps; memory = 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 : Eva.Froms.Memory.t
+ deps_table : Eva.Assigns.Memory.t
(** dependency table *)
}
@@ -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 -> Eva.Froms.Memory.find_precise deps_tbl d) pre_trans
+ (fun d -> Eva.Assigns.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 = Eva.Froms.Memory.empty }
+ deps_table = Eva.Assigns.Memory.empty }
let bottom_from =
{ additional_deps_table = ZoneStmtMap.empty;
additional_deps = Zone.bottom;
- deps_table = Eva.Froms.Memory.bottom }
+ deps_table = Eva.Assigns.Memory.bottom }
module Computer = struct
@@ -257,7 +257,7 @@ struct
Eva.Deps.add_indirect subst_deps extra_loc
let display_one_from fmt v =
- Eva.Froms.Memory.pretty fmt v.deps_table;
+ Eva.Assigns.Memory.pretty fmt v.deps_table;
Format.fprintf fmt "Additional Variable Map : %a@\n"
ZoneStmtMap.pretty v.additional_deps_table;
Format.fprintf fmt
@@ -291,10 +291,10 @@ struct
m, new_z, false
in
let map =
- Eva.Froms.Memory.join new_.deps_table old.deps_table
+ Eva.Assigns.Memory.join new_.deps_table old.deps_table
in
let included' =
- Eva.Froms.Memory.is_included new_.deps_table old.deps_table
+ Eva.Assigns.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 = Eva.Froms.Memory.find state.deps_table deps in
+ let deps_of_deps = Eva.Assigns.Memory.find state.deps_table deps in
let all_indirect = Zone.join state.additional_deps deps_of_deps 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 =
- Eva.Froms.Memory.add_binding_precise_loc
+ Eva.Assigns.Memory.add_binding_precise_loc
~exact access state.deps_table loc deps }
let transfer_call stmt dest f args _loc state =
@@ -328,7 +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 = Eva.Froms.Memory.find state.deps_table f_deps in
+ let f_deps = Eva.Assigns.Memory.find state.deps_table f_deps in
let additional_deps =
Zone.join
state.additional_deps
@@ -348,8 +348,8 @@ struct
state
else
let froms_call = To_Use.get_from_call kf stmt in
- let froms_call_table = froms_call.Eva.Froms.deps_table in
- if Eva.Froms.Memory.is_bottom froms_call_table then
+ let froms_call_table = froms_call.Eva.Assigns.memory in
+ if Eva.Assigns.Memory.is_bottom froms_call_table then
bottom_from
else
let formal_args = Kernel_function.get_formals kf in
@@ -390,7 +390,7 @@ struct
match dest with
| None -> state
| Some lv ->
- let return_from = froms_call.Eva.Froms.deps_return in
+ let return_from = froms_call.Eva.Assigns.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
@@ -402,7 +402,7 @@ struct
| Some acc_memory ->
Some
{state with
- deps_table = Eva.Froms.Memory.join
+ deps_table = Eva.Assigns.Memory.join
p.deps_table
acc_memory.deps_table}
in
@@ -519,7 +519,7 @@ struct
(* Filter out unreachable values. *)
let transfer_stmt s d =
if Eva.Results.is_reachable s &&
- not (Eva.Froms.Memory.is_bottom d.deps_table)
+ not (Eva.Assigns.Memory.is_bottom d.deps_table)
then transfer_stmt s d
else []
@@ -545,12 +545,12 @@ struct
(* Remove all local variables and formals from table *)
- let externalize return kf state =
- let deps_return =
- (match return.skind with
+ let externalize return_stmt kf state =
+ let return =
+ (match return_stmt.skind with
| Return (Some ({enode = Lval v}),_) ->
- let zone = lval_to_zone_with_deps return v in
- let deps = Eva.Froms.Memory.find_precise state.deps_table zone in
+ let zone = lval_to_zone_with_deps return_stmt v in
+ let deps = Eva.Assigns.Memory.find_precise state.deps_table zone in
let size = Bit_utils.sizeof (Cil.typeOfLval v) in
From_memory.add_to_return ~size deps
| Return (None,_) ->
@@ -558,17 +558,14 @@ struct
| _ -> assert false)
in
let accept = To_Use.keep_base kf in
- let deps_table =
- Eva.Froms.Memory.filter_base accept state.deps_table
- in
- Eva.Froms.{ deps_return = deps_return;
- deps_table = deps_table }
+ let memory = Eva.Assigns.Memory.filter_base accept state.deps_table in
+ Eva.Assigns.{ return; memory }
let compute_using_cfg kf =
match kf.fundec with
| Declaration _ -> assert false
| Definition (f,_) ->
- if not (Eva.Analysis.save_results kf) then Eva.Froms.top
+ if not (Eva.Analysis.save_results kf) then Eva.Assigns.top
else
try
Stack.iter (fun g -> if kf == g then raise Exit) call_stack;
@@ -613,15 +610,19 @@ struct
From_parameters.result
"Non-terminating function %a (no dependencies)"
Kernel_function.pretty kf;
- Eva.Froms.{ deps_return = From_memory.default_return;
- deps_table = Eva.Froms.Memory.bottom }
+ Eva.Assigns.{
+ return = From_memory.default_return;
+ memory = Eva.Assigns.Memory.bottom
+ }
end
in
last_from
with Exit (* Recursive call *) ->
- { deps_return = From_memory.default_return;
- deps_table = Eva.Froms.Memory.empty }
+ {
+ return = From_memory.default_return;
+ memory = Eva.Assigns.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 2d9f43e4bb4b8d705098e97d1915feff95e8f00c..a48e9c38d2675bd00784dc2a7af4a1230328ccf9 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 -> Eva.Froms.t
+ val get_from_call : kernel_function -> stmt -> Eva.Assigns.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 -> Eva.Froms.t -> Eva.Froms.t
+ val cleanup_and_save : kernel_function -> Eva.Assigns.t -> Eva.Assigns.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 ->
- Eva.Froms.t
+ Eva.Assigns.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 -> Eva.Froms.t
+ val compute_and_return : Kernel_function.t -> Eva.Assigns.t
(** Compute the dependencies of the given function *)
val compute : Kernel_function.t -> unit
diff --git a/src/plugins/from/from_memory.ml b/src/plugins/from/from_memory.ml
index 2ae5ab4c97a7fc6c546511b2ea8b438c8e5d53fe..57d9fde7a112b070d89182f35e8ac20107f5bc62 100644
--- a/src/plugins/from/from_memory.ml
+++ b/src/plugins/from/from_memory.ml
@@ -24,7 +24,7 @@ open Locations
module Deps = Eva.Deps
module DepsOrUnassigned = struct
- include Eva.Froms.DepsOrUnassigned
+ include Eva.Assigns.DepsOrUnassigned
let subst f d =
match d with
@@ -68,7 +68,7 @@ module DepsOrUnassigned = struct
Format.fprintf fmt "%a (and SELF)" Deps.pretty_precise fd
end
-include Eva.Froms.Memory
+include Eva.Assigns.Memory
let bind_var vi v m =
let z = Locations.zone_of_varinfo vi in
@@ -217,9 +217,10 @@ let pretty_ind_data =
precise information.
@raise Error if the given type is not a function type
*)
-let pretty_with_type ~indirect typ fmt Eva.Froms.{ deps_return = r; deps_table = t } =
+let pretty_with_type ~indirect typ fmt assigns =
+ let Eva.Assigns.{ memory; return } = assigns in
let (rt_typ,_,_,_) = Cil.splitFunctionType typ in
- if is_bottom t
+ if is_bottom memory
then Format.fprintf fmt
"@[NON TERMINATING - NO EFFECTS@]"
else
@@ -230,18 +231,18 @@ let pretty_with_type ~indirect typ fmt Eva.Froms.{ deps_return = r; deps_table =
in
if Cil.isVoidType rt_typ
then begin
- if is_empty t
+ if is_empty memory
then Format.fprintf fmt "@[NO EFFECTS@]"
- else map_pretty fmt t
+ else map_pretty fmt memory
end
else
let pp_space fmt =
- if not (is_empty t) then
+ if not (is_empty memory) then
Format.fprintf fmt "@ "
in
Format.fprintf fmt "@[<v>%a%t@[\\result FROM @[%a@]@]@]"
- map_pretty t pp_space
- (if indirect then Deps.pretty_precise else Deps.pretty) r
+ map_pretty memory pp_space
+ (if indirect then Deps.pretty_precise else Deps.pretty) return
let pretty_with_type_indirect = pretty_with_type ~indirect:true
let pretty_with_type = pretty_with_type ~indirect:false
diff --git a/src/plugins/from/from_memory.mli b/src/plugins/from/from_memory.mli
index 15768ea0547beaeaaafa9ee95f9a6d28f34c385c..8e6f08e5905a93ea68fc7f20a0c284b27eaa0f02 100644
--- a/src/plugins/from/from_memory.mli
+++ b/src/plugins/from/from_memory.mli
@@ -22,7 +22,7 @@
(** Utilitary functions on the {!Eva.Froms.Memory.t} type. *)
-type t = Eva.Froms.Memory.t
+type t = Eva.Assigns.Memory.t
val top : t
@@ -69,8 +69,10 @@ val collapse_return: return -> Eva.Deps.t
(** Display dependencies of a function, using the function's type to improve
readability *)
-val pretty_with_type: Cil_types.typ -> Eva.Froms.t Pretty_utils.formatter
+val pretty_with_type: Cil_types.typ -> Eva.Assigns.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 -> Eva.Froms.t Pretty_utils.formatter
+val pretty_with_type_indirect:
+ Cil_types.typ ->
+ Eva.Assigns.t Pretty_utils.formatter
diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml
index 69caa8a39593169f0d369b54904c2690298152b1..972c2749f7f19c2ea85b81ed1339a71acf19e48b 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
- (Eva.Froms)
+ (Eva.Assigns)
(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 Eva.Froms.Memory.is_bottom froms.Eva.Froms.deps_table
+ if Eva.Assigns.Memory.is_bottom froms.Eva.Assigns.memory
then froms
else
let accept_base =
@@ -76,8 +76,8 @@ module To_Use = struct
with Abstract_interp.Error_Top -> Zone.top
in
let map_zone = Eva.Deps.map zone_substitution in
- { deps_table = From_memory.map map_zone froms.deps_table;
- deps_return = Eva.Deps.map zone_substitution froms.deps_return;
+ { memory = From_memory.map map_zone froms.memory;
+ return = Eva.Deps.map zone_substitution froms.return;
}
let cleanup_and_save kf froms =
diff --git a/src/plugins/from/functionwise.mli b/src/plugins/from/functionwise.mli
index aee21d2668d2b74d8e9090a1c16eabf71f305441..5f0ba60bace3c7b9c29a4dfa3c4506482b3b25a7 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 -> Eva.Froms.t
+val get : Cil_types.kernel_function -> Eva.Assigns.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 03c8aca99b100baf8c42109d3bb206f14e24fa07..74d506662ca0d90cfad653097b3140edffa329d9 100644
--- a/src/plugins/inout/operational_inputs.ml
+++ b/src/plugins/inout/operational_inputs.ml
@@ -514,8 +514,8 @@ let get_external_aux ?stmt kf =
r
else !ref_get_external kf
-let extract_inout_from_froms froms =
- let Eva.Froms.{ deps_return; deps_table } = froms in
+let extract_inout_from_froms assigns =
+ let Eva.Assigns.{ return = deps_return; memory = deps_table } = assigns in
let in_return = Eva.Deps.to_zone deps_return in
let in_, out_ =
match deps_table with
@@ -525,13 +525,13 @@ let extract_inout_from_froms froms =
let aux_from out in_ (acc_in,acc_out as acc) =
(* Skip zones fully unassigned, they are not really port of the
dependencies, but just present in the offsetmap to avoid "holes" *)
- match (in_ : Eva.Froms.DepsOrUnassigned.t) with
+ match (in_ : Eva.Assigns.DepsOrUnassigned.t) with
| DepsBottom | Unassigned -> acc
| AssignedFrom in_ | MaybeAssignedFrom in_ ->
Zone.join acc_in (Eva.Deps.to_zone in_),
Zone.join acc_out out
in
- Eva.Froms.Memory.fold aux_from m (Zone.bottom, Zone.bottom)
+ Eva.Assigns.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 ae522d4da803106814534acf3f548b4c15ad41ff..c2268d86d6f084325f3b5cf096c294eb2e2749d5 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 Eva.Froms.DepsOrUnassigned in
+ let open Eva.Assigns.DepsOrUnassigned in
if (equal Unassigned deps)
then s
else
@@ -574,22 +574,22 @@ 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.Eva.Froms.deps_table in
+ let from_table = froms.Eva.Assigns.memory in
let new_state =
- if Eva.Froms.Memory.is_bottom from_table then
+ if Eva.Assigns.Memory.is_bottom from_table then
Pdg_state.bottom
else
let new_state =
match from_table with
| Top ->
process_out
- Locations.Zone.top Eva.Froms.DepsOrUnassigned.top state
+ Locations.Zone.top Eva.Assigns.DepsOrUnassigned.top state
| Map m ->
- Eva.Froms.Memory.fold_fuse_same process_out m state
+ Eva.Assigns.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 deps_ret = froms.Eva.Froms.deps_return in
+ let deps_ret = froms.Eva.Assigns.return in
let deps_ret = Eva.Deps.to_zone deps_ret in
ignore
(create_fun_output_node pdg (Some new_state) deps_ret)
@@ -647,45 +647,44 @@ let process_args pdg st stmt argl =
and [new_state] the state to modify.
* Process call outputs (including returned value) *)
let call_outputs pdg state_before_call state_with_inputs stmt
- lvaloption froms fct_dpds =
+ lvaloption assigns fct_dpds =
(* obtain inputs from state_with_inputs
to avoid mixing in and out *)
- let froms_deps_return = froms.Eva.Froms.deps_return in
- let from_table = froms.Eva.Froms.deps_table in
+ let Eva.Assigns.{ return = return_deps; memory = memory_deps } = assigns in
let print_outputs fmt =
Format.fprintf fmt "call outputs : %a"
- Eva.Froms.Memory.pretty from_table;
+ Eva.Assigns.Memory.pretty memory_deps;
if not (lvaloption = None) then
Format.fprintf fmt "\t and \\result %a@."
- Eva.Deps.pretty froms_deps_return
+ Eva.Deps.pretty return_deps
in
debug "%t" print_outputs;
let process_out out deps state =
- if Eva.Froms.DepsOrUnassigned.(equal Unassigned deps) then
+ if Eva.Assigns.DepsOrUnassigned.(equal Unassigned deps) then
state
else
- let from_out = Eva.Froms.DepsOrUnassigned.to_zone deps in
- let default = Eva.Froms.DepsOrUnassigned.may_be_unassigned deps in
+ let from_out = Eva.Assigns.DepsOrUnassigned.to_zone deps in
+ let default = Eva.Assigns.DepsOrUnassigned.may_be_unassigned deps in
process_call_output
pdg state_with_inputs state stmt out default from_out fct_dpds
in
- if Eva.Froms.Memory.is_bottom from_table then
+ if Eva.Assigns.Memory.is_bottom memory_deps then
Pdg_state.bottom
else
let state_with_outputs =
- match from_table with
+ match memory_deps with
| Top ->
process_out
- Locations.Zone.top Eva.Froms.DepsOrUnassigned.top state_before_call
+ Locations.Zone.top Eva.Assigns.DepsOrUnassigned.top state_before_call
| Bottom -> assert false (* checked above *)
| Map m ->
- Eva.Froms.Memory.fold_fuse_same process_out m state_before_call
+ Eva.Assigns.Memory.fold_fuse_same process_out m state_before_call
in
match lvaloption with
| None -> state_with_outputs
| Some lval ->
- let r_dpds = Eva.Deps.to_zone froms_deps_return in
+ let r_dpds = Eva.Deps.to_zone return_deps 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 f4196e083083c0c5c4ddfd3bc113f8f8b648475f..3c2ecaa401f5672483771b620db63c95b9c8dea9 100644
--- a/src/plugins/scope/zones.ml
+++ b/src/plugins/scope/zones.ml
@@ -79,7 +79,7 @@ let process_call_res data stmt lvaloption froms =
let data = match lvaloption with
| None -> false, data
| Some lval ->
- let ret_dpds = froms.Eva.Froms.deps_return in
+ let ret_dpds = froms.Eva.Assigns.return in
let r_dpds = Eva.Deps.to_zone ret_dpds in
let l_dpds, exact, l_zone =
get_lval_zones ~for_writing:true stmt lval in
@@ -91,10 +91,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.Eva.Froms.deps_table in
+ let from_table = froms.Eva.Assigns.memory in
let process_out_call out deps (to_prop, used, new_data) =
- let out_dpds = Eva.Froms.DepsOrUnassigned.to_zone deps in
- let default = Eva.Froms.DepsOrUnassigned.may_be_unassigned deps in
+ let out_dpds = Eva.Assigns.DepsOrUnassigned.to_zone deps in
+ let default = Eva.Assigns.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
@@ -114,10 +114,10 @@ let process_froms data_after froms =
match from_table with
| Bottom -> to_prop, used, new_data
| Top ->
- let v = Eva.Froms.DepsOrUnassigned.top in
+ let v = Eva.Assigns.DepsOrUnassigned.top in
process_out_call Locations.Zone.top v (to_prop, used, new_data)
| Map m ->
- Eva.Froms.Memory.fold process_out_call m (to_prop, used, new_data)
+ Eva.Assigns.Memory.fold process_out_call m (to_prop, used, new_data)
in let data = Data.merge to_prop new_data in
(used, data)