From 2d4ae4d7b49c9fca0ac6a0f81c91ae662301b24d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 4 Jul 2022 11:11:51 +0200
Subject: [PATCH] [Eva] In the engine, applies the callbacks from
Cvalue_callbacks.
---
src/plugins/value/domains/cvalue/builtins.ml | 6 ++---
src/plugins/value/engine/compute_functions.ml | 15 ++++++-----
src/plugins/value/engine/iterator.ml | 25 ++++++-------------
src/plugins/value/engine/transfer_stmt.ml | 5 ++--
4 files changed, 19 insertions(+), 32 deletions(-)
diff --git a/src/plugins/value/domains/cvalue/builtins.ml b/src/plugins/value/domains/cvalue/builtins.ml
index e630950b1fd..c5682f2f857 100644
--- a/src/plugins/value/domains/cvalue/builtins.ml
+++ b/src/plugins/value/domains/cvalue/builtins.ml
@@ -265,14 +265,12 @@ let apply_builtin (builtin:builtin) call ~pre ~post =
let arguments = compute_arguments call.arguments call.rest in
try
let call_result = builtin pre arguments in
- let call_stack = Eva_utils.call_stack () in
let froms =
match call_result with
| Full result -> `Builtin result.c_from
- | States _ -> `Builtin None
- | Result _ -> `Spec (Annotations.funspec call.kf)
+ | States _ | Result _ -> `Builtin None
in
- Db.Value.Call_Type_Value_Callbacks.apply (froms, pre, call_stack);
+ Cvalue_callbacks.apply_call_hooks call.callstack call.kf froms pre;
process_result call post call_result
with
| Invalid_nb_of_args n ->
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index c4288155ea6..530750b8893 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -184,9 +184,8 @@ module Make (Abstract: Abstractions.Eva) = struct
in
call_result
| Some (states, i) ->
- let stack = Eva_utils.call_stack () in
let cvalue = Abstract.Dom.get_cvalue_or_top init_state in
- Db.Value.Call_Type_Value_Callbacks.apply (`Memexec, cvalue, stack);
+ Cvalue_callbacks.apply_call_hooks call.callstack call.kf `Memexec cvalue;
(* Evaluate the preconditions of kf, to update the statuses
at this call. *)
let spec = Annotations.funspec call.kf in
@@ -202,7 +201,8 @@ module Make (Abstract: Abstractions.Eva) = struct
Self.debug ~dkey
"calling Record_Value_New callbacks on saved previous result";
end;
- Db.Value.Record_Value_Callbacks_New.apply (stack, Value_types.Reuse i);
+ let reuse = Cvalue_callbacks.Reuse i in
+ Cvalue_callbacks.apply_call_results_hooks call.callstack call.kf reuse;
(* call can be cached since it was cached once *)
Transfer.{states; cacheable = Cacheable; builtin=false}
@@ -234,11 +234,10 @@ module Make (Abstract: Abstractions.Eva) = struct
let compute_using_spec_or_body target kinstr call state =
let global = match kinstr with Kglobal -> true | _ -> false in
let pp = not global && Parameters.ValShowProgress.get () in
- let call_stack = Eva_utils.call_stack () in
if pp then
Self.feedback
"@[computing for function %a.@\nCalled from %a.@]"
- Value_types.Callstack.pretty_short call_stack
+ Value_types.Callstack.pretty_short call.callstack
Cil_datatype.Location.pretty (Cil_datatype.Kinstr.loc kinstr);
let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
let compute, kind =
@@ -248,7 +247,7 @@ module Make (Abstract: Abstractions.Eva) = struct
| `Spec funspec ->
compute_using_spec funspec, `Spec funspec
in
- Db.Value.Call_Type_Value_Callbacks.apply (kind, cvalue_state, call_stack);
+ Cvalue_callbacks.apply_call_hooks call.callstack call.kf kind cvalue_state;
let resulting_states, cacheable = compute kinstr call state in
if pp then
Self.feedback
@@ -293,8 +292,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
match final_state with
| `Bottom ->
- let cs = Eva_utils.call_stack () in
- Db.Value.Call_Type_Value_Callbacks.apply (`Spec spec, cvalue_state, cs);
+ let kind = `Spec spec in
+ Cvalue_callbacks.apply_call_hooks call.callstack call.kf kind cvalue_state;
let cacheable = Eval.Cacheable in
Transfer.{states; cacheable; builtin=true}
| `Value final_state ->
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 3be91801bcb..2fc4a8215b0 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -448,8 +448,8 @@ module Make_Dataflow
(* TODO: apply on all domains. *)
let states = Partitioning.contents f in
let cvalue_states = gather_cvalues states in
- Db.Value.Compute_Statement_Callbacks.apply
- (stmt, Eva_utils.call_stack (), cvalue_states)
+ let callstack = Eva_utils.call_stack () in
+ Cvalue_callbacks.apply_statement_hooks callstack stmt cvalue_states
let update_vertex ?(widening : bool = false) (v : vertex)
(sources : ('branch * flow) list) : bool =
@@ -723,21 +723,12 @@ module Make_Dataflow
Db.Value.Record_Value_Callbacks.apply
(callstack, merged_pre_cvalues)
end;
- if not (Db.Value.Record_Value_Callbacks_New.is_empty ())
- then begin
- if Parameters.ValShowProgress.get () then
- Self.debug ~dkey:dkey_callbacks
- "now calling Record_Value_New callbacks";
- if Parameters.MemExecAll.get () then
- Db.Value.Record_Value_Callbacks_New.apply
- (callstack,
- Value_types.NormalStore ((merged_pre_cvalues, merged_post_cvalues),
- (Mem_exec.new_counter ())))
- else
- Db.Value.Record_Value_Callbacks_New.apply
- (callstack,
- Value_types.Normal (merged_pre_cvalues, merged_post_cvalues))
- end;
+ let states =
+ Cvalue_callbacks.{ before_stmts = merged_pre_cvalues;
+ after_stmts = merged_post_cvalues }
+ in
+ let results = Cvalue_callbacks.Store (states, Mem_exec.new_counter ()) in
+ Cvalue_callbacks.apply_call_results_hooks callstack kf results;
if not (Db.Value.Record_Value_After_Callbacks.is_empty ())
then begin
if Parameters.ValShowProgress.get () then
diff --git a/src/plugins/value/engine/transfer_stmt.ml b/src/plugins/value/engine/transfer_stmt.ml
index 34ec661ec42..09bcb4f40fc 100644
--- a/src/plugins/value/engine/transfer_stmt.ml
+++ b/src/plugins/value/engine/transfer_stmt.ml
@@ -731,9 +731,8 @@ module Make (Abstract: Abstractions.Eva) = struct
let cvalue_state = Domain.get_cvalue_or_top state in
Db.Value.Call_Value_Callbacks.apply (cvalue_state, stack_with_call);
Db.Value.merge_initial_state (Eva_utils.call_stack ()) cvalue_state;
- Db.Value.Call_Type_Value_Callbacks.apply
- (`Builtin None, cvalue_state, stack_with_call)
-
+ let kind = `Builtin None in
+ Cvalue_callbacks.apply_call_hooks stack_with_call kf kind cvalue_state
(* --------------------- Process the call statement ---------------------- *)
--
GitLab