From 2d0e69c191405135d29f0ada2d0d14d00f05acf7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 11 Jul 2023 10:04:10 +0200
Subject: [PATCH] [Eva] Uses new callstack type in Eva_perf.
---
.../abstract_interp/eva_types.ml | 11 +++---
.../abstract_interp/eva_types.mli | 1 +
src/plugins/eva/Eva.mli | 2 +
src/plugins/eva/types/callstack.mli | 2 +
src/plugins/eva/utils/eva_perf.ml | 37 +++++++++----------
src/plugins/eva/utils/eva_perf.mli | 4 +-
src/plugins/eva/utils/eva_utils.ml | 8 ++--
7 files changed, 35 insertions(+), 30 deletions(-)
diff --git a/src/kernel_services/abstract_interp/eva_types.ml b/src/kernel_services/abstract_interp/eva_types.ml
index aa8a24814b9..6d07a666499 100644
--- a/src/kernel_services/abstract_interp/eva_types.ml
+++ b/src/kernel_services/abstract_interp/eva_types.ml
@@ -126,13 +126,14 @@ struct
(* Conversion *)
- let to_legacy cs =
+ let to_kf_list cs = cs.entry_point :: List.rev_map fst cs.stack
+ let to_stmt_list cs = List.rev_map snd cs.stack
+
+ let to_call_list cs =
let l =
List.rev_map (fun (kf, stmt) -> (kf, Cil_types.Kstmt stmt)) cs.stack
in
- List.rev ((cs.entry_point, Cil_types.Kglobal) :: l)
+ (cs.entry_point, Cil_types.Kglobal) :: l
- let to_kf_list cs = cs.entry_point :: List.rev_map fst cs.stack
-
- let to_stmt_list cs = List.rev_map snd cs.stack
+ let to_legacy cs = List.rev (to_call_list cs)
end
diff --git a/src/kernel_services/abstract_interp/eva_types.mli b/src/kernel_services/abstract_interp/eva_types.mli
index bffc1c71b20..57944aea8df 100644
--- a/src/kernel_services/abstract_interp/eva_types.mli
+++ b/src/kernel_services/abstract_interp/eva_types.mli
@@ -54,6 +54,7 @@ sig
val to_legacy : t -> Value_types.callstack
val to_kf_list : t -> Cil_types.kernel_function list
val to_stmt_list : t -> Cil_types.stmt list
+ val to_call_list : t -> (Cil_types.kernel_function * Cil_types.kinstr) list
end
[@@alert db_deprecated
"Eva_types is only provided for compatibility reason and will be removed \
diff --git a/src/plugins/eva/Eva.mli b/src/plugins/eva/Eva.mli
index 45bcd42e26f..7cf6b0097b1 100644
--- a/src/plugins/eva/Eva.mli
+++ b/src/plugins/eva/Eva.mli
@@ -168,6 +168,8 @@ module Callstack: sig
(** Gives the list of call statements from the bottom to the top of the callstack (i.e. reverse order of the call stack). *)
val to_stmt_list : t -> Cil_types.stmt list
+ val to_call_list : t -> (Cil_types.kernel_function * Cil_types.kinstr) list
+
end
module Results: sig
diff --git a/src/plugins/eva/types/callstack.mli b/src/plugins/eva/types/callstack.mli
index 9476b2a7386..6460b8d5bc2 100644
--- a/src/plugins/eva/types/callstack.mli
+++ b/src/plugins/eva/types/callstack.mli
@@ -73,6 +73,8 @@ val to_kf_list : t -> Cil_types.kernel_function list
(** Gives the list of call statements from the bottom to the top of the callstack (i.e. reverse order of the call stack). *)
val to_stmt_list : t -> Cil_types.stmt list
+val to_call_list : t -> (Cil_types.kernel_function * Cil_types.kinstr) list
+
[@@@ api_end]
val pretty_debug : Format.formatter -> t -> unit
diff --git a/src/plugins/eva/utils/eva_perf.ml b/src/plugins/eva/utils/eva_perf.ml
index 1efc3d7c32a..e8bd382190e 100644
--- a/src/plugins/eva/utils/eva_perf.ml
+++ b/src/plugins/eva/utils/eva_perf.ml
@@ -218,7 +218,8 @@ module Imperative_callstack_trie(M:sig type t val default:unit -> t end) = struc
n
in find_subtree subnode.subtree b (Some subnode)
- let find_subtree t callstack = find_subtree t (List.rev callstack) None
+ let find_subtree t callstack =
+ find_subtree t (Callstack.to_call_list callstack) None
let find t callstack = (find_subtree t callstack).self
@@ -285,25 +286,25 @@ let display fmt =
end
;;
-let caller_callee_callinfo = function
- | (callee_kf,_)::(caller_kf,_)::_ ->
- (let caller_flat = Kernel_function.Hashtbl.find flat caller_kf in
- try
+let caller_callee_callinfo callstack =
+ match Callstack.last_caller callstack with
+ | Some caller_kf ->
+ let callee_kf = Callstack.top_kf callstack in
+ let caller_flat = Kernel_function.Hashtbl.find flat caller_kf in
+ (try
Kernel_function.Hashtbl.find caller_flat.called_functions callee_kf
with Not_found ->
let call_info = Call_info.create() in
Kernel_function.Hashtbl.add caller_flat.called_functions callee_kf call_info;
call_info)
- | [_] -> Call_info.main
- | [] -> assert false
+ | None -> Call_info.main
;;
let start_doing_perf callstack =
if Parameters.ValShowPerf.get()
then begin
let time = Sys.time() in
- assert (callstack != []);
- let kf = fst (List.hd callstack) in
+ let kf = Callstack.top_kf callstack in
let flat_info =
try Kernel_function.Hashtbl.find flat kf
with Not_found ->
@@ -325,7 +326,7 @@ let stop_doing_perf callstack =
if Parameters.ValShowPerf.get()
then begin
let time = Sys.time() in
- let kf = fst (List.hd callstack) in
+ let kf = Callstack.top_kf callstack in
let flat_info = Kernel_function.Hashtbl.find flat kf in
Call_info.after_call flat_info.call_info time;
let node = Perf_by_callstack.find perf callstack in
@@ -365,14 +366,13 @@ let stack_flamegraph = ref []
(* pretty-prints the functions in a Value callstack, starting by main (i.e.
in reverse order). *)
-let pretty_callstack oc l =
+let pretty_callstack oc callstack =
let rec aux oc = function
| [] -> () (* does not happen in theory *)
- | [main, _] -> Printf.fprintf oc "%s" (Kernel_function.get_name main)
- | (f, _) :: q ->
- Printf.fprintf oc "%a;%s" aux q (Kernel_function.get_name f)
+ | [main] -> Printf.fprintf oc "%s" (Kernel_function.get_name main)
+ | kf :: q -> Printf.fprintf oc "%s;%a" (Kernel_function.get_name kf) aux q
in
- aux oc l
+ aux oc (Callstack.to_kf_list callstack)
(* update the [self_total_time] information for the function being analyzed,
assuming that the current time is [time] *)
@@ -385,9 +385,8 @@ let update_self_total_time time =
(* called when a new function is being analyzed *)
let start_doing_flamegraph callstack =
- match callstack with
- | [] -> assert false
- | [_] ->
+ match callstack.Callstack.stack with
+ | [] ->
(* Analysis of main *)
if not (Parameters.ValPerfFlamegraphs.is_empty ()) then begin
let file = Parameters.ValPerfFlamegraphs.get () in
@@ -401,7 +400,7 @@ let start_doing_flamegraph callstack =
(Printexc.to_string e);
oc_flamegraph := None (* to be on the safe side *)
end
- | _ :: _ :: _ ->
+ | _ :: _ ->
if !oc_flamegraph <> None then
(* Flamegraphs are being computed. Update time spent in current function
so far, then push a slot for the analysis of the new function *)
diff --git a/src/plugins/eva/utils/eva_perf.mli b/src/plugins/eva/utils/eva_perf.mli
index 2c0a2edd183..cb4a2af9a1e 100644
--- a/src/plugins/eva/utils/eva_perf.mli
+++ b/src/plugins/eva/utils/eva_perf.mli
@@ -22,11 +22,11 @@
(** Call [start_doing] when starting analyzing a new function. The new
function is on the top of the call stack.*)
-val start_doing: Value_types.callstack -> unit
+val start_doing: Callstack.t -> unit
(** Call [start_doing] when finishing analyzing a function. The
function must still be on the top of the call stack. *)
-val stop_doing: Value_types.callstack -> unit
+val stop_doing: Callstack.t -> unit
(** Display a complete summary of performance informations. Can be
called during the analysis. *)
diff --git a/src/plugins/eva/utils/eva_utils.ml b/src/plugins/eva/utils/eva_utils.ml
index c6b504fd2f4..5982ade6c13 100644
--- a/src/plugins/eva/utils/eva_utils.ml
+++ b/src/plugins/eva/utils/eva_utils.ml
@@ -30,13 +30,13 @@ let clear_call_stack () =
match !current_callstack with
| None -> ()
| Some cs ->
- Eva_perf.stop_doing (Callstack.to_legacy cs);
+ Eva_perf.stop_doing cs;
current_callstack := None
let set_call_stack cs =
assert (!current_callstack = None);
current_callstack := Some cs;
- Eva_perf.start_doing (Callstack.to_legacy cs)
+ Eva_perf.start_doing cs
let current_call_stack_opt () = !current_callstack
@@ -57,11 +57,11 @@ let legacy_call_stack () =
let push_call_stack kf stmt =
let cs = current_call_stack () in
current_callstack := Some (Callstack.push kf stmt cs);
- Eva_perf.start_doing (Callstack.to_legacy cs)
+ Eva_perf.start_doing cs
let pop_call_stack () =
let cs = current_call_stack () in
- Eva_perf.stop_doing (Callstack.to_legacy cs);
+ Eva_perf.stop_doing cs;
current_callstack := Callstack.pop cs
let pp_callstack fmt =
--
GitLab