Compile Sail ASTs to Jib intermediate representation
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.
(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 = {records : (Ast.kid list * Jib.ctyp Jib_util.UBindings.t) Ast_util.Bindings.t;enums : Ast_util.IdSet.t Ast_util.Bindings.t;variants : (Ast.kid list * Jib.ctyp Jib_util.UBindings.t) Ast_util.Bindings.t;valspecs : (string option * Jib.ctyp list * Jib.ctyp) 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;letbinds : int list;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 initial_ctx : Type_check.Env.t -> Effects.side_effect_info -> ctxmodule 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)
val add_special_functions :
Type_check.Env.t ->
Effects.side_effect_info ->
Type_check.Env.t * Effects.side_effect_infoAdds some special functions to the environment that are used to convert several Sail language features, these are sail_assert, sail_exit, and sail_cons.