From 3f5e9b2b6bd5ad00ce5a0b020e69c79732d4ee7a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 11 Jul 2023 12:09:47 +0200
Subject: [PATCH] [Eva] Eva_utils: slightly changes API to modify the current
callstack.
Replaces [set_call_stack] by [init_call_stack].
Removes [legacy_call_stack], which is never used.
Comments all function in the interface.
---
src/plugins/eva/engine/compute_functions.ml | 4 +---
src/plugins/eva/utils/eva_utils.ml | 18 +++++++---------
src/plugins/eva/utils/eva_utils.mli | 23 +++++++++++++++++----
3 files changed, 28 insertions(+), 17 deletions(-)
diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 3ec8ff93ca4..58c9b2173fc 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -352,8 +352,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let compute kf init_state =
let restore_signals = register_signal_handler () in
let compute () =
- let callstack = Callstack.init kf in
- Eva_utils.set_call_stack callstack;
+ let callstack = Eva_utils.init_call_stack kf in
store_initial_state callstack kf init_state;
let call = { kf; callstack; arguments = []; rest = []; return = None; } in
let final_result = compute_call Kglobal call None init_state in
@@ -372,7 +371,6 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
let cleanup () =
Abstract.Dom.Store.mark_as_computed ();
Self.(set_computation_state Aborted);
- Eva_utils.clear_call_stack ();
post_analysis_cleanup ~aborted:true
in
Eva_utils.protect compute ~cleanup
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index 5982ade6c13..73dc03924ed 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -33,31 +33,29 @@ let clear_call_stack () =
Eva_perf.stop_doing cs;
current_callstack := None
-let set_call_stack cs =
+let init_call_stack kf =
assert (!current_callstack = None);
+ let cs = Callstack.init kf in
current_callstack := Some cs;
- Eva_perf.start_doing cs
+ Eva_perf.start_doing cs;
+ cs
let current_call_stack_opt () = !current_callstack
let current_call_stack () =
match !current_callstack with
- | None -> invalid_arg "callstack not initialized"
+ | None -> Self.fatal "Callstack not initialized"
| Some cs -> cs
let current_kf () =
let cs = current_call_stack () in
Callstack.top_kf cs
-let legacy_call_stack () =
- match !current_callstack with
- | None -> []
- | Some cs -> Callstack.to_legacy cs
-
let push_call_stack kf stmt =
let cs = current_call_stack () in
- current_callstack := Some (Callstack.push kf stmt cs);
- Eva_perf.start_doing cs
+ let new_cs = Callstack.push kf stmt cs in
+ current_callstack := Some new_cs;
+ Eva_perf.start_doing new_cs
let pop_call_stack () =
let cs = current_call_stack () in
diff --git a/src/plugins/eva/utils/eva_utils.mli b/src/plugins/eva/utils/eva_utils.mli
index 69ea3f0bfc5..2e3ab131c5c 100644
--- a/src/plugins/eva/utils/eva_utils.mli
+++ b/src/plugins/eva/utils/eva_utils.mli
@@ -25,16 +25,31 @@ open Cil_types
(** {2 Callstacks related types and functions} *)
(** Functions dealing with call stacks. *)
+
+(** Clears the current callstack: future accesses to the current callstack
+ will fail. *)
val clear_call_stack : unit -> unit
-val set_call_stack : Callstack.t -> unit
+
+(** Initializes the current callstack with the main entry point. *)
+val init_call_stack : kernel_function -> Callstack.t
+
+(** Push a new call to the current callstack. *)
val push_call_stack : kernel_function -> stmt -> unit
+
+(** Removes the topmost call from the current callstack. *)
val pop_call_stack : unit -> unit
-(** The current function is the one on top of the call stack. *)
+(** Returns the current function, at the top of the current callstack.
+ Fails if no callstack has been initialized. This should only be called
+ during the analysis of a function. *)
val current_kf : unit -> kernel_function
-val current_call_stack_opt : unit -> Callstack.t option
+
+(** Returns the current callstack; fails if it has not been initialized.
+ This should only be called during the analysis of a function. *)
val current_call_stack : unit -> Callstack.t
-val legacy_call_stack : unit -> Value_types.callstack
+
+(** Returns the current callstack, or [None] if it has not been initialized. *)
+val current_call_stack_opt : unit -> Callstack.t option
(** Prints the current callstack. *)
val pp_callstack : Format.formatter -> unit
--
GitLab