From 98e5cdc77f2a8c9ce1653ad5b2413e9730776f49 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Mon, 29 Aug 2016 11:26:22 -0400 Subject: [PATCH] add more assert-type tests --- turnstile/examples/rosette/rosette2.rkt | 35 ++++++++++++++----- .../examples/tests/rosette/rosette2-tests.rkt | 32 ++++++++++++++++- 2 files changed, 57 insertions(+), 10 deletions(-) diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt index 177fa14..7443021 100644 --- a/turnstile/examples/rosette/rosette2.rkt +++ b/turnstile/examples/rosette/rosette2.rkt @@ -10,7 +10,8 @@ CU U C→ → (for-syntax ~C→ C→?) Ccase-> ; TODO: symbolic case-> not supported yet - CUnit CList CParam ; TODO: symbolic Param not supported yet + CList CParam ; TODO: symbolic Param not supported yet + CUnit Unit CNegInt NegInt CZero Zero CPosInt PosInt @@ -104,15 +105,22 @@ (define-syntax-parser add-predm [(_ stx pred) (add-pred #'stx #'pred)]) -(define-named-type-alias NegInt (U CNegInt)) -(define-named-type-alias Zero (U CZero)) -(define-named-type-alias PosInt - (add-predm (U CPosInt) - (lambda (x) - (ro:and (ro:#%app ro:integer? x) (ro:#%app ro:positive? x))))) +(ro:define (ro:zero-integer? x) + (ro:and (ro:#%app ro:integer? x) (ro:#%app ro:zero? x))) +(ro:define (ro:positive-integer? x) + (ro:and (ro:#%app ro:integer? x) (ro:#%app ro:positive? x))) +(ro:define (ro:negative-integer? x) + (ro:and (ro:#%app ro:integer? x) (ro:#%app ro:negative? x))) +(ro:define (no:nonnegative-integer? x) + (ro:and (ro:#%app ro:integer? x) (ro:#%app ro:not (ro:#%app ro:negative? x)))) + +(define-named-type-alias NegInt (add-predm (U CNegInt) ro:negative-integer?)) +(define-named-type-alias Zero (add-predm (U CZero) ro:zero-integer?)) +(define-named-type-alias PosInt (add-predm (U CPosInt) ro:positive-integer?)) (define-named-type-alias Float (U CFloat)) (define-named-type-alias Bool (add-predm (U CBool) ro:boolean?)) (define-named-type-alias String (U CString)) +(define-named-type-alias Unit (add-predm (U CUnit) ro:void?)) (define-named-type-alias (CParam X) (Ccase-> (C→ X) (C→ X CUnit))) @@ -132,8 +140,7 @@ (define-named-type-alias CName Cτ) (define-named-type-alias Name (add-predm (U CName) p?)))])) -(define-symbolic-named-type-alias Nat (CU CZero CPosInt) - #:pred (lambda (x) (ro:and (ro:integer? x) (ro:not (ro:negative? x))))) +(define-symbolic-named-type-alias Nat (CU CZero CPosInt) #:pred no:nonnegative-integer?) (define-symbolic-named-type-alias Int (CU CNegInt CNat) #:pred ro:integer?) (define-symbolic-named-type-alias Num (CU CFloat CInt) #:pred ro:real?) @@ -346,6 +353,16 @@ (C→ Int Int Int) (C→ CNum CNum CNum) (C→ Num Num Num))) +(define-rosette-primop = : (Ccase-> (C→ CInt CInt CBool) + (C→ Int Int Bool))) +(define-rosette-primop < : (Ccase-> (C→ CInt CInt CBool) + (C→ Int Int Bool))) +(define-rosette-primop > : (Ccase-> (C→ CInt CInt CBool) + (C→ Int Int Bool))) +(define-rosette-primop <= : (Ccase-> (C→ CInt CInt CBool) + (C→ Int Int Bool))) +(define-rosette-primop >= : (Ccase-> (C→ CInt CInt CBool) + (C→ Int Int Bool))) (define-rosette-primop not : (C→ Any Bool)) (define-rosette-primop false? : (C→ Any Bool)) diff --git a/turnstile/examples/tests/rosette/rosette2-tests.rkt b/turnstile/examples/tests/rosette/rosette2-tests.rkt index fa8561b..9ae8f78 100644 --- a/turnstile/examples/tests/rosette/rosette2-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette2-tests.rkt @@ -262,12 +262,42 @@ (check-type ((λ ([bvp : BVPred]) bvp) (λ ([bv : BV]) ((bitvector 2) bv))) : BVPred) ;; assert-type tests -(check-type (assert-type (sub1 10) : PosInt) : PosInt -> 9) +(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) (check-type (clear-asserts!) : CUnit -> (void)) +;; asserts directly on a symbolic union (check-type+asserts (assert-type (if b1 1 #f) : Int) : Int -> (if b1 1 #f) (list b1)) (check-type+asserts (assert-type (if b2 1 #f) : Bool) : Bool -> (if b2 1 #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? : Int) +(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 -> (if b1 i1 b2) (list b1)) +(check-type+asserts (assert-type (if b1 i1 b2) : Bool) : Bool -> (if b1 i1 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 -> b1 (list b1)) +(check-type+asserts (integer? (assert-type (if b1 i1 b2) : Bool)) : Bool -> b1 (list (not b1))) +(check-type+asserts (boolean? (assert-type (if b1 i1 b2) : Int)) : Bool -> (not b1) (list b1)) +(check-type+asserts (boolean? (assert-type (if b1 i1 b2) : Bool)) : Bool -> (not b1) (list (not b1))) (check-type (asserts) : (CList Bool) -> (list))