From 76c3ec443f95150338a2b2f97d296dd97a17ffb2 Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Sat, 24 May 2014 13:45:42 -0700 Subject: [PATCH] Remove ability to check unreachable code. If code is unreachable then looking up any variable should return Bottom. But implementing checking unreachable code that way is not that useful. --- .../typed-racket/typecheck/tc-if.rkt | 37 ++++------------- .../typed-racket/typecheck/tc-lambda-unit.rkt | 2 +- .../typed-racket/types/type-table.rkt | 40 +++++++++++-------- .../typed-racket/utils/tc-utils.rkt | 2 - .../typed-racket/fail/check-unreachable.rkt | 17 -------- 5 files changed, 32 insertions(+), 66 deletions(-) delete mode 100644 pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/check-unreachable.rkt diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt index 97d4a2d857..34fe39d4a3 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-if.rkt @@ -15,19 +15,10 @@ (define (tc/if-twoarm tst thn els [expected #f]) (define (tc expr reachable?) (unless reachable? (warn-unreachable expr)) - (cond - ;; if reachable? is #f, then we don't want to verify that this branch has the appropriate type - ;; in particular, it might be (void) - [(and expected reachable?) - (tc-expr/check expr (erase-filter expected))] - ;; this code is reachable, but we have no expected type - [reachable? (tc-expr expr)] - ;; otherwise, this code is unreachable - ;; and the resulting type should be the empty type - [(check-unreachable-code?) - (tc-expr expr) - (ret (Un))] - [else (ret (Un))])) + ;; If the code is unreachable, the resulting type should be Bottom. + (if reachable? + (tc-expr/check expr (and expected (erase-filter expected))) + (ret -Bottom))) (match (single-value tst) [(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _) (define flag+ (box #t)) @@ -42,20 +33,8 @@ (tc els (unbox flag-)) fs-))) ;; record reachability - ;; since we may typecheck a given piece of code multiple times in different - ;; contexts, we need to take previous results into account - (cond [(and (not (unbox flag+)) ; maybe contradiction - ;; to be an actual contradiction, we must have either previously - ;; recorded this test as a contradiction, or have never seen it - ;; before - (not (tautology? tst)) - (not (neither? tst))) - (add-contradiction tst)] - [(and (not (unbox flag-)) ; maybe tautology - ;; mirror case - (not (contradiction? tst)) - (not (neither? tst))) - (add-tautology tst)] - [else - (add-neither tst)]) + (when (unbox flag+) + (test-position-add-true tst)) + (when (unbox flag-) + (test-position-add-false tst)) (merge-tc-results (list results-t results-u))])) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt index 8534f0eaf2..00ed03c8f6 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt @@ -347,7 +347,7 @@ (null? matching-arrs)) (warn-unreachable body) (add-dead-lambda-branch (formals-syntax formal)) - (list formal body (if (check-unreachable-code?) #f null))] + (list formal body null)] [else (list formal body matching-arrs)]) formals+bodies+arrs*) (arities-seen-add arities-seen arity))]))) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/type-table.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/type-table.rkt index c7d847d327..455e9b1fc4 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/type-table.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/type-table.rkt @@ -16,12 +16,10 @@ [add-typeof-expr (syntax? tc-results/c . -> . any/c)] [type-of (syntax? . -> . tc-results/c)] [reset-type-table (-> any/c)] - [add-tautology (syntax? . -> . any)] - [add-contradiction (syntax? . -> . any)] - [add-neither (syntax? . -> . any)] + [test-position-add-true (syntax? . -> . any)] + [test-position-add-false (syntax? . -> . any)] [tautology? (syntax? . -> . boolean?)] [contradiction? (syntax? . -> . boolean?)] - [neither? (syntax? . -> . boolean?)] [add-dead-lambda-branch (syntax? . -> . any)] [dead-lambda-branch? (syntax? . -> . boolean?)] [;; Register that the given expression should be ignored @@ -64,22 +62,30 @@ (syntax-line e) (syntax-column e)))))) -;; keeps track of expressions that always evaluate to true or always evaluate -;; to false, so that the optimizer can eliminate dead code -;; 3 possible values: 'tautology 'contradiction 'neither -(define tautology-contradiction-table (make-hasheq)) +;; For expressions in test position keep track of if it evaluates to true/false +;; values: can be 'true, 'false, 'both. +(define test-position-table (make-hasheq)) -(define-values (add-tautology add-contradiction add-neither) +(define (test-position-add-true expr) + (hash-update! test-position-table expr + (lambda (v) + (case v + [(true) 'true] + [(false both) 'both])) + 'true)) +(define (test-position-add-false expr) + (hash-update! test-position-table expr + (lambda (v) + (case v + [(false) 'false] + [(true both) 'both])) + 'false)) + +(define-values (tautology? contradiction?) (let () (define ((mk t?) e) - (when (optimize?) - (hash-set! tautology-contradiction-table e t?))) - (values (mk 'tautology) (mk 'contradiction) (mk 'neither)))) -(define-values (tautology? contradiction? neither?) - (let () - (define ((mk t?) e) - (eq? t? (hash-ref tautology-contradiction-table e 'not-there))) - (values (mk 'tautology) (mk 'contradiction) (mk 'neither)))) + (eq? t? (hash-ref test-position-table e 'not-there))) + (values (mk 'true) (mk 'false)))) ;; keeps track of lambda branches that never get evaluated, so that the ;; optimizer can eliminate dead code. The key is the formals syntax object. diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/tc-utils.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/tc-utils.rkt index d2c202f8cd..e0a5992235 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/tc-utils.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/utils/tc-utils.rkt @@ -15,7 +15,6 @@ don't depend on any other portion of the system orig-module-stx expanded-module-stx print-syntax? - check-unreachable-code? warn-unreachable? delay-errors? current-type-names @@ -57,7 +56,6 @@ don't depend on any other portion of the system ;; do we print the fully-expanded syntax in error messages? (define print-syntax? (make-parameter #f)) -(define check-unreachable-code? (make-parameter #f)) (define warn-unreachable? (make-parameter #t)) diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/check-unreachable.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/check-unreachable.rkt deleted file mode 100644 index 511f2bd269..0000000000 --- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/check-unreachable.rkt +++ /dev/null @@ -1,17 +0,0 @@ -#; -(exn-pred #rx"expected: Symbol.*given: String") -#lang racket/load - -;; This test makes sure that the check-unreachable-code mode -;; actually works. - -(require (for-syntax typed-racket/utils/tc-utils)) - -(begin-for-syntax - (check-unreachable-code? #t)) - -(require typed/racket) - -(if #t - "foo" - (symbol->string "foo"))