package sail

You can search for identifiers within the package.

in-package search v0.2.0

package sail

sail
- Anf
- Ast
- Ast_defs
- Ast_util
  - BE
  - BESet
  - Bindings
  - Id
  - IdSet
  - KBindings
  - KOpt
  - KOptMap
  - KOptSet
  - Kid
  - KidSet
  - Kind
  - NC
  - NCMap
  - Nexp
  - NexpMap
  - NexpSet
  - Typ
  - TypMap
- Bitfield
- C_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
- Slice
  - Node
- Smtlib
- Spec_analysis
- Specialize
- Splice
- 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 ii = Nat_big_num.num

type nn = Nat_big_num.num

val nat_of_int : Nat_big_num.num -> int

val pow : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num

val pow2 : Nat_big_num.num -> Nat_big_num.num

val prerr : string -> unit

val print_int : string -> Nat_big_num.num -> unit

val prerr_int : string -> Nat_big_num.num -> unit

val shr_int : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num

val shl_int : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num

val take_list : Nat_big_num.num -> 'a list -> 'a list

val drop_list : Nat_big_num.num -> 'a list -> 'a list

val repeat : 'a list -> Nat_big_num.num -> 'a list

val duplicate_to_list : 'a -> Nat_big_num.num -> 'a list

val replace : 'a list -> Nat_big_num.num -> 'a -> 'a list

val upper : 'a -> 'a

val tmod_int : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num

val hardware_mod : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num

val tdiv_int : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num

val hardware_quot : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num

val max_64u : Nat_big_num.num

val max_64 : Nat_big_num.num

val min_64 : Nat_big_num.num

val max_32u : Nat_big_num.num

val max_32 : Nat_big_num.num

val min_32 : Nat_big_num.num

val max_8 : Nat_big_num.num

val min_8 : Nat_big_num.num

val max_5 : Nat_big_num.num

val min_5 : Nat_big_num.num

val just_list : 'a option list -> 'a list option

val maybe_failwith : 'a option -> 'a

type bitU =

| B0
| B1
| BU

val showBitU : bitU -> string

val bitU_char : bitU -> char

val instance_Show_Show_Sail2_values_bitU_dict : 
  bitU Lem_pervasives_extra.show_class

val compare_bitU : bitU -> bitU -> int

val instance_Basic_classes_Ord_Sail2_values_bitU_dict : 
  bitU Lem_pervasives_extra.ord_class

type !'a bitU_class = {

to_bitU_method : 'a -> bitU;
of_bitU_method : bitU -> 'a;

}

val instance_Sail2_values_BitU_Sail2_values_bitU_dict : bitU bitU_class

val bool_of_bitU : bitU -> bool option

val bitU_of_bool : bool -> bitU

val cast_bit_bool : bitU -> bool option

val not_bit : bitU -> bitU

val is_one : Nat_big_num.num -> bitU

val and_bit : bitU -> bitU -> bitU

val or_bit : bitU -> bitU -> bitU

val xor_bit : bitU -> bitU -> bitU

val bools_of_nat_aux : 
  Nat_big_num.num ->
  Nat_big_num.num ->
  bool list ->
  bool list

val bools_of_nat : Nat_big_num.num -> Nat_big_num.num -> bool list

val nat_of_bools_aux : Nat_big_num.num -> bool list -> Nat_big_num.num

val nat_of_bools : bool list -> Nat_big_num.num

val unsigned_of_bools : bool list -> Nat_big_num.num

val signed_of_bools : bool list -> Nat_big_num.num

val int_of_bools : bool -> bool list -> Nat_big_num.num

val pad_list : 'a -> 'a list -> Nat_big_num.num -> 'a list

val ext_list : 'a -> Nat_big_num.num -> 'a list -> 'a list

val extz_bools : Nat_big_num.num -> bool list -> bool list

val exts_bools : Nat_big_num.num -> bool list -> bool list

val add_one_bool_ignore_overflow_aux : bool list -> bool list

val add_one_bool_ignore_overflow : bool list -> bool list

val bools_of_int : Nat_big_num.num -> Nat_big_num.num -> bool list

val has_undefined_bits : bitU list -> bool

val bits_of_nat : Nat_big_num.num -> Nat_big_num.num -> bitU list

val nat_of_bits : bitU list -> Nat_big_num.num option

val not_bits : bitU list -> bitU list

val binop_list : ('b -> 'c -> 'a) -> 'b list -> 'c list -> 'a list

val unsigned_of_bits : bitU list -> Nat_big_num.num option

val signed_of_bits : bitU list -> Nat_big_num.num option

val int_of_bits : bool -> bitU list -> Nat_big_num.num option

val extz_bits : Nat_big_num.num -> bitU list -> bitU list

val exts_bits : Nat_big_num.num -> bitU list -> bitU list

val add_one_bit_ignore_overflow_aux : bitU list -> bitU list

val add_one_bit_ignore_overflow : bitU list -> bitU list

val bits_of_int : Nat_big_num.num -> Nat_big_num.num -> bitU list

val arith_op_bits : 
  (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) ->
  bool ->
  bitU list ->
  bitU list ->
  bitU list

val char_of_nibble : (bitU * bitU * bitU * bitU) -> char option

val nibble_of_char : char -> (bitU * bitU * bitU * bitU) option

val hexstring_of_bits : bitU list -> char list option

val show_bitlist_prefix : char -> bitU list -> string

val show_bitlist : bitU list -> string

val hex_char : Nat_big_num.num -> char

val hex_str_aux : Nat_big_num.num -> char list -> char list

val hex_str : Nat_big_num.num -> string

val subrange_list_inc : 
  'a list ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  'a list

val subrange_list_dec : 
  'a list ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  'a list

val subrange_list : 
  bool ->
  'a list ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  'a list

val update_subrange_list_inc : 
  'a list ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  'a list ->
  'a list

val update_subrange_list_dec : 
  'a list ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  'a list ->
  'a list

val update_subrange_list : 
  bool ->
  'a list ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  'a list ->
  'a list

val access_list_inc : 'a list -> Nat_big_num.num -> 'a

val access_list_dec : 'a list -> Nat_big_num.num -> 'a

val access_list : bool -> 'a list -> Nat_big_num.num -> 'a

val update_list_inc : 'a list -> Nat_big_num.num -> 'a -> 'a list

val update_list_dec : 'a list -> Nat_big_num.num -> 'a -> 'a list

val update_list : bool -> 'a list -> Nat_big_num.num -> 'a -> 'a list

val extract_only_bit : bitU list -> bitU

val slice_mword_dec : 
  ('a * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Lem.mword

val slice_mword_inc : 
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Lem.mword

val slice_mword : 
  bool ->
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Lem.mword

val update_slice_mword_dec : 
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  ('a * Big_int_impl.BI.big_int) ->
  Lem.mword

val update_slice_mword_inc : 
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  ('a * Big_int_impl.BI.big_int) ->
  Lem.mword

val update_slice_mword : 
  bool ->
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  ('a * Big_int_impl.BI.big_int) ->
  Lem.mword

val access_mword_dec : 
  ('a * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  bitU

val access_mword_inc : 
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  bitU

val access_mword : 
  bool ->
  (int * Big_int_impl.BI.big_int) ->
  Nat_big_num.num ->
  bitU

val update_mword_bool_dec : 
  (int * Nat_big_num.num) ->
  Nat_big_num.num ->
  bool ->
  Lem.mword

val update_mword_dec : 
  (int * Nat_big_num.num) ->
  Nat_big_num.num ->
  bitU ->
  Lem.mword option

val update_mword_bool_inc : 
  (int * Nat_big_num.num) ->
  Nat_big_num.num ->
  bool ->
  Lem.mword

val update_mword_inc : 
  (int * Nat_big_num.num) ->
  Nat_big_num.num ->
  bitU ->
  Lem.mword option

val int_of_mword : bool -> (int * Big_int_impl.BI.big_int) -> Nat_big_num.num

val size_itself_int : 'a Lem_machine_word.size_class -> 'b -> Nat_big_num.num

val make_the_value : 'a -> unit

type !'a bitvector_class = {

bits_of_method : 'a -> bitU list;
of_bits_method : bitU list -> 'a option;
of_bools_method : bool list -> 'a;
length_method : 'a -> Nat_big_num.num;
of_int_method : Nat_big_num.num -> Nat_big_num.num -> 'a;
unsigned_method : 'a -> Nat_big_num.num option;
signed_method : 'a -> Nat_big_num.num option;
arith_op_bv_method : (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) -> bool -> 'a -> 'a -> 'a;

}

val of_bits_failwith : 'a bitvector_class -> bitU list -> 'a

val int_of_bv : 'a bitvector_class -> bool -> 'a -> Nat_big_num.num option

val instance_Sail2_values_Bitvector_list_dict : 
  'a bitU_class ->
  'a list bitvector_class

val instance_Sail2_values_Bitvector_Machine_word_mword_dict : 
  'a Lem_machine_word.size_class ->
  Lem.mword bitvector_class

val access_bv_inc : 'a bitvector_class -> 'a -> Nat_big_num.num -> bitU

val access_bv_dec : 'a bitvector_class -> 'a -> Nat_big_num.num -> bitU

val update_bv_inc : 
  'a bitvector_class ->
  'a ->
  Nat_big_num.num ->
  bitU ->
  bitU list

val update_bv_dec : 
  'a bitvector_class ->
  'a ->
  Nat_big_num.num ->
  bitU ->
  bitU list

val subrange_bv_inc : 
  'a bitvector_class ->
  'a ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  bitU list

val subrange_bv_dec : 
  'a bitvector_class ->
  'a ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  bitU list

val update_subrange_bv_inc : 
  'a bitvector_class ->
  'b bitvector_class ->
  'b ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  'a ->
  bitU list

val update_subrange_bv_dec : 
  'a bitvector_class ->
  'b bitvector_class ->
  'b ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  'a ->
  bitU list

val extz_bv : 'a bitvector_class -> Nat_big_num.num -> 'a -> bitU list

val exts_bv : 'a bitvector_class -> Nat_big_num.num -> 'a -> bitU list

val nat_of_bv : 'a bitvector_class -> 'a -> int option

val string_of_bv : 'a bitvector_class -> 'a -> string

val print_bits : 'a bitvector_class -> string -> 'a -> unit

val dec_str : Nat_big_num.num -> string

val concat_str : string -> string -> string

val int_of_bit : bitU -> Nat_big_num.num

val count_leading_zero_bits : bitU list -> Nat_big_num.num

val count_leading_zeros_bv : 'a bitvector_class -> 'a -> Nat_big_num.num

val decimal_string_of_bv : 'a bitvector_class -> 'a -> string

type memory_byte = bitU list

val byte_chunks : 'a list -> 'a list list option

val bytes_of_bits : 'a bitvector_class -> 'a -> bitU list list option

val bits_of_bytes : bitU list list -> bitU list

val mem_bytes_of_bits : 'a bitvector_class -> 'a -> bitU list list option

val bits_of_mem_bytes : bitU list list -> bitU list

val reverse_endianness_list : 'a list -> 'a list

type (!'regstate, !'regval, !'a) register_ref = {

name : string;
read_from : 'regstate -> 'a;
write_to : 'a -> 'regstate -> 'regstate;
of_regval : 'regval -> 'a option;
regval_of : 'a -> 'regval;

}

type (!'regstate, !'regval) register_accessors =
  (string ->
  'regstate ->
  'regval option)
  * (string ->
  'regval ->
  'regstate ->
  'regstate option)

type (!'regtype, !'a) field_ref = {

field_name : string;
field_start : Nat_big_num.num;
field_is_inc : bool;
get_field : 'regtype -> 'a;
set_field : 'regtype -> 'a -> 'regtype;

}

val foreach : 'a list -> 'vars -> ('a -> 'vars -> 'vars) -> 'vars

val index_list : 
  Nat_big_num.num ->
  Nat_big_num.num ->
  Nat_big_num.num ->
  Nat_big_num.num list

val while0 : 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars

val until : 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars

type !'a toNatural_class = {

toNatural_method : 'a -> Nat_big_num.num;

}

val instance_Sail2_values_ToNatural_Num_integer_dict : 
  Nat_big_num.num toNatural_class

val instance_Sail2_values_ToNatural_Num_int_dict : int toNatural_class

val instance_Sail2_values_ToNatural_nat_dict : int toNatural_class

val instance_Sail2_values_ToNatural_Num_natural_dict : 
  Nat_big_num.num toNatural_class

val toNaturalFiveTup : 
  'a toNatural_class ->
  'b toNatural_class ->
  'c toNatural_class ->
  'd toNatural_class ->
  'e toNatural_class ->
  ('d * 'c * 'b * 'a * 'e) ->
  Nat_big_num.num
  * Nat_big_num.num
  * Nat_big_num.num
  * Nat_big_num.num
  * Nat_big_num.num