asli 0.2.0 (latest) · OCaml Package

ASL primitive types and operations

module AST = Asl_ast

Boolean primops

val prim_eq_bool : bool -> bool -> bool

val prim_ne_bool : bool -> bool -> bool

val prim_and_bool : bool -> bool -> bool

val prim_or_bool : bool -> bool -> bool

val prim_equiv_bool : bool -> bool -> bool

val prim_not_bool : bool -> bool

Integer primops

type bigint = Z.t

val prim_eq_int : bigint -> bigint -> bool

val prim_ne_int : bigint -> bigint -> bool

val prim_le_int : bigint -> bigint -> bool

val prim_lt_int : bigint -> bigint -> bool

val prim_ge_int : bigint -> bigint -> bool

val prim_gt_int : bigint -> bigint -> bool

val prim_is_pow2_int : bigint -> bool

val prim_neg_int : bigint -> bigint

val prim_add_int : bigint -> bigint -> bigint

val prim_sub_int : bigint -> bigint -> bigint

val prim_shl_int : bigint -> bigint -> bigint

val prim_shr_int : bigint -> bigint -> bigint

val prim_mul_int : bigint -> bigint -> bigint

val prim_zdiv_int : bigint -> bigint -> bigint

val prim_zrem_int : bigint -> bigint -> bigint

val prim_fdiv_int : bigint -> bigint -> bigint

val prim_frem_int : bigint -> bigint -> bigint

val prim_mod_pow2_int : bigint -> bigint -> bigint

val prim_align_int : bigint -> bigint -> bigint

val prim_pow2_int : bigint -> bigint

val prim_pow_int_int : bigint -> bigint -> bigint

Real primops

type real = Q.t

val prim_cvt_int_real : bigint -> real

val prim_eq_real : real -> real -> bool

val prim_ne_real : real -> real -> bool

val prim_le_real : real -> real -> bool

val prim_lt_real : real -> real -> bool

val prim_ge_real : real -> real -> bool

val prim_gt_real : real -> real -> bool

val prim_neg_real : real -> real

val prim_add_real : real -> real -> real

val prim_sub_real : real -> real -> real

val prim_mul_real : real -> real -> real

val prim_div_real : real -> real -> real

val prim_pow2_real : bigint -> real

val prim_round_tozero_real : real -> bigint

val prim_round_down_real : real -> bigint

val prim_round_up_real : real -> bigint

val 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

type bitvector = {

n : int;
v : Z.t;

}

val empty_bits : bitvector

val checked_extract : ('a -> 'b -> int -> Z.t) -> 'c -> 'd -> int -> Z.t

val z_extract : Z.t -> int -> int -> Z.t

val z_signed_extract : Z.t -> int -> int -> Z.t

val mkBits : int -> bigint -> bitvector

val mkBits2 : int -> int -> bigint -> bitvector

val prim_length_bits : bitvector -> int

val prim_cvt_int_bits : bigint -> bigint -> bitvector

val prim_cvt_bits_sint : bitvector -> bigint

val prim_cvt_bits_uint : bitvector -> bigint

val prim_eq_bits : bitvector -> bitvector -> bool

val prim_ne_bits : bitvector -> bitvector -> bool

val prim_add_bits : bitvector -> bitvector -> bitvector

val prim_sub_bits : bitvector -> bitvector -> bitvector

val prim_mul_bits : bitvector -> bitvector -> bitvector

val prim_and_bits : bitvector -> bitvector -> bitvector

val prim_or_bits : bitvector -> bitvector -> bitvector

val prim_eor_bits : bitvector -> bitvector -> bitvector

val prim_not_bits : bitvector -> bitvector

val prim_zeros_bits : bigint -> bitvector

val prim_ones_bits : bigint -> bitvector

val prim_append_bits : bitvector -> bitvector -> bitvector

val prim_replicate_bits : bitvector -> bigint -> bitvector

val prim_extract : bitvector -> bigint -> bigint -> bitvector

val prim_extract_int : Z.t -> bigint -> bigint -> bitvector

val prim_insert : bitvector -> bigint -> bigint -> bitvector -> bitvector

Mask primops

type mask = {

n : int;
v : Z.t;
m : Z.t;

}

val mkMask : int -> Z.t -> Z.t -> mask

val prim_in_mask : bitvector -> mask -> bool

val prim_notin_mask : bitvector -> mask -> bool

Exception primops

type exc =

| Exc_ConstrainedUnpredictable
| Exc_ExceptionTaken
| Exc_ImpDefined of string
| Exc_SEE of string
| Exc_Undefined
| Exc_Unpredictable

val prim_is_cunpred_exc : exc -> bool

val prim_is_exctaken_exc : exc -> bool

val prim_is_impdef_exc : exc -> bool

val prim_is_see_exc : exc -> bool

val prim_is_undefined_exc : exc -> bool

val prim_is_unpred_exc : exc -> bool

String primops

val prim_eq_str : string -> string -> bool

val prim_ne_str : string -> string -> bool

val prim_append_str : string -> string -> string

val prim_cvt_int_hexstr : bigint -> string

val prim_cvt_int_decstr : bigint -> string

val prim_cvt_bool_str : bool -> string

val prim_cvt_bits_str : bigint -> bitvector -> string

val prim_cvt_real_str : real -> string

Immutable Array type

module Index : sig ... end

module ImmutableArray : sig ... end

val prim_empty_array : 'a ImmutableArray.t

val prim_read_array : 'a ImmutableArray.t -> int -> 'a0 -> 'a1

val prim_write_array : 
  'a ImmutableArray.t ->
  int ->
  'a0 ->
  'a1 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.

module Pages : sig ... end

type ram = {

mutable contents : Bytes.t Pages.t;
mutable default : char;

}

val logPageSize : int

val pageSize : int

val pageMask : Z.t

val pageIndexOfAddr : bigint -> bigint

val pageOffsetOfAddr : bigint -> bigint

val init_ram : char -> ram

val clear_ram : ram -> char -> unit

val readByte_ram : ram -> bigint -> char

val writeByte_ram : ram -> bigint -> char -> unit

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

val prim_read_ram : bigint -> bigint -> ram -> bigint -> bitvector

val 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.

val prim_open_file : string -> string -> bigint

val prim_write_file : bigint -> string -> unit

val prim_getc_file : bigint -> bigint

val prim_print_str : string -> unit

val prim_print_char : bigint -> unit

Trace primops