rosette2-tests.rkt (15285B)
1 #lang s-exp "../../rosette/rosette2.rkt" 2 (require "../rackunit-typechecking.rkt" 3 "check-type+asserts.rkt") 4 5 ;; subtyping among concrete 6 (check-type ((λ ([x : CPosInt]) x) ((λ ([x : CPosInt]) x) 1)) : CPosInt -> 1) 7 (check-type ((λ ([x : CZero]) x) ((λ ([x : CZero]) x) 0)) : CZero -> 0) 8 (check-type ((λ ([x : CNegInt]) x) ((λ ([x : CNegInt]) x) -1)) : CNegInt -> -1) 9 (check-type ((λ ([x : PosInt]) x) ((λ ([x : PosInt]) x) 1)) : PosInt -> 1) 10 (check-type ((λ ([x : Zero]) x) ((λ ([x : Zero]) x) 0)) : Zero -> 0) 11 (check-type ((λ ([x : NegInt]) x) ((λ ([x : NegInt]) x) -1)) : NegInt -> -1) 12 13 (check-type ((λ ([x : CNat]) x) ((λ ([x : CZero]) x) 0)) : CNat -> 0) 14 (check-type ((λ ([x : CNat]) x) ((λ ([x : CPosInt]) x) 1)) : CNat -> 1) 15 (check-type ((λ ([x : CNat]) x) ((λ ([x : CNat]) x) 1)) : CNat -> 1) 16 (typecheck-fail ((λ ([x : CPosInt]) x) ((λ ([x : CNat]) x) 1))) 17 (check-type ((λ ([x : Nat]) x) ((λ ([x : Zero]) x) 0)) : Nat -> 0) 18 (check-type ((λ ([x : Nat]) x) ((λ ([x : PosInt]) x) 1)) : Nat -> 1) 19 (check-type ((λ ([x : Nat]) x) ((λ ([x : Nat]) x) 1)) : Nat -> 1) 20 (typecheck-fail ((λ ([x : PosInt]) x) ((λ ([x : Nat]) x) 1))) 21 22 (check-type ((λ ([x : CInt]) x) ((λ ([x : CNegInt]) x) -1)) : CInt -> -1) 23 (check-type ((λ ([x : CInt]) x) ((λ ([x : CZero]) x) 0)) : CInt -> 0) 24 (check-type ((λ ([x : CInt]) x) ((λ ([x : CPosInt]) x) 1)) : CInt -> 1) 25 (check-type ((λ ([x : CInt]) x) ((λ ([x : CNat]) x) 1)) : CInt -> 1) 26 (check-type ((λ ([x : CInt]) x) ((λ ([x : CInt]) x) 1)) : CInt -> 1) 27 (typecheck-fail ((λ ([x : CPosInt]) x) ((λ ([x : CInt]) x) 1))) 28 (typecheck-fail ((λ ([x : CNat]) x) ((λ ([x : CInt]) x) 1))) 29 (check-type ((λ ([x : Int]) x) ((λ ([x : NegInt]) x) -1)) : Int -> -1) 30 (check-type ((λ ([x : Int]) x) ((λ ([x : Zero]) x) 0)) : Int -> 0) 31 (check-type ((λ ([x : Int]) x) ((λ ([x : PosInt]) x) 1)) : Int -> 1) 32 (check-type ((λ ([x : Int]) x) ((λ ([x : Nat]) x) 1)) : Int -> 1) 33 (check-type ((λ ([x : Int]) x) ((λ ([x : Int]) x) 1)) : Int -> 1) 34 (typecheck-fail ((λ ([x : PosInt]) x) ((λ ([x : Int]) x) 1))) 35 (typecheck-fail ((λ ([x : Nat]) x) ((λ ([x : Int]) x) 1))) 36 37 ;; illustrates flattening 38 (define-type-alias A Int) 39 (define-type-alias B CString) 40 (define-type-alias C Bool) 41 (define-type-alias AC (U A C)) 42 (define-type-alias BC (U B C)) 43 (define-type-alias A-BC (U A BC)) 44 (define-type-alias B-AC (U B AC)) 45 (check-type ((λ ([x : A-BC]) x) ((λ ([x : B-AC]) x) "1")) : A-BC -> "1") 46 (check-type ((λ ([x : A-BC]) x) ((λ ([x : AC]) x) #t)) : A-BC -> #t) 47 (check-type ((λ ([x : B-AC]) x) ((λ ([x : A-BC]) x) "1")) : A-BC -> "1") 48 (check-type ((λ ([x : B-AC]) x) ((λ ([x : BC]) x) "1")) : A-BC -> "1") 49 (typecheck-fail ((λ ([x : BC]) x) ((λ ([x : B-AC]) x) "1"))) 50 (typecheck-fail ((λ ([x : AC]) x) ((λ ([x : B-AC]) x) "1"))) 51 52 ;; subtyping between concrete and symbolic types 53 (check-type ((λ ([x : Int]) x) ((λ ([x : CInt]) x) 1)) : Int -> 1) 54 (typecheck-fail ((λ ([x : CInt]) x) ((λ ([x : Int]) x) 1))) 55 (check-type ((λ ([x : Bool]) x) ((λ ([x : CBool]) x) #t)) : Bool -> #t) 56 (typecheck-fail ((λ ([x : CBool]) x) ((λ ([x : Bool]) x) #t))) 57 (check-type ((λ ([x : (U CInt CBool)]) x) ((λ ([x : (CU CInt CBool)]) x) 1)) : (U CInt CBool)) 58 (typecheck-fail ((λ ([x : (CU CInt CBool)]) x) ((λ ([x : (U CInt CBool)]) x) 1))) 59 (check-type ((λ ([x : (U Int Bool)]) x) ((λ ([x : (U CInt CBool)]) x) 1)) : (U CInt CBool)) 60 (check-type ((λ ([x : (U CInt CBool)]) x) ((λ ([x : (U Int Bool)]) x) 1)) : (U CInt CBool)) 61 62 ;; add1 has a case-> type with cases for different subtypes of Int 63 ;; to preserve some of the type information through the operation 64 (check-type (add1 9) : CPosInt -> 10) 65 (check-type (add1 0) : CPosInt -> 1) 66 (check-type (add1 -1) : (CU CNegInt CZero) -> 0) 67 (check-type (add1 -9) : (CU CNegInt CZero) -> -8) 68 (check-type (add1 (ann 9 : PosInt)) : PosInt -> 10) 69 (check-type (add1 (ann 0 : Zero)) : PosInt -> 1) 70 (check-type (add1 (ann 9 : Nat)) : PosInt -> 10) 71 (check-type (add1 (ann 0 : Nat)) : PosInt -> 1) 72 (check-type (add1 (ann -1 : NegInt)) : (U NegInt Zero) -> 0) 73 (check-type (add1 (ann -9 : NegInt)) : (U NegInt Zero) -> -8) 74 (check-type (add1 (ann 9 : Int)) : Int -> 10) 75 76 ;; sub1 has a similar case-> type 77 (check-type (sub1 10) : CNat -> 9) 78 (check-type (sub1 0) : CNegInt -> -1) 79 (check-type (sub1 -1) : CNegInt -> -2) 80 (check-type (sub1 (ann 10 : PosInt)) : Nat -> 9) 81 (check-type (sub1 (ann 0 : Zero)) : NegInt -> -1) 82 (check-type (sub1 (ann -1 : NegInt)) : NegInt -> -2) 83 84 (check-type (+ 1 10) : CNat -> 11) 85 (check-type (+ -10 10) : CInt -> 0) 86 (check-type (+ (ann 1 : PosInt) (ann 10 : PosInt)) : Nat -> 11) 87 (check-type (+ (ann -10 : NegInt) (ann 10 : PosInt)) : Int -> 0) 88 89 ;; if tests 90 ;; if expr has concrete type only if test and both branches are concrete 91 (check-type (if #t 1 #f) : (CU CBool CInt)) 92 (check-type (if #t 1 #f) : (U CBool CInt)) 93 (check-type (if #t 1 #f) : (U Bool CInt)) 94 (check-type (if #t 1 #f) : (U Bool Int)) 95 (check-type (if #t 1 2) : CInt) 96 (check-type (if #t 1 2) : Int) 97 (check-type (if #t 1 2) : (CU CInt CBool)) 98 (check-type (if #t 1 2) : (U Int Bool)) 99 ;; non-bool test 100 (check-type (if 1 2 3) : CInt) 101 ;; else, if expr produces symbolic type 102 (define-symbolic b0 boolean? : Bool) 103 (define-symbolic i0 integer? : Int) 104 (check-type (if b0 1 2) : Int) 105 (check-not-type (if b0 1 2) : CInt) 106 (check-type (if #t i0 2) : Int) 107 (check-not-type (if #t i0 2) : CInt) 108 (check-type (if #t 2 i0) : Int) 109 (check-not-type (if #t 2 i0) : CInt) 110 (check-type (if b0 i0 2) : Int) 111 (check-type (if b0 1 #f) : (U CInt CBool)) 112 (check-type (if b0 1 #f) : (U Int Bool)) 113 ;; slightly unintuitive case: (U Int Bool) <: (U CInt Bool), ok for now (see notes) 114 (check-type (if #f i0 #f) : (U CInt CBool)) 115 (check-type (if #f i0 #f) : (U CInt Bool)) 116 (check-type (if #f i0 #f) : (U Int Bool)) 117 (check-type (if #f (+ i0 1) #f) : (U Int Bool)) 118 119 ;; BVs 120 121 (check-type bv : (Ccase-> (C→ CInt CBVPred CBV) 122 (C→ CInt CPosInt CBV))) 123 (typecheck-fail (bv "1" 2) #:with-msg "expected.*Int.*given.*String") 124 (check-type (bv 1 2) : CBV -> (bv 1 (bitvector 2))) 125 (check-type (bv 1 (bitvector 2)) : CBV -> (bv 1 (bitvector 2))) 126 (typecheck-fail (bv (ann 1 : Int) 2) #:with-msg "expected.*CInt") 127 (typecheck-fail (bv (ann 1 : Int) (bitvector 2)) #:with-msg "expected.*CInt") 128 129 (typecheck-fail (bv 0 0) #:with-msg "expected.*PosInt.*given.*Zero") 130 (check-type bitvector : (C→ CPosInt CBVPred)) 131 (check-type (bitvector 3) : CBVPred) 132 (typecheck-fail ((bitvector 4) 1)) 133 (check-type ((bitvector 4) (bv 10 (bitvector 4))) : Bool) 134 135 (check-type (bitvector? "2") : Bool -> #f) 136 (check-type (bitvector? (bitvector 10)) : Bool -> #t) 137 138 ;; bvops 139 (check-type (bveq (bv 1 3) (bv 1 3)) : Bool -> #t) 140 (typecheck-fail (bveq (bv 1 3) 1)) 141 (check-type (bveq (bv 1 2) (bv 1 3)) : Bool) ; -> runtime exn 142 (check-runtime-exn (bveq (bv 1 2) (bv 1 3))) 143 (clear-asserts!) 144 145 (check-type (bvand (bv -1 4) (bv 2 4)) : BV 146 -> (bv 2 4)) 147 (check-type (bvor (bv 0 3) (bv 1 3)) : BV 148 -> (bv 1 3)) 149 (check-type (bvxor (bv -1 5) (bv 1 5)) : BV 150 -> (bv -2 5)) 151 152 ;; examples from rosette guide 153 (check-type (bvand (bv -1 4) (bv 2 4)) : BV -> (bv 2 4)) 154 (check-type (bvor (bv 0 3) (bv 1 3)) : BV -> (bv 1 3)) 155 (check-type (bvxor (bv -1 5) (bv 1 5)) : BV -> (bv -2 5)) 156 157 (define-symbolic b boolean? : Bool) 158 (check-type (bvand (bv -1 4) (if b (bv 3 4) (bv 2 4))) : BV 159 -> (if b (bv 3 4) (bv 2 4))) 160 161 (check-type (bvshl (bv 1 4) (bv 2 4)) : BV -> (bv 4 4)) 162 (check-type (bvlshr (bv -1 3) (bv 1 3)) : BV -> (bv 3 3)) 163 (check-type (bvashr (bv -1 5) (bv 1 5)) : BV -> (bv -1 5)) 164 ;; TODO: see rosette issue #23 --- issue closed, won't fix 165 (check-type (bvshl (bv -1 4) (if b (bv 3 4) (bv 2 4))) : BV) 166 167 (check-type (bvneg (bv -1 4)) : BV -> (bv 1 4)) 168 (check-type (bvneg (bv 0 4)) : BV -> (bv 0 4)) 169 (define-symbolic z (bitvector 3) : BV) 170 (check-type (bvneg z) : BV) 171 (check-type (bvadd (bv -1 4) (bv 2 4)) : BV -> (bv 1 4)) 172 (check-type (bvsub (bv 0 3) (bv 1 3)) : BV -> (bv -1 3)) 173 (check-type (bvmul (bv -1 5) (bv 1 5)) : BV -> (bv -1 5)) 174 ;; TODO: see rosette issue #23 --- issue closed, won't fix 175 (check-type (bvadd (bvadd (bv -1 4) (bv 2 4)) (if b (bv 1 4) (bv 3 4))) : BV) 176 (check-type (bvsdiv (bv -3 4) (bv 2 4)) : BV -> (bv -1 4)) 177 (check-type (bvudiv (bv -3 3) (bv 2 3)) : BV -> (bv 2 3)) 178 (check-type (bvsmod (bv 1 5) (bv 0 5)) : BV -> (bv 1 5)) 179 (check-type (bvsrem (bv -3 4) (if b (bv 2 4) (bv 3 4))) : BV 180 -> (if b (bv -1 4) (bv 0 4))) 181 (check-type (concat (concat (bv -1 4) (bv 0 1)) (bv -1 3)) : BV -> (bv -9 8)) 182 (check-type (concat (concat (bv -1 4) (if b (bv 0 1) (bv 0 2))) (bv -1 3)) : BV 183 -> (if b (bv -9 8) (bv -25 9))) 184 185 (check-type (extract 2 1 (bv -1 4)) : BV -> (bv -1 2)) 186 (check-type (extract 3 3 (bv 1 4)) : BV -> (bv 0 1)) 187 (define-symbolic i j integer? : Int) 188 (check-type (extract i j (bv 1 2)) : BV) 189 ; -> {[(&& (= 0 j) (= 1 i)) (bv 1 2)] ...}) 190 191 (check-type (sign-extend (bv -3 4) (bitvector 6)) : BV -> (bv -3 6)) 192 (check-type (zero-extend (bv -3 4) (bitvector 6)) : BV -> (bv 13 6)) 193 (define-symbolic c boolean? : Bool) 194 (check-type (zero-extend (bv -3 4) (if b (bitvector 5) (bitvector 6))) 195 : BV -> (if b (bv 13 5) (bv 13 6))) 196 (check-type+asserts 197 (zero-extend (bv -3 4) (assert-type (if b (bitvector 5) "bad") : BVPred)) 198 : BV -> (bv 13 5) (list b)) 199 (check-type+asserts (zero-extend (bv -3 4) (if c (bitvector 5) (bitvector 1))) 200 : BV -> (bv 13 5) (list c)) 201 202 (check-type (bitvector->integer (bv -1 4)) : Int -> -1) 203 (check-type (bitvector->natural (bv -1 4)) : Int -> 15) 204 (check-type (bitvector->integer (if b (bv -1 3) (bv -3 4))) 205 : Int -> (if b -1 -3)) 206 (check-type+asserts 207 (bitvector->integer (assert-type (if b (bv -1 3) "bad") : BV)) 208 : Int -> -1 (list b)) 209 (check-type (integer->bitvector 4 (bitvector 2)) : BV -> (bv 0 2)) 210 (check-type (integer->bitvector 15 (bitvector 4)) : BV -> (bv -1 4)) 211 (check-type+asserts (integer->bitvector (assert-type (if b pi 3) : Int) 212 (if c (bitvector 5) (bitvector 6))) 213 : BV -> (integer->bitvector 3 (if c (bitvector 5) (bitvector 6))) 214 (list (not b))) 215 ;; TODO: check that CInt also has the right pred (do we want this?) 216 #;(check-type+asserts (integer->bitvector (assert-type (if b pi 3) : CInt) 217 (if c (bitvector 5) (bitvector 6))) 218 : BV -> (integer->bitvector 3 (if c (bitvector 5) (bitvector 6))) 219 (list (not b))) 220 (check-type (integer->bitvector 3 221 (if c (bitvector 5) (bitvector 6))) 222 : BV -> (if c (bv 3 5) (bv 3 6))) 223 224 ;; case-> subtyping 225 (check-type ((λ ([f : (C→ Int Int)]) (f 10)) add1) : Int -> 11) 226 (check-type ((λ ([f : (Ccase-> (C→ Int Int))]) (f 10)) add1) : Int -> 11) 227 (check-type ((λ ([f : (Ccase-> (C→ Nat Nat) 228 (C→ Int Int))]) (f 10)) add1) : Int -> 11) 229 (check-not-type ((λ ([f : (Ccase-> (C→ Int Int))]) (f 10)) add1) : Nat) 230 (check-type ((λ ([f : (Ccase-> (C→ Nat Nat) 231 (C→ Int Int))]) (f 10)) add1) : Nat -> 11) 232 (typecheck-fail ((λ ([f : (Ccase-> (C→ Zero Zero) 233 (C→ Int Int))]) (f 10)) add1) 234 #:with-msg 235 (string-append "expected \\(Ccase-> \\(C→ Zero Zero\\) \\(C→ Int Int\\)\\), " 236 "given \\(Ccase-> .*\\(C→ NegInt \\(U NegInt Zero\\)\\) .*\\(C→ Zero PosInt\\) " 237 ".*\\(C→ PosInt PosInt\\) .*\\(C→ Nat PosInt\\) .*\\(C→ Int Int\\)\\)")) 238 239 ;; applying symbolic function types 240 (check-type ((λ ([f : (U (C→ CInt CInt))]) (f 10)) add1) : Int -> 11) 241 ;; it's either (→ CInt CInt) or (→ CInt CBool), but not both, so 242 ;; add1 can have this type even though it never returns a boolean 243 (check-type ((λ ([f : (U (C→ CInt CInt) (C→ CInt CBool))]) (f 10)) add1) : (U Int Bool) -> 11) 244 (check-type ((λ ([f : (U (C→ CInt CInt) (C→ CInt Bool))]) (f 10)) 245 (if #t add1 positive?)) 246 : (U CInt Bool) -> 11) 247 (check-type ((λ ([f : (U (C→ CInt CInt) (C→ CInt Bool))]) (f 10)) 248 (if #t add1 positive?)) 249 : (U Int Bool) -> 11) 250 ;; concrete union of functions 251 (check-type ((λ ([f : (CU (C→ CInt CInt) (C→ CInt CBool))]) (f 10)) add1) : (CU CInt CBool) -> 11) 252 (check-type ((λ ([f : (CU (C→ CInt CInt) (C→ CInt CBool))]) (f 10)) 253 (if #t add1 positive?)) 254 : (CU CInt CBool) -> 11) 255 256 ;; check BVPred as type annotation 257 ;; CBV input annotation on arg is too restrictive to work as BVPred 258 (typecheck-fail ((λ ([bvp : BVPred]) bvp) (λ ([bv : CBV]) #t)) 259 #:with-msg "expected BVPred.*given.*CBV") 260 (check-type ((λ ([bvp : BVPred]) bvp) (λ ([bv : BV]) #t)) : BVPred) 261 ;; this should pass, but will not if BVPred is a case-> 262 (check-type ((λ ([bvp : BVPred]) bvp) (λ ([bv : BV]) ((bitvector 2) bv))) : BVPred) 263 264 ;; assert-type tests 265 (check-type+asserts (assert-type (sub1 10) : PosInt) : PosInt -> 9 (list)) 266 (check-runtime-exn (assert-type (sub1 1) : PosInt)) 267 (define-symbolic b1 b2 boolean? : Bool) 268 269 (check-type (clear-asserts!) : CUnit -> (void)) 270 ;; asserts directly on a symbolic union 271 (check-type+asserts (assert-type (if b1 1 #f) : Int) : Int -> 1 (list b1)) 272 (check-type+asserts (assert-type (if b2 1 #f) : Bool) : Bool -> #f (list (not b2))) 273 ;; asserts on the (pc) 274 (check-type+asserts (if b1 (assert-type 1 : Int) (assert-type #f : Int)) : Int 275 -> 1 (list b1)) 276 (check-type+asserts (if b2 (assert-type 1 : Bool) (assert-type #f : Bool)) : Bool 277 -> #f (list (not b2))) 278 ;; asserts on a define-symbolic value 279 (define-symbolic i1 integer? : Int) 280 (check-type+asserts (assert-type i1 : PosInt) : PosInt -> i1 (list (< 0 i1))) 281 (check-type+asserts (assert-type i1 : Zero) : Zero -> i1 (list (= 0 i1))) 282 (check-type+asserts (assert-type i1 : NegInt) : NegInt -> i1 (list (< i1 0))) 283 ;; TODO: should this assertion be equivalent to (<= 0 i1) ? 284 (check-type+asserts (assert-type i1 : Nat) : Nat -> i1 (list (not (< i1 0)))) 285 ;; asserts on other terms involving define-symbolic values 286 (check-type+asserts (assert-type (+ i1 1) : PosInt) : PosInt -> (+ 1 i1) (list (< 0 (+ 1 i1)))) 287 (check-type+asserts (assert-type (+ i1 1) : Zero) : Zero -> (+ 1 i1) (list (= 0 (+ 1 i1)))) 288 (check-type+asserts (assert-type (+ i1 1) : NegInt) : NegInt -> (+ 1 i1) (list (< (+ 1 i1) 0))) 289 290 (check-type+asserts (assert-type (if b1 i1 b2) : Int) : Int -> i1 (list b1)) 291 (check-type+asserts (assert-type (if b1 i1 b2) : Bool) : Bool -> b2 (list (not b1))) 292 ;; asserts on the (pc) 293 (check-type+asserts (if b1 (assert-type i1 : Int) (assert-type b2 : Int)) : Int 294 -> i1 (list b1)) 295 (check-type+asserts (if b1 (assert-type i1 : Bool) (assert-type b2 : Bool)) : Bool 296 -> b2 (list (not b1))) 297 ;; TODO: should assert-type cause some predicates to return true or return false? 298 (check-type+asserts (integer? (assert-type (if b1 i1 b2) : Int)) : Bool -> #t (list b1)) 299 (check-type+asserts (integer? (assert-type (if b1 i1 b2) : Bool)) : Bool -> #f (list (not b1))) 300 (check-type+asserts (boolean? (assert-type (if b1 i1 b2) : Int)) : Bool -> #f (list b1)) 301 (check-type+asserts (boolean? (assert-type (if b1 i1 b2) : Bool)) : Bool -> #t (list (not b1))) 302 303 (check-type (asserts) : (CListof Bool) -> (list))