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

Add a custom object contract for use in TR

Browse Source 
This corresponds to the more strict object contracts
from the OOPSLA paper. Also use `object/c-opaque` in
TR contract generation
This commit is contained in:
Asumu Takikawa 2013-10-25 12:52:33 -04:00
parent e2fd3b6653
commit 8d0c352dcc
11 changed files with 327 additions and 43 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
typed-racket-lib/typed-racket/base-env/class-prims.rkt
View File

@ -7,6 +7,7 @@
"colon.rkt"
"../typecheck/internal-forms.rkt"
"../private/class-literals.rkt"
"../utils/typed-method-property.rkt"
(only-in "prims.rkt" [define tr:define])
(for-syntax
racket/base
@ -169,7 +170,11 @@
(set-tr-class-info-maybe-private!
info
(cons #'id (tr-class-info-maybe-private info)))
(tr:class:def-property #'class-exp #'id)]
(define new-def
(syntax/loc #'class-exp
(define-values (id)
(chaperone-procedure body #f prop:typed-method #t))))
(tr:class:def-property new-def #'id)]
;; private field definition
[(define-values (id ...) . rst)
(set-tr-class-info-private-fields!

4
typed-racket-lib/typed-racket/private/type-contract.rkt
View File

@ -145,6 +145,7 @@
typed-racket/utils/utils
(for-syntax typed-racket/utils/utils)
typed-racket/utils/any-wrap typed-racket/utils/struct-type-c
typed-racket/utils/opaque-object
typed-racket/utils/evt-contract
unstable/contract racket/contract/parametric))
@ -448,7 +449,8 @@
[(Instance: (Class: _ _ fields methods _ _))
(match-define (list (list field-names field-types) ...) fields)
(match-define (list (list public-names public-types) ...) methods)
(object/sc (append (map (λ (n sc) (member-spec 'method n sc))
(object/sc (from-typed? typed-side)
(append (map (λ (n sc) (member-spec 'method n sc))
public-names (map t->sc/meth public-types))
(map (λ (n sc) (member-spec 'field n sc))
field-names (map t->sc/both field-types))))]

22
typed-racket-lib/typed-racket/static-contracts/combinators/object.rkt
View File

@ -7,13 +7,15 @@
racket/list racket/match
racket/contract
racket/syntax
(for-template racket/base racket/class)
typed-racket/utils/opaque-object
(for-template racket/base racket/class
typed-racket/utils/opaque-object)
(for-syntax racket/base syntax/parse))
(provide
(contract-out
[struct member-spec ([modifier symbol?] [id symbol?] [sc static-contract?])]
[object/sc ((listof object-member-spec?) . -> . static-contract?)]
[object/sc (boolean? (listof object-member-spec?) . -> . static-contract?)]
[class/sc (boolean? (listof member-spec?) . -> . static-contract?)]
[instanceof/sc (static-contract? . -> . static-contract?)]))
@ -24,12 +26,13 @@
(define field-modifiers '(field init init-field inherit-field))
(define method-modifiers '(method inherit super inner override augment augride))
(struct object-combinator combinator ()
(struct object-combinator combinator (opaque?)
#:transparent
#:property prop:combinator-name "object/sc"
#:methods gen:sc
[(define (sc-map v f)
(object-combinator (member-seq-sc-map f (combinator-args v))))
(object-combinator (member-seq-sc-map f (combinator-args v))
(object-combinator-opaque? v)))
(define (sc-traverse v f)
(member-seq-sc-map f (combinator-args v))
(void))
@ -98,8 +101,8 @@
;; TODO make this the correct subset
(define object-member-spec? member-spec?)
(define (object/sc specs)
(object-combinator (member-seq specs)))
(define (object/sc opaque? specs)
(object-combinator (member-seq specs) opaque?))
(define (class/sc opaque? specs)
(class-combinator (member-seq specs) opaque?))
(define (instanceof/sc class)
@ -127,8 +130,11 @@
(define (object/sc->contract v f)
(match v
[(object-combinator (member-seq vals))
#`(object/c #,@(map (member-spec->form f) vals))]))
[(object-combinator (member-seq vals) opaque?)
#`(#,(if opaque?
#'object/c-opaque
#'object/c)
#,@(map (member-spec->form f) vals))]))
(define (class/sc->contract v f)
(match v
[(class-combinator (member-seq vals) opaque)

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

@ -20,7 +20,8 @@
(for-syntax racket/base)
(for-template racket/base
(private class-literals)
(typecheck internal-forms)))
(typecheck internal-forms)
(utils typed-method-property)))
(import tc-expr^)
(export check-class^)
@ -231,6 +232,17 @@
[else #'props-core])
#:with form #'(let-values ([(meth-name) plam-core])
meth-name-2))
;; Typed Racket can't directly typecheck uses of `chaperone-procedure` which
;; are allowed in method definitions (to accommodate TR object contracts).
;; For special cases generated by TR's class macro, strip off the chaperone
;; part and typecheck the rest. Let other cases pass through.
(pattern (#%plain-app (~literal chaperone-procedure)
meth (quote #f) (~literal prop:typed-method) (quote #t))
#:declare meth (core-method register/method register/self)
#:with form #'meth.form)
(pattern (#%plain-app (~literal chaperone-procedure) meth . other-args)
#:declare meth (core-method register/method register/self)
#:with form #'(#%plain-app chaperone-procedure meth.form . other-args))
(pattern ((~and head (~or let-values letrec-values))
([(meth-name:id) meth] ...)
meth-name-2:id)
@ -544,9 +556,10 @@
#:when (set-member? (hash-ref parse-info 'private-fields) name))
(hash-set! private-field-types name (list type)))
(synthesize-private-field-types private-field-stxs
local-private-field-table
private-field-types)
(define synthesized-init-val-stxs
(synthesize-private-field-types private-field-stxs
local-private-field-table
private-field-types))
;; Detect mutation of private fields for occurrence typing
(for ([stx (in-sequences
@ -590,6 +603,7 @@
(do-timestamp "checked other top-level exprs")
(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))
(do-timestamp "checked field initializers")
(define checked-method-types
@ -1014,11 +1028,11 @@
(process-method-syntax stx self-type #f))
(tc-expr/t xformed-stx)])))
;; check-field-set!s : Syntax Dict<Symbol, Type> -> Void
;; check-field-set!s : Syntax Listof<Syntax> Dict<Symbol, 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 inits)
(define (check-field-set!s stx synthed-stxs inits)
(for ([form (syntax->list stx)])
(syntax-parse form
#:literal-sets (kernel-literals)
@ -1075,8 +1089,14 @@
;; field this setter corresponds to (except via the local
;; binding name in the `let-values` which doesn't seem
;; very reliable).
(define type (setter->type #'local-setter))
(tc-expr/check #'init-val (ret type))]
;;
;; Also don't check if this is a private field that's already
;; been synthesized.
(unless (member #'init-val synthed-stxs)
(define type (setter->type #'local-setter))
(define processed
(process-private-field-init-val #'init-val))
(tc-expr/check processed (ret type)))]
[_ (void)])))
;; setter->type : Id -> Type
@ -1109,11 +1129,13 @@
[else
(tc-expr/check init-val (ret init-type))])))
;; synthesize-private-field-types : Listof<Syntax> Dict Hash -> Void
;; synthesize-private-field-types : Listof<Syntax> Dict Hash -> Listof<Syntax>
;; Given top-level expressions in the class, synthesize types from
;; the initialization expressions for private fields.
;; the initialization expressions for private fields. Returns the initial
;; value expressions that were type synthesized.
(define (synthesize-private-field-types stxs locals types)
(for ([stx (in-list stxs)])
(for/fold ([synthed-stxs null])
([stx (in-list stxs)])
(syntax-parse stx
#:literal-sets (kernel-literals)
[(begin
@ -1126,13 +1148,17 @@
(define name (if (stx-pair? name-stx)
(syntax-e (stx-car name-stx))
(syntax-e name-stx)))
(define processed-init
(process-private-field-init-val #'initial-value))
;; don't synthesize if there's already a type annotation
(unless (hash-has-key? types name)
;; FIXME: this always generalizes the private field
;; type, but it's better to only generalize if
;; the field is actually mutated.
(hash-set! types name
(list (generalize (tc-expr/t #'initial-value)))))]
(cond [(hash-has-key? types name) synthed-stxs]
[else
;; FIXME: this always generalizes the private field
;; type, but it's better to only generalize if
;; the field is actually mutated.
(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 ...)])
(begin
@ -1144,11 +1170,14 @@
...
(#%plain-app _))
(define names (map syntax-e (syntax-e (tr:class:def-property stx))))
(for ([name (in-list names)]
[initial-value-stx (in-list (syntax->list #'(initial-value ...)))])
(unless (hash-has-key? types name)
(hash-set! types name
(list (generalize (tc-expr/t initial-value-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)]))])))
;; Syntax -> Dict<Symbol, Id> Dict<Symbol, Id>
;; Dict<Symbol, (List Symbol Symbol)> Dict<Symbol, Id>
@ -1570,6 +1599,23 @@
[_ (int-err "process-method-syntax: unexpected syntax ~a"
(syntax->datum stx))]))
;; process-private-field-init-val : Syntax -> Syntax
;; Pre-process field syntax before typechecking
(define (process-private-field-init-val stx)
(syntax-parse stx
#:literal-sets (kernel-literals)
;; Remove TR-specific expressions that aren't typecheckable yet.
;; FIXME: can remove this hack when TR has both bounded polymorphism
;; and support for non-uniform rest-args. Also can remove
;; the analogous cases in the core-method syntax class.
[(#%plain-app (~literal chaperone-procedure)
form
(quote #f)
(~literal prop:typed-method)
(quote #t))
#'form]
[_ stx]))
;; Set<Symbol> Set<Symbol> String -> Void
;; check that all the required names are actually present
;;

141
typed-racket-lib/typed-racket/utils/opaque-object.rkt Normal file
View File

@ -0,0 +1,141 @@
#lang racket/base
;; This module provides object contracts that prevent access
;; to typed methods and fields that are left out of an object type
;; via subtyping.
;;
;; These correspond to `object/c` and `OG` guards from
;; "Gradual Typing for First-Class Classes"
;;
;; Methods:
;; --------
;; The contract allows untyped contexts to call untyped methods on
;; protected objects freely. Typed methods without explicit contracts
;; are in the opaque part and cannot be called from any context after
;; the contract is applied.
;;
;; Allowing untyped-untyped calls (without any contract) is a liberalization
;; of the contract semantics, but it should not cause problems because
;; typed code always protects its own invariants via contracted imports or
;; exports (and typed methods are not callable without contracts).
;;
;; Fields:
;; -------
;; Fields are blocked from access without a contract in all cases. Allowing
;; untyped-untyped access may be ok, but could produce unhelpful blame.
;; Allowing typed-typed access is not ok unless it's restricted to identical
;; blame parties (e.g., a particular module).
(require racket/class
racket/match
racket/contract/base
racket/contract/combinator
"typed-method-property.rkt"
(for-syntax racket/base
syntax/parse))
(provide object/c-opaque)
;; projection for base-object/c-opaque
(define ((object/c-opaque-proj ctc) blame)
(λ (obj)
(match-define (base-object/c-opaque
methods method-ctcs
fields field-ctcs)
ctc)
(when (not (object? obj))
(raise-blame-error blame obj "expected an object got ~a" obj))
(define actual-fields (field-names obj))
(define actual-methods
(interface->method-names (object-interface obj)))
(define remaining-fields
(remove* fields actual-fields))
(define remaining-methods
(remove* methods actual-methods))
(define guard/c
(dynamic-object/c (append methods remaining-methods)
(append method-ctcs
(for/list ([m remaining-methods])
(restrict-typed->/c)))
(append fields remaining-fields)
(append field-ctcs
(for/list ([m remaining-fields])
(restrict-typed-field/c obj m)))))
;; FIXME: this is a bit sketchy because we have to construct
;; a contract that depends on the actual object that we got
;; since we don't know its methods beforehand
(((contract-projection guard/c) blame) obj)))
(struct base-object/c-opaque
(method-names method-ctcs field-names field-ctcs)
#:property prop:contract
(build-contract-property
#:projection object/c-opaque-proj))
(begin-for-syntax
(define-syntax-class object/c-clause
#:attributes (method-names method-ctcs field-names field-ctcs)
(pattern (field [name:id ctc:expr] ...)
#:with field-names #'(list (quote name) ...)
#:with field-ctcs #'(list ctc ...)
#:with method-names #'null
#:with method-ctcs #'null)
(pattern [name:id ctc:expr]
#:with field-names #'null
#:with field-ctcs #'null
#:with method-names #'(list (quote name))
#:with method-ctcs #'(list ctc))))
(define-syntax (object/c-opaque stx)
(syntax-parse stx
[(_ ?clause:object/c-clause ...)
(syntax/loc stx
(base-object/c-opaque
(append ?clause.method-names ...)
(append ?clause.method-ctcs ...)
(append ?clause.field-names ...)
(append ?clause.field-ctcs ...)))]))
;; This contract combinator prevents the method call if the target
;; method is typed (assuming that the caller is untyped or the receiving
;; object went through untyped code)
(define (((restrict-typed->-projection ctc) blame) val)
(chaperone-procedure val
(make-keyword-procedure
(λ (_ kw-args . rst)
(when (typed-method? val)
(raise-blame-error (blame-swap blame) val
"cannot call uncontracted typed method"))
(apply values kw-args rst))
(λ args
(when (typed-method? val)
(raise-blame-error (blame-swap blame) val
"cannot call uncontracted typed method"))
(apply values args)))))
(struct restrict-typed->/c ()
#:property prop:chaperone-contract
(build-chaperone-contract-property
#:name (λ (ctc) '<hidden-method>) ; FIXME
#:projection restrict-typed->-projection))
(define (restrict-typed-field-proj ctc)
(define name (restrict-typed-field/c-name ctc))
(λ (*blame)
(define blame
;; Blame has been swapped if this is for a set-field!, in which case
;; the blame matches the original negative party. Otherwise we want
;; to swap to blame negative.
(if (blame-swapped? *blame)
*blame
(blame-swap *blame)))
(λ (val)
(raise-blame-error
blame val
"cannot read or write field hidden by Typed Racket"))))
(struct restrict-typed-field/c (obj name)
#:property prop:flat-contract
(build-flat-contract-property
#:name (λ (ctc) '<hidden-field>) ; FIXME
#:projection restrict-typed-field-proj))

12
typed-racket-lib/typed-racket/utils/typed-method-property.rkt Normal file
View File

@ -0,0 +1,12 @@
#lang racket/base
(provide prop:typed-method
typed-method?)
(define-values (prop:typed-method
typed-method?
;; the payload doesn't matter since this
;; property is only used to detect a boolean
;; property of the method
_)
(make-impersonator-property 'typed-method))

22
typed-racket-test/fail/opaque-object-contract-2.rkt Normal file
View File

@ -0,0 +1,22 @@
#;
(exn-pred #rx"cannot read or write.*blaming:.*b\\)")
#lang racket/base
;; Ensure that opaque object contracts prevent access to fields
;; that should be hidden from untyped code
(require racket/class)
(module a typed/racket
(provide o)
(: o (Object))
(define o (new (class object%
(super-new)
(field [x 0])))))
(module b racket
(require (submod ".." a))
(set-field! x o "wrong type")
(get-field x o))
(require 'b)

25
typed-racket-test/fail/opaque-object-contract.rkt Normal file
View File

@ -0,0 +1,25 @@
#;
(exn-pred #rx"uncontracted typed.*blaming: .*opaque-object-contract.rkt")
#lang racket/base
(require racket/class)
(module a racket
(provide c%)
(define c%
(class object%
(super-new)
(define/public (m) (void)))))
(module b typed/racket
(require/typed (submod ".." a) [c% (Class [m (-> Void)])])
(provide o)
(: o (Object))
(define o (new (class c%
(super-new)
(define/public (n) (void))))))
(require 'b)
(send o m)
(send o n)

25
typed-racket-test/succeed/opaque-object-contract.rkt Normal file
View File

@ -0,0 +1,25 @@
#lang racket/base
;; Ensure that for untyped-untyped calls, the opaque object
;; contract does not interfere.
(require racket/class)
(module a racket
(provide c%)
(define c%
(class object%
(super-new)
(define/public (m) (void)))))
(module b typed/racket
(require/typed (submod ".." a) [c% (Class [m (-> Void)])])
(provide o)
(: o (Object))
(define o (new (class c%
(super-new)
(define/public (n) (void))))))
(require 'b)
(send o m)

11
typed-racket-test/unit-tests/contract-tests.rkt
View File

@ -12,7 +12,7 @@
(submod typed-racket/private/type-contract test-exports)
(only-in racket/contract contract)
racket/match
(except-in racket/class private)
(except-in typed/racket/class private)
rackunit)
(provide tests)
(gen-test-main)
@ -64,6 +64,7 @@
(namespace-require 'unstable/contract)
(namespace-require 'typed-racket/utils/any-wrap)
(namespace-require 'typed-racket/utils/evt-contract)
(namespace-require 'typed-racket/utils/opaque-object)
(namespace-require '(submod typed-racket/private/type-contract predicates))
(namespace-require 'typed/racket/class)
(current-namespace)))
@ -272,19 +273,13 @@
#:untyped
#:msg #rx"cannot put on a channel")
;; typed/untyped interaction with class/object contracts
(t-int/fail (-object #:field ([f -String]))
(λ (o) (get-field g o))
(new (class object% (super-new)
(field [f "f"] [g "g"])))
#:typed
#:msg #rx"does not have the requested field")
(t-int/fail (-object #:method ([m (-> -String)]))
(λ (o) (send o n))
(new (class object% (super-new)
(define/public (m) "m")
(define/public (n) "n")))
#:typed
#:msg #rx"no such method")
#:msg #rx"cannot call uncontracted")
(t-int (-class #:method ([m (-> -String)]))
(λ (s%) (class s% (super-new)
(define/public (n) "ok")))

11
typed-racket-test/unit-tests/static-contract-optimizer-tests.rkt
View File

@ -275,9 +275,14 @@
#:neg (case->/sc (list (arr/sc (list any/sc) any/sc (list list?/sc)))))
(check-optimize
(object/sc (list (member-spec 'field 'x (listof/sc any/sc))))
#:pos (object/sc (list (member-spec 'field 'x list?/sc)))
#:neg (object/sc (list (member-spec 'field 'x list?/sc))))
(object/sc #t (list (member-spec 'field 'x (listof/sc any/sc))))
#:pos (object/sc #t (list (member-spec 'field 'x list?/sc)))
#:neg (object/sc #t (list (member-spec 'field 'x list?/sc))))
(check-optimize
(object/sc #f (list (member-spec 'field 'x (listof/sc any/sc))))
#:pos (object/sc #f (list (member-spec 'field 'x list?/sc)))
#:neg (object/sc #f (list (member-spec 'field 'x list?/sc))))
(check-optimize
(class/sc #t (list (member-spec 'field 'x (listof/sc any/sc))))