libsail 0.15 · OCaml Package

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 Constant_fold : sig ... end

module Constant_propagation : sig ... end

const_prop defs 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 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

module Lexer : sig ... end

module Libsail_sites : sig ... end

module Monomorphise : sig ... end

module Nl_flow : sig ... end

module Optimize : 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 registering Sail targets/backends

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

package libsail