From 2f60ad5e27dc8c46bce3ede800af81a246e16f6d Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Wed, 13 Jul 2016 19:21:12 -0400 Subject: [PATCH] finish typed-bv lang: typechecks all easy/med/hard tests --- macrotypes/typecheck.rkt | 3 +- turnstile/examples/rosette/bv.rkt | 113 ++++++ turnstile/examples/rosette/rosette.rkt | 46 ++- .../examples/tests/rosette/bv-ref-tests.rkt | 357 ++++++++++++++++++ turnstile/examples/tests/rosette/bv-tests.rkt | 30 ++ 5 files changed, 546 insertions(+), 3 deletions(-) create mode 100644 turnstile/examples/rosette/bv.rkt create mode 100644 turnstile/examples/tests/rosette/bv-ref-tests.rkt create mode 100644 turnstile/examples/tests/rosette/bv-tests.rkt diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt index 5a22d6e..8440e25 100644 --- 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 new file mode 100644 index 0000000..34ea710 --- /dev/null +++ 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 index e08804d..324c8d7 100644 --- 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 new file mode 100644 index 0000000..d198288 --- /dev/null +++ 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 new file mode 100644 index 0000000..b51cf98 --- /dev/null +++ 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))