4.3 Bitvectors
Rosette extends Racket with a primitive bitvector datatype whose values are
fixed-size words—
> (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)
> (asserts) ; so Rosette emits a corresponding assertion '(b)
procedure
(bitvector size) → bitvector?
size : (and/c integer? positive? (not/c term?) (not/c union?))
procedure
(bitvector? v) → boolean?
v : any/c
> (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
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?))
4.3.1 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)
> (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
x : (bitvector n) (bvor x ...+) → (bitvector n) x : (bitvector n) (bvxor x ...+) → (bitvector n) x : (bitvector n)
procedure
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)
> (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)
> (asserts) ; so Rosette emits a corresponding assertion '((! b))
4.3.3 Arithmetic Operators
procedure
x : (bitvector n) (bvsub x ...+) → (bitvector n) x : (bitvector n) (bvmul x ...+) → (bitvector n) x : (bitvector n)
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)
4.3.4 Conversion Operators
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?)
> (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))) {[b (bv #b01101 5)] [(! b) (bv #b001101 6)]}
> (zero-extend (bv -3 4) (if b (bitvector 5) "bad")) (bv #b01101 5)
> (asserts) '(b)
> (zero-extend (bv -3 4) (if c (bitvector 5) (bitvector 1))) (bv #b01101 5)
> (asserts) '(c b)
procedure
(bitvector->integer x) → integer?
x : bv? (bitvector->natural x) → integer? x : bv?
> (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?)
> (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))) {[c (bv #b00011 5)] [(! c) (bv #b000011 6)]}
> (asserts) '((! b))
4.3.5 Additional Operators
> (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))))
> (asserts) '((< i 4) (<= 0 i))
> (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))
> (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)) {[b (bvadd (bv #x1 4) x)] [(! b) (bvadd (bv #x01 8) y)]}
> (bvsub1 (if b x y)) {[b (bvadd (bv #xf 4) x)] [(! b) (bvadd (bv #xff 8) y)]}
procedure
x : (bitvector n) (bvumin x ...+) → (bitvector n) x : (bitvector n) (bvsmax x ...+) → (bitvector n) x : (bitvector n) (bvumax x ...+) → (bitvector n) x : (bitvector n)
procedure
x : (bitvector n) y : (bitvector n) (bvror x y) → (bitvector n) x : (bitvector n) y : (bitvector n)
procedure
(rotate-left i x) → (bitvector n)
i : integer? x : (bitvector n) (rotate-right i x) → (bitvector n) i : integer? x : (bitvector n)
> (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)))
{[b (ite* (⊢ (= 0 i) (bv #x3 4)) (⊢ (= 1 i) (bv #x6 4)) (⊢ (= 2 ...) ...) ...)]
[(! b) (ite* (⊢ (= 0 i) (bv #x07 8)) (⊢ (= 1 i) (bv #x0e 8)) (⊢ (= ...) ...) ...)]}
> (asserts) '((|| b (< i 8)) (|| (! b) (< i 4)) (<= 0 i))
procedure
(bitvector->bits x) → (listof (bitvector n))
x : (bitvector n)
> (bitvector->bits (bv 3 4)) '((bv #b1 1) (bv #b1 1) (bv #b0 1) (bv #b0 1))
> (define-symbolic y (bitvector 2)) > (bitvector->bits y) '((extract 0 0 y) (extract 1 1 y))
> (define-symbolic b boolean?) > (bitvector->bits (if b (bv 3 4) y))
{[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)
procedure
(bool->bitvector b [t]) → bv?
b : any/c t : (or/c positive-integer? (bitvector n)) = (bitvector 1)
> (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))