package sail

  1. Overview
  2. Docs
type gstate = {
  1. registers : Value.value Ast_util.Bindings.t;
  2. allow_registers : bool;
  3. primops : (Value.value list -> Value.value) Value.StringMap.t;
  4. letbinds : Type_check.tannot Ast.letbind list;
  5. fundefs : Type_check.tannot Ast.fundef Ast_util.Bindings.t;
  6. last_write_ea : (Value.value * Value.value * Value.value) option;
  7. typecheck_env : Type_check.Env.t;
}
type lstate = {
  1. 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 =
  1. | Return_ok of Value.value
  2. | Return_exception of Value.value
type !'a response =
  1. | Early_return of Value.value
  2. | Exception of Value.value
  3. | Assertion_failed of string
  4. | Call of Ast.id * Value.value list * return_value -> 'a
  5. | Fail of string
  6. | Read_mem of Value.value * Value.value * Value.value * Value.value -> 'a
  7. | Write_ea of Value.value * Value.value * Value.value * unit -> 'a
  8. | Excl_res of bool -> 'a
  9. | Write_mem of Value.value * Value.value * Value.value * Value.value * bool -> 'a
  10. | Barrier of Value.value * unit -> 'a
  11. | Read_reg of string * Value.value -> 'a
  12. | Write_reg of string * Value.value * unit -> 'a
  13. | Get_primop of string * (Value.value list -> Value.value) -> 'a
  14. | Get_local of string * Value.value -> 'a
  15. | Put_local of string * Value.value * unit -> 'a
  16. | Get_global_letbinds of Type_check.tannot Ast.letbind list -> 'a
and !'a monad =
  1. | Pure of 'a
  2. | 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 =
  1. | Left of 'a
  2. | 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 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 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 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 defs_letbinds : 'a Ast.def list -> '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 =
  1. | Done of state * Value.value
  2. | Step of string Lazy.t * state * Type_check.tannot Ast.exp monad * (string Lazy.t * lstate * (return_value -> Type_check.tannot Ast.exp monad)) list
  3. | Break of frame
  4. | Effect_request of string Lazy.t * state * (string Lazy.t * lstate * (return_value -> Type_check.tannot Ast.exp monad)) list * effect_request
  5. | Fail of string Lazy.t * state * Type_check.tannot Ast.exp monad * (string Lazy.t * lstate * (return_value -> Type_check.tannot Ast.exp monad)) list * string
and effect_request =
  1. | Read_mem of Value.value * Value.value * Value.value * Value.value -> state -> frame
  2. | Write_ea of Value.value * Value.value * Value.value * unit -> state -> frame
  3. | Excl_res of bool -> state -> frame
  4. | Write_mem of Value.value * Value.value * Value.value * Value.value * bool -> state -> frame
  5. | Barrier of Value.value * unit -> state -> frame
  6. | Read_reg of string * Value.value -> state -> frame
  7. | 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) ref
val set_effect_interp : (state -> effect_request -> frame) -> unit
val run_frame : frame -> Value.value
val initialize_registers : bool -> gstate -> Type_check.tannot Ast.def list -> gstate
val initial_state : ?registers:bool -> Type_check.tannot Ast_defs.ast -> Type_check.Env.t -> (Value.value list -> Value.value) Value.StringMap.t -> lstate * gstate
type value_result =
  1. | Value_success of Value.value
  2. | Value_error of exn
val decode_instruction : state -> Ast.lit_aux list -> value_result
val id_typ : string -> Ast.typ
val analyse_instruction : state -> Value.value -> frame
val execute_instruction : state -> Value.value -> frame