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 ref
val trace_depth : int ref
val random : bool ref
val opt_cycle_limit : int 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 : Bytes.t Mem.t 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 -> 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 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 : (String.t * String.t) -> bool
val string_startswith : (string * 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 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