package libsail

  1. Overview
  2. Docs
Sail is a language for describing the instruction semantics of processors

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (6)

Authors

  1. A
    Alasdair Armstrong
  2. T
    Thomas Bauereiss
  3. B
    Brian Campbell
  4. S
    Shaked Flur
  5. J
    Jonathan French
  6. K
    Kathy Gray
  7. R
    Robert Norton
  8. C
    Christopher Pulte
  9. P
    Peter Sewell
  10. M
    Mark Wassell

Maintainers

  1. S
    Sail Devs <cl-sail-dev@lists.cam.ac.uk>

Sources

sail-0.18.tbz
sha256=fcdbda14f1ed59fa30e23da34abe02547416e3c2a83fbeee5606e100a5edcf35
sha512=0bbd72706cb4c1ddf13ea1c42004ec498aa9db8a301020f0dd3d8ac582d1bed8a48c7a825b8e3e6f629279f1f900384f6966608e1cd59e7b1217776413c7fa27

doc/libsail/Libsail/Sail2_values/index.html

Module Libsail.Sail2_valuesSource

Sourcetype ('a, 'b) result =
  1. | Ok of 'a
  2. | Err of 'b
Sourcetype ii = Nat_big_num.num
Sourcetype nn = Nat_big_num.num
Sourceval nat_of_int : Nat_big_num.num -> int
Sourceval pow : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
Sourceval pow2 : Nat_big_num.num -> Nat_big_num.num
Sourceval prerr : string -> unit
Sourceval print_int : string -> Nat_big_num.num -> unit
Sourceval prerr_int : string -> Nat_big_num.num -> unit
Sourceval shr_int : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
Sourceval shl_int : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
Sourceval align_int : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
Sourceval take_list : Nat_big_num.num -> 'a list -> 'a list
Sourceval drop_list : Nat_big_num.num -> 'a list -> 'a list
Sourceval repeat : 'a list -> Nat_big_num.num -> 'a list
Sourceval duplicate_to_list : 'a -> Nat_big_num.num -> 'a list
Sourceval vector_init : Nat_big_num.num -> 'a -> 'a list
Sourceval replace : 'a list -> Nat_big_num.num -> 'a -> 'a list
Sourceval upper : 'a -> 'a
Sourceval tmod_int : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
Sourceval hardware_mod : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
Sourceval tdiv_int : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
Sourceval hardware_quot : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num
Sourceval max_64u : Nat_big_num.num
Sourceval max_64 : Nat_big_num.num
Sourceval min_64 : Nat_big_num.num
Sourceval max_32u : Nat_big_num.num
Sourceval max_32 : Nat_big_num.num
Sourceval min_32 : Nat_big_num.num
Sourceval max_8 : Nat_big_num.num
Sourceval min_8 : Nat_big_num.num
Sourceval max_5 : Nat_big_num.num
Sourceval min_5 : Nat_big_num.num
Sourceval just_list : 'a option list -> 'a list option
Sourceval maybe_failwith : 'a option -> 'a
Sourcetype bitU =
  1. | B0
  2. | B1
  3. | BU
Sourceval showBitU : bitU -> string
Sourceval bitU_char : bitU -> char
Sourceval instance_Show_Show_Sail2_values_bitU_dict : bitU Lem_pervasives_extra.show_class
Sourceval compare_bitU : bitU -> bitU -> int
Sourceval instance_Basic_classes_Ord_Sail2_values_bitU_dict : bitU Lem_pervasives_extra.ord_class
Sourcetype 'a bitU_class = {
  1. to_bitU_method : 'a -> bitU;
  2. of_bitU_method : bitU -> 'a;
}
Sourceval instance_Sail2_values_BitU_Sail2_values_bitU_dict : bitU bitU_class
Sourceval bool_of_bitU : bitU -> bool option
Sourceval bitU_of_bool : bool -> bitU
Sourceval cast_bit_bool : bitU -> bool option
Sourceval not_bit : bitU -> bitU
Sourceval is_one : Nat_big_num.num -> bitU
Sourceval and_bit : bitU -> bitU -> bitU
Sourceval or_bit : bitU -> bitU -> bitU
Sourceval xor_bit : bitU -> bitU -> bitU
Sourceval bools_of_nat_aux : Nat_big_num.num -> Nat_big_num.num -> bool list -> bool list
Sourceval bools_of_nat : Nat_big_num.num -> Nat_big_num.num -> bool list
Sourceval nat_of_bools_aux : Nat_big_num.num -> bool list -> Nat_big_num.num
Sourceval nat_of_bools : bool list -> Nat_big_num.num
Sourceval unsigned_of_bools : bool list -> Nat_big_num.num
Sourceval signed_of_bools : bool list -> Nat_big_num.num
Sourceval int_of_bools : bool -> bool list -> Nat_big_num.num
Sourceval pad_list : 'a -> 'a list -> Nat_big_num.num -> 'a list
Sourceval ext_list : 'a -> Nat_big_num.num -> 'a list -> 'a list
Sourceval extz_bools : Nat_big_num.num -> bool list -> bool list
Sourceval exts_bools : Nat_big_num.num -> bool list -> bool list
Sourceval add_one_bool_ignore_overflow_aux : bool list -> bool list
Sourceval add_one_bool_ignore_overflow : bool list -> bool list
Sourceval bools_of_int : Nat_big_num.num -> Nat_big_num.num -> bool list
Sourceval has_undefined_bits : bitU list -> bool
Sourceval bits_of_nat : Nat_big_num.num -> Nat_big_num.num -> bitU list
Sourceval nat_of_bits : bitU list -> Nat_big_num.num option
Sourceval not_bits : bitU list -> bitU list
Sourceval binop_list : ('b -> 'c -> 'a) -> 'b list -> 'c list -> 'a list
Sourceval unsigned_of_bits : bitU list -> Nat_big_num.num option
Sourceval signed_of_bits : bitU list -> Nat_big_num.num option
Sourceval int_of_bits : bool -> bitU list -> Nat_big_num.num option
Sourceval extz_bits : Nat_big_num.num -> bitU list -> bitU list
Sourceval exts_bits : Nat_big_num.num -> bitU list -> bitU list
Sourceval add_one_bit_ignore_overflow_aux : bitU list -> bitU list
Sourceval add_one_bit_ignore_overflow : bitU list -> bitU list
Sourceval bits_of_int : Nat_big_num.num -> Nat_big_num.num -> bitU list
Sourceval arith_op_bits : (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) -> bool -> bitU list -> bitU list -> bitU list
Sourceval char_of_nibble : (bitU * bitU * bitU * bitU) -> char option
Sourceval nibble_of_char : char -> (bitU * bitU * bitU * bitU) option
Sourceval hexstring_of_bits : bitU list -> char list option
Sourceval show_bitlist_prefix : char -> bitU list -> string
Sourceval show_bitlist : bitU list -> string
Sourceval hex_char : Nat_big_num.num -> char
Sourceval hex_str_aux : Nat_big_num.num -> char list -> char list
Sourceval hex_str : Nat_big_num.num -> string
Sourceval hex_str_upper : Nat_big_num.num -> string
Sourceval subrange_list_inc : 'a list -> Nat_big_num.num -> Nat_big_num.num -> 'a list
Sourceval subrange_list_dec : 'a list -> Nat_big_num.num -> Nat_big_num.num -> 'a list
Sourceval subrange_list : bool -> 'a list -> Nat_big_num.num -> Nat_big_num.num -> 'a list
Sourceval update_subrange_list_inc : 'a list -> Nat_big_num.num -> Nat_big_num.num -> 'a list -> 'a list
Sourceval update_subrange_list_dec : 'a list -> Nat_big_num.num -> Nat_big_num.num -> 'a list -> 'a list
Sourceval update_subrange_list : bool -> 'a list -> Nat_big_num.num -> Nat_big_num.num -> 'a list -> 'a list
Sourceval access_list_inc : 'a list -> Nat_big_num.num -> 'a
Sourceval access_list_dec : 'a list -> Nat_big_num.num -> 'a
Sourceval access_list : bool -> 'a list -> Nat_big_num.num -> 'a
Sourceval update_list_inc : 'a list -> Nat_big_num.num -> 'a -> 'a list
Sourceval update_list_dec : 'a list -> Nat_big_num.num -> 'a -> 'a list
Sourceval update_list : bool -> 'a list -> Nat_big_num.num -> 'a -> 'a list
Sourceval extract_only_bit : bitU list -> bitU
Sourceval slice_mword_dec : ('a * Big_int_impl.BI.big_int) -> Nat_big_num.num -> Nat_big_num.num -> Lem.mword
Sourceval slice_mword_inc : (int * Big_int_impl.BI.big_int) -> Nat_big_num.num -> Nat_big_num.num -> Lem.mword
Sourceval slice_mword : bool -> (int * Big_int_impl.BI.big_int) -> Nat_big_num.num -> Nat_big_num.num -> Lem.mword
Sourceval 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
Sourceval 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
Sourceval 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
Sourceval access_mword_dec : ('a * Big_int_impl.BI.big_int) -> Nat_big_num.num -> bitU
Sourceval access_mword_inc : (int * Big_int_impl.BI.big_int) -> Nat_big_num.num -> bitU
Sourceval access_mword : bool -> (int * Big_int_impl.BI.big_int) -> Nat_big_num.num -> bitU
Sourceval update_mword_bool_dec : (int * Nat_big_num.num) -> Nat_big_num.num -> bool -> Lem.mword
Sourceval update_mword_dec : (int * Nat_big_num.num) -> Nat_big_num.num -> bitU -> Lem.mword option
Sourceval update_mword_bool_inc : (int * Nat_big_num.num) -> Nat_big_num.num -> bool -> Lem.mword
Sourceval update_mword_inc : (int * Nat_big_num.num) -> Nat_big_num.num -> bitU -> Lem.mword option
Sourceval int_of_mword : bool -> (int * Big_int_impl.BI.big_int) -> Nat_big_num.num
Sourceval size_itself_int : 'a Lem_machine_word.size_class -> 'b -> Nat_big_num.num
Sourceval make_the_value : 'a -> unit
Sourcetype 'a bitvector_class = {
  1. bits_of_method : 'a -> bitU list;
  2. of_bits_method : bitU list -> 'a option;
  3. of_bools_method : bool list -> 'a;
  4. length_method : 'a -> Nat_big_num.num;
  5. of_int_method : Nat_big_num.num -> Nat_big_num.num -> 'a;
  6. unsigned_method : 'a -> Nat_big_num.num option;
  7. signed_method : 'a -> Nat_big_num.num option;
  8. arith_op_bv_method : (Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num) -> bool -> 'a -> 'a -> 'a;
}
Sourceval of_bits_failwith : 'a bitvector_class -> bitU list -> 'a
Sourceval int_of_bv : 'a bitvector_class -> bool -> 'a -> Nat_big_num.num option
Sourceval instance_Sail2_values_Bitvector_list_dict : 'a bitU_class -> 'a list bitvector_class
Sourceval instance_Sail2_values_Bitvector_Machine_word_mword_dict : 'a Lem_machine_word.size_class -> Lem.mword bitvector_class
Sourceval access_bv_inc : 'a bitvector_class -> 'a -> Nat_big_num.num -> bitU
Sourceval access_bv_dec : 'a bitvector_class -> 'a -> Nat_big_num.num -> bitU
Sourceval update_bv_inc : 'a bitvector_class -> 'a -> Nat_big_num.num -> bitU -> bitU list
Sourceval update_bv_dec : 'a bitvector_class -> 'a -> Nat_big_num.num -> bitU -> bitU list
Sourceval subrange_bv_inc : 'a bitvector_class -> 'a -> Nat_big_num.num -> Nat_big_num.num -> bitU list
Sourceval subrange_bv_dec : 'a bitvector_class -> 'a -> Nat_big_num.num -> Nat_big_num.num -> bitU list
Sourceval update_subrange_bv_inc : 'a bitvector_class -> 'b bitvector_class -> 'b -> Nat_big_num.num -> Nat_big_num.num -> 'a -> bitU list
Sourceval update_subrange_bv_dec : 'a bitvector_class -> 'b bitvector_class -> 'b -> Nat_big_num.num -> Nat_big_num.num -> 'a -> bitU list
Sourceval extz_bv : 'a bitvector_class -> Nat_big_num.num -> 'a -> bitU list
Sourceval exts_bv : 'a bitvector_class -> Nat_big_num.num -> 'a -> bitU list
Sourceval nat_of_bv : 'a bitvector_class -> 'a -> int option
Sourceval string_of_bv : 'a bitvector_class -> 'a -> string
Sourceval string_of_bv_subrange : 'a bitvector_class -> 'a -> Nat_big_num.num -> Nat_big_num.num -> string
Sourceval print_bits : 'a bitvector_class -> string -> 'a -> unit
Sourceval prerr_bits : 'a bitvector_class -> string -> 'a -> unit
Sourceval dec_str : Nat_big_num.num -> string
Sourceval concat_str : string -> string -> string
Sourceval int_of_bit : bitU -> Nat_big_num.num
Sourceval count_leading_zero_bits : bitU list -> Nat_big_num.num
Sourceval count_leading_zeros_bv : 'a bitvector_class -> 'a -> Nat_big_num.num
Sourceval decimal_string_of_bv : 'a bitvector_class -> 'a -> string
Sourceval align_bits : 'a bitvector_class -> 'a -> Nat_big_num.num -> 'a
Sourcetype memory_byte = bitU list
Sourceval byte_chunks : 'a list -> 'a list list option
Sourceval bytes_of_bits : 'a bitvector_class -> 'a -> bitU list list option
Sourceval bits_of_bytes : bitU list list -> bitU list
Sourceval mem_bytes_of_bits : 'a bitvector_class -> 'a -> bitU list list option
Sourceval bits_of_mem_bytes : bitU list list -> bitU list
Sourceval reverse_endianness_list : 'a list -> 'a list
Sourcetype 'rv register_Value_class = {
  1. bool_of_regval_method : 'rv -> bool option;
  2. regval_of_bool_method : bool -> 'rv;
  3. int_of_regval_method : 'rv -> Nat_big_num.num option;
  4. regval_of_int_method : Nat_big_num.num -> 'rv;
  5. real_of_regval_method : 'rv -> float option;
  6. regval_of_real_method : float -> 'rv;
  7. string_of_regval_method : 'rv -> string option;
  8. regval_of_string_method : string -> 'rv;
}
Sourcetype ('regstate, 'regval, 'a) register_ref = {
  1. name : string;
  2. read_from : 'regstate -> 'a;
  3. write_to : 'a -> 'regstate -> 'regstate;
  4. of_regval : 'regval -> 'a option;
  5. regval_of : 'a -> 'regval;
}
Sourcetype ('regstate, 'regval) register_ops = ('regval -> bool) * ('regstate -> 'regval) * ('regval -> 'regstate -> 'regstate option)
Sourceval register_ops_of : ('st, 'regval, 'a) register_ref -> ('regval -> bool) * ('st -> 'regval) * ('regval -> 'st -> 'st option)
Sourcetype ('regstate, 'regval) register_accessors = (string -> 'regstate -> 'regval option) * (string -> 'regval -> 'regstate -> 'regstate option)
Sourceval mk_accessors : (string -> ('a * ('st -> 'v) * ('v -> 'st -> 'st option)) option) -> (string -> 'st -> 'v option) * (string -> 'v -> 'st -> 'st option)
Sourcetype ('regtype, 'a) field_ref = {
  1. field_name : string;
  2. field_start : Nat_big_num.num;
  3. field_is_inc : bool;
  4. get_field : 'regtype -> 'a;
  5. set_field : 'regtype -> 'a -> 'regtype;
}
Sourceval foreach : 'a list -> 'vars -> ('a -> 'vars -> 'vars) -> 'vars
Sourceval index_list : Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num -> Nat_big_num.num list
Sourceval while0 : 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
Sourceval until : 'vars -> ('vars -> bool) -> ('vars -> 'vars) -> 'vars
Sourcetype 'a toNatural_class = {
  1. toNatural_method : 'a -> Nat_big_num.num;
}
Sourceval instance_Sail2_values_ToNatural_Num_integer_dict : Nat_big_num.num toNatural_class
Sourceval instance_Sail2_values_ToNatural_Num_int_dict : int toNatural_class
Sourceval instance_Sail2_values_ToNatural_nat_dict : int toNatural_class
Sourceval instance_Sail2_values_ToNatural_Num_natural_dict : Nat_big_num.num toNatural_class
Sourceval 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
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