Bitvectors
1 Constructing Bitvectors
bv
bitvector
bitvector?
bv?
2 Comparison Operators
bveq
bvslt
bvult
bvsle
bvule
bvsgt
bvugt
bvsge
bvuge
3 Bitwise Operators
bvnot
4 Arithmetic Operators
bvneg
bvadd
bvsub
bvmul
bvsdiv
bvudiv
bvsrem
bvurem
bvsmod
5 Conversion Operators
concat
extract
sign-extend
zero-extend
bitvector->integer
bitvector->natural
integer->bitvector
6 Additional Operators
bit
bvzero?
bool->bitvector
7 Extensions
random-bv
random-bv/  limits
7.7

Bitvectors

Paulo Matos <pmatos@linki.tools>

 (require bv) package: bv

This module is inspired by the bitvector interface exposed by Rosette. Functions with the same name will behave the same.

Bitvectors are constant-sized vectors of bits and the provided interface extends the one defined in the Rosette Bitvector Guide.

For example, all of the non-symbolic examples in Rosette’s Guide work as expected:

Examples:
> (bv 4 (bitvector 7))        ; a bitvector literal of size 7

{bv #b0000100 7}

> (bv 4 7)                    ; a shorthand for the same literal

{bv #b0000100 7}

> (bvslt (bv 4 7) (bv -1 7))  ; signed 7-bit < comparison of 4 and -1

#f

> (bvult (bv 4 7) (bv -1 7))  ; unsigned 7-bit < comparison of 4 and -1

#t

1 Constructing Bitvectors

To construct bitvectors you can use the function bv.

procedure

(bv val size)  bv?

  val : (and/c integer? (not/c term?) (not/c union?))
  size : 
(and/c (or/c bitvector? (and/c integer? positive?))
       (not/c term?) (not/c union?))
Returns a bitvector literal of the given size, which may be given either as a concrete bitvector? type or a concrete positive integer.

procedure

(bitvector size)  bitvector?

  size : (and/c integer? positive? (not/c term?) (not/c union?))
Returns a type predicate that recognizes bitvectors of the given size. Note that size must be a concrete positive integer. The type predicate itself is recognized by the bitvector? predicate.

Examples:
> (define bv6? (bitvector 6))
> (bv6? 1)

#f

> (bv6? (bv 3 6))

#t

> (bv6? (bv 3 5))

#f

procedure

(bitvector? v)  boolean?

  v : any/c
Returns true if v is a concrete type predicate that recognizes bitvector values.

Examples:
> (define bv6? (bitvector 6))
> (define bv7? (bitvector 7))
> (bitvector? bv6?) ; a concrete bitvector type

#t

> (bitvector? integer?) ; not a bitvector type

#f

> (bitvector? 3) ; not a type

#f

procedure

(bv? v)  boolean?

  v : any/c
Recognizes concrete or symbolic bitvector values of any size.

Examples:
> (bv? 1)

#f

> (bv? (bv 1 1))

#t

> (bv? (bv 2 2))

#t

2 Comparison Operators

procedure

(bveq x y)  boolean?

  x : (bitvector n)
  y : (bitvector n)
(bvslt x y)  boolean?
  x : (bitvector n)
  y : (bitvector n)
(bvult x y)  boolean?
  x : (bitvector n)
  y : (bitvector n)
(bvsle x y)  boolean?
  x : (bitvector n)
  y : (bitvector n)
(bvule x y)  boolean?
  x : (bitvector n)
  y : (bitvector n)
(bvsgt x y)  boolean?
  x : (bitvector n)
  y : (bitvector n)
(bvugt x y)  boolean?
  x : (bitvector n)
  y : (bitvector n)
(bvsge x y)  boolean?
  x : (bitvector n)
  y : (bitvector n)
(bvuge x y)  boolean?
  x : (bitvector n)
  y : (bitvector n)
Compares two bitvector values of the same bitvector type. Comparison relations include equality (bveq) and signed / unsigned versions of <, <=, >, and >= (bvslt, bvult, bvsle, bvule, bvsgt, and bvugt).

Examples:
> (bvslt (bv 4 7) (bv -1 7))  ; signed 7-bit < comparison of 4 and -1

#f

> (bvult (bv 4 7) (bv -1 7))  ; unsigned 7-bit < comparison of 4 and -1

#t

3 Bitwise Operators

procedure

(bvnot x)  (bitvector n)

  x : (bitvector n)
Returns the bitwise negation of the given bitvector value.

Examples:
> (bvnot (bv -1 4))

{bv #x0 4}

> (bvnot (bv 0 4))

{bv #xf 4}

4 Arithmetic Operators

procedure

(bvneg x)  (bitvector n)

  x : (bitvector n)
Returns the arithmetic negation of the given bitvector value.

Examples:
> (bvneg (bv -1 4))

{bv #x1 4}

> (bvneg (bv 0 4))

{bv #x0 4}

procedure

(bvadd x ...+)  (bitvector n)

  x : (bitvector n)
(bvsub x ...+)  (bitvector n)
  x : (bitvector n)
(bvmul x ...+)  (bitvector n)
  x : (bitvector n)
Returns the sum, difference, or product of one or more bitvector values of the same type.

Examples:
> (bvadd (bv -1 4) (bv 2 4))

{bv #x1 4}

> (bvsub (bv 0 3)  (bv 1 3))

{bv #b111 3}

> (bvmul (bv -1 5) (bv 1 5))

{bv #b11111 5}

procedure

(bvsdiv x y)  (bitvector n)

  x : (bitvector n)
  y : (bitvector n)
(bvudiv x y)  (bitvector n)
  x : (bitvector n)
  y : (bitvector n)
(bvsrem x y)  (bitvector n)
  x : (bitvector n)
  y : (bitvector n)
(bvurem x y)  (bitvector n)
  x : (bitvector n)
  y : (bitvector n)
(bvsmod x y)  (bitvector n)
  x : (bitvector n)
  y : (bitvector n)
Returns (un)signed quotient, remainder, or modulo of two bitvector values of the same type. Exception: None of these operations is valid for a zero denominator.

Examples:
> (bvsdiv (bv -3 4) (bv 2 4))

{bv #xf 4}

> (bvudiv (bv -3 3) (bv 2 3))

{bv #b010 3}

5 Conversion Operators

procedure

(concat x ...+)  bv?

  x : bv?
Returns the bitwise concatenation of the given bitvector values.

Example:
> (concat (bv -1 4) (bv 0 1) (bv -1 3))

{bv #xf7 8}

procedure

(extract i j x)  (bitvector (+ 1 (- i j)))

  i : integer?
  j : integer?
  x : (bitvector n)
Extracts bits i down to j from a bitvector of size n, yielding a bitvector of size i - j + 1. This procedure assumes that n > i >= j >= 0.

Examples:
> (extract 2 1 (bv -1 4))

{bv #b11 2}

> (extract 3 3 (bv 1 4))

{bv #b0 1}

procedure

(sign-extend x t)  bv?

  x : bv?
  t : (or/c bitvector? union?)
(zero-extend x t)  bv?
  x : bv?
  t : (or/c bitvector? union?)
Returns a bitvector of type t that represents the (un)signed extension of the bitvector x. Note that both x and t may be symbolic. The size of t must not be smaller than the size of x’s type.

Examples:
> (sign-extend (bv -3 4) (bitvector 6))

{bv #b111101 6}

> (zero-extend (bv -3 4) (bitvector 6))

{bv #b001101 6}

procedure

(bitvector->integer x)  integer?

  x : bv?
(bitvector->natural x)  integer?
  x : bv?
Returns the (un)signed integer value of the given bitvector.

Examples:
> (bitvector->integer (bv -1 4))

-1

> (bitvector->natural (bv -1 4))

15

procedure

(integer->bitvector i t)  bv?

  i : integer?
  t : (or/c bitvector? union?)
Returns a bitvector of type t that represents the k lowest order bits of the integer i, where k is the size of t. Note that both i and t may be symbolic.

Examples:
> (integer->bitvector 4 (bitvector 2))

{bv #b00 2}

> (integer->bitvector 15 (bitvector 4))

{bv #xf 4}

6 Additional Operators

procedure

(bit i x)  (bitvector 1)

  i : integer?
  x : (bitvector n)
Extracts the ith bit from the bitvector x of size n, yielding a bitvector of size 1. This procedure assumes that n > i >= 0.

Examples:
> (bit 1 (bv 3 4))

{bv #b1 1}

> (bit 2 (bv 1 4))

{bv #b0 1}

procedure

(bvzero? x)  boolean?

  x : (bitvector n)
Returns (bveq x (bv 0 n)).

Examples:
> (bvzero? (bv 0 32))

#t

> (bvzero? (bv 2 8))

#f

procedure

(bool->bitvector b [t])  bv?

  b : any/c
  t : (or/c positive-integer? (bitvector n)) = (bitvector 1)
Returns (bv 0 t) if (false? b) and otherwise returns (bv 1 t), where t is (bitvector 1) by default. If provided, t must be a positive integer or a bitvector type value.

Examples:
> (bool->bitvector #f 3)

{bv #b000 3}

> (bool->bitvector "non-false-value")

{bv #b1 1}

7 Extensions

The following operators are an extension to what Rosette provides.

procedure

(random-bv n)  bv?

  n : exact-positive-integer?
Returns a random bitvector, of type (bitvector (* 8 n)), between 0 and (- (expt 2 (* 8 n)) 1) (inclusive).

procedure

(random-bv/limits n min max)  bv?

  n : exact-positive-integer?
  min : exact-nonnegative-integer?
  max : exact-nonnegative-integer?
Returns random bitvector, of type (bitvector (* 8 n)), between min and max (inclusive).