1#lang racket
2
3(require "grammar.rkt"
4         "reduce.rkt"
5         (except-in redex/reduction-semantics plug)
6         racket/runtime-path)
7
8(provide (all-defined-out))
9
10(module+ main (apply main (vector->list (current-command-line-arguments))))
11(module+ test
12  (main "--rules" "2250" "--size" "3")
13  (module config info
14    (define timeout 240)
15    (define random? #t)))
16
17(define (main . args)
18  (define from-grammar-tests #f)
19  (define from-rules-tests #f)
20
21  (define seed (add1 (random (sub1 (expt 2 31)))))
22
23  (define size #f)
24  (define attempt->size default-attempt-size)
25
26  (define repetitions 1)
27
28  (printf "seed: ~s\n" seed) (flush-output)
29
30  (command-line
31   #:argv args
32   #:once-each
33   ["--grammar"
34    n
35    "Perform n tests generated from the grammar for programs"
36    (set! from-grammar-tests (string->number n))]
37   ["--rules"
38    n
39    "Perform n tests generated from the reduction relation"
40    (set! from-rules-tests (string->number n))]
41   ["--seed"
42    n
43    "Generate tests using the PRG seed n"
44    (set! seed (string->number n))]
45   ["--size"
46    n
47    "Generate tests of size at most n"
48    (set! size (string->number n))
49    (set! attempt->size (const size))]
50   ["--log"
51    p
52    "Log generated tests to path p"
53    (log-test (curryr pretty-write (open-output-file p #:exists 'truncate)))]
54   ["--repetitions"
55    n
56    "Repeats the command n times"
57    (set! repetitions (string->number n))])
58
59
60  (for ([_ (in-range 0 repetitions)])
61
62    (printf "Test seed: ~a (size: ~a)\n" seed (or size "variable"))
63    (parameterize ([current-pseudo-random-generator test-prg])
64      (random-seed seed))
65
66    (parameterize ([redex-pseudo-random-generator test-prg])
67      (when from-grammar-tests
68        (time (test #:attempts from-grammar-tests #:attempt-size attempt->size)))
69      (when from-rules-tests
70        (time (test #:source :-> #:attempts from-rules-tests #:attempt-size attempt->size))))))
71
72(define log-test (make-parameter void))
73
74(define-syntax-rule (test . kw-args)
75  (redex-check grammar p (begin ((log-test) (term p)) (same-behavior? (term p)))
76               #:prepare fix-prog . kw-args))
77
78(define fix-prog
79  (match-lambda
80    [`(<> ,s ,_ ,e)
81     (match-let ([`([,xs ,vs] ...) (remove-duplicates s #:key first)])
82       `(<> ,(map list xs (map (fix-expr xs) vs)) [] ,((fix-expr xs) e)))]))
83
84(define (fix-expr top-vars)
85  (define rewrite
86    (compose drop-duplicate-binders
87             proper-wcms
88             proper-conts
89             consistent-dws
90             (curry close top-vars '())))
91  ; Must call proper-wcm after proper-conts because the latter
92  ; exposes opportunities to the former.
93  ;
94  ; (% 1
95  ;    (cont 1
96  ;          (wcm ([2 3])
97  ;               (% 1
98  ;                  (wcm ([2 4])
99  ;                       hole)
100  ;                  (λ (x) x))))
101  ;   (λ (x) x))
102  ;
103  ; But proper-conts sometimes cannot do its job until proper-wcms
104  ; turns an arbitrary context into an evaluation context.
105  ;
106  ; (% 1
107  ;  (cont 1
108  ;        (wcm ([2 3])
109  ;             (wcm ([2 4])
110  ;                  (% 1 hole (λ (x) x)))))
111  ;  (λ (x) x))
112  ;
113  ; It might work to make proper-conts work in more contexts,
114  ; but it's easier to iterate the rules to a fixed point (and
115  ; there may be more dependencies that require iteration anyway).
116  (λ (e)
117    (let loop ([e e])
118      (define e’ (rewrite e))
119      (if (equal? e e’) e (loop e’)))))
120
121(struct error (cause) #:transparent)
122(struct answer (output result) #:transparent)
123(struct bad-test (reason) #:transparent)
124(struct timeout ())
125
126(define (same-behavior? prog)
127  (let ([impl-behavior (timeout-kill 15 (impl-eval (impl-program (transform-intermediate prog))))])
128    (or (bad-test? impl-behavior)
129        (timeout? impl-behavior)
130        (let ([model-behavior (timeout-warn 30 (model-eval prog) (pretty-write prog))])
131          (or (timeout? model-behavior)
132              (if (error? impl-behavior)
133                  (error? model-behavior)
134                  (and (answer? model-behavior)
135                       (equal? impl-behavior model-behavior))))))))
136
137(define impl-program
138  (match-lambda
139    [`(<> ,s [] ,e)
140     `(let* ([previous-error #f]
141             [result
142              (with-handlers ([exn:fail? void])
143                (call-with-exception-handler
144                 (λ (exn)
145                   (when (and (exn:fail? exn) (not previous-error))
146                     (set! previous-error exn))
147                   exn)
148                 (λ () (letrec ,s ,e))))])
149            (if (exn:fail? previous-error)
150                (raise previous-error)
151                result))]
152    [e e]))
153
154(define-runtime-module-path model-impl "model-impl.rkt")
155
156(define impl-eval
157  (let ([ns (make-base-empty-namespace)])
158    (parameterize ([current-namespace ns])
159      (namespace-require 'racket)
160      (namespace-require (resolved-module-path-name model-impl)))
161    (define show
162      (match-lambda
163        [(? procedure?) 'procedure]
164        [(? list? vs) (map show vs)]
165        [v v]))
166    (λ (test)
167      (define output (open-output-string))
168      (define result
169        (with-handlers ([exn:fail?
170                         (match-lambda
171                           [(exn:fail (regexp "%: expected argument of type <non-procedure>") _)
172                            (bad-test "procedure as tag")]
173                           [(exn:fail m _)
174                            (error m)])])
175          (parameterize ([current-output-port output])
176            (eval test ns))))
177      (if (or (error? result) (bad-test? result))
178          result
179          (answer (get-output-string output)
180                  (show result))))))
181
182(define model-eval-steps (make-parameter +inf.0))
183
184(define (model-eval prog)
185  (let/ec return
186    (define show
187      (match-lambda
188        [(? number? n) n]
189        [(? boolean? b) b]
190        [`(list . ,vs) (map show vs)]
191        [v 'procedure]))
192    (define (eval prog steps)
193      (define ns (set))
194      (let recur ([p prog] [d steps] [s (set)])
195        (define qs (apply-reduction-relation :-> p))
196        (if (empty? qs)
197            (set! ns (set-add ns p))
198            (if (< d 0)
199                (return (timeout))
200                (for ([q qs])
201                     (if (set-member? s q)
202                         (return (timeout))
203                         (recur q (sub1 d) (set-add s p)))))))
204      (set-map ns values))
205    (match (eval prog (model-eval-steps))
206      [(list (and p `(<> ,_ ,output ,result)))
207       (if (v? result)
208           (answer
209            (apply string-append (map (curry format "~v") output))
210            (show result))
211           (error p))])))
212
213(define (with-timeout thunk timeout on-timeout)
214  (let ([c (make-channel)])
215    (struct raised (value))
216    (let ([t (thread
217              (λ ()
218                (channel-put
219                 c (with-handlers ([exn:fail? raised])
220                     (thunk)))))])
221      (match (sync/timeout timeout c)
222        [#f (on-timeout t c)]
223        [(raised v) (raise v)]
224        [x x]))))
225
226(define-syntax-rule (timeout-kill time expr)
227  (with-timeout (λ () expr) time
228                (λ (t _)
229                  (kill-thread t)
230                  (timeout))))
231(define-syntax-rule (timeout-warn time expr warn)
232  (with-timeout (λ () expr) time
233                (λ (_ c)
234                  warn
235                  (sync c))))
236
237(define (close top-vars loc-vars expr)
238  (match expr
239    [(? x? x)
240     (let ([bound (append top-vars loc-vars)])
241       (cond [(memq x bound) x]
242             [(not (empty? bound))
243              (random-member bound)]
244             [else (random-literal)]))]
245    [`(set! ,x ,e)
246     (define e’ (close top-vars loc-vars e))
247     (cond [(memq x top-vars)
248            `(set! ,x ,e’)]
249           [(empty? top-vars) e’]
250           [else `(set! ,(random-member top-vars) ,e’)])]
251    [`(λ ,xs ,e)
252     `(λ ,xs
253        ,(close (filter (negate (curryr member xs)) top-vars)
254                (append xs loc-vars)
255                e))]
256    [`(dw ,x ,e_1 ,e_2 ,e_3)
257     ; Local variables are substituted away in realistic pre-
258     ; and post-thunks. This invariant is important to
259     ; `consistent-dws', which copies such thunks into different
260     ; scopes.
261     `(dw ,x
262          ,(close top-vars '() e_1)
263          ,(close top-vars loc-vars e_2)
264          ,(close top-vars '() e_3))]
265    ; substitution does not recur inside continuation values
266    ; (not sure why it bothers to recur within dw expression)
267    [`(cont ,v ,E)
268     `(cont ,(close top-vars '() v)
269            ,(close top-vars '() E))]
270    [`(cont ,E)
271     `(comp ,(close top-vars '() E))]
272    [(? list?)
273     (map (curry close top-vars loc-vars) expr)]
274    [_ expr]))
275
276(define drop-duplicate-binders
277  (match-lambda
278    [`(λ ,xs ,e)
279     `(λ ,(remove-duplicates xs) ,(drop-duplicate-binders e))]
280    [(? list? es)
281     (map drop-duplicate-binders es)]
282    [e e]))
283
284(define (consistent-dws p)
285  (define pre-post
286    (let ([h (make-hash)])
287      (λ (id pre post)
288        (match (hash-ref h id #f)
289          [#f
290           (hash-set! h id (list pre post))
291           (list pre post)]
292          [x x]))))
293  (let recur ([x p] [excluded '()])
294    (match x
295      [`(dw ,x ,e1 ,e2 ,e3)
296       (if (member x excluded)
297           (recur e2 excluded)
298           (match-let ([(list e1’ e3’) (pre-post x e1 e3)])
299             `(dw ,x
300                  ,(recur e1’ (cons x excluded))
301                  ,(recur e2 excluded)
302                  ,(recur e3’ (cons x excluded)))))]
303      [(? list?) (map (curryr recur excluded) x)]
304      [_ x])))
305
306(define (proper-wcms e)
307  ; Performs two tasks:
308  ; 1. drops duplicate cm keys, and
309  ; 2. drops `wcm' frames when the reduction relation
310  ; would not otherwise merge the marks (replacing them
311  ; with `call/cm' requires more care, since the `wcm'
312  ; body may contain a hole).
313  (let fix ([ctxt 'wont-have-wcm] [e e])
314    (define tail
315      (match-lambda
316        [(or 'comp-top 'may-have-wcm) 'may-have-wcm]
317        ['wont-have-wcm 'wont-have-wcm]))
318    (match e
319      [`(wcm ,w ,e)
320       (match ctxt
321         [(or 'comp-top 'wont-have-wcm)
322          `(wcm ,(remove-duplicates (fix 'dont-care w) #:key first)
323                ,(fix 'may-have-wcm e))]
324         ['may-have-wcm
325          (fix 'may-have-wcm e)])]
326      [`(list . ,vs)
327       ; context doesn't matter for values
328       `(list . ,(map (curry fix 'dont-care) vs))]
329      [`(λ ,xs ,e)
330       ; caller's continuation may be marked
331       `(λ ,xs ,(fix 'may-have-wcm e))]
332      [`(cont ,v ,E)
333       ; body will be wrapped in a prompt
334       `(cont ,(fix 'dont-care v) ,(fix 'wont-have-wcm E))]
335      [`(comp ,E)
336       ; comp application merges only top-level marks
337       `(comp ,(fix 'comp-top E))]
338      [`(begin ,e1 ,e2)
339       `(begin ,(fix 'wont-have-wcm e1)
340               ; "begin-v" does not merge marks
341               ,(fix (tail ctxt) e2))]
342      [`(% ,e1 ,e2 ,e3)
343       `(% ,(fix 'wont-have-wcm e1)
344           ; prompt persists until e2 is a value
345           ,(fix 'wont-have-wcm e2)
346           ,(fix 'wont-have-wcm e3))]
347      [`(dw ,x ,e1 ,e2 ,e3)
348       `(dw ,x
349            ,(fix 'wont-have-wcm e1)
350            ; dw persists until e2 is a value
351            ,(fix 'wont-have-wcm e2)
352            ,(fix 'wont-have-wcm e3))]
353      [`(if ,e1 ,e2 ,e3)
354       `(if ,(fix 'wont-have-wcm e1)
355            ; "ift" and "iff" do not merge marks
356            ,(fix (tail ctxt) e2)
357            ,(fix (tail ctxt) e3))]
358      [`(set! ,x ,e)
359       `(set! ,x ,(fix 'wont-have-wcm e))]
360      [(? list?)
361       (map (curry fix 'wont-have-wcm) e)]
362      [_ e])))
363
364(define proper-conts
365  ; Turns (cont v_1 (in-hole E_1 (% v_1 E_2 v_2)))
366  ; into  (cont v_1 (in-hole E_1        E_2     ))
367  ; since no real program can construct the former.
368  ;
369  ; It would be nice to perform this transformation
370  ; by iteratively applying this rewrite rule
371  ;
372  ; (--> (in-hole (name C (cross e)) (cont v_1 (in-hole E_1 (% v_1 E_2 v_2))))
373  ;      (in-hole C (cont v_1 (in-hole E_1 E_2))))
374  ;
375  ; but a Redex bug (PR 11579) prevents that from working.
376  (let ([none (gensym)])
377    (define-metafunction grammar
378      [(fix (cont v E) any)
379       (cont (fix v ,none) (fix E v))]
380
381      [(fix (dw x e_1 E e_2) any)
382       (dw x (fix e_1 ,none) (fix E any) (fix e_2 ,none))]
383      [(fix (wcm w E) any)
384       (wcm (fix w ,none) (fix E any))]
385      [(fix (v ... E e ...) any)
386       ((fix v ,none) ... (fix E any) (fix e ,none) ...)]
387      [(fix (begin E e) any)
388       (begin (fix E any) (fix e ,none))]
389      [(fix (% E e_1 e_2) any)
390       (% (fix E any) (fix e_1 ,none) (fix e_2 ,none))]
391      [(fix (% v e E) any)
392       (% (fix v ,none) (fix e ,none) (fix E any))]
393      [(fix (% any E v) any)
394       (fix E any)]
395      [(fix (% v_1 E v_2) any)
396       (% (fix v_1 ,none) (fix E any) (fix v_2 ,none))]
397      [(fix (set! x E) any)
398       (set! x (fix E any))]
399      [(fix (if E e_1 e_2) any)
400       (if (fix E any) (fix e_1 ,none) (fix e_2 ,none))]
401
402      [(fix (any_1 ...) any_2)
403       ((fix any_1 ,none) ...)]
404      [(fix any_1 any_2)
405       any_1])
406    (λ (expr)
407      (term (fix ,expr ,none)))))
408
409(define transform-intermediate
410  (match-lambda
411    [(and p `(<> ,s ,o ,e))
412     (define fresh (make-fresh p))
413     (define allocated (map first s))
414     (define (alloc-cell prefix)
415       (define cell (fresh prefix))
416       (set! allocated (cons cell allocated))
417       cell)
418     (define capts (alloc-cell "active-cont-capts"))
419     (define dw-frame-locs
420       (let ([locs (make-hash)])
421         (λ (x)
422           (hash-ref
423            locs x
424            (λ () (let ([ys (list (alloc-cell (format "~s-allocated?" x))
425                                  (alloc-cell (format "~s-skip-pre?" x))
426                                  (alloc-cell (format "~s-comp-cont" x)))])
427                    (hash-set! locs x ys)
428                    ys))))))
429     (define transform
430       (match-lambda
431         [`(wcm () ,m)
432          (transform m)]
433         [`(wcm ([,k ,v] . ,w) ,m)
434          `(call/cm ,(transform k) ,(transform v)
435                    (λ () ,(transform `(wcm ,w ,m))))]
436         [(and e `(dw ,x ,e1 ,e2 ,e3))
437          (match-let ([(list a? s? c) (dw-frame-locs x)]
438                      [t (fresh "t")])
439            `((λ (,t)
440                (if ,a?
441                    (begin (if (zero? ,capts) (set! ,s? #t) #f) (,c ,t))
442                    (% 1
443                       (dynamic-wind
444                        (λ ()
445                          (if (zero? ,capts)
446                              (if ,a?
447                                  (if ,s? (set! ,s? #f) ,(transform e1))
448                                  #f)
449                              #f))
450                        (λ ()
451                          ((call/comp
452                            (λ (k)
453                              (begin
454                                (set! ,c k)
455                                (abort 1 k)))
456                            1)))
457                        (λ ()
458                          (if (zero? ,capts)
459                              (if ,a?
460                                  ,(transform e3)
461                                  (set! ,a? #t))
462                              (set! ,a? #t))))
463                       (λ (k) (begin (if (zero? ,capts) (set! ,s? #t) #f) (k ,t))))))
464              (λ () ,(transform e2))))]
465         [`(cont ,v ,E)
466          (let ([x (fresh "v")])
467            `(begin
468               (set! ,capts (+ ,capts 1))
469               ((λ (,x)
470                  (% ,x
471                     ,(transform
472                       (term (plug ,E (call/cc (λ (k) (abort ,x k)) ,x))))
473                     (λ (x) (begin (set! ,capts (+ ,capts -1)) x))))
474                ,(transform v))))]
475         [`(comp ,E)
476          (define numbers
477            (match-lambda
478              [(? integer? n) (list n)]
479              [(? list? l) (append-map numbers l)]
480              [_ (list)]))
481          (define t (add1 (apply max 0 (numbers E))))
482          `(begin
483             (set! ,capts (+ ,capts 1))
484             (% ,t
485                ,(transform
486                  (term (plug ,E (call/comp (λ (k) (abort ,t k)) ,t))))
487                (λ (x) (begin (set! ,capts (+ ,capts -1)) x))))]
488         [`(list ,vs ...)
489          `(list ,@(map transform-value vs))]
490         [(? list? xs)
491          (map transform xs)]
492         [e e]))
493     (define transform-value
494       (match-lambda
495         [(and e (or `(cont ,_ ,_) `(comp ,_)))
496          `(λ (x) (,(transform e) x))]
497         [e (transform e)]))
498     (define e’ (transform e))
499     (define s’ (map (match-lambda [(list x v) (list x (transform-value v))]) s))
500     `(<> ,(map (λ (x) (match (assoc x s’)
501                         [#f (list x #f)]
502                         [(list _ v’) (list x v’)]))
503                allocated)
504          ,o
505          (begin
506            (set! ,capts 0)
507            ,e’))]))
508
509;; The built-in `plug' sometimes chooses the wrong hole.
510(define-metafunction grammar
511  [(plug hole any) any]
512  [(plug (in-hole W (dw x e_1 E e_2)) any)
513   (in-hole W (dw x e_1 (plug E any) e_2))]
514  [(plug (wcm w M) any)
515   (wcm w (plug M any))]
516  [(plug (v ... W e ...) any)
517   (v ... (plug W any) e ...)]
518  [(plug (begin W e) any)
519   (begin (plug W any) e)]
520  [(plug (% W e_1 e_2) any)
521   (% (plug W any) e_1 e_2)]
522  [(plug (% v e W) any)
523   (% v e (plug W any))]
524  [(plug (% v_1 W v_2) any)
525   (% v_1 (plug W any) v_2)]
526  [(plug (set! x W) any)
527   (set! x (plug W any))]
528  [(plug (if W e_1 e_2) any)
529   (if (plug W any) e_1 e_2)])
530
531(define (make-fresh p)
532  (define suffix
533    (let recur ([x p] [s 0])
534      (cond [(symbol? x)
535             (match (regexp-match #rx"_(.+)$" (symbol->string x))
536               [(list _ n) (max s (add1 (string->number n)))]
537               [#f s])]
538            [(pair? x) (recur (cdr x) (recur (car x) s))]
539            [else s])))
540  (λ (prefix)
541    (begin0 (string->symbol (format "~a_~a" prefix suffix))
542            (set! suffix (add1 suffix)))))
543
544(define (random-literal)
545  (random-member
546   '(dynamic-wind abort current-marks cons
547                  -inf.0 +inf.0 -1 0 1 1/3 -1/4 .33 -.25 4-3i 3+4i
548                  call/cc call/comp call/cm
549                  #f #t zero? print + first rest)))
550
551(define (random-member xs)
552  (parameterize ([current-pseudo-random-generator test-prg])
553    (list-ref xs (random (length xs)))))
554
555(define test-prg (make-pseudo-random-generator))
556