Improve timing, add Trace Event Format output

.semgrep/timing.yml

@@ -0,0 +1,16 @@
+rules:
+  - id: cil-stats
+    pattern-either:
+      - pattern: Stats.$FUN
+      - pattern: GoblintCil.Stats.$FUN
+    fix: Timing.$FUN
+    message: use Timing instead
+    languages: [ocaml]
+    severity: ERROR
+
+  - id: timing-time-partial
+    patterns:
+      - pattern: Timing.time $NAME $FUNC $ARG $BADARG ...
+    message: Timing.time measuring only partial, not complete function application (see https://goblint.readthedocs.io/en/latest/developer-guide/profiling/#timing)
+    languages: [ocaml]
+    severity: ERROR

conf/incremental.json

@@ -28,9 +28,11 @@
     "trace": {
       "context": true
     },
-    "debug": true
+    "debug": true,
+    "timing": {
+      "enabled": true
+    }
   },
-  "printstats": true,
   "result": "none",
   "solver": "td3",
   "solvers": {

conf/minimal_incremental.json

@@ -27,9 +27,11 @@
     "trace": {
       "context": true
     },
-    "debug": true
+    "debug": true,
+    "timing": {
+      "enabled": true
+    }
   },
-  "printstats": true,
   "result": "none",
   "solver": "td3",
   "solvers": {

conf/zstd-race.json

@@ -75,7 +75,11 @@
       "inlines": false
     }
   },
-  "printstats": true,
+  "dbg": {
+    "timing": {
+      "enabled": true
+    }
+  },
   "warn": {
     "assert": false,
     "behavior": false,

docs/developer-guide/profiling.md

@@ -1,24 +1,34 @@
 # Profiling
 
-## Stats
-`Stats` is an OCaml module from CIL that can be used to profile certain parts of code.
+## Timing
+`Timing` is an OCaml module (based on CIL's `Stats`) that can be used to profile certain parts of code.
 
-Wrap the function call to be profiled with `Stats.time`. For example, replace
+Wrap the function call to be profiled with `Timing.wrap`. For example, replace
 ```ocaml
 f x y z
 ```
 with
 ```ocaml
-Stats.time "mything" (f x y) z
+Timing.wrap "mything" (f x y) z
 ```
 where `mything` should be replaced with a relevant name to be shown in the output.
 Note that all but the last argument are partially applied to `f`.
-The last argument is given separately for `Stats.time` to apply and measure.
+The last argument is given separately for `Timing.wrap` to apply and measure.
 
-Then run Goblint with `--enable printstats` or `-v` (verbose) to see the timing stats under `Timings:`.
+Then run Goblint with `--enable dbg.timing.enabled` or `-v` (verbose) to see the timing stats under `Timings:`.
 
-The timings are automatically presented as a tree which follows the nesting of `Stats.time` calls.
-Unlike [tracing](./debugging.md#tracing), timings cannot be toggled easily, so be considerate of where you leave them after doing the profiling.
+The timings are automatically presented as a tree which follows the nesting of `Timing.wrap` calls.
+Unlike [tracing](./debugging.md#tracing), timings cannot be toggled easily individually, so be considerate of where you leave them after doing the profiling.
+
+### Trace Event Format
+[Trace Event Format (TEF)](https://docs.google.com/document/d/1CvAClvFfyA5R-PhYUmn5OOQtYMH4h6I0nSsKchNAySU/edit) is a simple JSON-based format for profiling data.
+Besides just accumulating timing information, all timed calls are individually recorded, allowing flamegraph-style visualization.
+
+Goblint can produce a TEF file with
+```console
+--enable dbg.timing.enabled --set dbg.timing.tef goblint.timing.json
+```
+Then open `goblint.timing.json` in [Perfetto UI](https://ui.perfetto.dev/).
 
 
 ## perf

dune-project

@@ -48,6 +48,8 @@
     arg-complete
     yaml
     uuidm
+    catapult
+    catapult-file
     (conf-gmp (>= 3)) ; only needed transitively, but they don't have lower bound, which is needed on MacOS
     (conf-ruby :with-test)
     (benchmark :with-test) ; TODO: make this optional somehow, (optional) on bench executable doesn't work

goblint.opam

@@ -42,6 +42,8 @@ depends: [
   "arg-complete"
   "yaml"
   "uuidm"
+  "catapult"
+  "catapult-file"
   "conf-gmp" {>= "3"}
   "conf-ruby" {with-test}
   "benchmark" {with-test}
@@ -72,7 +74,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
-  [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#d4724fe93b0356c611b0b0bd2172210d3f1eeb5b" ]
+  [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#bfb977b48d6d92e0ecbdab2e04f2576095506107" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # TODO: add back after release, only pinned for CI stability

goblint.opam.locked

@@ -34,6 +34,8 @@ depends: [
   "bigstringaf" {= "0.8.0"}
   "bos" {= "0.2.1"}
   "camlidl" {= "1.09"}
+  "catapult" {= "0.1.1"}
+  "catapult-file" {= "0.1.1"}
   "cmdliner" {= "1.1.1" & with-doc}
   "conf-autoconf" {= "0.1"}
   "conf-gcc" {= "1.0"}
@@ -122,7 +124,7 @@ available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
   [
     "goblint-cil.2.0.0"
-    "git+https://github.com/goblint/cil.git#d4724fe93b0356c611b0b0bd2172210d3f1eeb5b"
+    "git+https://github.com/goblint/cil.git#bfb977b48d6d92e0ecbdab2e04f2576095506107"
   ]
   [
     "apron.v0.9.13"

goblint.opam.template

@@ -2,7 +2,7 @@
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
 pin-depends: [
-  [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#d4724fe93b0356c611b0b0bd2172210d3f1eeb5b" ]
+  [ "goblint-cil.2.0.0" "git+https://github.com/goblint/cil.git#bfb977b48d6d92e0ecbdab2e04f2576095506107" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # TODO: add back after release, only pinned for CI stability

scripts/test-incremental-multiple.sh

@@ -7,7 +7,7 @@ conf=$base/$test.json
 patch1=$base/${test}_1.patch
 patch2=$base/${test}_2.patch
 
-args="--enable dbg.debug --enable printstats -v"
+args="--enable dbg.debug --enable dbg.timing.enabled -v"
 
 cat $source
 

scripts/test-incremental.sh

@@ -11,7 +11,7 @@ source=$base/$test.c
 conf=$base/$test.json
 patch=$base/$test.patch
 
-args="--enable dbg.debug --enable printstats -v --enable allglobs"
+args="--enable dbg.debug --enable dbg.timing.enabled -v --enable allglobs"
 
 ./goblint --conf $conf $args --enable incremental.save $source &> $base/$test.before.log
 

scripts/update_suite.rb

@@ -368,7 +368,7 @@ def run_testset (testset, cmd, starttime)
 
   def run
     filename = File.basename(@path)
-    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --set goblint-dir .goblint-#{@id.sub('/','-')} 2>#{@testset.statsfile}"
+    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --set goblint-dir .goblint-#{@id.sub('/','-')} 2>#{@testset.statsfile}"
     starttime = Time.now
     run_testset(@testset, cmd, starttime)
   end
@@ -434,8 +434,8 @@ def create_test_set(lines)
 
   def run
     filename = File.basename(@path)
-    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --enable incremental.save --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-save 2>#{@testset.statsfile}"
-    cmd_incr = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset_incr.warnfile} --set printstats true --enable incremental.load --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-load 2>#{@testset_incr.statsfile}"
+    cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --enable incremental.save --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-save 2>#{@testset.statsfile}"
+    cmd_incr = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset_incr.warnfile} --enable dbg.timing.enabled --enable incremental.load --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-load 2>#{@testset_incr.statsfile}"
     starttime = Time.now
     run_testset(@testset_incr, cmd, starttime)
     # apply patch
@@ -478,8 +478,8 @@ def create_test_set(lines)
   end
   def run ()
     filename = File.basename(@path)
-    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --set save_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-save 2>#{@testset.statsfile}"
-    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set printstats true --conf run/config.json --set save_run '' --set load_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-load 2>#{@testset.statsfile}"
+    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --set save_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-save 2>#{@testset.statsfile}"
+    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --conf run/config.json --set save_run '' --set load_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-load 2>#{@testset.statsfile}"
     starttime = Time.now
     run_testset(@testset, cmd1, starttime)
     run_testset(@testset, cmd2, starttime)

src/analyses/accessAnalysis.ml

@@ -245,7 +245,7 @@ struct
         | `Left g' -> (* accesses *)
           (* ignore (Pretty.printf "WarnGlobal %a\n" CilType.Varinfo.pretty g); *)
           let accs = G.access (ctx.global g) in
-          Stats.time "access" (Access.warn_global safe vulnerable unsafe g') accs
+          Timing.wrap "access" (Access.warn_global safe vulnerable unsafe g') accs
         | `Right _ -> (* vars *)
           ()
       end

src/analyses/apron/apronAnalysis.apron.ml

@@ -603,7 +603,7 @@ struct
       RH.map (fun _ -> AD.to_oct) m
     in
     let post_process m =
-      let m = Stats.time "convert" convert m in
+      let m = Timing.wrap "convert" convert m in
       RH.map (fun _ v -> OctApron.marshal v) m
     in
     let results = post_process results in
@@ -615,7 +615,7 @@ struct
     let file = GobConfig.get_string "exp.apron.prec-dump" in
     if file <> "" then begin
       Printf.printf "exp.apron.prec-dump is potentially costly (for domains other than octagons), do not use for performance data!\n";
-      Stats.time "apron.prec-dump" store_data (Fpath.v file)
+      Timing.wrap "apron.prec-dump" store_data (Fpath.v file)
     end;
     Priv.finalize ()
 end

src/analyses/basePriv.ml

@@ -1528,7 +1528,7 @@ struct
   module G = Priv.G
   module V = Priv.V
 
-  let time str f arg = Stats.time "priv" (Stats.time str f) arg
+  let time str f arg = Timing.wrap "priv" (Timing.wrap str f) arg
 
   let startstate = Priv.startstate
   let read_global ask getg st x = time "read_global" (Priv.read_global ask getg st) x

src/analyses/deadlock.ml

@@ -108,7 +108,7 @@ struct
         end
       in
 
-      Stats.time "deadlock" (iter_lock LS.empty []) g
+      Timing.wrap "deadlock" (iter_lock LS.empty []) g
     | _ -> Queries.Result.top q
 end
 

src/domains/mapDomain.ml

@@ -287,7 +287,7 @@ module Timed (M: S) : S with
   type key = M.key and
   type value = M.value =
 struct
-  let time str f arg = GoblintCil.Stats.time (M.name ()) (GoblintCil.Stats.time str f) arg
+  let time str f arg = Timing.wrap (M.name ()) (Timing.wrap str f) arg
 
   (* Printable.S *)
   type t = M.t

src/dune

@@ -7,7 +7,7 @@
   (name goblint_lib)
   (public_name goblint.lib)
   (modules :standard \ goblint mainspec privPrecCompare apronPrecCompare messagesCompare)
-  (libraries goblint.sites goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm
+  (libraries goblint.sites goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult
     ; Conditionally compile based on whether apron optional dependency is installed or not.
     ; Alternative dependencies seem like the only way to optionally depend on optional dependencies.
     ; See: https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies.

src/framework/analyses.ml

@@ -252,14 +252,9 @@ struct
         BatPrintf.fprintf f "<run>";
         BatPrintf.fprintf f "<parameters>%s</parameters>" Goblintutil.command_line;
         BatPrintf.fprintf f "<statistics>";
-        (* FIXME: This is a super ridiculous hack we needed because BatIO has no way to get the raw channel CIL expects here. *)
-        let name, chn = Filename.open_temp_file "stat" "goblint" in
-        Stats.print chn "";
-        Stdlib.close_out chn;
-        let f_in = BatFile.open_in name in
-        let s = BatIO.read_all f_in in
-        BatIO.close_in f_in;
-        BatPrintf.fprintf f "%s" s;
+        let timing_ppf = BatFormat.formatter_of_out_channel f in
+        Timing.Default.print timing_ppf;
+        Format.pp_print_flush timing_ppf ();
         BatPrintf.fprintf f "</statistics>";
         BatPrintf.fprintf f "<result>\n";
         BatEnum.iter (fun b -> BatPrintf.fprintf f "<file name=\"%s\" path=\"%s\">\n%a</file>\n" (Filename.basename b) b p_funs (SH.find_all file2funs b)) (BatEnum.uniq @@ SH.keys file2funs);

src/framework/cfgTools.ml

@@ -113,7 +113,7 @@ let computeSCCs (module Cfg: CfgBidir) nodes =
   );
   r
 
-let computeSCCs x = Stats.time "computeSCCs" (computeSCCs x)
+let computeSCCs x = Timing.wrap "computeSCCs" (computeSCCs x)
 
 let rec pretty_edges () = function
   | [] -> Pretty.dprintf ""
@@ -359,7 +359,7 @@ let createCFG (file: file) =
           | ComputedGoto _ ->
             failwith "MyCFG.createCFG: unsupported stmt"
         in
-        Stats.time "handle" (List.iter handle) fd.sallstmts;
+        Timing.wrap ~args:[("function", `String fd.svar.vname)] "handle" (List.iter handle) fd.sallstmts;
 
         if Messages.tracing then Messages.trace "cfg" "Over\n";
 
@@ -436,7 +436,7 @@ let createCFG (file: file) =
           else
             NH.iter (NH.replace node_scc_global) node_scc; (* there's no merge inplace *)
         in
-        Stats.time "iter_connect" iter_connect ();
+        Timing.wrap ~args:[("function", `String fd.svar.vname)] "iter_connect" iter_connect ();
 
         (* Verify that function is now connected *)
         let reachable_return' = find_backwards_reachable ~initial_size:(NH.keys fd_nodes |> BatEnum.hard_count) (module TmpCfg) (Function fd) in
@@ -450,7 +450,7 @@ let createCFG (file: file) =
     ignore (Pretty.eprintf "cfgF (%a), cfgB (%a)\n" GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgF) GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgB));
   cfgF, cfgB
 
-let createCFG = Stats.time "createCFG" createCFG
+let createCFG = Timing.wrap "createCFG" createCFG
 
 
 let minimizeCFG (fw,bw) =
@@ -580,7 +580,7 @@ let getCFG (file: file) : cfg * cfg =
   let cfgF, cfgB = createCFG file in
   let cfgF, cfgB =
     if get_bool "exp.mincfg" then
-      Stats.time "minimizing the cfg" minimizeCFG (cfgF, cfgB)
+      Timing.wrap "minimizing the cfg" minimizeCFG (cfgF, cfgB)
     else
       (cfgF, cfgB)
   in

src/framework/constraints.ml

@@ -690,12 +690,18 @@ struct
 
   let tf (v,c) (e,u) getl sidel getg sideg =
     let old_node = !current_node in
+    let old_fd = Option.map Node.find_fundec old_node |? Cil.dummyFunDec in
+    let new_fd = Node.find_fundec v in
+    if not (CilType.Fundec.equal old_fd new_fd) then
+      Timing.Program.enter new_fd.svar.vname;
     let old_context = !M.current_context in
     current_node := Some u;
     M.current_context := Some (Obj.repr c);
     Fun.protect ~finally:(fun () ->
         current_node := old_node;
-        M.current_context := old_context
+        M.current_context := old_context;
+        if not (CilType.Fundec.equal old_fd new_fd) then
+          Timing.Program.exit new_fd.svar.vname
       ) (fun () ->
         let d       = tf (v,c) (e,u) getl sidel getg sideg in
         d

src/framework/control.ml

@@ -332,7 +332,7 @@ struct
 
     let startstate, more_funs =
       if (get_bool "dbg.verbose") then print_endline ("Initializing "^string_of_int (CfgTools.numGlobals file)^" globals.");
-      Stats.time "global_inits" do_global_inits file
+      Timing.wrap "global_inits" do_global_inits file
     in
 
     let otherfuns = if get_bool "kernel" then otherfuns @ more_funs else otherfuns in
@@ -463,7 +463,7 @@ struct
           if get_bool "dbg.verbose" then
             print_endline ("Solving the constraint system with " ^ get_string "solver" ^ ". Solver statistics are shown every " ^ string_of_int (get_int "dbg.solver-stats-interval") ^ "s or by signal " ^ get_string "dbg.solver-signal" ^ ".");
           Goblintutil.should_warn := get_string "warn_at" = "early" || gobview;
-          let (lh, gh), solver_data = Stats.time "solving" (Slvr.solve entrystates entrystates_global) startvars' in
+          let (lh, gh), solver_data = Timing.wrap "solving" (Slvr.solve entrystates entrystates_global) startvars' in
           if GobConfig.get_bool "incremental.save" then
             Serialize.Cache.(update_data SolverData solver_data);
           if save_run_str <> "" then (
@@ -494,7 +494,7 @@ struct
               Serialize.marshal MCPRegistry.registered_name analyses;
               Serialize.marshal (file, Cabs2cil.environment) cil;
               Serialize.marshal !Messages.Table.messages_list warnings;
-              Serialize.marshal (Stats.top, Gc.quick_stat ()) stats
+              Serialize.marshal (Timing.Default.root, Gc.quick_stat ()) stats
             );
             Goblintutil.(self_signal (signal_of_string (get_string "dbg.solver-signal"))); (* write solver_stats after solving (otherwise no rows if faster than dbg.solver-stats-interval). TODO better way to write solver_stats without terminal output? *)
           );
@@ -645,7 +645,7 @@ struct
       | `Right _ -> (* contexts global *)
         ()
     in
-    Stats.time "warn_global" (GHT.iter warn_global) gh;
+    Timing.wrap "warn_global" (GHT.iter warn_global) gh;
 
     if get_bool "ana.sv-comp.enabled" then
       WResult.write lh gh entrystates;