package sail

  1. Overview
  2. Docs
package sail
Legend:
Library
Module
Module type
Parameter
Class
Class type
module Big_int = Nat_big_num
module type BitType = sig ... end
type !'a return = {
  1. return : 'b. 'a -> 'b;
}
type !'za zoption =
  1. | ZNone of unit
  2. | ZSome of 'za
val zint_forwards : Big_int.num -> string
val opt_trace : bool Stdlib.ref
val trace_depth : int Stdlib.ref
val random : bool Stdlib.ref
val opt_cycle_limit : int Stdlib.ref
val cycle_limit_reached : unit -> bool
val sail_call : ('t return -> 't) -> 't
val trace : string -> unit
val trace_write : string -> string -> unit
val trace_read : string -> string -> unit
val sail_trace_call : string -> string -> ('t -> string) -> ('t return -> 't) -> 't
val trace_call : string -> unit
type bit =
  1. | B0
  2. | B1
val eq_anything : ('a * 'a) -> bool
val eq_bit : ('a * 'a) -> bool
val and_bit : (bit * bit) -> bit
val or_bit : (bit * bit) -> bit
val xor_bit : (bit * bit) -> bit
val and_vec : (bit list * bit list) -> bit list
val and_bool : (bool * bool) -> bool
val or_vec : (bit list * bit list) -> bit list
val or_bool : (bool * bool) -> bool
val xor_vec : (bit list * bit list) -> bit list
val xor_bool : (bool * bool) -> bool
val undefined_bit : unit -> bit
val undefined_bool : unit -> bool
val undefined_vector : (Big_int.num * 'a) -> 'a list
val undefined_list : 'a -> 'b list
val undefined_bitvector : Big_int.num -> bit list
val undefined_string : unit -> string
val undefined_unit : unit -> unit
val undefined_int : unit -> Big_int.num
val undefined_nat : unit -> Big_int.num
val undefined_range : ('a * 'b) -> 'a
val internal_pick : 'a list -> 'a
val eq_int : (Big_int.num * Big_int.num) -> bool
val eq_bool : (bool * bool) -> bool
val drop : int -> 'a list -> 'a list
val take : int -> 'a list -> 'a list
val count_leading_zeros : bit list -> Big_int.num
val subrange : ('a list * Big_int.num * Big_int.num) -> 'a list
val slice : ('a list * Big_int.num * Big_int.num) -> 'a list
val eq_list : ('a list * 'a list) -> bool
val access : ('a list * Big_int.num) -> 'a
val append : ('a list * 'a list) -> 'a list
val update : ('a list * Big_int.num * 'a) -> 'a list
val update_subrange : ('a list * Big_int.num * 'b * 'a list) -> 'a list
val vector_truncate : ('a list * Big_int.num) -> 'a list
val vector_truncateLSB : ('a list * Big_int.num) -> 'a list
val length : 'a list -> Big_int.num
val big_int_of_bit : bit -> Big_int.num
val uint : bit list -> Big_int.num
val sint : bit list -> Big_int.num
val add_int : (Big_int.num * Big_int.num) -> Big_int.num
val sub_int : (Big_int.num * Big_int.num) -> Big_int.num
val sub_nat : (Big_int.num * Big_int.num) -> Big_int.num
val quotient : (Big_int.num * Big_int.num) -> Big_int.num
val quot_round_zero : (Big_int.num * Big_int.num) -> Big_int.num
val rem_round_zero : (Big_int.num * Big_int.num) -> Big_int.num
val modulus : (Big_int.num * Big_int.num) -> Big_int.num
val negate : Big_int.num -> Big_int.num
val tdiv_int : (Big_int.num * Big_int.num) -> Big_int.num
val tmod_int : (Big_int.num * Big_int.num) -> Big_int.num
val add_bit_with_carry : (bit * bit * bit) -> bit * bit
val sub_bit_with_carry : (bit * bit * bit) -> bit * bit
val not_bit : bit -> bit
val not_vec : bit list -> bit list
val add_vec_carry : (bit list * bit list) -> bit * bit list
val add_vec : (bit list * bit list) -> bit list
val replicate_bits : ('a list * Big_int.num) -> 'a list
val identity : 'a -> 'a
val get_slice_int' : (int * Big_int.num * int) -> bit list
val get_slice_int : (Big_int.num * Big_int.num * Big_int.num) -> bit list
val to_bits' : (int * Big_int.num) -> bit list
val to_bits : (Big_int.num * Big_int.num) -> bit list
val mult_vec : (bit list * bit list) -> bit list
val mults_vec : (bit list * bit list) -> bit list
val add_vec_int : (bit list * Big_int.num) -> bit list
val sub_vec : (bit list * bit list) -> bit list
val sub_vec_int : (bit list * Big_int.num) -> bit list
val bin_char : char -> bit
val hex_char : char -> bit list
val list_of_string : string -> char list
val bits_of_string : string -> bit list
val concat_str : (string * string) -> string
val break : int -> 'a list -> 'a list list
val string_of_bit : bit -> string
val char_of_bit : bit -> char
val int_of_bit : bit -> int
val bool_of_bit : bit -> bool
val bit_of_bool : bool -> bit
val bigint_of_bit : bit -> Big_int.num
val string_of_hex : bit list -> string
val string_of_bits : bit list -> string
val decimal_string_of_bits : bit list -> string
val hex_slice : (string * Big_int.num * Big_int.num) -> bit list
val putchar : Big_int.num -> unit
val bits_of_int : int -> int -> bit list
val bits_of_big_int : int -> Big_int.num -> bit list
val byte_of_int : int -> bit list
module Mem : sig ... end
val mem_pages : Stdlib.Bytes.t Mem.t Stdlib.ref
val page_shift_bits : int
val page_size_bytes : int
val page_no_of_addr : Big_int.num -> Big_int.num
val bottom_addr_of_page : Big_int.num -> Big_int.num
val top_addr_of_page : Big_int.num -> Big_int.num
val get_mem_page : Mem.key -> Stdlib.Bytes.t
val add_mem_bytes : Big_int.num -> bytes -> int -> int -> unit
val read_mem_bytes : Big_int.num -> int -> bytes
val write_ram' : (Big_int.num * Big_int.num * bit list) -> unit
val write_ram : ('a * Big_int.num * 'b * bit list * bit list) -> bool
val wram : Big_int.num -> int -> unit
val read_ram : ('a * Big_int.num * 'b * bit list) -> bit list
val fast_read_ram : (Big_int.num * bit list) -> bit list
val tag_ram : bool Mem.t Stdlib.ref
val write_tag_bool : (bit list * bool) -> unit
val read_tag_bool : bit list -> bool
val reverse_endianness : 'a list -> 'a list
val zcast_unit_vec : 'a -> 'a list
val shl_int : (Big_int.num * Big_int.num) -> Big_int.num
val shr_int : (Big_int.num * Big_int.num) -> Big_int.num
val lor_int : (Big_int.num * Big_int.num) -> Big_int.num
val land_int : (Big_int.num * Big_int.num) -> Big_int.num
val lxor_int : (Big_int.num * Big_int.num) -> Big_int.num
val debug : (string * Big_int.num * string * bit list) -> unit
val eq_string : (Stdlib.String.t * Stdlib.String.t) -> bool
val string_startswith : (string * Stdlib.String.t) -> bool
val string_drop : (string * Big_int.num) -> string
val string_take : (string * Big_int.num) -> string
val string_length : string -> Big_int.num
val string_append : (string * string) -> string
val int_of_string_opt : string -> Big_int.num option
val maybe_int_of_prefix : string -> (Big_int.num * Big_int.num) zoption
val maybe_int_of_string : string -> Big_int.num zoption
val lt_int : (Big_int.num * Big_int.num) -> bool
val set_slice : (Big_int.num * 'a * 'b list * Big_int.num * 'b list) -> 'b list
val set_slice_int : (Big_int.num * Big_int.num * Big_int.num * bit list) -> Big_int.num
val eq_real : (Rational.t * Rational.t) -> bool
val lt_real : (Rational.t * Rational.t) -> bool
val gt_real : (Rational.t * Rational.t) -> bool
val lteq_real : (Rational.t * Rational.t) -> bool
val gteq_real : (Rational.t * Rational.t) -> bool
val to_real : Big_int.num -> Rational.t
val negate_real : Rational.t -> Rational.t
val string_of_real : Rational.t -> string
val print_real : (string * Rational.t) -> unit
val prerr_real : (string * Rational.t) -> unit
val quotient_real : (Rational.t * Rational.t) -> Rational.t
val div_real : (Rational.t * Rational.t) -> Rational.t
val mult_real : (Rational.t * Rational.t) -> Rational.t
val real_power : ('a * 'b) -> 'c
val int_power : (Big_int.num * Big_int.num) -> Big_int.num
val add_real : (Rational.t * Rational.t) -> Rational.t
val sub_real : (Rational.t * Rational.t) -> Rational.t
val abs_real : Rational.t -> Rational.t
val sqrt_real : Rational.t -> Rational.t
val random_real : unit -> Rational.t
val lt : (Big_int.num * Big_int.num) -> bool
val gt : (Big_int.num * Big_int.num) -> bool
val lteq : (Big_int.num * Big_int.num) -> bool
val gteq : (Big_int.num * Big_int.num) -> bool
val pow2 : Big_int.num -> Big_int.num
val max_int : (Big_int.num * Big_int.num) -> Big_int.num
val min_int : (Big_int.num * Big_int.num) -> Big_int.num
val abs_int : Big_int.num -> Big_int.num
val string_of_int : Big_int.num -> string
val undefined_real : unit -> Rational.t
val pow : int -> int -> int
val real_of_string : string -> Rational.t
val print : string -> unit
val prerr : string -> unit
val print_int : (string * Big_int.num) -> unit
val prerr_int : (string * Big_int.num) -> unit
val print_bits : (string * bit list) -> unit
val prerr_bits : (string * bit list) -> unit
val print_string : (string * string) -> unit
val prerr_string : (string * string) -> unit
val reg_deref : 'a Stdlib.ref -> 'a
val string_of_zbit : bit -> string
val string_of_znat : Big_int.num -> string
val string_of_zint : Big_int.num -> string
val string_of_zimplicit : Big_int.num -> string
val string_of_zunit : unit -> string
val string_of_zbool : bool -> string
val string_of_zreal : 'a -> string
val string_of_zstring : string -> string
val string_of_list : string -> ('a -> string) -> 'a list -> string
val skip : unit -> unit
val memea : ('a * 'b) -> unit
val zero_extend : (bit list * Big_int.num) -> bit list
val sign_extend : (bit list * Big_int.num) -> bit list
val zeros : Big_int.num -> bit list
val ones : Big_int.num -> bit list
val shift_bits_right_arith : ('a list * bit list) -> 'a list
val shiftr : (bit list * Big_int.num) -> bit list
val arith_shiftr : ('a list * Big_int.num) -> 'a list
val shift_bits_right : (bit list * bit list) -> bit list
val shiftl : (bit list * Big_int.num) -> bit list
val shift_bits_left : (bit list * bit list) -> bit list
val speculate_conditional_success : unit -> bool
val get_time_ns : unit -> Big_int.num
val hex_bits_1_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_2_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_3_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_4_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_5_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_6_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_7_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_8_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_9_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_10_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_11_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_12_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_13_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_14_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_15_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_16_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_17_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_18_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_19_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_20_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_21_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_22_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_23_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_24_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_25_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_26_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_27_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_28_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_29_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_30_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_31_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_32_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_33_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_48_matches_prefix : string -> (bit list * Big_int.num) zoption
val hex_bits_64_matches_prefix : string -> (bit list * Big_int.num) zoption
val string_of_bool : bool -> string
val dec_str : Big_int.num -> string
val hex_str : Big_int.num -> string
val trace_memory_write : ('a * 'b * 'c) -> unit
val trace_memory_read : ('a * 'b * 'c) -> unit
val sleep_request : unit -> unit
val load_raw : (bit list * string) -> unit
val cycle_count : unit -> unit
val rand_zvector : 'generators -> int -> bool -> ('generators -> 'a) -> 'a list
val rand_zbit : 'generators -> bit
val rand_zbool : 'generators -> bool
val rand_zunit : 'generators -> unit
val rand_choice : 'a list -> 'a
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct