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

Forbid singleton types for integers whose type is platform-dependent.

Browse Source 
Closes PR13501.
This commit is contained in:
Vincent St-Amour 2013-02-11 12:25:30 -05:00
parent b9d1194225
commit 0bccf6b0b0
3 changed files with 34 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
collects/tests/typed-racket/fail/non-portable-fixnum-singleton.rkt Normal file
View File

@ -0,0 +1,8 @@
#;
(exn-pred exn:fail:syntax?)
#lang typed/racket
;; singleton types for values who runtime type depends is platform-dependent are unsafe
;; PR13501
(define: z : 10000000000000 10000000000000)
(ann (if (and #t (fixnum? z)) z 0) (U 0 1))

9
collects/tests/typed-racket/unit-tests/typecheck-tests.rkt
View File

@ -218,6 +218,15 @@
(tc-e (min (ann -2 Negative-Fixnum) (ann 3 Fixnum)) -NegFixnum) (tc-e (min (ann -2 Negative-Fixnum) (ann 3 Fixnum)) -NegFixnum)
(tc-e (min (ann 3 Fixnum) (ann -2 Negative-Fixnum)) -NegFixnum) (tc-e (min (ann 3 Fixnum) (ann -2 Negative-Fixnum)) -NegFixnum)
(tc-e (exact->inexact (ann 3 Number)) (t:Un -InexactReal -InexactComplex)) (tc-e (exact->inexact (ann 3 Number)) (t:Un -InexactReal -InexactComplex))
(tc-err (let: ([z : 10000000000000 10000000000000]) z)) ; unsafe
(tc-err (let: ([z : -4611686018427387904 -4611686018427387904]) z)) ; unsafe
(tc-e (let: ([z : -4611686018427387905 -4611686018427387905]) z) (-val -4611686018427387905))
(tc-err (let: ([z : -1073741825 -1073741825]) z)) ; unsafe
(tc-e (let: ([z : -1073741824 -1073741824]) z) (-val -1073741824))
(tc-e (let: ([z : 268435455 268435455]) z) (-val 268435455))
(tc-err (let: ([z : 268435456 268435456]) z)) ; unsafe
(tc-err (let: ([z : 4611686018427387903 4611686018427387903]) z)) ; unsafe
(tc-e (let: ([z : 4611686018427387904 4611686018427387904]) z) (-val 4611686018427387904))
[tc-e/t (lambda: () 3) (t:-> -PosByte : -true-lfilter)] [tc-e/t (lambda: () 3) (t:-> -PosByte : -true-lfilter)]
[tc-e/t (lambda: ([x : Number]) 3) (t:-> N -PosByte : -true-lfilter)] [tc-e/t (lambda: ([x : Number]) 3) (t:-> N -PosByte : -true-lfilter)]

18
collects/typed-racket/private/parse-type.rkt
View File

@ -378,7 +378,23 @@
[(Error:) Err] [(Error:) Err]
[_ Err]))] [_ Err]))]
[t:atom [t:atom
(-val (syntax-e #'t))] ;; Integers in a "grey area", that is, integers whose runtime type is
;; platform-dependent, cannot be safely assigned singleton types.
;; Short story: (subtype (-val 10000000000000) -Fixnum) has no safe
;; answer. It's not a fixnum on 32 bits, and saying it's not a fixnum
;; causes issues with type-dead code detection.
;; Long story: See email trail for PR13501 and #racket IRC logs from
;; Feb 11 2013.
(let ([val (syntax-e #'t)])
(when (and (exact-integer? val)
;; [min-64bit-fixnum, min-portable-fixnum)
(or (and (>= val (- (expt 2 62)))
(< val (- (expt 2 30))))
;; (max-portable-index, max-64bit-fixnum]
(and (> val (sub1 (expt 2 28)))
(<= val (sub1 (expt 2 62))))))
(tc-error "non-portable fixnum singleton types are not valid types: ~a" val))
(-val val))]
[_ (tc-error "not a valid type: ~a" (syntax->datum stx))]))) [_ (tc-error "not a valid type: ~a" (syntax->datum stx))])))
(define (parse-list-type stx) (define (parse-list-type stx)