rosette-tests.rkt (5575B)
1 #lang s-exp "../../rosette/rosette.rkt" 2 (require "../rackunit-typechecking.rkt") 3 4 (check-type (sub1 10) : Nat -> 9) 5 (check-type (sub1 0) : NegInt -> -1) 6 (check-type (sub1 -1) : NegInt -> -2) 7 8 (check-type bv : (case-> (→ Int BVPred BV) 9 (→ Int PosInt BV))) 10 (typecheck-fail (bv "1" 2) #:with-msg "expected.*Int.*given.*String") 11 (check-type (bv 1 2) : BV -> (bv 1 (bvpred 2))) 12 (check-type (bv 1 (bvpred 2)) : BV -> (bv 1 (bvpred 2))) 13 14 (typecheck-fail (bv 0 0) #:with-msg "expected.*PosInt.*given.*Zero") 15 (check-type bitvector : (→ PosInt BVPred)) 16 (check-type (bitvector 3) : BVPred) 17 (typecheck-fail ((bitvector 4) 1)) 18 (check-type ((bitvector 4) (bv 10 (bvpred 4))) : Bool) 19 20 ;; same as above, but with bvpred 21 (check-type bvpred : (→ PosInt BVPred)) 22 (check-type (bvpred 3) : BVPred) 23 (typecheck-fail ((bvpred 4) 1)) 24 (check-type ((bvpred 4) (bv 10 (bvpred 4))) : Bool) 25 ;; typed rosette catches this during typechecking, 26 ;; whereas untyped rosette uses a runtime exn 27 (typecheck-fail (bvpred -1) #:with-msg "expected PosInt, given NegInt") 28 ;(check-runtime-exn (bvpred -1)) 29 30 (typecheck-fail (bitvector? "2")) 31 (check-type (bitvector? (bitvector 10)) : Bool -> #t) 32 (typecheck-fail (bvpred? "2")) 33 (check-type (bvpred? (bvpred 10)) : Bool -> #t) 34 35 ;; bvops 36 (check-type (bveq (bv 1 (bvpred 3)) (bv 1 (bvpred 3))) : Bool -> #t) 37 (typecheck-fail (bveq (bv 1 (bvpred 3)) 1)) 38 (check-type (bveq (bv 1 (bvpred 2)) (bv 1 (bvpred 3))) : Bool) ; -> runtime exn 39 (check-runtime-exn (bveq (bv 1 (bvpred 2)) (bv 1 (bvpred 3)))) 40 41 ;; non-primop bvops 42 (check-type (bvand (bv -1 (bvpred 4)) (bv 2 (bvpred 4))) : BV 43 -> (bv 2 (bvpred 4))) 44 (check-type (bvor (bv 0 (bvpred 3)) (bv 1 (bvpred 3))) : BV 45 -> (bv 1 (bvpred 3))) 46 (check-type (bvxor (bv -1 (bvpred 5)) (bv 1 (bvpred 5))) : BV 47 -> (bv -2 (bvpred 5))) 48 49 ;; examples from rosette guide 50 (check-type (bvand (bv -1 4) (bv 2 4)) : BV -> (bv 2 4)) 51 (check-type (bvor (bv 0 3) (bv 1 3)) : BV -> (bv 1 3)) 52 (check-type (bvxor (bv -1 5) (bv 1 5)) : BV -> (bv -2 5)) 53 54 (define-symbolic b boolean? : Bool) 55 (check-type (bvand (bv -1 4) (if b (bv 3 4) (bv 2 4))) : BV 56 -> (if b (bv 3 4) (bv 2 4))) 57 58 (check-type (bvshl (bv 1 4) (bv 2 4)) : BV -> (bv 4 4)) 59 (check-type (bvlshr (bv -1 3) (bv 1 3)) : BV -> (bv 3 3)) 60 (check-type (bvashr (bv -1 5) (bv 1 5)) : BV -> (bv -1 5)) 61 ;; TODO: see issue #23 62 (check-type (bvshl (bv -1 4) (if b (bv 3 4) (bv 2 4))) : BV) 63 64 (check-type (bvneg (bv -1 4)) : BV -> (bv 1 4)) 65 (check-type (bvneg (bv 0 4)) : BV -> (bv 0 4)) 66 (define-symbolic z (bitvector 3) : BV) 67 (check-type (bvneg z) : BV) 68 (check-type (bvadd (bv -1 4) (bv 2 4)) : BV -> (bv 1 4)) 69 (check-type (bvsub (bv 0 3) (bv 1 3)) : BV -> (bv -1 3)) 70 (check-type (bvmul (bv -1 5) (bv 1 5)) : BV -> (bv -1 5)) 71 ;; TODO: see issue #23 72 (check-type (bvadd (bv -1 4) (bv 2 4) (if b (bv 1 4) (bv 3 4))) : BV) 73 (check-type (bvsdiv (bv -3 4) (bv 2 4)) : BV -> (bv -1 4)) 74 (check-type (bvudiv (bv -3 3) (bv 2 3)) : BV -> (bv 2 3)) 75 (check-type (bvsmod (bv 1 5) (bv 0 5)) : BV -> (bv 1 5)) 76 (check-type (bvsrem (bv -3 4) (if b (bv 2 4) (bv 3 4))) : BV 77 -> (if b (bv -1 4) (bv 0 4))) 78 79 (check-type (concat (bv -1 4) (bv 0 1) (bv -1 3)) : BV -> (bv -9 8)) 80 (check-type (concat (bv -1 4) (if b (bv 0 1) (bv 0 2)) (bv -1 3)) : BV 81 -> (if b (bv -9 8) (bv -25 9))) 82 83 (check-type (extract 2 1 (bv -1 4)) : BV -> (bv -1 2)) 84 (check-type (extract 3 3 (bv 1 4)) : BV -> (bv 0 1)) 85 (define-symbolic i j integer? : Int) 86 (check-type (extract i j (bv 1 2)) : BV) 87 ; -> {[(&& (= 0 j) (= 1 i)) (bv 1 2)] ...}) 88 89 (check-type (sign-extend (bv -3 4) (bitvector 6)) : BV -> (bv -3 6)) 90 (check-type (zero-extend (bv -3 4) (bitvector 6)) : BV -> (bv 13 6)) 91 (define-symbolic c boolean? : Bool) 92 (check-type (zero-extend (bv -3 4) (if b (bitvector 5) (bitvector 6))) 93 : BV -> (if b (bv 13 5) (bv 13 6))) 94 #;(check-type (zero-extend (bv -3 4) (if b (bitvector 5) "bad")) 95 : BV -> (bv 13 5)) 96 (check-type (zero-extend (bv -3 4) (if c (bitvector 5) (bitvector 1))) 97 : BV -> (bv 13 5)) 98 99 (check-type (bitvector->integer (bv -1 4)) : Int -> -1) 100 (check-type (bitvector->natural (bv -1 4)) : Int -> 15) 101 (check-type (bitvector->integer (if b (bv -1 3) (bv -3 4))) 102 : Int -> (if b -1 -3)) 103 ;(check-type (bitvector->integer (if b (bv -1 3) "bad")) : BV -> -1) 104 (check-type (integer->bitvector 4 (bitvector 2)) : BV -> (bv 0 2)) 105 (check-type (integer->bitvector 15 (bitvector 4)) : BV -> (bv -1 4)) 106 #;(check-type (integer->bitvector (if b pi 3) 107 (if c (bitvector 5) (bitvector 6))) 108 : BV -> {[c (bv 3 5)] [(! c) (bv 3 6)]}) 109 (check-type (integer->bitvector 3 110 (if c (bitvector 5) (bitvector 6))) 111 : BV -> (if c (bv 3 5) (bv 3 6))) 112 113 ;; case-> subtyping 114 (check-type ((λ ([f : (→ Int Int)]) (f 10)) add1) : Int -> 11) 115 (check-type ((λ ([f : (case-> (→ Int Int))]) (f 10)) add1) : Int -> 11) 116 (check-type ((λ ([f : (case-> (→ Nat Nat) 117 (→ Int Int))]) (f 10)) add1) : Int -> 11) 118 (check-not-type ((λ ([f : (case-> (→ Int Int))]) (f 10)) add1) : Nat) 119 (check-type ((λ ([f : (case-> (→ Nat Nat) 120 (→ Int Int))]) (f 10)) add1) : Nat -> 11) 121 (typecheck-fail ((λ ([f : (case-> (→ Zero Zero) 122 (→ Int Int))]) (f 10)) add1) 123 #:with-msg 124 (string-append "expected \\(case-> \\(→ Zero Zero\\) \\(→ Int Int\\)\\), " 125 "given \\(case-> \\(→ NegInt \\(U NegInt Zero\\)\\) \\(→ Zero PosInt\\) " 126 "\\(→ PosInt PosInt\\) \\(→ Nat PosInt\\) \\(→ Int Int\\)\\)")) 127