fix timing statistics

Author: stilscher

src/state/state.ml

@@ -22,7 +22,7 @@ type t = {
   goblint : GvGoblint.solver_state;
   warnings : GvMessages.t;
   meta : Yojson.Safe.t;
-  stats : Stats.t * Gc.stat;
+  stats : Timing.tree * Gc.stat;
   file_loc : (string, string) Hashtbl.t;
   display : display option;
   inspect : inspect option;
@@ -37,7 +37,7 @@ let default =
     goblint = GvGoblint.empty;
     warnings = [];
     meta = `Null;
-    stats = (Stats.top, Gc.quick_stat ());
+    stats = (Timing.create_tree "default", Gc.quick_stat ());
     file_loc = Hashtbl.create 113;
     display = None;
     inspect = None;

src/state/timing.ml

@@ -0,0 +1,20 @@
+
+(** Timing tree node. *)
+type tree = {
+  name: string; (** Name of node. *)
+  mutable cputime: float; (** Accumulated CPU time in seconds. *)
+  mutable walltime: float; (** Accumulated wall time in seconds. *)
+  mutable allocated: float; (** Accumulated allocated memory in bytes. *)
+  mutable count: int; (** Number of repetitions. Only set if {!Timing.countCalls} is true. *)
+  mutable children: tree list; (** Child nodes. *)
+}
+
+let create_tree name =
+  {
+    name = name;
+    cputime = 0.0;
+    walltime = 0.0;
+    allocated = 0.0;
+    count = 0;
+    children = [];
+  }

src/ui/panel/gvStatisticsView.re

@@ -1,21 +1,20 @@
 open Batteries;
-module Stats = GoblintCil.Stats;
 
 let rec make_task_list = tasks =>
   if (List.is_empty(tasks)) {
     React.null;
   } else {
     <ul>
       {tasks
-       |> List.mapi((i, task: Stats.t) => {
+       |> List.mapi((i, task: Timing.tree) => {
             let key = string_of_int(i);
             <li key>
               {task.name
                ++ ": "
-               ++ string_of_float(task.time)
+               ++ string_of_float(task.cputime)
                ++ " s"
                |> React.string}
-              {task.sub |> List.rev |> make_task_list}
+              {task.children |> List.rev |> make_task_list}
             </li>;
           })
        |> React.list}
@@ -26,16 +25,23 @@ let as_megabytes = words => Printf.sprintf("%.2f MB", words /. 131072.0);
 
 [@react.component]
 let make = (~stats) => {
-  let (time: Stats.t, gc: Gc.stat) = stats;
+  let (time: Timing.tree, gc: Gc.stat) = stats;
   let total =
-    time.sub |> List.fold_left((acc, sub: Stats.t) => acc +. sub.time, 0.0);
+    time.children |> List.fold_left((acc, sub: Timing.tree) => acc +. sub.cputime, 0.0);
 
   <div>
-    <span>
+    {if(total == 0.) {
+      <div className="bg-warning">
+        {"For timing statistics the analysis has to be run with -v (alternatively, either option dbg.verbose or dbg.timing.enabled can be activated)" |> React.string}
+      </div>;
+    } else {
+      React.null
+    }}
+    <div>
       {"Total: " ++ string_of_float(total) ++ " s" |> React.string}
-    </span>
-    {time.sub |> List.rev |> make_task_list}
-    <span>
+    </div>
+    {time.children |> List.rev |> make_task_list}
+    <div>
       {Printf.sprintf(
          "Memory: total=%s, max=%s, minor=%s, major=%s, promoted=%s, minor collections=%d, major collections=%d, compactions=%d",
          as_megabytes(gc.minor_words +. gc.major_words -. gc.promoted_words),
@@ -48,6 +54,6 @@ let make = (~stats) => {
          gc.compactions,
        )
        |> React.string}
-    </span>
+    </div>
   </div>;
 };