Compile Sail ASTs to Jib intermediate representation
val optimize_aarch64_fast_struct : bool refThis 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 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.
type ctx = {target_name : string;records : (Ast.kid list * Jib.ctyp Ast_util.Bindings.t) Ast_util.Bindings.t;enums : Ast_util.IdSet.t Ast_util.Bindings.t;variants : (Ast.kid list * Jib.ctyp Ast_util.Bindings.t) Ast_util.Bindings.t;abstracts : Jib.ctyp Ast_util.Bindings.t;valspecs : (string option * Jib.ctyp list * Jib.ctyp * Ast_util.uannot)
Ast_util.Bindings.t;quants : Jib.ctyp Ast_util.KBindings.t;local_env : Type_check.Env.t;tc_env : Type_check.Env.t;effect_info : Effects.side_effect_info;locals : (Ast_util.mut * Jib.ctyp) Ast_util.Bindings.t;registers : Jib.ctyp Ast_util.Bindings.t;letbinds : int list;letbind_ids : Ast_util.IdSet.t;no_raw : bool;no_static : bool;coverage_override : bool;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.
val initial_ctx :
?for_target:string ->
Type_check.Env.t ->
Effects.side_effect_info ->
ctxCreate 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".
module type CONFIG = sig ... endThe 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 ... endval callgraph : Jib.cdef list -> IdGraph.graph