Implement object/c-opaque-stronger

An opaque object contract is stronger than another (opaque) object contract if:
- it has stronger field/method contracts on fields/methods common to both
- and it has no more field/method contracts than the other, if the other is opaque
This commit is contained in:
Ben Greenman 2016-07-08 03:10:11 -04:00
parent 7c495eea62
commit 3e2d020a19
4 changed files with 319 additions and 7 deletions

View File

@ -27,6 +27,9 @@
;; 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
@ -57,21 +60,55 @@
(dynamic-object/c (append methods remaining-methods)
(append method-ctcs
(for/list ([m remaining-methods])
(restrict-typed->/c)))
(restrict-typed->/c m)))
(append fields remaining-fields)
(append field-ctcs
(for/list ([m remaining-fields])
(restrict-typed-field/c obj m)))))
(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 guard/c) blame) obj 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]))
(struct base-object/c-opaque
(obj/c ; keep a copy of the normal object/c for first-order checks
(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
#:name object/c-opaque-name
#:first-order (λ (ctc)
(define obj/c (base-object/c-opaque-obj/c ctc))
(λ (val)
@ -126,10 +163,16 @@
"cannot call uncontracted typed method"))
(apply values args))))))
(struct restrict-typed->/c ()
;; Returns original method name
(define (restrict-typed->-name ctc)
(define name (restrict-typed->/c-name ctc))
(build-compound-type-name 'restrict-typed->/c name))
(struct restrict-typed->/c (name)
#:property prop:chaperone-contract
(build-chaperone-contract-property
#:name (λ (ctc) '<hidden-method>) ; FIXME
#:name restrict-typed->-name
#:stronger equal?
#:late-neg-projection restrict-typed->-late-neg-projection))
(define (restrict-typed-field-late-neg-proj ctc)
@ -147,8 +190,13 @@
blame val #:missing-party neg-party
"cannot read or write field hidden by Typed Racket"))))
(struct restrict-typed-field/c (obj name)
(define (restrict-typed-field-name ctc)
(define name (restrict-typed-field/c-name ctc))
(build-compound-type-name 'restrict-typed-field/c name))
(struct restrict-typed-field/c (name)
#:property prop:flat-contract
(build-flat-contract-property
#:name (λ (ctc) '<hidden-field>) ; FIXME
#:name restrict-typed-field-name
#:stronger equal?
#:late-neg-projection restrict-typed-field-late-neg-proj))

View File

@ -0,0 +1,52 @@
#lang racket
(require typed-racket/utils/opaque-object rackunit
(for-syntax (only-in syntax/srcloc build-source-location-list)))
;; --------------------------------------------------------------------------------------------------
;; object/c-opaque names should be lists:
;; - with 'object/c-opaque as the first element
;; - and 1 element for each member of the contract (field spec, method, ...)
(define-syntax (test-object/c-opaque-name-shape stx)
(syntax-case stx ()
[(_ . ctc-spec*)
#`(begin
#,@(for/list ([ctc-spec (in-list (syntax-e #'ctc-spec*))])
#`(let ([nm (contract-name (object/c-opaque #,@ctc-spec))])
(with-check-info* (list (make-check-location '#,(build-source-location-list ctc-spec)))
(lambda ()
(check-equal? (car nm) 'object/c-opaque)
(check-equal? (length nm) (+ 1 #,(length (syntax-e ctc-spec)))))))))]))
(test-object/c-opaque-name-shape
[]
[(field [i integer?] [j string?])]
[(field [k (<=/c 0)])
(m (->m (-> integer? integer?) zero?))]
[(m1 (->m (-> integer? integer?) zero?))
(m2 (->m boolean?))
(m3 (->m natural-number/c any/c))]
[(field [a real?] [b (-> string?)])
(m1 (->m (-> integer? integer?) zero?))
(m2 (->m boolean?))
(m3 (->m natural-number/c any/c))]
)
;; --------------------------------------------------------------------------------------------------
(define-syntax (test-object/c-vs-opaque-name stx)
(syntax-case stx ()
[(_ . ctc-spec*)
#`(begin
#,@(for/list ([ctc-spec (in-list (syntax-e #'ctc-spec*))])
#`(check-not-equal?
(contract-name (object/c #,@ctc-spec))
(contract-name (object/c-opaque #,@ctc-spec)))))]))
(test-object/c-vs-opaque-name
[]
[(field [i integer?])
(f (->m string? boolean?))]
[(hd (->m any/c))
(tl (->m object?))]
)

View File

@ -0,0 +1,186 @@
#lang racket
(require typed-racket/utils/opaque-object)
;; --------------------------------------------------------------------------------------------------
;; test helpers
(define (test-stronger? ctc-stronger ctc-weaker)
(unless (contract-stronger? ctc-stronger ctc-weaker)
(error 'pr267
"contract ~a is unexpectedly weaker than ~a"
(contract-name ctc-stronger)
(contract-name ctc-weaker))))
(define (test-not-stronger? ctc-stronger ctc-weaker)
(when (contract-stronger? ctc-stronger ctc-weaker)
(error 'pr267
"contract ~a is unexpectedly stronger than ~a"
(contract-name ctc-stronger)
(contract-name ctc-weaker))))
;; --------------------------------------------------------------------------------------------------
;; stronger? tests
(let () ;; object/c-opaque with the same members
(test-stronger?
(object/c-opaque)
(object/c-opaque))
(test-stronger?
(object/c-opaque
(field (f1 integer?))
(m1 (->m object? object?)))
(object/c-opaque
(field (f1 integer?))
(m1 (->m object? object?))))
(test-stronger?
(object/c-opaque
(m1 (->m any/c object? (-> integer? integer?))))
(object/c-opaque
(m1 (->m any/c object? (-> integer? integer?)))))
)
(let () ;; object/c-opaque with fewer members (unspecified = opaque)
(test-stronger?
(object/c-opaque)
(object/c-opaque
(field (x symbol?))))
(test-stronger?
(object/c-opaque
(field (x symbol?)))
(object/c-opaque
(field (x symbol?))
(y (->m none/c none/c))))
(test-stronger?
(object/c-opaque
(f (->m void? any/c)))
(object/c-opaque
(f (->m void? any/c))
(g (->m integer? integer? integer?))))
(test-stronger?
(object/c-opaque
(field (a integer?))
(c (-> real? real?)))
(object/c-opaque
(field (a integer?)
(b integer?))
(c (-> real? real?))
(d (-> real? real?))))
)
(let () ;; object/c-opaque with stronger members
(test-stronger?
(object/c-opaque
(m1 (->m any/c integer?)))
(object/c-opaque
(m1 (->m any/c any/c))))
(test-stronger?
(object/c-opaque
(m1 (->m any/c any/c)))
(object/c-opaque
(m1 (->m integer? any/c))))
(test-stronger?
(object/c-opaque
(m1 (->m any/c integer?))
(m2 (->m any/c (listof boolean?))))
(object/c-opaque
(m1 (->m any/c integer?))
(m2 (->m any/c (listof any/c)))))
(test-stronger?
(object/c-opaque
(a (->m symbol?))
(b (->m (between/c 2 3)))
(c (->m any/c (listof (char-in #\A #\B)))))
(object/c-opaque
(a (->m symbol?))
(b (->m (between/c 0 5)))
(c (->m any/c (listof (char-in #\A #\Z))))))
)
(let () ;; vs. object/c
(test-stronger?
(object/c-opaque)
(object/c
(field (a boolean?))
(b (->m string? any/c))))
(test-stronger?
(object/c-opaque
(field (x any/c))
(h (->m (-> boolean? boolean? boolean?) integer?)))
(object/c))
(test-stronger?
(object/c-opaque
(field (x integer?))
(m1 (->m any/c any/c any/c)))
(object/c
(field (x integer?))
(m1 (->m any/c any/c any/c))))
(test-stronger?
(object/c-opaque
(m1 (->m any/c (</c 2))))
(object/c
(field (a real?) (b boolean?))
(m1 (->m any/c (</c 10)))))
)
;; --------------------------------------------------------------------------------------------------
;; not-stronger? tests
(let () ;; fields must be the same for stronger?
(test-not-stronger?
(object/c-opaque
(field (number (</c 999))))
(object/c-opaque
(field (number (</c 1)))))
(test-not-stronger?
(object/c-opaque
(field (number (</c 1))))
(object/c-opaque
(field (number (</c 999)))))
(test-not-stronger?
(object/c-opaque
(field (a symbol?)
(b integer?)
(c (-> any/c (listof zero?)))))
(object/c-opaque
(field (a symbol?)
(b real?)
(c (-> any/c (listof exact-nonnegative-integer?))))))
)
(let () ;; an object/c is never stronger than an object/c-opaque
(test-not-stronger?
(object/c-opaque
(f (->m integer? integer?)))
(object/c
(f (->m any/c none/c))))
(test-not-stronger?
(object/c
(f (->m any/c none/c)))
(object/c-opaque
(f (->m integer? integer?))))
(test-not-stronger?
(object/c
(field (x integer?))
(m1 (->m any/c any/c any/c)))
(object/c-opaque
(field (x real?))
(m1 (->m any/c any/c any/c))))
)

View File

@ -0,0 +1,26 @@
#lang racket
;; Regression test for PR 267
;; https://github.com/racket/typed-racket/pull/267
;; Issue reported separately as:
;; https://github.com/racket/racket/issues/1198
;; becuase it was really a racket/contract issue
;; (impersonate-vector contracts were using chaperone-contract)
(define con
(object/c (field [a* any/c])
(regenerate (->m (object/c (field [a* (vectorof (object/c))]))))))
(define population%
(class object%
(super-new)
(init-field a*)
(define/public (regenerate)
(vector-ref (get-field a* this) 0)
this)))
(define pop
(contract con (new population% [a* (vector (new (class object% (super-new))))]) 'p 'n))
(void (send (send pop regenerate) regenerate))