From e3171e2b47894470451675bd382c3c323c5ad4ca Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Thu, 8 Sep 2016 13:06:29 -0400 Subject: [PATCH] change BVPred input to Any; add remaining sec4.3 BV examples --- turnstile/examples/rosette/bv.rkt | 8 +- turnstile/examples/rosette/rosette-notes.txt | 2 +- turnstile/examples/rosette/rosette2.rkt | 41 ++-- .../rosette/rosette-guide-sec43-tests.rkt | 183 +++++++++++++++++- .../examples/tests/rosette/rosette2-tests.rkt | 9 +- 5 files changed, 218 insertions(+), 25 deletions(-) diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt index 042e3ab..f7c5da2 100644 --- a/turnstile/examples/rosette/bv.rkt +++ b/turnstile/examples/rosette/bv.rkt @@ -77,9 +77,13 @@ "given ops must be enclosed with braces" [⊢ [n ≫ n- ⇐ : Int] ...] [⊢ [id ≫ id- ⇒ : ty_id] ... ...] - #:fail-unless (stx-andmap C→? #'(ty_id ... ...)) + #:fail-unless (stx-andmap (lambda (t) (or (C→? t) (Ccase->? t))) #'(ty_id ... ...)) "given op must be a function" - #:with ((~C→ ty ...) ...) #'(ty_id ... ...) + ;; outer ~and wrapper is a syntax-parse workaround + #:with ((~and (~or (~C→ ty ...) + (~and (~Ccase-> (~C→ ty* ...) ...) + (~parse (ty ...) #'(ty* ... ...))))) ...) + #'(ty_id ... ...) #:fail-unless (stx-andmap τ⊑BV? #'(ty ... ...)) "given op must have BV inputs and output" -------- diff --git a/turnstile/examples/rosette/rosette-notes.txt b/turnstile/examples/rosette/rosette-notes.txt index b58f9c6..cf85f0d 100644 --- a/turnstile/examples/rosette/rosette-notes.txt +++ b/turnstile/examples/rosette/rosette-notes.txt @@ -2,7 +2,7 @@ Typed Rosette tricky subtyping examples: -) Both these should be true: +***** Both these should be true: (Constant Int) <: (U (Constant Int) (Constant Bool)) (Constant Int) <: Int = (U CInt) diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt index 560d31b..7c143cd 100644 --- a/turnstile/examples/rosette/rosette2.rkt +++ b/turnstile/examples/rosette/rosette2.rkt @@ -11,8 +11,7 @@ CU U Constant C→ → (for-syntax ~C→ C→?) - Ccase-> ; TODO: symbolic case-> not supported yet - CListof CVectorof CMVectorof CIVectorof + CListof Listof CVectorof CMVectorof CIVectorof CParamof ; TODO: symbolic Param not supported yet CUnit Unit CNegInt NegInt @@ -25,6 +24,7 @@ CFalse CTrue CBool Bool CString String CStx ; symblic Stx not supported + CAsserts ;; BV types CBV BV CBVPred BVPred @@ -37,7 +37,7 @@ (combine-in (only-in "../stlc+union+case.rkt" PosInt Zero NegInt Float True False String [U U*] U*? - [case-> case->*] → →?) + [case-> case->*] case->? → →?) (only-in "../stlc+cons.rkt" Unit [List Listof]))) (only-in "../stlc+union+case.rkt" [~U* ~CU*] [~case-> ~Ccase->] [~→ ~C→]) (only-in "../stlc+cons.rkt" [~List ~CListof]) @@ -623,6 +623,8 @@ ;; --------------------------------- ;; IO and other built-in ops +(define-named-type-alias CAsserts (CListof Bool)) + (provide (rosette-typed-out [printf : (Ccase-> (C→ CString CUnit) (C→ CString Any CUnit) (C→ CString Any Any CUnit))] @@ -815,7 +817,7 @@ (C→ Int Int Int))] ;; rosette-specific - [asserts : (C→ (CListof Bool))] + [asserts : (C→ CAsserts)] [clear-asserts! : (C→ CUnit)])) ;; --------------------------------- @@ -893,13 +895,14 @@ -------- [⊢ [_ ≫ (ro:current-bitwidth e-) ⇒ : CUnit]]]) -(define-named-type-alias BV (add-predm (U CBV) ro:bv?)) -(define-symbolic-named-type-alias BVPred (C→ BV Bool) #:pred lifted-bitvector?) +(define-named-type-alias BV (add-predm (U CBV) bv?)) +(define-symbolic-named-type-alias BVPred (C→ Any Bool) #:pred lifted-bitvector?) +(define-named-type-alias BVMultiArgOp (Ccase-> (C→ BV BV BV) + (C→ BV BV BV BV))) (provide (rosette-typed-out [bv : (Ccase-> (C→ CInt CBVPred CBV) (C→ CInt CPosInt CBV))] [bv? : (C→ Any Bool)] - [bitvector? : (C→ Any Bool)] [bveq : (C→ BV BV Bool)] [bvslt : (C→ BV BV Bool)] @@ -922,9 +925,9 @@ [bvashr : (C→ BV BV BV)] [bvneg : (C→ BV BV)] - [bvadd : (C→ BV BV BV)] - [bvsub : (C→ BV BV BV)] - [bvmul : (C→ BV BV BV)] + [bvadd : BVMultiArgOp] + [bvsub : BVMultiArgOp] + [bvmul : BVMultiArgOp] [bvsdiv : (C→ BV BV BV)] [bvudiv : (C→ BV BV BV)] @@ -932,7 +935,7 @@ [bvurem : (C→ BV BV BV)] [bvsmod : (C→ BV BV BV)] - [concat : (C→ BV BV BV)] + [concat : BVMultiArgOp] [extract : (C→ Int Int BV BV)] [sign-extend : (C→ BV CBVPred BV)] [zero-extend : (C→ BV BVPred BV)] @@ -956,6 +959,22 @@ (ro:bitvector n-) BV)) ⇒ : CBVPred]]]) +;; bitvector? can produce type CFalse if input does not have type (C→ Any Bool) +;; result is always CBool, since anything symbolic returns false +;(define-rosette-primop bitvector? : (C→ Any Bool)) +(define-typed-syntax bitvector? + [_:id ≫ + -------- + [⊢ [_ ≫ ro:bitvector? ⇒ : (C→ Any CBool)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇐ : (C→ Any Bool)]] + -------- + [⊢ [_ ≫ (ro:bitvector? e-) ⇒ : CBool]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : _]] + -------- + [⊢ [_ ≫ (ro:bitvector? e-) ⇒ : CFalse]]]) + ;; --------------------------------- ;; Uninterpreted functions diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec43-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec43-tests.rkt index 3eff78d..fb8e648 100644 --- a/turnstile/examples/tests/rosette/rosette-guide-sec43-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette-guide-sec43-tests.rkt @@ -13,10 +13,179 @@ (check-type x : BV) (check-type y : BV) (check-type (bvslt (bv 4 7) (bv -1 7)) : Bool -> #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) +; unsigned 7-bit < comparison of 4 and -1 +(check-type (bvult (bv 4 7) (bv -1 7)) : Bool -> #t) +(define-symbolic b boolean?) +; this typechecks only when b is true +(check-type (bvadd x (if b y (bv 3 4))) : BV -> (bvadd x y)) +(check-type (asserts) : (CListof Bool) -> (list b)) ; Rosette emits an appropriate assertion +(clear-asserts!) + +;; bitvector +(define bv6? (bitvector 6)) +(check-type (bv6? 1) : Bool -> #f) +(check-type (bv6? (bv 3 6)) : Bool -> #t) +(check-type (bv6? (bv 3 5)) : Bool -> #f) +;(define-symbolic b boolean?) +(check-type (bv6? (if b (bv 3 6) #t)) : Bool -> b) +(check-not-type (bv6? (if b (bv 3 6) #t)) : CBool) + +;; bitvector? +;(define bv6? (bitvector 6)) +(define bv7? (bitvector 7)) +;(define-symbolic b boolean?) +(check-type (bitvector? bv6?) : Bool -> #t) ; a concrete bitvector type +(check-type (bitvector? (if b bv6? bv7?)) : Bool -> #f) ; not a concrete type +(check-type (bitvector? integer?) : Bool -> #f) ; not a bitvector type +(check-type (bitvector? 3) : Bool -> #f) ; not a type +;; result is always CBool +(check-type (bitvector? bv6?) : CBool -> #t) ; a concrete bitvector type +(check-type (bitvector? (if b bv6? bv7?)) : CBool -> #f) ; not a concrete type +(check-type (bitvector? integer?) : CBool -> #f) ; not a bitvector type +(check-type (bitvector? 3) : CBool -> #f) ; not a type +;; check CFalse when possible +(check-not-type (bitvector? bv6?) : CFalse) ; a concrete bitvector type +(check-type (bitvector? (if b bv6? bv7?)) : CFalse -> #f) ; not a concrete type +(check-not-type (bitvector? integer?) : CFalse) ; not a bitvector type +(check-type (bitvector? 3) : CFalse -> #f) ; not a type + +;; bv? +(check-type (bv? 1) : Bool -> #f) +(check-type (bv? (bv 1 1)) : Bool -> #t) +(check-type (bv? (bv 2 2)) : Bool -> #t) +;define-symbolic b boolean?) +(check-type (bv? (if b (bv 3 6) #t)) : Bool -> b) + +;; 4.3.1 Comparison Ops +(define-symbolic u v (bitvector 7)) ; symbolic bitvector constants +(check-type (bvslt (bv 4 7) (bv -1 7)) : Bool -> #f) ; signed 7-bit < of 4 and -1 +(check-type (bvult (bv 4 7) (bv -1 7)) : Bool -> #t) ; unsigned 7-bit < of 4 and -1 +;(define-symbolic b boolean?) +(check-type (bvsge u (if b v (bv 3 4))) : Bool -> (bvsle v u)) ; b must be true, else err +(check-type (asserts) : (CListof Bool) -> (list b)) ; so Rosette emits assertion +(clear-asserts!) + +;; 4.3.2 Bitwise Ops +(check-type (bvnot (bv -1 4)) : BV -> (bv 0 4)) +(check-type (bvnot (bv 0 4)) : BV -> (bv -1 4)) +;(define-symbolic b boolean?) +;; typed Rosette rejects this program +(typecheck-fail (bvnot (if b 0 (bv 0 4))) + #:with-msg "expected BV, given \\(U Zero CBV\\)") +;; need assert-type annotation +(check-type (bvnot (assert-type (if b 0 (bv 0 4)) : BV)) : BV -> (bv -1 4)) +(check-type (asserts) : (CListof Bool) -> (list (! b))) +(clear-asserts!) + +(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?) +;; typed Rosette rejects this program +(typecheck-fail (bvand (bv -1 4) (if b 0 (bv 2 4))) + #:with-msg "expected BV, given \\(U Zero CBV\\)") +;; need assert-type annotation +(check-type (bvand (bv -1 4) (assert-type (if b 0 (bv 2 4)) : BV)) : BV -> (bv 2 4)) +(check-type (asserts) : (CListof Bool) -> (list (! b))) +(clear-asserts!) + +(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)) +;(define-symbolic b boolean?) +;; typed Rosette rejects this program +(typecheck-fail (bvshl (bv -1 4) (if b 0 (bv 2 4))) + #:with-msg "expected BV, given \\(U Zero CBV\\)") +;; need assert-type annotation +(check-type (bvshl (bv -1 4) (assert-type (if b 0 (bv 2 4)) : BV)) : BV -> (bv -4 4)) +(check-type (asserts) : CAsserts -> (list (! b))) +(clear-asserts!) + +;; 4.3.3 Arithmetic Ops +(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)) +(check-type (bvneg z) : BV -> (bvneg z)) + +(check-type (bvadd (bv -1 4) (bv 2 4)) : BV -> (bv 1 4)) +(check-type (bvsub (bv 0 3) (bv 1 3)) : BV -> (bv -1 3)) +(check-type (bvmul (bv -1 5) (bv 1 5)) : BV -> (bv -1 5)) +;> (define-symbolic b boolean?) +;; typed Rosette rejects this program +(typecheck-fail (bvadd (bv -1 4) (bv 2 4) (if b (bv 1 4) "bad")) + #:with-msg "expected.*BV.*given.*\\(U CBV String\\)") +;; need assert-type annotation +(check-type (bvadd (bv -1 4) (bv 2 4) (assert-type (if b (bv 1 4) "bad") : BV)) + : BV -> (bv 2 4)) +(check-type (asserts) : CAsserts -> (list b)) +(clear-asserts!) + +(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)) +;> (define-symbolic b boolean?) +;; typed Rosette rejects this program +(typecheck-fail (bvsrem (bv -3 4) (if b (bv 2 4) "bad")) + #:with-msg "expected.*BV.*given.*\\(U CBV String\\)") +;; need assert-type annotation +(check-type (bvsrem (bv -3 4) (assert-type (if b (bv 2 4) "bad") : BV)) + : BV -> (bv -1 4)) +(check-type (asserts) : CAsserts -> (list b)) +(clear-asserts!) + +;; 4.3.4 Conversion Ops +(check-type (concat (bv -1 4) (bv 0 1) (bv -1 3)) : BV -> (bv -9 8)) +;> (define-symbolic b boolean?) +(check-type (concat (bv -1 4) (if b (bv 0 1) (bv 0 2)) (bv -1 3)) + : BV); -> {[b (bv -9 8)] [(! b) (bv -25 9)]}) + +(check-type (extract 2 1 (bv -1 4)) : BV -> (bv -1 2)) +(check-type (extract 3 3 (bv 1 4)) : BV -> (bv 0 1)) +(define-symbolic i j integer?) +(check-type (extract i j (bv 1 2)) : BV -> (extract i j (bv 1 2))) + ; -> {[(&& (= 0 j) (= 1 i)) (bv 1 2)] ...} +(check-type (asserts) : CAsserts -> (list (< i 2) (<= 0 j) (<= j i))) +(clear-asserts!) + +(check-type (sign-extend (bv -3 4) (bitvector 6)) : BV -> (bv -3 6)) +(check-type (zero-extend (bv -3 4) (bitvector 6)) : BV -> (bv 13 6)) +(define-symbolic c boolean?) +(check-type (zero-extend (bv -3 4) (if b (bitvector 5) (bitvector 6))) + : BV -> (zero-extend (bv -3 4) (if b (bitvector 5) (bitvector 6)))) +; {[b (bv 13 5)] [(! b) (bv 13 6)]}) +;; typed Rosette rejects this program +(typecheck-fail (zero-extend (bv -3 4) (if b (bitvector 5) "bad")) + #:with-msg "expected.*BVPred.*given.*\\(U CBVPred String\\)") +;; need assert-type annotation +(check-type (zero-extend (bv -3 4) (assert-type (if b (bitvector 5) "bad") : BVPred)) + : BV -> (bv 13 5)) +(check-type (asserts) : CAsserts -> (list b)) +(check-type (zero-extend (bv -3 4) (if c (bitvector 5) (bitvector 1))) : BV -> (bv 13 5)) +(check-type (asserts) : CAsserts -> (list c b)) +(clear-asserts!) + +(check-type (bitvector->integer (bv -1 4)) : Int -> -1) +(check-type (bitvector->natural (bv -1 4)) : Nat -> 15) +;> (define-symbolic b boolean?) +(check-type (bitvector->integer (if b (bv -1 3) (bv -3 4))) : Int -> (if b -1 -3)) +;; typed Rosette rejects this program +(typecheck-fail (bitvector->integer (if b (bv -1 3) "bad")) + #:with-msg "expected.*BV.*given.*\\(U CBV String\\)") +;; need assert-type annotation +(check-type (bitvector->integer (assert-type (if b (bv -1 3) "bad") : BV)) : Int -> -1) +(check-type (asserts) : CAsserts -> (list b)) +(clear-asserts!) + +(check-type (integer->bitvector 4 (bitvector 2)) : BV -> (bv 0 2)) +(check-type (integer->bitvector 15 (bitvector 4)) : BV -> (bv -1 4)) +;> (define-symbolic b c boolean?) +;; typed Rosette rejects this program +(typecheck-fail (integer->bitvector (if b pi 3) (if c (bitvector 5) (bitvector 6))) + #:with-msg "expected Int, given.*Num") +(check-type (if b pi 3) : Num) +(check-not-type (if b pi 3) : Int) +;; need assert-type annotation +(define res (integer->bitvector (assert-type (if b pi 3) : Int) + (if c (bitvector 5) (bitvector 6)))) +(check-type res : BV) ;{[c (bv 3 5)] [(! c) (bv 3 6)]}) +(check-type (asserts) : CAsserts -> (list (! b))) diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt index 07b9247..20d9a30 100644 --- a/turnstile/examples/tests/rosette/rosette2-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette2-tests.rkt @@ -137,7 +137,7 @@ (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) 1) : Bool -> #f) (check-type ((bitvector 4) (bv 10 (bitvector 4))) : Bool) (check-type (bitvector? "2") : Bool -> #f) @@ -265,9 +265,10 @@ ;; CBV input annotation on arg is too restrictive to work as BVPred (typecheck-fail ((λ ([bvp : BVPred]) bvp) (λ ([bv : CBV]) #t)) #:with-msg "expected BVPred.*given.*CBV") -(check-type ((λ ([bvp : BVPred]) bvp) (λ ([bv : BV]) #t)) : BVPred) -;; this should pass, but will not if BVPred is a case-> -(check-type ((λ ([bvp : BVPred]) bvp) (λ ([bv : BV]) ((bitvector 2) bv))) : BVPred) +(typecheck-fail ((λ ([bvp : BVPred]) bvp) (λ ([bv : BV]) #t)) + #:with-msg "expected BVPred.*given.*BV") +;; BVpred arg must have Any input type +(check-type ((λ ([bvp : BVPred]) bvp) (λ ([bv : Any]) ((bitvector 2) bv))) : BVPred) ;; assert-type tests (check-type+asserts (assert-type (sub1 10) : PosInt) : PosInt -> 9 (list))