Mica: Automated Differential Testing for OCaml Modules

1. Overview
2. Description of source files
3. Examples
4. Building & running
5. Example (finite sets)
6. Performance Benchmarks
7. Dependencies
8. Acknowledgements
9. Origin of name
10. References

Overview

Mica checks whether two OCaml modules implementing the same signature are observationally equivalent. Mica does this by parsing the signature & automatically generating property-based testing (PBT) code specialised to the signature.

Presented at the ICFP '23 Student Research Competition.

ICFP SRC documents:

• Extended Abstract
• Poster
• Talk

Other talks on Mica:

• Penn PLClub talk (~45 mins)
• OPLSS '23 talk (~10 mins)

Description of source files

Core components of Mica:

• Parser.ml: parser utility functions, modified from the Angstrom parser-combinator library
• ParserTypes.ml: Datatypes defining an AST for OCaml module signatures
• ModuleParser.ml: Parser for OCaml module signatures
• CodeGenerator.ml: Takes a parsed AST representing a module signature & generates specialized PBT code
• CmdLineParser.ml: Parses user input from the command line

Auxiliary utility files:

• Utils.ml: Utility functions for the code generator
• Stats.ml: Functions for examining the distribution of randomly generated symbolic expressions
• Latin.ml: QuickCheck generator for Latin words (taken from Lorem Ipsum placeholder text)

Benchmark suites:

• Mica_QC_Bench.ml: Benchmarks Mica's parser, code generator & the auto-generated PBT executables
• Mica_Bench.ml: Benchmarks Mica's parser & code generator only

Examples

The lib directory also contains five example module signatures, each of which has two different implementations. Mica has been tested extensively with these five pairs of modules.

The code for these example modules has been adapted from various sources, listed in the references section of this README.

1. Finite Sets (Lists & BSTs)

• Signature: SetInterface.ml
• List implementation: ListSet.ml
• BST implementation: BSTSet.ml
• Running the auto-generated code: dune exec -- sets
  • Example auto-generated code: GeneratedSetPBTCode.ml & GeneratedSetExecutable.ml

2. Regex matchers (Brzozowski derivatives & DFAs)

• Signature: RegexMatcher.mli (Commented version: RegexMatcher.ml)
• Brzozowski derivatives: Brzozowski.ml
• DFAs: DFA.ml
• Running the auto-generated code: dune exec -- regexes
  • Example auto-generated code: GeneratedRegexPBTCode.ml & GeneratedRegexExecutable.ml

3. Polynomials (Horner schema & list folds)

• Signature: PolyInterface.ml
• Polynomial evaluation using list folds: Poly1.ml
• Polynomial evaluation using Horner's algorithm: Poly2.ml
• Running the auto-generated code: dune exec -- polynomials
  • Example auto-generated code: GeneratedPolyPBTCode.ml & GeneratedPolyExecutable.ml

4. Functional Maps (Association lists & Red-black trees)

• Signature: MapInterface.ml (Commented version: MapInterface.mli)
• Association lists: AssocListMap.ml
  • See AssocList.ml for the definition of the AssocList type & its QuickCheck generator
• Red-Black tree maps: RedBlackMap.ml
• Running the auto-generated code: dune exec -- maps
  • Example auto-generated code: GeneratedMapPBTCode.ml & GeneratedMapExecutable.ml

5. Stacks (List & algebraic data type representations)

• Signature: StackInterface.ml
• List implementation: ListStack.ml
• Implementation using custom ADT: VariantStack.ml
• Running the auto-generated code: dune exec -- stacks
  • Example auto-generated code: GeneratedStackPBTCode.ml & GeneratedStackExecutable.ml

Building & running

Run make (or dune build) to build and compile the library.
Run make install to install dependencies.

Usage:

dune exec -- mica [.ml file containing signature] [.ml file containing 1st module] [.ml file containing 2nd module]

This command runs Mica and creates two new files:

1. lib/Generated.ml (contains PBT code for testing an OCaml module)
2. bin/compare_impls.ml (code for an executable that tests two modules for observational equivalence)

To run the generated executable, run dune exec -- compare_impls.

Example (finite sets)

  dune exec -- mica lib/sets/SetInterface.ml lib/sets/ListSet.ml lib/sets/BSTSet.ml

This runs Mica on the Set example above, checking if the ListSet and BSTSet modules both correctly implement the interface SetInterface.
The files GeneratedSetPBTCode.ml and GeneratedSetExecutable.ml contain PBT code that is automatically generated by Mica.

Performance Benchmarks

• Run dune exec -- mica_qc_bench to benchmark both Mica's code-generation executable & the auto-generated PBT executables on all example modules
• Run dune exec -- mica_bench to benchmark only the main Mica executable
  • When this option is selected, the auto-generated PBT executables will not be benchmarked

The following table contains performance benchmarks for Mica on the five example module signatures.
Benchmarks were conducted on an 2023 M2 Macbook Pro using Jane Street's Core_bench library, which estimates Mica's runtime over a large no. of runs (~1000) using linear regression (link).

Example Module Signature	Runtime of Mica Parser & Code Generator	Runtime of Auto-Generated PBT executable
Sets	309.25 μs	2.55 ns
Stacks	361.08 μs	2.54 ns
Polynomials	302.82 μs	2.57 ns
Maps	262.84 μs	2.56 ns
Regexes	266.61 μs	2.57 ns

Dependencies

Please see mica.opam for a full list of dependencies. Mica has been tested primarily with versions 4.13.1 & 5.0.0 of the OCaml base compiler (on an M1 Mac).

• Base & Base_quickcheck
• Core & Core.Quickcheck
• Angstrom
• PPrint
• Stdio
• Re
• Odoc (for generating documentation)
• Core_bench (for running benchmarks)
• OCaml-CI (for CI)

Acknowledgements

I'm incredibly fortunate to have two fantastic advisors: Harry Goldstein & Prof. Benjamin Pierce. Harry & Benjamin have provided lots of useful feedback on the design of Mica, and I'm extremely grateful for their mentorship.

I'd also like to thank:

• Penn's PLClub for their feedback on my presentation slides
• Jan Midtggard (Tarides) & Carl Eastlund (Jane Street) for answering my questions about QCSTM and Core.Quickcheck
• Cassia Torczon for the idea behind the name Mica

Origin of name

Mica stands for "Module-Implementation Comparison Automation". Mica is also a type mineral commonly found in rocks -- this name was inspired by several relevant OCaml libraries that are also named after stones/rocks:

• Monolith (Randomised testing tool for OCaml modules)
• Opal (parser combinator library)
• Menhir (parser library)
• Obelisk (pretty-printer for Menhir)

References

• Jane Street's Base_quickcheck & Core.Quickcheck
• QuviQ QuickCheck
• QCSTM
• Model_quickcheck
• Monolith
• Articheck
• Advanced Topics in Types & Programming Languages, Chapter 8
• Real World OCaml

The code for the example modules has been adapted from the following sources:

Finite Sets:

• Cornell CS 3110 OCaml textbook
• Penn CIS 1200 lecture notes
• Yale-NUS YSC2229 website

Regex matchers:

• Harry Goldstein's livestream on regex derivatives & DFAs

Polynomials:

• Jean-Christophe Filliatre's implementation
• Shayne Fletcher's implementation

Functional maps:

• Colin Shaw's RB tree implementation
• Benedikt Meurer RB tree implementation
• Cornell CS 3110 textbook, chapter 8
• The implementation of red-black tree deletion follows the approach taken by Germane & Might (2014).

Stacks:

• Cornell CS 3110 textbook, chapter 5