package libsail

  1. Overview
  2. Docs
package libsail
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Libsail.Jib_compileSource

Compile Sail ASTs to Jib intermediate representation

Sourceval optimize_aarch64_fast_struct : bool 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.

Sourceval opt_memo_cache : bool 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

Sourcetype ctx = {
  1. target_name : string;
  2. records : (Ast.kid list * Jib.ctyp Ast_util.Bindings.t) Ast_util.Bindings.t;
  3. enums : Ast_util.IdSet.t Ast_util.Bindings.t;
  4. variants : (Ast.kid list * Jib.ctyp Ast_util.Bindings.t) Ast_util.Bindings.t;
  5. abstracts : Jib.ctyp Ast_util.Bindings.t;
  6. valspecs : (string option * Jib.ctyp list * Jib.ctyp * Ast_util.uannot) Ast_util.Bindings.t;
  7. quants : Jib.ctyp Ast_util.KBindings.t;
  8. local_env : Type_check.Env.t;
  9. tc_env : Type_check.Env.t;
  10. effect_info : Effects.side_effect_info;
  11. locals : (Ast_util.mut * Jib.ctyp) Jib_util.NameMap.t;
  12. registers : Jib.ctyp Ast_util.Bindings.t;
  13. letbinds : int list;
  14. letbind_ids : Jib_util.NameSet.t;
  15. no_raw : bool;
  16. no_static : bool;
  17. coverage_override : bool;
  18. def_annot : unit Ast.def_annot option;
}

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

Sourceval ctx_is_extern : Ast.id -> ctx -> bool
Sourceval ctx_get_extern : Ast.id -> ctx -> string
Sourceval ctx_has_val_spec : Ast.id -> ctx -> bool
Sourceval initial_ctx : ?for_target:string -> Type_check.Env.t -> Effects.side_effect_info -> ctx

Create an inital Jib compilation context.

The target is the name that would appear in a valspec extern section, i.e.

val foo = { systemverilog: "bar", c: "baz" } = ...

would mean "systemverilog" and "c" would be valid for_target parameters. If unspecified it will get the current target name from the Target module. If unspecified and there is no current target, it defaults to "c".

Sourcetype funwire =
  1. | Arg of int
  2. | Ret
  3. | Invoke
Sourceval transparent_newtype : ctx -> Jib.ctyp -> Jib.ctyp
Sourceval struct_field_bindings : Ast.l -> ctx -> Jib.ctyp -> Ast.id * Jib.ctyp Ast_util.Bindings.t
Sourceval struct_fields : Ast.l -> ctx -> Jib.ctyp -> Ast.id * (Ast.id -> Jib.ctyp)
Sourceval variant_constructor_bindings : Ast.l -> ctx -> Jib.ctyp -> Ast.id * Jib.ctyp Ast_util.Bindings.t
Sourceval enum_members : Ast.l -> ctx -> Ast.id -> Ast_util.IdSet.t

Compilation functions

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

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