Remove code that handles #<undefined> in TR
TR no longer needs to handle #<undefined> because the value no longer leaks out from uninitialized variables. However, uses of uninitialized variables are not caught by TR (they are treated like errors from the `error` function).
This commit is contained in:
Asumu Takikawa
parent
d4c60e8608
commit
715d596e47
|
|
@ -35,63 +35,50 @@
|
|||
;; Checks that the body has the expected type when names are bound to the types spcified by results.
|
||||
;; The exprs are also typechecked by using expr->type.
|
||||
;; TODO: make this function sane.
|
||||
(define/cond-contract (do-check expr->type namess results expected-results exprs body expected)
|
||||
((syntax? tc-results/c . -> . any/c)
|
||||
(listof (listof identifier?)) (listof tc-results/c) (listof tc-results/c)
|
||||
(listof syntax?) syntax? (or/c #f tc-results/c)
|
||||
. -> .
|
||||
tc-results/c)
|
||||
(with-cond-contract t/p ([types (listof (listof Type/c))] ; types that may contain undefined (letrec)
|
||||
[expected-types (listof (listof Type/c))] ; types that may not contain undefined (what we got from the user)
|
||||
[props (listof (listof Filter?))])
|
||||
(define-values (types expected-types props)
|
||||
(for/lists (t e p)
|
||||
([r (in-list results)]
|
||||
[e-r (in-list expected-results)]
|
||||
[names (in-list namess)])
|
||||
(match* (r e-r)
|
||||
[((tc-results: ts (FilterSet: fs+ fs-) os) (tc-results: e-ts _ _)) ; rest should be the same
|
||||
;(printf "f+: ~a\n" fs+)
|
||||
;(printf "f-: ~a\n" fs-)
|
||||
(values ts
|
||||
e-ts
|
||||
(apply append
|
||||
(for/list ([n (in-list names)]
|
||||
[f+ (in-list fs+)]
|
||||
[f- (in-list fs-)])
|
||||
(if (is-var-mutated? n)
|
||||
(list)
|
||||
(list (-imp (-not-filter (-val #f) n) f+)
|
||||
(-imp (-filter (-val #f) n) f-))))))]
|
||||
[((tc-results: ts (NoFilter:) _) (tc-results: e-ts (NoFilter:) _))
|
||||
(values ts e-ts null)]))))
|
||||
(with-cond-contract append-region ([p1 (listof Filter?)]
|
||||
[p2 (listof Filter?)])
|
||||
(define-values (p1 p2)
|
||||
(combine-props (apply append props) (env-props (lexical-env)) (box #t))))
|
||||
;; extend the lexical environment for checking the body
|
||||
(define/cond-contract (do-check expr->type namess expected-results exprs body expected)
|
||||
((syntax? tc-results/c . -> . any/c)
|
||||
(listof (listof identifier?)) (listof tc-results/c) (listof tc-results/c)
|
||||
(listof syntax?) syntax? (or/c #f tc-results/c)
|
||||
. -> .
|
||||
tc-results/c)
|
||||
(with-cond-contract t/p ([expected-types (listof (listof Type/c))]
|
||||
[props (listof (listof Filter?))])
|
||||
(define-values (expected-types props)
|
||||
(for/lists (e p)
|
||||
([e-r (in-list expected-results)]
|
||||
[names (in-list namess)])
|
||||
(match e-r
|
||||
[(tc-results: e-ts (FilterSet: fs+ fs-) os)
|
||||
(values e-ts
|
||||
(apply append
|
||||
(for/list ([n (in-list names)]
|
||||
[f+ (in-list fs+)]
|
||||
[f- (in-list fs-)])
|
||||
(if (is-var-mutated? n)
|
||||
(list)
|
||||
(list (-imp (-not-filter (-val #f) n) f+)
|
||||
(-imp (-filter (-val #f) n) f-))))))]
|
||||
[(tc-results: e-ts (NoFilter:) _)
|
||||
(values e-ts null)]))))
|
||||
(with-cond-contract append-region ([p1 (listof Filter?)]
|
||||
[p2 (listof Filter?)])
|
||||
(define-values (p1 p2)
|
||||
(combine-props (apply append props) (env-props (lexical-env)) (box #t))))
|
||||
;; extend the lexical environment for checking the body
|
||||
(with-lexical-env/extend/props
|
||||
;; the list of lists of name
|
||||
namess
|
||||
;; the types
|
||||
types
|
||||
(append p1 p2)
|
||||
(for-each expr->type
|
||||
exprs
|
||||
expected-results)
|
||||
(with-lexical-env/extend/props
|
||||
;; we typechecked the rhss with the lhss having types that potentially contain undefined
|
||||
;; if undefined can actually show up, a type error will have been triggered
|
||||
;; it is therefore safe to typecheck the body with the original types the user gave us
|
||||
;; any undefined-related problems have been caught already
|
||||
namess
|
||||
expected-types ; types w/o undefined
|
||||
expected-types
|
||||
(append p1 p2)
|
||||
;; type-check the rhs exprs
|
||||
(for-each expr->type
|
||||
exprs
|
||||
expected-results)
|
||||
;; typecheck the body
|
||||
(replace-names (get-names+objects namess expected-results)
|
||||
(if expected
|
||||
(tc-body/check body (erase-filter expected))
|
||||
(tc-body body))))))
|
||||
(replace-names
|
||||
(get-names+objects namess expected-results)
|
||||
(if expected
|
||||
(tc-body/check body (erase-filter expected))
|
||||
(tc-body body)))))
|
||||
|
||||
(define (tc-expr/maybe-expected/t e names)
|
||||
(syntax-parse names
|
||||
|
|
@ -152,37 +139,14 @@
|
|||
(cond
|
||||
;; after everything, check the body expressions
|
||||
[(null? remaining-names)
|
||||
(if expected
|
||||
(tc-body/check body (erase-filter expected))
|
||||
(tc-body body))]
|
||||
(if expected
|
||||
(tc-body/check body (erase-filter expected))
|
||||
(tc-body body))]
|
||||
[else
|
||||
(define flat-names (apply append remaining-names))
|
||||
(do-check tc-expr/check
|
||||
remaining-names
|
||||
;; compute set of variables that can't be undefined. see below.
|
||||
(let-values
|
||||
([(safe-bindings _)
|
||||
(for/fold ([safe-bindings '()] ; includes transitively-safe
|
||||
[transitively-safe-bindings '()])
|
||||
([names (in-list remaining-names)]
|
||||
[expr (in-list remaining-exprs)])
|
||||
(case (safe-letrec-values-clause? expr transitively-safe-bindings flat-names)
|
||||
;; transitively safe -> safe to mention in a subsequent rhs
|
||||
[(transitively-safe) (values (append names safe-bindings)
|
||||
(append names transitively-safe-bindings))]
|
||||
;; safe -> safe by itself, but may not be safe to use in a subsequent rhs
|
||||
[(safe) (values (append names safe-bindings)
|
||||
transitively-safe-bindings)]
|
||||
;; unsafe -> could be undefined
|
||||
[(unsafe) (values safe-bindings transitively-safe-bindings)]))])
|
||||
(map (λ (l) (let ([types-from-user (map get-type l)])
|
||||
(ret (if (andmap (λ (x) ; are all the lhs vars safe?
|
||||
(member x safe-bindings bound-identifier=?))
|
||||
l)
|
||||
types-from-user
|
||||
(map (λ (x) (Un x -Undefined)) types-from-user)))))
|
||||
remaining-names))
|
||||
;; types the user gave. check against that to error if we could get undefined
|
||||
;; types the user gave.
|
||||
(map (λ (l) (ret (map get-type l))) remaining-names)
|
||||
remaining-exprs body expected)])))))
|
||||
|
||||
|
|
@ -267,37 +231,6 @@
|
|||
(cons names env-ids)
|
||||
(cons results env-types)))])))
|
||||
|
||||
;; determines whether any of the variables bound in the given clause can have an undefined value
|
||||
;; in this case, we cannot trust the type the user gave us and must union it with undefined
|
||||
;; for example, the following code:
|
||||
;; (letrec: ([x : Float x]) x)
|
||||
;; should not typecheck with type Float, even though the user said so, because the actual value
|
||||
;; is undefined.
|
||||
;; this implements a conservative analysis.
|
||||
;; we identify 3 kinds of bindings:
|
||||
;; - safe bindings cannot be undefined
|
||||
;; - transitively safe bindings are safe and can safely be used in subsequent rhss
|
||||
;; - unsafe bindings may be undefined
|
||||
;; x is transitively safe if for all its free variables, they are either transitively safe and
|
||||
;; earlier in the letrec or they are bound outside the letrec
|
||||
;; x is safe if it is transitively safe or if its rhs is a lambda
|
||||
;; otherwise, x is unsafe
|
||||
;; this function returns either 'transitively-safe, 'safe or 'unsafe
|
||||
;; Note: In some cases (such as the example on the bottom of page 6 of Ghuloum and Dybvig's
|
||||
;; Fixing Letrec (reloaded) paper), we are more conservative than a fully-connected component
|
||||
;; based approach. On the other hand, our algorithm should cover most interesting cases and
|
||||
;; is much simpler than Tarjan's.
|
||||
(define (safe-letrec-values-clause? expr transitively-safe-bindings letrec-bound-ids)
|
||||
(cond [(andmap (lambda (fv)
|
||||
(or (not (member fv letrec-bound-ids bound-identifier=?)) ; from outside
|
||||
(member fv transitively-safe-bindings bound-identifier=?)))
|
||||
(free-vars expr))
|
||||
'transitively-safe]
|
||||
[else
|
||||
(syntax-parse expr #:literal-sets (kernel-literals)
|
||||
[(#%plain-lambda _ ...) 'safe]
|
||||
[else 'unsafe])]))
|
||||
|
||||
;; this is so match can provide us with a syntax property to
|
||||
;; say that this binding is only called in tail position
|
||||
(define ((tc-expr-t/maybe-expected expected) e)
|
||||
|
|
@ -322,4 +255,4 @@
|
|||
[types (for/list ([name (in-list names)] [e (in-list exprs)])
|
||||
(get-type/infer name e (tc-expr-t/maybe-expected expected)
|
||||
tc-expr/check))])
|
||||
(do-check void names types types exprs body expected)))
|
||||
(do-check void names types exprs body expected)))
|
||||
|
|
|
|||
|
|
@ -1,8 +1,9 @@
|
|||
#;
|
||||
(exn-pred 2)
|
||||
(exn-pred "x:.*cannot use before initialization")
|
||||
#lang typed/racket
|
||||
|
||||
;; make sure letrec takes into account that some bindings may be undefined
|
||||
;; This test previously tested TR's static analysis of undefined
|
||||
;; variables, but it now just delegates to Racket's dynamic checks.
|
||||
|
||||
(+ (letrec: ([x : Float x]) x) 1) ; PR 11511
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,10 @@
|
|||
#;
|
||||
(exn-pred "Undefined")
|
||||
(exn-pred "x:.*cannot use before initialization")
|
||||
#lang scheme/load
|
||||
|
||||
;; This test used to fail due to a type error, but TR no longer
|
||||
;; tracks undefined statically, so it is just a dynamic error.
|
||||
|
||||
(module A scheme
|
||||
|
||||
(define (f x) (add1 x))
|
||||
|
|
|
|||
|
|
@ -846,15 +846,36 @@
|
|||
|
||||
[tc-e (letrec: ([x : Number (values 1)]) (add1 x)) -Number]
|
||||
|
||||
;; This test case used to test Undefined, but the `x` is now Bottom because
|
||||
;; cyclic definitions can be given *any* type. This is ok since cyclic definitions
|
||||
;; are just errors that TR does not handle (because #<undefined> no longer leaks out
|
||||
;; in such cases).
|
||||
[tc-e (let ()
|
||||
(: complicated Boolean)
|
||||
(define complicated #f)
|
||||
(: undefined Undefined)
|
||||
(define undefined (letrec: ((x : Undefined x)) x))
|
||||
(letrec: ((x : Undefined (if complicated undefined undefined))
|
||||
(y : Undefined (if complicated x undefined)))
|
||||
(: undefined (Un))
|
||||
(define undefined (letrec: ((x : (Un) x)) x))
|
||||
(letrec: ((x : (Un) (if complicated undefined undefined))
|
||||
(y : (Un) (if complicated x undefined)))
|
||||
y))
|
||||
-Undefined]
|
||||
-Bottom]
|
||||
|
||||
;; This case fails, unlike the last one, since the types in the
|
||||
;; cycle are inconsistent. Note that this will error (if it typechecked)
|
||||
;; because of the uninitialized variables.
|
||||
[tc-err (let ()
|
||||
(: x String)
|
||||
(define x y)
|
||||
(: y Symbol)
|
||||
(define y x)
|
||||
y)
|
||||
#:ret (ret -Symbol)
|
||||
#:msg #rx"expected: String|expected: Symbol"]
|
||||
|
||||
;; Test ill-typed code in letrec RHS
|
||||
[tc-err (let () (: x String) (define x 'foo) x)
|
||||
#:ret (ret -String)
|
||||
#:msg #rx"expected: String.*given: 'foo"]
|
||||
|
||||
[tc-err (let ([x (add1 5)])
|
||||
(set! x "foo")
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user