diff --git a/src/plugins/from/callwise.ml b/src/plugins/from/callwise.ml
index f1119b1bed4377aa39a0f9a4b5cc69552238a4de..41a49e2e0a289dd89aa561ba2584d8fb2bc09b5c 100644
--- a/src/plugins/from/callwise.ml
+++ b/src/plugins/from/callwise.ml
@@ -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 *);
- value_initial_state: Db.Value.state (** State of Value at the beginning of
+ value_initial_state: Cvalue.Model.t (** State of Eva at the beginning of
the call *);
table_for_calls: Function_Froms.t Kinstr.Hashtbl.t
(** State of the From plugin for each statement containing a function call
@@ -94,7 +94,7 @@ let call_for_individual_froms callstack _kf call_type value_initial_state =
register_from result
| `Builtin None ->
let behaviors =
- !Db.Value.valid_behaviors current_function value_initial_state
+ Eva.Logic_inout.valid_behaviors current_function value_initial_state
in
compute_from_behaviors behaviors
| `Spec spec ->
@@ -136,9 +136,10 @@ let compute_call_from_value_states current_function states =
try Kinstr.Hashtbl.find table_for_calls (Cil_types.Kstmt callsite)
with Not_found -> raise From_compute.Call_did_not_take_place
- let get_value_state s =
- try Stmt.Hashtbl.find states s
- with Not_found -> Cvalue.Model.bottom
+ let stmt_request stmt =
+ Eva.Results.in_cvalue_state
+ (try Stmt.Hashtbl.find states stmt
+ with Not_found -> Cvalue.Model.bottom)
let keep_base kf base =
let fundec = Kernel_function.get_definition kf in
@@ -165,7 +166,7 @@ let record_for_individual_froms callstack cur_kf value_res =
| { value_initial_state } :: _ -> value_initial_state
in
if From_parameters.VerifyAssigns.get () then
- !Db.Value.verify_assigns_froms cur_kf ~pre:pre_state froms;
+ Eva.Logic_inout.verify_assigns cur_kf ~pre:pre_state froms;
MemExec.replace memexec_counter froms;
froms
diff --git a/src/plugins/from/from_compute.ml b/src/plugins/from/from_compute.ml
index 7b0300f32fe2728086234c6f7c74d1039e84b5cc..9a875ee9477b613bcdac6980795be2c9d242d04e 100644
--- a/src/plugins/from/from_compute.ml
+++ b/src/plugins/from/from_compute.ml
@@ -31,7 +31,7 @@ exception Call_did_not_take_place
module type To_Use =
sig
val get_from_call : kernel_function -> stmt -> Function_Froms.t
- val get_value_state : stmt -> Db.Value.state
+ 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
end
@@ -80,7 +80,7 @@ let compute_using_prototype_for_state state kf assigns =
let (rt_typ,_,_,_) = splitFunctionTypeVI varinfo in
let input_zone out ins =
(* Technically out is unused, but there is a signature problem *)
- !Db.Value.assigns_inputs_to_zone state (Writes [out, ins])
+ Eva.Logic_inout.assigns_inputs_to_zone state (Writes [out, ins])
in
let treat_assign acc (out, ins) =
try
@@ -245,23 +245,21 @@ struct
let find stmt deps_tbl expr =
- let state = To_Use.get_value_state stmt in
- let pre_trans = find_deps_no_transitivity state expr in
+ 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
- let lval_to_zone_with_deps stmt ~for_writing lv =
- let state = To_Use.get_value_state stmt in
- !Db.Value.lval_to_zone_with_deps_state
- state ~deps:(Some Zone.bottom) ~for_writing lv
+ let lval_to_zone_with_deps stmt lv =
+ let request = To_Use.stmt_request stmt in
+ Eva.Results.lval_deps lv request
let lval_to_precise_loc_with_deps stmt ~for_writing lv =
- let state = To_Use.get_value_state stmt in
- let deps, loc =
- !Db.Value.lval_to_precise_loc_with_deps_state
- state ~deps:(Some Zone.bottom) lv
- in
- let exact = Precise_locs.valid_cardinal_zero_or_one ~for_writing loc in
+ let request = To_Use.stmt_request stmt in
+ let deps = Eva.Results.address_deps lv request in
+ let address = Eva.Results.eval_address ~for_writing lv request in
+ let loc = Eva.Results.as_precise_loc address
+ and exact = Eva.Results.(is_singleton address || is_bottom address) in
deps, loc, exact
let empty_from =
@@ -353,11 +351,9 @@ struct
let transfer_call stmt dest f args _loc state =
Db.yield ();
- let value_state = To_Use.get_value_state stmt in
- let f_deps, called_vinfos =
- !Db.Value.expr_to_kernel_function_state
- value_state ~deps:(Some Zone.bottom) f
- in
+ let request = To_Use.stmt_request stmt in
+ 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
@@ -428,7 +424,7 @@ struct
let init = Cil.is_mutable_or_initialized lv in
transfer_assign stmt ~init lv deps_ret state
in
- let f f acc =
+ let f acc f =
let p = do_on f in
match acc with
| None -> Some p
@@ -441,7 +437,7 @@ struct
in
let result =
try
- (match Kernel_function.Hptset.fold f called_vinfos None with
+ (match List.fold_left f None called_vinfos with
| None -> state
| Some s -> s);
with Call_did_not_take_place -> state
@@ -495,8 +491,8 @@ struct
let transfer_guard s e d =
- let value_state = To_Use.get_value_state s in
- let interpreted_e = !Db.Value.eval_expr value_state e in
+ let request = To_Use.stmt_request s in
+ let interpreted_e = Eva.Results.(eval_exp e request |> as_cvalue) in
let t1 = unrollType (typeOf e) in
let do_then, do_else =
if isIntegralType t1 || isPointerType t1
@@ -582,11 +578,8 @@ struct
let deps_return =
(match return.skind with
| Return (Some ({enode = Lval v}),_) ->
- let deps, target, _exact =
- lval_to_zone_with_deps ~for_writing:false return v
- in
- let z = Zone.join target deps in
- let deps = Function_Froms.Memory.find_precise state.deps_table z in
+ let zone = lval_to_zone_with_deps return v in
+ let deps = Function_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)
| Return (None,_) ->
@@ -661,8 +654,8 @@ struct
deps_table = Function_Froms.Memory.empty }
let compute_using_prototype kf =
- let state = Db.Value.get_initial_state kf in
- let behaviors = !Db.Value.valid_behaviors kf state in
+ let state = Eva.Results.(at_start_of kf |> get_cvalue_model) in
+ let behaviors = Eva.Logic_inout.valid_behaviors kf state in
let assigns = Ast_info.merge_assigns behaviors in
compute_using_prototype_for_state state kf assigns
diff --git a/src/plugins/from/from_compute.mli b/src/plugins/from/from_compute.mli
index b1017c26489bec197e63d2acd77ffdc687858fcf..d66e9312f4920256752b91ce16e00dc2fb86067a 100644
--- a/src/plugins/from/from_compute.mli
+++ b/src/plugins/from/from_compute.mli
@@ -32,8 +32,9 @@ sig
(** How to find the Froms for a given call during the analysis. *)
val get_from_call : kernel_function -> stmt -> Function_Froms.t
- (** How to find the state of Value at a given statement during the analysis.*)
- val get_value_state : stmt -> Db.Value.state
+ (** The Eva request that can be used to evaluate expressions at a given
+ statement through the Eva public API. *)
+ val stmt_request : stmt -> Eva.Results.request
val keep_base : kernel_function -> Base.t -> bool
(** Return true if the given base is in scope after a call to the given
@@ -48,7 +49,7 @@ end
(** Function that compute the Froms from a given prototype, called
in the given state *)
val compute_using_prototype_for_state :
- Db.Value.state ->
+ Cvalue.Model.t ->
Kernel_function.t ->
assigns ->
Function_Froms.froms
diff --git a/src/plugins/from/functionwise.ml b/src/plugins/from/functionwise.ml
index a4f0a3e3065f582eab966749d0c87bcdb2265d98..e397a4d3dbedee8475acaf33ba0ee3c9677fe909 100644
--- a/src/plugins/from/functionwise.ml
+++ b/src/plugins/from/functionwise.ml
@@ -37,7 +37,7 @@ let () = From_parameters.ForceDeps.set_output_dependencies [Tbl.self]
let force_compute = ref (fun _ -> assert false)
module To_Use = struct
- let get_value_state s = Db.Value.get_stmt_state s
+ let stmt_request stmt = Eva.Results.before stmt
let memo kf =
Tbl.memo
@@ -110,10 +110,8 @@ let () =
let deps = To_Use.memo v in
Function_Froms.pretty_with_type (Kernel_function.get_type v) fmt deps);
Db.From.find_deps_no_transitivity :=
- (fun stmt lv ->
- let state = Db.Value.get_stmt_state stmt in
- let deps = From_compute.find_deps_no_transitivity state lv in
- Function_Froms.Deps.to_zone deps);
+ (fun stmt expr ->
+ Eva.Results.(before stmt |> expr_deps expr));
(* Once this function has been moved to Eva, remove the dependency of Inout
from From. *)
Db.From.find_deps_no_transitivity_state :=