www

commit e07f912cf788223417f830307f17a3a72ab52db4
parent 6ee48d12a5106d211fec67a03d4ba2f2c4dc2741
Author: AlexKnauth <alexander@knauth.org>
Date:   Thu, 25 Aug 2016 11:59:17 -0400

rosette2: support more bv operations

Diffstat:
M
turnstile/examples/rosette/rosette2.rkt
 | 
8
++++++--
M
turnstile/examples/tests/rosette/rosette2-tests.rkt
 | 
24
++++++++++++------------

2 files changed, 18 insertions(+), 14 deletions(-)
diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
@@ -213,14 +213,18 @@
 
 (define-rosette-primop bvnot : (C→ BV BV))
 
-;; TODO: bvand, bvor, bvxor
+(define-rosette-primop bvand : (C→ BV BV BV))
+(define-rosette-primop bvor : (C→ BV BV BV))
+(define-rosette-primop bvxor : (C→ BV BV BV))
 
 (define-rosette-primop bvshl : (C→ BV BV BV))
 (define-rosette-primop bvlshr : (C→ BV BV BV))
 (define-rosette-primop bvashr : (C→ BV BV BV))
 (define-rosette-primop bvneg : (C→ BV BV))
 
-;; TODO: bvadd, bvsub, bvmul
+(define-rosette-primop bvadd : (C→ BV BV BV))
+(define-rosette-primop bvsub : (C→ BV BV BV))
+(define-rosette-primop bvmul : (C→ BV BV BV))
 
 (define-rosette-primop bvsdiv : (C→ BV BV BV))
 (define-rosette-primop bvudiv : (C→ BV BV BV))
diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt
@@ -124,18 +124,18 @@
 (check-type (bveq (bv 1 2) (bv 1 3)) : Bool) ; -> runtime exn
 (check-runtime-exn (bveq (bv 1 2) (bv 1 3)))
 
-;; ;; non-primop bvops
-;; (check-type (bvand (bv -1 (bvpred 4)) (bv 2 (bvpred 4))) : BV 
-;;             -> (bv 2 (bvpred 4)))
-;; (check-type (bvor  (bv 0 (bvpred 3))  (bv 1 (bvpred 3))) : BV 
-;;             -> (bv 1 (bvpred 3)))
-;; (check-type (bvxor (bv -1 (bvpred 5)) (bv 1 (bvpred 5))) : BV 
-;;             -> (bv -2 (bvpred 5)))
-
-;; ;; examples from rosette guide
-;; (check-type (bvand (bv -1 4) (bv 2 4)) : BV -> (bv 2 4))
-;; (check-type (bvor  (bv 0 3)  (bv 1 3)) : BV -> (bv 1 3))
-;; (check-type (bvxor (bv -1 5) (bv 1 5)) : BV -> (bv -2 5))
+
+(check-type (bvand (bv -1 4) (bv 2 4)) : BV 
+            -> (bv 2 4))
+(check-type (bvor  (bv 0 3)  (bv 1 3)) : BV 
+            -> (bv 1 3))
+(check-type (bvxor (bv -1 5) (bv 1 5)) : BV 
+            -> (bv -2 5))
+
+;; examples from rosette guide
+(check-type (bvand (bv -1 4) (bv 2 4)) : BV -> (bv 2 4))
+(check-type (bvor  (bv 0 3)  (bv 1 3)) : BV -> (bv 1 3))
+(check-type (bvxor (bv -1 5) (bv 1 5)) : BV -> (bv -2 5))
 
 ;; (define-symbolic b boolean? : Bool)
 ;; (check-type (bvand (bv -1 4) (if b (bv 3 4) (bv 2 4))) : BV