From 8e55e443630bef2bf4be911965ed153df6a7e6f4 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Wed, 7 Sep 2016 12:23:50 -0400 Subject: [PATCH] eliminate type annotation in define-symbolic - relevant preds have analogous type as stx prop - add extra more precise solvable? and function? stx props - define-symbolic et al require explicit preds (no exprs) (for now) --- turnstile/examples/rosette/rosette-notes.txt | 5 + turnstile/examples/rosette/rosette2.rkt | 166 ++++++++++++++---- turnstile/examples/tests/rosette/bv-tests.rkt | 4 +- .../rosette/rosette-guide-sec2-tests.rkt | 16 +- .../rosette/rosette-guide-sec3-tests.rkt | 17 +- .../rosette/rosette-guide-sec4-tests.rkt | 30 ++-- .../rosette/rosette-guide-sec43-tests.rkt | 22 +++ .../examples/tests/rosette/rosette2-tests.rkt | 18 +- .../rosette/run-all-rosette-tests-script.rkt | 3 +- 9 files changed, 202 insertions(+), 79 deletions(-) create mode 100644 turnstile/examples/tests/rosette/rosette-guide-sec43-tests.rkt diff --git a/turnstile/examples/rosette/rosette-notes.txt b/turnstile/examples/rosette/rosette-notes.txt index bf65a9e..37acb7c 100644 --- a/turnstile/examples/rosette/rosette-notes.txt +++ b/turnstile/examples/rosette/rosette-notes.txt @@ -54,6 +54,11 @@ TODOs: - add pred properties to types - use it to validate given pred in define-symbolic - STARTED 2016-08-25 + - alternative: don't require type, but associate type with pred? + - advantage: soundness + - disadvantage: cannot compute pred in define-symbolic + - Rosette users won't care? + - TODO: add extra type rules to propagate 'typefor tag - implement assert-type, which adds to the assertion store - DONE 2016-08-25 - add polymorphism diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt index 9a6f724..b277e3b 100644 --- a/turnstile/examples/rosette/rosette2.rkt +++ b/turnstile/examples/rosette/rosette2.rkt @@ -85,7 +85,8 @@ (define-type-constructor CMVectorof #:arity = 1) (define-type-constructor CBoxof #:arity = 1) ;; TODO: Hash subtyping? -(define-type-constructor HashTable #:arity = 2) +;; - invariant for now, like TR, though Rosette only uses immutable hashes? +(define-type-constructor CHashTable #:arity = 2) (define-named-type-alias (CVectorof X) (CU (CIVectorof X) (CMVectorof X))) (define-type-constructor CList #:arity >= 0) @@ -134,10 +135,28 @@ (define (add-pred stx pred) (set-stx-prop/preserved stx 'pred pred)) (define (get-pred stx) - (syntax-property stx 'pred))) + (syntax-property stx 'pred)) + (define (add-typefor stx t) + (set-stx-prop/preserved stx 'typefor t)) + (define (get-typefor stx) + (syntax-property stx 'typefor)) + (define (mark-solvable stx) + (set-stx-prop/preserved stx 'solvable? #t)) + (define (solvable? stx) + (syntax-property stx 'solvable?)) + (define (mark-function stx) + (set-stx-prop/preserved stx 'function? #t)) + (define (function? stx) + (syntax-property stx 'function?))) (define-syntax-parser add-predm [(_ stx pred) (add-pred #'stx #'pred)]) +(define-syntax-parser add-typeform + [(_ stx t) (add-typefor #'stx #'t)]) +(define-syntax-parser mark-solvablem + [(_ stx) (mark-solvable #'stx)]) +(define-syntax-parser mark-functionm + [(_ stx) (mark-function #'stx)]) (define-named-type-alias NegInt (add-predm (U CNegInt) negative-integer?)) (define-named-type-alias Zero (add-predm (U CZero) zero-integer?)) @@ -177,51 +196,55 @@ ;; --------------------------------- ;; define-symbolic -(define-typed-syntax define-symbolic #:datum-literals (:) - [(_ x:id ...+ pred : ty:type) ≫ - #:fail-when (concrete? #'ty.norm) - (format "A symbolic value cannot have a concrete type, given ~a." - (type->str #'ty.norm)) - ;; TODO: still unsound - [⊢ [pred ≫ pred- ⇐ : (C→ ty.norm Bool)]] +(define-typed-syntax define-symbolic + [(_ x:id ...+ pred?) ≫ + [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]] + #:fail-unless (syntax-e #'s?) + (format "Must provide a Rosette-solvable type, given ~a." + (syntax->datum #'pred?)) #:with (y ...) (generate-temporaries #'(x ...)) -------- [_ ≻ (begin- - (define-syntax- x (make-rename-transformer (⊢ y : ty.norm))) ... - (ro:define-symbolic y ... pred-))]]) + (define-syntax- x (make-rename-transformer (⊢ y : ty))) ... + (ro:define-symbolic y ... pred?-))]]) -(define-typed-syntax define-symbolic* #:datum-literals (:) - [(_ x:id ...+ pred : ty:type) ≫ - #:fail-when (concrete? #'ty.norm) - (format "A symbolic value cannot have a concrete type, given ~a." - (type->str #'ty.norm)) - ;; TODO: still unsound - [⊢ [pred ≫ pred- ⇐ : (C→ ty.norm Bool)]] +(define-typed-syntax define-symbolic* + [(_ x:id ...+ pred?) ≫ + [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]] + #:fail-unless (syntax-e #'s?) + (format "Must provide a Rosette-solvable type, given ~a." + (syntax->datum #'pred?)) #:with (y ...) (generate-temporaries #'(x ...)) -------- [_ ≻ (begin- - (define-syntax- x (make-rename-transformer (⊢ y : ty.norm))) ... - (ro:define-symbolic* y ... pred-))]]) + (define-syntax- x (make-rename-transformer (⊢ y : ty))) ... + (ro:define-symbolic* y ... pred?-))]]) ;; TODO: support internal definition contexts (define-typed-syntax let-symbolic - [(_ ([(x:id ...+) pred : ty:type]) e ...) ≫ - [⊢ [pred ≫ pred- ⇐ : (C→ ty.norm Bool)]] - [([x ≫ x- : ty.norm] ...) ⊢ [(begin e ...) ≫ e- ⇒ τ_out]] + [(_ (x:id ...+ pred?) e ...) ≫ + [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]] + #:fail-unless (syntax-e #'s?) + (format "Must provide a Rosette-solvable type, given ~a." + (syntax->datum #'pred?)) + [([x ≫ x- : ty] ...) ⊢ [(begin e ...) ≫ e- ⇒ τ_out]] -------- [⊢ [_ ≫ (ro:let-values ([(x- ...) (ro:let () - (ro:define-symbolic x ... pred-) + (ro:define-symbolic x ... pred?-) (ro:values x ...))]) e-) ⇒ : τ_out]]]) (define-typed-syntax let-symbolic* - [(_ ([(x:id ...+) pred : ty:type]) e ...) ≫ - [⊢ [pred ≫ pred- ⇐ : (C→ ty.norm Bool)]] - [([x ≫ x- : ty.norm] ...) ⊢ [(begin e ...) ≫ e- ⇒ τ_out]] + [(_ (x:id ...+ pred?) e ...) ≫ + [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?)]] + #:fail-unless (syntax-e #'s?) + (format "Must provide a Rosette-solvable type, given ~a." + (syntax->datum #'pred?)) + [([x ≫ x- : ty] ...) ⊢ [(begin e ...) ≫ e- ⇒ τ_out]] -------- [⊢ [_ ≫ (ro:let-values ([(x- ...) (ro:let () - (ro:define-symbolic* x ... pred-) + (ro:define-symbolic* x ... pred?-) (ro:values x ...))]) e-) ⇒ : τ_out]]]) @@ -455,7 +478,11 @@ ;; --------------------------------- ;; hash tables -(define-rosette-primop hash-keys : (C→ (HashTable Any Any) (CListof Any))) +(define-typed-syntax hash-keys + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CHashTable τ _)]] + -------- + [⊢ [_ ≫ (ro:hash-keys e-) ⇒ : (CListof τ)]]]) ;; --------------------------------- ;; lists @@ -734,9 +761,6 @@ [true : CTrue] [false : CFalse] - [boolean? : (C→ Any Bool)] - [integer? : (C→ Any Bool)] - [real? : (C→ Any Bool)] [number? : (C→ Any Bool)] [positive? : (Ccase-> (C→ CNum CBool) (C→ Num Bool))] @@ -763,6 +787,49 @@ [asserts : (C→ (CListof Bool))] [clear-asserts! : (C→ CUnit)])) +;; --------------------------------- +;; more built-in ops +;(define-rosette-primop boolean? : (C→ Any Bool)) +(define-typed-syntax boolean? + [_:id ≫ + -------- + [⊢ [_ ≫ (mark-solvablem + (add-typeform + ro:boolean? + Bool)) + ⇒ : (C→ Any Bool)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : ty]] + -------- + [⊢ [_ ≫ (ro:boolean? e-) ⇒ : #,(if (concrete? #'ty) #'CBool #'Bool)]]]) + +;(define-rosette-primop integer? : (C→ Any Bool)) +(define-typed-syntax integer? + [_:id ≫ + -------- + [⊢ [_ ≫ (mark-solvablem + (add-typeform + ro:integer? + Int)) + ⇒ : (C→ Any Bool)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : ty]] + -------- + [⊢ [_ ≫ (ro:integer? e-) ⇒ : #,(if (concrete? #'ty) #'CBool #'Bool)]]]) + +;(define-rosette-primop real? : (C→ Any Bool)) +(define-typed-syntax real? + [_:id ≫ + -------- + [⊢ [_ ≫ (mark-solvablem + (add-typeform + ro:real? + Num)) ⇒ : (C→ Any Bool)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : ty]] + -------- + [⊢ [_ ≫ (ro:real? e-) ⇒ : #,(if (concrete? #'ty) #'CBool #'Bool)]]]) + ;; --------------------------------- ;; mutable boxes @@ -801,7 +868,6 @@ (provide (rosette-typed-out [bv : (Ccase-> (C→ CInt CBVPred CBV) (C→ CInt CPosInt CBV))] [bv? : (C→ Any Bool)] - [bitvector : (C→ CPosInt CBVPred)] [bitvector? : (C→ Any Bool)] [bveq : (C→ BV BV Bool)] @@ -846,14 +912,38 @@ [bitvector-size : (C→ CBVPred CPosInt)])) +;(define-rosette-primop bitvector : (C→ CPosInt CBVPred)) +(define-typed-syntax bitvector + [_:id ≫ + -------- + [⊢ [_ ≫ ro:bitvector ⇒ : (C→ CPosInt CBVPred)]]] + [(_ n) ≫ + [⊢ [n ≫ n- ⇐ : CPosInt]] + -------- + [⊢ [_ ≫ (mark-solvablem + (add-typeform + (ro:bitvector n-) + BV)) ⇒ : CBVPred]]]) + ;; --------------------------------- ;; Uninterpreted functions (define-typed-syntax ~> - [(_ e ...+) ≫ - [⊢ [e ≫ e- ⇐ : (C→ Nothing Bool)] ...] + [(_ pred? ...+) ≫ + [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]] ... + #:fail-unless (stx-andmap syntax-e #'(s? ...)) + (format "Must provide a Rosette-solvable type, given ~a." + (syntax->datum #'(pred? ...))) + #:fail-when (stx-ormap syntax-e #'(f? ...)) + (format "Must provide a non-function Rosette type, given ~a." + (syntax->datum #'(pred? ...))) -------- - [⊢ [_ ≫ (ro:~> e- ...) ⇒ : (C→ Any Bool)]]]) + [⊢ [_ ≫ (mark-solvablem + (mark-functionm + (add-typeform + (ro:~> pred?- ...) + (C→ ty ...)))) + ⇒ : (C→ Any Bool)]]]) ;; --------------------------------- ;; Logic operators @@ -925,9 +1015,9 @@ (provide (rosette-typed-out [core : (C→ CSolution (U (Listof Any) CFalse))] ; TODO: implement hash - [model : (C→ CSolution (HashTable Any Any))] + [model : (C→ CSolution (CHashTable Any Any))] [sat : (Ccase-> (C→ CSolution) - (C→ (HashTable Any Any) CSolution))] + (C→ (CHashTable Any Any) CSolution))] [sat? : (C→ Any Bool)] [unsat? : (C→ Any Bool)] [unsat : (Ccase-> (C→ CSolution) diff --git a/turnstile/examples/tests/rosette/bv-tests.rkt b/turnstile/examples/tests/rosette/bv-tests.rkt index 186ea43..72a60d3 100644 --- a/turnstile/examples/tests/rosette/bv-tests.rkt +++ b/turnstile/examples/tests/rosette/bv-tests.rkt @@ -17,8 +17,8 @@ (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? : Int) -(define-symbolic b boolean? : Bool) +(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))) diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt index 3245239..7284ed6 100644 --- a/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt @@ -4,7 +4,7 @@ ;; all examples from the Rosette Guide, Sec 2 -(define-symbolic b boolean? : Bool) +(define-symbolic b boolean?) (check-type b : Bool) (check-type (boolean? b) : Bool -> #t) (check-type (integer? b) : Bool -> #f) @@ -25,17 +25,17 @@ (check-type (not b) : Bool -> (! b)) (check-type (boolean? (not b)) : Bool -> #t) -(define-symbolic* n integer? : Int) +(define-symbolic* n integer?) ;; TODO: support internal definition contexts (define (static -> Bool) - (let-symbolic ([(x) boolean? : Bool]) x)) + (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? : Int]) y)) + (let-symbolic* (y integer?) y)) #;(define (dynamic -> Int) (define-symbolic* y integer? : Int) ; creates a different constant when evaluated y) @@ -52,7 +52,7 @@ (check-type (eq? sym*1 sym*2) : Bool -> (= sym*1 sym*2)) (define (yet-another-x -> Bool) - (let-symbolic ([(x) boolean? : Bool]) x)) + (let-symbolic (x boolean?) x)) (check-type (eq? (static) (yet-another-x)) : Bool -> (<=> (static) (yet-another-x))) @@ -82,7 +82,7 @@ ;; 2.3.1 Verification -(define-symbolic i integer? : Int) +(define-symbolic i integer?) (define cex (verify (same poly factored i))) (check-type cex : CSolution) (check-type (sat? cex) : Bool -> #t) @@ -124,7 +124,7 @@ ;; 2.3.4 Angelic Execution -(define-symbolic x y integer? : Int) +(define-symbolic x y integer?) (define sol (solve (begin (assert (not (= x y))) (assert (< (abs x) 10)) @@ -141,7 +141,7 @@ ;; 2.4 Symbolic Reasoning -(define-symbolic x1 y1 real? : Num) +(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) diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt index 9bbe5e9..03fe292 100644 --- a/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette-guide-sec3-tests.rkt @@ -13,7 +13,8 @@ ;; y1 unchanged: 0 (check-type y1 : Nat -> 0) ;; symbolic effect! -(define-symbolic x1 boolean? : Bool) +(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)) @@ -25,7 +26,7 @@ (printf "y unchanged: ~a\n" y) (if #f (set! y 3) (void)) (printf "y unchanged: ~a\n" y) - (let-symbolic ([(x) boolean? : Bool]) + (let-symbolic (x boolean?) (if x (void) (set! y 3)) (printf "y symbolic: ~a\n" y) (list x y)))) @@ -41,13 +42,13 @@ ;; 3.2.1 Symbolic Constants (define (always-same -> Int) - (let-symbolic ([(x) integer? : 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? : Int]) + (let-symbolic* (x integer?) x)) (check-type (always-different) : Int) (define diff-sym*1 (always-different)) @@ -58,7 +59,7 @@ (check-type+asserts (assert #t) : Unit -> (void) (list)) (check-type+asserts (assert 1) : Unit -> (void) (list)) -(define-symbolic x123 boolean? : Bool) +(define-symbolic x123 boolean?) (check-type+asserts (assert x123) : Unit -> (void) (list x123)) (check-runtime-exn (assert #f "bad value")) @@ -67,7 +68,7 @@ (check-type (asserts) : (CListof Bool) -> (list)) ;; 3.2.3 Angelic Execution -(define-symbolic x y boolean? : Bool) +(define-symbolic x y boolean?) (check-type (assert x) : Unit -> (void)) (check-type (asserts) : (CListof Bool) -> (list x)) (define solve-sol (solve (assert y))) @@ -90,7 +91,7 @@ (clear-asserts!) ;; 3.2.5 Synthesis -(define-symbolic synth-x synth-c integer? : Int) +(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 @@ -103,7 +104,7 @@ ;; 3.2.6 Optimization (current-bitwidth #f) ; use infinite-precision arithmetic -(define-symbolic opt-x opt-y integer? : Int) +(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 diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt index d5fdd0f..79ca61c 100644 --- a/turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt @@ -2,7 +2,7 @@ (require "../rackunit-typechecking.rkt" "check-type+asserts.rkt") -;; Examples from the Rosette Guide, Section 4 +;; Examples from the Rosette Guide, Section 4.1 - 4.2 ;; 4.1 Equality @@ -22,15 +22,16 @@ (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? : Int) +(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) -(define-symbolic f g (~> integer? integer?) : (→ Int Int)) -(typecheck-fail - (define-symbolic f g (~> integer? integer?) : (C→ Int Int)) - #:with-msg "symbolic value cannot have a concrete type") +(typecheck-fail (~> positive?) + #:with-msg "Must provide a Rosette\\-solvable type, given.*positive?") +(typecheck-fail (~> (~> integer?)) + #:with-msg "Must provide 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) @@ -49,16 +50,16 @@ (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? : Int) +(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? : Bool) +(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? : Bool) +;(define-symbolic b boolean?) (check-type (boolean? b) : Bool -> #t) (check-type (boolean? #t) : Bool -> #t) (check-type (boolean? #f) : Bool -> #t) @@ -211,7 +212,7 @@ (check-type (||) : Bool -> #f) ; no shortcircuiting (check-type (&& #f (begin (displayln "hello") #t)) : Bool -> #f) -(define-symbolic a boolean? : Bool) +(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 @@ -227,21 +228,22 @@ (current-bitwidth #f) -(define-symbolic a1 b1 integer? : Int) +(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 ; so the model has no bindings (define sol1 (solve (assert f1))) (check-type sol1 : CSolution) -(check-type (model sol1) : (HashTable Any Any)) +(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)))) ; b is free in g +(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) -(define h (exists (list a1) (forall (list a1) (= a1 (+ a1 a1))))) ; body refers to the innermost a +; 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)) diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec43-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec43-tests.rkt new file mode 100644 index 0000000..3eff78d --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette-guide-sec43-tests.rkt @@ -0,0 +1,22 @@ +#lang s-exp "../../rosette/rosette2.rkt" +(require "../rackunit-typechecking.rkt" + "check-type+asserts.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) +;; > (bvult (bv 4 7) (bv -1 7)) ; unsigned 7-bit < comparison of 4 and -1 +;; #t +;; > (define-symbolic b boolean?) +;; > (bvadd x (if b y (bv 3 4))) ; this typechecks only when b is true +;; (bvadd x y) +;; > (asserts) ; so Rosette emits a corresponding assertion +;; '(b) diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt index efedb3a..986bc64 100644 --- a/turnstile/examples/tests/rosette/rosette2-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette2-tests.rkt @@ -99,8 +99,10 @@ ;; non-bool test (check-type (if 1 2 3) : CInt) ;; else, if expr produces symbolic type -(define-symbolic b0 boolean? : Bool) -(define-symbolic i0 integer? : Int) +(define-symbolic b0 boolean?) +(define-symbolic i0 integer?) +(typecheck-fail (define-symbolic posint1 positive?) + #:with-msg "Must provide a Rosette-solvable type, given positive?") (check-type (if b0 1 2) : Int) (check-not-type (if b0 1 2) : CInt) (check-type (if #t i0 2) : Int) @@ -154,7 +156,7 @@ (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? : Bool) +(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))) @@ -166,7 +168,7 @@ (check-type (bvneg (bv -1 4)) : BV -> (bv 1 4)) (check-type (bvneg (bv 0 4)) : BV -> (bv 0 4)) -(define-symbolic z (bitvector 3) : BV) +(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)) @@ -184,13 +186,13 @@ (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? : Int) +(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? : Bool) +(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 @@ -264,7 +266,7 @@ ;; 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? : Bool) +(define-symbolic b1 b2 boolean?) (check-type (clear-asserts!) : CUnit -> (void)) ;; asserts directly on a symbolic union @@ -276,7 +278,7 @@ (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? : Int) +(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))) diff --git a/turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt b/turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt index bd11507..ccf640f 100644 --- a/turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt +++ b/turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt @@ -5,7 +5,8 @@ (do-tests "rosette2-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") + "rosette-guide-sec4-tests.rkt" "Rosette Guide, Section 4.1-4.2" + "rosette-guide-sec43-tests.rkt" "Rosette Guide, Section 4.3") (do-tests "bv-tests.rkt" "BV SDSL - General" "bv-ref-tests.rkt" "BV SDSL - Hacker's Delight synthesis")