diff --git a/src/kernel_services/abstract_interp/eva_types.ml b/src/kernel_services/abstract_interp/eva_types.ml
index aa8a24814b93ab2033a6351bc5ee53132465ba97..6d07a6664995b30734696addf631c57096f3a1f2 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 bffc1c71b201c34854dac48d2ff758f8fc2a48dc..57944aea8dfd6898296bd6a318ff11197b549e71 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 45bcd42e26f41b3408ee3781474fcdbe14301314..7cf6b0097b1d86f42761050b1104c3ccaf7e207d 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 9476b2a7386b9f9993e0e99bcdf51434f03e2d88..6460b8d5bc2fac91104ac585f4b5b0e444a57fcb 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 1efc3d7c32ab56ef25903adfc736f74add3278af..e8bd382190ec9b9a71970290f74b19f38cd7ae72 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 2c0a2edd183946a7d6970bd7139e2560a7f62ec5..cb4a2af9a1eb768e56c5e454594206e1ef4b0fdf 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 c6b504fd2f4715fe7b009d27ba7aea1cfa5f918e..5982ade6c130c22c16394b134f54f8e6222f1175 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 =