Module `LibASL.Primops`Source

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

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/asli.libASL/LibASL/Primops/index.html

Module `LibASL.Primops`Source

Boolean primops

Integer primops

Real primops

Bitvector primops

Mask primops

Exception primops

String primops

Immutable Array type

Mutable RAM type

File primops

Trace primops

package asli

Install

Dune Dependency

Authors

Maintainers

Sources

doc/asli.libASL/LibASL/Primops/index.html

Module LibASL.PrimopsSource

Boolean primops

Integer primops

Real primops

Bitvector primops

Mask primops

Exception primops

String primops

Immutable Array type

Mutable RAM type

File primops

Trace primops

Module `LibASL.Primops`Source