Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion typed-racket-lib/info.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@

(define collection 'multi)

(define deps '(("base" #:version "8.18.0.4")
(define deps '(("base" #:version "9.1.0.7")
"source-syntax"
"pconvert-lib"
"compatibility-lib" ;; to assign types
Expand Down
12 changes: 5 additions & 7 deletions typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -283,13 +283,11 @@
(let-values ([(rcvr-var) rcvr])
(let-values (((meth-var) (~and find-app (#%plain-app find-method/who _ _ _))))
(let-values ([(arg-var) args] ...)
(if wrapped-object-check
ignore-this-case
(~and core-app
(~or (#%plain-app _ _ _arg-var2 ...)
(let-values ([(_) _] ...)
(#%plain-app (#%plain-app _ _ _ _ _ _)
_ _ _ ...)))))))))
(~and core-app
(~or (#%plain-app _ _ _arg-var2 ...)
(let-values ([(_) _] ...)
(#%plain-app (#%plain-app _ _ _ _ _ _)
_ _ _ ...))))))))
(register-ignored! form)
(tc/send #'find-app #'core-app
#'rcvr-var #'rcvr
Expand Down
174 changes: 4 additions & 170 deletions typed-racket-lib/typed-racket/utils/opaque-object.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -27,9 +27,6 @@
;; blame parties (e.g., a particular module).

(require racket/class
(only-in racket/private/class-c-old
base-object/c? build-object/c-type-name object/c-width-subtype?
object/c-common-methods-stronger? object/c-common-fields-stronger?)
racket/match
racket/contract/base
racket/contract/combinator
Expand All @@ -39,100 +36,6 @@

(provide object/c-opaque)

(module+ for-testing
(provide restrict-typed->/c
restrict-typed-field/c))

;; projection for base-object/c-opaque
(define ((object/c-opaque-late-neg-proj ctc) blame)
(match-define (base-object/c-opaque
base-ctc
methods method-ctcs
fields field-ctcs)
ctc)
(define guard/c (dynamic-object/c methods method-ctcs fields field-ctcs))
(define guard/c-proj ((contract-late-neg-projection guard/c) blame))
(λ (obj neg-party)
(unless (object? obj)
(raise-blame-error blame #:missing-party neg-party 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))
(cond
[(and (null? remaining-methods) (null? remaining-fields))
(guard/c-proj obj neg-party)]
[else
(define restrict-guard/c
(dynamic-object/c remaining-methods
(for/list ([m (in-list remaining-methods)])
(restrict-typed->/c m))
remaining-fields
(for/list ([m (in-list remaining-fields)])
(restrict-typed-field/c 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-late-neg-projection restrict-guard/c) blame)
(guard/c-proj obj neg-party)
neg-party)])))

(define (object/c-opaque-name ctc)
(build-object/c-type-name 'object/c-opaque
(base-object/c-opaque-method-names ctc)
(base-object/c-opaque-method-ctcs ctc)
(base-object/c-opaque-field-names ctc)
(base-object/c-opaque-field-ctcs ctc)))

;; Similar to object/c-stronger, but without width subtyping.
;; (Intuition: unspecified fields are guarded by the strongest possible contract)
;; An opaque object contract `this` is stronger than `that` when:
;; - `that` is an opaque contract
;; and `this` specifies at most the same members as `that`
;; and `this` has stronger contracts on all members
;; - `that` is an object/c contract
;; and `this` has stronger contracts on their common members
(define (object/c-opaque-stronger? this that)
(define that-opaque? (base-object/c-opaque? that))
(cond
[(or that-opaque?
(base-object/c? that))
(define this-ctc (base-object/c-opaque-obj/c this))
(define that-ctc (if that-opaque? (base-object/c-opaque-obj/c that) that))
(and
(if that-opaque?
;; then members of `this` should be a SUBSET of members of `that`
(object/c-width-subtype? that-ctc this-ctc)
#t)
(object/c-common-fields-stronger? this-ctc that-ctc)
(object/c-common-methods-stronger? this-ctc that-ctc)
#t)]
[else #f]))

;; An `object/c-opaque` contract is equivalent to another `object/c-opaque`
;; contract that has the same fields+methods and the same contracts on them.
(define (object/c-opaque-equivalent? this that)
(and (base-object/c-opaque? that)
(contract-equivalent? (base-object/c-opaque-obj/c this)
(base-object/c-opaque-obj/c that))))

(struct base-object/c-opaque
(obj/c ; keep a copy of the normal object/c for first-order and stronger checks
method-names method-ctcs field-names field-ctcs)
#:property prop:contract
(build-contract-property
#:stronger object/c-opaque-stronger?
#:equivalent object/c-opaque-equivalent?
#:name object/c-opaque-name
#:first-order (λ (ctc)
(define obj/c (base-object/c-opaque-obj/c ctc))
(λ (val)
(contract-first-order-passes? obj/c val)))
#:late-neg-projection object/c-opaque-late-neg-proj))

(begin-for-syntax
(define-syntax-class object/c-clause
#:attributes (method-names method-ctcs field-names field-ctcs)
Expand All @@ -151,76 +54,7 @@
(syntax-parse stx
[(_ ?clause:object/c-clause ...)
(syntax/loc stx
(let ([names (append ?clause.method-names ...)]
[ctcs (append ?clause.method-ctcs ...)]
[fnames (append ?clause.field-names ...)]
[fctcs (append ?clause.field-ctcs ...)])
(base-object/c-opaque
(dynamic-object/c names ctcs fnames fctcs)
names ctcs fnames fctcs)))]))

;; 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->-late-neg-projection ctc) blame) val neg-party)
(cond
[(typed-method? val)
(chaperone-procedure val
(make-keyword-procedure
(λ (_ kw-args . rst)
(raise-blame-error (blame-swap blame) val #:missing-party neg-party
"cannot call uncontracted typed method"))
(λ args
(raise-blame-error (blame-swap blame) val #:missing-party neg-party
"cannot call uncontracted typed method"))))]
[else val]))

;; Returns original method name
(define (restrict-typed->-name ctc)
(define name (restrict-typed->/c-name ctc))
(build-compound-type-name 'restrict-typed->/c name))

(define (restrict-typed->/c-equivalent? this that)
(and (restrict-typed->/c? that)
(eq? (restrict-typed->/c-name this)
(restrict-typed->/c-name that))))

(struct restrict-typed->/c (name)
#:property prop:chaperone-contract
(build-chaperone-contract-property
#:name restrict-typed->-name
#:stronger restrict-typed->/c-equivalent?
#:equivalent restrict-typed->/c-equivalent?
#:late-neg-projection restrict-typed->-late-neg-projection))

(define (restrict-typed-field-late-neg-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 neg-party)
(raise-blame-error
blame val #:missing-party neg-party
"cannot read or write field hidden by Typed Racket"))))

(define (restrict-typed-field-name ctc)
(define name (restrict-typed-field/c-name ctc))
(build-compound-type-name 'restrict-typed-field/c name))

(define (restrict-typed-field-equivalent? this that)
(and (restrict-typed-field/c? that)
(equal? (restrict-typed-field/c-name this)
(restrict-typed-field/c-name that))))

(struct restrict-typed-field/c (name)
#:property prop:flat-contract
(build-flat-contract-property
#:name restrict-typed-field-name
#:stronger restrict-typed-field-equivalent?
#:equivalent restrict-typed-field-equivalent?
#:late-neg-projection restrict-typed-field-late-neg-proj))
(object/c ?clause ...
#:opaque-except typed-method?
#:opaque-fields #t
#:do-not-check-class-field-accessor-or-mutator-access))]))
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does this keyword mean that we're maintaining the unsoundness here? I think we should just fix it.

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes.

Fixing it is fine but shouldn't hold up these changes, in my opinion. This argument isn't there just for TR, as others may be relying on that behavior too.

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just for clarity, dropping this keyword would (we think) break existing programs until we do something smarter elsewhere.

Loading