From 4f0b24467b808e1d9fb6318e4743147e67cfa426 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 13 Jul 2021 10:12:24 +0200
Subject: [PATCH] [Eva] Do not call Db.Value.mark_as_computed before the
analysis.
Instead, calls Domain.Store.mark_as_computed at the end of the analysis.
---
src/kernel_services/plugin_entry_points/db.ml | 15 ++++++++-------
src/plugins/value/engine/compute_functions.ml | 5 +++--
src/plugins/value/engine/iterator.ml | 1 -
3 files changed, 11 insertions(+), 10 deletions(-)
diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml
index 298ad6fe8ee..64bc3512a2b 100644
--- a/src/kernel_services/plugin_entry_points/db.ml
+++ b/src/kernel_services/plugin_entry_points/db.ml
@@ -502,7 +502,7 @@ module Value = struct
Callstack.Hashtbl.add by_callstack cs state
let get_initial_state kf =
- assert (is_computed ()); (* this assertion fails during value analysis *)
+ assert (is_computed ()); (* this assertion fails during Eva analysis *)
try Called_Functions_Memo.find kf
with Not_found ->
let state =
@@ -517,8 +517,9 @@ module Value = struct
Called_Functions_Memo.add kf state;
state
+ (* This function is used by the Inout plugin during Eva analysis, so it
+ should not fail during Eva analysis, even if results are incomplete. *)
let get_initial_state_callstack kf =
- assert (is_computed ()); (* this assertion fails during value analysis *)
try Some (Called_Functions_By_Callstack.find kf)
with Not_found -> None
@@ -568,28 +569,28 @@ module Value = struct
noassert_get_stmt_state ~after s
let get_stmt_state ?(after=false) s =
- assert (is_computed ()); (* this assertion fails during value analysis *)
+ assert (is_computed ()); (* this assertion fails during Eva analysis *)
noassert_get_stmt_state ~after s
let get_state ?(after=false) k =
- assert (is_computed ()); (* this assertion fails during value analysis *)
+ assert (is_computed ()); (* this assertion fails during Eva analysis *)
noassert_get_state ~after k
let get_stmt_state_callstack ~after stmt =
- assert (is_computed ()); (* this assertion fails during value analysis *)
+ assert (is_computed ()); (* this assertion fails during Eva analysis *)
try
Some (if after then AfterTable_By_Callstack.find stmt else
Table_By_Callstack.find stmt)
with Not_found -> None
let fold_stmt_state_callstack f acc ~after stmt =
- assert (is_computed ()); (* this assertion fails during value analysis *)
+ assert (is_computed ()); (* this assertion fails during Eva analysis *)
match get_stmt_state_callstack ~after stmt with
| None -> acc
| Some h -> Value_types.Callstack.Hashtbl.fold (fun _ -> f) h acc
let fold_state_callstack f acc ~after ki =
- assert (is_computed ()); (* this assertion fails during value analysis *)
+ assert (is_computed ()); (* this assertion fails during Eva analysis *)
match ki with
| Kglobal -> f (globals_state ()) acc
| Kstmt stmt -> fold_stmt_state_callstack f acc ~after stmt
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 4d517e199e2..64f0a753188 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -82,8 +82,7 @@ let pre_analysis () =
degeneration states *)
Value_util.DegenerationPoints.clear ();
Cvalue.V.clear_garbled_mix ();
- Value_util.clear_call_stack ();
- Db.Value.mark_as_computed ()
+ Value_util.clear_call_stack ()
let post_analysis_cleanup ~aborted =
Value_util.clear_call_stack ();
@@ -341,11 +340,13 @@ module Make (Abstract: Abstractions.Eva) = struct
let final_state = PowersetDomain.(final_states >>-: of_list >>- join) in
Value_util.pop_call_stack ();
Value_parameters.feedback "done for function %a" Kernel_function.pretty kf;
+ Abstract.Dom.Store.mark_as_computed ();
post_analysis ();
Abstract.Dom.post_analysis final_state;
Value_results.print_summary ();
with
| Db.Value.Aborted ->
+ Abstract.Dom.Store.mark_as_computed ();
post_analysis_cleanup ~aborted:true;
(* Signal that a degeneration occurred *)
if Value_util.DegenerationPoints.length () > 0 then
diff --git a/src/plugins/value/engine/iterator.ml b/src/plugins/value/engine/iterator.ml
index 930c01942de..30680db8feb 100644
--- a/src/plugins/value/engine/iterator.ml
+++ b/src/plugins/value/engine/iterator.ml
@@ -782,7 +782,6 @@ module Computer
with Db.Value.Aborted as e ->
(* analysis was aborted: pop the call stack and inform the caller *)
Dataflow.mark_degeneration ();
- Db.Value.mark_as_computed ();
Dataflow.merge_results ();
raise e
end
--
GitLab