Mica: Automated Differential Testing for OCaml Modules

Note: Mica is a research tool and should not be used in production code. Please contact Ernest Ng ([email protected]) if you'd like to contribute to Mica or have any questions!

README Contents:

• Overview
• Installation
• Using Mica
  • Limitations
• Compilation notes
• Case studies
• An overview of the codebase
• Differences between the OCaml Workshop '24 & ICFP '23 SRC artifacts
• Notes for implementors
  • Testing changes locally
  • Dependencies

Overview

Mica is a PPX extension that automates differential testing for a pair of OCaml modules implementing the same signature. Users annotate module signatures with the directive [@@deriving mica], and at compile-time, Mica derives specialized property-based testing (PBT) code that checks if two modules implementing the signature are observationally equivalent. (Under the hood, Mica uses Jane Street's Core.Quickcheck PBT library.)

Mica docs can be found here. A simple webapp demonstrating Mica is available here.

Installation

Mica is available on opam. To install, run:

opam update
opam install ppx_mica

Note that OCaml 5.1 or newer is required. We recommend using OCaml 5.1.0 or 5.2.0 -- some build issues have been observed with OCaml 5.2.1.

To use Mica, add ppx_mica, ppx_deriving.show and ppx_jane to the preprocess field in your dune file: (Mica produces code that uses ppx_deriving and ppx_jane under the hood, so these two PPXes are also required in order for the code produced by Mica to compile.)

(library 
 ...
 (preprocess (pps ppx_mica ppx_deriving.show ppx_jane)))

Using Mica

Mica was presented at the OCaml Workshop 2024 and the ICFP 2023 Student Research Competition. The OCaml Workshop paper contains a lot more details about Mica's design -- this README focuses on describing how to interact with our OCaml artifact.

Here is how we envisage users interacting with Mica:
Suppose modules M1 & M2 both implement the module signature S. Users insert the directive [@@deriving_inline mica] beneath the definition of S, like so:

module type S = sig
  type 'a t 
  val empty : 'a t
  val add : 'a -> 'a t -> 'a t
  ...
end
[@@deriving_inline mica] 
...
[@@@end]

Then, after users run dune build --auto-promote, the derived PBT code is automatically inserted in-line in the source file in-between [@@deriving_inline mica] and [@@@end]. (Note: this doesn't work fully out of the box at the moment -- see compilation notes for details.)

Specifically, Mica derives the following PBT code:

module Mica = struct 
  (** [expr] is an inductively-defined algebraic data type 
      representing {i symbolic expressions}. 
      
      Each [val] declaration in the module signature [S] corresponds to a 
      cosntructor for [expr] that shares the same name, arity & argument types. 
      - Type variables ['a] are instantiated with [int]
      - Function arguments of type ['a t] correpond to
        constructor arguments of type [expr] *)
  type expr =
    | Empty
    | Is_empty of expr
    ...
  [@@deriving show, ...]

  (** Types of symbolic expressions *)
  type ty = Int | IntT | ... [@@deriving show, ...]

  (** QuickCheck generator for symbolic expressions. 
      [gen_expr ty] generates random [expr]s of type [ty]. *)
  let rec gen_expr : ty -> Core.Quickcheck.Generator.t = ...

  (** Functor that interprets symbolic expressions *)
  module Interpret (M : S) = struct   
    (** Values of symbolic expressions *)
    type value = ValInt of int | ValIntT of int M.t | ...

    (** Big-step interpreter for symbolic expressions: 
        [interp] takes an [expr] and interprets it over the module 
        [M], evaluating the [expr] to a [value] *)
    let rec interp : expr -> value = ...
  end 

  (** Functor that tests [M1] and [M2] for observational equivalence *)
  module TestHarness (M1 : S) (M2 : S) = struct 
    (* Runs all observational equivalence tests *)
    let run_tests : unit -> unit = ... 
  end
end

• Now suppose modules M1 and M2 both implement S. To run Mica's testing code and check whether M1 & M2 are observationally equivalent with respect to S, one can invoke the run_tests : unit -> unit function in Mica's TestHarness functor, like so:

module T = Mica.TestHarness(M1)(M2)
let () = T.run_tests ()

• Note: Mica only tests for observational equivalence at concrete types (e.g. int, string option), and not abstract types defined in a module (e.g. 'a M.t), since abstract types have a more abstract notion of equality different from OCaml's standard notion of polymorphic equality.

Limitations

At the moment, Mica only works with module signatures that define one abstract type (e.g. t or 'a t) and only contain pure functions. Modules with multiple abstract types and/or abstract types with multiple type parameters are not supported at the moment.

Compilation notes

There is a known issue with Ppxlib (#338, #342) which causes Ppxlib to error when Dune is promoting changes (i.e. after one runs dune build --auto-promote, during which Dune inserts the code derived by Mica into the source file).

To fix this issue, remove [@@deriving_inline mica] and [@@@end] from the source file while keeping the code inserted by Dune/Mica. Then, recompile by running dune build again. This second compilation run should complete successfully!

Case Studies

Code for the following case studies (along with the code automatically derived by Mica) is located in the ancillary mica_case_studies repo.

We have tested Mica with the following module signatures, each of which is implemented by two different modules:

• Finite Sets (lists & BSTs) (link)
• Regular Expression Matchers (Brzozowski Derivatives & DFAs) (link)
• Polynomials (Horner schema & monomial-based representations) (link)
• Ephemeral Queues (Base.Queue & Base.Linked_queue) (link)
• Unsigned integer arithmetic (the stdint and ocaml-integers libraries) (link)
• Character sets (the charset library & the standard library's Set.Make(Char) module) (link)
• Persistent maps (red-black trees & association lists) (link)
• John Hughes's How to Specify It (catching bugs in BST implementations) (link)
• UPenn CIS 1200 student homework submissions (link)
  • Note: no student code is available for this case study (to avoid posting homework solutions online)

For more details regarding these case studies, we refer the reader to the mica_case_studies repo as well as the OCaml Workshop paper.

An overview of the codebase

The lib subdirectory contains the code for the Mica PPX deriver.
The PPX code is organized as follows:

• ppx_mica.ml: Declares the main Mica PPX deriver
• type_deriver.ml: Derives the definitions of auxiliary data types & the gen_expr Quickcheck generator
• interp_deriver.ml: Derives the Interpret functor
• test_harness_deriver.ml: Derives the TestHarness functor
• overall_deriver.ml: Produces a module called Mica containing all the automatically derived code
• utils.ml: Includes all the following helper modules for convenience:
  • builders.ml: Functions for creating AST nodes
  • getters.ml: Functions for inspecting AST nodes
  • equality.ml: Location-agnostic equality functions for Parsetree types
  • lident.ml: Utilities for working with the Longident type
  • names.ml: Functions for generating fresh variable names & quoting expressions
  • printers.ml: Pretty-printers for AST types + functions for monomorphizing types
  • errors.ml: Functions for error handling (embedding errors as extension nodes in the derived code)
  • inv_ctx.ml: The "inverse typing context", mapping types ty to expressions of type ty
  • let_open.ml: Helpers for producing let open expressions
  • include.ml: Helpers for producing include statements
  • miscellany.ml: Miscellaneous helpers for working with lists & strings

The ancillary mica_tyche_utils repo contains a small library for creating JSON files that are ingested by Tyche, a VS Code extension for visualizing property-based testing effectiveness.

• Note: the Tyche-Mica integration is still work in progress (contact Ernest Ng for more details).
• For more details about Tyche, we refer the reader to the UIST '24 paper by Goldstein et al.

Differences between the OCaml Workshop & ICFP SRC artifacts

• The OCaml Workshop artifact (2024) includes a version of Mica that has been
  re-implemented from scratch as a PPX deriver (using Ppxlib). This artifact derives code at compile-time and is more feature rich (e.g. is compatible with Tyche).

  • The main branch of this repo currently contains the OCaml Workshop artifact.

• The ICFP SRC artifact (2023) contained a Mica prototype that was implemented as a command-line script. This prototype contained a parser for ML module signatures (written using Angstrom) and pretty-printed the derived PBT code to a new .ml file (using PPrint). This artifact derived code at runtime and is less robust compared to the newer OCaml Workshop artifact.

  • Contact Ernest ([email protected]) for access to the (now-deprecated) ICFP '23 SRC artifact.

Notes for Implementors

Testing changes locally

1. test/utils_test contains Alcotest unit tests for various helper functions.

• See the README in utils_test for instructions on how to add new tests to the Alcotest test suite.

2. test/ppx_test contains .ml test files used to test the PPX functionality

• To add a new test file to the corpus of test files, in either ppx_test/passing or ppx_test/errors, run:

$ touch test_file.{ml,expected}; dune runtest --auto-promote

(This automatically generates new Dune stanzas that are needed for the new test files to compile.)

• Then fill in the newly-created .ml and .expected files with the module signature under test (plus relevant PPX annotations), and execute dune runtest. If the test output from Dune looks good, run dune promote to update the .expected file with the contents of the .actual file (which contains what the PPX actually generated from that test run).

Dependencies

• This repo has been tested with OCaml 5.1.0 on an M1 Mac.
• To install all dependencies required for local development, run make install
• We recommend having the following libraries installed:
  • ppxlib
  • ppx_jane
  • ppx_deriving.show
  • base
  • base_quickcheck
  • core
  • core_unix
  • alcotest
• You can also run dune utop to see the output of functions in the codebase in a REPL.