From a846514f281aa98d16892ec8be56c9418a5eac9f Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Wed, 25 May 2016 17:45:59 -0400 Subject: [PATCH] make cast sound --- .../scribblings/reference/special-forms.scrbl | 13 +++- .../typed-racket/base-env/prims-contract.rkt | 49 +++++++++--- .../typed-racket/private/cast-table.rkt | 25 +++++++ .../private/syntax-properties.rkt | 3 +- .../typed-racket/private/type-contract.rkt | 16 +++- .../typed-racket/private/with-types.rkt | 3 +- .../typed-racket/typecheck/tc-expression.rkt | 8 ++ typed-racket-test/succeed/cast-mod.rkt | 75 +++++++++++++++++-- typed-racket-test/succeed/cast-top-level.rkt | 72 +++++++++++++++++- 9 files changed, 243 insertions(+), 21 deletions(-) create mode 100644 typed-racket-lib/typed-racket/private/cast-table.rkt diff --git a/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl b/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl index a01a60d3..c5b7816a 100644 --- a/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl +++ b/typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl @@ -541,9 +541,18 @@ returned by @racket[e], protected by a contract ensuring that it has type @ex[(cast 3 Integer) (eval:error (cast 3 String)) -(cast (lambda: ([x : Any]) x) (String -> String)) +(cast (lambda ([x : Any]) x) (String -> String)) +((cast (lambda ([x : Any]) x) (String -> String)) "hello") ] -} + +The value is actually protected with two contracts. The second contract checks +the new type, but the first contract is put there to enforce the old type, to +protect higher-order uses of the value. + +@ex[ +((cast (lambda ([s : String]) s) (Any -> Any)) "hello") +(eval:error ((cast (lambda ([s : String]) s) (Any -> Any)) 5)) +]} @defform*[[(inst e t ...) (inst e t ... t ooo bound)]]{ diff --git a/typed-racket-lib/typed-racket/base-env/prims-contract.rkt b/typed-racket-lib/typed-racket/base-env/prims-contract.rkt index 8fa62d5f..d075e1d5 100644 --- a/typed-racket-lib/typed-racket/base-env/prims-contract.rkt +++ b/typed-racket-lib/typed-racket/base-env/prims-contract.rkt @@ -75,6 +75,7 @@ (for-template "../utils/any-wrap.rkt") "../utils/tc-utils.rkt" "../private/syntax-properties.rkt" + "../private/cast-table.rkt" "../typecheck/internal-forms.rkt" ;; struct-extraction is actually used at both of these phases "../utils/struct-extraction.rkt" @@ -250,9 +251,27 @@ ;; make-predicate ;; cast -;; Helper to construct syntax for contract definitions +;; Helpers to construct syntax for contract definitions +;; make-contract-def-rhs : Type-Stx Boolean Boolean -> Syntax (define (make-contract-def-rhs type flat? maker?) - (contract-def-property #'#f `#s(contract-def ,type ,flat? ,maker? untyped))) + (define contract-def `#s(contract-def ,type ,flat? ,maker? untyped)) + (contract-def-property #'#f (λ () contract-def))) + +;; make-contract-def-rhs/from-typed : Id Boolean Boolean -> Syntax +(define (make-contract-def-rhs/from-typed id flat? maker?) + (contract-def-property + #'#f + ;; This function should only be called after the type-checking pass has finished. + ;; By then `tc/#%expression` will have recognized the `casted-expr` property and + ;; will have added the casted expression's original type to the cast-table, so + ;; that `(cast-table-ref id)` can get that type here. + (λ () + (define type-stx + (or (cast-table-ref id) + (int-err (string-append + "contract-def-property: thunk called too early\n" + " This should only be called after the type-checking pass has finished.")))) + `#s(contract-def ,type-stx ,flat? ,maker? typed)))) (define (define-predicate stx) @@ -289,17 +308,17 @@ (define (cast stx) (syntax-parse stx [(_ v:expr ty:expr) - (define (apply-contract ctc-expr) + (define (apply-contract v ctc-expr pos neg) #`(#%expression #,(ignore-some/expr - #`(let-values (((val) #,(with-type* #'v #'Any))) + #`(let-values (((val) #,(with-type* v #'Any))) #,(syntax-property (quasisyntax/loc stx (contract #,ctc-expr val - 'cast - 'typed-world + '#,pos + '#,neg val (quote-srcloc #,stx))) 'feature-profile:TR-dynamic-check #t)) @@ -308,8 +327,15 @@ (cond [(not (unbox typed-context?)) ; no-check, don't check #'v] [else - (define ctc (syntax-local-lift-expression - (make-contract-def-rhs #'ty #f #f))) + (define new-ty-ctc (syntax-local-lift-expression + (make-contract-def-rhs #'ty #f #f))) + (define existing-ty-id new-ty-ctc) + (define existing-ty-ctc (syntax-local-lift-expression + (make-contract-def-rhs/from-typed existing-ty-id #f #f))) + (define (store-existing-type existing-type) + (cast-table-set! existing-ty-id existing-type)) + (when (equal? (syntax-local-context) 'top-level) + (store-existing-type #'Any)) (define (check-valid-type _) (define type (parse-type #'ty)) (define vars (fv type)) @@ -319,7 +345,12 @@ "Type ~a could not be converted to a contract because it contains free variables." type))) #`(#,(external-check-property #'#%expression check-valid-type) - #,(apply-contract ctc))])])) + #,(apply-contract + (apply-contract + #`(#,(casted-expr-property #'#%expression store-existing-type) + v) + existing-ty-ctc 'typed-world 'cast) + new-ty-ctc 'cast 'typed-world))])])) diff --git a/typed-racket-lib/typed-racket/private/cast-table.rkt b/typed-racket-lib/typed-racket/private/cast-table.rkt new file mode 100644 index 00000000..44aace7a --- /dev/null +++ b/typed-racket-lib/typed-racket/private/cast-table.rkt @@ -0,0 +1,25 @@ +#lang racket/base + +(provide cast-table-ref + cast-table-set!) + +(require syntax/id-table) + +;; A module that helps store information about the original types of casted +;; expressions. +;; +;; Casts in Typed Racket must generate two contracts. One from typed to untyped, +;; and another from untyped to typed. The contract from typed to untyped is +;; generated based on the existing type of the expression, which must be stored +;; in this table so that it can be looked up later in the contract-generation +;; pass. + +(define cast-table (make-free-id-table)) + +;; cast-table-set! : Id Type-Stx -> Void +(define (cast-table-set! id type-stx) + (free-id-table-set! cast-table id type-stx)) + +;; cast-table-ref : Id -> (U False Type-Stx) +(define (cast-table-ref id) + (free-id-table-ref cast-table id #f)) diff --git a/typed-racket-lib/typed-racket/private/syntax-properties.rkt b/typed-racket-lib/typed-racket/private/syntax-properties.rkt index f9b4500e..a6fbc91f 100644 --- a/typed-racket-lib/typed-racket/private/syntax-properties.rkt +++ b/typed-racket-lib/typed-racket/private/syntax-properties.rkt @@ -50,9 +50,10 @@ (ignore typechecker:ignore #:mark) (ignore-some typechecker:ignore-some #:mark) (ignore-some-expr typechecker:ignore-some) - (contract-def typechecker:contract-def) + (contract-def typechecker:contract-def) ; -> Contract-Def (struct in type-contract.rkt) (contract-def/provide typechecker:contract-def/provide) (external-check typechecker:external-check) + (casted-expr typechecker:casted-expr) ; Type -> Void, takes the original type of the casted expr (with-type typechecker:with-type #:mark) (type-ascription type-ascription) (type-inst type-inst) diff --git a/typed-racket-lib/typed-racket/private/type-contract.rkt b/typed-racket-lib/typed-racket/private/type-contract.rkt index e0d00490..2d175dc6 100644 --- a/typed-racket-lib/typed-racket/private/type-contract.rkt +++ b/typed-racket-lib/typed-racket/private/type-contract.rkt @@ -39,14 +39,26 @@ ;; submod for testing (module* test-exports #f (provide type->contract)) +;; has-contrat-def-property? : Syntax -> Boolean +(define (has-contract-def-property? stx) + (syntax-parse stx + #:literal-sets (kernel-literals) + [(define-values (_) e) + (and (contract-def-property #'e) + #t)] + [_ #f])) + (struct contract-def (type flat? maker? typed-side) #:prefab) +;; get-contract-def-property : Syntax -> (U False Contract-Def) ;; Checks if the given syntax needs to be fixed up for contract generation ;; and if yes it returns the information stored in the property (define (get-contract-def-property stx) (syntax-parse stx #:literal-sets (kernel-literals) - [(define-values (_) e) (contract-def-property #'e)] + [(define-values (_) e) + (and (contract-def-property #'e) + ((contract-def-property #'e)))] [_ #f])) ;; type->contract-fail : Syntax Type #:ctc-str String @@ -185,7 +197,7 @@ (define sc-cache (make-hash)) (with-new-name-tables (for/list ((e (in-list forms))) - (if (not (get-contract-def-property e)) + (if (not (has-contract-def-property? e)) e (begin (set-box! include-extra-requires? #t) (generate-contract-def e ctc-cache sc-cache)))))) diff --git a/typed-racket-lib/typed-racket/private/with-types.rkt b/typed-racket-lib/typed-racket/private/with-types.rkt index 21b904f0..b3613d7e 100644 --- a/typed-racket-lib/typed-racket/private/with-types.rkt +++ b/typed-racket-lib/typed-racket/private/with-types.rkt @@ -154,10 +154,11 @@ (define (type-stxs->ids+defs type-stxs typed-side) (for/lists (_1 _2) ([t (in-list type-stxs)]) (define ctc-id (generate-temporary)) + (define contract-def `#s(contract-def ,t #f #f ,typed-side)) (values ctc-id #`(define-values (#,ctc-id) #,(contract-def-property - #'#f `#s(contract-def ,t #f #f ,typed-side)))))) + #'#f (λ () contract-def)))))) (define (wt-core stx) (define-syntax-class typed-id diff --git a/typed-racket-lib/typed-racket/typecheck/tc-expression.rkt b/typed-racket-lib/typed-racket/typecheck/tc-expression.rkt index fe3d93ff..e2e847e6 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-expression.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-expression.rkt @@ -34,6 +34,14 @@ (if expected (tc-expr/check #'e expected) (tc-expr #'e))] + [(exp:casted-expr^ e) + (define result (tc-expr #'e)) + (match result + [(tc-result1: ty) + ((attribute exp.value) ty) + result] + [_ + (tc-error/expr "Cannot cast expression that produces multiple values")])] [(_ e) (if expected (tc-expr/check #'e expected) diff --git a/typed-racket-test/succeed/cast-mod.rkt b/typed-racket-test/succeed/cast-mod.rkt index 2b3c4758..3c9762a2 100644 --- a/typed-racket-test/succeed/cast-mod.rkt +++ b/typed-racket-test/succeed/cast-mod.rkt @@ -1,9 +1,74 @@ #lang typed/racket/base -(cast 2 Number) -(cast 2 Integer) -(cast (list 2 4) (Listof Byte)) -(cast (vector 2 4) (Vectorof Byte)) +(require typed/rackunit) +(check-equal? (cast 2 Number) 2) +(check-equal? (cast 2 Integer) 2) +(check-equal? (cast (list 2 4) (Listof Byte)) (list 2 4)) +(check-pred vector? (cast (vector 2 4) (Vectorof Byte))) + +(check-equal? ((cast (lambda (x) 7) (String -> Number)) "seven") 7) + +(: pos-fx-sub1 : Positive-Fixnum -> Nonnegative-Fixnum) +(define (pos-fx-sub1 x) + (sub1 x)) + +(check-equal? ((cast pos-fx-sub1 (Number -> Number)) 5) 4) + +(check-exn #rx"expected: Positive-Fixnum\n *given: 0.5" + (λ () ((cast pos-fx-sub1 (Number -> Number)) 0.5) 4)) + +(check-exn #rx"expected: Positive-Fixnum\n *given: \"hello\"" + (λ () ((cast pos-fx-sub1 (String -> String)) "hello"))) + +(check-exn #rx"expected: Positive-Fixnum\n *given: \"hello\"" + (λ () ((cast pos-fx-sub1 (Any -> Any)) "hello"))) + +(test-case "cast on mutator functions" + (: v : Boolean) + (define v #f) + (: f : Boolean -> Boolean) + (define (f x) + (set! v x) + x) + + (check-equal? v #f) + (check-equal? ((cast f (Boolean -> Boolean)) #t) #t) + (check-equal? v #t) + (check-exn #rx"expected: \\(or/c #f #t\\)\n *given: \"hello\"" + (λ () ((cast f (String -> String)) "hello"))) + (check-equal? v #t + "if the previous test hadn't errored, this would be \"hello\" with type Boolean")) + +(test-case "cast on mutable boxes" + (: b1 : (Boxof Integer)) + (define b1 (box 42)) + (define b2 (cast b1 (Boxof String))) + (check-equal? (unbox b1) 42) + (check-exn #rx"expected: Integer\n *given: \"hi\"" + (λ () (set-box! b2 "hi"))) + (check-equal? (unbox b1) 42 + "if the previous test hadn't errored, this would be \"hi\" with type Integer")) + +(test-case "cast on mutable vectors" + (: v1 : (Vectorof Integer)) + (define v1 (vector 42)) + (define v2 (cast v1 (Vectorof String))) + (check-equal? (vector-ref v1 0) 42) + (check-exn #rx"expected: Integer\n *given: \"hi\"" + (λ () (vector-set! v2 0 "hi"))) + (check-equal? (vector-ref v1 0) 42 + "if the previous test hadn't errored, this would be \"hi\" with type Integer")) + +;; Struct definitions need to be at the module level for some reason. +(struct (X) s ([i : X]) #:mutable) +(test-case "cast on mutable structs" + (: s1 : (s Integer)) + (define s1 (s 42)) + (define s2 (cast s1 (s String))) + (check-equal? (s-i s1) 42) + (check-exn #rx"expected: Integer\n *given: \"hi\"" + (λ () (set-s-i! s2 "hi"))) + (check-equal? (s-i s1) 42 + "if the previous test hadn't errored, this would be \"hi\" with type Integer")) -((cast (lambda (x) 7) (String -> Number)) "seven") diff --git a/typed-racket-test/succeed/cast-top-level.rkt b/typed-racket-test/succeed/cast-top-level.rkt index b55f91f7..e849e50e 100644 --- a/typed-racket-test/succeed/cast-top-level.rkt +++ b/typed-racket-test/succeed/cast-top-level.rkt @@ -2,10 +2,80 @@ (require typed/racket/base) +(require typed/rackunit) + (cast 2 Number) (cast 2 Integer) (cast (list 2 4) (Listof Byte)) (cast (vector 2 4) (Vectorof Byte)) +(check-equal? (cast 2 Number) 2) +(check-equal? (cast 2 Integer) 2) +(check-equal? (cast (list 2 4) (Listof Byte)) (list 2 4)) +(check-pred vector? (cast (vector 2 4) (Vectorof Byte))) + +(check-equal? ((cast (lambda (x) 7) (String -> Number)) "seven") 7) + +(: pos-fx-sub1 : Positive-Fixnum -> Nonnegative-Fixnum) +(define (pos-fx-sub1 x) + (sub1 x)) + +(check-equal? ((cast pos-fx-sub1 (Number -> Number)) 5) 4) + +(check-exn #rx"expected: Positive-Fixnum\n *given: 0.5" + (λ () ((cast pos-fx-sub1 (Number -> Number)) 0.5) 4)) + +(check-exn #rx"expected: Positive-Fixnum\n *given: \"hello\"" + (λ () ((cast pos-fx-sub1 (String -> String)) "hello"))) + +(check-exn #rx"expected: Positive-Fixnum\n *given: \"hello\"" + (λ () ((cast pos-fx-sub1 (Any -> Any)) "hello"))) + +(test-case "cast on mutator functions" + (: v : Boolean) + (define v #f) + (: f : Boolean -> Boolean) + (define (f x) + (set! v x) + x) + + (check-equal? v #f) + (check-equal? ((cast f (Boolean -> Boolean)) #t) #t) + (check-equal? v #t) + (check-exn #rx"expected: \\(or/c #f #t\\)\n *given: \"hello\"" + (λ () ((cast f (String -> String)) "hello"))) + (check-equal? v #t + "if the previous test hadn't errored, this would be \"hello\" with type Boolean")) + +(test-case "cast on mutable boxes" + (: b1 : (Boxof Integer)) + (define b1 (box 42)) + (define b2 (cast b1 (Boxof String))) + (check-equal? (unbox b1) 42) + (check-exn #rx"expected: Integer\n *given: \"hi\"" + (λ () (set-box! b2 "hi"))) + (check-equal? (unbox b1) 42 + "if the previous test hadn't errored, this would be \"hi\" with type Integer")) + +(test-case "cast on mutable vectors" + (: v1 : (Vectorof Integer)) + (define v1 (vector 42)) + (define v2 (cast v1 (Vectorof String))) + (check-equal? (vector-ref v1 0) 42) + (check-exn #rx"expected: Integer\n *given: \"hi\"" + (λ () (vector-set! v2 0 "hi"))) + (check-equal? (vector-ref v1 0) 42 + "if the previous test hadn't errored, this would be \"hi\" with type Integer")) + +;; Struct definitions need to be at the top level for some reason. +(struct (X) s ([i : X]) #:mutable) +(test-case "cast on mutable structs" + (: s1 : (s Integer)) + (define s1 (s 42)) + (define s2 (cast s1 (s String))) + (check-equal? (s-i s1) 42) + (check-exn #rx"expected: Integer\n *given: \"hi\"" + (λ () (set-s-i! s2 "hi"))) + (check-equal? (s-i s1) 42 + "if the previous test hadn't errored, this would be \"hi\" with type Integer")) -((cast (lambda (x) 7) (String -> Number)) "seven")