[Eva] always compute flamegraph information

src/plugins/eva/Eva.mli

@@ -132,8 +132,12 @@ module Callstack: sig
 
   include Datatype.S_with_collections with type t = callstack
 
-  (** Prints a callstack without displaying call sites. *)
-  val pretty_short : Format.formatter -> t -> unit
+  (** Prints a callstack without displaying call sites.
+      ~sep is the separator between function names.
+      ~hide_hash forces printing wihout hash (see {!pretty_hash}),
+      useful when a precise format is expected. *)
+  val pretty_short :
+    hide_hash:bool -> sep:Pretty_utils.sformat -> Format.formatter -> t -> unit
 
   (** Prints a hash of the callstack when '-kernel-msg-key callstack'
       is enabled (prints nothing otherwise). *)

src/plugins/eva/engine/compute_functions.ml

@@ -261,7 +261,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
       | Kstmt stmt when Parameters.ValShowProgress.get () ->
         Self.feedback
           "@[computing for function %a.@\nCalled from %a.@]"
-          Callstack.pretty_short call.callstack
+          (Callstack.pretty_short ~hide_hash:false ~sep:" <- ") call.callstack
           Cil_datatype.Location.pretty (Cil_datatype.Stmt.loc stmt)
       | _ -> ()
     end;

src/plugins/eva/types/callstack.ml

@@ -172,10 +172,10 @@ let pretty_hash fmt callstack =
     Format.fprintf fmt "<%s> " (base58_of_int (stable_hash callstack))
   else Format.ifprintf fmt ""
 
-let pretty_short fmt callstack =
-  Format.fprintf fmt "%a" pretty_hash callstack;
+let pretty_short ~hide_hash ~sep fmt callstack =
+  if not hide_hash then Format.fprintf fmt "%a" pretty_hash callstack;
   let list = List.rev (to_kf_list callstack) in
-  Pretty_utils.pp_flowlist ~left:"" ~sep:" <- " ~right:""
+  Pretty_utils.pp_flowlist ~left:"" ~sep ~right:""
     (fun fmt kf -> Kernel_function.pretty fmt kf)
     fmt list
 

src/plugins/eva/types/callstack.mli

@@ -41,8 +41,12 @@ type callstack = {
 
 include Datatype.S_with_collections with type t = callstack
 
-(** Prints a callstack without displaying call sites. *)
-val pretty_short : Format.formatter -> t -> unit
+(** Prints a callstack without displaying call sites.
+    ~sep is the separator between function names.
+    ~hide_hash forces printing wihout hash (see {!pretty_hash}),
+    useful when a precise format is expected. *)
+val pretty_short :
+  hide_hash:bool -> sep:Pretty_utils.sformat -> Format.formatter -> t -> unit
 
 (** Prints a hash of the callstack when '-kernel-msg-key callstack'
     is enabled (prints nothing otherwise). *)

src/plugins/eva/utils/eva_perf.ml

@@ -353,7 +353,7 @@ let reset_perf () =
 
 (* Set to [Some _] if option [-eva-flamegraph] is set and [main] is
    currently being analyzed and the file is ok. Otherwise, set to [None]. *)
-let oc_flamegraph = ref None
+let oc_fmt_flamegraph = ref None
 
 let stack_flamegraph = ref []
 (* Callstack for flamegraphs. The most recent function is at the top of the
@@ -374,16 +374,6 @@ module EvaFlamegraph =
       let size = 20
     end)
 
-(* pretty-prints the functions in a Value callstack, starting by main (i.e.
-   in reverse order). *)
-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)
-    | kf :: q -> Printf.fprintf oc "%s;%a" (Kernel_function.get_name kf) aux q
-  in
-  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] *)
 let update_self_total_time time =
@@ -398,36 +388,30 @@ let start_doing_flamegraph callstack =
   match callstack.Callstack.stack with
   | [] ->
     (* Analysis of main *)
+    EvaFlamegraph.clear ();
+    stack_flamegraph := [ (Sys.time (), 0.) ];
     if not (Parameters.ValPerfFlamegraphs.is_empty ()) then begin
       let file = Parameters.ValPerfFlamegraphs.get () in
       try
-        (* Flamegraphs must be computed. Set up the stack and the output file *)
-        EvaFlamegraph.clear ();
         let oc = open_out (file:>string) in
-        oc_flamegraph := Some oc;
-        stack_flamegraph := [ (Sys.time (), 0.) ]
+        oc_fmt_flamegraph := Some (oc, Format.formatter_of_out_channel oc);
       with e ->
         Self.error "cannot open flamegraph file: %s"
           (Printexc.to_string e);
-        oc_flamegraph := None (* to be on the safe side  *)
+        oc_fmt_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 *)
-      let time = Sys.time () in
-      update_self_total_time time;
-      stack_flamegraph := (time, 0.) :: !stack_flamegraph;
+    let time = Sys.time () in
+    update_self_total_time time;
+    stack_flamegraph := (time, 0.) :: !stack_flamegraph;
 ;;
 
 (* called when the analysis of a function ends. This function is at the top
    of [callstack] *)
 let stop_doing_flamegraph callstack =
-  match !oc_flamegraph with
-  | None -> ()
-  | Some oc -> (* Flamegraphs are being recorded *)
-    let time = Sys.time() in
-    update_self_total_time time; (* update current function *)
+  let time = Sys.time() in
+  update_self_total_time time; (* update current function *)
+  begin
     match !stack_flamegraph with
     | [] -> assert false
     | (_, total) :: q ->
@@ -436,8 +420,14 @@ let stop_doing_flamegraph callstack =
         try EvaFlamegraph.find callstack with Not_found -> 0.0
       in
       EvaFlamegraph.replace callstack (prev_total +. total);
-      Printf.fprintf oc "%a %.3f\n%!"
-        pretty_callstack callstack (total *. 1000.);
+      begin
+        match !oc_fmt_flamegraph with
+        | None -> ()
+        | Some (_, fmt) -> (* Flamegraphs are being written to a file *)
+          Format.fprintf fmt "%a %.3f\n%!"
+            (Callstack.pretty_short ~hide_hash:true ~sep:";") callstack
+            (total *. 1000.)
+      end;
       match q with
       | [] -> stack_flamegraph := [] (* we are back to the main function *)
       | (_, total_caller) :: q' ->
@@ -445,15 +435,15 @@ let stop_doing_flamegraph callstack =
            the 'current time' information, so that the time spent in the
            callee is not counted. *)
         stack_flamegraph := (time, total_caller) :: q'
-;;
+  end
 
 let reset_flamegraph () =
-  match !oc_flamegraph with
+  EvaFlamegraph.clear ();
+  stack_flamegraph := [];
+  match !oc_fmt_flamegraph with
   | None -> ()
-  | Some fd ->
-    close_out fd; stack_flamegraph := []; oc_flamegraph := None;
-    EvaFlamegraph.clear ()
-
+  | Some (oc, _) ->
+    close_out oc; oc_fmt_flamegraph := None
 
 (* -------------------------------------------------------------------------- *)
 (* --- Exported interface                                                 --- *)
@@ -461,19 +451,15 @@ let reset_flamegraph () =
 
 let start_doing callgraph =
   start_doing_perf callgraph;
-  start_doing_flamegraph callgraph;
-;;
+  start_doing_flamegraph callgraph
 
 let stop_doing callgraph =
   stop_doing_perf callgraph;
-  stop_doing_flamegraph callgraph;
-;;
-
+  stop_doing_flamegraph callgraph
 
 let reset () =
   reset_perf ();
-  reset_flamegraph ();
-;;
+  reset_flamegraph ()
 
 
 (* TODO: Output files with more graphical outputs, such as