From f6ef864dd09a088212606c0404237bdaf9759b26 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 21 Feb 2022 16:40:01 +0100
Subject: [PATCH] [Eva] Iterator: save results according to
[Function_calls.define_analysis_target].
---
src/plugins/value/engine/compute_functions.ml | 10 ++++++----
src/plugins/value/engine/function_calls.mli | 3 ++-
src/plugins/value/engine/iterator.ml | 10 +++++-----
src/plugins/value/engine/iterator.mli | 1 +
4 files changed, 14 insertions(+), 10 deletions(-)
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 3f88ff3f854..58a7232b07e 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -212,8 +212,8 @@ module Make (Abstract: Abstractions.Eva) = struct
(* Interprets a [call] at callsite [kinstr] in the state [state] by analyzing
the body of the called function. *)
- let compute_using_body fundec kinstr call state =
- let result = Computer.compute call.kf kinstr state in
+ let compute_using_body fundec ~save_results kinstr call state =
+ let result = Computer.compute ~save_results call.kf kinstr state in
Summary.FunctionStats.recompute fundec;
result
@@ -246,8 +246,10 @@ module Make (Abstract: Abstractions.Eva) = struct
let call_stack = Eva_utils.call_stack () in
let compute, kind =
match target with
- | `Def (fundec, _) -> compute_using_body fundec, `Def
- | `Spec funspec -> compute_using_spec funspec, `Spec funspec
+ | `Def (fundec, save_results) ->
+ compute_using_body fundec ~save_results, `Def
+ | `Spec funspec ->
+ compute_using_spec funspec, `Spec funspec
in
Db.Value.Call_Type_Value_Callbacks.apply (kind, cvalue_state, call_stack);
let resulting_states, cacheable = compute kinstr call state in
diff --git a/src/plugins/value/engine/function_calls.mli b/src/plugins/value/engine/function_calls.mli
index 3cf91982cc0..7a9cfcdc4fc 100644
--- a/src/plugins/value/engine/function_calls.mli
+++ b/src/plugins/value/engine/function_calls.mli
@@ -25,7 +25,8 @@ open Cil_types
(** What is used for the analysis of a given function:
- a Cvalue builtin (and other domains use the specification)
- the function specification
- - the function body. *)
+ - the function body. The boolean indicates whether the resulting states
+ must be recorded at each statement of this function. *)
type analysis_target =
[ `Builtin of string * Builtins.builtin * Eval.cacheable * funspec
| `Spec of Cil_types.funspec
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index d9d50612ebb..3be91801bcb 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -667,7 +667,7 @@ module Make_Dataflow
);
states_after
- let merge_results () =
+ let merge_results ~save_results =
let get_merged_states =
let merged_states = VertexTable.create control_point_count
and get_smashed_store v =
@@ -700,7 +700,7 @@ module Make_Dataflow
let merged_pre_cvalues = lazy (lift_to_cvalues merged_pre_states)
and merged_post_cvalues = lazy (lift_to_cvalues merged_post_states) in
let callstack = Eva_utils.call_stack () in
- if Mark_noresults.should_memorize_function fundec then begin
+ if save_results then begin
let register_pre = Domain.Store.register_state_before_stmt callstack
and register_post = Domain.Store.register_state_after_stmt callstack in
StmtTable.iter register_pre (Lazy.force merged_pre_states);
@@ -762,7 +762,7 @@ module Computer
end)
= struct
- let compute kf call_kinstr state =
+ let compute ~save_results kf call_kinstr state =
let module Dataflow =
Make_Dataflow
(Abstract) (States) (Transfer) (Init) (Logic) (Spec)
@@ -778,7 +778,7 @@ module Computer
if Parameters.ValShowProgress.get () then
Self.feedback "Recording results for %a"
Kernel_function.pretty kf;
- Dataflow.merge_results ();
+ Dataflow.merge_results ~save_results;
let f = Kernel_function.get_definition kf in
if Cil.hasAttribute "noreturn" f.svar.vattr && results <> [] then
Eva_utils.warning_once_current
@@ -788,7 +788,7 @@ module Computer
in
let cleanup () =
Dataflow.mark_degeneration ();
- Dataflow.merge_results ()
+ Dataflow.merge_results ~save_results
in
Eva_utils.protect compute ~cleanup
end
diff --git a/src/plugins/value/engine/iterator.mli b/src/plugins/value/engine/iterator.mli
index 81c8cc65844..47ca49314a2 100644
--- a/src/plugins/value/engine/iterator.mli
+++ b/src/plugins/value/engine/iterator.mli
@@ -44,6 +44,7 @@ module Computer
: sig
val compute:
+ save_results:bool ->
kernel_function -> kinstr -> Abstract.Dom.t ->
(Partition.key * Abstract.Dom.t) list * Eval.cacheable
--
GitLab