sail

Sail is a language for describing the instruction semantics of processors
IN THIS PACKAGE
Module Interpreter
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 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 =
| Done of state * Value.value
| 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
| Break of frame
| Effect_request of string Lazy.t * state * (string Lazy.t * lstate * ( return_value -> Type_check.tannot Ast.exp monad )) list * effect_request
| 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 =
| 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 ) 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 =
| Value_success of Value.value
| 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