Primops (p.asli.0.2.0.doc.asli.libASL.LibASL.Primops)

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 = {

n : int;
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 = {

n : int;
v : Z.t;
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 =

| Exc_ConstrainedUnpredictable
| Exc_ExceptionTaken
| Exc_ImpDefined of string
| Exc_SEE of string
| Exc_Undefined
| 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 = {

mutable contents : Bytes.t Pages.t;
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.

Source

val prim_trace_memory_read : 
  bigint ->
  bigint ->
  ram ->
  bigint ->
  bitvector ->
  unit

Source

val prim_trace_memory_write : 
  bigint ->
  bigint ->
  ram ->
  bigint ->
  bitvector ->
  unit

Sourceval prim_trace_event : string -> unit