Fixed loophole which allowed external mutation of free variables (the shadowing copy was made at each call of the lambda, instead of being outside of it).

This commit is contained in:
Georges Dupéron 2017-05-18 20:56:12 +02:00
parent 3d8b7cf0be
commit f3d357943a
4 changed files with 115 additions and 12 deletions

View File

@ -9,6 +9,8 @@
(prefix-in te: type-expander)
phc-toolkit
(for-syntax (rename-in racket/base [... ])
racket/match
syntax/modcollapse
racket/list
racket/syntax
racket/contract
@ -62,13 +64,16 @@
(define-for-syntax built-in-pure-functions-free-id-set
(immutable-free-id-set
(syntax->list
#'(+ - * / modulo add1 sub1;; …
#'(+ - * / modulo add1 sub1 =;; …
eq? eqv? equal? ;; TODO: equal? can still cause problems if the
;; struct's prop:equal+hash is effectful.
error
format values
promise/pure/maybe-stateful? promise/pure/stateless?
;; Does not have a type yet:
;; list*
cons car cdr list list? pair? length reverse ;; …
null cons car cdr list list? pair? null? length reverse ;; …
void
vector-ref vector-immutable vector-length vector->list vector? ;; …
hash-ref hash->list hash? ;; …
set-member? set->list set? ;; …
@ -80,7 +85,13 @@
))))
(define-for-syntax (built-in-pure-function? id)
(free-id-set-member? built-in-pure-functions-free-id-set id))
(or (free-id-set-member? built-in-pure-functions-free-id-set id)
(match (identifier-binding id)
[(list (app collapse-module-path-index '(lib "racket/private/kw.rkt"))
'make-optional-keyword-procedure
_ _ _ _ _)
#t]
[_ #f])))
(define-syntax (def-built-in-set stx)
(syntax-case stx ()
@ -299,18 +310,18 @@
(define/with-syntax varref (datum->syntax self `(#%variable-reference)))
;; Prevent the mutation of the cached copy, by making it a macro which
;; rejects uses as the target of a set! .
#`(let ()
marked-as-unsafe ...
(let ([free free] )
;; Prevent the mutation of the cached copy, by making it a macro which
;; rejects uses as the target of a set! .
(let-syntax ([free (make-no-set!-transformer #'free)] )
;; The input should always be stateless
(assert free (check-immutable/error varref 'stateless))
;; The result must be pure too, otherwise it could (I
;; suppose) cause problems with occurrence typing, if a
;; copy if mutated but not the other, and TR still
;; copy is mutated but not the other, and TR still
;; expects them to be equal?
;; By construction, it should be immutable, except for functions
;; (which can hold internal state), but TR won't assume that when
@ -368,8 +379,9 @@
(quasisyntax/top-loc this-syntax
(define name
(declared-wrapper
(lam #,@(when-attr tvars #'(fa tvars)) args maybe-result-type
(pure/? (let () body ))))))]))
(pure/?
(lam #,@(when-attr tvars #'(fa tvars)) args maybe-result-type
(let () body ))))))]))
(define-syntax define-pure/stateful (define-pure/impl 'stateful))
(define-syntax define-pure/stateless (define-pure/impl 'stateless))

View File

@ -17,8 +17,8 @@
[make-promise/pure/stateful ( (a) ( ( a) (Promise a)))]
[make-promise/pure/stateless ( (a) ( ( a) (Promise a)))])
(define-syntax (delay/pure/stateful/unsafe stx)
(make-delayer stx #'make-promise/pure/stateful '()))
(define-for-syntax (stx-e x)
(if (syntax? x) (syntax-e x) x))
(define-syntax (delay/pure/stateless/unsafe stx)
(make-delayer stx #'make-promise/pure/stateless '()))
@ -27,10 +27,12 @@
(syntax-parser
[(_ e)
(syntax/top-loc this-syntax
(delay/pure/stateful/unsafe (pure/stateful e)))]))
(make-promise/pure/stateful
(pure-thunk/stateful (λ () e))))]))
(define-syntax delay/pure/stateless
(syntax-parser
[(_ e)
(syntax/top-loc this-syntax
(delay/pure/stateless/unsafe (pure/stateless e)))]))
(make-promise/pure/stateless
(pure-thunk/stateless (λ () e))))]))

View File

@ -46,6 +46,14 @@
@racket[struct] accessors and predicates, and @racket[struct] constructors for
immutable structures.
Note that the expressions can refer to variables mutated with @racket[set!]
by other code. Placing the expression in a lambda function and calling that
function twice may therefore yield different results, if other code mutates
some free variables between the two invocations. In order to produce a pure
thunk which caches its inputs (thereby shielding them from any mutation of the
external environment), use @racket[pure-thunk/stateless] and
@racket[pure-thunk/stateful] instead.
The first form, @racket[pure/stateless], checks that once fully-expanded, the
@racket[expression] does not contain uses of @racket[set!]. Since the free
variables can never refer to stateful functions, this means that any function

View File

@ -0,0 +1,81 @@
#lang typed/racket
(require delay-pure
typed/rackunit)
;; This file checks that externally mutating a free variable on which a pure
;; function or promise depends does not affect the function's result.
(check-equal? (let ([x 1])
(define d (delay/pure/stateful (add1 x)))
(list (begin (set! x -10) (force d))
(begin (set! x -11) (force d))))
'(2 2))
(check-equal? (let ([x 1])
(define d (delay/pure/stateless (add1 x)))
(list (begin (set! x -10) (force d))
(begin (set! x -11) (force d))))
'(2 2))
;; pure/stateless and pure/stateful do not protect the expression from
;; external mutations, so we are not testing this case here.
(check-equal? (let ([x 1])
(define d (pure-thunk/stateless (λ () (add1 x))))
(list (begin (set! x -10) (d))
(begin (set! x -11) (d))))
'(2 2))
(check-equal? (let ([x 1])
(define d (pure-thunk/stateless (λ () (add1 x)) #:check-result))
(list (begin (set! x -10) (d))
(begin (set! x -11) (d))))
'(2 2))
(check-equal? (let ([x 1])
(define d (pure-thunk/stateful (λ () (add1 x))))
(list (begin (set! x -10) (d))
(begin (set! x -11) (d))))
'(2 2))
(check-equal? (let ([x 1])
(define d (pure-thunk/stateful (λ () (add1 x)) #:check-result))
(list (begin (set! x -10) (d))
(begin (set! x -11) (d))))
'(2 2))
(check-equal? (let ([x 1])
(define-pure/stateless (d) (add1 x))
(list (begin (set! x -10) (d))
(begin (set! x -11) (d))))
'(2 2))
(check-equal? (let ([x 1])
(define-pure/stateless (d [opt : Number x]) (add1 opt))
(list (begin (set! x -10) (d))
(begin (set! x -11) (d))))
'(2 2))
(check-equal? (let ([x 1])
(define-pure/stateless (d #:kw [opt : Number x]) (add1 opt))
(list (begin (set! x -10) (d))
(begin (set! x -11) (d))))
'(2 2))
(check-equal? (let ([x 1])
(define-pure/stateful (d) (add1 x))
(list (begin (set! x -10) (d))
(begin (set! x -11) (d))))
'(2 2))
(check-equal? (let ([x 1])
(define-pure/stateful (d [opt : Number x]) (add1 opt))
(list (begin (set! x -10) (d))
(begin (set! x -11) (d))))
'(2 2))
(check-equal? (let ([x 1])
(define-pure/stateful (d #:kw [opt : Number x]) (add1 opt))
(list (begin (set! x -10) (d))
(begin (set! x -11) (d))))
'(2 2))