sail

Sail is a language for describing the instruction semantics of processors
IN THIS PACKAGE
Module Jib
type name =
| Name of Ast.id * int
| Global of Ast.id * int
| Have_exception of int
| Current_exception of int
| Throw_location of int
| Return of int
type ctyp =
| CT_lint
| CT_fint of int
| CT_constant of Nat_big_num.num
| CT_lbits of bool
| CT_sbits of int * bool
| CT_fbits of int * bool
| CT_unit
| CT_bool
| CT_bit
| CT_string
| CT_real
| CT_tup of ctyp list
| CT_enum of Ast.id * Ast.id list
| CT_struct of Ast.id * ((Ast.id * ctyp list) * ctyp) list
| CT_variant of Ast.id * ((Ast.id * ctyp list) * ctyp) list
| CT_fvector of int * bool * ctyp
| CT_vector of bool * ctyp
| CT_list of ctyp
| CT_ref of ctyp
| CT_poly
type op =
| Bnot
| Bor
| Band
| List_hd
| List_tl
| Eq
| Neq
| Ilt
| Ilteq
| Igt
| Igteq
| Iadd
| Isub
| Unsigned of int
| Signed of int
| Bvnot
| Bvor
| Bvand
| Bvxor
| Bvadd
| Bvsub
| Bvaccess
| Concat
| Zero_extend of int
| Sign_extend of int
| Slice of int
| Sslice of int
| Set_slice
| Replicate of int
type clexp =
| CL_id of name * ctyp
| CL_rmw of name * name * ctyp
| CL_field of clexp * Ast.id * ctyp list
| CL_addr of clexp
| CL_tuple of clexp * int
| CL_void
type cval =
| V_id of name * ctyp
| V_lit of Value2.vl * ctyp
| V_struct of ((Ast.id * ctyp list) * cval) list * ctyp
| V_ctor_kind of cval * Ast.id * ctyp list * ctyp
| V_ctor_unwrap of Ast.id * cval * ctyp list * ctyp
| V_tuple_member of cval * int * int
| V_call of op * cval list
| V_field of cval * Ast.id * ctyp list
| V_poly of cval * ctyp
type iannot = int * Parse_ast.l
type ctype_def =
| CTD_enum of Ast.id * Ast.id list
| CTD_struct of Ast.id * ((Ast.id * ctyp list) * ctyp) list
| CTD_variant of Ast.id * ((Ast.id * ctyp list) * ctyp) list
type instr_aux =
| I_decl of ctyp * name
| I_init of ctyp * name * cval
| I_jump of cval * string
| I_goto of string
| I_label of string
| I_funcall of clexp * bool * Ast.id * ctyp list * cval list
| I_copy of clexp * cval
| I_clear of ctyp * name
| I_undefined of ctyp
| I_match_failure
| I_end of name
| I_if of cval * instr list * instr list * ctyp
| I_block of instr list
| I_try_block of instr list
| I_throw of cval
| I_comment of string
| I_raw of string
| I_return of cval
| I_reset of ctyp * name
| I_reinit of ctyp * name * cval
and instr =
| I_aux of instr_aux * iannot
type cdef =
| CDEF_reg_dec of Ast.id * ctyp * instr list
| CDEF_type of ctype_def
| CDEF_let of int * (Ast.id * ctyp) list * instr list
| CDEF_spec of Ast.id * string option * ctyp list * ctyp
| CDEF_fundef of Ast.id * Ast.id option * Ast.id list * instr list
| CDEF_startup of Ast.id * instr list
| CDEF_finish of Ast.id * instr list