package asli

  1. Overview
  2. Docs

Module LibASL.PrimopsSource

ASL primitive types and operations

Sourcemodule AST = Asl_ast

Boolean primops

Sourceval prim_eq_bool : bool -> bool -> bool
Sourceval prim_ne_bool : bool -> bool -> bool
Sourceval prim_and_bool : bool -> bool -> bool
Sourceval prim_or_bool : bool -> bool -> bool
Sourceval prim_equiv_bool : bool -> bool -> bool
Sourceval prim_not_bool : bool -> bool

Integer primops

Sourcetype bigint = Z.t
Sourceval prim_eq_int : bigint -> bigint -> bool
Sourceval prim_ne_int : bigint -> bigint -> bool
Sourceval prim_le_int : bigint -> bigint -> bool
Sourceval prim_lt_int : bigint -> bigint -> bool
Sourceval prim_ge_int : bigint -> bigint -> bool
Sourceval prim_gt_int : bigint -> bigint -> bool
Sourceval prim_is_pow2_int : bigint -> bool
Sourceval prim_neg_int : bigint -> bigint
Sourceval prim_add_int : bigint -> bigint -> bigint
Sourceval prim_sub_int : bigint -> bigint -> bigint
Sourceval prim_shl_int : bigint -> bigint -> bigint
Sourceval prim_shr_int : bigint -> bigint -> bigint
Sourceval prim_mul_int : bigint -> bigint -> bigint
Sourceval prim_zdiv_int : bigint -> bigint -> bigint
Sourceval prim_zrem_int : bigint -> bigint -> bigint
Sourceval prim_fdiv_int : bigint -> bigint -> bigint
Sourceval prim_frem_int : bigint -> bigint -> bigint
Sourceval prim_mod_pow2_int : bigint -> bigint -> bigint
Sourceval prim_align_int : bigint -> bigint -> bigint
Sourceval prim_pow2_int : bigint -> bigint
Sourceval prim_pow_int_int : bigint -> bigint -> bigint

Real primops

Sourcetype real = Q.t
Sourceval prim_cvt_int_real : bigint -> real
Sourceval prim_eq_real : real -> real -> bool
Sourceval prim_ne_real : real -> real -> bool
Sourceval prim_le_real : real -> real -> bool
Sourceval prim_lt_real : real -> real -> bool
Sourceval prim_ge_real : real -> real -> bool
Sourceval prim_gt_real : real -> real -> bool
Sourceval prim_neg_real : real -> real
Sourceval prim_add_real : real -> real -> real
Sourceval prim_sub_real : real -> real -> real
Sourceval prim_mul_real : real -> real -> real
Sourceval prim_div_real : real -> real -> real
Sourceval prim_pow2_real : bigint -> real
Sourceval prim_round_tozero_real : real -> bigint
Sourceval prim_round_down_real : real -> bigint
Sourceval prim_round_up_real : real -> bigint
Sourceval prim_sqrt_real : real -> real

Bitvector primops

Invariants:

  • the bigint part of a bitvector is positive
  • the bigint part of an N-bit bitvector is less than 2^N
Sourcetype bitvector = {
  1. n : int;
  2. v : Z.t;
}
Sourceval empty_bits : bitvector
Sourceval checked_extract : ('a -> 'b -> int -> Z.t) -> 'a -> 'b -> int -> Z.t
Sourceval z_extract : Z.t -> int -> int -> Z.t
Sourceval z_signed_extract : Z.t -> int -> int -> Z.t
Sourceval mkBits : int -> bigint -> bitvector
Sourceval mkBits2 : int -> int -> bigint -> bitvector
Sourceval prim_length_bits : bitvector -> int
Sourceval prim_cvt_int_bits : bigint -> bigint -> bitvector
Sourceval prim_cvt_bits_sint : bitvector -> bigint
Sourceval prim_cvt_bits_uint : bitvector -> bigint
Sourceval prim_eq_bits : bitvector -> bitvector -> bool
Sourceval prim_ne_bits : bitvector -> bitvector -> bool
Sourceval prim_add_bits : bitvector -> bitvector -> bitvector
Sourceval prim_sub_bits : bitvector -> bitvector -> bitvector
Sourceval prim_mul_bits : bitvector -> bitvector -> bitvector
Sourceval prim_and_bits : bitvector -> bitvector -> bitvector
Sourceval prim_or_bits : bitvector -> bitvector -> bitvector
Sourceval prim_eor_bits : bitvector -> bitvector -> bitvector
Sourceval prim_not_bits : bitvector -> bitvector
Sourceval prim_zeros_bits : bigint -> bitvector
Sourceval prim_ones_bits : bigint -> bitvector
Sourceval prim_append_bits : bitvector -> bitvector -> bitvector
Sourceval prim_replicate_bits : bitvector -> bigint -> bitvector
Sourceval prim_extract : bitvector -> bigint -> bigint -> bitvector
Sourceval prim_extract_int : Z.t -> bigint -> bigint -> bitvector
Sourceval prim_insert : bitvector -> bigint -> bigint -> bitvector -> bitvector

Mask primops

Sourcetype mask = {
  1. n : int;
  2. v : Z.t;
  3. m : Z.t;
}
Sourceval mkMask : int -> Z.t -> Z.t -> mask
Sourceval prim_in_mask : bitvector -> mask -> bool
Sourceval prim_notin_mask : bitvector -> mask -> bool

Exception primops

Sourcetype exc =
  1. | Exc_ConstrainedUnpredictable
  2. | Exc_ExceptionTaken
  3. | Exc_ImpDefined of string
  4. | Exc_SEE of string
  5. | Exc_Undefined
  6. | Exc_Unpredictable
Sourceval prim_is_cunpred_exc : exc -> bool
Sourceval prim_is_exctaken_exc : exc -> bool
Sourceval prim_is_impdef_exc : exc -> bool
Sourceval prim_is_see_exc : exc -> bool
Sourceval prim_is_undefined_exc : exc -> bool
Sourceval prim_is_unpred_exc : exc -> bool

String primops

Sourceval prim_eq_str : string -> string -> bool
Sourceval prim_ne_str : string -> string -> bool
Sourceval prim_append_str : string -> string -> string
Sourceval prim_cvt_int_hexstr : bigint -> string
Sourceval prim_cvt_int_decstr : bigint -> string
Sourceval prim_cvt_bool_str : bool -> string
Sourceval prim_cvt_bits_str : bigint -> bitvector -> string
Sourceval prim_cvt_real_str : real -> string

Immutable Array type

Sourcemodule Index : sig ... end
Sourcemodule ImmutableArray : sig ... end
Sourceval prim_empty_array : 'a ImmutableArray.t
Sourceval prim_read_array : 'a ImmutableArray.t -> int -> 'a -> 'a
Sourceval prim_write_array : 'a ImmutableArray.t -> int -> 'a -> 'a ImmutableArray.t

Mutable RAM type

RAM is implemented as a paged data structure and pages are allocated on demand and initialized with a specified default value.

Sourcemodule Pages : sig ... end
Sourcetype ram = {
  1. mutable contents : Bytes.t Pages.t;
  2. mutable default : char;
}
Sourceval logPageSize : int
Sourceval pageSize : int
Sourceval pageMask : Z.t
Sourceval pageIndexOfAddr : bigint -> bigint
Sourceval pageOffsetOfAddr : bigint -> bigint
Sourceval init_ram : char -> ram
Sourceval clear_ram : ram -> char -> unit
Sourceval readByte_ram : ram -> bigint -> char
Sourceval writeByte_ram : ram -> bigint -> char -> unit
Sourceval prim_init_ram : bigint -> bigint -> ram -> bitvector -> unit
Sourceval prim_read_ram : bigint -> bigint -> ram -> bigint -> bitvector
Sourceval prim_write_ram : bigint -> bigint -> ram -> bigint -> bitvector -> unit

File primops

These are not part of the official ASL language but they are useful when implementing the infrastructure needed in simulators.

Sourceval prim_open_file : string -> string -> bigint
Sourceval prim_write_file : bigint -> string -> unit
Sourceval prim_getc_file : bigint -> bigint
Sourceval prim_print_str : string -> unit
Sourceval prim_print_char : bigint -> unit

Trace primops

These are not part of the official ASL language but they are useful when implementing the infrastructure needed in simulators.

Sourceval prim_trace_memory_read : bigint -> bigint -> ram -> bigint -> bitvector -> unit
Sourceval prim_trace_memory_write : bigint -> bigint -> ram -> bigint -> bitvector -> unit
Sourceval prim_trace_event : string -> unit