start host lang param experiment
This commit is contained in:
Stephen Chang
parent
4f400b5e0a
commit
297e5df6ae
|
|
@ -76,7 +76,10 @@
|
|||
;; extract-filename : PathString -> String
|
||||
(define (extract-filename f)
|
||||
(path->string (path-replace-suffix (file-name-from-path f) "")))
|
||||
(define-syntax-parameter stx (syntax-rules ())))
|
||||
(define-syntax-parameter stx (syntax-rules ()))
|
||||
|
||||
;; parameter is an identifier transformer
|
||||
(define current-host-lang (make-parameter mk--)))
|
||||
|
||||
;; non-Turnstile define-typed-syntax
|
||||
;; TODO: potentially confusing? get rid of this?
|
||||
|
|
|
|||
97
turnstile/examples/rosette/bv3.rkt
Normal file
97
turnstile/examples/rosette/bv3.rkt
Normal file
|
|
@ -0,0 +1,97 @@
|
|||
#lang turnstile
|
||||
(extends "rosette3.rkt" ; extends typed rosette
|
||||
#:except bv bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge)
|
||||
(require (prefix-in ro: rosette)) ; untyped
|
||||
(require (only-in sdsl/bv/lang/bvops bvredand bvredor bv bv*)
|
||||
(prefix-in bv: (only-in sdsl/bv/lang/bvops BV)))
|
||||
(require sdsl/bv/lang/core (prefix-in bv: sdsl/bv/lang/form))
|
||||
|
||||
(provide Prog Lib
|
||||
(typed-out [bv : (Ccase-> (C→ CInt CBV)
|
||||
(C→ CInt CBVPred CBV)
|
||||
(C→ CInt CPosInt CBV))]
|
||||
[bv* : (Ccase-> (C→ BV)
|
||||
(C→ CBVPred BV))]
|
||||
[bvredor : (C→ BV BV)]
|
||||
[bvredand : (C→ BV BV)])
|
||||
current-bvpred define-fragment bvlib thunk)
|
||||
|
||||
;; this must be a macro in order to support Racket's overloaded set/get
|
||||
;; parameter patterns
|
||||
(define-typed-syntax current-bvpred
|
||||
[c-bvpred:id ≫
|
||||
--------
|
||||
[⊢ [_ ≫ bv:BV ⇒ : (CParamof CBVPred)]]]
|
||||
[(_) ≫
|
||||
--------
|
||||
[⊢ [_ ≫ (bv:BV) ⇒ : CBVPred]]]
|
||||
[(_ e) ≫
|
||||
[⊢ [e ≫ e- ⇐ : CBVPred]]
|
||||
--------
|
||||
[⊢ [_ ≫ (bv:BV e-) ⇒ : CUnit]]])
|
||||
|
||||
(define-syntax-rule (bv:bool->bv b)
|
||||
(ro:if b
|
||||
(bv (rosette3:#%datum . 1))
|
||||
(bv (rosette3:#%datum . 0))))
|
||||
|
||||
(define-simple-macro (define-comparators id ...)
|
||||
#:with (op ...) (stx-map (lambda (o) (format-id o "ro:~a" o)) #'(id ...))
|
||||
#:with (id/tc ...) (generate-temporaries #'(id ...))
|
||||
(begin-
|
||||
(define- (id x y) (bv:bool->bv (ro:#%app op x y))) ...
|
||||
(provide (rename-out [id/tc id] ...))
|
||||
(define-primop id/tc id (C→ BV BV BV)) ...))
|
||||
|
||||
(define-comparators bveq bvslt bvult bvsle bvule bvsgt bvugt bvsge bvuge)
|
||||
|
||||
(define-base-types Prog Lib)
|
||||
|
||||
(define-typed-syntax define-fragment
|
||||
[(_ (id param ...) #:implements spec #:library lib-expr) ≫
|
||||
--------
|
||||
[_ ≻ (define-fragment (id param ...)
|
||||
#:implements spec #:library lib-expr #:minbv (rosette3:#%datum . 4))]]
|
||||
[(_ (id param ...) #:implements spec #:library lib-expr #:minbv minbv) ≫
|
||||
[⊢ [spec ≫ spec- ⇒ : ty_spec]]
|
||||
#:fail-unless (C→? #'ty_spec) "spec must be a function"
|
||||
[⊢ [lib-expr ≫ lib-expr- ⇐ : Lib]]
|
||||
[⊢ [minbv ≫ minbv- ⇐ : Int]]
|
||||
#:with id-stx (format-id #'id "~a-stx" #'id #:source #'id)
|
||||
--------
|
||||
[_ ≻ (begin-
|
||||
(define-values- (id-internal id-stx-internal)
|
||||
(bv:synthesize-fragment (id param ...)
|
||||
#:implements spec-
|
||||
#:library lib-expr-
|
||||
#:minbv minbv-))
|
||||
(define-syntax id
|
||||
(make-rename-transformer (⊢ id-internal : ty_spec)))
|
||||
(define-syntax id-stx
|
||||
(make-rename-transformer (⊢ id-stx-internal : CStx)))
|
||||
)]])
|
||||
|
||||
(define-typed-syntax bvlib
|
||||
[(_ [(~and ids (id ...)) n] ...) ≫
|
||||
#:fail-unless (stx-andmap brace? #'(ids ...))
|
||||
"given ops must be enclosed with braces"
|
||||
[⊢ [n ≫ n- ⇐ : Int] ...]
|
||||
[⊢ [id ≫ id- ⇒ : ty_id] ... ...]
|
||||
#:fail-unless (stx-andmap (lambda (t) (or (C→? t) (Ccase->? t))) #'(ty_id ... ...))
|
||||
"given op must be a function"
|
||||
;; 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"
|
||||
--------
|
||||
[⊢ [_ ≫ (bv:bvlib [{id- ...} n-] ...) ⇒ : Lib]]])
|
||||
|
||||
(begin-for-syntax
|
||||
(define BV* ((current-type-eval) #'BV))
|
||||
(define (τ⊑BV? τ)
|
||||
(typecheck? τ BV*)))
|
||||
|
||||
(define-syntax-rule (thunk e) (rosette3:λ () e))
|
||||
14
turnstile/examples/rosette/lib/angelic3.rkt
Normal file
14
turnstile/examples/rosette/lib/angelic3.rkt
Normal file
|
|
@ -0,0 +1,14 @@
|
|||
#lang turnstile
|
||||
(require
|
||||
(prefix-in t/ro: (only-in "../rosette3.rkt" U))
|
||||
(prefix-in ro: rosette/lib/angelic))
|
||||
(provide choose*)
|
||||
|
||||
(define-typed-syntax choose*
|
||||
[(ch e ...+) ≫
|
||||
[⊢ [e ≫ e- ⇒ : ty]] ...
|
||||
#:with (e/disarmed ...) (stx-map replace-stx-loc #'(e- ...) #'(e ...))
|
||||
--------
|
||||
;; the #'choose* identifier itself must have the location of its use
|
||||
;; see define-synthax implementation, specifically syntax/source in utils
|
||||
[⊢ [_ ≫ (#,(syntax/loc #'ch ro:choose*) e/disarmed ...) ⇒ : (t/ro:U ty ...)]]])
|
||||
23
turnstile/examples/rosette/lib/lift3.rkt
Normal file
23
turnstile/examples/rosette/lib/lift3.rkt
Normal file
|
|
@ -0,0 +1,23 @@
|
|||
#lang turnstile
|
||||
(require
|
||||
(prefix-in t/ro: (only-in "../rosette3.rkt" U ~C→ C→))
|
||||
(prefix-in ro: rosette/lib/lift))
|
||||
(provide define-lift)
|
||||
|
||||
(define-typed-syntax define-lift
|
||||
[(_ x:id [(pred? ...) racket-fn:id]) ≫
|
||||
[⊢ [pred? ≫ pred?- ⇒ : (t/ro:~C→ _ ...)]] ...
|
||||
[⊢ [racket-fn ≫ racket-fn- ⇒ : (t/ro:~C→ ty1 ty2)]]
|
||||
#:with y (generate-temporary #'x)
|
||||
--------
|
||||
[_ ≻ (begin-
|
||||
(define-syntax- x (make-rename-transformer (⊢ y : (t/ro:C→ (t/ro:U ty1) (t/ro:U ty2)))))
|
||||
(ro:define-lift y [(pred?- ...) racket-fn-]))]]
|
||||
[(_ x:id [pred? racket-fn:id]) ≫
|
||||
[⊢ [pred? ≫ pred?- ⇒ : (t/ro:~C→ _ ...)]]
|
||||
[⊢ [racket-fn ≫ racket-fn- ⇒ : (t/ro:~C→ ty1 ty2)]]
|
||||
#:with y (generate-temporary #'x)
|
||||
--------
|
||||
[_ ≻ (begin-
|
||||
(define-syntax- x (make-rename-transformer (⊢ y : (t/ro:C→ (t/ro:U ty1) (t/ro:U ty2)))))
|
||||
(ro:define-lift y [pred?- racket-fn-]))]])
|
||||
17
turnstile/examples/rosette/lib/render3.rkt
Normal file
17
turnstile/examples/rosette/lib/render3.rkt
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
#lang turnstile
|
||||
(require
|
||||
(prefix-in t/ro: (only-in "../rosette3.rkt" CNat CSolution CPict))
|
||||
(prefix-in ro: rosette/lib/render))
|
||||
(provide render)
|
||||
|
||||
(define-typed-syntax render
|
||||
[(_ s) ≫
|
||||
[⊢ [s ≫ s- ⇐ : t/ro:CSolution]]
|
||||
--------
|
||||
[⊢ [_ ≫ (ro:render s-) ⇒ : t/ro:CPict]]]
|
||||
[(_ s sz) ≫
|
||||
[⊢ [s ≫ s- ⇐ : t/ro:CSolution]]
|
||||
[⊢ [sz ≫ sz- ⇐ : t/ro:CNat]]
|
||||
--------
|
||||
[⊢ [_ ≫ (ro:render s- sz-) ⇒ : t/ro:CPict]]])
|
||||
|
||||
80
turnstile/examples/rosette/lib/synthax3.rkt
Normal file
80
turnstile/examples/rosette/lib/synthax3.rkt
Normal file
|
|
@ -0,0 +1,80 @@
|
|||
#lang turnstile
|
||||
(require
|
||||
(only-in "../rosette3.rkt" rosette-typed-out)
|
||||
(prefix-in
|
||||
t/ro:
|
||||
(only-in "../rosette3.rkt" U Int Bool C→ CSolution Unit CSyntax CListof))
|
||||
(prefix-in ro: rosette/lib/synthax))
|
||||
|
||||
(provide (rosette-typed-out [print-forms : (t/ro:C→ t/ro:CSolution t/ro:Unit)])
|
||||
??)
|
||||
|
||||
(provide generate-forms choose)
|
||||
|
||||
(define-typed-syntax ??
|
||||
[(qq) ≫
|
||||
#:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq)
|
||||
--------
|
||||
[⊢ [_ ≫ (??/progsrc) ⇒ : t/ro:Int]]]
|
||||
[(qq pred?) ≫
|
||||
#:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq)
|
||||
[⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]]
|
||||
#:fail-unless (syntax-e #'s?)
|
||||
(format "Expected a Rosette-solvable type, given ~a."
|
||||
(syntax->datum #'pred?))
|
||||
#:fail-when (syntax-e #'f?)
|
||||
(format "Expected a non-function Rosette type, given ~a."
|
||||
(syntax->datum #'pred?))
|
||||
--------
|
||||
[⊢ [_ ≫ (??/progsrc pred?-) ⇒ : ty]]])
|
||||
|
||||
(define-syntax print-forms
|
||||
(make-variable-like-transformer
|
||||
(assign-type #'ro:print-forms #'(t/ro:C→ t/ro:CSolution t/ro:Unit))))
|
||||
|
||||
(define-syntax generate-forms
|
||||
(make-variable-like-transformer
|
||||
(assign-type #'ro:generate-forms #'(t/ro:C→ t/ro:CSolution (t/ro:CListof t/ro:CSyntax)))))
|
||||
|
||||
(define-typed-syntax choose
|
||||
[(ch e ...+) ≫
|
||||
[⊢ [e ≫ e- ⇒ : ty]] ...
|
||||
#:with (e/disarmed ...) (stx-map replace-stx-loc #'(e- ...) #'(e ...))
|
||||
--------
|
||||
;; the #'choose identifier itself must have the location of its use
|
||||
;; see define-synthax implementation, specifically syntax/source in utils
|
||||
[⊢ [_ ≫ (#,(syntax/loc #'ch ro:choose) e/disarmed ...) ⇒ : (t/ro:U ty ...)]]])
|
||||
|
||||
;; TODO: not sure how to handle define-synthax
|
||||
;; it defines a macro, but may refer to itself in #:base and #:else
|
||||
;; - so must expand "be" and "ee", but what to do about self reference?
|
||||
;; - the current letrec-like implementation results in an #%app of the the f macro
|
||||
;; which isnt quite right
|
||||
#;(define-typed-syntax define-synthax #:datum-literals (: -> →)
|
||||
#;[(_ x:id ([pat e] ...+)) ≫
|
||||
[⊢ [e ≫ e- ⇒ : τ]] ...
|
||||
#:with y (generate-temporary #'x)
|
||||
--------
|
||||
[_ ≻ (begin-
|
||||
(define-syntax- x (make-rename-transformer (⊢ y : t/ro:Int)))
|
||||
(ro:define-synthax y ([pat e-] ...)))]]
|
||||
[(_ (f [x:id : ty] ... [k:id : tyk] -> ty_out) #:base be #:else ee) ≫
|
||||
#:with (e ...) #'(be ee)
|
||||
[() ([x ≫ x- : ty] ... [k ≫ k- : tyk] [f ≫ f- : (t/ro:C→ ty ... tyk ty_out)]) ⊢
|
||||
[e ≫ e- ⇒ : ty_e] ...]
|
||||
#:with (be- ee-) #'(e- ...)
|
||||
#:with f* (generate-temporary)
|
||||
#:with app-f (format-id #'f "apply-~a" #'f)
|
||||
--------
|
||||
[_ ≻ (begin-
|
||||
(ro:define-synthax (f- x- ... k-) #:base be- #:else ee-)
|
||||
(define-syntax- app-f
|
||||
(syntax-parser
|
||||
[(_ . es)
|
||||
;; TODO: typecheck es
|
||||
#:with es- (stx-map expand/df #'es)
|
||||
; #:with es/fixsrc (stx-map replace-stx-loc #'es- #'es)
|
||||
(assign-type #'(f- . es) #'ty_out)])))]])
|
||||
; (⊢ f- : (t/ro:C→ ty ... tyk ty_out))
|
||||
; #;(ro:define-synthax (f- x- ... k-)
|
||||
; #:base be- #:else ee-))]])
|
||||
39
turnstile/examples/rosette/query/debug3.rkt
Normal file
39
turnstile/examples/rosette/query/debug3.rkt
Normal file
|
|
@ -0,0 +1,39 @@
|
|||
#lang turnstile
|
||||
(require
|
||||
(prefix-in t/ro: (only-in "../rosette3.rkt"
|
||||
λ ann begin C→ Nothing Bool CSolution))
|
||||
(prefix-in ro: rosette/query/debug))
|
||||
|
||||
(provide define/debug debug)
|
||||
|
||||
(define-typed-syntax define/debug #:datum-literals (: -> →)
|
||||
[(_ x:id e) ≫
|
||||
[⊢ [e ≫ e- ⇒ : τ]]
|
||||
#:with y (generate-temporary #'x)
|
||||
--------
|
||||
[_ ≻ (begin-
|
||||
(define-syntax- x (make-rename-transformer (⊢ y : τ)))
|
||||
(ro:define/debug y e-))]]
|
||||
[(_ (f [x : ty] ... (~or → ->) ty_out) e ...+) ≫
|
||||
; [⊢ [e ≫ e- ⇒ : ty_e]]
|
||||
#:with f- (generate-temporary #'f)
|
||||
--------
|
||||
[_ ≻ (begin-
|
||||
(define-syntax- f (make-rename-transformer (⊢ f- : (t/ro:C→ ty ... ty_out))))
|
||||
(ro:define/debug f-
|
||||
(t/ro:λ ([x : ty] ...)
|
||||
(t/ro:ann (t/ro:begin e ...) : ty_out))))]])
|
||||
|
||||
(define-typed-syntax debug
|
||||
[(_ (pred? ...+) e) ≫
|
||||
[⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]] ...
|
||||
#:fail-unless (stx-andmap syntax-e #'(s? ...))
|
||||
(format "Expected a Rosette-solvable type, given ~a."
|
||||
(syntax->datum #'(pred? ...)))
|
||||
#:fail-when (stx-ormap syntax-e #'(f? ...))
|
||||
(format "Expected a non-function Rosette type, given ~a."
|
||||
(syntax->datum #'(pred? ...)))
|
||||
[⊢ [e ≫ e- ⇒ : τ]]
|
||||
--------
|
||||
[⊢ [_ ≫ (ro:debug (pred?- ...) e-) ⇒ : t/ro:CSolution]]])
|
||||
|
||||
1789
turnstile/examples/rosette/rosette3.rkt
Normal file
1789
turnstile/examples/rosette/rosette3.rkt
Normal file
File diff suppressed because it is too large
Load Diff
404
turnstile/examples/tests/rosette/rosette3/bv-ref-tests.rkt
Normal file
404
turnstile/examples/tests/rosette/rosette3/bv-ref-tests.rkt
Normal file
|
|
@ -0,0 +1,404 @@
|
|||
#lang s-exp "../../../rosette/bv3.rkt"
|
||||
(require syntax/parse/define
|
||||
(only-in racket/base for-syntax) (for-syntax racket/base))
|
||||
(require "../../rackunit-typechecking.rkt")
|
||||
|
||||
; The 25 Hacker's Delight benchmarks from the following paper:
|
||||
; Sumit Gulwani, Susmit Jha, Ashish Tiwari, and Ramarathnam Venkatesan.
|
||||
; 2011. Synthesis of loop-free programs. In Proceedings of the 32nd ACM
|
||||
; SIGPLAN Conference on Programming Language Design and Implementation (PLDI '11).
|
||||
;
|
||||
; The first 20 benchmarks are also used in the SyGuS competition: http://www.sygus.org
|
||||
|
||||
(current-bvpred (bitvector 32))
|
||||
|
||||
(check-type (thunk (bv 1)) : (C→ BV))
|
||||
|
||||
; Constants.
|
||||
(define bv1 (thunk (bv 1)))
|
||||
(define bv2 (thunk (bv 2)))
|
||||
(define bvsz (thunk (bv (sub1 (bitvector-size (current-bvpred))))))
|
||||
|
||||
(check-type bv1 : (C→ BV))
|
||||
(check-type (bv1) : BV -> (bv 1))
|
||||
(check-type ((bitvector 4) (bv1)) : Bool -> #f)
|
||||
(check-type ((bitvector 32) (bv1)) : Bool -> #t)
|
||||
(check-type bv2 : (C→ BV))
|
||||
(check-type bvsz : (C→ BV))
|
||||
|
||||
(check-type (bvsub (bv 1) (bv1)) : BV -> (bv 0))
|
||||
(check-type ((bitvector 32) (bvsub (bv 1) (bv1))) : Bool -> #t)
|
||||
|
||||
; Mask off the rightmost 1-bit.
|
||||
(define (p1 [x : BV] -> BV)
|
||||
(let* ([o1 (bvsub x (bv 1))]
|
||||
[o2 (bvand x o1)])
|
||||
o2))
|
||||
|
||||
(check-type (p1 (bv 1)) : BV -> (bv 0))
|
||||
(check-type ((bitvector 32) (p1 (bv 1))) : Bool -> #t)
|
||||
|
||||
; Test whether an unsigned integer is of the form 2^n-1.
|
||||
(define (p2 [x : BV] -> BV)
|
||||
(let* ([o1 (bvadd x (bv 1))]
|
||||
[o2 (bvand x o1)])
|
||||
o2))
|
||||
|
||||
; Isolate the right most 1-bit.
|
||||
(define (p3 [x : BV] -> BV)
|
||||
(let* ([o1 (bvneg x)]
|
||||
[o2 (bvand x o1)])
|
||||
o2))
|
||||
|
||||
; Form a mask that identifies the rightmost 1-bit and trailing 0s.
|
||||
(define (p4 [x : BV] -> BV)
|
||||
(let* ([o1 (bvsub x (bv 1))]
|
||||
[o2 (bvxor x o1)])
|
||||
o2))
|
||||
|
||||
; Right propagate rightmost 1-bit.
|
||||
(define (p5 [x : BV] -> BV)
|
||||
(let* ([o1 (bvsub x (bv 1))]
|
||||
[o2 (bvor x o1)])
|
||||
o2))
|
||||
|
||||
; Turn on the right-most 0-bit in a word.
|
||||
(define (p6 [x : BV] -> BV)
|
||||
(let* ([o1 (bvadd x (bv 1))]
|
||||
[o2 (bvor x o1)])
|
||||
o2))
|
||||
|
||||
; Isolate the right most 0 bit of a given bitvector.
|
||||
(define (p7 [x : BV] -> BV)
|
||||
(let* ([o1 (bvnot x)]
|
||||
[o2 (bvadd x (bv 1))]
|
||||
[o3 (bvand o1 o2)])
|
||||
o3))
|
||||
|
||||
; Form a mask that identifies the trailing 0s.
|
||||
(define (p8 [x : BV] -> BV)
|
||||
(let* ([o1 (bvsub x (bv 1))]
|
||||
[o2 (bvnot x)]
|
||||
[o3 (bvand o1 o2)])
|
||||
o3))
|
||||
|
||||
; Absolute value function.
|
||||
(define (p9 [x : BV] -> BV)
|
||||
(let* ([o1 (bvashr x (bv 31))]
|
||||
[o2 (bvxor x o1)]
|
||||
[o3 (bvsub o2 o1)])
|
||||
o3))
|
||||
|
||||
; Test if nlz(x) == nlz(y) where nlz is number of leading zeroes.
|
||||
(define (p10 [x : BV] [y : BV] -> BV)
|
||||
(let* ([o1 (bvand x y)]
|
||||
[o2 (bvxor x y)]
|
||||
[o3 (bvule o2 o1)])
|
||||
o3))
|
||||
|
||||
; Test if nlz(x) < nlz(y) where nlz is number of leading zeroes.
|
||||
(define (p11 [x : BV] [y : BV] -> BV)
|
||||
(let* ([o1 (bvnot y)]
|
||||
[o2 (bvand x o1)]
|
||||
[o3 (bvugt o2 y)])
|
||||
o3))
|
||||
|
||||
; Test if nlz(x) <= nlz(y) where nlz is number of leading zeroes.
|
||||
(define (p12 [x : BV] [y : BV] -> BV)
|
||||
(let* ([o1 (bvnot x)]
|
||||
[o2 (bvand y o1)]
|
||||
[o3 (bvule o2 x)])
|
||||
o3))
|
||||
|
||||
; Sign function.
|
||||
(define (p13 [x : BV] -> BV)
|
||||
(let* ([o1 (bvneg x)]
|
||||
[o2 (bvlshr o1 (bv 31))]
|
||||
[o3 (bvashr x (bv 31))]
|
||||
[o4 (bvor o2 o3)])
|
||||
o4))
|
||||
|
||||
; Floor of average of two integers without over-flowing.
|
||||
(define (p14 [x : BV] [y : BV] -> BV)
|
||||
(let* ([o1 (bvand x y)]
|
||||
[o2 (bvxor x y)]
|
||||
[o3 (bvlshr o2 (bv 1))]
|
||||
[o4 (bvadd o1 o3)])
|
||||
o4))
|
||||
|
||||
; Ceil of average of two integers without over-flowing.
|
||||
(define (p15 [x : BV] [y : BV] -> BV)
|
||||
(let* ([o1 (bvor x y)]
|
||||
[o2 (bvxor x y)]
|
||||
[o3 (bvlshr o2 (bv 1))]
|
||||
[o4 (bvsub o1 o3)])
|
||||
o4))
|
||||
|
||||
; The max function.
|
||||
(define (p16 [x : BV] [y : BV] -> BV)
|
||||
(if (equal? (bv 1) (bvsge x y)) x y))
|
||||
|
||||
; Turn-off the rightmost contiguous string of 1 bits.
|
||||
(define (p17 [x : BV] -> BV)
|
||||
(let* ([o1 (bvsub x (bv 1))]
|
||||
[o2 (bvor x o1)]
|
||||
[o3 (bvadd o2 (bv 1))]
|
||||
[o4 (bvand o3 x)])
|
||||
o4))
|
||||
|
||||
; Test whether an unsigned integer is of the form 2^n.
|
||||
(define (p18 [x : BV] -> BV)
|
||||
(let* ([o1 (bvsub x (bv 1))]
|
||||
[o2 (bvand o1 x)]
|
||||
[o3 (bvredor x)]
|
||||
[o4 (bvredor o2)]
|
||||
[o5 (bvnot o4)]
|
||||
[o6 (bvand o5 o3)])
|
||||
o6))
|
||||
|
||||
; Exchanging 2 fields A and B of the same register
|
||||
; x where m is mask which identifies field B and k
|
||||
; is number of bits from end of A to start of B.
|
||||
(define (p19 [x : BV] [m : BV] [k : BV] -> BV)
|
||||
(let* ([o1 (bvlshr x k)]
|
||||
[o2 (bvxor x o1)]
|
||||
[o3 (bvand o2 m)]
|
||||
[o4 (bvshl o3 k)]
|
||||
[o5 (bvxor o4 o3)]
|
||||
[o6 (bvxor o5 x)])
|
||||
o6))
|
||||
|
||||
; Next higher unsigned number with the same number of 1 bits.
|
||||
(define (p20 [x : BV] -> BV)
|
||||
(let* ([o1 (bvneg x)]
|
||||
[o2 (bvand x o1)]
|
||||
[o3 (bvadd x o2)]
|
||||
[o4 (bvxor x o2)]
|
||||
[o5 (bvlshr o4 (bv 2))]
|
||||
[o6 (bvudiv o5 o2)]
|
||||
[o7 (bvor o6 o3)])
|
||||
o7))
|
||||
|
||||
; Cycling through 3 values a, b, c.
|
||||
(define (p21 [x : BV] [a : BV] [b : BV] [c : BV] -> BV)
|
||||
(let* ([o1 (bveq x c)]
|
||||
[o2 (bvneg o1)]
|
||||
[o3 (bvxor a c)]
|
||||
[o4 (bveq x a)]
|
||||
[o5 (bvneg o4)]
|
||||
[o6 (bvxor b c)]
|
||||
[o7 (bvand o2 o3)]
|
||||
[o8 (bvand o5 o6)]
|
||||
[o9 (bvxor o7 o8)]
|
||||
[o10 (bvxor o9 c)])
|
||||
o10))
|
||||
|
||||
; Compute parity.
|
||||
(define (p22 [x : BV] -> BV)
|
||||
(let* ([o1 (bvlshr x (bv 1))]
|
||||
[o2 (bvxor o1 x)]
|
||||
[o3 (bvlshr o2 (bv 2))]
|
||||
[o4 (bvxor o2 o3)]
|
||||
[o5 (bvand o4 (bv #x11111111))]
|
||||
[o6 (bvmul o5 (bv #x11111111))]
|
||||
[o7 (bvlshr o6 (bv 28))]
|
||||
[o8 (bvand o7 (bv 1))])
|
||||
o8))
|
||||
|
||||
; Counting number of bits.
|
||||
(define (p23 [x : BV] -> BV)
|
||||
(let* ([o1 (bvlshr x (bv 1))]
|
||||
[o2 (bvand o1 (bv #x55555555))]
|
||||
[o3 (bvsub x o2)]
|
||||
[o4 (bvand o3 (bv #x33333333))]
|
||||
[o5 (bvlshr o3 (bv 2))]
|
||||
[o6 (bvand o5 (bv #x33333333))]
|
||||
[o7 (bvadd o4 o6)]
|
||||
[o8 (bvlshr o7 (bv 4))]
|
||||
[o9 (bvadd o8 o7)]
|
||||
[o10 (bvand o9 (bv #x0f0f0f0f))])
|
||||
o10))
|
||||
|
||||
; Round up to the next higher power of 2.
|
||||
(define (p24 [x : BV] -> BV)
|
||||
(let* ([o1 (bvsub x (bv 1))]
|
||||
[o2 (bvlshr o1 (bv 1))]
|
||||
[o3 (bvor o1 o2)]
|
||||
[o4 (bvlshr o3 (bv 2))]
|
||||
[o5 (bvor o3 o4)]
|
||||
[o6 (bvlshr o5 (bv 4))]
|
||||
[o7 (bvor o5 o6)]
|
||||
[o8 (bvlshr o7 (bv 8))]
|
||||
[o9 (bvor o7 o8)]
|
||||
[o10 (bvlshr o9 (bv 16))]
|
||||
[o11 (bvor o9 o10)]
|
||||
[o12 (bvadd o11 (bv 1))])
|
||||
o12))
|
||||
|
||||
; Compute higher order half of product of x and y.
|
||||
(define (p25 [x : BV] [y : BV] -> BV)
|
||||
(let* ([o1 (bvand x (bv #xffff))]
|
||||
[o2 (bvlshr x (bv 16))]
|
||||
[o3 (bvand y (bv #xffff))]
|
||||
[o4 (bvlshr y (bv 16))]
|
||||
[o5 (bvmul o1 o3)]
|
||||
[o6 (bvmul o2 o3)]
|
||||
[o7 (bvmul o1 o4)]
|
||||
[o8 (bvmul o2 o4)]
|
||||
[o9 (bvlshr o5 (bv 16))]
|
||||
[o10 (bvadd o6 o9)]
|
||||
[o11 (bvand o10 (bv #xffff))]
|
||||
[o12 (bvlshr o10 (bv 16))]
|
||||
[o13 (bvadd o7 o11)]
|
||||
[o14 (bvlshr o13 (bv 16))]
|
||||
[o15 (bvadd o14 o12)]
|
||||
[o16 (bvadd o15 o8)])
|
||||
o16))
|
||||
|
||||
(define-simple-macro (check-equal/rand/bv f)
|
||||
#:with out (syntax/loc this-syntax
|
||||
(check-equal/rand f #:process (λ ([x : CInt]) (bv x))))
|
||||
out)
|
||||
|
||||
;; Mask off the rightmost 1-bit. < 1 sec.
|
||||
(define-fragment (p1* x)
|
||||
#:implements p1
|
||||
#:library (bvlib [{bv1 bvand bvsub} 1]))
|
||||
|
||||
(check-equal/rand/bv p1)
|
||||
|
||||
; Test whether an unsigned integer is of the form 2^n-1. < 1 sec.
|
||||
(define-fragment (p2* x)
|
||||
#:implements p2
|
||||
#:library (bvlib [{bv1 bvand bvadd} 1]))
|
||||
|
||||
(check-equal/rand/bv p2)
|
||||
|
||||
; Isolate the right most 1-bit. < 1 sec.
|
||||
(define-fragment (p3* x)
|
||||
#:implements p3
|
||||
#:library (bvlib [{bvand bvneg} 1]))
|
||||
|
||||
(check-equal/rand/bv p3)
|
||||
|
||||
;; Form a mask that identifies the rightmost 1-bit and trailing 0s. < 1 sec.
|
||||
(define-fragment (p4* x)
|
||||
#:implements p4
|
||||
#:library (bvlib [{bv1 bvsub bvxor} 1]))
|
||||
|
||||
(check-equal/rand/bv p4)
|
||||
|
||||
; Right propagate rightmost 1-bit. < 1 sec.
|
||||
(define-fragment (p5* x)
|
||||
#:implements p5
|
||||
#:library (bvlib [{bv1 bvsub bvor} 1]))
|
||||
|
||||
(check-equal/rand/bv p5)
|
||||
|
||||
; Turn on the right-most 0-bit in a word. < 1 sec.
|
||||
(define-fragment (p6* x)
|
||||
#:implements p6
|
||||
#:library (bvlib [{bv1 bvor bvadd} 1]))
|
||||
|
||||
(check-equal/rand/bv p6)
|
||||
|
||||
; Isolate the right most 0 bit of a given bitvector. < 1 sec.
|
||||
(define-fragment (p7* x)
|
||||
#:implements p7
|
||||
#:library (bvlib [{bvand bvadd bvnot bv1} 1]))
|
||||
|
||||
(check-equal/rand/bv p7)
|
||||
|
||||
; Form a mask that identifies the trailing 0s. < 1 sec.
|
||||
(define-fragment (p8* x)
|
||||
#:implements p8
|
||||
#:library (bvlib [{bv1 bvsub bvand bvnot} 1]))
|
||||
|
||||
(check-equal/rand/bv p8)
|
||||
|
||||
; Absolute value function. ~ 1 sec.
|
||||
(define-fragment (p9* x)
|
||||
#:implements p9
|
||||
#:library (bvlib [{bvsz bvsub bvxor bvashr} 1]))
|
||||
|
||||
(check-equal/rand/bv p9)
|
||||
|
||||
; Test if nlz(x) == nlz(y) where nlz is number of leading zeroes. < 1 sec.
|
||||
(define-fragment (p10* x y)
|
||||
#:implements p10
|
||||
#:library (bvlib [{bvand bvxor bvule} 1]))
|
||||
|
||||
(check-equal/rand/bv p10)
|
||||
|
||||
; Test if nlz(x) < nlz(y) where nlz is number of leading zeroes. < 1 sec.
|
||||
(define-fragment (p11* x y)
|
||||
#:implements p11
|
||||
#:library (bvlib [{bvnot bvand bvugt} 1]))
|
||||
|
||||
(check-equal/rand/bv p11)
|
||||
|
||||
; Test if nlz(x) <= nlz(y) where nlz is number of leading zeroes. < 1 sec.
|
||||
(define-fragment (p12* x y)
|
||||
#:implements p12
|
||||
#:library (bvlib [{bvand bvnot bvule} 1]))
|
||||
|
||||
(check-equal/rand/bv p12)
|
||||
|
||||
; Sign function. ~ 1.4 sec.
|
||||
(define-fragment (p13* x)
|
||||
#:implements p13
|
||||
#:library (bvlib [{bvsz bvneg bvlshr bvashr bvor} 1])
|
||||
#:minbv 32)
|
||||
|
||||
(check-equal/rand/bv p13)
|
||||
|
||||
; Floor of average of two integers without over-flowing. ~ 2.5 sec.
|
||||
(define-fragment (p14* x y)
|
||||
#:implements p14
|
||||
#:library (bvlib [{bv1 bvand bvlshr bvxor bvadd} 1]))
|
||||
|
||||
(check-equal/rand/bv p14)
|
||||
|
||||
; Ceil of average of two integers without over-flowing. ~ 1 sec.
|
||||
(define-fragment (p15* x y)
|
||||
#:implements p15
|
||||
#:library (bvlib [{bv1 bvor bvlshr bvxor bvsub} 1]))
|
||||
|
||||
(check-equal/rand/bv p15)
|
||||
|
||||
; Compute max of two integers. Bug in the PLDI'11 paper: bvuge should be bvge.
|
||||
; ~ 1.3 sec.
|
||||
(define-fragment (p16* x y)
|
||||
#:implements p16
|
||||
#:library (bvlib [{bvneg bvsge bvand} 1] [{bvxor} 2]))
|
||||
|
||||
(check-equal/rand/bv p16)
|
||||
|
||||
; Turn-off the rightmost contiguous string of 1 bits. ~ 1.8 sec.
|
||||
(define-fragment (p17* x)
|
||||
#:implements p17
|
||||
#:library (bvlib [{bv1 bvand bvor bvadd bvsub} 1]))
|
||||
|
||||
(check-equal/rand/bv p17)
|
||||
|
||||
; Test whether an unsigned integer is of the form 2^n. ~ 1.6 sec.
|
||||
(define-fragment (p18* x)
|
||||
#:implements p18
|
||||
#:library (bvlib [{bvand bvredor} 2] [{bvsub bvnot bv1} 1]))
|
||||
|
||||
(check-equal/rand/bv p18)
|
||||
|
||||
; x where m is mask which identifies field B and k
|
||||
; is number of bits from end of A to start of B. ~ 3.5 sec.
|
||||
(define-fragment (p19* x m k)
|
||||
#:implements p19
|
||||
#:library (bvlib [{bvlshr bvshl bvand} 1] [{bvxor} 3]))
|
||||
|
||||
(check-equal/rand/bv p19)
|
||||
|
||||
; Next higher unsigned number with the same number of 1 bits. ~ 600 sec.
|
||||
(define-fragment (p20* x)
|
||||
#:implements p20
|
||||
#:library (bvlib [{bv2 bvneg bvand bvadd bvxor bvlshr bvudiv bvor} 1]))
|
||||
|
||||
(check-equal/rand/bv p20)
|
||||
30
turnstile/examples/tests/rosette/rosette3/bv-tests.rkt
Normal file
30
turnstile/examples/tests/rosette/rosette3/bv-tests.rkt
Normal file
|
|
@ -0,0 +1,30 @@
|
|||
#lang s-exp "../../../rosette/bv3.rkt"
|
||||
(require "../../rackunit-typechecking.rkt")
|
||||
|
||||
(check-type current-bvpred : (CParamof CBVPred))
|
||||
(check-type (current-bvpred) : BVPred -> (bitvector 4))
|
||||
(check-type (current-bvpred (bitvector 5)) : CUnit -> (void))
|
||||
(check-type (current-bvpred) : BVPred -> (bitvector 5))
|
||||
(check-type (current-bvpred (bitvector 4)) : CUnit -> (void))
|
||||
|
||||
(check-type (bv 1) : BV)
|
||||
(check-type ((bitvector 4) (bv 1)) : Bool -> #t)
|
||||
(check-type ((bitvector 1) (bv 1)) : Bool -> #f)
|
||||
(check-type (bv 2 (bitvector 3)) : BV)
|
||||
(check-type ((bitvector 3) (bv 2 (bitvector 3))) : Bool -> #t)
|
||||
|
||||
(check-type (bv*) : BV)
|
||||
|
||||
(check-type (if 1 (bv 1) (bv 0)) : BV -> (bv 1))
|
||||
(check-type (if #f (bv 1) (bv 0)) : BV -> (bv 0))
|
||||
(define-symbolic i integer?)
|
||||
(define-symbolic b boolean?)
|
||||
(check-type (if i (bv 1) (bv 0)) : BV -> (bv 1))
|
||||
(check-type (if b (bv 1) (bv 0)) : BV -> (if b (bv 1) (bv 0)))
|
||||
|
||||
(check-type (bvredor (bv 1)) : BV)
|
||||
(check-type (bvredand (bv 1)) : BV)
|
||||
|
||||
(check-type bveq : (→ BV BV BV))
|
||||
(check-type (bveq (bv 1) (bv 1)) : BV -> (bv 1))
|
||||
(check-type (bveq (bv 1) (bv 0)) : BV -> (bv 0))
|
||||
|
|
@ -0,0 +1,17 @@
|
|||
#lang racket/base
|
||||
|
||||
(provide check-type+asserts)
|
||||
|
||||
(require turnstile/turnstile
|
||||
"../check-asserts.rkt"
|
||||
(only-in "../../../rosette/rosette3.rkt" CListof Bool CUnit))
|
||||
|
||||
(define-typed-syntax check-type+asserts #:datum-literals (: ->)
|
||||
[(_ e : τ-expected -> v asserts) ≫
|
||||
[⊢ [e ≫ e- ⇐ : τ-expected]]
|
||||
--------
|
||||
[⊢ [_ ≫ (check-equal?/asserts e-
|
||||
(add-expected v τ-expected)
|
||||
(add-expected asserts (CListof Bool)))
|
||||
⇒ : CUnit]]])
|
||||
|
||||
43
turnstile/examples/tests/rosette/rosette3/fsm-test.rkt
Normal file
43
turnstile/examples/tests/rosette/rosette3/fsm-test.rkt
Normal file
|
|
@ -0,0 +1,43 @@
|
|||
#lang s-exp "../../rosette/fsm3.rkt"
|
||||
(require "../../rackunit-typechecking.rkt")
|
||||
|
||||
(define m
|
||||
(automaton init
|
||||
[init : (c → more)]
|
||||
[more : (a → more)
|
||||
(d → more)
|
||||
(r → end)]
|
||||
[end : ]))
|
||||
|
||||
(define rx #px"^c[ad]+r$")
|
||||
|
||||
(typecheck-fail (automaton init)
|
||||
#:with-msg "initial state init is not declared state")
|
||||
(typecheck-fail (automaton init [init : (c → more)])
|
||||
#:with-msg "unbound identifier")
|
||||
(typecheck-fail (automaton init [init : (c → "more")])
|
||||
#:with-msg "expected State, given String")
|
||||
|
||||
(define M
|
||||
(automaton init
|
||||
[init : (c → (? s1 s2))]
|
||||
[s1 : (a → (? s1 s2 end reject))
|
||||
(d → (? s1 s2 end reject))
|
||||
(r → (? s1 s2 end reject))]
|
||||
[s2 : (a → (? s1 s2 end reject))
|
||||
(d → (? s1 s2 end reject))
|
||||
(r → (? s1 s2 end reject))]
|
||||
[end : ]))
|
||||
|
||||
|
||||
(check-type (M '(c a r)) : Bool) ; symbolic result
|
||||
(check-type (if (M '(c a r)) 1 2) : Int)
|
||||
|
||||
;; example commands
|
||||
(check-type (m '(c a r)) : Bool -> #t)
|
||||
(check-type (m '(c d r)) : Bool -> #t)
|
||||
(check-type (m '(c a d a r)) : Bool -> #t)
|
||||
(check-type (m '(c a d a)) : Bool -> #f)
|
||||
(check-type (verify-automaton m #px"^c[ad]+r$") : (List Symbol) -> '(c r))
|
||||
(check-type (debug-automaton m #px"^c[ad]+r$" '(c r)) : Pict)
|
||||
(check-type (synthesize-automaton M #px"^c[ad]+r$") : Unit)
|
||||
92
turnstile/examples/tests/rosette/rosette3/ifc-tests.rkt
Normal file
92
turnstile/examples/tests/rosette/rosette3/ifc-tests.rkt
Normal file
|
|
@ -0,0 +1,92 @@
|
|||
#lang s-exp "../../rosette/ifc3.rkt"
|
||||
(require "../../rackunit-typechecking.rkt")
|
||||
|
||||
#;(define (cex-case name ended? prog [k #f])
|
||||
(test-case name (check-pred EENI-witness? (verify-EENI* init ended? mem≈ prog k))))
|
||||
(define p0 (program 3 (list Halt Noop Push Pop Add* Load* Store*AB)))
|
||||
(check-type p0 : Prog)
|
||||
|
||||
;; expected:
|
||||
;; m0 initial:
|
||||
;; (machine [pc = 0@⊥]
|
||||
;; [stack = ()]
|
||||
;; [mem = (0@⊥ 0@⊥)]
|
||||
;; [insts = ((Push -16@⊥) (Push 1@⊤) (Store*AB))]
|
||||
;; m0 final:
|
||||
;; (machine [pc = 3@⊥]
|
||||
;; [stack = ()]
|
||||
;; [mem = (0@⊥ -16@⊥)]
|
||||
;; [insts = ((Push -16@⊥) (Push 1@⊤) (Store*AB))]
|
||||
;; m1 initial:
|
||||
;; (machine [pc = 0@⊥]
|
||||
;; [stack = ()]
|
||||
;; [mem = (0@⊥ 0@⊥)]
|
||||
;; [insts = ((Push -16@⊥) (Push 0@⊤) (Store*AB))]
|
||||
;; m1 final:
|
||||
;; (machine [pc = 3@⊥]
|
||||
;; [stack = ()]
|
||||
;; [mem = (-16@⊥ 0@⊥)]
|
||||
;; [insts = ((Push -16@⊥) (Push 0@⊤) (Store*AB))]
|
||||
(define w0 (verify-EENI* init halted? mem≈ p0 #f))
|
||||
(check-type w0 : Witness)
|
||||
(check-type (EENI-witness? w0) : Bool -> #t)
|
||||
|
||||
;; (define (valid-case name ended? prog [k #f])
|
||||
;; (test-case name (check-true (verify-EENI* init ended? mem≈ prog k))))
|
||||
|
||||
;; (define-syntax-rule (define-tests id desc expr ...)
|
||||
;; (define id
|
||||
;; (test-suite+
|
||||
;; desc
|
||||
;; (begin expr ...))))
|
||||
|
||||
;; ; Checks for counterexamples for bugs in basic semantics.
|
||||
;; (define-tests basic-bugs "IFC: counterexamples for bugs in basic semantics"
|
||||
;; (cex-case "Fig. 1" halted? (program 3 (list Halt Noop Push Pop Add* Load* Store*AB)))
|
||||
;; (cex-case "Fig. 2" halted? (program 3 (list Halt Noop Push Pop Add* Load* Store*B)))
|
||||
;; (cex-case "Fig. 3" halted? (program 5 (list Halt Noop Push Pop Add* Load* Store)))
|
||||
;; (cex-case "Fig. 4" halted? (program 7 (list Halt Noop Push Pop Add Load* Store))))
|
||||
|
||||
;; (define-tests basic-correct "IFC: no bounded counterexamples for correct basic semantics"
|
||||
;; (valid-case "*" halted? (program 7 (list Halt Noop Push Pop Add Load Store)))
|
||||
;; (valid-case "+" halted? (program 8 (list Halt Noop Push Pop Add Load Store))))
|
||||
|
||||
;; (define-tests jump-bugs "IFC: counterexamples for bugs in jump+basic semantics"
|
||||
;; (cex-case "11" halted? (program 6 (list Halt Noop Push Pop Add Load Store Jump*AB)))
|
||||
;; (cex-case "12" halted? (program 4 (list Halt Noop Push Pop Add Load Store Jump*B))))
|
||||
|
||||
;; (define-tests jump-correct "IFC: no bounded counterexamples for correct jump+basic semantics"
|
||||
;; (valid-case "**" halted? (program 7 (list Halt Noop Push Pop Add Load Store Jump)))
|
||||
;; (valid-case "++" halted? (program 8 (list Halt Noop Push Pop Add Load Store Jump))))
|
||||
|
||||
;; (define-tests call-return-bugs "IFC: counterexamples for buggy call+return+basic semantics"
|
||||
;; (cex-case "Fig. 13" halted∩low? (program 7 (list Halt Noop Push Pop Add Load Store Call*B Return*AB)))
|
||||
;; (cex-case "Fig. 15" halted∩low? (program 8 (list Halt Noop Push Pop Add Load StoreCR Call*B Return*AB)))
|
||||
;; (cex-case "Fig. 16" halted∩low? (program 8 (list Halt Noop Push Pop Add Load StoreCR Call*B Return*B)))
|
||||
;; (cex-case "Fig. 17" halted∩low? (program 10 (list Halt Noop Push Pop Add Load StoreCR Call Return))))
|
||||
|
||||
;; (define-tests reproduce-bugs "IFC: counterexamples that are structurally similar to those in prior work"
|
||||
;; (cex-case "Fig. 13*" halted∩low? (program (list Push Call*B Halt Push Push Store Return*AB)))
|
||||
;; (cex-case "Fig. 15*" halted∩low? (program (list Push Push Call*B Push StoreCR Halt Push Return*AB)))
|
||||
;; (cex-case "Fig. 16*" halted∩low? (program (list Push Push Call*B Push StoreCR Halt Return*B Push Return*B)))
|
||||
;; (cex-case "Fig. 17*"
|
||||
;; halted∩low?
|
||||
;; (program (list Push Call Push StoreCR Halt Push Push Call Pop Push Return))
|
||||
;; 13))
|
||||
|
||||
;; (define (fast-tests)
|
||||
;; (time (run-tests basic-bugs)) ; ~10 sec
|
||||
;; (time (run-tests basic-correct)) ; ~20 sec
|
||||
;; (time (run-tests jump-bugs))) ; ~7 sec
|
||||
|
||||
;; (define (slow-tests)
|
||||
;; (time (run-tests jump-correct)) ; ~52 sec
|
||||
;; (time (run-tests call-return-bugs)) ; ~440 sec
|
||||
;; (time (run-tests reproduce-bugs))) ; ~256 sec
|
||||
|
||||
;; (module+ fast
|
||||
;; (fast-tests))
|
||||
|
||||
;; (module+ test
|
||||
;; (fast-tests)
|
||||
;; (slow-tests))
|
||||
|
|
@ -0,0 +1,251 @@
|
|||
#lang s-exp "../../../rosette/rosette3.rkt"
|
||||
(require "../../rackunit-typechecking.rkt"
|
||||
"check-type+asserts.rkt")
|
||||
|
||||
;; all examples from the Rosette Guide, Sec 2
|
||||
|
||||
(define-symbolic b boolean?)
|
||||
(check-type b : Bool)
|
||||
(check-type (boolean? b) : Bool -> #t)
|
||||
(check-type (integer? b) : Bool -> #f)
|
||||
|
||||
;; TODO: fix these tests?
|
||||
(check-type (vector b 1) : (CMVectorof (U (Constant Bool) CPosInt)) -> (vector b 1))
|
||||
;; mut vectors are invariant
|
||||
(check-not-type (vector b 1) : (CMVectorof (U Bool CPosInt)))
|
||||
(check-not-type (vector b 1) : (CIVectorof (U Bool CPosInt)))
|
||||
(check-not-type (vector b 1) : (CMVectorof (CU CBool CPosInt)))
|
||||
(check-type (vector b 1) : (CMVectorof (U (Constant Bool) CPosInt)))
|
||||
;; mutable vectors are invariant
|
||||
(check-not-type (vector b 1) : (CMVectorof (U CBool CPosInt)))
|
||||
(check-not-type (vector b 1) : (CMVectorof (U Bool CInt)))
|
||||
|
||||
(check-type (vector b 1) : (CVectorof (U (Constant Bool) PosInt)))
|
||||
;; vectors are also invariant, because it includes mvectors
|
||||
(check-not-type (vector b 1) : (CVectorof (U Bool PosInt)))
|
||||
(check-not-type (vector b 1) : (CVectorof (U Bool CInt)))
|
||||
(check-not-type (vector b 1) : (CVectorof (U Bool Int)))
|
||||
|
||||
(check-type (not b) : Bool -> (! b))
|
||||
(check-type (boolean? (not b)) : Bool -> #t)
|
||||
|
||||
(define-symbolic* n integer?)
|
||||
|
||||
;; TODO: support internal definition contexts
|
||||
(define (static -> Bool)
|
||||
(let-symbolic (x boolean?) x))
|
||||
#;(define (static -> Bool)
|
||||
(define-symbolic x boolean? : Bool) ; creates the same constant when evaluated
|
||||
x)
|
||||
|
||||
(define (dynamic -> Int)
|
||||
(let-symbolic* (y integer?) y))
|
||||
#;(define (dynamic -> Int)
|
||||
(define-symbolic* y integer? : Int) ; creates a different constant when evaluated
|
||||
y)
|
||||
|
||||
(check-type static : (C→ Bool))
|
||||
(check-not-type static : (C→ CBool))
|
||||
(check-type dynamic : (C→ Int))
|
||||
(check-type dynamic : (C→ Num))
|
||||
(check-not-type dynamic : (C→ CInt))
|
||||
(check-type (eq? (static) (static)) : Bool -> #t)
|
||||
|
||||
(define sym*1 (dynamic))
|
||||
(define sym*2 (dynamic))
|
||||
(check-type (eq? sym*1 sym*2) : Bool -> (= sym*1 sym*2))
|
||||
|
||||
(define (yet-another-x -> Bool)
|
||||
(let-symbolic (x boolean?) x))
|
||||
|
||||
(check-type (eq? (static) (yet-another-x))
|
||||
: Bool -> (<=> (static) (yet-another-x)))
|
||||
|
||||
(check-type+asserts (assert #t) : Unit -> (void) (list))
|
||||
(check-runtime-exn (assert #f))
|
||||
|
||||
(check-type+asserts (assert (not b)) : Unit -> (void) (list (! b) #f))
|
||||
|
||||
(check-type (clear-asserts!) : Unit -> (void))
|
||||
(check-type (asserts) : (CListof Bool) -> (list))
|
||||
|
||||
;; sec 2.3
|
||||
(define (poly [x : Int] -> Int)
|
||||
(+ (* x x x x) (* 6 x x x) (* 11 x x) (* 6 x)))
|
||||
|
||||
(define (factored [x : Int] -> Int)
|
||||
(* x (+ x 1) (+ x 2) (+ x 2)))
|
||||
|
||||
(define (same [p : (C→ Int Int)] [f : (C→ Int Int)] [x : Int] -> Unit)
|
||||
(assert (= (p x) (f x))))
|
||||
|
||||
; check zeros; all seems well ...
|
||||
(check-type+asserts (same poly factored 0) : Unit -> (void) (list))
|
||||
(check-type+asserts (same poly factored -1) : Unit -> (void) (list))
|
||||
(check-type+asserts (same poly factored -2) : Unit -> (void) (list))
|
||||
|
||||
;; 2.3.1 Verification
|
||||
|
||||
(define-symbolic i integer?)
|
||||
(define cex (verify (same poly factored i)))
|
||||
(check-type cex : CSolution)
|
||||
(check-type (sat? cex) : Bool -> #t)
|
||||
(check-type (unsat? cex) : Bool -> #f)
|
||||
(check-type (evaluate i cex) : Int -> 12)
|
||||
(check-runtime-exn (same poly factored 12))
|
||||
(clear-asserts!)
|
||||
|
||||
;; 2.3.2 Debugging
|
||||
|
||||
(require "../../../rosette/query/debug3.rkt"
|
||||
"../../../rosette/lib/render3.rkt")
|
||||
(define/debug (factored/d [x : Int] -> Int)
|
||||
(* x (+ x 1) (+ x 2) (+ x 2)))
|
||||
|
||||
(define ucore (debug [integer?] (same poly factored/d 12)))
|
||||
(typecheck-fail (debug [positive?] (same poly factored/d 12))
|
||||
#:with-msg "Expected a Rosette-solvable type, given.*positive?")
|
||||
(typecheck-fail (debug [(~> integer? integer?)] (same poly factored/d 12))
|
||||
#:with-msg "Expected a non-function Rosette type, given.*~> integer\\? integer\\?")
|
||||
(check-type ucore : CSolution)
|
||||
;; TESTING TODO: requires visual inspection (in DrRacket)
|
||||
(check-type (render ucore) : CPict)
|
||||
|
||||
;; 2.3.3 Synthesis
|
||||
|
||||
(require "../../../rosette/lib/synthax3.rkt")
|
||||
(check-type (??) : Int)
|
||||
(check-type (?? boolean?) : Bool)
|
||||
(typecheck-fail (?? positive?)
|
||||
#:with-msg "Expected a Rosette-solvable type, given.*positive?")
|
||||
(typecheck-fail (?? (~> integer? integer?))
|
||||
#:with-msg "Expected a non-function Rosette type, given.*integer\\? integer\\?")
|
||||
|
||||
|
||||
(define (factored/?? [x : Int] -> Int)
|
||||
(* (+ x (??)) (+ x 1) (+ x (??)) (+ x (??))))
|
||||
|
||||
|
||||
(define binding
|
||||
(synthesize #:forall (list i)
|
||||
#:guarantee (same poly factored/?? i)))
|
||||
(check-type binding : CSolution)
|
||||
(check-type (sat? binding) : Bool -> #t)
|
||||
(check-type (unsat? binding) : Bool -> #f)
|
||||
;; TESTING TODO: requires visual inspection of stdout
|
||||
(check-type (print-forms binding) : Unit -> (void))
|
||||
;; typed/rosette should print:
|
||||
;; '(define (factored/?? (x : Int) -> Int) (* (+ x 3) (+ x 1) (+ x 2) (+ x 0)))
|
||||
;; (untyped) rosette should print:
|
||||
;; '(define (factored x) (* (+ x 3) (+ x 1) (+ x 2) (+ x 0)))
|
||||
|
||||
;; 2.3.4 Angelic Execution
|
||||
|
||||
(define-symbolic x y integer?)
|
||||
(define sol
|
||||
(solve (begin (assert (not (= x y)))
|
||||
(assert (< (abs x) 10))
|
||||
(assert (< (abs y) 10))
|
||||
(assert (not (= (poly x) 0)))
|
||||
(assert (= (poly x) (poly y))))))
|
||||
(check-type sol : CSolution)
|
||||
(check-type (sat? sol) : Bool -> #t)
|
||||
(check-type (unsat? sol) : Bool -> #f)
|
||||
(check-type (evaluate x sol) : Int -> -5)
|
||||
(check-type (evaluate y sol) : Int -> 2)
|
||||
(check-type (evaluate (poly x) sol) : Int -> 120)
|
||||
(check-type (evaluate (poly y) sol) : Int -> 120)
|
||||
|
||||
;; 2.4 Symbolic Reasoning
|
||||
|
||||
(define-symbolic x1 y1 real?)
|
||||
(check-type (current-bitwidth) : (CU CPosInt CFalse) -> 5)
|
||||
(check-type (current-bitwidth #f) : CUnit -> (void))
|
||||
(check-type (current-bitwidth) : (CU CPosInt CFalse) -> #f)
|
||||
(check-not-type (current-bitwidth) : CFalse)
|
||||
(typecheck-fail (current-bitwidth #t) #:with-msg "expected \\(CU CFalse CPosInt\\), given True")
|
||||
(typecheck-fail (current-bitwidth 0) #:with-msg "expected \\(CU CFalse CPosInt\\), given Zero")
|
||||
(typecheck-fail (current-bitwidth -1) #:with-msg "expected \\(CU CFalse CPosInt\\), given NegInt")
|
||||
(check-type (current-bitwidth 5) : CUnit -> (void))
|
||||
|
||||
; there is no solution under 5-bit signed integer semantics
|
||||
(check-type (solve (assert (= x1 3.5))) : CSolution -> (unsat))
|
||||
(check-type (solve (assert (= x1 64))) : CSolution -> (unsat))
|
||||
|
||||
; and quantifiers are not supported
|
||||
(check-runtime-exn (solve (assert (forall (list x1) (= x1 (+ x1 y1))))))
|
||||
;; expected err:
|
||||
;; finitize: cannot use (current-bitwidth 5) with a quantified formula
|
||||
;; (forall (x1) (= x1 (+ x1 y1))); use (current-bitwidth #f) instead
|
||||
|
||||
;; infinite precision semantics
|
||||
(current-bitwidth #f)
|
||||
|
||||
(define sol1 (solve (assert (= x1 3.5))))
|
||||
;; sol1 = (model [x1 7/2])
|
||||
(check-type sol1 : CSolution)
|
||||
(check-type (sat? sol1) : Bool -> #t)
|
||||
(check-type (evaluate x1 sol1) : Num -> 7/2)
|
||||
|
||||
(define sol2 (solve (assert (= x1 64))))
|
||||
;; sol2 = (model [x1 64.0])
|
||||
(check-type sol2 : CSolution)
|
||||
(check-type (sat? sol2) : Bool -> #t)
|
||||
(check-type (evaluate x1 sol2) : Num -> 64.0)
|
||||
|
||||
;; and quantifiers work
|
||||
(define sol3 (solve (assert (forall (list x1) (= x1 (+ x1 y1))))))
|
||||
;; sol3 = (model [y1 0.0])
|
||||
(check-type sol3 : CSolution)
|
||||
(check-type (sat? sol3) : Bool -> #t)
|
||||
(check-type (evaluate y1 sol3) : Num -> 0.0)
|
||||
|
||||
;; these examples uses symbolic lists
|
||||
(check-type
|
||||
(letrec ([[ones : (C→ Int (Listof Int))]
|
||||
(lambda ([n : Int])
|
||||
(if (<= n 0)
|
||||
(list)
|
||||
(cons 1 (ones (- n 1)))))])
|
||||
(printf "~a" (ones 3))
|
||||
(printf "~a" (ones x)))
|
||||
: Unit)
|
||||
|
||||
(check-type
|
||||
(letrec ([[ones : (C→ Int (Listof Int))]
|
||||
(lambda ([n : Int])
|
||||
(if (<= n 0)
|
||||
(list)
|
||||
(cons 1 (ones (- n 1)))))])
|
||||
(ones 3))
|
||||
: (Listof Int) -> (list 1 1 1))
|
||||
|
||||
;; inf loop
|
||||
(check-type
|
||||
(letrec ([[ones : (C→ Int (Listof Int))]
|
||||
(lambda ([n : Int])
|
||||
(if (<= n 0)
|
||||
(list)
|
||||
(cons 1 (ones (- n 1)))))])
|
||||
(ones x))
|
||||
: (Listof Int))
|
||||
|
||||
;; drop lambda annotation
|
||||
(check-type
|
||||
(letrec ([[ones : (C→ Int (Listof Int))]
|
||||
(lambda (n)
|
||||
(if (<= n 0)
|
||||
(list)
|
||||
(cons 1 (ones (- n 1)))))])
|
||||
(printf "~a" (ones 3))
|
||||
(printf "~a" (ones x)))
|
||||
: Unit)
|
||||
|
||||
(check-type
|
||||
(letrec ([[adder : (C→ (CListof Int) Int (CListof Int))]
|
||||
(lambda (vs n)
|
||||
(if (null? vs)
|
||||
(list)
|
||||
(cons (+ (car vs) n) (adder (cdr vs) n))))])
|
||||
(adder '(1 2 3) x))
|
||||
: (CListof Int) -> (list (+ 1 x) (+ 2 x) (+ 3 x)))
|
||||
|
|
@ -0,0 +1,120 @@
|
|||
#lang s-exp "../../../rosette/rosette3.rkt"
|
||||
(require "../../rackunit-typechecking.rkt"
|
||||
"check-type+asserts.rkt")
|
||||
|
||||
;; Examples from the Rosette Guide, Section 3
|
||||
|
||||
;; Symbolic effects
|
||||
(define y1 (ann 0 : Nat))
|
||||
(check-type (if #t (void) (set! y1 3)) : CUnit -> (void))
|
||||
;; y1 unchanged: 0
|
||||
(check-type y1 : Nat -> 0)
|
||||
(check-type (if #f (set! y1 3) (void)) : CUnit -> (void))
|
||||
;; y1 unchanged: 0
|
||||
(check-type y1 : Nat -> 0)
|
||||
;; symbolic effect!
|
||||
(define-symbolic x1 boolean?)
|
||||
(typecheck-fail (define-symbolic x1 boolean? : Bool))
|
||||
(check-type (if x1 (void) (set! y1 3)) : Unit -> (void))
|
||||
;; y1 symbolic: (ite x1 0 3)
|
||||
(check-type y1 : Nat -> (if x1 0 3))
|
||||
|
||||
|
||||
(define res
|
||||
(let ([y (ann 0 : Nat)])
|
||||
(if #t (void) (set! y 3))
|
||||
(printf "y unchanged: ~a\n" y)
|
||||
(if #f (set! y 3) (void))
|
||||
(printf "y unchanged: ~a\n" y)
|
||||
(let-symbolic (x boolean?)
|
||||
(if x (void) (set! y 3))
|
||||
(printf "y symbolic: ~a\n" y)
|
||||
(list x y))))
|
||||
|
||||
(check-type res : (CList Bool Nat))
|
||||
|
||||
(check-type (second res) : Nat -> (if (first res) 0 3))
|
||||
;; use car and cdr instead
|
||||
(check-type (car (cdr res)) : Nat -> (if (car res) 0 3))
|
||||
|
||||
;; 3.2 Solver-Aided Forms
|
||||
|
||||
;; 3.2.1 Symbolic Constants
|
||||
|
||||
(define (always-same -> Int)
|
||||
(let-symbolic (x integer?)
|
||||
x))
|
||||
(check-type (always-same) : Int)
|
||||
(check-type (eq? (always-same) (always-same)) : Bool -> #t)
|
||||
|
||||
(define (always-different -> Int)
|
||||
(let-symbolic* (x integer?)
|
||||
x))
|
||||
(check-type (always-different) : Int)
|
||||
(define diff-sym*1 (always-different))
|
||||
(define diff-sym*2 (always-different))
|
||||
(check-type (eq? diff-sym*1 diff-sym*2) : Bool -> (= diff-sym*1 diff-sym*2))
|
||||
|
||||
;; 3.2.2 Assertions
|
||||
|
||||
(check-type+asserts (assert #t) : Unit -> (void) (list))
|
||||
(check-type+asserts (assert 1) : Unit -> (void) (list))
|
||||
(define-symbolic x123 boolean?)
|
||||
(check-type+asserts (assert x123) : Unit -> (void) (list x123))
|
||||
(check-runtime-exn (assert #f "bad value"))
|
||||
|
||||
(check-type (asserts) : (CListof Bool) -> (list #f))
|
||||
(check-type (clear-asserts!) : Unit -> (void))
|
||||
(check-type (asserts) : (CListof Bool) -> (list))
|
||||
|
||||
;; 3.2.3 Angelic Execution
|
||||
(define-symbolic x y boolean?)
|
||||
(check-type (assert x) : Unit -> (void))
|
||||
(check-type (asserts) : (CListof Bool) -> (list x))
|
||||
(define solve-sol (solve (assert y)))
|
||||
(check-type solve-sol : CSolution)
|
||||
(check-type (sat? solve-sol) : Bool -> #t)
|
||||
(check-type (evaluate x solve-sol) : Bool -> #t) ; x must be true
|
||||
(check-type (evaluate y solve-sol) : Bool -> #t) ; y must be true
|
||||
(check-type (solve (assert (not x))) : CSolution -> (unsat))
|
||||
(clear-asserts!)
|
||||
|
||||
;; 3.2.4 Verification
|
||||
(check-type (assert x) : Unit -> (void))
|
||||
(check-type (asserts) : (CListof Bool) -> (list x))
|
||||
(define verif-sol (verify (assert y)))
|
||||
(check-type (asserts) : (CListof Bool) -> (list x))
|
||||
(check-type (evaluate x verif-sol) : Bool -> #t) ; x must be true
|
||||
(check-type (evaluate y verif-sol) : Bool -> #f) ; y must be false
|
||||
(check-type (verify #:assume (assert y) #:guarantee (assert (and x y)))
|
||||
: CSolution -> (unsat))
|
||||
(clear-asserts!)
|
||||
|
||||
;; 3.2.5 Synthesis
|
||||
(define-symbolic synth-x synth-c integer?)
|
||||
(check-type (assert (even? synth-x)) : Unit -> (void))
|
||||
(check-type (asserts) : (CListof Bool) -> (list (= 0 (remainder synth-x 2))))
|
||||
(define synth-sol
|
||||
(synthesize #:forall (list synth-x)
|
||||
#:guarantee (assert (odd? (+ synth-x synth-c)))))
|
||||
(check-type (asserts) : (CListof Bool) -> (list (= 0 (remainder synth-x 2))))
|
||||
(check-type (evaluate synth-x synth-sol) : Int -> synth-x) ; x is unbound
|
||||
(check-type (evaluate synth-c synth-sol) : Int -> 1) ; c must an odd integer
|
||||
(clear-asserts!)
|
||||
|
||||
;; 3.2.6 Optimization
|
||||
(current-bitwidth #f) ; use infinite-precision arithmetic
|
||||
(define-symbolic opt-x opt-y integer?)
|
||||
(check-type (assert (< opt-x 2)) : Unit -> (void))
|
||||
(check-type (asserts) : (CListof Bool) -> (list (< opt-x 2)))
|
||||
(define opt-sol
|
||||
(optimize #:maximize (list (+ opt-x opt-y))
|
||||
#:guarantee (assert (< (- opt-y opt-x) 1))))
|
||||
; assertion store same as before
|
||||
(check-type (asserts) : (CListof Bool) -> (list (< opt-x 2)))
|
||||
; x + y is maximal at x = 1 and y = 1
|
||||
(check-type (evaluate opt-x opt-sol) : Int -> 1)
|
||||
(check-type (evaluate opt-y opt-sol) : Int -> 1)
|
||||
|
||||
;; 3.2.8 Reasoning Precision
|
||||
;; see rosette-guide-sec2-tests.rkt, Sec 2.4 Symbolic Reasoning
|
||||
|
|
@ -0,0 +1,259 @@
|
|||
#lang s-exp "../../../rosette/rosette3.rkt"
|
||||
(require "../../rackunit-typechecking.rkt")
|
||||
|
||||
;; Examples from the Rosette Guide, Section 4.1 - 4.2
|
||||
|
||||
;; 4.1 Equality
|
||||
|
||||
;; should equal? produce CBool?
|
||||
;; (check-type (equal? 1 #t) : CBool -> #f)
|
||||
;; (check-type (equal? 1 1.0) : CBool -> #t)
|
||||
;; (check-type (equal? (list 1) (list 1.0)) : CBool -> #t)
|
||||
;; (check-type (equal? (box 1) (box 1)) : CBool -> #t)
|
||||
;; (check-type (equal? (box 1) (box 1.0)) : CBool -> #t)
|
||||
;; (check-type (equal? (list (box 1)) (list (box 1))) : CBool -> #t)
|
||||
;; (check-type (equal? (list (box 1)) (list (box 1.0))) : CBool -> #t)
|
||||
(check-type (equal? 1 #t) : Bool -> #f)
|
||||
(check-type (equal? 1 1.0) : Bool -> #t)
|
||||
(check-type (equal? (list 1) (list 1.0)) : Bool -> #t)
|
||||
(check-type (equal? (box 1) (box 1)) : Bool -> #t)
|
||||
(check-type (equal? (box 1) (box 1.0)) : Bool -> #t)
|
||||
(check-type (equal? (list (box 1)) (list (box 1))) : Bool -> #t)
|
||||
(check-type (equal? (list (box 1)) (list (box 1.0))) : Bool -> #t)
|
||||
|
||||
(define-symbolic n integer?)
|
||||
(check-type (equal? n 1) : Bool -> (= 1 n))
|
||||
(check-type (equal? (box n) (box 1)) : Bool -> (= 1 n))
|
||||
(check-not-type (equal? n 1) : CBool)
|
||||
(check-not-type (equal? (box n) (box 1)) : CBool)
|
||||
(typecheck-fail (~> positive? positive?)
|
||||
#:with-msg "Expected a Rosette\\-solvable type, given.*positive?")
|
||||
(typecheck-fail (~> (~> integer? integer?) integer?)
|
||||
#:with-msg "Expected a non\\-function Rosette type, given.*~> integer?")
|
||||
(define-symbolic f g (~> integer? integer?))
|
||||
(check-type f : (→ Int Int))
|
||||
(check-type g : (→ Int Int))
|
||||
(check-type (equal? f g) : Bool -> #f)
|
||||
(check-type (f 1) : Int -> (f 1))
|
||||
|
||||
(check-type (eq? 1 #t) : Bool -> #f)
|
||||
(check-type (eq? 1 1.0) : Bool -> #t) ; equal? transparent solvable values
|
||||
(check-type (eq? (list 1) (list 1.0)) : Bool -> #t) ; transparent immutable values with eq? contents
|
||||
(check-type (eq? (box 1) (box 1)) : Bool -> #f); but boxes are mutable, so eq? follows Racket
|
||||
(check-type (eq? (list (box 1)) (list (box 1))) : Bool -> #f)
|
||||
(check-type (eq? n 1) : Bool -> (= 1 n))
|
||||
(check-type (eq? (box n) (box 1)) : Bool -> #f)
|
||||
(check-type (eq? f g) : Bool -> #f) ; and procedures are opaque, so eq? follows Racket
|
||||
(check-type (eq? f f) : Bool -> #t)
|
||||
|
||||
(check-type (distinct?) : Bool -> #t)
|
||||
(check-type (distinct? 1) : Bool -> #t)
|
||||
(check-type (distinct? (list 1 2) (list 3) (list 1 2)) : Bool -> #f)
|
||||
(define-symbolic x y z integer?)
|
||||
(check-type (distinct? 3 z x y 2) : Bool -> (distinct? 2 3 x y z))
|
||||
(define-symbolic b boolean?)
|
||||
(check-type (distinct? 3 (bv 3 4) (list 1) (list x) y 2)
|
||||
: Bool -> (&& (! (= 3 y)) (&& (! (= 1 x)) (! (= 2 y)))))
|
||||
(clear-asserts!)
|
||||
|
||||
;; 4.2 Booleans, Integers, and Reals
|
||||
|
||||
;(define-symbolic b boolean?)
|
||||
(check-type (boolean? b) : Bool -> #t)
|
||||
(check-type (boolean? #t) : Bool -> #t)
|
||||
(check-type (boolean? #f) : Bool -> #t)
|
||||
(check-type (boolean? true) : Bool -> #t)
|
||||
(check-type (boolean? false) : Bool -> #t)
|
||||
(check-type (boolean? 1) : Bool -> #f)
|
||||
(check-type (not b) : Bool -> (! b))
|
||||
|
||||
(check-type (nand) : CFalse -> #f)
|
||||
(check-type (nand #t #t) : Bool -> #f)
|
||||
(check-type (nand 1 2) : Bool -> #f)
|
||||
(check-type (nor) : CTrue -> #t)
|
||||
(check-type (nor #f #f) : Bool -> #t)
|
||||
(check-type (nor 1 2) : Bool -> #f)
|
||||
|
||||
(check-type (nand #f #t) : Bool -> #t)
|
||||
(check-type (nand #f (error 'ack "we don't get here")) : Bool -> #t)
|
||||
(check-type (nor #f #t) : Bool -> #f)
|
||||
(check-type (nor #t (error 'ack "we don't get here")) : Bool -> #f)
|
||||
(check-type (implies #f #t) : Bool -> #t)
|
||||
(check-type (implies #f #f) : Bool -> #t)
|
||||
(check-type (implies #t #f) : Bool -> #f)
|
||||
(check-type (implies #f (error 'ack "we don't get here")) : Bool -> #t)
|
||||
;; (check-type (xor 11 #f) : Any -> 11)
|
||||
;; (check-type (xor #f 22) : Any -> 22)
|
||||
;; (check-type (xor 11 22) : Any -> #f)
|
||||
;; (check-type (xor #f #f) : Any -> #f)
|
||||
|
||||
(check-type +inf.0 : CFloat)
|
||||
(check-type -inf.0 : CFloat)
|
||||
(check-type +nan.0 : CFloat)
|
||||
(check-type -nan.0 : CFloat)
|
||||
|
||||
(check-type (number? 1) : Bool -> #t)
|
||||
(typecheck-fail (number? 2+3i) #:with-msg "Unsupported literal")
|
||||
(check-type (number? "hello") : Bool -> #f)
|
||||
(check-type (real? 1) : Bool -> #t)
|
||||
(check-type (real? +inf.0) : Bool -> #t)
|
||||
(typecheck-fail (real? 2+3i) #:with-msg "Unsupported literal")
|
||||
(typecheck-fail (real? 2.0+0.0i) #:with-msg "Unsupported literal")
|
||||
(check-type (real? "hello") : Bool -> #f)
|
||||
(check-type (integer? 1) : Bool -> #t)
|
||||
(check-type (integer? 2.3) : Bool -> #f)
|
||||
(check-type (integer? 4.0) : Bool -> #t)
|
||||
(check-type (integer? +inf.0) : Bool -> #f)
|
||||
(typecheck-fail (integer? 2+3i) #:with-msg "Unsupported literal")
|
||||
(check-type (integer? "hello") : Bool -> #f)
|
||||
(check-type (zero? 0) : CBool -> #t)
|
||||
(check-type (zero? -0.0) : CBool -> #t)
|
||||
(check-type (positive? 10) : CBool -> #t)
|
||||
(check-type (positive? -10) : CBool -> #f)
|
||||
(check-type (positive? 0.0) : CBool -> #f)
|
||||
(check-type (negative? 10) : CBool -> #f)
|
||||
(check-type (negative? -10) : CBool -> #t)
|
||||
(check-type (negative? -0.0) : CBool -> #f)
|
||||
(check-type (even? 10.0) : CBool -> #t)
|
||||
(check-type (even? 11) : CBool -> #f)
|
||||
(check-type +inf.0 : CNum)
|
||||
(typecheck-fail (even? +inf.0) #:with-msg "expected.*Int")
|
||||
(check-type (odd? 10.0) : Bool -> #f)
|
||||
(check-type (odd? 11) : Bool -> #t)
|
||||
(typecheck-fail (odd? +inf.0) #:with-msg "expected.*Int")
|
||||
(check-type (inexact->exact 1) : CNum -> 1)
|
||||
(check-type (inexact->exact 1.0) : CNum -> 1)
|
||||
(check-type (exact->inexact 1) : CNum -> 1.0)
|
||||
(check-type (exact->inexact 1.0) : CNum -> 1.0)
|
||||
|
||||
(check-type (+ 1 2) : CInt -> 3)
|
||||
(typecheck-fail (+ 1.0 2+3i 5) #:with-msg "Unsupported literal")
|
||||
(check-type (+) : CInt -> 0)
|
||||
(check-type (- 5 3.0) : CInt -> 2.0)
|
||||
(check-type (- 1) : CInt -> -1)
|
||||
(typecheck-fail (- 2+7i 1 3) #:with-msg "Unsupported literal")
|
||||
(check-type (* 2 3) : CInt -> 6)
|
||||
(check-type (* 8.0 9) : CInt -> 72.0)
|
||||
(typecheck-fail (* 1+2i 3+4i) #:with-msg "Unsupported literal")
|
||||
(check-type (/ 3 4) : CNum -> 3/4)
|
||||
(check-type (/ 81 3 3) : CNum -> 9)
|
||||
(check-type (/ 10.0) : CNum -> 0.1)
|
||||
(typecheck-fail (/ 1+2i 3+4i) #:with-msg "Unsupported literal")
|
||||
(check-type (quotient 10 3) : CInt -> 3)
|
||||
(check-type (quotient -10.0 3) : CInt -> -3.0)
|
||||
(typecheck-fail (quotient +inf.0 3) #:with-msg "expected.*Int")
|
||||
(check-type (remainder 10 3) : CInt -> 1)
|
||||
(check-type (remainder -10.0 3) : CInt -> -1.0)
|
||||
(check-type (remainder 10.0 -3) : CInt -> 1.0)
|
||||
(check-type (remainder -10 -3) : CInt -> -1)
|
||||
(typecheck-fail (remainder +inf.0 3) #:with-msg "expected.*Int")
|
||||
(check-type (modulo 10 3) : CInt -> 1)
|
||||
(check-type (modulo -10.0 3) : CInt -> 2.0)
|
||||
(check-type (modulo 10.0 -3) : CInt -> -2.0)
|
||||
(check-type (modulo -10 -3) : CInt -> -1)
|
||||
(typecheck-fail (modulo +inf.0 3) #:with-msg "expected.*Int")
|
||||
(check-type (abs 1.0) : CInt -> 1.0)
|
||||
(check-type (abs -1) : CInt -> 1)
|
||||
(check-type (max 1 3 2) : CInt -> 3)
|
||||
(check-type (max 1 3 2.0) : CInt -> 3) ; Racket coerces to inexact, but Rosette does not?
|
||||
(check-type (min 1 3 2) : CInt -> 1)
|
||||
(check-type (min 1 3 2.0) : CInt -> 1) ; Racket coerces to inexact, but Rosette does not?
|
||||
(check-type (floor 17/4) : CNum -> 4)
|
||||
(check-type (floor -17/4) : CNum -> -5)
|
||||
(check-type (floor 2.5) : CNum -> 2.0)
|
||||
(check-type (floor -2.5) : CNum -> -3.0)
|
||||
(check-type (floor +inf.0) : CNum -> +inf.0)
|
||||
(check-type (ceiling 17/4) : CNum -> 5)
|
||||
(check-type (ceiling -17/4) : CNum -> -4)
|
||||
(check-type (ceiling 2.5) : CNum -> 3.0)
|
||||
(check-type (ceiling -2.5) : CNum -> -2.0)
|
||||
(check-type (ceiling +inf.0) : CNum -> +inf.0)
|
||||
(check-type (truncate 17/4) : CNum -> 4)
|
||||
(check-type (truncate -17/4) : CNum -> -4)
|
||||
(check-type (truncate 2.5) : CNum -> 2.0)
|
||||
(check-type (truncate -2.5) : CNum -> -2.0)
|
||||
(check-type (truncate +inf.0) : CNum -> +inf.0)
|
||||
(check-type (= 1 1.0) : CBool -> #t)
|
||||
(check-type (= 1 2) : CBool -> #f)
|
||||
(typecheck-fail (= 2+3i 2+3i 2+3i) #:with-msg "Unsupported literal")
|
||||
(check-type (< 1 1) : CBool -> #f)
|
||||
(check-type (< 1 2 3) : CBool -> #t)
|
||||
(check-type (< 1 +inf.0) : CBool -> #t)
|
||||
(check-type (< 1 +nan.0) : CBool -> #f)
|
||||
(check-type (<= 1 1) : CBool -> #t)
|
||||
(check-type (<= 1 2 1) : CBool -> #f)
|
||||
(check-type (> 1 1) : CBool -> #f)
|
||||
(check-type (> 3 2 1) : CBool -> #t)
|
||||
(check-type (> +inf.0 1) : CBool -> #t)
|
||||
(check-type (> +nan.0 1) : CBool -> #f)
|
||||
(check-type (>= 1 1) : CBool -> #t)
|
||||
(check-type (>= 1 2 1) : CBool -> #f)
|
||||
(check-type (expt 2 3) : CInt -> 8)
|
||||
(check-type (expt 4 0.5) : CNum -> 2.0)
|
||||
(check-type (expt +inf.0 0) : CInt -> 1)
|
||||
(check-type pi : CNum -> 3.141592653589793)
|
||||
(check-type (sgn 10) : CInt -> 1)
|
||||
(check-type (sgn -10.0) : CInt -> -1.0)
|
||||
(check-type (sgn 0) : CInt -> 0)
|
||||
(check-type (sgn +nan.0) : CNum -> +nan.0)
|
||||
|
||||
(clear-asserts!)
|
||||
|
||||
;; 4.2.1 Additional Logic Operators
|
||||
(check-type (! #f) : Bool -> #t)
|
||||
(check-type (! #t) : Bool -> #f)
|
||||
; this typechecks only when b is true
|
||||
(check-type (! (assert-type (if b #f 3) : Bool)) : Bool -> #t)
|
||||
; so Rosette emits a corresponding assertion
|
||||
(check-type (asserts) : (CListof Bool) -> (list b))
|
||||
(clear-asserts!)
|
||||
(check-type (&&) : Bool -> #t)
|
||||
(check-type (||) : Bool -> #f)
|
||||
; no shortcircuiting
|
||||
(check-type (&& #f (begin (displayln "hello") #t)) : Bool -> #f)
|
||||
(define-symbolic a boolean?)
|
||||
; this typechecks only when b is true
|
||||
(check-type (&& a (assert-type (if b #t 1) : Bool)) : Bool -> a)
|
||||
; so Rosette emits a corresponding assertion
|
||||
(check-type (asserts) : (CListof Bool) -> (list b))
|
||||
(clear-asserts!)
|
||||
; no shortcircuiting
|
||||
(check-type (=> #f (begin (displayln "hello") #f)) : Bool -> #t)
|
||||
; this typechecks only when b is true
|
||||
(check-type (<=> a (assert-type (if b #t 1) : Bool)) : Bool -> a)
|
||||
; so Rosette emits a corresponding assertion
|
||||
(check-type (asserts) : (CListof Bool) -> (list b))
|
||||
(clear-asserts!)
|
||||
|
||||
(current-bitwidth #f)
|
||||
|
||||
(define-symbolic a1 b1 integer?)
|
||||
(check-type (forall (list) (= a1 b1)) : Bool -> (= a1 b1))
|
||||
(define f1 (forall (list a1) (exists (list b1) (= a1 (+ a1 b1))))) ; no free constants
|
||||
(check-type (list 1) : (CListof PosInt))
|
||||
(check-type (list 1) : (CList PosInt))
|
||||
(typecheck-fail (exists (list 1) (= a1 b1))
|
||||
#:with-msg "Expected list of symbolic constants, given list containing: PosInt")
|
||||
(typecheck-fail (exists (list (+ a1 b1)) (= a1 b1))
|
||||
#:with-msg "Expected list of symbolic constants, given list containing: Int")
|
||||
(check-type (cons a1 (cons b (list))) : (CList (Constant Int) (Constant Bool)))
|
||||
(typecheck-fail (forall (list 1) (= a1 b1))
|
||||
#:with-msg "Expected list of symbolic constants, given list containing: PosInt")
|
||||
(typecheck-fail (forall (list (+ a1 b1)) (= a1 b1))
|
||||
#:with-msg "Expected list of symbolic constants, given list containing: Int")
|
||||
; so the model has no bindings
|
||||
(define sol1 (solve (assert f1)))
|
||||
(check-type sol1 : CSolution)
|
||||
(check-type (model sol1) : (CHashTable Any Any))
|
||||
(check-type (hash-keys (model sol1)) : (CListof Any) -> (list)) ; empty solution
|
||||
(check-type (sat? sol1) : Bool -> #t)
|
||||
(define g1 (forall (list a1) (= a1 (+ a1 b1)))) ; b1 is free in g1
|
||||
; so the model has a binding for b
|
||||
(define sol2 (solve (assert g1)))
|
||||
(check-type sol2 : CSolution)
|
||||
(check-type (sat? sol2) : Bool -> #t)
|
||||
(check-type (evaluate b1 sol2) : Int -> 0)
|
||||
; body refers to the innermost a1
|
||||
(define h (exists (list a1) (forall (list a1) (= a1 (+ a1 a1)))))
|
||||
; so h is unsatisfiable.
|
||||
(check-type (solve (assert h)) : CSolution -> (unsat))
|
||||
|
|
@ -0,0 +1,190 @@
|
|||
#lang s-exp "../../../rosette/rosette3.rkt"
|
||||
(require "../../rackunit-typechecking.rkt")
|
||||
|
||||
;; Examples from the Rosette Guide, Section 4.3
|
||||
|
||||
;; 4.3 Bitvectors
|
||||
|
||||
; a bitvector literal of size 7
|
||||
(check-type (bv 4 (bitvector 7)) : BV -> (bv 4 7))
|
||||
(check-type (bv 4 7) : BV -> (bv 4 7))
|
||||
(define-symbolic x y (bitvector 7)) ; symbolic bitvector constants
|
||||
(check-type x : BV)
|
||||
(check-type y : BV)
|
||||
(check-type (bvslt (bv 4 7) (bv -1 7)) : Bool -> #f)
|
||||
; 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)))
|
||||
|
|
@ -0,0 +1,114 @@
|
|||
#lang s-exp "../../../rosette/rosette3.rkt"
|
||||
(require "../../rackunit-typechecking.rkt")
|
||||
|
||||
;; Examples from the Rosette Guide, Section 4.4
|
||||
|
||||
;; 4.4 Uninterpreted Functions
|
||||
|
||||
;; example demonstrating unsoundness of Constant
|
||||
;; (define-symbolic f (~> integer? boolean?))
|
||||
;; (define-symbolic x integer?)
|
||||
;; (define sol (solve (assert (not (equal? (f x) (f 1))))))
|
||||
;; (define res (evaluate x sol))
|
||||
;; (check-type res : (Constant Int))
|
||||
;; (constant? res)
|
||||
|
||||
; an uninterpreted function from integers to booleans:
|
||||
(define-symbolic f (~> integer? boolean?))
|
||||
; no built-in interpretation for 1
|
||||
(check-type (f 1) : Bool -> (f 1))
|
||||
(check-not-type (f 1) : CBool)
|
||||
(define-symbolic x real?)
|
||||
; typed Rosette rejects tis program
|
||||
(typecheck-fail (f x) #:with-msg "expected Int, given.*Num")
|
||||
;; must use assert-type to cast to Int
|
||||
(check-type (f (assert-type x : Int))
|
||||
: Bool -> (f (assert-type x : Int))) ;(app f (real->integer x)))
|
||||
(check-type (asserts) : CAsserts -> (list (integer? x)))
|
||||
(clear-asserts!)
|
||||
;(clear-terms!) ; must not clear terms
|
||||
|
||||
;; typed Rosette rejects this program
|
||||
(typecheck-fail (solve (assert (not (equal? (f x) (f 1)))))
|
||||
#:with-msg "expected Int, given.*Num")
|
||||
;; must use assert-type to cast x toInt
|
||||
(define sol (solve (assert (not (equal? (f (assert-type x : Int)) (f 1))))))
|
||||
(check-type sol : CSolution)
|
||||
(define g (evaluate f sol)) ; an interpretation of f
|
||||
(check-type g : (→ Int Bool)) ; -> (fv (((1) . #f) ((0) . #t)) #f integer?~>boolean?)
|
||||
; f is a function value
|
||||
(check-type (fv? f) : Bool -> #t)
|
||||
; and so is g
|
||||
(check-type (fv? g) : Bool -> #t)
|
||||
|
||||
;; The tests below depend on a specific term-cache (should be commented out above)
|
||||
;; at the time solve was called
|
||||
;; should this be Num or Int?
|
||||
;(check-type (evaluate x sol) : Int -> 0)
|
||||
(check-type (evaluate x sol) : Num -> 0)
|
||||
;; check soundness of Constant
|
||||
(check-not-type (evaluate x sol) : (Constant Num))
|
||||
; we can apply g to concrete values
|
||||
(check-type (g 2) : Bool -> #f)
|
||||
; and to symbolic values
|
||||
(check-type (g (assert-type x : Int)) : Bool -> (= 0 (real->integer x)))
|
||||
|
||||
;; this test does not depend on the term cache
|
||||
(check-type (equal? (g 1) (g (assert-type (evaluate x sol) : Int))) : Bool -> #f)
|
||||
(clear-asserts!)
|
||||
|
||||
;; ~>
|
||||
(define t (~> integer? real? boolean? (bitvector 4)))
|
||||
(check-type t : (C→ Any Bool) -> (~> integer? real? boolean? (bitvector 4))) ;integer?~>real?~>boolean?~>(bitvector? 4)
|
||||
(typecheck-fail (~> t integer?)
|
||||
#:with-msg "Expected a non-function Rosette type, given.*t")
|
||||
(define-symbolic b boolean?)
|
||||
(typecheck-fail (~> integer? (if b boolean? real?))
|
||||
#:with-msg "Expected a Rosette-solvable type, given")
|
||||
(typecheck-fail (~> real?) #:with-msg "expected more terms")
|
||||
|
||||
;; function?
|
||||
(define t0? (~> integer? real? boolean? (bitvector 4)))
|
||||
(define t1? (~> integer? real?))
|
||||
(check-type (function? t0?) : Bool -> #t)
|
||||
(check-type (function? t1?) : Bool -> #t)
|
||||
;> (define-symbolic b boolean?)
|
||||
(check-type (function? (if b t0? t1?)) : Bool -> #f) ; not a concrete type
|
||||
(check-type (function? integer?) : Bool -> #f) ; not a function type
|
||||
(check-type (function? 3) : Bool -> #f) ; not a type
|
||||
|
||||
;; should always be CBool, and sometimes CFalse
|
||||
(check-type (function? t0?) : CBool -> #t)
|
||||
(check-type (function? t1?) : CBool -> #t)
|
||||
(check-type (function? (if b t0? t1?)) : CBool -> #f) ; not a concrete type
|
||||
(check-type (function? integer?) : CBool -> #f) ; not a function type
|
||||
(check-type (function? 3) : CBool -> #f) ; not a type
|
||||
|
||||
(check-type (function? t0?) : CBool -> #t)
|
||||
(check-type (function? t1?) : CBool -> #t)
|
||||
(check-type (function? (if b t0? t1?)) : CFalse -> #f) ; not a concrete type
|
||||
(check-type (function? integer?) : CBool -> #f) ; not a function type
|
||||
(check-type (function? 3) : CFalse -> #f) ; not a type
|
||||
|
||||
;; fv?
|
||||
(define-symbolic f2 (~> boolean? boolean?))
|
||||
(check-type (fv? f2) : Bool -> #t)
|
||||
(check-not-type (fv? f2) : CBool)
|
||||
(check-type (fv? (lambda ([x : Int]) x)) : Bool -> #f)
|
||||
;> (define-symbolic b boolean?)
|
||||
(check-type (fv? (if b f2 1)) : Bool -> b)
|
||||
(define sol2
|
||||
(solve
|
||||
(begin
|
||||
(assert (not (f2 #t)))
|
||||
(assert (f2 #f)))))
|
||||
(check-type sol2 : CSolution)
|
||||
(check-type (sat? sol2) : Bool -> #t)
|
||||
(define g2 (evaluate f2 sol2))
|
||||
(check-type g2 : (→ Bool Bool)) ; g2 implements logical negation
|
||||
;(fv (((#f) . #t) ((#t) . #f)) #t boolean?~>boolean?)
|
||||
(check-type (fv? g2) : Bool -> #t)
|
||||
; verify that g implements logical negation:
|
||||
(check-type (verify (assert (equal? (g2 b) (not b)))) : CSolution -> (unsat))
|
||||
(check-type (g2 #t) : Bool -> #f)
|
||||
(check-type (g2 #f) : Bool -> #t)
|
||||
|
|
@ -0,0 +1,21 @@
|
|||
#lang s-exp "../../../rosette/rosette3.rkt"
|
||||
(require "../../rackunit-typechecking.rkt")
|
||||
|
||||
;; Examples from the Rosette Guide, Section 4.5
|
||||
|
||||
;; 4.5 Procedures
|
||||
(define-symbolic b boolean?)
|
||||
(define-symbolic x integer?)
|
||||
(define p (if b * -)) ; p is a symbolic procedure
|
||||
(check-type p : (→ Num Num Num))
|
||||
(check-not-type p : (C→ Num Num Num)) ; should not have concrete type
|
||||
(check-type p : (→ Int Int Int))
|
||||
(define sol (synthesize #:forall (list x)
|
||||
#:guarantee (assert (= x (p x 1)))))
|
||||
(check-type (evaluate p sol) : (→ Int Int Int) -> *)
|
||||
;; this doesnt hold bc type of result is from p
|
||||
;(check-type (evaluate p sol) : (→ PosInt PosInt PosInt) -> *)
|
||||
(define sol2 (synthesize #:forall (list x)
|
||||
#:guarantee (assert (= x (p x 0)))))
|
||||
(check-type (evaluate p sol2) : (→ Int Int Int) -> -)
|
||||
(check-not-type (evaluate p sol2) : (→ PosInt PosInt PosInt))
|
||||
|
|
@ -0,0 +1,95 @@
|
|||
#lang s-exp "../../../rosette/rosette3.rkt"
|
||||
(require "../../rackunit-typechecking.rkt")
|
||||
|
||||
;; Examples from the Rosette Guide, Section 4.6-4.8
|
||||
|
||||
;; 4.6 Pairs and Lists
|
||||
(define-symbolic x y z n integer?)
|
||||
(define xs (take (list x y z) n)) ; (1) xs is a symbolic list
|
||||
(check-type xs : (Listof Int))
|
||||
(define sol1 (solve (assert (null? xs))))
|
||||
(check-type sol1 : CSolution)
|
||||
(check-type (sat? sol1) : Bool -> #t)
|
||||
(check-type (evaluate xs sol1) : (Listof Int) -> '())
|
||||
(define sol2
|
||||
(solve (begin
|
||||
(assert (= (length xs) 2))
|
||||
(assert (not (equal? xs (reverse xs))))
|
||||
(assert (equal? xs (sort xs <))))))
|
||||
(check-type (evaluate xs sol2) : (Listof Int) -> '(1 4))
|
||||
(define-symbolic b boolean?)
|
||||
(define p (if b (cons 1 2) (cons 4 #f))) ; (2) p is a symbolic pair
|
||||
(check-type p : (Pair Nat (U Nat Bool)))
|
||||
(check-type p : (Pair Any Any))
|
||||
(check-not-type p : (CPair Any Any)) ; check not concrete
|
||||
(check-type p : (Pair CNat (CU CNat CBool))) ; contents are concrete
|
||||
(define sol3 (solve (assert (boolean? (cdr p)))))
|
||||
(check-type (evaluate p sol3) : (Pair Nat (U Nat Bool)) -> '(4 . #f))
|
||||
(define sol4 (solve (assert (odd? (car p)))))
|
||||
(check-type (evaluate p sol4) : (Pair Nat (U Nat Bool)) -> '(1 . 2))
|
||||
|
||||
;; 4.7 Vectors
|
||||
(define v1 (vector 1 2 #f))
|
||||
(define v2 (vector 1 2 #f))
|
||||
;; mutable vectors are invariant
|
||||
(check-type v1 : (CMVectorof (CU CPosInt CFalse)))
|
||||
(check-type v1 : (CVectorof (CU CPosInt CFalse)))
|
||||
(check-not-type v1 : (CMVectorof (U Nat Bool)))
|
||||
(check-not-type v1 : (CVectorof (U Nat Bool)))
|
||||
(check-type v2 : (CMVectorof (CU CPosInt CFalse)))
|
||||
(check-type (eq? v1 v2) : Bool -> #f)
|
||||
(check-type (equal? v1 v2) : Bool -> #t)
|
||||
|
||||
(define v3 (vector-immutable 1 2 #f))
|
||||
(define v4 (vector-immutable 1 2 #f))
|
||||
;; immutable vectors have supertypes
|
||||
(check-type v3 : (CIVectorof (CU CPosInt CFalse)))
|
||||
(check-type v3 : (CVectorof (U Nat Bool)))
|
||||
(check-type v4 : (CIVectorof (CU CPosInt CFalse)))
|
||||
(check-type (eq? v3 v4) : Bool -> #t)
|
||||
(check-type (equal? v1 v3) : Bool -> #t)
|
||||
;(define-symbolic x y z n integer?)
|
||||
;(define xs (take (list x y z) n)) ; xs is a symbolic list
|
||||
(define vs (list->vector xs)) ; vs is a symbolic vector
|
||||
(check-type vs : (CVectorof (U (Constant Int))))
|
||||
(check-type vs : (CMVectorof (U (Constant Int))))
|
||||
(define sol5 (solve (assert (= 4 (vector-ref vs (sub1 n))))))
|
||||
(check-type (= 4 (vector-ref (evaluate vs sol5) (sub1 (evaluate n sol5))))
|
||||
: Bool -> #t)
|
||||
;; TODO: Constant unsound
|
||||
(check-type (evaluate vs sol5) : (CVectorof Int) -> (vector 0 4))
|
||||
(check-type (evaluate xs sol5) : (Listof Int) -> '(0 4))
|
||||
|
||||
;; 4.8 Boxes
|
||||
(define b1 (box 1))
|
||||
(define b2 (box 1))
|
||||
(check-type b1 : (CMBoxof CPosInt))
|
||||
(check-type b1 : (CBoxof CPosInt))
|
||||
(check-not-type b1 : (CMBoxof Nat)) ; invariant
|
||||
(check-type b2 : (CMBoxof CPosInt))
|
||||
|
||||
(check-type (eq? b1 b2) : Bool -> #f)
|
||||
(check-type (equal? b1 b2) : Bool -> #t)
|
||||
|
||||
(define b3 (box-immutable 1))
|
||||
(define b4 (box-immutable 1))
|
||||
(check-type b3 : (CIBoxof CPosInt))
|
||||
(check-type b3 : (CBoxof CPosInt))
|
||||
(check-type b3 : (CBoxof Nat)) ; subtype ok
|
||||
(check-type b4 : (CBoxof Nat))
|
||||
|
||||
(check-type (eq? b3 b4) : Bool -> #t)
|
||||
(check-type (equal? b1 b3) : Bool -> #t)
|
||||
;> (define-symbolic x integer?)
|
||||
;> (define-symbolic b boolean?)
|
||||
|
||||
(define sb1 (box x)) ; sb1 is a box with symbolic contents
|
||||
(check-type sb1 : (CMBoxof (Constant Int)))
|
||||
(define sb2 (if b sb1 (box 3))) ; sb2 is a symbolic box
|
||||
(check-type sb2 : (U (CMBoxof (Constant Int)) (CMBoxof CPosInt)))
|
||||
(define sol6 (solve (assert (= 4 (unbox sb2)))))
|
||||
(check-type (evaluate sb1 sol6) : (CMBoxof Int) -> (box 4))
|
||||
(check-type (evaluate sb2 sol6) : (U (CMBoxof Int) (CMBoxof CPosInt)) -> (box 4))
|
||||
(check-not-type (evaluate sb2 sol6) : (MBoxof Int))
|
||||
(check-type (= 4 (unbox (evaluate sb2 sol6))) : Bool -> #t)
|
||||
(check-type (evaluate (eq? sb1 sb2) sol6) : Bool -> #t)
|
||||
|
|
@ -0,0 +1,32 @@
|
|||
#lang s-exp "../../../rosette/rosette3.rkt"
|
||||
(require "../../rackunit-typechecking.rkt")
|
||||
|
||||
;; Examples from the Rosette Guide, Section 4.9 Solvers and Solutions
|
||||
|
||||
;; 4.9.1 The Solver Interface
|
||||
|
||||
(check-type (current-solver) : CSolver -> (current-solver))
|
||||
;; TODO
|
||||
;(check-type gen:solver : CSolver)
|
||||
|
||||
;; 4.9.2 Solutions
|
||||
(define-symbolic a b boolean?)
|
||||
(define-symbolic x y integer?)
|
||||
(define sol
|
||||
(solve (begin (assert a)
|
||||
(assert (= x 1))
|
||||
(assert (= y 2)))))
|
||||
(check-type sol : CSolution)
|
||||
(check-type (sat? sol) : Bool -> #t)
|
||||
(check-type (evaluate (list 4 5 x) sol) : (Listof Int) -> '(4 5 1))
|
||||
(check-type (evaluate (list 4 5 x) sol) : (CListof Int)) ; concrete list ok
|
||||
(check-not-type (evaluate (list 4 5 x) sol) : (Listof Nat))
|
||||
(define vec (vector a))
|
||||
(check-type (evaluate vec sol) : (CMVectorof Bool))
|
||||
;'#(#t)
|
||||
; evaluation produces a new vector
|
||||
(check-type (eq? vec (evaluate vec sol)) : Bool -> #f)
|
||||
(check-type (evaluate (+ x y) sol) : Int -> 3)
|
||||
(check-not-type (evaluate (+ x y) sol) : CInt) ; not concrete
|
||||
(check-type (evaluate (and a b) sol) : Bool -> b)
|
||||
(check-not-type (evaluate (and a b) sol) : CBool) ; not concrete
|
||||
|
|
@ -0,0 +1,59 @@
|
|||
#lang s-exp "../../../rosette/rosette3.rkt"
|
||||
(require "../../rackunit-typechecking.rkt")
|
||||
|
||||
;; Examples from the Rosette Guide, Section 5 Structures
|
||||
|
||||
; immutable transparent type
|
||||
(struct point ([x : Int] [y : Int]) #:transparent)
|
||||
(check-type point : (C→ Int Int (CPoint Int Int)))
|
||||
(check-type point-x : (C→ (CPoint Int Int) Int))
|
||||
(check-type point-y : (C→ (CPoint Int Int) Int))
|
||||
(check-type point? : (C→ Any Bool))
|
||||
|
||||
; opaque immutable type
|
||||
(struct pt ([x : Int] [y : Int]))
|
||||
; mutable transparent type
|
||||
(struct pnt ([x : Int] [y : Int]) #:mutable #:transparent)
|
||||
|
||||
(check-type (point 1 2) : (CPoint Int Int) -> (point 1 2))
|
||||
(typecheck-fail (point #f 2) #:with-msg "expected Int, given False")
|
||||
(check-type (pt 1 2) : (CPt Int Int)) ; opaque, incomparable
|
||||
(check-type (pnt 1 2) : (CPnt Int Int) -> (pnt 1 2))
|
||||
|
||||
(check-type (eq? (point 1 2) (point 1 2)) : Bool -> #t) ; point structures are values
|
||||
(check-type (eq? (pt 1 2) (pt 1 2)) : Bool -> #f) ; pt structures are references
|
||||
|
||||
(check-type (eq? (pnt 1 2) (pnt 1 2)) : Bool -> #f) ; pnt structures are references
|
||||
|
||||
(define-symbolic b boolean?)
|
||||
(define p (if b (point 1 2) (point 3 4))) ; p holds a symbolic structure
|
||||
(check-type p : (Point Int Int))
|
||||
(check-not-type p : (CPoint Int Int))
|
||||
(check-type (point-x p) : Int -> (if b 1 3)) ;(ite b 1 3)
|
||||
(check-type (point-y p) : Int -> (if b 2 4)) ;(ite b 2 4)
|
||||
(define sol (solve (assert (= (point-x p) 3))))
|
||||
(check-type (evaluate p sol) : (Point Int Int) -> (point 3 4)) ;#(struct:point 3 4)
|
||||
(check-type (= (point-x (evaluate p sol)) 3) : Bool -> #t)
|
||||
|
||||
;; Generics
|
||||
(define-generics viewable (view viewable -> Nat))
|
||||
(typecheck-fail
|
||||
(struct square (side)
|
||||
#:methods gen:viewable
|
||||
[(define (view self) (square-side self))])
|
||||
#:with-msg "Missing type annotations for fields")
|
||||
(struct square ([side : Nat])
|
||||
#:methods gen:viewable
|
||||
[(define (view [self : (Square Nat)] -> Nat) (square-side self))])
|
||||
(struct circle ([radius : Nat])
|
||||
#:transparent
|
||||
#:methods gen:viewable
|
||||
[(define (view [self : (Circle Nat)] -> Nat) (circle-radius self))])
|
||||
;(define-symbolic b boolean?)
|
||||
(define p2 (if b (square 2) (circle 3))) ; p holds a symbolic structure
|
||||
(check-type p2 : (U (CSquare Nat) (CCircle Nat)))
|
||||
(check-type p2 : (U (Square Nat) (Circle Nat)))
|
||||
(check-type (apply-view p2) : Nat -> (if b 2 3)) ;(ite b 2 3)
|
||||
(define sol2 (solve (assert (= (apply-view p2) 3))))
|
||||
(check-type (evaluate p2 sol2) : (U (Square Nat) (Circle Nat)) -> (circle 3))
|
||||
(check-type (= (apply-view (evaluate p2 sol2)) 3) : Bool -> #t)
|
||||
|
|
@ -0,0 +1,52 @@
|
|||
#lang s-exp "../../../rosette/rosette3.rkt"
|
||||
(require "../../rackunit-typechecking.rkt")
|
||||
|
||||
;; Examples from the Rosette Guide, Section 6 Libraries
|
||||
|
||||
;; 6.2.1 Synthesis library
|
||||
(require "../../../rosette/lib/synthax3.rkt")
|
||||
|
||||
;; choose
|
||||
(define (div2 [x : BV] -> BV)
|
||||
([choose bvshl bvashr bvlshr bvadd bvsub bvmul] x (?? (bitvector 8))))
|
||||
(define-symbolic i (bitvector 8))
|
||||
(print-forms
|
||||
(synthesize #:forall (list i)
|
||||
#:guarantee (assert (equal? (div2 i) (bvudiv i (bv 2 8))))))
|
||||
(printf "expected output:\n~a\n"
|
||||
"'(define (div2 [x : BV] -> BV) (bvlshr x (bv 1 8)))")
|
||||
|
||||
;; TODO: define-synthax
|
||||
; Defines a grammar for boolean expressions
|
||||
; in negation normal form (NNF).
|
||||
#;(define-synthax (nnf [x : Bool] [y : Bool] [depth : Int] -> Bool)
|
||||
#:base (choose x (! x) y (! y))
|
||||
#:else (choose
|
||||
x (! x) y (! y)
|
||||
((choose && ||) (nnf x y (- depth 1))
|
||||
(nnf x y (- depth 1)))))
|
||||
|
||||
; The body of nnf=> is a hole to be filled with an
|
||||
; expression of depth (up to) 1 from the NNF grammar.
|
||||
#;(define (nnf=> [x : Bool] [y : Bool] -> Bool)
|
||||
(apply-nnf x y 1))
|
||||
|
||||
;; (define-symbolic a b boolean?)
|
||||
;; (print-forms
|
||||
;; (synthesize
|
||||
;; #:forall (list a b)
|
||||
;; #:guarantee (assert (equal? (=> a b) (nnf=> a b)))))
|
||||
;; (printf "expected output:\n~a\n"
|
||||
;; "'(define (nnf=> [x : Bool] [y : Bool] -> Bool) (|| (! x) y))")
|
||||
|
||||
;; 6.2.2 Angelic Execution Library
|
||||
(require "../../../rosette/lib/angelic3.rkt")
|
||||
|
||||
(define (static -> Int) (choose 1 2 3))
|
||||
(define (dynamic -> Int) (choose* 1 2 3))
|
||||
(check-type (equal? (static) (static)) : Bool -> #t)
|
||||
(define dyn1 (dynamic))
|
||||
(define dyn2 (dynamic))
|
||||
(check-type (equal? dyn1 dyn2) : Bool -> (equal? dyn1 dyn2))
|
||||
;(= (ite xi?$4 1 (ite xi?$5 2 3)) (ite xi?$6 1 (ite xi?$7 2 3)))
|
||||
|
||||
|
|
@ -0,0 +1,230 @@
|
|||
#lang s-exp "../../../rosette/rosette3.rkt"
|
||||
(require "../../rackunit-typechecking.rkt")
|
||||
|
||||
;; Examples from the Rosette Guide, Section 7 Reflecting on Symbolic Values
|
||||
|
||||
;; 7.1.1 Symbolic Terms
|
||||
(define-symbolic x integer?) ; constant
|
||||
(define e (+ x 1)) ; expression
|
||||
(check-type (list (term? x) (term? e)) : (CListof Bool) -> (list #t #t))
|
||||
(check-type (list (constant? x) (constant? e)) : (CListof Bool) -> (list #t #f))
|
||||
(check-type (list (expression? x) (expression? e)) : (CListof Bool) -> (list #f #t))
|
||||
(check-type (term? 1) : Bool -> #f)
|
||||
|
||||
;; TODO: match and match expanders
|
||||
;; > (define-symbolic x integer?) ; constant
|
||||
;; > (define e (+ x 1)) ; expression
|
||||
;; > (match x
|
||||
;; [(constant identifier type) (list identifier type)])
|
||||
;; '(#<syntax:8:0 x> integer?)
|
||||
;; > (match x
|
||||
;; [(term content type) (list content type)])
|
||||
;; '(#<syntax:8:0 x> integer?)
|
||||
;; > (match e
|
||||
;; [(expression op child ...) (cons op child)])
|
||||
;; '(+ 1 x)
|
||||
;; > (match e
|
||||
;; [(term content type) (list content type)])
|
||||
;; '((+ 1 x) integer?)
|
||||
|
||||
;(define-symbolic x integer?)
|
||||
(check-type (type-of x) : (C→ Any Bool) -> integer?)
|
||||
(check-type (type-of (+ x 1)) : (C→ Any Bool) -> integer?)
|
||||
(check-type (type-of x 3.14) : (C→ Any Bool) -> real?)
|
||||
(check-type (type-of #t) : (C→ Any Bool) -> boolean?)
|
||||
(check-type (type-of #t 1) : (C→ Any Bool) -> any/c)
|
||||
|
||||
(check-type (type? integer?) : Bool -> #t)
|
||||
(check-type (type? boolean?) : Bool -> #t)
|
||||
(check-type (type? list?) : Bool -> #t)
|
||||
(struct circle ([radius : Nat]))
|
||||
(check-type (type? circle?) : Bool -> #t)
|
||||
(check-type (type? any/c) : Bool -> #t)
|
||||
(check-type (type? 1) : Bool -> #f)
|
||||
|
||||
(check-type (solvable? boolean?) : Bool -> #t)
|
||||
(check-type (solvable? integer?) : Bool -> #t)
|
||||
(check-type (solvable? real?) : Bool -> #t)
|
||||
(check-type (solvable? (~> (bitvector 3) (bitvector 4))) : Bool -> #t)
|
||||
(check-type (solvable? list?) : Bool -> #f)
|
||||
;(struct circle (radius))
|
||||
(check-type (solvable? circle?) : Bool -> #f)
|
||||
(check-type (solvable? any/c) : Bool -> #f)
|
||||
|
||||
;; 7.1.2 Symbolic Unions
|
||||
(define-symbolic b boolean?)
|
||||
(define v (vector 1))
|
||||
(check-type v : (CVectorof CPosInt))
|
||||
(define w (vector 2 3))
|
||||
(check-type v : (CVectorof CPosInt))
|
||||
(define s (if b v w))
|
||||
(check-type s : (Vectorof CPosInt)) ;{[b #(1)] [(! b) #(2 3)]}
|
||||
(check-not-type s : (CVectorof CPosInt)) ; check union doesnt have concrete type
|
||||
(check-type (type-of s) : (C→ Any Bool) -> vector?)
|
||||
(check-type (eq? s v) : Bool -> b)
|
||||
(check-type (eq? s w) : Bool -> (! b))
|
||||
|
||||
; (define-symbolic b boolean?)
|
||||
(define-symbolic c boolean?)
|
||||
(define v2 (if c "c" 0))
|
||||
(check-type v2 : (U String Int))
|
||||
(check-type v2 : (U CString CInt))
|
||||
(check-not-type v2 : (CU CString CInt)) ; check not concrete
|
||||
(check-type v2 : (U CString CInt))
|
||||
(check-type v2 : (U CString CZero))
|
||||
(define u (if b (vector v2) 4))
|
||||
(check-type u : (U (CVectorof (U CString CZero)) Int)) ;{[b #({[c "c"] [(! c) 0]})] [(! b) 4]}
|
||||
(check-type (type-of u) : (C→ Any Bool) -> any/c)
|
||||
|
||||
(check-type '(1 2) : (CListof CPosInt))
|
||||
;> (define-symbolic b boolean?)
|
||||
(define u2 (if b '(1 2) 3))
|
||||
(check-type u2 : (U (CListof CPosInt) CPosInt))
|
||||
(check-type (union? u2) : Bool -> #t)
|
||||
(check-type (union? b) : Bool -> #f)
|
||||
(define v3 (if b '(1 2) 3))
|
||||
(check-type (union-contents v3)
|
||||
: (CListof (CPair Bool (U (CListof CPosInt) CPosInt)))
|
||||
-> (list (cons b '(1 2)) (cons (! b) 3)))
|
||||
|
||||
;; 7.1.3 Symbolic Lifting
|
||||
(require (only-in "../../../rosette/rosette3.rkt" [string-length racket/string-length]))
|
||||
|
||||
(define (string-length [value : String] -> Nat)
|
||||
(for/all ([str value])
|
||||
(racket/string-length str)))
|
||||
|
||||
|
||||
(check-type (string-length "abababa") : Nat -> 7)
|
||||
(check-type (racket/string-length "abababa") : CNat -> 7)
|
||||
(check-not-type (string-length "abababa") : CNat)
|
||||
|
||||
(typecheck-fail (string-length 3) #:with-msg "expected String")
|
||||
;> (define-symbolic b boolean?)
|
||||
(check-type (string-length (if b "a" "abababa")) : Nat -> (if b 1 7)) ;(ite b 1 7)
|
||||
(check-not-type (string-length (if b "a" "abababa")) : CNat)
|
||||
|
||||
;; Typed Rosette rejects this program
|
||||
(typecheck-fail (string-length (if b "a" 3)) #:with-msg "expected String")
|
||||
;; need assert-type
|
||||
;; TODO: this doesnt work yet because String has no pred
|
||||
;; - and we cant use string? bc it's unlifted --- will always be assert fail
|
||||
;(check-type (string-length (assert-type (if b "a" 3) : String)) : Nat -> 1)
|
||||
;;(check-type (asserts) : CAsserts -> (list b))
|
||||
(typecheck-fail (string-length (if b 3 #f)) #:with-msg "expected String")
|
||||
;; not runtime exn: for/all: all paths infeasible
|
||||
|
||||
;; Making symbolic evaluation more efficient.
|
||||
;; (require (only-in racket build-list))
|
||||
|
||||
(define limit 1000)
|
||||
|
||||
(define (slow [xs : (Listof CInt)] -> (U CFalse Int))
|
||||
(and (= (length xs) limit) (car (map add1 xs))))
|
||||
|
||||
(define (fast [xs : (Listof CInt)] -> (U CFalse Int))
|
||||
(for/all ([xs xs]) (slow xs)))
|
||||
|
||||
(define ys (build-list limit (lambda ([x : CNat]) x)))
|
||||
(check-type ys : (CListof CInt))
|
||||
|
||||
(define-symbolic a boolean?)
|
||||
|
||||
(define xs (if a ys (cdr ys)))
|
||||
(check-type xs : (Listof CInt))
|
||||
(check-not-type xs : (CListof CInt))
|
||||
|
||||
(check-type (time (slow xs)) : (U CFalse Int) -> (if a 1 #f))
|
||||
;; cpu time: 1 real time: 2 gc time: 0
|
||||
;; {[a 1] [(! a) #f]}
|
||||
(check-type (time (fast xs)) : (U CFalse Int) -> (if a 1 #f))
|
||||
;; cpu time: 0 real time: 0 gc time: 0
|
||||
;; {[a 1] [(! a) #f]}
|
||||
(printf "First printed time should be slightly slower than second time\n")
|
||||
|
||||
;; define-lift
|
||||
(require "../../../rosette/lib/lift3.rkt")
|
||||
(define-lift lifted-string-length [(string?) racket/string-length])
|
||||
|
||||
(check-type (lifted-string-length "abababa") : Nat -> 7)
|
||||
(check-not-type (lifted-string-length "abababa") : CNat)
|
||||
;> (define-symbolic b boolean?)
|
||||
(check-type (lifted-string-length (if b "a" "abababa"))
|
||||
: Nat -> (if b 1 7)) ;(ite b 1 7)
|
||||
;; typed rosette rejects this progrm
|
||||
(typecheck-fail (lifted-string-length (if b "a" 3)) #:with-msg "expected.*String")
|
||||
;; TODO: need type-assert
|
||||
;; (check-type (lifted-string-length (assert-type (if b "a" 3) : String)) : Nat -> 1)
|
||||
;; (check-type (asserts) : CAsserts -> (list b))
|
||||
|
||||
;; 7.2 Reflecting on Symbolic State
|
||||
;> (define-symbolic a b boolean?)
|
||||
(check-type (if a
|
||||
(if b
|
||||
#f
|
||||
(pc))
|
||||
#f) : Bool -> (&& a (! b)))
|
||||
|
||||
(check-type (assert a) : CUnit -> (void))
|
||||
(check-type (asserts) : CAsserts -> (list a))
|
||||
(check-type (assert b) : CUnit -> (void))
|
||||
(check-type (asserts) : CAsserts -> (list b a))
|
||||
(check-type (clear-asserts!) : CUnit -> (void))
|
||||
(check-type (asserts) : CAsserts -> (list))
|
||||
|
||||
(printf "expected output: 4 and (list b a)\n")
|
||||
(with-asserts
|
||||
(begin (assert a)
|
||||
(assert b)
|
||||
4))
|
||||
(check-type (asserts) : CAsserts -> (list))
|
||||
|
||||
;; term-cache
|
||||
(clear-terms!)
|
||||
(check-type (term-cache) : (CHashTable Any Any) -> (term-cache))
|
||||
(check-type (hash-keys (term-cache)) : (CListof Any) -> (list))
|
||||
|
||||
(define-symbolic a1 b1 c1 d1 integer?)
|
||||
|
||||
(define (p? [x : Int] -> Bool)
|
||||
(or (eq? x a1) (eq? x b1) (eq? x c1) (eq? x d1)))
|
||||
|
||||
(check-type (hash-values (term-cache)) : (CListof Any)); -> (list d1 c1 b1 a1))
|
||||
;; make test more deterministic
|
||||
(check-type (andmap p? (hash-values (term-cache))) : Bool -> #t)
|
||||
;; (hash
|
||||
;; #<syntax:23:0 d>
|
||||
;; d
|
||||
;; #<syntax:23:0 c>
|
||||
;; c
|
||||
;; #<syntax:23:0 b>
|
||||
;; b
|
||||
;; #<syntax:23:0 a>
|
||||
;; a)
|
||||
(check-type (* d1 (- (+ a1 b1) c1)) : Int -> (* d1 (- (+ a1 b1) c1)))
|
||||
;(check-type (hash-keys (term-cache)) : CUnit -> (list (list * d (+ (+ a b) (- c))) d c b a))
|
||||
(printf "expected output: hash with a-d and large arith op with all subexprs\n")
|
||||
(pretty-print (term-cache))
|
||||
;; (hash
|
||||
;; (list * d (+ (+ a b) (- c)))
|
||||
;; (* d (+ (+ a b) (- c)))
|
||||
;; #<syntax:23:0 d>
|
||||
;; d
|
||||
;; #<syntax:23:0 c>
|
||||
;; c
|
||||
;; #<syntax:23:0 b>
|
||||
;; b
|
||||
;; #<syntax:23:0 a>
|
||||
;; a
|
||||
;; (list - c)
|
||||
;; (- c)
|
||||
;; (list + a b)
|
||||
;; (+ a b)
|
||||
;; (list + (+ a b) (- c))
|
||||
;; (+ (+ a b) (- c)))
|
||||
(check-type (clear-terms! (list c1 d1)) : CUnit -> (void))
|
||||
(printf "expected output: hash with c and d missing\n")
|
||||
(pretty-print (term-cache))
|
||||
(check-type (clear-terms!) : CUnit -> (void))
|
||||
(check-type (hash-keys (term-cache)) : (CListof Any) -> (list))
|
||||
|
||||
345
turnstile/examples/tests/rosette/rosette3/rosette3-tests.rkt
Normal file
345
turnstile/examples/tests/rosette/rosette3/rosette3-tests.rkt
Normal file
|
|
@ -0,0 +1,345 @@
|
|||
#lang s-exp "../../../rosette/rosette3.rkt"
|
||||
(require "../../rackunit-typechecking.rkt"
|
||||
"check-type+asserts.rkt")
|
||||
|
||||
;; subtyping among concrete
|
||||
(check-type ((λ ([x : CPosInt]) x) ((λ ([x : CPosInt]) x) 1)) : CPosInt -> 1)
|
||||
(check-type ((λ ([x : CZero]) x) ((λ ([x : CZero]) x) 0)) : CZero -> 0)
|
||||
(check-type ((λ ([x : CNegInt]) x) ((λ ([x : CNegInt]) x) -1)) : CNegInt -> -1)
|
||||
(check-type ((λ ([x : PosInt]) x) ((λ ([x : PosInt]) x) 1)) : PosInt -> 1)
|
||||
(check-type ((λ ([x : Zero]) x) ((λ ([x : Zero]) x) 0)) : Zero -> 0)
|
||||
(check-type ((λ ([x : NegInt]) x) ((λ ([x : NegInt]) x) -1)) : NegInt -> -1)
|
||||
|
||||
(check-type ((λ ([x : CNat]) x) ((λ ([x : CZero]) x) 0)) : CNat -> 0)
|
||||
(check-type ((λ ([x : CNat]) x) ((λ ([x : CPosInt]) x) 1)) : CNat -> 1)
|
||||
(check-type ((λ ([x : CNat]) x) ((λ ([x : CNat]) x) 1)) : CNat -> 1)
|
||||
(typecheck-fail ((λ ([x : CPosInt]) x) ((λ ([x : CNat]) x) 1)))
|
||||
(check-type ((λ ([x : Nat]) x) ((λ ([x : Zero]) x) 0)) : Nat -> 0)
|
||||
(check-type ((λ ([x : Nat]) x) ((λ ([x : PosInt]) x) 1)) : Nat -> 1)
|
||||
(check-type ((λ ([x : Nat]) x) ((λ ([x : Nat]) x) 1)) : Nat -> 1)
|
||||
(typecheck-fail ((λ ([x : PosInt]) x) ((λ ([x : Nat]) x) 1)))
|
||||
|
||||
(check-type ((λ ([x : CInt]) x) ((λ ([x : CNegInt]) x) -1)) : CInt -> -1)
|
||||
(check-type ((λ ([x : CInt]) x) ((λ ([x : CZero]) x) 0)) : CInt -> 0)
|
||||
(check-type ((λ ([x : CInt]) x) ((λ ([x : CPosInt]) x) 1)) : CInt -> 1)
|
||||
(check-type ((λ ([x : CInt]) x) ((λ ([x : CNat]) x) 1)) : CInt -> 1)
|
||||
(check-type ((λ ([x : CInt]) x) ((λ ([x : CInt]) x) 1)) : CInt -> 1)
|
||||
(typecheck-fail ((λ ([x : CPosInt]) x) ((λ ([x : CInt]) x) 1)))
|
||||
(typecheck-fail ((λ ([x : CNat]) x) ((λ ([x : CInt]) x) 1)))
|
||||
(check-type ((λ ([x : Int]) x) ((λ ([x : NegInt]) x) -1)) : Int -> -1)
|
||||
(check-type ((λ ([x : Int]) x) ((λ ([x : Zero]) x) 0)) : Int -> 0)
|
||||
(check-type ((λ ([x : Int]) x) ((λ ([x : PosInt]) x) 1)) : Int -> 1)
|
||||
(check-type ((λ ([x : Int]) x) ((λ ([x : Nat]) x) 1)) : Int -> 1)
|
||||
(check-type ((λ ([x : Int]) x) ((λ ([x : Int]) x) 1)) : Int -> 1)
|
||||
(typecheck-fail ((λ ([x : PosInt]) x) ((λ ([x : Int]) x) 1)))
|
||||
(typecheck-fail ((λ ([x : Nat]) x) ((λ ([x : Int]) x) 1)))
|
||||
|
||||
;; illustrates flattening
|
||||
(define-type-alias A Int)
|
||||
(define-type-alias B CString)
|
||||
(define-type-alias C Bool)
|
||||
(define-type-alias AC (U A C))
|
||||
(define-type-alias BC (U B C))
|
||||
(define-type-alias A-BC (U A BC))
|
||||
(define-type-alias B-AC (U B AC))
|
||||
(check-type ((λ ([x : A-BC]) x) ((λ ([x : B-AC]) x) "1")) : A-BC -> "1")
|
||||
(check-type ((λ ([x : A-BC]) x) ((λ ([x : AC]) x) #t)) : A-BC -> #t)
|
||||
(check-type ((λ ([x : B-AC]) x) ((λ ([x : A-BC]) x) "1")) : A-BC -> "1")
|
||||
(check-type ((λ ([x : B-AC]) x) ((λ ([x : BC]) x) "1")) : A-BC -> "1")
|
||||
(typecheck-fail ((λ ([x : BC]) x) ((λ ([x : B-AC]) x) "1")))
|
||||
(typecheck-fail ((λ ([x : AC]) x) ((λ ([x : B-AC]) x) "1")))
|
||||
|
||||
;; subtyping between concrete and symbolic types
|
||||
(check-type ((λ ([x : Int]) x) ((λ ([x : CInt]) x) 1)) : Int -> 1)
|
||||
(typecheck-fail ((λ ([x : CInt]) x) ((λ ([x : Int]) x) 1)))
|
||||
(check-type ((λ ([x : Bool]) x) ((λ ([x : CBool]) x) #t)) : Bool -> #t)
|
||||
(typecheck-fail ((λ ([x : CBool]) x) ((λ ([x : Bool]) x) #t)))
|
||||
(check-type ((λ ([x : (U CInt CBool)]) x) ((λ ([x : (CU CInt CBool)]) x) 1)) : (U CInt CBool))
|
||||
(typecheck-fail ((λ ([x : (CU CInt CBool)]) x) ((λ ([x : (U CInt CBool)]) x) 1)))
|
||||
(check-type ((λ ([x : (U Int Bool)]) x) ((λ ([x : (U CInt CBool)]) x) 1)) : (U CInt CBool))
|
||||
(check-type ((λ ([x : (U CInt CBool)]) x) ((λ ([x : (U Int Bool)]) x) 1)) : (U CInt CBool))
|
||||
|
||||
;; add1 has a case-> type with cases for different subtypes of Int
|
||||
;; to preserve some of the type information through the operation
|
||||
(check-type (add1 9) : CPosInt -> 10)
|
||||
(check-type (add1 0) : CPosInt -> 1)
|
||||
(check-type (add1 -1) : (CU CNegInt CZero) -> 0)
|
||||
(check-type (add1 -9) : (CU CNegInt CZero) -> -8)
|
||||
(check-type (add1 (ann 9 : PosInt)) : PosInt -> 10)
|
||||
(check-type (add1 (ann 0 : Zero)) : PosInt -> 1)
|
||||
(check-type (add1 (ann 9 : Nat)) : PosInt -> 10)
|
||||
(check-type (add1 (ann 0 : Nat)) : PosInt -> 1)
|
||||
(check-type (add1 (ann -1 : NegInt)) : (U NegInt Zero) -> 0)
|
||||
(check-type (add1 (ann -9 : NegInt)) : (U NegInt Zero) -> -8)
|
||||
(check-type (add1 (ann 9 : Int)) : Int -> 10)
|
||||
|
||||
;; sub1 has a similar case-> type
|
||||
(check-type (sub1 10) : CNat -> 9)
|
||||
(check-type (sub1 0) : CNegInt -> -1)
|
||||
(check-type (sub1 -1) : CNegInt -> -2)
|
||||
(check-type (sub1 (ann 10 : PosInt)) : Nat -> 9)
|
||||
(check-type (sub1 (ann 0 : Zero)) : NegInt -> -1)
|
||||
(check-type (sub1 (ann -1 : NegInt)) : NegInt -> -2)
|
||||
|
||||
(check-type (+ 1 10) : CNat -> 11)
|
||||
(check-type (+ -10 10) : CInt -> 0)
|
||||
(check-type (+ (ann 1 : PosInt) (ann 10 : PosInt)) : Nat -> 11)
|
||||
(check-type (+ (ann -10 : NegInt) (ann 10 : PosInt)) : Int -> 0)
|
||||
|
||||
;; if tests
|
||||
;; if expr has concrete type only if test and both branches are concrete
|
||||
(check-type (if #t 1 #f) : (CU CBool CInt))
|
||||
(check-type (if #t 1 #f) : (U CBool CInt))
|
||||
(check-type (if #t 1 #f) : (U Bool CInt))
|
||||
(check-type (if #t 1 #f) : (U Bool Int))
|
||||
(check-type (if #t 1 2) : CInt)
|
||||
(check-type (if #t 1 2) : Int)
|
||||
(check-type (if #t 1 2) : (CU CInt CBool))
|
||||
(check-type (if #t 1 2) : (U Int Bool))
|
||||
;; non-bool test
|
||||
(check-type (if 1 2 3) : CInt)
|
||||
;; else, if expr produces symbolic type
|
||||
(define-symbolic b0 boolean?)
|
||||
(define-symbolic i0 integer?)
|
||||
(typecheck-fail (define-symbolic posint1 positive?)
|
||||
#:with-msg "Expected a Rosette-solvable type, given positive?")
|
||||
(typecheck-fail (lambda ([x : (Constant CInt)]) x)
|
||||
#:with-msg "Constant requires a symbolic type")
|
||||
(check-type b0 : Bool -> b0)
|
||||
(check-type b0 : (Constant Bool) -> b0)
|
||||
(check-not-type b0 : CBool)
|
||||
(check-type i0 : Int -> i0)
|
||||
(check-type i0 : (Constant Int) -> i0)
|
||||
(check-type (if b0 1 2) : Int)
|
||||
(check-not-type (if b0 1 2) : CInt)
|
||||
(check-type (if #t i0 2) : Int)
|
||||
(check-not-type (if #t i0 2) : CInt)
|
||||
(check-type (if #t 2 i0) : Int)
|
||||
(check-not-type (if #t 2 i0) : CInt)
|
||||
(check-type (if b0 i0 2) : Int)
|
||||
(check-type (if b0 1 #f) : (U CInt CBool))
|
||||
(check-type (if b0 1 #f) : (U Int Bool))
|
||||
;; slightly unintuitive case: (U Int Bool) <: (U CInt Bool), ok for now (see notes)
|
||||
(check-type (if #f i0 #f) : (U CInt CBool))
|
||||
(check-type (if #f i0 #f) : (U CInt Bool))
|
||||
(check-type (if #f i0 #f) : (U Int Bool))
|
||||
(check-type (if #f (+ i0 1) #f) : (U Int Bool))
|
||||
|
||||
;; BVs
|
||||
|
||||
(check-type bv : (Ccase-> (C→ CInt CBVPred CBV)
|
||||
(C→ CInt CPosInt CBV)))
|
||||
(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)))
|
||||
(typecheck-fail (bv (ann 1 : Int) 2) #:with-msg "expected.*CInt")
|
||||
(typecheck-fail (bv (ann 1 : Int) (bitvector 2)) #:with-msg "expected.*CInt")
|
||||
|
||||
(typecheck-fail (bv 0 0) #:with-msg "expected.*PosInt.*given.*Zero")
|
||||
(check-type bitvector : (C→ CPosInt CBVPred))
|
||||
(check-type (bitvector 3) : CBVPred)
|
||||
(check-type ((bitvector 4) 1) : Bool -> #f)
|
||||
(check-type ((bitvector 4) (bv 10 (bitvector 4))) : Bool)
|
||||
|
||||
(check-type (bitvector? "2") : Bool -> #f)
|
||||
(check-type (bitvector? (bitvector 10)) : Bool -> #t)
|
||||
|
||||
;; 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)))
|
||||
(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))
|
||||
|
||||
;; 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?)
|
||||
(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))
|
||||
;; TODO: see rosette issue #23 --- issue closed, won't fix
|
||||
(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))
|
||||
(define-symbolic z (bitvector 3))
|
||||
(check-type (bvneg z) : BV)
|
||||
(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))
|
||||
;; TODO: see rosette issue #23 --- issue closed, won't fix
|
||||
(check-type (bvadd (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 (bvsrem (bv -3 4) (if b (bv 2 4) (bv 3 4))) : BV
|
||||
-> (if b (bv -1 4) (bv 0 4)))
|
||||
(check-type (concat (concat (bv -1 4) (bv 0 1)) (bv -1 3)) : BV -> (bv -9 8))
|
||||
(check-type (concat (concat (bv -1 4) (if b (bv 0 1) (bv 0 2))) (bv -1 3)) : BV
|
||||
-> (if b (bv -9 8) (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)
|
||||
; -> {[(&& (= 0 j) (= 1 i)) (bv 1 2)] ...})
|
||||
|
||||
(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 -> (if b (bv 13 5) (bv 13 6)))
|
||||
(check-type+asserts
|
||||
(zero-extend (bv -3 4) (assert-type (if b (bitvector 5) "bad") : BVPred))
|
||||
: BV -> (bv 13 5) (list b))
|
||||
(check-type+asserts (zero-extend (bv -3 4) (if c (bitvector 5) (bitvector 1)))
|
||||
: BV -> (bv 13 5) (list c))
|
||||
|
||||
(check-type (bitvector->integer (bv -1 4)) : Int -> -1)
|
||||
(check-type (bitvector->natural (bv -1 4)) : Int -> 15)
|
||||
(check-type (bitvector->integer (if b (bv -1 3) (bv -3 4)))
|
||||
: Int -> (if b -1 -3))
|
||||
(check-type+asserts
|
||||
(bitvector->integer (assert-type (if b (bv -1 3) "bad") : BV))
|
||||
: Int -> -1 (list b))
|
||||
(check-type (integer->bitvector 4 (bitvector 2)) : BV -> (bv 0 2))
|
||||
(check-type (integer->bitvector 15 (bitvector 4)) : BV -> (bv -1 4))
|
||||
(check-type+asserts (integer->bitvector (assert-type (if b pi 3) : Int)
|
||||
(if c (bitvector 5) (bitvector 6)))
|
||||
: BV -> (integer->bitvector 3 (if c (bitvector 5) (bitvector 6)))
|
||||
(list (not b)))
|
||||
;; TODO: check that CInt also has the right pred (do we want this?)
|
||||
#;(check-type+asserts (integer->bitvector (assert-type (if b pi 3) : CInt)
|
||||
(if c (bitvector 5) (bitvector 6)))
|
||||
: BV -> (integer->bitvector 3 (if c (bitvector 5) (bitvector 6)))
|
||||
(list (not b)))
|
||||
(check-type (integer->bitvector 3
|
||||
(if c (bitvector 5) (bitvector 6)))
|
||||
: BV -> (if c (bv 3 5) (bv 3 6)))
|
||||
|
||||
;; case-> subtyping
|
||||
(check-type ((λ ([f : (C→ Int Int)]) (f 10)) add1) : Int -> 11)
|
||||
(check-type ((λ ([f : (Ccase-> (C→ Int Int))]) (f 10)) add1) : Int -> 11)
|
||||
(check-type ((λ ([f : (Ccase-> (C→ Nat Nat)
|
||||
(C→ Int Int))]) (f 10)) add1) : Int -> 11)
|
||||
(check-not-type ((λ ([f : (Ccase-> (C→ Int Int))]) (f 10)) add1) : Nat)
|
||||
(check-type ((λ ([f : (Ccase-> (C→ Nat Nat)
|
||||
(C→ Int Int))]) (f 10)) add1) : Nat -> 11)
|
||||
(typecheck-fail ((λ ([f : (Ccase-> (C→ Zero Zero)
|
||||
(C→ Int Int))]) (f 10)) add1)
|
||||
#:with-msg
|
||||
(string-append "expected \\(Ccase-> \\(C→ Zero Zero\\) \\(C→ Int Int\\)\\), "
|
||||
"given \\(Ccase-> .*\\(C→ NegInt \\(U NegInt Zero\\)\\) .*\\(C→ Zero PosInt\\) "
|
||||
".*\\(C→ PosInt PosInt\\) .*\\(C→ Nat PosInt\\) .*\\(C→ Int Int\\)\\)"))
|
||||
|
||||
;; applying symbolic function types
|
||||
(check-type ((λ ([f : (U (C→ CInt CInt))]) (f 10)) add1) : Int -> 11)
|
||||
;; it's either (→ CInt CInt) or (→ CInt CBool), but not both, so
|
||||
;; add1 can have this type even though it never returns a boolean
|
||||
(check-type ((λ ([f : (U (C→ CInt CInt) (C→ CInt CBool))]) (f 10)) add1) : (U Int Bool) -> 11)
|
||||
(check-type ((λ ([f : (U (C→ CInt CInt) (C→ CInt Bool))]) (f 10))
|
||||
(if #t add1 positive?))
|
||||
: (U CInt Bool) -> 11)
|
||||
(check-type ((λ ([f : (U (C→ CInt CInt) (C→ CInt Bool))]) (f 10))
|
||||
(if #t add1 positive?))
|
||||
: (U Int Bool) -> 11)
|
||||
;; concrete union of functions
|
||||
(check-type ((λ ([f : (CU (C→ CInt CInt) (C→ CInt CBool))]) (f 10)) add1) : (CU CInt CBool) -> 11)
|
||||
(check-type ((λ ([f : (CU (C→ CInt CInt) (C→ CInt CBool))]) (f 10))
|
||||
(if #t add1 positive?))
|
||||
: (CU CInt CBool) -> 11)
|
||||
|
||||
;; check BVPred as type annotation
|
||||
;; 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")
|
||||
(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))
|
||||
(check-runtime-exn (assert-type (sub1 1) : PosInt))
|
||||
(define-symbolic b1 b2 boolean?)
|
||||
|
||||
(check-type (clear-asserts!) : CUnit -> (void))
|
||||
;; asserts directly on a symbolic union
|
||||
(check-type+asserts (assert-type (if b1 1 #f) : Int) : Int -> 1 (list b1))
|
||||
(check-type+asserts (assert-type (if b2 1 #f) : Bool) : Bool -> #f (list (not b2)))
|
||||
;; asserts on the (pc)
|
||||
(check-type+asserts (if b1 (assert-type 1 : Int) (assert-type #f : Int)) : Int
|
||||
-> 1 (list b1))
|
||||
(check-type+asserts (if b2 (assert-type 1 : Bool) (assert-type #f : Bool)) : Bool
|
||||
-> #f (list (not b2)))
|
||||
;; asserts on a define-symbolic value
|
||||
(define-symbolic i1 integer?)
|
||||
(check-type+asserts (assert-type i1 : PosInt) : PosInt -> i1 (list (< 0 i1)))
|
||||
(check-type+asserts (assert-type i1 : Zero) : Zero -> i1 (list (= 0 i1)))
|
||||
(check-type+asserts (assert-type i1 : NegInt) : NegInt -> i1 (list (< i1 0)))
|
||||
;; TODO: should this assertion be equivalent to (<= 0 i1) ?
|
||||
(check-type+asserts (assert-type i1 : Nat) : Nat -> i1 (list (not (< i1 0))))
|
||||
;; asserts on other terms involving define-symbolic values
|
||||
(check-type+asserts (assert-type (+ i1 1) : PosInt) : PosInt -> (+ 1 i1) (list (< 0 (+ 1 i1))))
|
||||
(check-type+asserts (assert-type (+ i1 1) : Zero) : Zero -> (+ 1 i1) (list (= 0 (+ 1 i1))))
|
||||
(check-type+asserts (assert-type (+ i1 1) : NegInt) : NegInt -> (+ 1 i1) (list (< (+ 1 i1) 0)))
|
||||
|
||||
(check-type+asserts (assert-type (if b1 i1 b2) : Int) : Int -> i1 (list b1))
|
||||
(check-type+asserts (assert-type (if b1 i1 b2) : Bool) : Bool -> b2 (list (not b1)))
|
||||
;; asserts on the (pc)
|
||||
(check-type+asserts (if b1 (assert-type i1 : Int) (assert-type b2 : Int)) : Int
|
||||
-> i1 (list b1))
|
||||
(check-type+asserts (if b1 (assert-type i1 : Bool) (assert-type b2 : Bool)) : Bool
|
||||
-> b2 (list (not b1)))
|
||||
;; TODO: should assert-type cause some predicates to return true or return false?
|
||||
(check-type+asserts (integer? (assert-type (if b1 i1 b2) : Int)) : Bool -> #t (list b1))
|
||||
(check-type+asserts (integer? (assert-type (if b1 i1 b2) : Bool)) : Bool -> #f (list (not b1)))
|
||||
(check-type+asserts (boolean? (assert-type (if b1 i1 b2) : Int)) : Bool -> #f (list b1))
|
||||
(check-type+asserts (boolean? (assert-type (if b1 i1 b2) : Bool)) : Bool -> #t (list (not b1)))
|
||||
|
||||
(check-type (asserts) : (CListof Bool) -> (list))
|
||||
|
||||
;; tests for Constant
|
||||
(define-symbolic ci1 integer?)
|
||||
(define-symbolic bi1 bi2 boolean?)
|
||||
|
||||
(check-type ci1 : (Constant Int))
|
||||
(check-type ci1 : Int)
|
||||
(check-type ci1 : (Constant Num))
|
||||
(check-type ci1 : Num)
|
||||
|
||||
;; homogeneous list of constants
|
||||
(check-type (list bi1 bi2) : (CList (Constant Bool) (Constant Bool)))
|
||||
(check-type (list bi1 bi2) : (CListof (Constant Bool)))
|
||||
|
||||
;; heterogeneous list of constants
|
||||
(check-type (list ci1 bi1) : (CList (Constant Int) (Constant Bool)))
|
||||
(check-type (cons ci1 (cons bi1 (list))) : (CList (Constant Int) (Constant Bool)))
|
||||
|
||||
(check-type
|
||||
(lambda ([x : CInt] [lst : (CListof CBool)]) (cons x lst))
|
||||
: (C→ CInt (CListof CBool) (CListof (CU CInt CBool))))
|
||||
(check-not-type
|
||||
(lambda ([x : Int] [lst : (CListof Bool)]) (cons x lst))
|
||||
: (C→ Int (CListof Bool) (CListof (CU CInt CBool))))
|
||||
(check-type
|
||||
(lambda ([x : Int] [lst : (CListof Bool)]) (cons x lst))
|
||||
: (C→ Int (CListof Bool) (CListof (U Int Bool))))
|
||||
|
||||
;; TODO: should these tests hold?
|
||||
;(check-type ci1 : (U (Constant Int) (Constant Bool)))
|
||||
;(check-type (list ci1 bi1) : (CListof (U (Constant Int) (Constant Bool))))
|
||||
;(check-type (cons ci1 (cons bi1 (list))) : (CListof (U (Constant Int) (Constant Bool))))
|
||||
|
|
@ -0,0 +1,23 @@
|
|||
#lang racket/base
|
||||
|
||||
(require macrotypes/examples/tests/do-tests)
|
||||
|
||||
(do-tests
|
||||
"rosette3-tests.rkt" "General"
|
||||
"rosette-guide-sec2-tests.rkt" "Rosette Guide, Section 2"
|
||||
"rosette-guide-sec3-tests.rkt" "Rosette Guide, Section 3"
|
||||
"rosette-guide-sec4-tests.rkt" "Rosette Guide, Section 4.1-4.2"
|
||||
"rosette-guide-sec43-tests.rkt" "Rosette Guide, Section 4.3 BVs"
|
||||
"rosette-guide-sec44-tests.rkt" "Rosette Guide, Section 4.4 Uninterp Fns"
|
||||
"rosette-guide-sec45-tests.rkt" "Rosette Guide, Section 4.5 Procedures"
|
||||
"rosette-guide-sec46-tests.rkt" "Rosette Guide, Section 4.6-4.8")
|
||||
|
||||
(do-tests
|
||||
"rosette-guide-sec49-tests.rkt" "Rosette Guide, Section 4.9"
|
||||
"rosette-guide-sec5-tests.rkt" "Rosette Guide, Section 5 Structures"
|
||||
"rosette-guide-sec6-tests.rkt" "Rosette Guide, Section 6 Libraries"
|
||||
"rosette-guide-sec7-tests.rkt" "Guide Sec. 7 Reflecting on Symbolic Values")
|
||||
|
||||
(do-tests "bv-tests.rkt" "BV SDSL - General"
|
||||
"bv-ref-tests.rkt" "BV SDSL - Hacker's Delight synthesis")
|
||||
|
||||
Loading…
Reference in New Issue
Block a user