package sail

You can search for identifiers within the package.

in-package search v0.2.0

package sail

sail
- Anf
- Ast
- Ast_util
  - BE
  - BESet
  - Bindings
  - Id
  - IdSet
  - KBindings
  - KOpt
  - KOptMap
  - KOptSet
  - Kid
  - KidSet
  - Kind
  - NC
  - NCMap
  - Nexp
  - NexpMap
  - NexpSet
  - Typ
  - TypMap
- Bitfield
- C_backend
- Cgen_backend
- Constant_fold
  - StringMap
- Constant_propagation
- Constant_propagation_mutrec
- Constraint
- Elf_loader
- Error_format
- Graph
  - Make
    
    Ord
  - OrderedType
  - S
- Initial_check
- Interactive
- Interpreter
- Jib
- Jib_compile
  - Config
  - Make
    
    C
- Jib_interactive
- Jib_ir
  - Flat_ir_config
  - Flat_ir_formatter
  - Ir_formatter
    
    Config
    
    Make
    
    C
  - StringMap
- Jib_optimize
- Jib_smt
  - EventMap
  - IntSet
  - Make_optimizer
    
    S
  - Sequence
- Jib_ssa
  - IntSet
- Jib_util
  - CT
  - CTMap
  - CTSet
  - Name
  - NameCT
  - NameCTMap
  - NameCTSet
  - NameMap
  - NameSet
  - UBindings
  - UId
- Latex
  - StringSet
- Lexer
  - M
- Manifest
- Monomorphise
- Nl_flow
- Ocaml_backend
- Optimize
- Parse_ast
- Parser
- Parser_combinators
- Pattern_completeness
- Pretty_print
- Pretty_print_common
- Pretty_print_coq
  - StringSet
- Pretty_print_lem
  - StringSet
- Pretty_print_sail
- Process_file
- Profile
- Property
  - Event
- Reporting
- Rewriter
- Rewrites
- Sail2_values
- Sail_lib
  - BitType
  - Mem
- Scattered
- Smtlib
- Spec_analysis
- Specialize
- State
- ToFromInterp_backend
- ToFromInterp_lib_bitlist
  - Make
    
    BitT
- ToFromInterp_lib_mword
- Type_check
  - Env
- Type_error
- Util
- Value
  - StringMap

Legend:
Library
Module
Module type
Parameter
Class
Class type

type gstate = {

registers : Value.value Ast_util.Bindings.t;
allow_registers : bool;
primops : (Value.value list -> Value.value) Value.StringMap.t;
letbinds : Type_check.tannot Ast.letbind list;
fundefs : Type_check.tannot Ast.fundef Ast_util.Bindings.t;
last_write_ea : (Value.value * Value.value * Value.value) option;
typecheck_env : Type_check.Env.t;

}

type lstate = {

locals : Value.value Ast_util.Bindings.t;

}

type state = lstate * gstate

val value_of_lit : Ast.lit -> Value.value

val is_value : 'a Ast.exp -> bool

val is_true : 'a Ast.exp -> bool

val is_false : 'a Ast.exp -> bool

val exp_of_value : Value.value -> Type_check.tannot Ast.exp

val value_of_exp : 'a Ast.exp -> Value.value

val fallthrough : Type_check.tannot Ast.pexp

type return_value =

| Return_ok of Value.value
| Return_exception of Value.value

type !'a response =

| Early_return of Value.value
| Exception of Value.value
| Assertion_failed of string
| Call of Ast.id * Value.value list * return_value -> 'a
| Fail of string
| Read_mem of Value.value * Value.value * Value.value * Value.value -> 'a
| Write_ea of Value.value * Value.value * Value.value * unit -> 'a
| Excl_res of bool -> 'a
| Write_mem of Value.value * Value.value * Value.value * Value.value * bool -> 'a
| Barrier of Value.value * unit -> 'a
| Read_reg of string * Value.value -> 'a
| Write_reg of string * Value.value * unit -> 'a
| Get_primop of string * (Value.value list -> Value.value) -> 'a
| Get_local of string * Value.value -> 'a
| Put_local of string * Value.value * unit -> 'a
| Get_global_letbinds of Type_check.tannot Ast.letbind list -> 'a

and !'a monad =

| Pure of 'a
| Yield of 'a monad response

val map_response : ('a -> 'b) -> 'a response -> 'b response

val liftM : ('a -> 'b) -> 'a monad -> 'b monad

val return : 'a -> 'a monad

val bind : 'a monad -> ('a -> 'b monad) -> 'b monad

val (>>=) : 'a monad -> ('a -> 'b monad) -> 'b monad

val (>>) : unit monad -> 'a monad -> 'a monad

type (!'a, !'b) either =

| Left of 'a
| Right of 'b

val catch : 'a monad -> (Value.value, 'a) either monad

val throw : Value.value -> 'a monad

val call : Ast.id -> Value.value list -> return_value monad

val read_mem : Value.value -> Value.value -> Value.value -> Value.value monad

val write_ea : Value.value -> Value.value -> Value.value -> unit monad

val excl_res : unit -> bool monad

val write_mem : 
  Value.value ->
  Value.value ->
  Value.value ->
  Value.value ->
  bool monad

val barrier : Value.value -> unit monad

val read_reg : string -> Value.value monad

val write_reg : string -> Value.value -> unit monad

val fail : string -> 'a monad

val get_primop : string -> (Value.value list -> Value.value) monad

val get_local : string -> Value.value monad

val put_local : string -> Value.value -> unit monad

val get_global_letbinds : unit -> Type_check.tannot Ast.letbind list monad

val early_return : Value.value -> 'a monad

val assertion_failed : string -> 'a monad

val liftM2 : ('a -> 'b -> 'c) -> 'a monad -> 'b monad -> 'c monad

val letbind_pat_ids : 'a Ast.letbind -> Ast_util.IdSet.t

val subst : 
  Ast.id ->
  Value.value ->
  Type_check.tannot Ast.exp ->
  Type_check.tannot Ast.exp

val local_variable : 
  Ast_util.Bindings.key ->
  lstate ->
  'a ->
  Type_check.tannot Ast.exp

val unit_exp : 'a Ast.exp_aux

val is_value_fexp : 'a Ast.fexp -> bool

val value_of_fexp : 'a Ast.fexp -> string * Value.value

val build_letchain : 
  Ast_util.IdSet.elt ->
  'a Ast.letbind list ->
  'a Ast.exp ->
  'a Ast.exp

val is_interpreter_extern : Ast.id -> Type_check.Env.t -> bool

val get_interpreter_extern : Ast.id -> Type_check.Env.t -> string

val step : Type_check.tannot Ast.exp -> Type_check.tannot Ast.exp monad

val combine : 
  Ast_util.Bindings.key ->
  Value.value option ->
  Value.value option ->
  Value.value option

val exp_of_lexp : unit Ast.lexp -> unit Ast.exp

val pattern_match : 
  Type_check.Env.t ->
  Type_check.tannot Ast.pat ->
  Value.value ->
  bool * Value.value Ast_util.Bindings.t

val exp_of_fundef : 
  Type_check.tannot Ast.fundef ->
  Value.value ->
  Type_check.tannot Ast.exp

val ast_letbinds : 'a Ast.defs -> 'a Ast.letbind list

val initial_lstate : lstate

val stack_cont : ('a * 'b * 'c) -> 'c

val stack_string : ('a * 'b * 'c) -> 'a

val stack_state : ('a * 'b * 'c) -> 'b

type frame =

| Done of state * Value.value
| Step of string Stdlib.Lazy.t * state * Type_check.tannot Ast.exp monad * (string Stdlib.Lazy.t * lstate * (return_value -> Type_check.tannot Ast.exp monad)) list
| Break of frame
| Effect_request of string Stdlib.Lazy.t * state * (string Stdlib.Lazy.t * lstate * (return_value -> Type_check.tannot Ast.exp monad)) list * effect_request
| Fail of string Stdlib.Lazy.t * state * Type_check.tannot Ast.exp monad * (string Stdlib.Lazy.t * lstate * (return_value -> Type_check.tannot Ast.exp monad)) list * string

and effect_request =

| Read_mem of Value.value * Value.value * Value.value * Value.value -> state -> frame
| Write_ea of Value.value * Value.value * Value.value * unit -> state -> frame
| Excl_res of bool -> state -> frame
| Write_mem of Value.value * Value.value * Value.value * Value.value * bool -> state -> frame
| Barrier of Value.value * unit -> state -> frame
| Read_reg of string * Value.value -> state -> frame
| Write_reg of string * Value.value * unit -> state -> frame

val eval_frame' : frame -> frame

val eval_frame : frame -> frame

val default_effect_interp : state -> effect_request -> frame

val effect_interp : (state -> effect_request -> frame) Stdlib.ref

val set_effect_interp : (state -> effect_request -> frame) -> unit

val run_frame : frame -> Value.value

val eval_exp : state -> Type_check.tannot Ast.exp -> Value.value

val initial_gstate : 
  (Value.value list -> Value.value) Value.StringMap.t ->
  Type_check.tannot Ast.defs ->
  Type_check.Env.t ->
  gstate

val initialize_registers : 
  bool ->
  gstate ->
  Type_check.tannot Ast.defs ->
  gstate

val initial_state : 
  ?registers:bool ->
  Type_check.tannot Ast.defs ->
  Type_check.Env.t ->
  (Value.value list -> Value.value) Value.StringMap.t ->
  lstate * gstate

type value_result =

| Value_success of Value.value
| Value_error of exn

val decode_instruction : state -> Ast.lit_aux list -> value_result

val annot_exp_effect : 
  Type_check.tannot Ast.exp_aux ->
  Ast.l ->
  Type_check.Env.t ->
  Ast.typ ->
  Ast.effect ->
  Type_check.tannot Ast.exp

val annot_exp : 
  Type_check.tannot Ast.exp_aux ->
  Ast.l ->
  Type_check.Env.t ->
  Ast.typ ->
  Type_check.tannot Ast.exp

val id_typ : string -> Ast.typ

val analyse_instruction : state -> Value.value -> frame

val execute_instruction : state -> Value.value -> frame