package soteria

  1. Overview
  2. Docs
package soteria
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Soteria Statistics Tutorial

Welcome to the Soteria statistics tutorial! This tutorial will guide you through using the Stats module for tracking, aggregating, and reporting metrics during symbolic execution and program analysis.

Today you'll be learning how to:

Introduction

The Soteria statistics system provides a flexible way to collect, aggregate, and report metrics during program analysis. It's particularly useful for:

  • Counting events (branches explored, functions called, etc.)
  • Recording sequences of events (errors found, assumptions made, etc.)
  • Tracking performance metrics (execution time, solver queries, etc.)

A key feature of the statistics system is that it automatically merges statistics from different branches of symbolic execution, using appropriate merge strategies for each statistic type.

Getting Started with Statistics

To collect statistics, you need to wrap your computation with with_. Note that with_ must be called outside of any symbolic process (i.e. outside functions returning 'a Symex.t). Also note that stats are only recorded if the --dump-stats flag is used (or if the output_stats configuration is programmatically set to Some _).

  (* Manually initialising stats configuration, should be done using the
     Cmdliner term in practice *)
  let () =
    Soteria.Stats.Config.set_and_lock { output_stats = Some "stats.json" }
  # let computation () =
      Stats.As_ctx.incr "operations";
      Stats.As_ctx.incr "operations";
      Stats.As_ctx.incr "operations";
      42
  val computation : unit -> int = <fun>
  # Stats.As_ctx.with_ () computation;;
  - : int * Stats.t = (42, <stats>)

Because wrapper functions are a regular pattern in Soteria, we recommend defining some syntax sugar to make this code nicer; this particular syntax is also provided by Soteria's Syntaxes.FunctionWrap module.

  # let ( let@ ) = ( @@ );;
  val ( let@ ) : ('a -> 'b) -> 'a -> 'b = <fun>
  # let@ () = Stats.As_ctx.with_ () in
    computation ();;
  - : int * Stats.t = (42, <stats>)

Basic Counter Operations

The simplest statistics are integer counters. Use incr to increment by 1 or add_int to add any amount:

  # let count_things () =
      (* Increment a counter *)
      Stats.As_ctx.incr "items_processed";
      Stats.As_ctx.incr "items_processed";
      Stats.As_ctx.incr "items_processed";

      (* Add a specific amount *)
      Stats.As_ctx.add_int "bytes_read" 1024;
      Stats.As_ctx.add_int "bytes_read" 2048;

      "done";;
  val count_things : unit -> string = <fun>

  # let result, stats = Stats.As_ctx.with_ () count_things;;
  val result : string = "done"
  val stats : Stats.t = <stats>

Now we can read the statistics back; Soteria.Stats exposes several helper getter functions to retrieve values of the correct type:

  # Stats.get_int stats "items_processed";;
  - : int = 3
  # Stats.get_int stats "bytes_read";;
  - : int = 3072

Tracking Time

Use add_time_of_to to measure how long an operation takes:

  # let slow_computation () =
      let rec fib n = if n <= 1 then n else fib (n-1) + fib (n-2) in
      fib 30
    in
    let res, stats =
      let@ () = Stats.As_ctx.with_ () in
      Stats.As_ctx.add_time_of_to "compute_time" slow_computation
    in
    res, Stats.get_float stats "compute_time";;
  - : int * float = (832040, 0.0228359699249267578)

Statistic Types

The stat_entry type supports five kinds of statistics:

  • Int: Integer values (merged by addition)
  • Float: Floating-point values (merged by addition)
  • StrSeq: Sequences of strings (merged by concatenation)
  • Map: Nested maps of statistics (merged recursively)
  • Yojson: Arbitrary JSON data (merged into arrays)

String Sequences

String sequences are useful for recording events or messages:

  # let log_events () =
      Stats.As_ctx.push_str "warnings" "Missing type annotation";
      Stats.As_ctx.push_str "warnings" "Unused variable x";
      Stats.As_ctx.push_str "warnings" "Deprecated function called";
      ()
    in
    let _, stats = Stats.As_ctx.with_ () log_events in
    Stats.get_strseq stats "warnings";;
  - : string Dynarray.t =
  ["Missing type annotation", "Unused variable x",
   "Deprecated function called"]

Nested Maps

Maps allow you to organize statistics hierarchically. Use push_binding to add entries to a map. A binding's value is any statistic type.

  # let track_by_function () =
      Stats.As_ctx.push_binding "function_calls" "main" (Int 5);
      Stats.As_ctx.push_binding "function_calls" "helper" (Int 12);
      Stats.As_ctx.push_binding "function_calls" "main" (Int 3);
      ()
    in
    let _, stats = Stats.As_ctx.with_ () track_by_function in
    Stats.get_map stats "function_calls";;
  - : Stats.stat_entry Soteria_std.Hashtbl.Hstring.t =
    main -> Stats.Int 8
    helper -> Stats.Int 12

Custom Printers

By default, statistics are printed in a generic format. You can register custom printers to make output more readable and context-aware.

The generic reigstration function is register_printer, but there are also type-specific helpers for common types.

For instance, use register_int_printer for integer statistics:

  # Stats.register_int_printer "operations"
      ~name:"Total Operations"
      (fun _stats ft count -> Fmt.pf ft "%d ops" count);

    let _, stats = Stats.As_ctx.with_ () (fun () ->
        Stats.As_ctx.add_int "operations" 42)
    in
    Fmt.pr "%a" Stats.pp stats;;
  Statistics:
  • Total Operations: 42 ops

  - : unit = ()

You can use disable_printer to hide certain statistics from output if you don't want them to be printed by default.

Printers receive the full statistics object, allowing context-aware formatting. Combined with hiding statistics, this allows you to create derived metrics that compute percentages, ratios, or other summaries based on multiple underlying statistics:

  # let () = Stats.register_int_printer "total_checks"
      ~name:"Checks"
      (fun stats ft total ->
          if total > 0 then
              let successes = Stats.get_int stats "successful_checks" in
              Fmt.pf ft "%d successes of %d (%a)" successes total
                  Soteria.Logs.Printers.pp_percenti (total, successes)
          else
              Fmt.pf ft "%d" total
      )
    in
    let () = Stats.disable_printer "successful_checks" in

    let demo_checks () =
      Stats.As_ctx.add_int "total_checks" 100;
      Stats.As_ctx.add_int "successful_checks" 85
    in

    let _, stats = Stats.As_ctx.with_ () demo_checks in
    Fmt.pr "%a" Stats.pp stats;;
  Statistics:
  • Checks: 85 successes of 100 (85%)

  - : unit = ()

Integration with Symbolic Execution

The statistics system is designed to work seamlessly with Soteria's symbolic execution engine. Furthermore, the Symex module internally uses statistics to track important metrics during symbolic execution, such as:

  • Execution time
  • SAT solving time
  • Number of SAT checks
  • Number of branches explored
  • Number of execution steps

See Symex.StatKeys for all available entries.

The Symex.S.run function receives an optional stats parameter that allows deciding how statistics should be tracked during symbolic execution:

Configuration

The Stats.Config module controls where statistics are output: either to stdout, to a JSON file, or disabled entirely. You can set the configuration at the start of your program before any statistics are collected with set_and_lock.

A Cmdliner term is provided, exposing a --output-stats flag to configure this from the command line.

You can then call output to write statistics according to the configuration.

Best Practices

Use consistent, hierarchical names for statistics, and define a StatKeys module to centralize your stat key constants, document them, and register their printers — this makes the code maintainable as the number of statistics grows:

  module StatKeys = struct
    let paths_explored = "analysis.paths_explored"
    let total_time = "analysis.time"
    let errors_found = "analysis.errors"

    let () =
      let open Soteria.Stats in
      register_int_printer paths_explored ~name:"Paths Explored" (fun _ ft n ->
          Fmt.pf ft "%d paths" n);
      register_float_printer total_time ~name:"Analysis Time" (fun _ ->
          Soteria.Logs.Printers.pp_time)
  end

  let my_process () =
    Soteria.Stats.As_ctx.incr StatKeys.paths_explored;
    Soteria.Stats.As_ctx.add_float StatKeys.total_time 1.5;
    ()

That's it!

You now know how to effectively use Soteria's statistics system! Key takeaways:

  • Wrap computations with Stats.As_ctx.with_ to enable tracking
  • Use incr, add_int, add_float for basic metrics
  • Use add_time_of_to for timing operations
  • Use push_str and push_binding for complex data
  • Statistics automatically merge across symbolic execution branches
  • Register custom printers for readable output
  • Consider performance: aggregate in hot loops, track at appropriate granularity
  • Use consistent naming conventions and organize related statistics

For more details, see the Stats API documentation.