Bitvec (bitvec.Bitvec)

type t

abstract representation of a fixed size bitvector

type 'a m

a computation in some modulo

type modulus

type denoting the arithmetic modulus

val modulus : int -> modulus

modulus s is the modulus of bitvectors with size s.

This is a number $2^s-1$, also known as a Mersenne number.

val m1 : modulus

m1 = modulus 1 = $1$ is the modulus of bitvectors with size 1

val m8 : modulus

m8 = modulus 8 = $255$ is the modulus of bitvectors with size 8

val m16 : modulus

m16 = modulus 16 = $65535$ is the modulus of bitvectors with size 16

since 2.5.0

val m32 : modulus

m32 = modulus 32 = $2^32-1$ is the modulus of bitvectors with size 32

val m64 : modulus

m64 = modulus 64 = $2^64-1$ is the modulus of bitvectors with size 64

val (mod) : 'a m -> modulus -> 'a

(x <op> y) mod m applies operation <op> modulo m.

Example: (x + y) mod m returns the sum of x and y modulo m.

Note: the mod function is declared as a primitive to enable support for inlining in non flambda versions of OCaml. Indeed, underneath the hood the 'a m type is defined as the reader monad modulus -> 'a, however we don't want to create a closure every time we compute an operation over bitvectors. With this trick, all versions of OCaml no matter the optimization options will inline (x+y) mod m and won't create any closures, even if m is not known at compile time.

module type S = sig ... end

val compare : t -> t -> int

compare x y compares x and y as unsigned integers, i.e., compare x y = compare (to_nat x) (to_nat y)

val equal : t -> t -> bool

equal x y is true if x and y represent the same integers

val (<) : t -> t -> bool

x < y iff compare x y = -1

val (>) : t -> t -> bool

x < y iff compare x y = -1

x > y iff compare x y = 1

val (=) : t -> t -> bool

x > y iff compare x y = 1

x = y iff compare x y = 0

val (<>) : t -> t -> bool

x = y iff compare x y = 0

x <> y iff compare x y <> 0

val (<=) : t -> t -> bool

x <> y iff compare x y <> 0

x <= y iff compare x y <= 0

val (>=) : t -> t -> bool

x <= y iff compare x y <= 0

x >= y iff compare x y >= 0

val hash : t -> int

hash x returns such z that forall y s.t. x=y, hash y = z

val pp : Stdlib.Format.formatter -> t -> unit

pp ppf x is a pretty printer for the bitvectors.

Could be used standalone or as an argument to the %a format specificator, e.g.,

Format.fprintf "0xBEEF != %a" Bitvec.pp !$"0xBEAF"

val to_binary : t -> string

to_binary x returns a canonical binary representation of x

val of_binary : string -> t

of_binary s returns a bitvector x s.t. to_binary x = s.

val to_string : t -> string

to_string x returns a textual (human readable) representation of the bitvector x.

val of_string : string -> t

of_string s returns a bitvector that corresponds to s.

The set of accepted strings is defined by the following EBNF grammar:

       valid-numbers ::=
        | "0b", bin-digit, {bin-digit}
        | "0o", oct-digit, {oct-digit}
        | "0x", hex-digit, {hex-digit}
        | dec-digit, {dec-digit}

      bin-digit ::= '0' | '1'
      oct-digit ::= '0'-'7'
      dec-digit ::= '0'-'9'
      hex-digit ::= '0'-'9' |'a'-'f'|'A'-'F'

raises Invalid_argument
if the string s is not recognized as valid-numbers.

val bigint_unsafe : Z.t -> t

bigint_unsafe x directly interprets a zarith value as bitvector.

The function is safe only if x is the result of to_bigint, otherwise the resulting value is unpredictable.

since 2.5.0

val of_substring : ?pos:int -> ?len:int -> string -> t

of_substring ~pos ~len s is a bitvector that corresponds to a substring of s designated by the start position pos and length len.

The result is the same as of_string (String.sub s pos len), except that no intermediate substring is created.

parameter pos
is the starting position of the substring (defaults to 0)

parameter len
is the length of the substring (defaults to the length of s.

raises Invalid_argument
if pos and len together do not define a valid substring of s or if the substring is not a sequence of numbers of the base b.

val of_string_base : int -> string -> t

of_string_base b x is a bitvector that corresponds to s represented in base b.

The base b must be between 2 and 16. The textual representation shall not contain a prefix that designates the base and must be a sequence of digits that are less than b.

Examples

Valid inputs:

of_string_base 16 "DEADBEEF";
of_string_base 2 "010110";
of_string_base 11 "AAAAAA".

Invalid inputs:

of_string_base 16 "0xDEADBEEF";
of_string_base 2 "-010100";
of_string_base 10 "AAAAA".

val of_substring_base : ?pos:int -> ?len:int -> int -> string -> t

of_substring_base b x is a bitvector that corresponds to a substring of s designated by the start position pos and length len that is a sequence of digits in base b.

The result is the same as of_string_base b x (String.sub s pos len), except that no intermediate substring is created.

parameter pos
is the starting position of the substring (default to 0)

parameter len
is the length of the substring (defaults to the length of s.

raises Invalid_argument
if pos and len together do not define a valid substring of s or if the substring is not a sequence of numbers of the base b.

val fits_int : t -> bool

fits_int x is true if x could be represented with the OCaml int type.

Note: it is not always true that fits_int (int x mod m), since depending on m a negative number might not fit into the OCaml representation. For positive numbers it is true, however.

val to_int : t -> int

to_int x returns an OCaml integer that has the same representation as x.

The function is undefined if not (fits_int x).

val fits_int32 : t -> bool

fits_int32 x is true if x could be represented with the OCaml int type.

Note: it is not always true that fits_int32 (int32 x mod m), since depending on m the negative x may not fit back into the int32 representation. For positive numbers it is true, however.

val to_int32 : t -> int32

to_int32 x returns an OCaml integer that has the same representation as x.

The function is undefined if not (fits_int32 x).

val fits_int64 : t -> bool

fits_int64 x is true if x could be represented with the OCaml int type.

Note: it is not always true that fits_int64 (int64 x mod m), since depending on m the negative x might not fit back into the int64 representation. For positive numbers it is true, however.

val to_int64 : t -> int64

to_int64 x returns an OCaml integer that has the same representation as x.

The function is undefined if not (fits_int64 x).

val to_bigint : t -> Z.t

to_bigint x returns a natural number that corresponds to x.

The returned value is always positive.

val extract : hi:int -> lo:int -> t -> t

extract ~hi ~lo x extracts bits from lo to hi.

The operation is effectively equivalent to (x lsr lo) mod (hi-lo+1)

val select : int list -> t -> t

select bits x builds a bitvector from bits of x.

Returns a bitvector y such that nth bit of it is equal to List.nth bits n bit of x.

Returns zero if bits are empty.

val append : int -> int -> t -> t -> t

append m n x y takes m bits of x and n bits of y and returns their concatenation. The result has m+n bits.

Examples:

append 16 16 !$"0xdead" !$"0xbeef" = !$"0xdeadbeef";
append 12 20 !$"0xbadadd" !$"0xbadbeef" = !$"0xadddbeef";;

val repeat : int -> times:int -> t -> t

repeat m ~times:n x repeats m bits of x n times.

The result has m*n bits.

val concat : int -> t list -> t

concat m xs concatenates m bits of each x in xs.

The operation is the reduction of the append operation with m=n. The result has m * List.length xs bits and is equal to 0 if xs is empty.

include S with type 'a m := 'a m

val bool : bool -> t

bool x returns one if x and zero otherwise.

val int : int -> t m

int n mod m is n modulo m.

val int32 : int32 -> t m

int32 n mod m is n modulo m.

val int64 : int64 -> t m

int64 n mod m is n modulo m.

val bigint : Z.t -> t m

bigint n mod m is n modulo m.

val zero : t

zero is 0.

val one : t

one is 1.

val ones : t m

ones mod m is a bitvector of size m with all bits set

val succ : t -> t m

succ x mod m is the successor of x modulo m

val nsucc : t -> int -> t m

nsucc x n mod m is the nth successor of x modulo m

val pred : t -> t m

pred x mod m is the predecessor of x modulo m

val npred : t -> int -> t m

npred x n mod m is the nth predecessor of x modulo m

val neg : t -> t m

neg x mod m is the 2-complement of x modulo m.

val lnot : t -> t m

lnot x is the 1-complement of x modulo m.

val abs : t -> t m

abs x mod m absolute value of x modulo m.

The absolute value of x is equal to neg x if msb x and to x otherwise.

val add : t -> t -> t m

add x y mod m is x + y modulo m

val sub : t -> t -> t m

sub x y mod m is x - y modulo m

val mul : t -> t -> t m

mul x y mod m is x * y modulo m

val div : t -> t -> t m

div x y mod m is x / y modulo m,

where / is the truncating towards zero division, that returns ones m if y = 0.

val sdiv : t -> t -> t m

sdiv x y mod m is signed division of x by y modulo m,

The signed division operator is defined in terms of the div operator as follows:

                        /
                        | div x y mod m : if not mx /\ not my
                        | neg (div (neg x) y) mod m if mx /\ not my
      x sdiv y mod m = <
                        | neg (div x (neg y)) mod m if not mx /\ my
                        | div (neg x) (neg y) mod m if mx /\ my
                        \

      where mx = msb x mod m,
        and my = msb y mod m.

val rem : t -> t -> t m

rem x y mod m is the remainder of x / y modulo m.

val srem : t -> t -> t m

srem x y mod m is the signed remainder x / y modulo m.

This version of the signed remainder where the sign follows the dividend, and is defined via the rem operation as follows

                        /
                        | rem x y mod m : if not mx /\ not my
                        | neg (rem (neg x) y) mod m if mx /\ not my
      x srem y mod m = <
                        | neg (rem x (neg y)) mod m if not mx /\ my
                        | neg (rem (neg x) (neg y)) mod m if mx /\ my
                        \

      where mx = msb x mod m,
        and my = msb y mod m.

val smod : t -> t -> t m

smod x y mod m is the signed remainder of x / y modulo m.

This version of the signed remainder where the sign follows the divisor, and is defined in terms of the rem operation as follows:

                        /
                        | u if u = 0
      x smod y mod m = <
                        | v if u <> 0
                        \

                        /
                        | u if not mx /\ not my
                        | add (neg u) y mod m if mx /\ not my
                   v = <
                        | add u x mod m if not mx /\ my
                        | neg u mod m if mx /\ my
                        \

      where mx = msb x mod m,
        and my = msb y mod m,
        and u = rem s t mod m.

val nth : t -> int -> bool m

nth x n mod m is true if nth bit of x is set.

Returns msb x mod m if n >= m and lsb x mod m if n < 0

val msb : t -> bool m

msb x mod m returns the most significand bit of x.

val lsb : t -> bool m

lsb x mod m returns the least significand bit of x.

val logand : t -> t -> t m

logand x y mod m is a bitwise logical and of x and y modulo m

val logor : t -> t -> t m

logor x y mod m is a bitwise logical or of x and y modulo m.

val logxor : t -> t -> t m

logxor x y mod m is exclusive or between x and y modulo m

val lshift : t -> t -> t m

lshift x y mod m shifts x to left by y. Returns 0 is y >= m.

val rshift : t -> t -> t m

rshift x y mod m shifts x right by y bits. Returns 0 if y >= m

val arshift : t -> t -> t m

arshift x y mod m shifts x right by y with msb x filling.

Returns ones mod m if y >= m /\ msb x mod m and zero if y >= m /\ msb x mod m = 0

val gcd : t -> t -> t m

gcd x y mod m returns the greatest common divisor modulo m

gcd x y is the meet operation of the divisibility lattice, with 0 being the top of the lattice and 1 being the bottom, therefore gcd x 0 = gcd x 0 = x.

val lcm : t -> t -> t m

lcm x y mod returns the least common multiplier modulo m.

lcm x y is the meet operation of the divisibility lattice, with 0 being the top of the lattice and 1 being the bottom, therefore lcm x 0 = lcm 0 x = 0

val gcdext : t -> t -> (t * t * t) m

(g,a,b) = gcdext x y mod m, where

g = gcd x y mod m,
g = (a * x + b * y) mod m.

The operation is well defined if one or both operands are equal to 0, in particular:

(x,1,0) = gcdext(x,0),
(x,0,1) = gcdext(0,x).

val (!$) : string -> t

!$x is of_string x

val (!!) : int -> t m

!!x mod m is int x mod m

val (~-) : t -> t m

~-x mod m is neg x mod m

val (~~) : t -> t m

~~x mod m is lnot x mod m

val (+) : t -> t -> t m

(x + y) mod m is add x y mod m

val (-) : t -> t -> t m

(x - y) mod m is sub x y mod m

val (*) : t -> t -> t m

(x * y) mod m is mul x y mod m

val (/) : t -> t -> t m

(x / y) mod m is div x y mod m

val (/$) : t -> t -> t m

x /$ y mod m is sdiv x y mod m

val (%) : t -> t -> t m

(x % y) mod m is rem x y mod m

val (%$) : t -> t -> t m

(x %$ y) mod m is smod x y mod m

val (%^) : t -> t -> t m

(x %^ y) mod m is srem x y mod m

val (land) : t -> t -> t m

(x land y) mod m is logand x y mod m

val (lor) : t -> t -> t m

(x lor y) mod m is logor x y mod m

val (lxor) : t -> t -> t m

(x lxor y) mod m is logxor x y mod m

val (lsl) : t -> t -> t m

(x lsl y) mod m lshift x y mod m

val (lsr) : t -> t -> t m

(x lsr y) mod m is rshift x y mod m

val (asr) : t -> t -> t m

(x asr y) = arshift x y

val (++) : t -> int -> t m

(x ++ n) mod m is nsucc x n mod m

val (--) : t -> int -> t m

(x -- n) mod mis npred x n mod m

module type Modulus = sig ... end

module Make (M : Modulus) : sig ... end

module Mx = Make(Modulus) produces a module Mx which implements all operation in S modulo Modulus.modulus, so that all operations return a bitvector directly.

module type D = S with type 'a m = 'a

module M1 : D

M1 specializes Make(struct let modulus = m1 end)

module M8 : D

M8 specializes Make(struct let modulus = m8 end)

module M16 : D

M16 specializes Make(struct let modulus = m16 end)

module M32 : D

M32 specializes Make(struct let modulus = m32 end)

module M64 : D

M64 specializes Make(struct let modulus = m64 end)

val modular : int -> (module D)

modular n returns a module M, which implements all operations in S modulo the bitwidth n.

since 2.5.0