From 23b147607ff91e66a0edcb785e5c911d9e8fc6e3 Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Wed, 16 Apr 2014 16:13:29 -0400 Subject: [PATCH] Remove code that handles # in TR TR no longer needs to handle # 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). original commit: 715d596e47b7c5cbd7b17ff36ceea73678c7071f --- .../typed-racket/typecheck/tc-let-unit.rkt | 157 +++++------------- .../tests/typed-racket/fail/safe-letrec.rkt | 5 +- .../tests/typed-racket/fail/undefined.rkt | 5 +- .../unit-tests/typecheck-tests.rkt | 31 +++- 4 files changed, 78 insertions(+), 120 deletions(-) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt index f9c2b8e4..0ea58643 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt @@ -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))) diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/safe-letrec.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/safe-letrec.rkt index c28a160f..671f2803 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/safe-letrec.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/safe-letrec.rkt @@ -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 diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/undefined.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/undefined.rkt index 53f0809a..5048e7d6 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/undefined.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/undefined.rkt @@ -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)) diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt index 9546c065..389a8589 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt @@ -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 # 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")