On this page:
bitvector
bitvector?
bv
bv?
4.3.1 Comparison Operators
bveq
bvslt
bvult
bvsle
bvule
bvsgt
bvugt
bvsge
bvuge
4.3.2 Bitwise Operators
bvnot
bvand
bvor
bvxor
bvshl
bvlshr
bvashr
4.3.3 Arithmetic Operators
bvneg
bvadd
bvsub
bvmul
bvsdiv
bvudiv
bvsrem
bvurem
bvsmod
4.3.4 Conversion Operators
concat
extract
sign-extend
zero-extend
bitvector->integer
bitvector->natural
integer->bitvector
6.6

4.3 Bitvectors

Rosette extends Racket with a primitive bitvector datatype whose values are fixed-size words—or, machine integers. Mainstream programming languages, such as C or Java, support bitvector types with a few fixed sizes (e.g., 8 bits, 16 bits, and 32 bits). Rosette supports bitvectors of arbitrary size, as well as both signed and unsigned versions of various bitvector operations (such as comparisons, division, remainder, etc.). Technically, Rosette’s bitvector datatype embeds the theory of bitvectors into a programming language.

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

(bv 4 7)

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

(bv 4 7)

> (define-symbolic x y (bitvector 7)) ; symbolic bitvector constants
> (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

> (define-symbolic b boolean?)
> (bvadd x (if b y (bv 3 4))) ; this typechecks only when b is true

(bvadd x y)

> (asserts)                   ; so Rosette emits a corresponding assertion

'(b)

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

> (define-symbolic b boolean?)
> (bv6? (if b (bv 3 6) #t))

b

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))
> (define-symbolic b boolean?)
> (bitvector? bv6?) ; a concrete bitvector type

#t

> (bitvector? (if b bv6? bv7?)) ; not a concrete type

#f

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

#f

> (bitvector? 3) ; not a type

#f

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

(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

> (define-symbolic b boolean?)
> (bv? (if b (bv 3 6) #t))

b

4.3.1 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:
> (define-symbolic u v (bitvector 7)) ; symbolic bitvector constants
> (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

> (define-symbolic b boolean?)
> (bvsge u (if b v (bv 3 4))) ; this typechecks only when b is true

(bvsle v u)

> (asserts)                   ; so Rosette emits a corresponding assertion

'(b)

4.3.2 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 0 4)

> (bvnot (bv 0 4))

(bv -1 4)

> (define-symbolic b boolean?)
> (bvnot (if b 0 (bv 0 4))) ; this typechecks only when b is false

(bv -1 4)

> (asserts)                 ; so Rosette emits a corresponding assertion

'((! b))

procedure

(bvand x ...+)  (bitvector n)

  x : (bitvector n)
(bvor x ...+)  (bitvector n)
  x : (bitvector n)
(bvxor x ...+)  (bitvector n)
  x : (bitvector n)
Returns the bitwise "and", "or", "xor" of one or more bitvector values of the same type.

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

(bv 2 4)

> (bvor  (bv 0 3)  (bv 1 3))

(bv 1 3)

> (bvxor (bv -1 5) (bv 1 5))

(bv -2 5)

> (define-symbolic b boolean?)
> (bvand (bv -1 4)
         (if b 0 (bv 2 4))) ; this typechecks only when b is false

(bv 2 4)

> (asserts)                 ; so Rosette emits a corresponding assertion

'((! b))

procedure

(bvshl x y)  (bitvector n)

  x : (bitvector n)
  y : (bitvector n)
(bvlshr x y)  (bitvector n)
  x : (bitvector n)
  y : (bitvector n)
(bvashr x y)  (bitvector n)
  x : (bitvector n)
  y : (bitvector n)
Returns the left, logical right, or arithmetic right shift of x by y bits, where x and y are bitvector values of the same type.

Examples:
> (bvshl  (bv 1 4) (bv 2 4))

(bv 4 4)

> (bvlshr (bv -1 3) (bv 1 3))

(bv 3 3)

> (bvashr (bv -1 5) (bv 1 5))

(bv -1 5)

> (define-symbolic b boolean?)
> (bvshl (bv -1 4)
         (if b 0 (bv 2 4))) ; this typechecks only when b is false

(bv -4 4)

> (asserts)                 ; so Rosette emits a corresponding assertion

'((! b))

4.3.3 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 1 4)

> (bvneg (bv 0 4))

(bv 0 4)

> (define-symbolic z (bitvector 3))
> (bvneg z)

(bvneg z)

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 1 4)

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

(bv -1 3)

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

(bv -1 5)

> (define-symbolic b boolean?)
> (bvadd (bv -1 4) (bv 2 4) (if b (bv 1 4) "bad"))

(bv 2 4)

> (asserts)

'(b)

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. All five operations are defined even when the second argument is zero.

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

(bv -1 4)

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

(bv 2 3)

> (bvsmod (bv 1 5) (bv 0 5))

(bv 1 5)

> (define-symbolic b boolean?)
> (bvsrem (bv -3 4) (if b (bv 2 4) "bad"))

(bv -1 4)

> (asserts)

'(b)

4.3.4 Conversion Operators

procedure

(concat x ...+)  bv?

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

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

(bv -9 8)

> (define-symbolic b boolean?)
> (concat (bv -1 4) (if b (bv 0 1) (bv 0 2)) (bv -1 3))

{[b (bv -9 8)] [(! b) (bv -25 9)]}

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 -1 2)

> (extract 3 3 (bv 1 4))

(bv 0 1)

> (define-symbolic i j integer?)
> (extract i j (bv 1 2))

{[(&& (= 0 j) (= 1 i)) (bv 1 2)] ...}

> (asserts)

'((< i 2) (<= 0 j) (<= j i))

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 -3 6)

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

(bv 13 6)

> (define-symbolic b c boolean?)
> (zero-extend (bv -3 4) (if b (bitvector 5) (bitvector 6)))

{[b (bv 13 5)] [(! b) (bv 13 6)]}

> (zero-extend (bv -3 4) (if b (bitvector 5) "bad"))

(bv 13 5)

> (asserts)

'(b)

> (zero-extend (bv -3 4) (if c (bitvector 5) (bitvector 1)))

(bv 13 5)

> (asserts)

'(c b)

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

> (define-symbolic b boolean?)
> (bitvector->integer (if b (bv -1 3) (bv -3 4)))

(ite b -1 -3)

> (bitvector->integer (if b (bv -1 3) "bad"))

-1

> (asserts)

'(b)

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 0 2)

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

(bv -1 4)

> (define-symbolic b c boolean?)
> (integer->bitvector (if b pi 3) (if c (bitvector 5) (bitvector 6)))

{[c (bv 3 5)] [(! c) (bv 3 6)]}

> (asserts)

'((! b))