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 47);A shorthand for the same literal.

(bv #b0000100 7)
> (define-symbolic xy(bitvector 7));Symbolic bitvector constants.
> (bvslt (bv 47)(bv -17));Signed 7-bit < comparison of 4 and -1.

#f
> (bvult (bv 47)(bv -17));Unsigned 7-bit < comparison of 4 and -1.

#t
> (define-symbolic bboolean? )
> (bvadd x(if by(bv 34)));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 36))

#t
> (bv6?(bv 35))

#f
> (define-symbolic bboolean? )
> (bv6?(if b(bv 36)#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 bboolean? )
> (bitvector? bv6?);A concrete bitvector type.

#t
> (bitvector? (if bbv6?bv7?));Not a concrete type.

#f
> (bitvector? integer? );Not a bitvector type.

#f
> (bitvector? 3);Not a type.

#f

procedure
( bv valsize)→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 11))

#t
> (bv? (bv 22))

#t
> (define-symbolic bboolean? )
> (bv? (if b(bv 36)#t))

b

4.3.1Comparison Operators🔗 i

procedure
( bveq xy)→boolean?
x:(bitvector n)
y:(bitvector n)
( bvslt xy)→boolean?
x:(bitvector n)
y:(bitvector n)
( bvult xy)→boolean?
x:(bitvector n)
y:(bitvector n)
( bvsle xy)→boolean?
x:(bitvector n)
y:(bitvector n)
( bvule xy)→boolean?
x:(bitvector n)
y:(bitvector n)
( bvsgt xy)→boolean?
x:(bitvector n)
y:(bitvector n)
( bvugt xy)→boolean?
x:(bitvector n)
y:(bitvector n)
( bvsge xy)→boolean?
x:(bitvector n)
y:(bitvector n)
( bvuge xy)→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 uv(bitvector 7));Symbolic bitvector constants.
> (bvslt (bv 47)(bv -17));Signed 7-bit < comparison of 4 and -1.

#f
> (bvult (bv 47)(bv -17));Unsigned 7-bit < comparison of 4 and -1.

#t
> (define-symbolic bboolean? )
> (bvsge u(if bv(bv 34)));This typechecks only when b is true,

(bvsle v u)
> (vc );so Rosette emits a corresponding assertion.

(vc #t b)

4.3.2Bitwise Operators🔗 i

procedure
( bvnot x)→(bitvector n)
x:(bitvector n)

Returns the bitwise negation of the given bitvector value.

Examples:

> (bvnot (bv -14))

(bv #x0 4)
> (bvnot (bv 04))

(bv #xf 4)
> (define-symbolic bboolean? )
> (bvnot (if b0(bv 04)));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 -14)(bv 24))

(bv #x2 4)
> (bvor (bv 03)(bv 13))

(bv #b001 3)
> (bvxor (bv -15)(bv 15))

(bv #b11110 5)
> (define-symbolic bboolean? )

> (bvand (bv -14)
(if b0(bv 24)));This typechecks only when b is false,

(bv #x2 4)
> (vc );so Rosette emits a corresponding assertion.

(vc #t (! b))

procedure
( bvshl xy)→(bitvector n)
x:(bitvector n)
y:(bitvector n)
( bvlshr xy)→(bitvector n)
x:(bitvector n)
y:(bitvector n)
( bvashr xy)→(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 14)(bv 24))

(bv #x4 4)
> (bvlshr (bv -13)(bv 13))

(bv #b011 3)
> (bvashr (bv -15)(bv 15))

(bv #b11111 5)
> (define-symbolic bboolean? )

> (bvshl (bv -14)
(if b0(bv 24)));This typechecks only when b is false,

(bv #xc 4)
> (vc );so Rosette emits a corresponding assertion.

(vc #t (! b))

4.3.3Arithmetic Operators🔗 i

procedure
( bvneg x)→(bitvector n)
x:(bitvector n)

Returns the arithmetic negation of the given bitvector value.

Examples:

> (bvneg (bv -14))

(bv #x1 4)
> (bvneg (bv 04))

(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 -14)(bv 24))

(bv #x1 4)
> (bvsub (bv 03)(bv 13))

(bv #b111 3)
> (bvmul (bv -15)(bv 15))

(bv #b11111 5)
> (define-symbolic bboolean? )
> (bvadd (bv -14)(bv 24)(if b(bv 14)"bad"))

(bv #x2 4)
> (vc )

(vc #t b)

procedure
( bvsdiv xy)→(bitvector n)
x:(bitvector n)
y:(bitvector n)
( bvudiv xy)→(bitvector n)
x:(bitvector n)
y:(bitvector n)
( bvsrem xy)→(bitvector n)
x:(bitvector n)
y:(bitvector n)
( bvurem xy)→(bitvector n)
x:(bitvector n)
y:(bitvector n)
( bvsmod xy)→(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 -34)(bv 24))

(bv #xf 4)
> (bvudiv (bv -33)(bv 23))

(bv #b010 3)
> (bvsmod (bv 15)(bv 05))

(bv #b00001 5)
> (define-symbolic bboolean? )
> (bvsrem (bv -34)(if b(bv 24)"bad"))

(bv #xf 4)
> (vc )

(vc #t b)

4.3.4Conversion Operators🔗 i

procedure
( concat x...+)→bv?
x:bv?

Returns the bitwise concatenation of the given bitvector values.

Examples:

> (concat (bv -14)(bv 01)(bv -13))

(bv #xf7 8)
> (define-symbolic bboolean? )
> (concat (bv -14)(if b(bv 01)(bv 02))(bv -13))

(union [b (bv #xf7 8)] [(! b) (bv #b111100111 9)])

procedure
( extract ijx)→(bitvector (+ 1(- ij)))
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 21(bv -14))

(bv #b11 2)
> (extract 33(bv 14))

(bv #b0 1)
> (define-symbolic ijinteger? )
> (extract ij(bv 12))

(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 xt)→bv?
x:bv?
t:(or/c bitvector? union? )
( zero-extend xt)→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 -34)(bitvector 6))

(bv #b111101 6)
> (zero-extend (bv -34)(bitvector 6))

(bv #b001101 6)
> (define-symbolic bcboolean? )
> (zero-extend (bv -34)(if b(bitvector 5)(bitvector 6)))

(union [b (bv #b01101 5)] [(! b) (bv #b001101 6)])
> (zero-extend (bv -34)(if b(bitvector 5)"bad"))

(bv #b01101 5)
> (vc )

(vc #t b)
> (zero-extend (bv -34)(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 -14))

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

15
> (define-symbolic bboolean? )
> (bitvector->integer (if b(bv -13)(bv -34)))

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

-1
> (vc )

(vc #t b)

procedure
( integer->bitvector it)→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 bcboolean? )
> (integer->bitvector (if bpi 3)(if c(bitvector 5)(bitvector 6)))

(union [c (bv #b00011 5)] [(! c) (bv #b000011 6)])
> (vc )

(vc #t (! b))

4.3.5Additional Operators🔗 i

procedure
( bit ix)→(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 34))

(bv #b1 1)
> (bit 2(bv 14))

(bv #b0 1)
> (define-symbolic iinteger? )
> (define-symbolic x(bitvector 4))
> (bit ix)

(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 34))

(bv #b1 1)
> (msb (bv 34))

(bv #b0 1)
> (define-symbolic x(bitvector 4))
> (define-symbolic y(bitvector 8))
> (lsb (if bxy))

(ite b (extract 0 0 x) (extract 0 0 y))
> (msb (if bxy))

(ite b (extract 3 3 x) (extract 7 7 y))

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

Returns (bveq x(bv 0n)).

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 bboolean? )
> (bvzero? (if bxy))

(|| (&& (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 1n)) or (bvsub x(bv 1n)).

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 bboolean? )
> (bvadd1 (if bxy))

(union [b (bvadd (bv #x1 4) x)] [(! b) (bvadd (bv #x01 8) y)])
> (bvsub1 (if bxy))

(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 -14)(bv 24))

(bv #xf 4)
> (bvumin (bv -14)(bv 24))

(bv #x2 4)
> (bvsmax (bv -14)(bv 24))

(bv #x2 4)
> (bvumax (bv -14)(bv 24))

(bv #xf 4)
> (define-symbolic bboolean? )
> (bvsmin (bv -14)(bv 24)(if b(bv 14)(bv 38)))

(bv #xf 4)
> (vc )

(vc #t b)

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

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

Examples:

> (bvrol (bv 34)(bv 24))

(bv #xc 4)
> (bvrol (bv 34)(bv -24))

(bv #xc 4)
> (define-symbolic bboolean? )

> (bvror (bv 34)
(if b0(bv 24)));This typechecks only when b is false,

(bv #xc 4)
> (vc );so Rosette emits a corresponding assertion.

(vc #t (! b))

procedure
( rotate-left ix)→(bitvector n)
i:integer?
x:(bitvector n)
( rotate-right ix)→(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 34))

(bv #x9 4)
> (rotate-right 1(bv 34))

(bv #x9 4)
> (define-symbolic iinteger? )
> (define-symbolic bboolean? )
> (rotate-left i(if b(bv 34)(bv 78)))

(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 1))
x:(bitvector n)

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

Examples:

> (bitvector->bits (bv 34))

(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 bboolean? )
> (bitvector->bits (if b(bv 34)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 0t) if (false? b) and otherwise returns (bv 1t), 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 #f3)

(bv #b000 3)
> (bool->bitvector "non-false-value")

(bv #b1 1)
> (define-symbolic bboolean? )
> (bool->bitvector b)

(ite b (bv #b1 1) (bv #b0 1))

top ← prev up next →