From 5862112f5781b9a3be0e11a1558c01f922d88a90 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Fri, 9 Sep 2016 10:44:04 -0400 Subject: [PATCH] add remaining sec44 guide tests; use term cache to improve testing --- turnstile/examples/rosette/rosette-notes.txt | 17 +++-- turnstile/examples/rosette/rosette2.rkt | 24 +++++++ .../rosette/rosette-guide-sec44-tests.rkt | 72 +++++++++++++++++-- 3 files changed, 102 insertions(+), 11 deletions(-) diff --git a/turnstile/examples/rosette/rosette-notes.txt b/turnstile/examples/rosette/rosette-notes.txt index a032e16..5801e69 100644 --- a/turnstile/examples/rosette/rosette-notes.txt +++ b/turnstile/examples/rosette/rosette-notes.txt @@ -9,7 +9,8 @@ res has type (Constant Int) but (constant? res) is false -** Workaround: +** Workaround: special case in evaluate + - still unsound with polymorphism 2016-09-08 -------------------- @@ -97,6 +98,8 @@ minimal example: Interesting parts of Typed Rosette - only need a single U symbolic constructor - assert-type, using cast-type and assertion store +- solvable?, function?, typefor tags +- Constant constructor? 2016-08-25 -------------------- @@ -109,14 +112,16 @@ TODOs: - disadvantage: cannot compute pred in define-symbolic - Rosette users won't care? - TODO: add extra type rules to propagate 'typefor tag + - DONE (alternative) 2016-09-07 - implement assert-type, which adds to the assertion store - DONE 2016-08-25 - add polymorphism - regular polymorphism + - BV size polymorphism? - extend BV type with a size - requires BV-size-polymorpism? - add Any type? - - STARTED 2016-08-26 + - STARTED 2016-08-26 DONE? - support internal definition contexts - fix type of Vector and List to differentiate homogeneous/hetero - 2016-09-01: add CList for hetero lists @@ -129,15 +134,19 @@ TODOs: - depends on macrotypes and rosette - create version of turnstile that does not provide #%module-begin - eg rename existing turnstile to turnstile/lang? + - DONE, see Alex's commit 2016-08-31 + - fixed set! bug - remove my-this-syntax stx param - add symbolic True and False? - orig stx prop confuses distinction between symbolic and non-sym values + in err msgs - use variance information in type constructors? - instead of special-casing individual constructors - ok to say "Rosette type" in type err msgs? -- 2016-09-08: fix Constant soundness wrt evaluate -- 2016-09-08: transfer "typefor" and "solvable?" props to id in define +- ADD 2016-09-08: fix Constant soundness wrt evaluate +- ADD 2016-09-08: transfer "typefor" and "solvable?" props to id in define - DONE 2016-09-08 +- is there a way to determine when evaluate produces concrete vals? 2016-08-25 -------------------- diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt index a65013d..d096471 100644 --- a/turnstile/examples/rosette/rosette2.rkt +++ b/turnstile/examples/rosette/rosette2.rkt @@ -883,6 +883,14 @@ -------- [⊢ [_ ≫ (ro:unbox e-) ⇒ : τ]]]) +(define-rosette-primop term-cache + : (Ccase-> (C→ (CHashTable Any Any)) + (C→ (CHashTable Any Any) CUnit))) +(define-rosette-primop clear-terms! + : (Ccase-> (C→ CUnit) + (C→ CFalse CUnit) + (C→ (CListof Any) CUnit))) ; list of terms + ;; --------------------------------- ;; BV Types and Operations @@ -1004,6 +1012,22 @@ (define-rosette-primop fv? : (C→ Any Bool)) +;; function? can produce type CFalse if input does not have type (C→ Any Bool) +;; result is always CBool, since anything symbolic returns false +;(define-rosette-primop function? : (C→ Any Bool)) +(define-typed-syntax function? + [_:id ≫ + -------- + [⊢ [_ ≫ ro:function? ⇒ : (C→ Any CBool)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇐ : (C→ Any Bool)]] + -------- + [⊢ [_ ≫ (ro:function? e-) ⇒ : CBool]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : _]] + -------- + [⊢ [_ ≫ (ro:function? e-) ⇒ : CFalse]]]) + ;; --------------------------------- ;; Logic operators (provide (rosette-typed-out [! : (C→ Bool Bool)] diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec44-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec44-tests.rkt index fd8b551..154f5cd 100644 --- a/turnstile/examples/tests/rosette/rosette-guide-sec44-tests.rkt +++ b/turnstile/examples/tests/rosette/rosette-guide-sec44-tests.rkt @@ -22,29 +22,41 @@ (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?) -;; should this be Num or Int? -;(check-type (evaluate x sol) : Int -> 0) -(check-type (evaluate x sol) : Num -> 0) ; nondeterministic result -;; check soundness of Constant -(check-not-type (evaluate x sol) : (Constant Num)) ; 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))) ; nondet result -;; this should be the only test that is deterministic +(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))) @@ -55,3 +67,49 @@ (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)