Add unit contracts from branches/sstrickl/unit-contracts.

svn: r13177
This commit is contained in:
Stevie Strickland 2009-01-16 19:03:11 +00:00
commit cc9925dd6b
5 changed files with 350 additions and 129 deletions

View File

@ -45,8 +45,8 @@
(cons (reverse requires) l)))))))
;; (make-var-info bool bool identifier)
(define-struct var-info (syntax? [exported? #:mutable] id))
;; (make-var-info bool bool identifier (or #f (syntax-object -> syntax-object)))
(define-struct var-info (syntax? [exported? #:mutable] id [add-ctc #:mutable]))
(define-syntax define-struct/proc
(syntax-rules ()
@ -57,8 +57,11 @@
;; - (cons identifier identifier)
;; A def is
;; - (listof (cons (listof int/ext) syntax-object))
;; A ctc is
;; - syntax-object
;; - #f
;; A sig is
;; - (list (listof int/ext) (listof def) (listof def))
;; - (list (listof int/ext) (listof def) (listof def) (listof ctc))
;; A tagged-sig is
;; - (listof (cons #f siginfo) (cons #f identifier) sig)
;; - (listof (cons symbol siginfo) (cons symbol identifier) sig)
@ -95,8 +98,9 @@
;; (listof identifier)
;; (listof (cons (listof identifier) syntax-object))
;; (listof (cons (listof identifier) syntax-object))
;; (listof (U syntax-object #f))
;; identifier)
(define-struct/proc signature (siginfo vars val-defs stx-defs orig-binder)
(define-struct/proc signature (siginfo vars val-defs stx-defs ctcs orig-binder)
(lambda (_ stx)
(parameterize ((error-syntax stx))
(raise-stx-err "illegal use of signature name"))))
@ -219,6 +223,7 @@
(vars (signature-vars sig))
(vals (signature-val-defs sig))
(stxs (signature-stx-defs sig))
(ctcs (signature-ctcs sig))
(delta-introduce (if bind?
(let ([f (syntax-local-make-delta-introducer
spec)])
@ -243,7 +248,8 @@
(cons (map (λ (id) (cons id id))
(car stx))
(cdr stx)))
stxs)))))
stxs)
ctcs))))
(define (sig-names sig)
(append (car sig)
@ -264,12 +270,19 @@
(car def))
(g (cdr def))))
;; map-ctc : (identifier -> identifier) (syntax-object -> syntax-object) ctc -> ctc
(define (map-ctc f g ctc)
(if ctc
(g ctc)
ctc))
;; map-sig : (identifier -> identifier) (sytnax-object -> syntax-object) sig -> sig
;; applies f to the internal parts, and g to the external parts.
(define (map-sig f g sig)
(list (map (lambda (x) (cons (f (car x)) (g (cdr x)))) (car sig))
(map (lambda (x) (map-def f g x)) (cadr sig))
(map (lambda (x) (map-def f g x)) (caddr sig))))
(map (lambda (x) (map-def f g x)) (caddr sig))
(map (lambda (x) (map-ctc f g x)) (cadddr sig))))
;; An import-spec is one of
;; - signature-name

View File

@ -3,7 +3,7 @@
(provide only except prefix rename tag
import export init-depend link
extends)
extends contracted)
(define-syntax-rule (define-syntax-for-error name message)
(define-syntax name
@ -34,3 +34,5 @@
"misuse of compound-unit keyword")
(define-syntax-for-error extends
"misuse of define-signature keyword")
(define-syntax-for-error contracted
"misuse of define-signature keyword")

View File

@ -10,12 +10,14 @@
"private/unit-syntax.ss")
(require mzlib/etc
mzlib/contract
mzlib/stxparam
"private/unit-keywords.ss"
"private/unit-runtime.ss")
(provide define-signature-form struct open
define-signature provide-signature-elements
only except rename import export prefix link tag init-depend extends
only except rename import export prefix link tag init-depend extends contracted
unit?
(rename :unit unit) define-unit
compound-unit define-compound-unit compound-unit/infer define-compound-unit/infer
@ -123,7 +125,8 @@
(define-for-syntax (build-val+macro-defs sig)
(with-syntax ([(((int-ivar . ext-ivar) ...)
((((int-vid . ext-vid) ...) . vbody) ...)
((((int-sid . ext-sid) ...) . sbody) ...))
((((int-sid . ext-sid) ...) . sbody) ...)
(cbody ...))
(map-sig (lambda (x) x)
(make-syntax-introducer)
sig)])
@ -170,7 +173,7 @@
(raise-stx-err "expected syntax matching (sig-expr ...)" sig-exprs))
(let ([ses (checked-syntax->list sig-exprs)])
(define-values (super-names super-ctimes super-rtimes super-bindings
super-val-defs super-stx-defs)
super-val-defs super-stx-defs super-ctcs)
(if super-sigid
(let* ([super-sig (lookup-signature super-sigid)]
[super-siginfo (signature-siginfo super-sig)])
@ -180,17 +183,24 @@
(siginfo-rtime-ids super-siginfo))
(map syntax-local-introduce (signature-vars super-sig))
(map introduce-def (signature-val-defs super-sig))
(map introduce-def (signature-stx-defs super-sig))))
(values '() '() '() '() '() '())))
(map introduce-def (signature-stx-defs super-sig))
(map (lambda (ctc)
(if ctc
(syntax-local-introduce ctc)
ctc))
(signature-ctcs super-sig))))
(values '() '() '() '() '() '() '())))
(let loop ((sig-exprs ses)
(bindings null)
(val-defs null)
(stx-defs null))
(stx-defs null)
(ctcs null))
(cond
((null? sig-exprs)
(let* ([all-bindings (append super-bindings (reverse bindings))]
[all-val-defs (append super-val-defs (reverse val-defs))]
[all-stx-defs (append super-stx-defs (reverse stx-defs))]
[all-ctcs (append super-ctcs (reverse ctcs))]
[dup
(check-duplicate-identifier
(append all-bindings
@ -221,12 +231,34 @@
((syntax-local-certifier)
(quote-syntax sbody)))
...)
(list #,@(map (lambda (c)
(if c
#`((syntax-local-certifier)
(quote-syntax #,c))
#'#f))
all-ctcs))
(quote-syntax #,sigid))))))))
(else
(syntax-case (car sig-exprs) (define-values define-syntaxes)
(syntax-case (car sig-exprs) (define-values define-syntaxes contracted)
(x
(identifier? #'x)
(loop (cdr sig-exprs) (cons #'x bindings) val-defs stx-defs))
(loop (cdr sig-exprs) (cons #'x bindings) val-defs stx-defs (cons #f ctcs)))
((x (y z) ...)
(and (identifier? #'x)
(module-identifier=? #'x #'contracted)
(andmap identifier? (syntax->list #'(y ...))))
(loop (cdr sig-exprs)
(append (syntax->list #'(y ...)) bindings)
val-defs
stx-defs
(append (syntax->list #'(z ...)) ctcs)))
((x . z)
(and (identifier? #'x)
(module-identifier=? #'x #'contracted))
(raise-syntax-error
'define-signature
"expected a list of [id contract] pairs after the contracted keyword"
(car sig-exprs)))
((x . y)
(and (identifier? #'x)
(or (module-identifier=? #'x #'define-values)
@ -248,7 +280,8 @@
(if (module-identifier=? #'x #'define-syntaxes)
(cons (cons (syntax->list #'(name ...)) b)
stx-defs)
stx-defs))))))))
stx-defs)
ctcs)))))))
((x . y)
(let ((trans
(set!-trans-extract
@ -266,7 +299,8 @@
(loop (append results (cdr sig-exprs))
bindings
val-defs
stx-defs))))
stx-defs
ctcs))))
(x (raise-stx-err
"expected either an identifier or signature form"
#'x))))))))
@ -425,6 +459,27 @@
(define-for-syntax process-unit-export
(process-unit-import/export process-tagged-export))
;; id->contract-src-info : identifier -> syntax
;; constructs the last argument to the contract, given an identifier
(define-for-syntax (id->contract-src-info id)
#`(list (make-srcloc (quote-syntax #,id)
#,(syntax-line id)
#,(syntax-column id)
#,(syntax-position id)
#,(syntax-span id))
#,(format "~s" (syntax-object->datum id))))
(define-syntax-parameter current-unit-blame-stx (lambda (stx) #'(#%variable-reference)))
(define-for-syntax (make-import-unboxing var loc ctc)
(if ctc
(quasisyntax/loc (error-syntax)
(quote-syntax (contract #,ctc (unbox #,loc) 'cant-happen
(current-unit-blame-stx)
#,(id->contract-src-info var))))
(quasisyntax/loc (error-syntax)
(quote-syntax (unbox #,loc)))))
;; build-unit : syntax-object ->
;; (values syntax-object (listof identifier) (listof identifier))
;; constructs the code for a unit expression. stx must be
@ -471,6 +526,13 @@
(map (lambda (x) (generate-temporaries (car x))) import-sigs)]
[((eloc ...) ...)
(map (lambda (x) (generate-temporaries (car x))) export-sigs)]
[((ectc ...) ...)
(map (λ (sig)
(map (λ (ctc)
(if ctc
(cons 'contract ctc)
#f))
(cadddr sig))) export-sigs)]
[((import-key import-super-keys ...) ...)
(map tagged-info->keys import-tagged-infos)]
[((export-key ...) ...)
@ -494,32 +556,36 @@
(vector-immutable (cons 'export-name
(vector-immutable export-key ...)) ...)
(list (cons 'dept depr) ...)
(lambda ()
(let ([eloc (box undefined)] ... ...)
(values
(lambda (import-table)
(let-values ([(iloc ...)
(vector->values (hash-table-get import-table import-key) 0 icount)]
...)
(letrec-syntaxes ([(int-ivar ...)
(make-id-mappers
(quote-syntax (unbox iloc))
...)]
...
[(int-evar ...)
(make-id-mappers
(quote-syntax (unbox eloc))
...)]
...)
(letrec-syntaxes+values (renames ...
mac ... ...)
(val ... ...)
(unit-body #,(error-syntax)
(int-ivar ... ...)
(int-evar ... ...)
(eloc ... ...)
. body)))))
(unit-export ((export-key ...) (vector-immutable eloc ...)) ...))))))
(syntax-parameterize ([current-unit-blame-stx (lambda (stx) #'(quote (unit name)))])
(lambda ()
(let ([eloc (box undefined)] ... ...)
(values
(lambda (import-table)
(let-values ([(iloc ...)
(vector->values (hash-table-get import-table import-key) 0 icount)]
...)
(letrec-syntaxes (#,@(map (lambda (ivs ils ics)
(quasisyntax/loc (error-syntax)
[#,ivs
(make-id-mappers
#,@(map (lambda (iv l c)
(make-import-unboxing iv l c))
(syntax->list ivs)
(syntax->list ils)
ics))]))
(syntax->list #'((int-ivar ...) ...))
(syntax->list #'((iloc ...) ...))
(map cadddr import-sigs)))
(letrec-syntaxes+values (renames ...
mac ... ...)
(val ... ...)
(unit-body #,(error-syntax)
(int-ivar ... ...)
(int-evar ... ...)
(eloc ... ...)
(ectc ... ...)
. body)))))
(unit-export ((export-key ...) (vector-immutable eloc ...)) ...)))))))
import-tagged-sigids
export-tagged-sigids
dep-tagged-sigids))))))
@ -533,17 +599,14 @@
(define-syntax (unit-body stx)
(syntax-case stx ()
((_ err-stx ivars evars elocs body ...)
((_ err-stx ivars evars elocs ectcs body ...)
(parameterize ((error-syntax #'err-stx))
(let* ([expand-context (generate-expand-context)]
[def-ctx (syntax-local-make-definition-context)]
[local-ivars (syntax->list (localify #'ivars def-ctx))]
[local-evars (syntax->list (localify #'evars def-ctx))]
[stop-list
(append
(kernel-form-identifier-list)
(syntax->list #'ivars)
(syntax->list #'evars))]
(syntax->list #'ivars))]
[definition?
(lambda (id)
(and (identifier? id)
@ -605,7 +668,8 @@
table id
(make-var-info (module-identifier=? #'dv (quote-syntax define-syntaxes))
#f
id)))
id
#f)))
(syntax->list #'(id ...)))]
[_ (void)])))
[_ (void)]))
@ -616,7 +680,7 @@
;; Mark exported names and
;; check that all exported names are defined (as var):
(for-each
(lambda (name loc)
(lambda (name loc ctc)
(let ([v (bound-identifier-mapping-get defined-names-table
name
(lambda () #f))])
@ -624,9 +688,16 @@
(raise-stx-err (format "undefined export ~a" (syntax-e name))))
(when (var-info-syntax? v)
(raise-stx-err "cannot export syntax from a unit" name))
(set-var-info-exported?! v loc)))
local-evars
(syntax->list #'elocs))
(set-var-info-exported?! v loc)
(when (pair? (syntax-e ctc))
(set-var-info-add-ctc!
v
(λ (e)
#`(contract #,(cdr (syntax-e ctc)) #,e (current-unit-blame-stx)
'cant-happen #,(id->contract-src-info e)))))))
(syntax->list (localify #'evars def-ctx))
(syntax->list #'elocs)
(syntax->list #'ectcs))
;; Check that none of the imports are defined
(for-each
@ -638,78 +709,42 @@
(raise-stx-err
"definition for imported identifier"
(var-info-id defid)))))
local-ivars)
(syntax->list (localify #'ivars def-ctx)))
(with-syntax ([(intname ...)
(foldr
(lambda (var res)
(cond
((not (or (var-info-syntax? (cdr var))
(var-info-exported? (cdr var))))
(cons (car var) res))
(else res)))
null
(bound-identifier-mapping-map defined-names-table cons))]
[(evar ...) #'evars]
[(l-evar ...) local-evars]
[(defn&expr ...)
(filter
values
(map (lambda (defn-or-expr)
(syntax-case defn-or-expr (define-values define-syntaxes)
[(define-values () expr)
(syntax/loc defn-or-expr (set!-values () expr))]
[(define-values ids expr)
(let ([ids (syntax->list #'ids)]
[do-one
(lambda (id tmp name)
(let ([export-loc
(var-info-exported?
(bound-identifier-mapping-get
defined-names-table
id))])
(cond
(export-loc
;; set! exported id:
(quasisyntax/loc defn-or-expr
(set-box! #,export-loc
#,(if name
#`(let ([#,name #,tmp])
#,name)
tmp))))
(else
;; not an exported id
(quasisyntax/loc defn-or-expr
(set! #,id #,tmp))))))])
(if (null? (cdr ids))
(do-one (car ids) (syntax expr) (car ids))
(let ([tmps (generate-temporaries ids)])
(with-syntax ([(tmp ...) tmps]
[(set ...)
(map (lambda (id tmp)
(do-one id tmp #f))
ids tmps)])
(syntax/loc defn-or-expr
(let-values ([(tmp ...) expr])
set ...))))))]
[(define-syntaxes . l) #f]
[else defn-or-expr]))
expanded-body))]
[(stx-defn ...)
(filter
values
(map (lambda (defn-or-expr)
(syntax-case defn-or-expr (define-syntaxes)
[(define-syntaxes . l) #'l]
[else #f]))
expanded-body))])
#'(letrec-syntaxes+values (stx-defn
...
((l-evar) (make-rename-transformer (quote-syntax evar)))
...)
([(intname) undefined] ...)
(void) ; in case the body would be empty
defn&expr ...)))))))
(let ([marker (make-syntax-introducer)])
(with-syntax ([(defn-or-expr ...)
(apply append
(map (λ (defn-or-expr)
(syntax-case defn-or-expr (define-values)
[(define-values (id ...) body)
(let* ([ids (syntax->list #'(id ...))]
[tmps (map marker ids)]
[do-one
(λ (id tmp)
(let ([var-info (bound-identifier-mapping-get
defined-names-table
id)])
(cond
[(var-info-exported? var-info)
=>
(λ (export-loc)
(let ([add-ctc (var-info-add-ctc var-info)])
(list (quasisyntax/loc defn-or-expr
(set-box! #,export-loc
(let ([#,id #,(if add-ctc (add-ctc tmp) tmp)])
#,id)))
(quasisyntax/loc defn-or-expr
(define-syntax #,id
(make-id-mapper (quote-syntax #,tmp)))))))]
[else (list (quasisyntax/loc defn-or-expr
(define-syntax #,id
(make-rename-transformer (quote-syntax #,tmp)))))])))])
(cons (quasisyntax/loc defn-or-expr
(define-values #,tmps body))
(apply append (map do-one ids tmps))))]
[else (list defn-or-expr)]))
expanded-body))])
#'(begin-with-definitions defn-or-expr ...))))))))
(define-for-syntax (redirect-imports/exports import?)
(lambda (table-stx
@ -1181,9 +1216,15 @@
(map
(lambda (os ov)
(map
(lambda (i)
#`(vector-ref #,ov #,i))
(iota (length (car os)))))
(lambda (i v c)
(if c
#`(contract #,c (unbox (vector-ref #,ov #,i))
'cant-happen (current-unit-blame-stx)
#,(id->contract-src-info v))
#`(unbox (vector-ref #,ov #,i))))
(iota (length (car os)))
(map car (car os))
(cadddr os)))
out-sigs
out-vec)))
(quasisyntax/loc stx
@ -1201,7 +1242,7 @@
((unit-go unit-tmp))))
(let ([out-vec (hash-table-get export-table key1)] ...)
(unit-fn #f)
(values (unbox out-code) ... ...))))))
(values out-code ... ...))))))
(define-syntaxes . renames) ...
(define-syntaxes (mac-name ...) mac-body) ... ...
(define-values (val-name ...) val-body) ... ...)))))
@ -1256,7 +1297,8 @@
((_ name . rest)
(begin
(check-id #'name)
(let-values (((exp i e d) (build #'rest)))
(let-values (((exp i e d) (parameterize ([error-syntax (syntax-property (error-syntax) 'inferred-name (syntax-e #'name))])
(build #'rest ))))
(with-syntax ((((itag . isig) ...) i)
(((etag . esig) ...) e)
(((deptag . depsig) ...) d))

View File

@ -160,6 +160,7 @@ the corresponding import. Each @scheme[tagged-sig-id] in an
[sig-elem
id
(contracted [id contract] ...)
(define-syntaxes (id ...) expr)
(define-values (value-id ...) expr)
(open sig-spec)
@ -175,6 +176,15 @@ of bindings for import or export:
@scheme[id]. That is, @scheme[id] is available for use in units
importing the signature, and @scheme[id] must be defined by units
exporting the signature.}
@item{Each @scheme[contracted] form in a signature declaration means
that a unit exporting the signature must supply a variable definition
for each @scheme[id] in that form. If the signature is imported, then
uses of @scheme[id] inside the unit are protected by the appropriate
contracts using the unit as the negative blame. If the signature is
exported, then the exported values are protected by the appropriate
contracts which use the unit as the positive blame, but internal uses
of the exported identifiers are not protected.}
@item{Each @scheme[define-syntaxes] form in a signature declaration
introduces a macro to that is available for use in any unit that

View File

@ -0,0 +1,154 @@
(require "test-harness.ss"
scheme/unit)
(define-signature sig1
((contracted [x number?])))
(define-signature sig2
((contracted [f (-> number? number?)])))
(define-signature sig3 extends sig2
((contracted [g (-> number? boolean?)])))
(define-signature sig4
((contracted [a number?] [b (-> boolean? number?)])))
(define-signature sig5
((contracted [c string?])
(contracted [d symbol?])))
(define-unit unit1
(import)
(export sig1)
(define x #f))
(define-unit unit2
(import sig1)
(export sig2)
(define (f n) x))
(define-unit unit3
(import sig3 sig4)
(export)
(b (g a)))
(define-unit unit4
(import sig3 sig4)
(export)
(g (b a)))
(define-unit unit5
(import)
(export sig5)
(define-values (c d) (values "foo" 3)))
(test-syntax-error "misuse of contracted"
contracted)
(test-syntax-error "invalid forms after contracted in signature"
(define-signature x ((contracted x y))))
(test-syntax-error "identifier not first part of pair after contracted in signature"
(define-signature x ((contracted [(-> number? number?) x]))))
(test-syntax-error "f not defined in unit exporting sig3"
(unit (import) (export sig3 sig4)
(define a #t)
(define g zero?)
(define (b t) (if t 3 0))))
(test-runtime-error exn:fail:contract? "x exported by unit1 not a number"
(invoke-unit unit1))
(test-runtime-error exn:fail:contract? "x exported by unit1 not a number"
(invoke-unit (compound-unit (import) (export)
(link (((S1 : sig1)) unit1)
(() unit2 S1)))))
(test-runtime-error exn:fail:contract? "a provided by anonymous unit not a number"
(invoke-unit (compound-unit (import) (export)
(link (((S3 : sig3) (S4 : sig4))
(unit (import) (export sig3 sig4)
(define a #t)
(define f add1)
(define g zero?)
(define (b t) (if t 3 0))))
(() unit3 S3 S4)))))
(test-runtime-error exn:fail:contract? "g provided by anonymous unit returns the wrong value"
(invoke-unit (compound-unit (import) (export)
(link (((S3 : sig3) (S4 : sig4))
(unit (import) (export sig3 sig4)
(define a 3)
(define f add1)
(define g values)
(define (b t) (if t 3 0))))
(() unit3 S3 S4)))))
(test-runtime-error exn:fail:contract? "unit4 misuses function b"
(invoke-unit (compound-unit (import) (export)
(link (((S3 : sig3) (S4 : sig4))
(unit (import) (export sig3 sig4)
(define a 3)
(define f add1)
(define g zero?)
(define (b t) (if t 3 0))))
(() unit4 S3 S4)))))
(test-runtime-error exn:fail:contract? "unit5 provides bad value for d"
(invoke-unit unit5))
(define-unit unit6
(import)
(export sig1)
(define-unit unit6-1
(import)
(export sig1)
(define x 3))
(define-values/invoke-unit unit6-1
(import)
(export sig1)))
(invoke-unit unit6)
(define-signature sig6
((contracted [x boolean?])))
(define-unit unit7
(import)
(export sig6)
(define-unit unit7-1
(import)
(export sig1)
(define x 3))
(define-values/invoke-unit unit7-1
(import)
(export sig1)))
(test-runtime-error exn:fail:contract? "unit7 reexports x with different (wrong) contract"
(invoke-unit unit7))
(define-unit unit8
(import)
(export)
(define-unit unit8-1
(import)
(export sig2)
(define f values))
(define-values/invoke-unit unit8-1
(import)
(export sig2))
(f #t))
(test-runtime-error exn:fail:contract? "unit8 misuses f from internal unit"
(invoke-unit unit8))
(define-unit unit9
(import)
(export)
(define-unit unit9-1
(import)
(export sig2)
(define f zero?))
(define-values/invoke-unit unit9-1
(import)
(export sig2))
(f 3))
(test-runtime-error exn:fail:contract? "unit9-1 provides wrong value for function f"
(invoke-unit unit9))