Module Asllib.BitvectorSource

This module provide an interface to ASL bitvector, and main operations on it.

Sourcetype t

Represent a bitvector.

Sourceval length : t -> int

The length of the bitvector.

Constructors

Sourceval one : t

A length 1 bitvector with a 1 bit inside.

Sourceval zero : t

A length 1 bitvector with a 0 bit inside.

Sourceval empty : t

A length 0 bitvector.

Sourceval ones : int -> t

ones n is a bitvector of length n with every bit set.

Sourceval zeros : int -> t

zeros n is a bitvector of length n without any bit set.

Sourceval of_string : string -> t

of_string s interpretes s as a right-indexed representation of a bitvector. Characters others than '0' or '1' are ignored. The length of of_string s is equal to the number of such characters in s.

Sourceval of_int : int -> t

of_int i is the bitvector of length Sys.int_size (e.g. 63) that corresponds to i in little-endian, i.e. index 0 (for slicing operations corresponds to i mod 2.

Sourceval of_int_sized : int -> int -> t

of_int n i is the bitvector of length n that corresponds to i in little-endian, i.e. index 0 (for slicing operations corresponds to i mod 2.

Sourceval of_int64 : int64 -> t

of_int i is the bitvector of length 64 that corresponds to i in little-endian, i.e. index 0 (for slicing operations corresponds to i mod 2.

Sourceval of_z : int -> Z.t -> t

of_int sz i is the bitvector of length sz that corresponds to i in little-endian.

Exports

Sourceval pp_t : Format.formatter -> t -> unit

Print the bitvector, indexed from the right, as a serie of '0' and '1', delimited by apostrophes. Inside a horizontal box.

Sourceval to_string : t -> string

Returns a string representing the bitvector, indexed from the right and delimited by apostrophes.

Sourceval to_string_hexa : t -> string

Returns a string representing the bitvector in hexadecimal, indexed from the right and preceded by '0x'.

Sourceval to_int : t -> int

Returns an integer representing the bitvector, little-endian. Result unspecified if length > Sys.int_size.

Sourceval to_int_signed : t -> int

Returns a signed integer representing the bitvector.

Sourceval to_int64_unsigned : t -> int64

Returns an integer representing the bitvector, little-endian. Result unspecified if length > 64.

Sourceval to_int64_signed : t -> int64

Returns an integer representing the bitvector, little-endian. Result unspecified if length > 64.

Sourceval to_z_unsigned : t -> Z.t
Sourceval to_z_signed : t -> Z.t
Sourceval printable : t -> Z.t

Operations on bitvectors

Sourceval lognot : t -> t

Bitwise not operation.

Sourceval logand : t -> t -> t

Bitwise and operation.

Sourceval logor : t -> t -> t

Bitwise or operation.

Sourceval logxor : t -> t -> t

Bitwise xor operation.

Sourceval equal : t -> t -> bool

equal b1 b2 is true if and only if b1 and b2 are bitwise equal.

Sourceval compare : t -> t -> int

The comparison function for bitvectors, with the same specification as Stdlib.compare.

Sourceval sign_extend : int -> t -> t

sign_extend nbytes bv returns a copy of bv of length 8*nbytes, left-padded with bv's bit-sign.

Sourceval bitcount : t -> int

Returns the number of bits set to 1.

Sourceval highest_set_bit : t -> int

Returns the index of the highest set bit.

Sourceval prefix : t -> int -> t

prefix src len returns the prefix of size len of bitvector src. Will crash if len is strictly more then the size of src.

Sourceval extract_slice : t -> int list -> t

extract_slice src positions returns a bitvector whose i-th bit is the bit of src whose index is the i-th element of positions.

  • raises Invalid_argument

    if any index in positions is greater or equal to the length of src.

Sourceval write_slice : t -> t -> int list -> t

write_slice dst src positions is a copy of dst where each bit at index i in src has been written in dst at the index given by the i-th element of positions.

  • raises Invalid_argument

    if positions has not the same length as src, or any of the indexes in positions is greater than the length of dst.

Sourceval concat : t list -> t

concat [bv2; bv1; bv0] is the concatenation of bv0, bv1, and bv2, in this order, i.e. if bv0 is not empty, the following is true:

equal (extract_slice (concat [bv1; bv0]) [ 0 ]) (extract_slice bv0 [ 0 ])
Sourceval is_zeros : t -> bool

is_zeros bv is true if every bit of bv is unset.

Sourceval is_ones : t -> bool

is_ones bv is true if every bit of bv is set.

Bitvector masks

Bitvector in ASL can be matched against masks, that have the same syntax than bitvectors, with an extra possible bit: 'x'. This bits indicates that the mask would match against any bit at this position.

For example:

  assert ('01' IN {'01'}) == TRUE;
  assert ('01' IN {'0x'}) == TRUE;
  assert ('10' IN {'0x'}) == FALSE;
Sourcetype mask

Internal representation of a mask.

Sourceval mask_length : mask -> int

Returns the length of bitvectors matched by this mask.

Sourceval mask_of_string : string -> mask

Build a mask from its ASL representation.

Sourceval mask_of_bitvector : t -> mask

Build a mask that matches a bitvector.

Sourceval matches : t -> mask -> bool

matches mask bv is true iff bv matches mask.

Sourceval mask_to_string : mask -> string

Returns an ASL string matching its value.

Sourceval mask_to_canonical_string : mask -> string

Returns a unique ASL string matching its value.

Sourceval mask_set : mask -> t

mask_set m's set bits are those required set by m.

Sourceval mask_unset : mask -> t

mask_unset m's set bits are those required unset by m.

Sourceval mask_specified : mask -> t

mask_specified m's set bits are those require set or unset by m.