Module `Libsail`Source

Sourcemodule Anf : sig ... end

The A-normal form (ANF) grammar

Sourcemodule Ast : sig ... end

Sourcemodule Ast_compare : sig ... end

Sourcemodule Ast_defs : sig ... end

Sourcemodule Ast_util : sig ... end

Utilities and helper functions for operating on Sail ASTs

Sourcemodule Bitfield : sig ... end

Sourcemodule Callgraph : sig ... end

Functions for generating and interacting with Sail call graphs.

Sourcemodule Chunk_ast : sig ... end

Module for breaking AST into syntactic chunks and interleaving comments.

Sourcemodule Config : sig ... end

Sail model configuration using JSON.

Sourcemodule Config_json : sig ... end

Interpreting JSON values from configuration files as Sail expressions.

Sourcemodule Constant_fold : sig ... end

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

Sourcemodule Constant_propagation_mutrec : sig ... end

Sourcemodule Constraint : sig ... end

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

Sourcemodule Corelib_project : sig ... end

Sourcemodule Corelib_sail : sig ... end

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

Sourcemodule Elf_loader : sig ... end

Sourcemodule Error_format : sig ... end

module Extraction : sig ... end

Sourcemodule Flag : sig ... end

Sourcemodule Format_sail : sig ... end

Sourcemodule Frontend : sig ... end

Sourcemodule Graph : sig ... end

Generic graph type based on OCaml Set and Map

Sourcemodule Infix_parser : sig ... end

Sourcemodule Infix_parser_token : sig ... end

Sourcemodule Initial_check : sig ... end

Initial desugaring pass over AST after parsing

Sourcemodule Interactive : sig ... end

Sourcemodule Interpreter : sig ... end

Sourcemodule Jib : sig ... end

Sourcemodule Jib_compile : sig ... end

Compile Sail ASTs to Jib intermediate representation

Sourcemodule Jib_optimize : sig ... end

Sourcemodule Jib_ssa : sig ... end

Sourcemodule Jib_util : sig ... end

Utilities and helper functions for operating on Jib instructions and definitions

Sourcemodule Jib_visitor : sig ... end

Sourcemodule Lexer : sig ... end

Sourcemodule Libsail_sites : sig ... end

Sourcemodule Lint : sig ... end

Sourcemodule Mappings : sig ... end

Sourcemodule Monad_params : sig ... end

Sourcemodule Monomorphise : sig ... end

Sourcemodule Name_generator : sig ... end

Sourcemodule Nl_flow : sig ... end

Sourcemodule Outcome_rewrites : sig ... end

Sourcemodule Parmap : sig ... end

This module provides a parallel map function that uses OCaml 5 Effect handlers to provide a limited form of parallelism.

Sourcemodule Parse_ast : sig ... end

Sourcemodule Parse_ast_diff : sig ... end

Sourcemodule Parser : sig ... end

Sourcemodule Parser_combinators : sig ... end

Sourcemodule Partial_eval : sig ... end

This module provides an interface to the Rocq Extraction.ZAst module for partial evaluation of Sail expressions.

Sourcemodule Pattern_completeness : sig ... end

Sourcemodule Pragma : sig ... end

Sourcemodule Preprocess : sig ... end

Sourcemodule Pretty_print_common : sig ... end

Sourcemodule Pretty_print_sail : sig ... end

Sourcemodule Profile : sig ... end

Sourcemodule Project : sig ... end

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

Sourcemodule Project_lexer : sig ... end

Sourcemodule Project_parser : sig ... end

Sourcemodule Project_token : sig ... end

Sourcemodule Property : sig ... end

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

Sourcemodule Reporting : sig ... end

Sail error reporting and warnings

Sourcemodule Rewriter : sig ... end

General rewriting framework for Sail to Sail rewrites

Sourcemodule Rewrites : sig ... end

Sourcemodule Sail2_instr_kinds : sig ... end

Sourcemodule Sail2_operators : sig ... end

Sourcemodule Sail2_operators_bitlists : sig ... end

Sourcemodule Sail2_prompt : sig ... end

Sourcemodule Sail2_prompt_monad : sig ... end

Sourcemodule Sail2_values : sig ... end

Sourcemodule Sail_file : sig ... end

This module contains all the logic for working with source files.

Sourcemodule Sail_lib : sig ... end

Sourcemodule Scattered : sig ... end

Sourcemodule Smt_exp : sig ... end

Sourcemodule Smt_gen : sig ... end

Compile Sail builtins to SMT bitvector expressions

Sourcemodule Spec_analysis : sig ... end

Sourcemodule Specialize : sig ... end

Rewrites for removing polymorphism from specifications

Sourcemodule Splice : sig ... end

Sourcemodule State : sig ... end

Sourcemodule Target : sig ... end

Infrastructure for plugins to register Sail targets.

Sourcemodule Token : sig ... end

Sourcemodule Type_check : sig ... end

The type checker API

Sourcemodule Type_env : sig ... end

Sourcemodule Type_error : sig ... end

Type error utilities

Sourcemodule Type_internal : sig ... end

Sourcemodule Util : sig ... end

Various non Sail specific utility functions

Sourcemodule Value : sig ... end

Sourcemodule Value2 : sig ... end

Sourcemodule Version : sig ... end

Sourcemodule Visitor : sig ... end

Install

dune-project
Dependency

Authors

Maintainers

Sources

doc/libsail/Libsail/index.html

Module `Libsail`Source

package libsail

Install

dune-project Dependency

Authors

Maintainers

Sources

doc/libsail/Libsail/index.html

Module LibsailSource

dune-project
Dependency

Module `Libsail`Source