4.3 Bitvectors

8.12

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 #b0000100 7)
> (bv 4 7)                    ; A shorthand for the same literal.
(bv #b0000100 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)
> (vc)                        ; so Rosette emits a corresponding assertion.
(vc #t 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)
> (vc)                        ; so Rosette emits a corresponding assertion.
(vc #t 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 #x0 4)
> (bvnot (bv 0 4))
(bv #xf 4)
> (define-symbolic b boolean?)
> (bvnot (if b 0 (bv 0 4))) ; This typechecks only when b is false,
(bv #xf 4)
> (vc) ; so Rosette emits a corresponding assertion.
(vc #t (! 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 #x2 4)
> (bvor  (bv 0 3)  (bv 1 3))
(bv #b001 3)
> (bvxor (bv -1 5) (bv 1 5))
(bv #b11110 5)
> (define-symbolic b boolean?)
> (bvand (bv -1 4)
         (if b 0 (bv 2 4))) ; This typechecks only when b is false,
(bv #x2 4)
> (vc)                      ; so Rosette emits a corresponding assertion.
(vc #t (! 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 #x4 4)
> (bvlshr (bv -1 3) (bv 1 3))
(bv #b011 3)
> (bvashr (bv -1 5) (bv 1 5))
(bv #b11111 5)
> (define-symbolic b boolean?)
> (bvshl (bv -1 4)
         (if b 0 (bv 2 4))) ; This typechecks only when b is false,
(bv #xc 4)
> (vc)                      ; so Rosette emits a corresponding assertion.
(vc #t (! 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 #x1 4)
> (bvneg (bv 0 4))
(bv #x0 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 #x1 4)
> (bvsub (bv 0 3) (bv 1 3))
(bv #b111 3)
> (bvmul (bv -1 5) (bv 1 5))
(bv #b11111 5)
> (define-symbolic b boolean?)
> (bvadd (bv -1 4) (bv 2 4) (if b (bv 1 4) "bad"))
(bv #x2 4)
> (vc)
(vc #t 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 #xf 4)
> (bvudiv (bv -3 3) (bv 2 3))
(bv #b010 3)
> (bvsmod (bv 1 5) (bv 0 5))
(bv #b00001 5)
> (define-symbolic b boolean?)
> (bvsrem (bv -3 4) (if b (bv 2 4) "bad"))
(bv #xf 4)
> (vc)
(vc #t 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 #xf7 8)
> (define-symbolic b boolean?)
> (concat (bv -1 4) (if b (bv 0 1) (bv 0 2)) (bv -1 3))
(union [b (bv #xf7 8)] [(! b) (bv #b111100111 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 #b11 2)
> (extract 3 3 (bv 1 4))
(bv #b0 1)
> (define-symbolic i j integer?)
> (extract i j (bv 1 2))
(union
[(&& (= 0 j) (= 1 i)) (bv #b01 2)]
[(|| (&& (= 0 i) (= 0 j)) (&& (= 1 i) (= 1 j)))
(ite* (⊢ (&& (= 0 i) (= 0 j)) (bv #b1 1)) (⊢ (&& (= 1 i) (= 1 j)) ...))])
> (vc)
(vc #t (&& (&& (<= j i) (<= 0 j)) (< i 2)))

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)
> (define-symbolic b c boolean?)
> (zero-extend (bv -3 4) (if b (bitvector 5) (bitvector 6)))
(union [b (bv #b01101 5)] [(! b) (bv #b001101 6)])
> (zero-extend (bv -3 4) (if b (bitvector 5) "bad"))
(bv #b01101 5)
> (vc)
(vc #t b)
> (zero-extend (bv -3 4) (if c (bitvector 5) (bitvector 1)))
(bv #b01101 5)
> (vc)
(vc #t (&& b c))

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
> (vc)
(vc #t 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 #b00 2)
> (integer->bitvector 15 (bitvector 4))
(bv #xf 4)
> (define-symbolic b c boolean?)
> (integer->bitvector (if b pi 3) (if c (bitvector 5) (bitvector 6)))
(union [c (bv #b00011 5)] [(! c) (bv #b000011 6)])
> (vc)
(vc #t (! b))

4.3.5 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)
> (define-symbolic i integer?)
> (define-symbolic x (bitvector 4))
> (bit i x)
(ite*
(⊢ (= 0 i) (extract 0 0 x))
(⊢ (= 1 i) (extract 1 1 x))
(⊢ (= 2 i) (extract 2 2 x))
(⊢ (= 3 i) (extract 3 3 x)))
> (vc)
(vc #t (&& (<= 0 i) (< i 4)))

procedure
(lsb x) → (bitvector 1)
x : (bitvector n)
(msb x) → (bitvector 1)
x : (bitvector n)

Returns the least or most significant bit of x.

Examples:

> (lsb (bv 3 4))
(bv #b1 1)
> (msb (bv 3 4))
(bv #b0 1)
> (define-symbolic x (bitvector 4))
> (define-symbolic y (bitvector 8))
> (lsb (if b x y))
(ite b (extract 0 0 x) (extract 0 0 y))
> (msb (if b x y))
(ite b (extract 3 3 x) (extract 7 7 y))

procedure
(bvzero? x) → boolean?
x : (bitvector n)

Returns (bveq x (bv 0 n)).

Examples:

> (define-symbolic x (bitvector 4))
> (bvzero? x)
(bveq (bv #x0 4) x)
> (define-symbolic y (bitvector 8))
> (bvzero? y)
(bveq (bv #x00 8) y)
> (define-symbolic b boolean?)
> (bvzero? (if b x y))
(|| (&& (bveq (bv #x00 8) y) (! b)) (&& (bveq (bv #x0 4) x) b))

procedure
(bvadd1 x) → (bitvector n)
x : (bitvector n)
(bvsub1 x) → (bitvector n)
x : (bitvector n)

Returns (bvadd x (bv 1 n)) or (bvsub x (bv 1 n)).

Examples:

> (define-symbolic x (bitvector 4))
> (bvadd1 x)
(bvadd (bv #x1 4) x)
> (define-symbolic y (bitvector 8))
> (bvsub1 y)
(bvadd (bv #xff 8) y)
> (define-symbolic b boolean?)
> (bvadd1 (if b x y))
(union [b (bvadd (bv #x1 4) x)] [(! b) (bvadd (bv #x01 8) y)])
> (bvsub1 (if b x y))
(union [b (bvadd (bv #xf 4) x)] [(! b) (bvadd (bv #xff 8) y)])

procedure
(bvsmin x ...+) → (bitvector n)
  x : (bitvector n)
(bvumin x ...+) → (bitvector n)
  x : (bitvector n)
(bvsmax x ...+) → (bitvector n)
  x : (bitvector n)
(bvumax x ...+) → (bitvector n)
  x : (bitvector n)

Returns the (un)signed minimum or maximum of one or more bitvector values of the same type.

Examples:

> (bvsmin (bv -1 4) (bv 2 4))
(bv #xf 4)
> (bvumin (bv -1 4) (bv 2 4))
(bv #x2 4)
> (bvsmax (bv -1 4) (bv 2 4))
(bv #x2 4)
> (bvumax (bv -1 4) (bv 2 4))
(bv #xf 4)
> (define-symbolic b boolean?)
> (bvsmin (bv -1 4) (bv 2 4) (if b (bv 1 4) (bv 3 8)))
(bv #xf 4)
> (vc)
(vc #t b)

procedure
(bvrol x y) → (bitvector n)
  x : (bitvector n)
  y : (bitvector n)
(bvror x y) → (bitvector n)
  x : (bitvector n)
  y : (bitvector n)

Returns the left or right rotation of x by (bvurem y n) bits, where x and y are bitvector values of the same type.

Examples:

> (bvrol (bv 3 4) (bv 2 4))
(bv #xc 4)
> (bvrol (bv 3 4) (bv -2 4))
(bv #xc 4)
> (define-symbolic b boolean?)
> (bvror (bv 3 4)
(if b 0 (bv 2 4))) ; This typechecks only when b is false,
(bv #xc 4)
> (vc) ; so Rosette emits a corresponding assertion.
(vc #t (! b))

procedure
(rotate-left i x) → (bitvector n)
  i : integer?
  x : (bitvector n)
(rotate-right i x) → (bitvector n)
  i : integer?
  x : (bitvector n)

Returns the left or right rotation of x by i bits. These procedures assume that n > i >= 0. See bvrol and bvror for an alternative way to perform rotations that usually leads to faster solving times.

Examples:

> (rotate-left 3 (bv 3 4))
(bv #x9 4)
> (rotate-right 1 (bv 3 4))
(bv #x9 4)
> (define-symbolic i integer?)
> (define-symbolic b boolean?)
> (rotate-left i (if b (bv 3 4) (bv 7 8)))
(union
[b
  (ite* (⊢ (= 0 i) (bv #x3 4)) (⊢ (= 1 i) (bv #x6 4)) (⊢ (= 2 i) ...) ...)]
[(! b)
  (ite* (⊢ (= 0 i) (bv #x07 8)) (⊢ (= 1 i) (bv #x0e 8)) (⊢ (= 2 ...) ...) ...)])
> (vc)
(vc
#t
(&&
  (<= 0 i)
  (|| (! b) (&& (<= 0 i) (|| (< i 4) (! (|| b (! (<= 0 i)))))))
  (|| b (&& (<= 0 i) (|| (< i 8) (! (|| (! b) (! (<= 0 i)))))))))

procedure
(bitvector->bits x) → (listof (bitvector n))
x : (bitvector n)

Returns the bits of x as a list, i.e., (list (bit 0 x) ... (bit (- n 1) x)).

Examples:

> (bitvector->bits (bv 3 4))
(list (bv #b1 1) (bv #b1 1) (bv #b0 1) (bv #b0 1))
> (define-symbolic y (bitvector 2))
> (bitvector->bits y)
(list (extract 0 0 y) (extract 1 1 y))
> (define-symbolic b boolean?)
> (bitvector->bits (if b (bv 3 4) y))
(union
[b ((bv #b1 1) (bv #b1 1) (bv #b0 1) (bv #b0 1))]
[(! b) ((extract 0 0 y) (extract 1 1 y))])

procedure
(bitvector->bool x) → boolean?
x : (bitvector n)

Returns (not (bvzero? x)).

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 concrete positive integer or a concrete bitvector type value.

Examples:

> (bool->bitvector #f 3)
(bv #b000 3)
> (bool->bitvector "non-false-value")
(bv #b1 1)
> (define-symbolic b boolean?)
> (bool->bitvector b)
(ite b (bv #b1 1) (bv #b0 1))

1	Getting Started
2	Rosette Essentials
3	Syntactic Forms
4	Built-In Datatypes
5	Structures
6	Libraries
7	Symbolic Reflection
8	Unsafe Operations
9	Performance
10	Debugging
11	References
	Index

4.1	Equality
4.2	Booleans, Integers, and Reals
4.3	Bitvectors
4.4	Uninterpreted Functions
4.5	Procedures
4.6	Pairs and Lists
4.7	Vectors
4.8	Boxes
4.9	Solvers and Solutions

4.3.1	Comparison Operators
4.3.2	Bitwise Operators
4.3.3	Arithmetic Operators
4.3.4	Conversion Operators
4.3.5	Additional Operators