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

port typed-racket contracts to late-neg projections

Browse Source
This commit is contained in:
Robby Findler 2015-12-30 21:22:21 -06:00
parent a3ca5aeefc
commit d58d7487e8
5 changed files with 75 additions and 77 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

37
typed-racket-lib/typed-racket/utils/any-wrap.rkt
View File

@ -17,7 +17,7 @@
;; introduce bounded polymorphism for Flvector/Fxvector.
(flvector? e) (fxvector? e) (extflvector? e)))
(define (val-first-projection b)
(define (late-neg-projection b)
(define (fail neg-party v)
(raise-blame-error
(blame-swap b) #:missing-party neg-party
@ -37,13 +37,13 @@
;; field is immutable
(values
(list* (make-struct-field-accessor ref n)
(lambda (s v) (any-wrap/traverse neg-party v))
(lambda (s v) (any-wrap/traverse v neg-party))
res)
(cdr imms))
;; field is mutable
(values
(list* (make-struct-field-accessor ref n)
(lambda (s v) (any-wrap/traverse neg-party v))
(lambda (s v) (any-wrap/traverse v neg-party))
(make-struct-field-mutator set! n)
(lambda (s v) (fail neg-party s))
res)
@ -55,17 +55,17 @@
(when skipped? (fail neg-party s)); "Opaque struct type!"
(apply chaperone-struct s (extract-functions type)))
(define (any-wrap/traverse neg-party v)
(define (any-wrap/traverse v neg-party)
(match v
[(? base-val?)
v]
[(cons x y) (cons (any-wrap/traverse neg-party x) (any-wrap/traverse neg-party y))]
[(cons x y) (cons (any-wrap/traverse x neg-party) (any-wrap/traverse y neg-party))]
[(? vector? (? immutable?))
;; fixme -- should have an immutable for/vector
(vector->immutable-vector
(for/vector #:length (vector-length v)
([i (in-vector v)]) (any-wrap/traverse neg-party i)))]
[(? box? (? immutable?)) (box-immutable (any-wrap/traverse neg-party (unbox v)))]
([i (in-vector v)]) (any-wrap/traverse i neg-party)))]
[(? box? (? immutable?)) (box-immutable (any-wrap/traverse (unbox v) neg-party))]
;; fixme -- handling keys properly makes it not a chaperone
;; [(? hasheq? (? immutable?))
;; (for/hasheq ([(k v) (in-hash v)]) (values k v))]
@ -75,26 +75,26 @@
[(? (λ (e)
(and (hash? e) (immutable? e)
(not (hash-eqv? e)) (not (hash-eq? e)))))
(for/hash ([(k v) (in-hash v)]) (values (any-wrap/traverse neg-party k)
(any-wrap/traverse neg-party v)))]
(for/hash ([(k v) (in-hash v)]) (values (any-wrap/traverse k neg-party)
(any-wrap/traverse v neg-party)))]
[(? vector?) (chaperone-vector v
(lambda (v i e) (any-wrap/traverse neg-party e))
(lambda (v i e) (any-wrap/traverse e neg-party))
(lambda (v i e) (fail neg-party v)))]
[(? box?) (chaperone-box v
(lambda (v e) (any-wrap/traverse neg-party e))
(lambda (v e) (any-wrap/traverse e neg-party))
(lambda (v e) (fail neg-party v)))]
[(? hash?) (chaperone-hash v
(lambda (h k)
(values k (lambda (h k v) (any-wrap/traverse neg-party v)))) ;; ref
(values k (lambda (h k v) (any-wrap/traverse v neg-party)))) ;; ref
(lambda (h k n)
(if (immutable? v)
(values k n)
(fail neg-party v))) ;; set
(lambda (h v) v) ;; remove
(lambda (h k) (any-wrap/traverse neg-party k)))] ;; key
[(? evt?) (chaperone-evt v (lambda (e) (values e (λ (v) (any-wrap/traverse neg-party v)))))]
(lambda (h k) (any-wrap/traverse k neg-party)))] ;; key
[(? evt?) (chaperone-evt v (lambda (e) (values e (λ (v) (any-wrap/traverse v neg-party)))))]
[(? set?)
(for/set ([i (in-set v)]) (any-wrap/traverse neg-party i))]
(for/set ([i (in-set v)]) (any-wrap/traverse i neg-party))]
;; could do something with generic sets here if they had
;; chaperones, or if i could tell if they were immutable.
[(? struct?) (wrap-struct neg-party v)]
@ -108,17 +108,16 @@
(chaperone-procedure
proc
(λ (promise)
(values (λ (val) (any-wrap/traverse neg-party val))
(values (λ (val) (any-wrap/traverse val neg-party))
promise)))))]
[_ (fail neg-party v)]))
(λ (v) (λ (neg-party) (any-wrap/traverse neg-party v))))
any-wrap/traverse)
(define any-wrap/c
(make-chaperone-contract
#:name 'Any
#:first-order (lambda (x) #t)
#:projection (λ (blame) (λ (val) (((val-first-projection blame) val) #f)))
#:val-first-projection val-first-projection))
#:late-neg-projection late-neg-projection))
;; Contract for "safe" struct predicate procedures.
;; We can trust that these obey the type (-> Any Boolean).

21
typed-racket-lib/typed-racket/utils/evt-contract.rkt
View File

@ -15,13 +15,13 @@
(raise-argument-error 'evt/c "chaperone-contract?" ctc))
(make-tr-evt/c ctc))
;; evt/c-proj : Contract -> (Blame -> Any -> Any)
(define (evt/c-proj ctc)
;; evt/c-proj : Contract -> (Blame -> Any Any -> Any)
(define (evt/c-late-neg-proj ctc)
(define real-evt/c (evt/c (tr-evt/c-ctc ctc)))
(define real-proj (contract-projection real-evt/c))
(define real-late-neg-proj (contract-late-neg-projection real-evt/c))
(λ (blame)
(define real-proj* (real-proj blame))
(λ (v)
(define real-late-neg-proj* (real-late-neg-proj blame))
(λ (v neg-party)
;; Must not allow a value of type (Evtof X) to be used as
;; a value of any type that is invariant in X (i.e., has a
;; writing end). For now, this is just channels.
@ -29,15 +29,16 @@
;; If we support custom evts via struct properties, then
;; we may need to tighten this restrictions.
(if (channel? v)
(real-proj*
(real-late-neg-proj*
(chaperone-channel
v
(λ (ch) (values ch values))
(λ (ch val)
(raise-blame-error
blame ch
"cannot put on a channel used as a typed evt"))))
(real-proj* v)))))
blame ch #:missing-party neg-party
"cannot put on a channel used as a typed evt")))
neg-party)
(real-late-neg-proj* v neg-party)))))
;; evt/c-first-order : Contract -> Any -> Boolean
(define ((evt/c-first-order ctc) v) (evt? v))
@ -55,7 +56,7 @@
(define-struct tr-evt/c (ctc)
#:property prop:chaperone-contract
(build-chaperone-contract-property
#:projection evt/c-proj
#:late-neg-projection evt/c-late-neg-proj
#:first-order evt/c-first-order
#:stronger evt/c-stronger?
#:name evt/c-name))

26
typed-racket-lib/typed-racket/utils/opaque-object.rkt
View File

@ -37,15 +37,15 @@
(provide object/c-opaque)
;; projection for base-object/c-opaque
(define ((object/c-opaque-proj ctc) blame)
(λ (obj)
(define ((object/c-opaque-late-neg-proj ctc) blame)
(λ (obj neg-party)
(match-define (base-object/c-opaque
base-ctc
methods method-ctcs
fields field-ctcs)
ctc)
(when (not (object? obj))
(raise-blame-error blame obj "expected an object got ~a" 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)))
@ -65,7 +65,7 @@
;; 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)))
(((contract-late-neg-projection guard/c) blame) obj neg-party)))
(struct base-object/c-opaque
(obj/c ; keep a copy of the normal object/c for first-order checks
@ -76,7 +76,7 @@
(define obj/c (base-object/c-opaque-obj/c ctc))
(λ (val)
(contract-first-order-passes? obj/c val)))
#:projection object/c-opaque-proj))
#:late-neg-projection object/c-opaque-late-neg-proj))
(begin-for-syntax
(define-syntax-class object/c-clause
@ -107,17 +107,17 @@
;; 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)
(define (((restrict-typed->-late-neg-projection ctc) blame) val neg-party)
(chaperone-procedure val
(make-keyword-procedure
(λ (_ kw-args . rst)
(when (typed-method? val)
(raise-blame-error (blame-swap blame) val
(raise-blame-error (blame-swap blame) val #:missing-party neg-party
"cannot call uncontracted typed method"))
(apply values kw-args rst))
(λ args
(when (typed-method? val)
(raise-blame-error (blame-swap blame) val
(raise-blame-error (blame-swap blame) val #:missing-party neg-party
"cannot call uncontracted typed method"))
(apply values args)))))
@ -125,9 +125,9 @@
#:property prop:chaperone-contract
(build-chaperone-contract-property
#:name (λ (ctc) '<hidden-method>) ; FIXME
#:projection restrict-typed->-projection))
#:late-neg-projection restrict-typed->-late-neg-projection))
(define (restrict-typed-field-proj ctc)
(define (restrict-typed-field-late-neg-proj ctc)
(define name (restrict-typed-field/c-name ctc))
(λ (*blame)
(define blame
@ -137,13 +137,13 @@
(if (blame-swapped? *blame)
*blame
(blame-swap *blame)))
(λ (val)
(λ (val neg-party)
(raise-blame-error
blame val
blame val #:missing-party neg-party
"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))
#:late-neg-projection restrict-typed-field-late-neg-proj))

38
typed-racket-lib/typed-racket/utils/sealing-contract.rkt
View File

@ -51,28 +51,28 @@
sealer/unsealer))]
[else #f])]
[else #f]))
#:projection
#:late-neg-projection
(λ (ctc)
(define unsealed (sealing-contract-unsealed ctc))
(define body (sealing-contract-proc ctc))
(λ (blame)
(define negative? (blame-swapped? blame))
(define (make-seal-function orig-fun)
(define (make-seal-function orig-fun neg-party)
(define sealing-key (gensym))
(define sealer/unsealer
(seal/unseal sealing-key negative? unsealed))
(define body-proj
(contract-projection (body sealer/unsealer)))
((body-proj blame) orig-fun))
(λ (val)
(contract-late-neg-projection (body sealer/unsealer)))
((body-proj blame) orig-fun neg-party))
(λ (val neg-party)
(unless (procedure? val)
(raise-blame-error
blame val
blame #:missing-party neg-party val
'(expected "a procedure" given: "~e") val))
;; ok to return an unrelated function since this
;; is an impersonator contract
(make-keyword-procedure (λ (kws kw-args . rst)
(keyword-apply (make-seal-function val)
(keyword-apply (make-seal-function val neg-party)
kws kw-args rst))))))))
;; represents a contract for each polymorphic seal/unseal corresponding
@ -89,39 +89,39 @@
,(seal/unseal-unsealed ctc))
'(unseal/c ,(seal/unseal-key ctc))))
#:stronger (λ (this that) (eq? this that))
#:projection
#:late-neg-projection
(λ (ctc)
(define sealing-key (seal/unseal-key ctc))
(define unsealed (seal/unseal-unsealed ctc))
(λ (blame)
(λ (val)
(λ (val neg-party)
(unless (class? val)
(raise-blame-error
blame val
blame #:missing-party neg-party val
'(expected: "a class" given: "~e") val))
(match-define (list init field method) unsealed)
(if (equal? (blame-original? blame)
(seal/unseal-positive? ctc))
(class-seal val sealing-key init field method
(inst-err val blame)
(subclass-err val blame))
(inst-err val blame neg-party)
(subclass-err val blame neg-party))
(class-unseal val sealing-key
(unseal-err val blame))))))))
(unseal-err val blame neg-party))))))))
;; error functions for use with class-seal, class-unseal
(define ((inst-err val blame) cls)
(define ((inst-err val blame neg-party) cls)
(raise-blame-error
blame val
blame #:missing-party neg-party val
"cannot instantiated a row polymorphic class"))
(define ((subclass-err val blame) cls names)
(define ((subclass-err val blame neg-party) cls names)
(raise-blame-error
blame val
blame #:missing-party neg-party val
"cannot subclass a row polymorphic class with disallowed members ~a"
names))
(define ((unseal-err val blame) cls)
(define ((unseal-err val blame neg-party) cls)
(raise-blame-error
blame val
blame #:missing-party neg-party val
'(expected "matching row polymorphic class"
given: "an unrelated class")))

30
typed-racket-lib/typed-racket/utils/struct-type-c.rkt
View File

@ -12,29 +12,27 @@
;; procedures created by reflective access to the structure obey
;; appropriate invariants.
(define (val-first-projection b)
(define (late-neg-projection b)
(define (fail neg-party v)
(raise-blame-error
(raise-blame-error
(blame-swap b) #:missing-party neg-party
v
"Attempted to use a struct type reflectively in untyped code: ~v" v))
(λ (v)
(λ (neg-party)
(chaperone-struct-type
v
;; the below interposition functions could be improved to fail later,
;; when the functions they produce are actually used.
(λ (v neg-party)
(chaperone-struct-type
v
;; the below interposition functions could be improved to fail later,
;; when the functions they produce are actually used.
;; interposition for `struct-type-info`
(λ _ (fail neg-party v))
;; interposition for `struct-type-make-constructor`
(λ _ (fail neg-party v))
;; guard for interposition on subtypes
(λ _ (fail neg-party v))))))
;; interposition for `struct-type-info`
(λ _ (fail neg-party v))
;; interposition for `struct-type-make-constructor`
(λ _ (fail neg-party v))
;; guard for interposition on subtypes
(λ _ (fail neg-party v)))))
(define (struct-type/c sty) ;; currently ignores sty
(make-chaperone-contract
#:name "struct-type/c"
#:first-order struct-type?
#:projection (λ (blame) (λ (val) (((val-first-projection blame) val) #f)))
#:val-first-projection val-first-projection))
#:late-neg-projection late-neg-projection))