package libsail

  1. Overview
  2. Docs
module Anf : sig ... end

The A-normal form (ANF) grammar

module Ast : sig ... end
module Ast_defs : sig ... end
module Ast_util : sig ... end

Utilities and helper functions for operating on Sail ASTs

module Bitfield : sig ... end
module Callgraph : sig ... end

Functions for generating and interacting with Sail call graphs.

module Chunk_ast : sig ... end

Module for breaking AST into syntactic chunks and interleaving comments.

module Constant_fold : sig ... end
module Constant_propagation : sig ... end

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).

module Constant_propagation_mutrec : sig ... end
module Constraint : sig ... end

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

module Effects : sig ... end

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.

module Elf_loader : sig ... end
module Error_format : sig ... end
module Format_sail : sig ... end
module Frontend : sig ... end
module Graph : sig ... end

Generic graph type based on OCaml Set and Map

module Initial_check : sig ... end

Initial desugaring pass over AST after parsing

module Interactive : sig ... end
module Interpreter : sig ... end
module Jib : sig ... end
module Jib_compile : sig ... end

Compile Sail ASTs to Jib intermediate representation

module Jib_optimize : sig ... end
module Jib_util : sig ... end

Utilities and helper functions for operating on Jib instructions and definitions

module Lexer : sig ... end
module Libsail_sites : sig ... end
module Mappings : sig ... end
module Monad_params : sig ... end
module Monomorphise : sig ... end
module Nl_flow : sig ... end
module Outcome_rewrites : sig ... end
module Parse_ast : sig ... end
module Parser : sig ... end
module Parser_combinators : sig ... end
module Pattern_completeness : sig ... end
module Preprocess : sig ... end
module Pretty_print_common : sig ... end
module Pretty_print_sail : sig ... end
module Profile : sig ... end
module Property : sig ... end

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

module Reporting : sig ... end

Sail error reporting

module Rewriter : sig ... end

General rewriting framework for Sail to Sail rewrites

module Rewrites : sig ... end
module Sail2_instr_kinds : sig ... end
module Sail2_operators : sig ... end
module Sail2_operators_bitlists : sig ... end
module Sail2_prompt : sig ... end
module Sail2_prompt_monad : sig ... end
module Sail2_values : sig ... end
module Sail_lib : sig ... end
module Scattered : sig ... end
module Spec_analysis : sig ... end
module Specialize : sig ... end

Rewrites for removing polymorphism from specifications

module Splice : sig ... end
module State : sig ... end
module Target : sig ... end

Infrastructure for plugins to register Sail targets.

module Type_check : sig ... end

The type checker API

module Type_error : sig ... end

Type error utilities

module Util : sig ... end

Various non Sail specific utility functions

module Value : sig ... end
module Value2 : sig ... end
OCaml

Innovation. Community. Security.