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