The A-normal form (ANF) grammar

Utilities and helper functions for operating on Sail ASTs

Functions for generating and interacting with Sail call graphs.

Module for breaking AST into syntactic chunks and interleaving comments.

const_prop target ast ref_vars substs assigns exp performs constant propagation on exp where substs is a pair of substitutions on immutable variables and type variables, assigns is a substitution on mutable variables, and ref_vars is the set of variable which may have had a reference taken (and hence we cannot reliably track).

This module implements the interface with the Z3 (or other) SMT solver

In Sail, we need to distinguish between pure and impure (side-effecting) functions. This is because there are few places, such as top-level let-bindings and loop termination measures where side effects must clearly be forbidden. This module implements inference for which functions are pure and which are effectful, and checking the above purity restrictions.

Generic graph type based on OCaml Set and Map

Initial desugaring pass over AST after parsing

Compile Sail ASTs to Jib intermediate representation

Utilities and helper functions for operating on Jib instructions and definitions

Definition of Sail project files, and functions for working with them.

This file implements utilities for dealing with $property and $counterexample pragmas.

Sail error reporting

General rewriting framework for Sail to Sail rewrites

Compile Sail builtins to SMT bitvector expressions

Rewrites for removing polymorphism from specifications

Infrastructure for plugins to register Sail targets.

The type checker API

Type error utilities

Various non Sail specific utility functions