8.12
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
1 Constructing Bitvectors
To construct bitvectors you can use the function bv.
procedure
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.
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
Recognizes concrete or symbolic bitvector values of any size.
2 Comparison Operators
procedure
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:
3 Bitwise Operators
Returns the bitwise negation of the given bitvector value.
4 Arithmetic Operators
Returns the arithmetic negation of the given bitvector value.
procedure
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:
procedure
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.
5 Conversion Operators
Returns the bitwise concatenation of the given bitvector values.
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.
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
Extracts the ith bit from the bitvector x of size n, yielding a
bitvector of size 1. This procedure assumes that n > i >= 0.
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
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?