8.2

## Bitvectors

 (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

### 1Constructing 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 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

### 2Comparison 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

### 3Bitwise 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}

### 4Arithmetic 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}

### 5Conversion 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 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 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}

 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}

### 7Extensions

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).