static-contracts: improve optimizer's test for flat scs

* Add `instantiate/optimize` to the static contracts API
  (new function in `instantiate.rkt`)
* Add optional kwd arg `#:recursive-kinds` to sc optimizer
* SC optimizer uses recursive kinds to tell if a `name/sc` or `recursive-sc`
  will generate a flat contract
* `instantiate/optimize`
  - solves for a recursive kinds table
  - calls `optimize` with the table
  - calls `instantiate` with the same table
This commit is contained in:
Ben Greenman 2017-10-14 02:51:51 -04:00
parent cd181f9d90
commit 966845304e
4 changed files with 84 additions and 26 deletions

View File

@ -17,7 +17,7 @@
racket/format
syntax/flatten-begin
(only-in (types abbrev) -Bottom -Boolean)
(static-contracts instantiate optimize structures combinators constraints)
(static-contracts instantiate structures combinators constraints)
(only-in (submod typed-racket/static-contracts/instantiate internals) compute-constraints)
;; TODO make this from contract-req
(prefix-in c: racket/contract)
@ -287,15 +287,14 @@
#:sc-cache [sc-cache (make-hash)])
(let/ec escape
(define (fail #:reason [reason #f]) (escape (init-fail #:reason reason)))
(instantiate
(optimize
(type->static-contract ty #:typed-side typed-side fail
#:cache sc-cache)
#:trusted-positive typed-side
#:trusted-negative (not typed-side))
(instantiate/optimize
(type->static-contract ty #:typed-side typed-side fail
#:cache sc-cache)
fail
kind
#:cache cache)))
#:cache cache
#:trusted-positive typed-side
#:trusted-negative (not typed-side))))
(define any-wrap/sc (chaperone/sc #'any-wrap/c))

View File

@ -15,6 +15,7 @@
"combinators/case-lambda.rkt"
"combinators/parametric.rkt"
"kinds.rkt"
"optimize.rkt"
"parametric-check.rkt"
"structures.rkt"
"constraints.rkt"
@ -23,33 +24,53 @@
(provide static-contract-may-contain-free-ids?)
(provide/cond-contract
[instantiate/optimize
(parametric->/c (a) ((static-contract? (-> #:reason (or/c #f string?) a))
(contract-kind? #:cache hash? #:trusted-positive boolean? #:trusted-negative boolean?)
. ->* . (or/c a (list/c (listof syntax?) syntax?))))]
[instantiate
(parametric->/c (a) ((static-contract? (-> #:reason (or/c #f string?) a))
(contract-kind? #:cache hash?)
(contract-kind? #:cache hash? #:recursive-kinds (or/c hash? #f))
. ->* . (or/c a (list/c (listof syntax?) syntax?))))]
[should-inline-contract? (-> syntax? boolean?)])
;; Providing these so that tests can work directly with them.
(module* internals #f
(provide compute-constraints
compute-recursive-kinds
instantiate/inner))
(define (instantiate/optimize sc fail [kind 'impersonator] #:cache [cache #f] #:trusted-positive [trusted-positive #f] #:trusted-negative [trusted-negative #f])
(define recursive-kinds
(with-handlers [(exn:fail:constraint-failure?
(lambda (exn)
;; Even if the constraints for `sc` are unsolvable,
;; the optimizer might be able to reduce parts of
;; `sc` to give a contract with solvable constraints.
;; This currently happens for the `Any-Syntax` type;
;; eventually that won't happen for `Any-Syntax`,
;; and at that point maybe we can fail here. -- Ben G.
#f))]
(compute-recursive-kinds
(contract-restrict-recursive-values (compute-constraints sc kind)))))
(define sc/opt (optimize sc #:trusted-positive trusted-positive #:trusted-negative trusted-negative #:recursive-kinds recursive-kinds))
(instantiate sc/opt fail kind #:cache cache #:recursive-kinds recursive-kinds))
;; kind is the greatest kind of contract that is supported, if a greater kind would be produced the
;; fail procedure is called.
;;
;; The cache is used to share contract definitions across multiple calls to
;; type->contract in a given contract fixup pass. If it's #f then that means don't
;; do any sharing (useful for testing).
(define (instantiate sc fail [kind 'impersonator] #:cache [cache #f])
(define (instantiate sc fail [kind 'impersonator] #:cache [cache #f] #:recursive-kinds [recursive-kinds #f])
(if (parametric-check sc)
(fail #:reason "multiple parametric contracts are not supported")
(with-handlers [(exn:fail:constraint-failure?
(lambda (exn) (fail #:reason (exn:fail:constraint-failure-reason exn))))]
(instantiate/inner sc
(compute-recursive-kinds
(contract-restrict-recursive-values (compute-constraints sc kind)))
(or recursive-kinds
(compute-recursive-kinds
(contract-restrict-recursive-values (compute-constraints sc kind))))
cache))))
;; computes the definitions that are in / used by `sc`

View File

@ -17,7 +17,7 @@
(provide/cond-contract
[optimize ((static-contract?) (#:trusted-positive boolean? #:trusted-negative boolean?)
[optimize ((static-contract?) (#:trusted-positive boolean? #:trusted-negative boolean? #:recursive-kinds (or/c #f hash?))
. ->* . static-contract?)])
;; Reduce a static contract to a smaller simpler one that protects in the same way
@ -110,15 +110,15 @@
;; Reduce a static contract assuming that we trusted the current side
(define (trusted-side-reduce sc)
(define ((make-trusted-side-reduce flat-sc?) sc)
(match sc
[(->/sc: mand-args opt-args mand-kw-args opt-kw-args rest-arg (list (any/sc:) ...))
(function/sc #t mand-args opt-args mand-kw-args opt-kw-args rest-arg #f)]
[(arr/sc: args rest (list (any/sc:) ...))
(arr/sc args rest #f)]
[(none/sc:) any/sc]
[(or/sc: (? flat-terminal-kind?) ...) any/sc]
[(? flat-terminal-kind?) any/sc]
[(or/sc: (? flat-sc?) ...) any/sc]
[(? flat-sc?) any/sc]
[(syntax/sc: (? recursive-sc?))
;;bg; _temporary_ case to allow contracts from the `Syntax` type.
;; This is temporary until TR has types for immutable-vector
@ -126,9 +126,6 @@
any/sc]
[else sc]))
(define (flat-terminal-kind? sc)
(eq? 'flat (sc-terminal-kind sc)))
;; The side of a static contract describes the source of the values that
;; the contract needs to check.
;; - 'positive : values exported by the server module
@ -176,12 +173,13 @@
;; update-side : sc? weak-side? -> weak-side?
;; Change the current side to something safe & strong-as-possible
;; for optimizing the sub-contracts of the given `sc`.
(define (update-side sc side)
(define ((make-update-side flat-sc?) sc side)
(match sc
[(or/sc: scs ...)
#:when (not (andmap flat-terminal-kind? scs))
#:when (not (andmap flat-sc? scs))
(weaken-side side)]
[(? guarded-sc?)
[_
#:when (guarded-sc? sc)
(strengthen-side side)]
[_
;; Keep same side by default.
@ -194,8 +192,7 @@
;; type constructor. E.g. list/sc is "real" and or/sc is not.
(define (guarded-sc? sc)
(match sc
[(or (? flat-terminal-kind?)
(->/sc: _ _ _ _ _ _)
[(or (->/sc: _ _ _ _ _ _)
(arr/sc: _ _ _)
(async-channel/sc: _)
(box/sc: _)
@ -292,9 +289,28 @@
(sc-map sc trim)]))
(trim sc 'covariant))
(define (make-sc->kind recursive-kinds)
(if recursive-kinds
(λ (sc)
(let loop ([sc sc])
(match sc
[(recursive-sc _ _ body)
(loop body)]
[(or (recursive-sc-use id)
(name/sc: id))
(hash-ref recursive-kinds id #f)]
[_
(sc-terminal-kind sc)])))
sc-terminal-kind))
;; If we trust a specific side then we drop all contracts protecting that side.
(define (optimize sc #:trusted-positive [trusted-positive #f] #:trusted-negative [trusted-negative #f])
(define (optimize sc #:trusted-positive [trusted-positive #f] #:trusted-negative [trusted-negative #f] #:recursive-kinds [recursive-kinds #f])
(define flat-sc?
(let ([sc->kind (make-sc->kind recursive-kinds)])
(λ (sc) (eq? 'flat (sc->kind sc)))))
(define trusted-side-reduce (make-trusted-side-reduce flat-sc?))
(define update-side (make-update-side flat-sc?))
;; single-step: reduce and trusted-side-reduce if appropriate
(define (single-step sc maybe-weak-side)
(define trusted

View File

@ -0,0 +1,22 @@
#lang racket/base
;; Test that the `Spec` type can be converted to a contract that
;; successfully **runs**
(module t typed/racket/base
(provide f g)
(define-type Spec
(-> (U Spec String)))
(: f (-> Spec))
(define (f)
(λ () "hello"))
(: g (-> (Rec T (-> (U T String)))))
(define (g)
(λ () "hello")))
(require 't)
(void f g)