wingo pushed a commit to branch master in repository guile. commit 1071e77785aca6cb319e3258e187f63f890da2e0 Author: Andy Wingo <wi...@pobox.com> Date: Thu Jun 4 12:53:18 2015 +0200
Add CPS2 verification pass * module/language/cps2/verify.scm: New diagnostic pass. * module/Makefile.am: Add verify.scm. * module/language/cps2/optimize.scm: Wire up verification pass. Always run the pass at the end, and if a variable is set run it between passes too. --- module/Makefile.am | 1 + module/language/cps2/optimize.scm | 14 ++- module/language/cps2/verify.scm | 303 +++++++++++++++++++++++++++++++++++++ 3 files changed, 316 insertions(+), 2 deletions(-) diff --git a/module/Makefile.am b/module/Makefile.am index 666175c..0bb2a56 100644 --- a/module/Makefile.am +++ b/module/Makefile.am @@ -166,6 +166,7 @@ CPS2_LANG_SOURCES = \ language/cps2/type-fold.scm \ language/cps2/types.scm \ language/cps2/utils.scm \ + language/cps2/verify.scm \ language/cps2/with-cps.scm BYTECODE_LANG_SOURCES = \ diff --git a/module/language/cps2/optimize.scm b/module/language/cps2/optimize.scm index ba8699f..e0f9aca 100644 --- a/module/language/cps2/optimize.scm +++ b/module/language/cps2/optimize.scm @@ -35,6 +35,7 @@ #:use-module (language cps2 simplify) #:use-module (language cps2 specialize-primcalls) #:use-module (language cps2 type-fold) + #:use-module (language cps2 verify) #:export (optimize)) (define (kw-arg-ref args kw default) @@ -42,13 +43,22 @@ ((_ val . _) val) (_ default))) +(define *debug?* #f) + +(define (maybe-verify program) + (if *debug?* + (verify program) + program)) + (define* (optimize program #:optional (opts '())) (define (run-pass! pass kw default) (set! program (if (kw-arg-ref opts kw default) - (pass program) + (maybe-verify (pass program)) program))) + (maybe-verify program) + ;; This series of assignments to `program' used to be a series of let* ;; bindings of `program', as you would imagine. In compiled code this ;; is fine because the compiler is able to allocate all let*-bound @@ -75,4 +85,4 @@ ;; (run-pass! eliminate-dead-code #:eliminate-dead-code? #t) ;; (run-pass! simplify #:simplify? #t) - program) + (verify program)) diff --git a/module/language/cps2/verify.scm b/module/language/cps2/verify.scm new file mode 100644 index 0000000..8d55042 --- /dev/null +++ b/module/language/cps2/verify.scm @@ -0,0 +1,303 @@ +;;; Diagnostic checker for CPS +;;; Copyright (C) 2014, 2015 Free Software Foundation, Inc. +;;; +;;; This library is free software: you can redistribute it and/or modify +;;; it under the terms of the GNU Lesser General Public License as +;;; published by the Free Software Foundation, either version 3 of the +;;; License, or (at your option) any later version. +;;; +;;; This library is distributed in the hope that it will be useful, but +;;; WITHOUT ANY WARRANTY; without even the implied warranty of +;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU +;;; Lesser General Public License for more details. +;;; +;;; You should have received a copy of the GNU Lesser General Public +;;; License along with this program. If not, see +;;; <http://www.gnu.org/licenses/>. + +;;; Commentary: +;;; +;;; A routine to detect invalid CPS. +;;; +;;; Code: + +(define-module (language cps2 verify) + #:use-module (ice-9 match) + #:use-module (language cps2) + #:use-module (language cps2 utils) + #:use-module (language cps intmap) + #:use-module (language cps intset) + #:use-module (language cps primitives) + #:use-module (srfi srfi-11) + #:export (verify)) + +(define (intset-pop set) + (match (intset-next set) + (#f (values set #f)) + (i (values (intset-remove set i) i)))) + +(define-syntax-rule (make-worklist-folder* seed ...) + (lambda (f worklist seed ...) + (let lp ((worklist worklist) (seed seed) ...) + (call-with-values (lambda () (intset-pop worklist)) + (lambda (worklist i) + (if i + (call-with-values (lambda () (f i seed ...)) + (lambda (i* seed ...) + (let add ((i* i*) (worklist worklist)) + (match i* + (() (lp worklist seed ...)) + ((i . i*) (add i* (intset-add worklist i))))))) + (values seed ...))))))) + +(define worklist-fold* + (case-lambda + ((f worklist seed) + ((make-worklist-folder* seed) f worklist seed)))) + +(define (check-distinct-vars conts) + (define (adjoin-def var seen) + (when (intset-ref seen var) + (error "duplicate var name" seen var)) + (intset-add seen var)) + (intmap-fold + (lambda (label cont seen) + (match (intmap-ref conts label) + (($ $kargs names vars ($ $continue k src exp)) + (fold1 adjoin-def vars seen)) + (($ $kfun src meta self tail clause) + (adjoin-def self seen)) + (_ seen)) + ) + conts + empty-intset)) + +(define (compute-available-definitions conts kfun) + "Compute and return a map of LABEL->VAR..., where VAR... are the +definitions that are available at LABEL." + (define (adjoin-def var defs) + (when (intset-ref defs var) + (error "var already present in defs" defs var)) + (intset-add defs var)) + + (define (propagate defs succ out) + (let* ((in (intmap-ref defs succ (lambda (_) #f))) + (in* (if in (intset-intersect in out) out))) + (if (eq? in in*) + (values '() defs) + (values (list succ) + (intmap-add defs succ in* (lambda (old new) new)))))) + + (define (visit-cont label defs) + (let ((in (intmap-ref defs label))) + (define (propagate0 out) + (values '() defs)) + (define (propagate1 succ out) + (propagate defs succ out)) + (define (propagate2 succ0 succ1 out) + (let*-values (((changed0 defs) (propagate defs succ0 out)) + ((changed1 defs) (propagate defs succ1 out))) + (values (append changed0 changed1) defs))) + + (match (intmap-ref conts label) + (($ $kargs names vars ($ $continue k src exp)) + (let ((out (fold1 adjoin-def vars in))) + (match exp + (($ $branch kt) (propagate2 k kt out)) + (($ $prompt escape? tag handler) (propagate2 k handler out)) + (_ (propagate1 k out))))) + (($ $kreceive arity k) + (propagate1 k in)) + (($ $kfun src meta self tail clause) + (let ((out (adjoin-def self in))) + (if clause + (propagate1 clause out) + (propagate0 out)))) + (($ $kclause arity kbody kalt) + (if kalt + (propagate2 kbody kalt in) + (propagate1 kbody in))) + (($ $ktail) (propagate0 in))))) + + (worklist-fold* visit-cont + (intset kfun) + (intmap-add empty-intmap kfun empty-intset))) + +(define (intmap-for-each f map) + (intmap-fold (lambda (k v seed) (f k v) seed) map *unspecified*)) + +(define (check-valid-var-uses conts kfun) + (define (adjoin-def var defs) (intset-add defs var)) + (let visit-fun ((kfun kfun) (free empty-intset)) + (define (visit-exp exp bound) + (define (check-use var) + (unless (intset-ref bound var) + (error "unbound var" var))) + (match exp + ((or ($ $const) ($ $prim)) #t) + ;; todo: $closure + (($ $fun kfun) + (visit-fun kfun bound)) + (($ $rec names vars (($ $fun kfuns) ...)) + (let ((bound (fold1 adjoin-def vars bound))) + (for-each (lambda (kfun) (visit-fun kfun bound)) kfuns))) + (($ $values args) + (for-each check-use args)) + (($ $call proc args) + (check-use proc) + (for-each check-use args)) + (($ $callk k proc args) + (check-use proc) + (for-each check-use args)) + (($ $branch kt ($ $values (arg))) + (check-use arg)) + (($ $branch kt ($ $primcall name args)) + (for-each check-use args)) + (($ $primcall name args) + (for-each check-use args)) + (($ $prompt escape? tag handler) + (check-use tag)))) + (intmap-for-each + (lambda (label bound) + (let ((bound (intset-union free bound))) + (match (intmap-ref conts label) + (($ $kargs names vars ($ $continue k src exp)) + (visit-exp exp (fold1 adjoin-def vars bound))) + (_ #t)))) + (compute-available-definitions conts kfun)))) + +(define (fold-nested-funs f conts kfun seed) + (intset-fold + (lambda (label seed) + (match (intmap-ref conts label) + (($ $kargs _ _ ($ $continue _ _ ($ $fun label))) + (f label seed)) + (($ $kargs _ _ ($ $continue _ _ ($ $rec _ _ (($ $fun label) ...)))) + (fold1 f label seed)) + (_ seed))) + (compute-function-body conts kfun) + seed)) + +(define (check-label-partition conts kfun) + ;; A continuation can only belong to one function. + (let visit-fun ((kfun kfun) (seen empty-intmap)) + (fold-nested-funs + visit-fun + conts + kfun + (intset-fold + (lambda (label seen) + (intmap-add seen label kfun + (lambda (old new) + (error "label used by two functions" label old new)))) + (compute-function-body conts kfun) + seen)))) + +(define (compute-reachable-labels conts kfun) + (let visit-fun ((kfun kfun) (seen empty-intset)) + (fold-nested-funs visit-fun conts kfun + (intset-union seen (compute-function-body conts kfun))))) + +(define (check-arities conts kfun) + (define (check-arity exp cont) + (define (assert-unary) + (match cont + (($ $kargs (_) (_)) #t) + (_ (error "expected unary continuation" cont)))) + (define (assert-nullary) + (match cont + (($ $kargs () ()) #t) + (_ (error "expected unary continuation" cont)))) + (define (assert-n-ary n) + (match cont + (($ $kargs names vars) + (unless (= (length vars) n) + (error "expected n-ary continuation" n cont))) + (_ (error "expected $kargs continuation" cont)))) + (define (assert-kreceive-or-ktail) + (match cont + ((or ($ $kreceive) ($ $ktail)) #t) + (_ (error "expected $kreceive or $ktail continuation" cont)))) + (match exp + ((or ($ $const) ($ $prim) ($ $closure) ($ $fun)) + (assert-unary)) + (($ $rec names vars funs) + (unless (= (length names) (length vars) (length funs)) + (error "invalid $rec" exp)) + (assert-n-ary (length names)) + (match cont + (($ $kargs names vars*) + (unless (equal? vars* vars) + (error "bound variable mismatch" vars vars*))))) + (($ $values args) + (match cont + (($ $ktail) #t) + (_ (assert-n-ary (length args))))) + (($ $call proc args) + (assert-kreceive-or-ktail)) + (($ $callk k proc args) + (assert-kreceive-or-ktail)) + (($ $branch kt exp) + (assert-nullary) + (match (intmap-ref conts kt) + (($ $kargs () ()) #t) + (cont (error "bad kt" cont)))) + (($ $primcall name args) + (match cont + (($ $kargs names) + (match (prim-arity name) + ((out . in) + (unless (= in (length args)) + (error "bad arity to primcall" name args in)) + (unless (= out (length names)) + (error "bad return arity from primcall" name names out))))) + (($ $kreceive) + (when (false-if-exception (prim-arity name)) + (error "primitive should continue to $kargs, not $kreceive" name))) + (($ $ktail) + (unless (eq? name 'return) + (when (false-if-exception (prim-arity name)) + (error "primitive should continue to $kargs, not $ktail" name)))))) + (($ $prompt escape? tag handler) + (assert-nullary) + (match (intmap-ref conts handler) + (($ $kreceive) #t) + (cont (error "bad handler" cont)))))) + (let ((reachable (compute-reachable-labels conts kfun))) + (intmap-for-each + (lambda (label cont) + (when (intset-ref reachable label) + (match cont + (($ $kargs names vars ($ $continue k src exp)) + (unless (= (length names) (length vars)) + (error "broken $kargs" label names vars)) + (check-arity exp (intmap-ref conts k))) + (_ #t)))) + conts))) + +(define (check-functions-bound-once conts kfun) + (let ((reachable (compute-reachable-labels conts kfun))) + (define (add-fun fun functions) + (when (intset-ref functions fun) + (error "function already bound" fun)) + (intset-add functions fun)) + (intmap-fold + (lambda (label cont functions) + (if (intset-ref reachable label) + (match cont + (($ $kargs _ _ ($ $continue _ _ ($ $fun kfun))) + (add-fun kfun functions)) + (($ $kargs _ _ ($ $continue _ _ ($ $rec _ _ (($ $fun kfuns) ...)))) + (fold1 add-fun kfuns functions)) + (_ functions)) + functions)) + conts + empty-intset))) + +(define (verify conts) + (check-distinct-vars conts) + (check-label-partition conts 0) + (check-valid-var-uses conts 0) + (check-arities conts 0) + (check-functions-bound-once conts 0) + conts)