commit 2f60ad5e27dc8c46bce3ede800af81a246e16f6d
parent 99693756549b79ab4da9cd0d9fbb4ae4e27b6e6d
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 13 Jul 2016 19:21:12 -0400
finish typed-bv lang: typechecks all easy/med/hard tests
Diffstat:
5 files changed, 546 insertions(+), 3 deletions(-)
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
@@ -10,11 +10,12 @@
"stx-utils.rkt")
(for-meta 2 racket/base syntax/parse racket/syntax syntax/stx "stx-utils.rkt")
(for-meta 3 racket/base syntax/parse racket/syntax)
- racket/bool racket/provide racket/require racket/match racket/promise)
+ racket/bool racket/provide racket/require racket/match racket/promise syntax/parse/define)
(provide
postfix-in
symbol=?- match- delay-
(except-out (all-from-out racket/base) #%module-begin)
+ (all-from-out syntax/parse/define)
(for-syntax (all-defined-out)) (all-defined-out)
(for-syntax
(all-from-out racket syntax/parse racket/syntax syntax/stx
diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt
@@ -0,0 +1,113 @@
+#lang turnstile
+(extends "rosette.rkt" #:except bv)
+(require (prefix-in ro: rosette)) ; untyped
+(require (except-in "rosette.rkt" #%app define)) ; typed
+(require (only-in sdsl/bv/lang/bvops bvredand bvredor)
+ (prefix-in bv: (only-in sdsl/bv/lang/bvops BV)))
+(require sdsl/bv/lang/core (prefix-in bv: sdsl/bv/lang/form))
+(provide bool->bv thunk)
+
+;(define current-bvpred-internal (ro:make-parameter (ro:bitvector 4)))
+;; this must be a macro in order to support Racket's overloaded set/get
+;; parameter patterns
+(define-typed-syntax current-bvpred
+ [c-bvpred:id ≫
+ --------
+ [⊢ [[_ ≫ bv:BV] ⇒ : (Param BVPred)]]]
+ [(_) ≫
+ --------
+ [⊢ [[_ ≫ (bv:BV)] ⇒ : BVPred]]]
+ [(_ e) ≫
+ [⊢ [[e ≫ e-] ⇒ : BVPred]]
+ --------
+ [⊢ [[_ ≫ (bv:BV e-)] ⇒ : Unit]]])
+
+(define-typed-syntax bv
+ [(_ e_val) ≫
+ --------
+ [_ ≻ (rosette:bv e_val (current-bvpred))]]
+ [(_ e_val e_size) ≫
+ --------
+ [_ ≻ (rosette:bv e_val e_size)]])
+
+(define-typed-syntax bv*
+ [(_) ≫
+ --------
+ [_ ≻ (bv* (current-bvpred))]]
+ [(_ e_size) ≫
+ [⊢ [[e_size ≫ e_size-] ⇐ : BVPred]]
+ --------
+ [⊢ [[_ ≫ ((lambda- () (ro:define-symbolic* b e_size-) b))] ⇒ : BV]]])
+
+(define-syntax-rule (bool->bv b) (if b (bv 1) (bv 0)))
+#;(define-typed-syntax bool->bv
+ [(_ e) ≫
+ [⊢ [[e ≫ e-] ⇐ : Bool]]
+ --------
+ [⊢ [[_ ≫ (if- e- (bv 1) (bv 0))] ⇒ : BV]]])
+
+;; (define- (bvredor x) (ro:bveq (ro:bveq x (bv 0)) (bv 0)))
+;; (define- (bvredand x) (ro:bveq x (bv -1)))
+(define-primop bvredor : (→ BV BV))
+(define-primop bvredand : (→ BV BV))
+
+(define-simple-macro (define-comparators id ...)
+ #:with (op ...) (stx-map (lambda (o) (format-id o "ro:~a" o)) #'(id ...))
+ (begin-
+ (define- (id x y) (bool->bv (op x y))) ...
+ (define-primop id : (→ BV BV BV)) ...))
+
+(define-comparators bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge)
+
+(define-base-types Prog Lib)
+
+(define-typed-syntax define-fragment
+ [(_ (id param ...) #:implements spec #:library lib-expr) ≫
+ --------
+ [_ ≻ (define-fragment (id param ...) #:implements spec #:library lib-expr #:minbv 4)]]
+ [(_ (id param ...) #:implements spec #:library lib-expr #:minbv minbv) ≫
+ [⊢ [[spec ≫ spec-] ⇒ : ty_spec]]
+ [#:fail-unless (→? #'ty_spec) "spec must be a function"]
+ [⊢ [[lib-expr ≫ lib-expr-] ⇐ : Lib]]
+ [⊢ [[minbv ≫ minbv-] ⇐ : Int]]
+ [#:with id-stx (format-id #'id "~a-stx" #'id #:source #'id)]
+ --------
+ [_ ≻ (begin-
+ (define-values- (id-internal id-stx-internal)
+ (bv:synthesize-fragment (id param ...)
+ #:implements spec-
+ #:library lib-expr-
+ #:minbv minbv-))
+ (define-syntax id (make-rename-transformer (⊢ id-internal : ty_spec)))
+ (define-syntax id-stx (make-rename-transformer (⊢ id-stx-internal : Stx)))
+ )]])
+
+(define-typed-syntax bvlib
+ [(_ [(~and ids (id ...)) n] ...) ≫
+ [#:fail-unless (stx-andmap brace? #'(ids ...))
+ "given ops must be enclosed with braces"]
+ [⊢ [[n ≫ n-] ⇐ : Int] ...]
+ [⊢ [[id ≫ id-] ⇒ : ty_id] ...] ...
+ [#:fail-unless (stx-andmap →? #'(ty_id ... ...))
+ "given op must be a function"]
+ [#:with ((~→ ty ...) ...) #'(ty_id ... ...)]
+ [#:fail-unless (stx-andmap BV? #'(ty ... ...))
+ "given op must have BV inputs and output"]
+ --------
+ [⊢ [[_ ≫ (bv:bvlib [{id- ...} n-] ...)] ⇒ : Lib]]])
+
+
+#;(define-typed-syntax synthesize-fragment
+ [(_ (id param ...) #:implements spec #:library lib-expr)
+ --------
+ [_ ≻ (synthesize-fragment (id param ...) #:implements spec #:library lib-expr #:minbv 4)]]
+ [(_ (id param ...) #:implements spec #:library lib-expr #:minbv minbv)
+ [⊢ [[spec ≫ spec-] ⇐ : Spec]]
+ [⊢ [[lib-expr ≫ lib-expr-] ⇐ : Lib]]
+ [⊢ [[minbv ≫ minbv-] ⇐ : Int]]]
+ --------
+ [⊢ [[_ ≫ (bv:synthesize-fragment (id param) #:implements spec-
+ #:library lib-expr-
+ #:minbv minbv-)] ⇒ : BV]])
+
+(define-syntax-rule (thunk e) (λ () e))
diff --git a/turnstile/examples/rosette/rosette.rkt b/turnstile/examples/rosette/rosette.rkt
@@ -1,8 +1,9 @@
#lang turnstile
;(require (only-in rosette bv bitvector))
;(require (only-in rosette [exact-integer? integer?]))
-(require syntax/parse/define)
(extends "../ext-stlc.rkt" #:except if)
+(reuse equal? #:from "../mlish.rkt")
+(require (prefix-in stlc: (only-in "../stlc+reco+var.rkt" define λ)))
(require (only-in "../stlc+reco+var.rkt" define-type-alias))
(require (prefix-in ro: rosette))
(provide BVPred)
@@ -51,8 +52,10 @@
--------
[⊢ [[_ ≫ (ro:if e_tst- e1- e2-)] ⇒ : (⊔ τ1 τ2)]]])
+;; TODO: fix this to support Racket parameter usage patterns?
+;; eg, this wont work if applied since it's not a function type
(define-typed-syntax make-parameter
- [(_ e) ⇐ : (~Param τ_expected) ≫
+ #;[(_ e) ⇐ : (~Param τ_expected) ≫
[⊢ [[e ≫ e-] ⇐ : τ_expected]]
--------
[⊢ [[_ ≫ (ro:make-parameter e-)]]]]
@@ -61,6 +64,25 @@
--------
[⊢ [[_ ≫ (ro:make-parameter e-)] ⇒ : (Param τ)]]])
+(define-typed-syntax define #:datum-literals (: -> →)
+ [(_ x:id e) ≫
+ --------
+ [_ ≻ (stlc:define x e)]]
+ [(_ (f [x : ty] ... (~or → ->) ty_out) e) ≫
+; [⊢ [[e ≫ e-] ⇒ : ty_e]]
+ [#:with f- (generate-temporary #'f)]
+ --------
+ [_ ≻ (begin-
+ (define-syntax- f (make-rename-transformer (⊢ f- : (→ ty ... ty_out))))
+ (stlc:define f- (stlc:λ ([x : ty] ...) e)))]])
+
+(define-base-type Stx)
+
+#;(define-typed-syntax syntax
+ [(_ template) ≫
+ --------
+ [⊢ [[_ ≫ (syntax- template)] ⇒ : Stx]]])
+
;; ----------------------------------------------------------------------------
;; BV stuff
@@ -92,6 +114,8 @@
(define-rosette-primop bitvector? : (→ BVPred Bool))
(define-rosette-primop* bitvector bvpred : (→ Nat BVPred))
(define-rosette-primop* bitvector? bvpred? : (→ BVPred Bool))
+(define-rosette-primop bitvector-size : (→ BVPred Int))
+(define-rosette-primop* bitvector-size bvpred-size : (→ BVPred Int))
(define-rosette-primop bveq : (→ BV BV Bool))
(define-rosette-primop bvslt : (→ BV BV Bool))
@@ -107,16 +131,25 @@
(define-typed-syntax bvand
+ [f:id ≫ ; TODO: implement variable arity types
+ --------
+ [⊢ [[_ ≫ ro:bvand] ⇒ : (→ BV BV BV)]]]
[(_ e ...+) ≫
[⊢ [[e ≫ e-] ⇐ : BV] ...]
--------
[⊢ [[_ ≫ (ro:bvand e- ...)] ⇒ : BV]]])
(define-typed-syntax bvor
+ [f:id ≫ ; TODO: implement variable arity types
+ --------
+ [⊢ [[_ ≫ ro:bvor] ⇒ : (→ BV BV BV)]]]
[(_ e ...+) ≫
[⊢ [[e ≫ e-] ⇐ : BV] ...]
--------
[⊢ [[_ ≫ (ro:bvor e- ...)] ⇒ : BV]]])
(define-typed-syntax bvxor
+ [f:id ≫ ; TODO: implement variable arity types
+ --------
+ [⊢ [[_ ≫ ro:bvxor] ⇒ : (→ BV BV BV)]]]
[(_ e ...+) ≫
[⊢ [[e ≫ e-] ⇐ : BV] ...]
--------
@@ -128,16 +161,25 @@
(define-rosette-primop bvneg : (→ BV BV))
(define-typed-syntax bvadd
+ [f:id ≫ ; TODO: implement variable arity types
+ --------
+ [⊢ [[_ ≫ ro:bvadd] ⇒ : (→ BV BV BV)]]]
[(_ e ...+) ≫
[⊢ [[e ≫ e-] ⇐ : BV] ...]
--------
[⊢ [[_ ≫ (ro:bvadd e- ...)] ⇒ : BV]]])
(define-typed-syntax bvsub
+ [f:id ≫ ; TODO: implement variable arity types
+ --------
+ [⊢ [[_ ≫ ro:bvsub] ⇒ : (→ BV BV BV)]]]
[(_ e ...+) ≫
[⊢ [[e ≫ e-] ⇐ : BV] ...]
--------
[⊢ [[_ ≫ (ro:bvsub e- ...)] ⇒ : BV]]])
(define-typed-syntax bvmul
+ [f:id ≫ ; TODO: implement variable arity types
+ --------
+ [⊢ [[_ ≫ ro:bvmul] ⇒ : (→ BV BV BV)]]]
[(_ e ...+) ≫
[⊢ [[e ≫ e-] ⇐ : BV] ...]
--------
diff --git a/turnstile/examples/tests/rosette/bv-ref-tests.rkt b/turnstile/examples/tests/rosette/bv-ref-tests.rkt
@@ -0,0 +1,357 @@
+#lang s-exp "../../rosette/bv.rkt"
+(require "../rackunit-typechecking.rkt")
+
+; The 25 Hacker's Delight benchmarks from the following paper:
+; Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan.
+; 2011. Synthesis of loop-free programs. In Proceedings of the 32nd ACM
+; SIGPLAN Conference on Programming Language Design and Implementation (PLDI '11).
+;
+; The first 20 benchmarks are also used in the SyGuS competition: http://www.sygus.org
+
+(current-bvpred (bvpred 32))
+
+(check-type (thunk (bv 1)) : (→ BV))
+
+; Constants.
+(define bv1 (thunk (bv 1)))
+(define bv2 (thunk (bv 2)))
+(define bvsz (thunk (bv (sub1 (bvpred-size (current-bvpred))))))
+
+(check-type bv1 : (→ BV))
+(check-type (bv1) : BV -> (bv 1))
+(check-type ((bvpred 4) (bv1)) : Bool -> #f)
+(check-type ((bvpred 32) (bv1)) : Bool -> #t)
+(check-type bv2 : (→ BV))
+(check-type bvsz : (→ BV))
+
+(check-type (bvsub (bv 1) (bv1)) : BV -> (bv 0))
+(check-type ((bvpred 32) (bvsub (bv 1) (bv1))) : Bool -> #t)
+
+; Mask off the rightmost 1-bit.
+(define (p1 [x : BV] -> BV)
+ (let* ([o1 (bvsub x (bv 1))]
+ [o2 (bvand x o1)])
+ o2))
+
+(check-type (p1 (bv 1)) : BV -> (bv 0))
+(check-type ((bvpred 32) (p1 (bv 1))) : Bool -> #t)
+
+; Test whether an unsigned integer is of the form 2^n-1.
+(define (p2 [x : BV] -> BV)
+ (let* ([o1 (bvadd x (bv 1))]
+ [o2 (bvand x o1)])
+ o2))
+
+; Isolate the right most 1-bit.
+(define (p3 [x : BV] -> BV)
+ (let* ([o1 (bvneg x)]
+ [o2 (bvand x o1)])
+ o2))
+
+; Form a mask that identifies the rightmost 1-bit and trailing 0s.
+(define (p4 [x : BV] -> BV)
+ (let* ([o1 (bvsub x (bv 1))]
+ [o2 (bvxor x o1)])
+ o2))
+
+; Right propagate rightmost 1-bit.
+(define (p5 [x : BV] -> BV)
+ (let* ([o1 (bvsub x (bv 1))]
+ [o2 (bvor x o1)])
+ o2))
+
+; Turn on the right-most 0-bit in a word.
+(define (p6 [x : BV] -> BV)
+ (let* ([o1 (bvadd x (bv 1))]
+ [o2 (bvor x o1)])
+ o2))
+
+; Isolate the right most 0 bit of a given bitvector.
+(define (p7 [x : BV] -> BV)
+ (let* ([o1 (bvnot x)]
+ [o2 (bvadd x (bv 1))]
+ [o3 (bvand o1 o2)])
+ o3))
+
+; Form a mask that identifies the trailing 0s.
+(define (p8 [x : BV] -> BV)
+ (let* ([o1 (bvsub x (bv 1))]
+ [o2 (bvnot x)]
+ [o3 (bvand o1 o2)])
+ o3))
+
+; Absolute value function.
+(define (p9 [x : BV] -> BV)
+ (let* ([o1 (bvashr x (bv 31))]
+ [o2 (bvxor x o1)]
+ [o3 (bvsub o2 o1)])
+ o3))
+
+; Test if nlz(x) == nlz(y) where nlz is number of leading zeroes.
+(define (p10 [x : BV] [y : BV] -> BV)
+ (let* ([o1 (bvand x y)]
+ [o2 (bvxor x y)]
+ [o3 (bvule o2 o1)])
+ o3))
+
+; Test if nlz(x) < nlz(y) where nlz is number of leading zeroes.
+(define (p11 [x : BV] [y : BV] -> BV)
+ (let* ([o1 (bvnot y)]
+ [o2 (bvand x o1)]
+ [o3 (bvugt o2 y)])
+ o3))
+
+; Test if nlz(x) <= nlz(y) where nlz is number of leading zeroes.
+(define (p12 [x : BV] [y : BV] -> BV)
+ (let* ([o1 (bvnot x)]
+ [o2 (bvand y o1)]
+ [o3 (bvule o2 x)])
+ o3))
+
+; Sign function.
+(define (p13 [x : BV] -> BV)
+ (let* ([o1 (bvneg x)]
+ [o2 (bvlshr o1 (bv 31))]
+ [o3 (bvashr x (bv 31))]
+ [o4 (bvor o2 o3)])
+ o4))
+
+; Floor of average of two integers without over-flowing.
+(define (p14 [x : BV] [y : BV] -> BV)
+ (let* ([o1 (bvand x y)]
+ [o2 (bvxor x y)]
+ [o3 (bvlshr o2 (bv 1))]
+ [o4 (bvadd o1 o3)])
+ o4))
+
+; Ceil of average of two integers without over-flowing.
+(define (p15 [x : BV] [y : BV] -> BV)
+ (let* ([o1 (bvor x y)]
+ [o2 (bvxor x y)]
+ [o3 (bvlshr o2 (bv 1))]
+ [o4 (bvsub o1 o3)])
+ o4))
+
+; The max function.
+(define (p16 [x : BV] [y : BV] -> BV)
+ (if (equal? (bv 1) (bvsge x y)) x y))
+
+; Turn-off the rightmost contiguous string of 1 bits.
+(define (p17 [x : BV] -> BV)
+ (let* ([o1 (bvsub x (bv 1))]
+ [o2 (bvor x o1)]
+ [o3 (bvadd o2 (bv 1))]
+ [o4 (bvand o3 x)])
+ o4))
+
+; Test whether an unsigned integer is of the form 2^n.
+(define (p18 [x : BV] -> BV)
+ (let* ([o1 (bvsub x (bv 1))]
+ [o2 (bvand o1 x)]
+ [o3 (bvredor x)]
+ [o4 (bvredor o2)]
+ [o5 (bvnot o4)]
+ [o6 (bvand o5 o3)])
+ o6))
+
+; Exchanging 2 fields A and B of the same register
+; x where m is mask which identifies field B and k
+; is number of bits from end of A to start of B.
+(define (p19 [x : BV] [m : BV] [k : BV] -> BV)
+ (let* ([o1 (bvlshr x k)]
+ [o2 (bvxor x o1)]
+ [o3 (bvand o2 m)]
+ [o4 (bvshl o3 k)]
+ [o5 (bvxor o4 o3)]
+ [o6 (bvxor o5 x)])
+ o6))
+
+; Next higher unsigned number with the same number of 1 bits.
+(define (p20 [x : BV] -> BV)
+ (let* ([o1 (bvneg x)]
+ [o2 (bvand x o1)]
+ [o3 (bvadd x o2)]
+ [o4 (bvxor x o2)]
+ [o5 (bvlshr o4 (bv 2))]
+ [o6 (bvudiv o5 o2)]
+ [o7 (bvor o6 o3)])
+ o7))
+
+; Cycling through 3 values a, b, c.
+(define (p21 [x : BV] [a : BV] [b : BV] [c : BV] -> BV)
+ (let* ([o1 (bveq x c)]
+ [o2 (bvneg o1)]
+ [o3 (bvxor a c)]
+ [o4 (bveq x a)]
+ [o5 (bvneg o4)]
+ [o6 (bvxor b c)]
+ [o7 (bvand o2 o3)]
+ [o8 (bvand o5 o6)]
+ [o9 (bvxor o7 o8)]
+ [o10 (bvxor o9 c)])
+ o10))
+
+; Compute parity.
+(define (p22 [x : BV] -> BV)
+ (let* ([o1 (bvlshr x (bv 1))]
+ [o2 (bvxor o1 x)]
+ [o3 (bvlshr o2 (bv 2))]
+ [o4 (bvxor o2 o3)]
+ [o5 (bvand o4 (bv #x11111111))]
+ [o6 (bvmul o5 (bv #x11111111))]
+ [o7 (bvlshr o6 (bv 28))]
+ [o8 (bvand o7 (bv 1))])
+ o8))
+
+; Counting number of bits.
+(define (p23 [x : BV] -> BV)
+ (let* ([o1 (bvlshr x (bv 1))]
+ [o2 (bvand o1 (bv #x55555555))]
+ [o3 (bvsub x o2)]
+ [o4 (bvand o3 (bv #x33333333))]
+ [o5 (bvlshr o3 (bv 2))]
+ [o6 (bvand o5 (bv #x33333333))]
+ [o7 (bvadd o4 o6)]
+ [o8 (bvlshr o7 (bv 4))]
+ [o9 (bvadd o8 o7)]
+ [o10 (bvand o9 (bv #x0f0f0f0f))])
+ o10))
+
+; Round up to the next higher power of 2.
+(define (p24 [x : BV] -> BV)
+ (let* ([o1 (bvsub x (bv 1))]
+ [o2 (bvlshr o1 (bv 1))]
+ [o3 (bvor o1 o2)]
+ [o4 (bvlshr o3 (bv 2))]
+ [o5 (bvor o3 o4)]
+ [o6 (bvlshr o5 (bv 4))]
+ [o7 (bvor o5 o6)]
+ [o8 (bvlshr o7 (bv 8))]
+ [o9 (bvor o7 o8)]
+ [o10 (bvlshr o9 (bv 16))]
+ [o11 (bvor o9 o10)]
+ [o12 (bvadd o11 (bv 1))])
+ o12))
+
+; Compute higher order half of product of x and y.
+(define (p25 [x : BV] [y : BV] -> BV)
+ (let* ([o1 (bvand x (bv #xffff))]
+ [o2 (bvlshr x (bv 16))]
+ [o3 (bvand y (bv #xffff))]
+ [o4 (bvlshr y (bv 16))]
+ [o5 (bvmul o1 o3)]
+ [o6 (bvmul o2 o3)]
+ [o7 (bvmul o1 o4)]
+ [o8 (bvmul o2 o4)]
+ [o9 (bvlshr o5 (bv 16))]
+ [o10 (bvadd o6 o9)]
+ [o11 (bvand o10 (bv #xffff))]
+ [o12 (bvlshr o10 (bv 16))]
+ [o13 (bvadd o7 o11)]
+ [o14 (bvlshr o13 (bv 16))]
+ [o15 (bvadd o14 o12)]
+ [o16 (bvadd o15 o8)])
+ o16))
+
+;; Mask off the rightmost 1-bit. < 1 sec.
+(define-fragment (p1* x)
+ #:implements p1
+ #:library (bvlib [{bv1 bvand bvsub} 1]))
+
+; Test whether an unsigned integer is of the form 2^n-1. < 1 sec.
+(define-fragment (p2* x)
+ #:implements p2
+ #:library (bvlib [{bv1 bvand bvadd} 1]))
+
+; Isolate the right most 1-bit. < 1 sec.
+(define-fragment (p3* x)
+ #:implements p3
+ #:library (bvlib [{bvand bvneg} 1]))
+
+; Form a mask that identifies the rightmost 1-bit and trailing 0s. < 1 sec.
+(define-fragment (p4* x)
+ #:implements p4
+ #:library (bvlib [{bv1 bvsub bvxor} 1]))
+
+; Right propagate rightmost 1-bit. < 1 sec.
+(define-fragment (p5* x)
+ #:implements p5
+ #:library (bvlib [{bv1 bvsub bvor} 1]))
+
+; Turn on the right-most 0-bit in a word. < 1 sec.
+(define-fragment (p6* x)
+ #:implements p6
+ #:library (bvlib [{bv1 bvor bvadd} 1]))
+
+; Isolate the right most 0 bit of a given bitvector. < 1 sec.
+(define-fragment (p7* x)
+ #:implements p7
+ #:library (bvlib [{bvand bvadd bvnot bv1} 1]))
+
+; Form a mask that identifies the trailing 0s. < 1 sec.
+(define-fragment (p8* x)
+ #:implements p8
+ #:library (bvlib [{bv1 bvsub bvand bvnot} 1]))
+
+; Absolute value function. ~ 1 sec.
+(define-fragment (p9* x)
+ #:implements p9
+ #:library (bvlib [{bvsz bvsub bvxor bvashr} 1]))
+
+; Test if nlz(x) == nlz(y) where nlz is number of leading zeroes. < 1 sec.
+(define-fragment (p10* x y)
+ #:implements p10
+ #:library (bvlib [{bvand bvxor bvule} 1]))
+
+; Test if nlz(x) < nlz(y) where nlz is number of leading zeroes. < 1 sec.
+(define-fragment (p11* x y)
+ #:implements p11
+ #:library (bvlib [{bvnot bvand bvugt} 1]))
+
+; Test if nlz(x) <= nlz(y) where nlz is number of leading zeroes. < 1 sec.
+(define-fragment (p12* x y)
+ #:implements p12
+ #:library (bvlib [{bvand bvnot bvule} 1]))
+
+; Sign function. ~ 1.4 sec.
+(define-fragment (p13* x)
+ #:implements p13
+ #:library (bvlib [{bvsz bvneg bvlshr bvashr bvor} 1])
+ #:minbv 32)
+
+; Floor of average of two integers without over-flowing. ~ 2.5 sec.
+(define-fragment (p14* x y)
+ #:implements p14
+ #:library (bvlib [{bv1 bvand bvlshr bvxor bvadd} 1]))
+
+; Ceil of average of two integers without over-flowing. ~ 1 sec.
+(define-fragment (p15* x y)
+ #:implements p15
+ #:library (bvlib [{bv1 bvor bvlshr bvxor bvsub} 1]))
+
+; Compute max of two integers. Bug in the PLDI'11 paper: bvuge should be bvge.
+; ~ 1.3 sec.
+(define-fragment (p16* x y)
+ #:implements p16
+ #:library (bvlib [{bvneg bvsge bvand} 1] [{bvxor} 2]))
+
+; Turn-off the rightmost contiguous string of 1 bits. ~ 1.8 sec.
+(define-fragment (p17* x)
+ #:implements p17
+ #:library (bvlib [{bv1 bvand bvor bvadd bvsub} 1]))
+
+; Test whether an unsigned integer is of the form 2^n. ~ 1.6 sec.
+(define-fragment (p18* x)
+ #:implements p18
+ #:library (bvlib [{bvand bvredor} 2] [{bvsub bvnot bv1} 1]))
+
+; x where m is mask which identifies field B and k
+; is number of bits from end of A to start of B. ~ 3.5 sec.
+(define-fragment (p19* x m k)
+ #:implements p19
+ #:library (bvlib [{bvlshr bvshl bvand} 1] [{bvxor} 3]))
+
+; Next higher unsigned number with the same number of 1 bits. ~ 600 sec.
+(define-fragment (p20* x)
+ #:implements p20
+ #:library (bvlib [{bv2 bvneg bvand bvadd bvxor bvlshr bvudiv bvor} 1]))
diff --git a/turnstile/examples/tests/rosette/bv-tests.rkt b/turnstile/examples/tests/rosette/bv-tests.rkt
@@ -0,0 +1,30 @@
+#lang s-exp "../../rosette/bv.rkt"
+(require "../rackunit-typechecking.rkt")
+
+(check-type current-bvpred : (Param BVPred))
+(check-type (current-bvpred) : BVPred -> (bvpred 4))
+(check-type (current-bvpred (bvpred 5)) : Unit -> (void))
+(check-type (current-bvpred) : BVPred -> (bvpred 5))
+(check-type (current-bvpred (bvpred 4)) : Unit -> (void))
+
+(check-type (bv 1) : BV)
+(check-type ((bvpred 4) (bv 1)) : Bool -> #t)
+(check-type ((bvpred 1) (bv 1)) : Bool -> #f)
+(check-type (bv 2 (bvpred 3)) : BV)
+(check-type ((bvpred 3) (bv 2 (bvpred 3))) : Bool -> #t)
+
+(check-type (bv*) : BV)
+
+(check-type (bool->bv 1) : BV -> (bv 1))
+(check-type (bool->bv #f) : BV -> (bv 0))
+(define-symbolic i integer? : Int)
+(define-symbolic b boolean? : Bool)
+(check-type (bool->bv i) : BV -> (bv 1))
+(check-type (bool->bv b) : BV -> (if b (bv 1) (bv 0)))
+
+(check-type (bvredor (bv 1)) : Bool)
+(check-type (bvredand (bv 1)) : Bool)
+
+(check-type bveq : (→ BV BV BV))
+(check-type (bveq (bv 1) (bv 1)) : BV -> (bv 1))
+(check-type (bveq (bv 1) (bv 0)) : BV -> (bv 0))
