module/language/cps/verify.scm

   1 ;;; Continuation-passing style (CPS) intermediate language (IL)
   2
   3 ;; Copyright (C) 2013, 2014 Free Software Foundation, Inc.
   4
   5 ;;;; This library is free software; you can redistribute it and/or
   6 ;;;; modify it under the terms of the GNU Lesser General Public
   7 ;;;; License as published by the Free Software Foundation; either
   8 ;;;; version 3 of the License, or (at your option) any later version.
   9 ;;;;
  10 ;;;; This library is distributed in the hope that it will be useful,
  11 ;;;; but WITHOUT ANY WARRANTY; without even the implied warranty of
  12 ;;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  13 ;;;; Lesser General Public License for more details.
  14 ;;;;
  15 ;;;; You should have received a copy of the GNU Lesser General Public
  16 ;;;; License along with this library; if not, write to the Free Software
  17 ;;;; Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
  18
  19 ;;; Commentary:
  20 ;;;
  21 ;;;
  22 ;;; Code:
  23
  24 (define-module (language cps verify)
  25   #:use-module (ice-9 match)
  26   #:use-module (srfi srfi-26)
  27   #:use-module (language cps)
  28   #:export (verify-cps))
  29
  30 (define (verify-cps fun)
  31   (define seen-labels (make-hash-table))
  32   (define seen-vars (make-hash-table))
  33
  34   (define (add sym seen env)
  35     (when (hashq-ref seen sym)
  36       (error "duplicate gensym" sym))
  37     (hashq-set! seen sym #t)
  38     (cons sym env))
  39
  40   (define (add-env new seen env)
  41     (if (null? new)
  42         env
  43         (add-env (cdr new) seen (add (car new) seen env))))
  44
  45   (define (add-vars new env)
  46     (unless (and-map exact-integer? new)
  47       (error "bad vars" new))
  48     (add-env new seen-vars env))
  49
  50   (define (add-labels new env)
  51     (unless (and-map exact-integer? new)
  52       (error "bad labels" new))
  53     (add-env new seen-labels env))
  54
  55   (define (check-ref sym seen env)
  56     (cond
  57      ((not (hashq-ref seen sym))
  58       (error "unbound lexical" sym))
  59      ((not (memq sym env))
  60       (error "displaced lexical" sym))))
  61
  62   (define (check-label sym env)
  63     (check-ref sym seen-labels env))
  64
  65   (define (check-var sym env)
  66     (check-ref sym seen-vars env))
  67
  68   (define (check-src src)
  69     (if (and src (not (and (list? src) (and-map pair? src)
  70                            (and-map symbol? (map car src)))))
  71         (error "bad src")))
  72
  73   (define (visit-cont-body cont k-env v-env)
  74     (match cont
  75       (($ $kif kt kf)
  76        (check-label kt k-env)
  77        (check-label kf k-env))
  78       (($ $kreceive ($ $arity ((? symbol?) ...) () (or #f (? symbol?)) () #f) k)
  79        (check-label k k-env))
  80       (($ $kargs (name ...) (sym ...) body)
  81        (unless (= (length name) (length sym))
  82          (error "name and sym lengths don't match" name sym))
  83        (visit-term body k-env (add-vars sym v-env)))
  84       (_
  85        ;; $kclause, $kfun, and $ktail are only ever seen in $fun.
  86        (error "unexpected cont body" cont))))
  87
  88   (define (visit-clause clause k-env v-env)
  89     (match clause
  90       (($ $cont kclause
  91           ($ $kclause
  92              ($ $arity
  93                 ((? symbol? req) ...)
  94                 ((? symbol? opt) ...)
  95                 (and rest (or #f (? symbol?)))
  96                 (((? keyword? kw) (? symbol? kwname) kwsym) ...)
  97                 (or #f #t))
  98              ($ $cont kbody (and body ($ $kargs names syms _)))
  99              alternate))
 100        (for-each (lambda (sym)
 101                    (unless (memq sym syms)
 102                      (error "bad keyword sym" sym)))
 103                  kwsym)
 104        ;; FIXME: It is technically possible for kw syms to alias other
 105        ;; syms.
 106        (unless (equal? (append req opt (if rest (list rest) '()) kwname)
 107                        names)
 108          (error "clause body names do not match arity names" exp))
 109        (let ((k-env (add-labels (list kclause kbody) k-env)))
 110          (visit-cont-body body k-env v-env))
 111        (when alternate
 112          (visit-clause alternate k-env v-env)))
 113       (_
 114        (error "unexpected clause" clause))))
 115
 116   (define (visit-fun fun k-env v-env)
 117     (match fun
 118       (($ $fun (free ...)
 119           ($ $cont kbody
 120              ($ $kfun src meta self ($ $cont ktail ($ $ktail)) clause)))
 121        (when (and meta (not (and (list? meta) (and-map pair? meta))))
 122          (error "meta should be alist" meta))
 123        (for-each (cut check-var <> v-env) free)
 124        (check-src src)
 125        ;; Reset the continuation environment, because Guile's
 126        ;; continuations are local.
 127        (let ((v-env (add-vars (list self) v-env))
 128              (k-env (add-labels (list ktail) '())))
 129          (when clause
 130            (visit-clause clause k-env v-env))))
 131       (_
 132        (error "unexpected $fun" fun))))
 133
 134   (define (visit-expression exp k-env v-env)
 135     (match exp
 136       (($ $void)
 137        #t)
 138       (($ $const val)
 139        #t)
 140       (($ $prim (? symbol? name))
 141        #t)
 142       (($ $fun)
 143        (visit-fun exp k-env v-env))
 144       (($ $call proc (arg ...))
 145        (check-var proc v-env)
 146        (for-each (cut check-var <> v-env) arg))
 147       (($ $callk k* proc (arg ...))
 148        ;; We don't check that k* is in scope; it's actually inside some
 149        ;; other function, probably.  We rely on the transformation that
 150        ;; introduces the $callk to be correct, and the linker to resolve
 151        ;; the reference.
 152        (check-var proc v-env)
 153        (for-each (cut check-var <> v-env) arg))
 154       (($ $primcall (? symbol? name) (arg ...))
 155        (for-each (cut check-var <> v-env) arg))
 156       (($ $values (arg ...))
 157        (for-each (cut check-var <> v-env) arg))
 158       (($ $prompt escape? tag handler)
 159        (unless (boolean? escape?) (error "escape? should be boolean" escape?))
 160        (check-var tag v-env)
 161        (check-label handler k-env))
 162       (_
 163        (error "unexpected expression" exp))))
 164
 165   (define (visit-term term k-env v-env)
 166     (match term
 167       (($ $letk (($ $cont k cont) ...) body)
 168        (let ((k-env (add-labels k k-env)))
 169          (for-each (cut visit-cont-body <> k-env v-env) cont)
 170          (visit-term body k-env v-env)))
 171
 172       (($ $letrec (name ...) (sym ...) (fun ...) body)
 173        (unless (= (length name) (length sym) (length fun))
 174          (error "letrec syms, names, and funs not same length" term))
 175        (let ((v-env (add-vars sym v-env)))
 176          (for-each (cut visit-fun <> k-env v-env) fun)
 177          (visit-term body k-env v-env)))
 178
 179       (($ $continue k src exp)
 180        (check-label k k-env)
 181        (check-src src)
 182        (visit-expression exp k-env v-env))
 183
 184       (_
 185        (error "unexpected term" term))))
 186
 187   (visit-fun fun '() '())
 188   fun)