suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Improve typecheck for private field initializers

Browse Source 
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 ...)`.
This commit is contained in:
Marc Burns 2015-05-09 13:33:08 -04:00 committed by Asumu Takikawa
parent 5751a2e1cf
commit 609d6189e9
2 changed files with 95 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

66
typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt
View File

@ -556,10 +556,21 @@
#:when (set-member? (hash-ref parse-info 'private-fields) name))
(hash-set! private-field-types name (list type)))
;; Hash<Syntax -> Listof<Listof<Syntax>, Listof<Type>>>
;; 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<Syntax> Dict<Symbol, Type> -> Void
;; check-field-set!s : Syntax Listof<Syntax> Dict<Symbol, Type>
;; Dict<Syntax, List<Listof<Syntax>, Listof<Type>> -> 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<Syntax> Dict Hash -> Listof<Syntax>
;; synthesize-private-field-types : Listof<Syntax> Dict Hash Hash -> Listof<Syntax>
;; 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<Symbol, Id> Dict<Symbol, Id>
;; Dict<Symbol, (List Symbol Symbol)> Dict<Symbol, Id>

47
typed-racket-test/unit-tests/class-tests.rkt
View File

@ -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"]))