Module Typed.Bitv128

include Bitv.S with type w = bitv128
type w = bitv128
type t = w expr
val ty : w ty
val zero : t

The bitvector value 0.

val one : t

The bitvector value 1.

val v : Bitvector.t -> t
val of_int : int -> t

of_int i creates a bitvector term from an integer i.

val symbol : Symbol.t -> t
val clz : t -> t

clz t counts the leading zeros in t.

val ctz : t -> t

ctz t counts the trailing zeros in t.

val popcnt : t -> t

popcnt t counts the number of set bits (population count) in t.

val neg : t -> t

neg t computes the two's complement negation of t.

val lognot : t -> t

lognot t computes the bitwise NOT of t.

val to_int : signed:bool -> int expr -> t

to_int ~signed t converts the bitvector t to an integer term. If signed is true, t is treated as a 2's complement signed value.

val add : t -> t -> t

add t1 t2 computes the bitwise addition t1 + t2.

val sub : t -> t -> t

sub t1 t2 computes the bitwise subtraction t1 - t2.

val mul : t -> t -> t

mul t1 t2 computes the bitwise multiplication t1 * t2.

val div : t -> t -> t

div t1 t2 is integer division.

val unsigned_div : t -> t -> t

unsigned_div t1 t2 is explicitly unsigned integer division.

val logor : t -> t -> t
val logand : t -> t -> t
val logxor : t -> t -> t
val shl : t -> t -> t

shl t amount shifts t left by amount bits.

val ashr : t -> t -> t

ashr t amount performs an arithmetic shift right (preserving sign).

val lshr : t -> t -> t

lshr t amount performs a logical shift right (inserting zeros).

val rem : t -> t -> t

rem t1 t2 computes the signed remainder of t1 / t2.

val unsigned_rem : t -> t -> t

unsigned_rem t1 t2 computes the unsigned remainder of t1 / t2.

val rotate_left : t -> t -> t

rotate_left t amount rotates the bits of t to the left by amount.

val rotate_right : t -> t -> t

rotate_right t amount rotates the bits of t to the right by amount.

val eq : t -> t -> bool expr

Alias for Bool.eq.

val ne : t -> t -> bool expr

Negation of eq.

val lt : t -> t -> bool expr

lt t1 t2 is signed less-than.

val lt_u : t -> t -> bool expr

lt_u t1 t2 is unsigned less-than.

val le : t -> t -> bool expr

le t1 t2 is signed less-than-or-equal.

val le_u : t -> t -> bool expr

le t1 t2 is unsigned less-than-or-equal.

val concat : 'a expr -> 'b expr -> 'c expr

concat t1 t2 concatenates t1 (high bits) and t2 (low bits).

Example: concat (v8 0xAA) (v8 0xBB) results in 0xAABB (16-bit).

val extract : t -> high:int -> low:int -> 'a expr

extract t ~high ~low extracts the bits from index high down tolow (inclusive).

Example:extract (i32 0xAABBCCDD) ~high:15 ~low:8 results in 0xCC (8-bit).

val zero_extend : int -> t -> 'a expr

zero_extend n t extends t to a width of width(t) + n by padding with zeros.

val sign_extend : int -> t -> 'a expr

sign_extend n t extends t to a width of width(t) + n by replicating the sign bit.

val to_bool : t -> bool expr

to_bool t returns true if t is non-zero, false otherwise.

val of_bool : bool expr -> t

of_bool b converts true to 1 and false to 0.

val pp : t Fmt.t
val of_i32x4 : bitv32 expr -> bitv32 expr -> bitv32 expr -> bitv32 expr -> t

of_i32x4 a b c d constructs a 128-bit vector from four 32-bit lanes.

val to_i32x4 : t -> bitv32 expr * bitv32 expr * bitv32 expr * bitv32 expr

to_i32x4 t splits the 128-bit vector into four 32-bit lanes.

of_int64x2 high low constructs a 128-bit vector from two 64-bit integers.

val of_i64x2 : bitv64 expr -> bitv64 expr -> t

of_i64x2 a b constructs a 128-bit vector from two 64-bit lanes.

val to_i64x2 : t -> bitv64 expr * bitv64 expr

to_i64x2 t splits the 128-bit vector into two 64-bit terms.