package libsail

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Instruction construction functions, and Jib names
. Functions and modules for working with ctyps
1. Operations for polymorphic Jib ctyps
2. Infer types
Functions for mapping over and extracting information from instructions, values, and definitions

package libsail

libsail
- Libsail
  - Anf
  - Ast
  - Ast_defs
  - Ast_util
    
    Bindings
    
    Id
    
    IdSet
    
    KBindings
    
    KOpt
    
    KOptMap
    
    KOptSet
    
    Kid
    
    KidSet
    
    Kind
    
    NC
    
    NCMap
    
    Nexp
    
    NexpMap
    
    NexpSet
    
    Typ
    
    TypMap
  - Bitfield
  - Callgraph
    
    G
    
    Node
  - Chunk_ast
  - Constant_fold
    
    StringMap
  - Constant_propagation
  - Constant_propagation_mutrec
  - Constraint
  - Effects
    
    EffectSet
  - Elf_loader
  - Error_format
  - Format_sail
    
    CONFIG
    
    Make
    
    Config
  - Frontend
  - Graph
    
    Make
    
    Ord
    
    OrderedType
    
    S
  - Initial_check
  - Interactive
  - Interpreter
  - Jib
  - Jib_compile
    
    Config
    
    IdGraph
    
    Make
    
    C
  - Jib_optimize
  - Jib_util
    
    CTListSet
    
    CTMap
    
    CTSet
    
    Name
    
    NameCTMap
    
    NameCTSet
    
    NameMap
    
    NameSet
  - Lexer
    
    M
  - Libsail_sites
    
    Sites
  - Mappings
  - Monad_params
  - Monomorphise
  - Nl_flow
  - Outcome_rewrites
  - Parse_ast
  - Parser
  - Parser_combinators
  - Pattern_completeness
    
    Config
    
    Make
    
    C
  - Preprocess
  - Pretty_print_common
  - Pretty_print_sail
  - Profile
  - Property
    
    Event
  - Reporting
  - Rewriter
  - Rewrites
  - Sail2_instr_kinds
  - Sail2_operators
  - Sail2_operators_bitlists
  - Sail2_prompt
  - Sail2_prompt_monad
  - Sail2_values
  - Sail_lib
    
    BitType
    
    Mem
  - Scattered
    
    PC
    
    PC_config
  - Spec_analysis
  - Specialize
  - Splice
  - State
  - Target
  - Type_check
    
    Env
  - Type_error
  - Util
    
    Duplicate
    
    S
    
    IntIntSet
    
    IntSet
  - Value
    
    StringMap
  - Value2

Legend:
Library
Module
Module type
Parameter
Class
Class type

Utilities and helper functions for operating on Jib instructions and definitions

Instruction construction functions, and Jib names

val symbol_generator : string -> (unit -> Ast.id) * (unit -> unit)

Create a generator that produces fresh names, paired with a function that resets the generator (allowing it to regenerate the same name).

val idecl : Ast.l -> Jib.ctyp -> Jib.name -> Jib.instr

val ireset : Ast.l -> Jib.ctyp -> Jib.name -> Jib.instr

val iinit : Ast.l -> Jib.ctyp -> Jib.name -> Jib.cval -> Jib.instr

val iif : 
  Ast.l ->
  Jib.cval ->
  Jib.instr list ->
  Jib.instr list ->
  Jib.ctyp ->
  Jib.instr

val ifuncall : 
  Ast.l ->
  Jib.clexp ->
  (Ast.id * Jib.ctyp list) ->
  Jib.cval list ->
  Jib.instr

val iextern : 
  Ast.l ->
  Jib.clexp ->
  (Ast.id * Jib.ctyp list) ->
  Jib.cval list ->
  Jib.instr

val icopy : Ast.l -> Jib.clexp -> Jib.cval -> Jib.instr

val iclear : ?loc:Ast.l -> Jib.ctyp -> Jib.name -> Jib.instr

val ireturn : ?loc:Ast.l -> Jib.cval -> Jib.instr

val iend : Ast.l -> Jib.instr

val iblock : ?loc:Ast.l -> Jib.instr list -> Jib.instr

val itry_block : Ast.l -> Jib.instr list -> Jib.instr

val ithrow : Ast.l -> Jib.cval -> Jib.instr

val icomment : ?loc:Ast.l -> string -> Jib.instr

val ilabel : ?loc:Ast.l -> string -> Jib.instr

val igoto : ?loc:Ast.l -> string -> Jib.instr

val iundefined : ?loc:Ast.l -> Jib.ctyp -> Jib.instr

val imatch_failure : Ast.l -> Jib.instr

val iexit : Ast.l -> Jib.instr

val iraw : ?loc:Ast.l -> string -> Jib.instr

val ijump : Ast.l -> Jib.cval -> string -> Jib.instr

val label : string -> string

Create a new unique label by concatenating a string with a unique identifier

module Name : sig ... end

module NameSet : sig ... end

module NameMap : sig ... end

val current_exception : Jib.name

val have_exception : Jib.name

val throw_location : Jib.name

val return : Jib.name

val name : Ast.id -> Jib.name

val global : Ast.id -> Jib.name

val cval_rename : Jib.name -> Jib.name -> Jib.cval -> Jib.cval

val clexp_rename : Jib.name -> Jib.name -> Jib.clexp -> Jib.clexp

val instr_rename : Jib.name -> Jib.name -> Jib.instr -> Jib.instr

val instrs_rename : Jib.name -> Jib.name -> Jib.instr list -> Jib.instr list

val string_of_name : 
  ?deref_current_exception:bool ->
  ?zencode:bool ->
  Jib.name ->
  string

val string_of_op : Jib.op -> string

val string_of_ctyp : Jib.ctyp -> string

val string_of_uid : (Ast.id * Jib.ctyp list) -> string

val string_of_value : Value2.vl -> string

val string_of_cval : Jib.cval -> string

. Functions and modules for working with ctyps

val map_ctyp : (Jib.ctyp -> Jib.ctyp) -> Jib.ctyp -> Jib.ctyp

val ctyp_equal : Jib.ctyp -> Jib.ctyp -> bool

val ctyp_compare : Jib.ctyp -> Jib.ctyp -> int

module CTSet : sig ... end

module CTMap : sig ... end

module CTListSet : sig ... end

module NameCTSet : sig ... end

module NameCTMap : sig ... end

Operations for polymorphic Jib ctyps

val ctyp_unify : Ast.l -> Jib.ctyp -> Jib.ctyp -> Jib.ctyp Ast_util.KBindings.t

val merge_unifiers : Ast.kid -> Jib.ctyp -> Jib.ctyp -> Jib.ctyp option

val ctyp_suprema : Jib.ctyp -> Jib.ctyp

val ctyp_vars : Jib.ctyp -> Ast_util.KidSet.t

val ctyp_ids : Jib.ctyp -> Ast_util.IdSet.t

val is_polymorphic : Jib.ctyp -> bool

val subst_poly : Jib.ctyp Ast_util.KBindings.t -> Jib.ctyp -> Jib.ctyp

Infer types

val cval_ctyp : Jib.cval -> Jib.ctyp

val clexp_ctyp : Jib.clexp -> Jib.ctyp

val cdef_ctyps : Jib.cdef -> CTSet.t

Functions for mapping over and extracting information from instructions, values, and definitions

val instr_ids : Jib.instr -> NameSet.t

val instr_reads : Jib.instr -> NameSet.t

val instr_writes : Jib.instr -> NameSet.t

val instr_typed_writes : Jib.instr -> NameCTSet.t

val map_cval : (Jib.cval -> Jib.cval) -> Jib.cval -> Jib.cval

val map_instr : (Jib.instr -> Jib.instr) -> Jib.instr -> Jib.instr

Map over each instruction within an instruction, bottom-up

val map_instrs : (Jib.instr list -> Jib.instr list) -> Jib.instr -> Jib.instr

val concatmap_instr : 
  (Jib.instr -> Jib.instr list) ->
  Jib.instr ->
  Jib.instr list

Concat-map over each instruction within an instruction, bottom-up

val iter_instr : (Jib.instr -> unit) -> Jib.instr -> unit

Iterate over each instruction within an instruction, bottom-up

val cdef_map_instr : (Jib.instr -> Jib.instr) -> Jib.cdef -> Jib.cdef

Map over each instruction in a cdef using map_instr

val map_clexp_ctyp : (Jib.ctyp -> Jib.ctyp) -> Jib.clexp -> Jib.clexp

val map_cval_ctyp : (Jib.ctyp -> Jib.ctyp) -> Jib.cval -> Jib.cval

val map_instr_ctyp : (Jib.ctyp -> Jib.ctyp) -> Jib.instr -> Jib.instr

val cdef_map_ctyp : (Jib.ctyp -> Jib.ctyp) -> Jib.cdef -> Jib.cdef

val map_instr_cval : (Jib.cval -> Jib.cval) -> Jib.instr -> Jib.instr

val map_instr_list : 
  (Jib.instr -> Jib.instr) ->
  Jib.instr list ->
  Jib.instr list

val filter_instrs : (Jib.instr -> bool) -> Jib.instr list -> Jib.instr list

val instr_split_at : 
  (Jib.instr -> bool) ->
  Jib.instr list ->
  Jib.instr list * Jib.instr list

val map_funcall : 
  (Jib.instr -> Jib.instr list -> Jib.instr list) ->
  Jib.instr list ->
  Jib.instr list

Map over function calls in an instruction sequence, including exception handler where present

val cdef_map_funcall : 
  (Jib.instr -> Jib.instr list -> Jib.instr list) ->
  Jib.cdef ->
  Jib.cdef

Map over each function call in a cdef using map_funcall

val cdef_map_cval : (Jib.cval -> Jib.cval) -> Jib.cdef -> Jib.cdef

val cdef_concatmap_instr : 
  (Jib.instr -> Jib.instr list) ->
  Jib.cdef ->
  Jib.cdef

Map over each instruction in a cdef using concatmap_instr

val c_ast_registers : 
  Jib.cdef list ->
  (Ast.id * Jib.ctyp * Jib.instr list) list