Soteria Logging Tutorial

Welcome to the Soteria logging tutorial! This tutorial will guide you through using the Logs module for debugging and analyzing your symbolic execution programs.

Soteria's logging interface is inspired by the logs library, but its implementation is adapted to integrate with symbolic execution and produce structured HTML output.

Today you'll be learning how to:

• Log messages at different levels
• Configure logging for your needs
• Output to HTML with collapsible sections
• Format output with colors and styles
• Write efficient logging that won't slow your programs down
• Use the PPX extension for convenient logging

Basic Logging

The Soteria logging system provides a simple, flexible way to output diagnostic information. To get started, you need to open the Logs.Import module, which brings the L logging module into scope:

  open Soteria.Logs.Import

To ensure this import is always available in your project, you can instead also add it to your dune file:

  (flags :standard -open Soteria.Logs.Import)

The L module provides logging functions for different severity levels. The most common one is info, which logs informational messages:

  L.info (fun m -> m "Starting symbolic execution")
  (* -> Starting symbolic execution *)

The logging API uses a callback pattern: you pass a function that receives a formatter function m, which you then call with a format string and arguments. This design allows the logging system to avoid formatting work when a log level is disabled.

Let's log a message with a value:

  let x = 42 in
  L.info (fun m -> m "The answer is %d" x)
  (* -> The answer is 42 *)

Log Levels

Soteria provides six log levels, from most verbose to least verbose:

• Smt: For messages about SMT solver interactions (queries, results)
• Trace: For very detailed execution traces
• Debug: For debugging information
• Info: For general informational messages
• Warn: For warnings about potential issues
• Error: For errors and exceptions

Each level has a corresponding logging function in the L module:

  L.trace (fun m -> m "Detailed trace: entering function");
  (* -> [TRACE] Detailed trace: entering function *)
  L.debug (fun m -> m "Variable x = %d" 10);
  (* -> [DEBUG] Variable x = 10 *)
  L.info (fun m -> m "Processing completed successfully");
  (* -> [INFO ] Processing completed successfully *)
  L.warn (fun m -> m "This operation may be slow");
  (* -> [WARN ] This operation may be slow *)
  L.error (fun m -> m "Failed to parse input")
  (* -> [ERROR] Failed to parse input *)

The smt level is special: it's designed for logging SMT solver interactions, which can be extremely verbose but crucial for understanding solver behavior. Unless you're implementing a solver backend, you usually shouldn't need this level:

  L.smt (fun m -> m "Querying solver: (assert (> x 0))")
  (* -> [SMT ] Querying solver: (assert (> x 0)) *)

Configuration

Logging behavior is controlled by Logs.Config. You can configure:

• The maximum verbosity level to display
• The output format (text to stderr or HTML)
• Whether to always log SMT queries regardless of level
• Whether to use colors in text output
• Whether to hide unstable values like timestamps (useful for diffing)

Here's how to configure logging programmatically:

  (* Create a configuration that logs at Debug level and above *)
  let log_config =
    Soteria.Logs.Config.make ~level:(Some Debug) ~kind:Stderr ~no_color:false ()
  ;;

  Soteria.Logs.Config.set_and_lock log_config

Important: configuration is global and can only be set once. After calling set_and_lock, trying to set it again will raise an exception.

For command-line applications, Soteria provides Cmdliner integration via Logs.Config.cmdliner_term.

HTML Output

Soteria natively supports outputting logs in HTML format. This allows you to view logs in a browser, with a search/filter bar, and collapsible sections.

You can organize output into collapsible sections using with_section:

  L.with_section "Analyzing Module" (fun () ->
      L.info (fun m -> m "Starting analysis");

      L.with_section "Function: main" (fun () ->
          L.debug (fun m -> m "Analyzing function body");
          L.trace (fun m -> m "Thinking about it...");
          L.debug (fun m -> m "Found 3 branches"));

      L.with_section "Function: helper" (fun () ->
          L.debug (fun m -> m "Analyzing function body");
          L.warn (fun m -> m "Something bad is brewing...");
          L.error (fun m -> m "Oh no!"));

      L.info (fun m -> m "Analysis complete"))

In HTML mode, each call to with_section renders as a collapsible block that can be expanded or collapsed in the browser. For instance, the above code would generate the following HTML (you can click around!):

Important: Do not use with_section inside symbolic processes (functions that return 'a Symex.t) that may branch, because the section will be opened once but closed multiple times. Soteria will automatically create sections when branching occurs inside a process.

Note: with_section has a ?is_branch parameter, that is meant only for use when writing your own Symex implementation; most users should never use this parameter.

Pretty Printing and Formatting

The Logs.Printers module provides utilities for formatting output with colors, styles, and special formatting:

Colors and Styles

Note: colored text only works in stderr mode (~kind:Stderr); colors are not applied in HTML mode.

You can print colored text using pp_clr, apply text styles with pp_style, or combine both with pp_clr2:

  let open Soteria.Logs.Printers in
  L.info (fun m ->
      m "%a, %a, %a" (pp_clr `Green) "Success" (pp_style `Bold) "Important"
        (pp_clr2 `Red `Bold) "Critical")

Semantic Colors

For common message types, use semantic color functions (pp_ok, pp_warn, pp_err, pp_fatal):

  let open Soteria.Logs.Printers in
  L.info (fun m ->
      m "%a, %a, %a, %a" pp_ok "OK" pp_warn "Warning" pp_err "Error" pp_fatal
        "Fatal")

Special Formatters

The following formatters are available for common value types:

• pp_time: formats float seconds as 12ms or 1.54s
• pp_percent: formats a (total, part) float pair as a percentage, and pp_percenti does the same with integers
• pp_plural: handles singular/plural forms based on count
• pp_unstable: hides values that change between runs (when hide_unstable is set in config)

  let open Soteria.Logs.Printers in
  L.info (fun m ->
      m "Time: %a, Coverage: %a, Found: %a" pp_time 1.543 pp_percent (10.0, 2.5)
        (pp_plural ~sing:"branch" ~plur:"branches")
        5)
  (* -> Time: 1.54s, Coverage: 25.00%, Found: 5 branches *)

Unstable Values

When writing tests or generating reproducible output, you can hide values that change between runs (like timestamps or durations) using pp_unstable. Note that pp_time is already predefined as an unstable printer.

  let open Soteria.Logs.Printers in
  let current_time = Unix.gettimeofday () in

  L.info (fun m ->
      m "Completed at %a" (pp_unstable ~name:"timestamp" Fmt.float) current_time)
  (* hide_unstable = false -> Completed at 1775127711.926 hide_unstable = true
     -> Completed at <timestamp> *)

The --hide-unstable flag also makes sure that the printing profile (e.g. support for colors or utf8) is the same independently of the environment, which is useful for making test output deterministic.

Performance Considerations

Logging is designed to be efficient when disabled; avoid doing expensive work for printing before calling the logging function. Instead, do that work inside the logging lambda, so it only runs if the log level is enabled:

  (* BAD: Always computes the string, even if logging is disabled *)
  let expensive_string = String.concat ", " (List.init 1000 string_of_int) in
  L.trace (fun m -> m "Generated: %s" expensive_string)
  ;;

  (* GOOD: Only computes if needed *)
  L.trace (fun m ->
      let expensive_string =
        String.concat ", " (List.init 1000 string_of_int)
      in
      m "Generated: %s" expensive_string)

PPX Extension

Writing calls to the logging function can be a bit verbose, with the need to wrap everything in a lambda. Soteria provides a PPX extension that allows you to write more concise logging statements using [%l.info], [%l.debug], etc. To use it, first add the PPX dependency to your dune file:

  (preprocess (pps ppx_symex))

This is purely syntactic sugar to save some typing and improve readability. It does not supporting declarations within the logging statement, so if you need to do any let-bindings or computations, you should still use the full lambda form.

  [%l.info "Starting symbolic execution"];;
  [%l.debug "Variable x = %d" 67];;

  (* Expands to: *)
  L.info (fun m -> m "Starting symbolic execution");;
  L.debug (fun m -> m "Variable x = %d" 67)

That's it!

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

• Use the L module from Logs.Import for all logging
• Choose appropriate log levels for different types of information
• Configure logging behavior with Logs.Config
• Organize verbose output with sections in HTML mode
• Use pretty printing utilities for formatted, colorful output
• Keep performance in mind by doing expensive work inside the logging lambda

For more details, see the Logs API documentation.