From 6ee48d12a5106d211fec67a03d4ba2f2c4dc2741 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Thu, 25 Aug 2016 11:38:20 -0400 Subject: [PATCH] rosette2: start on bv operations --- turnstile/examples/rosette/rosette2.rkt | 49 ++++++++++++++++- .../examples/tests/rosette/rosette2-tests.rkt | 52 +++++++++++-------- 2 files changed, 76 insertions(+), 25 deletions(-) diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt index b9488ab..c213a5c 100644 --- a/turnstile/examples/rosette/rosette2.rkt +++ b/turnstile/examples/rosette/rosette2.rkt @@ -17,13 +17,20 @@ CNum Num CBool Bool CString ; symbolic string are not supported + ;; BV types + CBV BV + CBVPred ; symbolic bvpreds are not supported (yet) ) (require (prefix-in ro: rosette) (only-in "../stlc+union.rkt" define-named-type-alias prune+sort current-sub?) - (prefix-in C (only-in "../stlc+union+case.rkt" - PosInt Zero NegInt Float Bool String [U U*] U*? [case-> case->*] → →?)) + (prefix-in C + (combine-in + (only-in "../stlc+union+case.rkt" + PosInt Zero NegInt Float Bool String [U U*] U*? [case-> case->*] → →?) + (only-in "rosette.rkt" + BV BVPred))) (only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→]) (only-in "../ext-stlc.rkt" define-primop)) @@ -183,6 +190,44 @@ (C→ CNum CNum CNum) (C→ Num Num Num))) +;; --------------------------------- +;; BV Types and Operations + +(define-named-type-alias BV (U CBV)) + +(define-rosette-primop bv : (Ccase-> (C→ CInt CBVPred CBV) + (C→ Int CBVPred BV) + (C→ CInt CPosInt CBV) + (C→ Int CPosInt BV))) +(define-rosette-primop bitvector : (C→ CPosInt CBVPred)) + +(define-rosette-primop bveq : (C→ BV BV Bool)) +(define-rosette-primop bvslt : (C→ BV BV Bool)) +(define-rosette-primop bvult : (C→ BV BV Bool)) +(define-rosette-primop bvsle : (C→ BV BV Bool)) +(define-rosette-primop bvule : (C→ BV BV Bool)) +(define-rosette-primop bvsgt : (C→ BV BV Bool)) +(define-rosette-primop bvugt : (C→ BV BV Bool)) +(define-rosette-primop bvsge : (C→ BV BV Bool)) +(define-rosette-primop bvuge : (C→ BV BV Bool)) + +(define-rosette-primop bvnot : (C→ BV BV)) + +;; TODO: bvand, bvor, bvxor + +(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 bvsdiv : (C→ BV BV BV)) +(define-rosette-primop bvudiv : (C→ BV BV BV)) +(define-rosette-primop bvsrem : (C→ BV BV BV)) +(define-rosette-primop bvurem : (C→ BV BV BV)) +(define-rosette-primop bvsmod : (C→ BV BV BV)) + ;; --------------------------------- diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt index ede69ac..29062e7 100644 --- a/turnstile/examples/tests/rosette/rosette2-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette2-tests.rkt @@ -85,17 +85,23 @@ (check-type (+ (ann 1 : PosInt) (ann 10 : PosInt)) : Nat -> 11) (check-type (+ (ann -10 : NegInt) (ann 10 : PosInt)) : Int -> 0) -;; (check-type bv : (case-> (→ Int BVPred BV) -;; (→ Int PosInt BV))) -;; (typecheck-fail (bv "1" 2) #:with-msg "expected.*Int.*given.*String") -;; (check-type (bv 1 2) : BV -> (bv 1 (bvpred 2))) -;; (check-type (bv 1 (bvpred 2)) : BV -> (bv 1 (bvpred 2))) +;; BVs -;; (typecheck-fail (bv 0 0) #:with-msg "expected.*PosInt.*given.*Zero") -;; (check-type bitvector : (→ PosInt BVPred)) -;; (check-type (bitvector 3) : BVPred) -;; (typecheck-fail ((bitvector 4) 1)) -;; (check-type ((bitvector 4) (bv 10 (bvpred 4))) : Bool) +(check-type bv : (Ccase-> (C→ CInt CBVPred CBV) + (C→ Int CBVPred BV) + (C→ CInt CPosInt CBV) + (C→ Int CPosInt BV))) +(typecheck-fail (bv "1" 2) #:with-msg "expected.*Int.*given.*String") +(check-type (bv 1 2) : CBV -> (bv 1 (bitvector 2))) +(check-type (bv 1 (bitvector 2)) : CBV -> (bv 1 (bitvector 2))) +(check-type (bv (ann 1 : Int) 2) : BV -> (bv 1 (bitvector 2))) +(check-type (bv (ann 1 : Int) (bitvector 2)) : BV -> (bv 1 (bitvector 2))) + +(typecheck-fail (bv 0 0) #:with-msg "expected.*PosInt.*given.*Zero") +(check-type bitvector : (C→ CPosInt CBVPred)) +(check-type (bitvector 3) : CBVPred) +(typecheck-fail ((bitvector 4) 1)) +(check-type ((bitvector 4) (bv 10 (bitvector 4))) : CBool) ;; ;; same as above, but with bvpred ;; (check-type bvpred : (→ PosInt BVPred)) @@ -112,11 +118,11 @@ ;; (typecheck-fail (bvpred? "2")) ;; (check-type (bvpred? (bvpred 10)) : Bool -> #t) -;; ;; bvops -;; (check-type (bveq (bv 1 (bvpred 3)) (bv 1 (bvpred 3))) : Bool -> #t) -;; (typecheck-fail (bveq (bv 1 (bvpred 3)) 1)) -;; (check-type (bveq (bv 1 (bvpred 2)) (bv 1 (bvpred 3))) : Bool) ; -> runtime exn -;; (check-runtime-exn (bveq (bv 1 (bvpred 2)) (bv 1 (bvpred 3)))) +;; bvops +(check-type (bveq (bv 1 3) (bv 1 3)) : Bool -> #t) +(typecheck-fail (bveq (bv 1 3) 1)) +(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 @@ -135,14 +141,14 @@ ;; (check-type (bvand (bv -1 4) (if b (bv 3 4) (bv 2 4))) : BV ;; -> (if b (bv 3 4) (bv 2 4))) -;; (check-type (bvshl (bv 1 4) (bv 2 4)) : BV -> (bv 4 4)) -;; (check-type (bvlshr (bv -1 3) (bv 1 3)) : BV -> (bv 3 3)) -;; (check-type (bvashr (bv -1 5) (bv 1 5)) : BV -> (bv -1 5)) +(check-type (bvshl (bv 1 4) (bv 2 4)) : BV -> (bv 4 4)) +(check-type (bvlshr (bv -1 3) (bv 1 3)) : BV -> (bv 3 3)) +(check-type (bvashr (bv -1 5) (bv 1 5)) : BV -> (bv -1 5)) ;; ;; TODO: see issue #23 ;; (check-type (bvshl (bv -1 4) (if b (bv 3 4) (bv 2 4))) : BV) -;; (check-type (bvneg (bv -1 4)) : BV -> (bv 1 4)) -;; (check-type (bvneg (bv 0 4)) : BV -> (bv 0 4)) +(check-type (bvneg (bv -1 4)) : BV -> (bv 1 4)) +(check-type (bvneg (bv 0 4)) : BV -> (bv 0 4)) ;; (define-symbolic z (bitvector 3) : BV) ;; (check-type (bvneg z) : BV) ;; (check-type (bvadd (bv -1 4) (bv 2 4)) : BV -> (bv 1 4)) @@ -150,9 +156,9 @@ ;; (check-type (bvmul (bv -1 5) (bv 1 5)) : BV -> (bv -1 5)) ;; ;; TODO: see issue #23 ;; (check-type (bvadd (bv -1 4) (bv 2 4) (if b (bv 1 4) (bv 3 4))) : BV) -;; (check-type (bvsdiv (bv -3 4) (bv 2 4)) : BV -> (bv -1 4)) -;; (check-type (bvudiv (bv -3 3) (bv 2 3)) : BV -> (bv 2 3)) -;; (check-type (bvsmod (bv 1 5) (bv 0 5)) : BV -> (bv 1 5)) +(check-type (bvsdiv (bv -3 4) (bv 2 4)) : BV -> (bv -1 4)) +(check-type (bvudiv (bv -3 3) (bv 2 3)) : BV -> (bv 2 3)) +(check-type (bvsmod (bv 1 5) (bv 0 5)) : BV -> (bv 1 5)) ;; (check-type (bvsrem (bv -3 4) (if b (bv 2 4) (bv 3 4))) : BV ;; -> (if b (bv -1 4) (bv 0 4)))