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-gensyms (make-hash-table))
  32
  33   (define (add sym env)
  34     (if (hashq-ref seen-gensyms sym)
  35         (error "duplicate gensym" sym)
  36         (begin
  37           (hashq-set! seen-gensyms sym #t)
  38           (cons sym env))))
  39
  40   (define (add-env new env)
  41     (if (null? new)
  42         env
  43         (add-env (cdr new) (add (car new) env))))
  44
  45   (define (check-var sym env)
  46     (cond
  47      ((not (hashq-ref seen-gensyms sym))
  48       (error "unbound lexical" sym))
  49      ((not (memq sym env))
  50       (error "displaced lexical" sym))))
  51
  52   (define (check-src src)
  53     (if (and src (not (and (list? src) (and-map pair? src)
  54                            (and-map symbol? (map car src)))))
  55         (error "bad src")))
  56
  57   (define (visit-cont-body cont k-env v-env)
  58     (match cont
  59       (($ $kif kt kf)
  60        (check-var kt k-env)
  61        (check-var kf k-env))
  62       (($ $kreceive ($ $arity ((? symbol?) ...) () (or #f (? symbol?)) () #f) k)
  63        (check-var k k-env))
  64       (($ $kargs ((? symbol? name) ...) ((? symbol? sym) ...) body)
  65        (unless (= (length name) (length sym))
  66          (error "name and sym lengths don't match" name sym))
  67        (visit-term body k-env (add-env sym v-env)))
  68       (_
  69        ;; $kclause, $kentry, and $ktail are only ever seen in $fun.
  70        (error "unexpected cont body" cont))))
  71
  72   (define (visit-clause clause k-env v-env)
  73     (match clause
  74       (($ $cont kclause
  75           ($ $kclause
  76              ($ $arity
  77                 ((? symbol? req) ...)
  78                 ((? symbol? opt) ...)
  79                 (and rest (or #f (? symbol?)))
  80                 (((? keyword? kw) (? symbol? kwname) (? symbol? kwsym)) ...)
  81                 (or #f #t))
  82              ($ $cont kbody (and body ($ $kargs names syms _)))))
  83        (for-each (lambda (sym)
  84                    (unless (memq sym syms)
  85                      (error "bad keyword sym" sym)))
  86                  kwsym)
  87        ;; FIXME: It is technically possible for kw syms to alias other
  88        ;; syms.
  89        (unless (equal? (append req opt (if rest (list rest) '()) kwname)
  90                        names)
  91          (error "clause body names do not match arity names" exp))
  92        (let ((k-env (add-env (list kclause kbody) k-env)))
  93          (visit-cont-body body k-env v-env)))
  94       (_
  95        (error "unexpected clause" clause))))
  96
  97   (define (visit-fun fun k-env v-env)
  98     (match fun
  99       (($ $fun src meta ((? symbol? free) ...)
 100           ($ $cont kbody
 101              ($ $kentry (? symbol? self) ($ $cont ktail ($ $ktail)) clauses)))
 102        (when (and meta (not (and (list? meta) (and-map pair? meta))))
 103          (error "meta should be alist" meta))
 104        (for-each (cut check-var <> v-env) free)
 105        (check-src src)
 106        ;; Reset the continuation environment, because Guile's
 107        ;; continuations are local.
 108        (let ((v-env (add-env (list self) v-env))
 109              (k-env (add-env (list ktail) '())))
 110          (for-each (cut visit-clause <> k-env v-env) clauses)))
 111       (_
 112        (error "unexpected $fun" fun))))
 113
 114   (define (visit-expression exp k-env v-env)
 115     (match exp
 116       (($ $void)
 117        #t)
 118       (($ $const val)
 119        #t)
 120       (($ $prim (? symbol? name))
 121        #t)
 122       (($ $fun)
 123        (visit-fun exp k-env v-env))
 124       (($ $call (? symbol? proc) ((? symbol? arg) ...))
 125        (check-var proc v-env)
 126        (for-each (cut check-var <> v-env) arg))
 127       (($ $callk (? symbol? k*) (? symbol? proc) ((? symbol? arg) ...))
 128        ;; We don't check that k* is in scope; it's actually inside some
 129        ;; other function, probably.  We rely on the transformation that
 130        ;; introduces the $callk to be correct, and the linker to resolve
 131        ;; the reference.
 132        (check-var proc v-env)
 133        (for-each (cut check-var <> v-env) arg))
 134       (($ $primcall (? symbol? name) ((? symbol? arg) ...))
 135        (for-each (cut check-var <> v-env) arg))
 136       (($ $values ((? symbol? arg) ...))
 137        (for-each (cut check-var <> v-env) arg))
 138       (($ $prompt escape? tag handler)
 139        (unless (boolean? escape?) (error "escape? should be boolean" escape?))
 140        (check-var tag v-env)
 141        (check-var handler k-env))
 142       (_
 143        (error "unexpected expression" exp))))
 144
 145   (define (visit-term term k-env v-env)
 146     (match term
 147       (($ $letk (($ $cont (? symbol? k) cont) ...) body)
 148        (let ((k-env (add-env k k-env)))
 149          (for-each (cut visit-cont-body <> k-env v-env) cont)
 150          (visit-term body k-env v-env)))
 151
 152       (($ $letrec ((? symbol? name) ...) ((? symbol? sym) ...) (fun ...) body)
 153        (unless (= (length name) (length sym) (length fun))
 154          (error "letrec syms, names, and funs not same length" term))
 155        (let ((v-env (add-env sym v-env)))
 156          (for-each (cut visit-fun <> k-env v-env) fun)
 157          (visit-term body k-env v-env)))
 158
 159       (($ $continue k src exp)
 160        (check-var k k-env)
 161        (check-src src)
 162        (visit-expression exp k-env v-env))
 163
 164       (_
 165        (error "unexpected term" term))))
 166
 167   (visit-fun fun '() '())
 168   fun)