package libsail

  1. Overview
  2. Docs

Compile Sail ASTs to Jib intermediate representation

val optimize_aarch64_fast_struct : bool Stdlib.ref

This forces all integer struct fields to be represented as int64_t. Specifically intended for the various TLB structs in the ARM v8.5 spec. It is unsound in general.

val opt_memo_cache : bool Stdlib.ref

(WIP) opt_memo_cache will store the compiled function definitions in file _sbuild/ccacheDIGEST where DIGEST is the md5sum of the original function to be compiled. Enabled using the -memo flag. Uses Marshal so it's quite picky about the exact version of the Sail version. This cache can obviously become stale if the Sail changes - it'll load an old version compiled without said changes.

Jib context

type ctx = {
  1. records : (Ast.kid list * Jib.ctyp Ast_util.Bindings.t) Ast_util.Bindings.t;
  2. enums : Ast_util.IdSet.t Ast_util.Bindings.t;
  3. variants : (Ast.kid list * Jib.ctyp Ast_util.Bindings.t) Ast_util.Bindings.t;
  4. valspecs : (string option * Jib.ctyp list * Jib.ctyp) Ast_util.Bindings.t;
  5. quants : Jib.ctyp Ast_util.KBindings.t;
  6. local_env : Type_check.Env.t;
  7. tc_env : Type_check.Env.t;
  8. effect_info : Effects.side_effect_info;
  9. locals : (Ast_util.mut * Jib.ctyp) Ast_util.Bindings.t;
  10. letbinds : int list;
  11. letbind_ids : Ast_util.IdSet.t;
  12. no_raw : bool;
}

Dynamic context for compiling Sail to Jib. We need to pass a (global) typechecking environment given by checking the full AST.

val ctx_is_extern : Ast.id -> ctx -> bool
val ctx_get_extern : Ast.id -> ctx -> string
val ctx_has_val_spec : Ast.id -> ctx -> bool

Compilation functions

module type CONFIG = sig ... end

The Config module specifies static configuration for compiling Sail into Jib. We have to provide a conversion function from Sail types into Jib types, as well as a function that optimizes ANF expressions (which can just be the identity function)

module IdGraph : sig ... end
val callgraph : Jib.cdef list -> IdGraph.graph
module Make (C : CONFIG) : sig ... end

Adds some special functions to the environment that are used to convert several Sail language features, these are sail_assert, sail_exit, and sail_cons.

val name_or_global : ctx -> Ast.id -> Jib.name
OCaml

Innovation. Community. Security.