libsail 0.15 · OCaml Package

module Big_int = Nat_big_num

module type BitType = sig ... end

type 'a return = {

return : 'b. 'a -> 'b;

}

type 'za zoption =

| ZNone of unit
| 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 =

| B0
| 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 mult : (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 neg_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 round_down : Rational.t -> Big_int_impl.BI.big_int

val round_up : Rational.t -> Big_int_impl.BI.big_int

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 wakeup_request : unit -> unit

val reset_registers : 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_zbitvector : 'generators -> int -> bool -> bit list

val rand_zbool : 'generators -> bool

val rand_zunit : 'generators -> unit

val rand_choice : 'a list -> 'a

package libsail