From 609d6189e93d379062f572fc4371e81f56015c92 Mon Sep 17 00:00:00 2001 From: Marc Burns Date: Sat, 9 May 2015 13:33:08 -0400 Subject: [PATCH] Improve typecheck for private field initializers This patch addresses two issues with `typed/racket/class`: 1. For multiple private fields declared with `define-values`, type information does not propagate from the values produced by the initialization expression to the declared fields. This breaks soundness of private fields: A field can be annotated with a type that does not contain the field's initial value. This was resolved by keeping a table of temporary bindings introduced in the expansion of the initializer along with their types. The field setter's type is then checked against that of the corresponding temporary. 2. The class body typechecker assumes that the `expr` of a `define-values` clause will expand to a bare `(values vs ...)`. This was resolved by generalizing the template for matching an expanded `define-values` initializer and extracting the type information from the `expr` instead of each element in `(vs ...)`. --- .../typecheck/check-class-unit.rkt | 66 ++++++++++++++----- typed-racket-test/unit-tests/class-tests.rkt | 47 ++++++++++++- 2 files changed, 95 insertions(+), 18 deletions(-) diff --git a/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt b/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt index f00fc3cc..66bc1cf6 100644 --- a/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt +++ b/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt @@ -556,10 +556,21 @@ #:when (set-member? (hash-ref parse-info 'private-fields) name)) (hash-set! private-field-types name (list type))) + ;; Hash Listof, Listof>> + ;; Maps the outermost `let-values` expressions introduced by the expansion of + ;; `define-values` within the class body to a list of identifier syntaxes + ;; that represent variables and a list of corresponding types. + ;; The variables temporarily hold the values of the initializer expression; + ;; a field mutator is called on each one in the body of the `let-values`. + ;; Typechecking of these calls is done in `check-field-set!s` and requires + ;; the types of the initial values. + (define inits-temporaries-types (make-hasheq)) + (define synthesized-init-val-stxs (synthesize-private-field-types private-field-stxs local-private-field-table - private-field-types)) + private-field-types + inits-temporaries-types)) ;; Detect mutation of private fields for occurrence typing (for ([stx (in-sequences @@ -604,7 +615,8 @@ (with-lexical-env/extend-types lexical-names/top-level lexical-types/top-level (check-field-set!s (hash-ref parse-info 'initializer-body) synthesized-init-val-stxs - inits)) + inits + inits-temporaries-types)) (do-timestamp "checked field initializers") (define checked-method-types (with-lexical-env/extend-types lexical-names lexical-types @@ -1028,11 +1040,12 @@ (process-method-syntax stx self-type #f)) (tc-expr/t xformed-stx)]))) -;; check-field-set!s : Syntax Listof Dict -> Void +;; check-field-set!s : Syntax Listof Dict +;; Dict, Listof> -> Void ;; Check that fields are initialized to the correct type ;; FIXME: use syntax classes for matching and clearly separate the handling ;; of field initialization and set! uses -(define (check-field-set!s stx synthed-stxs inits) +(define (check-field-set!s stx synthed-stxs inits inits-temporaries-types) (for ([form (syntax->list stx)]) (syntax-parse form #:literal-sets (kernel-literals) @@ -1097,6 +1110,14 @@ (define processed (process-private-field-init-val #'init-val)) (tc-expr/check processed (ret type)))] + ;; multiple private fields + [(let-values ([(names:id ...) val-expr]) begins ... (#%plain-app _)) + (match-define (list t-names t-types) + (hash-ref inits-temporaries-types form (list empty empty))) + ;; Extend lexical type env with temporaries introduced in the + ;; expansion of the field initialization or setter + (with-lexical-env/extend-types t-names t-types + (check-field-set!s #'(begins ...) synthed-stxs inits inits-temporaries-types))] [_ (void)]))) ;; setter->type : Id -> Type @@ -1129,11 +1150,11 @@ [else (tc-expr/check init-val (ret init-type))]))) -;; synthesize-private-field-types : Listof Dict Hash -> Listof +;; synthesize-private-field-types : Listof Dict Hash Hash -> Listof ;; Given top-level expressions in the class, synthesize types from ;; the initialization expressions for private fields. Returns the initial ;; value expressions that were type synthesized. -(define (synthesize-private-field-types stxs locals types) +(define (synthesize-private-field-types stxs locals types inits-temporaries-types) (for/fold ([synthed-stxs null]) ([stx (in-list stxs)]) (syntax-parse stx @@ -1159,8 +1180,7 @@ (hash-set! types name (list (generalize (tc-expr/t processed-init)))) (cons #'initial-value synthed-stxs)])] - [(let-values ([(initial-value-name:id ...) - (#%plain-app _ initial-value ...)]) + [(let-values ([(initial-value-name:id ...) initial-values]) (begin (quote ((~datum declare-field-initialization) _)) (let-values ([(obj:id) self]) @@ -1169,15 +1189,27 @@ _ _ (#%plain-app setter:id obj2:id field2:id))))) ... (#%plain-app _)) - (define names (map syntax-e (syntax-e (tr:class:def-property stx)))) - (for/fold ([synthed-stxs synthed-stxs]) - ([name (in-list names)] - [initial-value-stx (in-list (syntax->list #'(initial-value ...)))]) - (cond [(hash-has-key? types name) synthed-stxs] - [else - (hash-set! types name - (list (generalize (tc-expr/t initial-value-stx)))) - (cons initial-value-stx synthed-stxs)]))]))) + (define field-names (map syntax-e (syntax-e (tr:class:def-property stx)))) + (define temporary-stxs (syntax-e #'(initial-value-name ...))) + (define init-types + (match (tc-expr/check #'initial-values #f) + [(tc-results: xs ) xs])) + (unless (= (length field-names) (length init-types)) + (tc-error/expr "wrong number of values: expected ~a but got ~a" + (length field-names) (length init-types))) + (define temporaries-types + (for/list + ([name (in-list field-names)] + [temp-stx (in-list temporary-stxs)] + [type (in-list init-types)]) + (define type-table-val (generalize type)) + (unless (hash-has-key? types name) + (hash-set! types name (list type-table-val))) + (cons temp-stx type-table-val))) + (hash-set! inits-temporaries-types stx + (list (map car temporaries-types) + (map cdr temporaries-types))) + (cons #'initial-values synthed-stxs)]))) ;; Syntax -> Dict Dict ;; Dict Dict diff --git a/typed-racket-test/unit-tests/class-tests.rkt b/typed-racket-test/unit-tests/class-tests.rkt index 928ff5f6..2aa41b09 100644 --- a/typed-racket-test/unit-tests/class-tests.rkt +++ b/typed-racket-test/unit-tests/class-tests.rkt @@ -2038,4 +2038,49 @@ [bsp-trees-val bsp-trees-val] [else 5])))) (void)) - -Void])) + -Void] + ;; tests private fields declared with define-values + [tc-e (let () + (send + (new + (class object% + (super-new) + (define-values (a b) (values 1 "foo")) + (: get-ab (-> (Values Integer String))) + (define/public (get-ab) (values a b)))) + get-ab) + (void)) + -Void] + [tc-e (let () + (send + (new + (class object% + (super-new) + (define-values (a b) + (let ([x 1] [y "foo"]) (values x y))) + (: get-ab (-> (Values Integer String))) + (define/public (get-ab) (values a b)))) + get-ab) + (void)) + -Void] + ;; Failure tests for soundness of private field initialization + [tc-err (let () + (define c% + (class object% + (super-new) + (: a String) + (define-values (a b) (values 1 2)) + (: get-a (-> String)) + (define/public (get-a) a))) + (error "foo")) + #:msg #rx"expected: String.*given: Integer"] + [tc-err (let () + (define c% + (class object% + (super-new) + (: a String) + (define-values (a b) (let ([z 1]) (values z z))) + (: get-a (-> String)) + (define/public (get-a) a))) + (error "foo")) + #:msg #rx"expected: String.*given: Integer"]))