Adds randomized tests for Racket VM model
This commit is contained in:
parent
7f0e712dab
commit
e9a909a504
|
@ -1201,6 +1201,8 @@ path/s is either such a string or a list of them.
|
|||
"collects/redex/examples/r6rs/r6rs-tests.rkt" drdr:command-line (mzc *)
|
||||
"collects/redex/examples/r6rs/racket-vs-redex.rkt" drdr:timeout 180
|
||||
"collects/redex/examples/r6rs/show-examples.rkt" drdr:command-line (mzc *)
|
||||
"collects/redex/examples/racket-machine/examples.rkt" drdr:command-line (gracket * "--no-pop-ups")
|
||||
"collects/redex/examples/racket-machine/randomized-tests.rkt" drdr:command-line (racket "-t" * "-m") drdr:timeout 300
|
||||
"collects/redex/examples/racket-machine/reduction-test.rkt" drdr:command-line (mzc *)
|
||||
"collects/redex/examples/racket-machine/verification-test.rkt" drdr:command-line (mzc *)
|
||||
"collects/redex/examples/semaphores.rkt" drdr:command-line (mzc *)
|
||||
|
|
93
collects/redex/examples/racket-machine/examples.rkt
Normal file
93
collects/redex/examples/racket-machine/examples.rkt
Normal file
|
@ -0,0 +1,93 @@
|
|||
#lang racket
|
||||
|
||||
(require (only-in "reduction.rkt" -> load)
|
||||
(only-in "verification.rkt" bytecode-ok?)
|
||||
(only-in "model-impl.rkt" compile-bytecode impl->model)
|
||||
redex
|
||||
rackunit)
|
||||
|
||||
;; eval: e ((x e) ...) -> (listof result)
|
||||
;; Evaluates a bytecode program.
|
||||
;; result ::= v | closure | stuck
|
||||
(define (eval expr [cycles '()])
|
||||
(map (match-lambda
|
||||
[`((clos ,_) ,_ ,_ ,_ ()) (closure)]
|
||||
[`(,v ,_ ,_ ,_ ()) v]
|
||||
[`(,_ ,_ ,_ ,_ (,_ ,_ ...)) (stuck)]
|
||||
['error (error)])
|
||||
(let ([seen (make-hash)]
|
||||
[finals '()])
|
||||
(let loop ([state (program expr cycles)])
|
||||
(unless (hash-ref seen state #f)
|
||||
(hash-set! seen state #t)
|
||||
(let ([succs (apply-reduction-relation -> state)])
|
||||
(if (null? succs)
|
||||
(set! finals (cons state finals))
|
||||
(map loop succs)))))
|
||||
finals)))
|
||||
|
||||
(define (program expr cycles)
|
||||
(term (load ,expr ,cycles)))
|
||||
|
||||
(struct closure () #:transparent)
|
||||
(struct stuck () #:transparent)
|
||||
(struct error () #:transparent)
|
||||
|
||||
(check-equal? (eval '(application (proc-const (val) (loc 0)) 'y))
|
||||
'('y))
|
||||
(check-equal? (eval '(application (indirect x) 'y) '((x (proc-const (val) (loc 0)))))
|
||||
'('y))
|
||||
(check-equal? (eval '(proc-const (val) (loc 0)))
|
||||
(list (closure)))
|
||||
(check-equal? (eval '(application (proc-const (val) (loc 0))))
|
||||
(list (error)))
|
||||
(define bug-#3
|
||||
'(let-one (proc-const (val) (loc 0))
|
||||
(application
|
||||
(loc-noclr 1)
|
||||
(install-value 1 (proc-const (val) 'x)
|
||||
'y))))
|
||||
(let ([sorted (λ (xs) (sort xs string<=? #:key (curry format "~s")))])
|
||||
(check-pred (negate bytecode-ok?) bug-#3)
|
||||
(check-equal? (sorted (eval bug-#3)) '('x 'y)))
|
||||
|
||||
(define (trace expr [cycles '()])
|
||||
(traces -> (program expr cycles)))
|
||||
(define (step expr [cycles '()])
|
||||
(stepper -> (program expr cycles)))
|
||||
|
||||
(when (let ([pop-ups? #t])
|
||||
(command-line
|
||||
#:once-any
|
||||
["--no-pop-ups"
|
||||
"Avoid opening the `traces' and `stepper' windows"
|
||||
(set! pop-ups? #f)])
|
||||
pop-ups?)
|
||||
(trace bug-#3)
|
||||
(step bug-#3))
|
||||
|
||||
;; racket->bytecode: syntax -> (e ((x e) ...))
|
||||
;; Compiles a Racket expression into bytecode.
|
||||
(define racket->bytecode
|
||||
(compose impl->model compile-bytecode))
|
||||
|
||||
(define a-racket-program
|
||||
#'(let ([cons (λ (x y) (λ (s) (s x y)))]
|
||||
[car (λ (p) (p (λ (x y) x)))]
|
||||
[cdr (λ (p) (p (λ (x y) y)))]
|
||||
[null #f]
|
||||
[null? (λ (x) (if x #f #t))])
|
||||
(letrec ([find (lambda (it? xs)
|
||||
(if (null? xs)
|
||||
#f
|
||||
(let ([x (car xs)])
|
||||
(if (it? x)
|
||||
x
|
||||
(find it? (cdr xs))))))])
|
||||
(find (λ (x) x) (cons #f (cons #f (cons 1 (cons 2 null))))))))
|
||||
|
||||
;; If this test fails, it's probably because the compiler has changed
|
||||
;; and no longer maps this program into the subset supported in the
|
||||
;; model. Try the version bundled with Redex (see the README).
|
||||
(match-let ([(cons expr cycles) (racket->bytecode a-racket-program)])
|
||||
(check-equal? (eval expr cycles) '(1)))
|
51
collects/redex/examples/racket-machine/impl-eval.rkt
Normal file
51
collects/redex/examples/racket-machine/impl-eval.rkt
Normal file
|
@ -0,0 +1,51 @@
|
|||
#lang racket
|
||||
|
||||
(require racket/serialize
|
||||
racket/runtime-path
|
||||
compiler/zo-marshal)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
(serializable-struct impl-timeout ())
|
||||
(serializable-struct impl-rejected ())
|
||||
(serializable-struct impl-exception (value))
|
||||
(serializable-struct impl-answer (value))
|
||||
(serializable-struct impl-clos-val ())
|
||||
(serializable-struct impl-undefined-val ())
|
||||
|
||||
(define (eval-impl expr timeout)
|
||||
(let* ([p (zo-marshal expr)]
|
||||
[c (make-channel)]
|
||||
[t (thread
|
||||
(λ ()
|
||||
(parameterize ([read-accept-compiled #t])
|
||||
(channel-put c (with-handlers ([exn:fail? values])
|
||||
(let ([val (eval (read (open-input-bytes p)))])
|
||||
(impl-answer
|
||||
(cond [(procedure? val) (impl-clos-val)]
|
||||
[(eq? (letrec ([x x]) x) val) (impl-undefined-val)]
|
||||
[else val]))))))))])
|
||||
|
||||
(match (sync/timeout timeout c)
|
||||
[(and (? exn:fail?) (exn (regexp #rx"ill-formed code") _))
|
||||
(impl-rejected)]
|
||||
[(exn msg _) (impl-exception msg)]
|
||||
[#f (begin (kill-thread t) (impl-timeout))]
|
||||
[x x])))
|
||||
|
||||
(define-runtime-path impl-exec-path "impl-exec.rkt")
|
||||
|
||||
(define (eval-impl-external expr timeout)
|
||||
(let-values ([(in-in in-out) (make-pipe)]
|
||||
[(out-in out-out) (make-pipe)])
|
||||
(parameterize ([current-input-port in-in]
|
||||
[current-output-port out-out])
|
||||
(write timeout in-out)
|
||||
(write (serialize expr) in-out)
|
||||
(if (system (format "racket -X ~a ~a"
|
||||
(find-executable-path
|
||||
(find-system-path 'exec-file)
|
||||
(find-system-path 'collects-dir))
|
||||
impl-exec-path))
|
||||
(deserialize (read out-in))
|
||||
(error 'eval-impl-external "failed to evaluate ~a" expr)))))
|
9
collects/redex/examples/racket-machine/impl-exec.rkt
Normal file
9
collects/redex/examples/racket-machine/impl-exec.rkt
Normal file
|
@ -0,0 +1,9 @@
|
|||
#lang racket
|
||||
|
||||
(require racket/serialize
|
||||
"impl-eval.rkt")
|
||||
|
||||
(define timeout (read))
|
||||
(define bytecode (deserialize (read)))
|
||||
|
||||
(write (serialize (eval-impl bytecode timeout)))
|
211
collects/redex/examples/racket-machine/model-impl.rkt
Normal file
211
collects/redex/examples/racket-machine/model-impl.rkt
Normal file
|
@ -0,0 +1,211 @@
|
|||
#lang racket
|
||||
|
||||
(require compiler/zo-parse
|
||||
compiler/zo-marshal
|
||||
"impl-eval.rkt")
|
||||
|
||||
(provide (all-defined-out)
|
||||
(all-from-out "impl-eval.rkt"))
|
||||
|
||||
(define (compile-bytecode expr)
|
||||
(let ([tmp (make-temporary-file)])
|
||||
(call-with-output-file tmp #:exists 'truncate
|
||||
(λ (p)
|
||||
(parameterize ([current-namespace (make-base-namespace)])
|
||||
(write (compile expr) p))))
|
||||
(begin0
|
||||
(call-with-input-file tmp zo-parse)
|
||||
(delete-file tmp))))
|
||||
|
||||
(define (impl->model expr)
|
||||
(define cycled (cycle-points expr))
|
||||
(define text-addr (make-hasheq))
|
||||
(define next-loc
|
||||
(let ([suffix 0])
|
||||
(λ ()
|
||||
(set! suffix (add1 suffix))
|
||||
(string->symbol (format "x~s" suffix)))))
|
||||
(define text-seg '())
|
||||
(cons
|
||||
(let recur ([e expr])
|
||||
(match e
|
||||
[(compilation-top _ _ e)
|
||||
(recur e)]
|
||||
[(localref #f n #f #t #f)
|
||||
`(loc ,n)]
|
||||
[(localref #f n #t _ #f)
|
||||
`(loc-clr ,n)]
|
||||
[(localref #f n #f #f #f)
|
||||
`(loc-noclr ,n)]
|
||||
[(localref #t n #f #t #f)
|
||||
`(loc-box ,n)]
|
||||
[(localref #t n #t _ #f)
|
||||
`(loc-box-clr ,n)]
|
||||
[(localref #t n #f #f #f)
|
||||
`(loc-box-noclr ,n)]
|
||||
[(let-one r b #f #f)
|
||||
`(let-one ,(recur r) ,(recur b))]
|
||||
[(let-void n #f b)
|
||||
`(let-void ,n ,(recur b))]
|
||||
[(let-void n #t b)
|
||||
`(let-void-box ,n ,(recur b))]
|
||||
[(install-value 1 n #f r b)
|
||||
`(install-value ,n ,(recur r) ,(recur b))]
|
||||
[(install-value 1 n #t r b)
|
||||
`(install-value-box ,n ,(recur r) ,(recur b))]
|
||||
[(boxenv n b)
|
||||
`(boxenv ,n ,(recur b))]
|
||||
[(application f as)
|
||||
`(application ,(recur f) ,@(map recur as))]
|
||||
[(seq es)
|
||||
`(seq ,@(map recur es))]
|
||||
[(branch c t e)
|
||||
`(branch ,(recur c) ,(recur t) ,(recur e))]
|
||||
[(let-rec rs b)
|
||||
`(let-rec ,(map recur rs) ,(recur b))]
|
||||
[(lam _ _ _ τs #f ns `(val/ref ...) _ b)
|
||||
`(lam ,τs ,(vector->list ns) ,(recur b))]
|
||||
[(closure l _)
|
||||
(define (model-rep)
|
||||
(match-let ([`(lam ,τs () ,b) (recur l)])
|
||||
`(proc-const ,τs ,b)))
|
||||
(if (hash-ref cycled e #f)
|
||||
`(indirect ,(let ([x (hash-ref text-addr e #f)])
|
||||
(or x
|
||||
(let ([x (next-loc)])
|
||||
(hash-set! text-addr e x)
|
||||
(set! text-seg (cons (list x (model-rep)) text-seg))
|
||||
x))))
|
||||
(model-rep))]
|
||||
[(case-lam _ ls)
|
||||
`(case-lam ,@(map recur ls))]
|
||||
[(? void?) 'void]
|
||||
[(? number?) e]
|
||||
[(? boolean?) e]
|
||||
[(? symbol?) `',e]
|
||||
[_ (error 'impl->model "unrecognized form ~s" e)]))
|
||||
text-seg))
|
||||
|
||||
(define (cycle-points expr)
|
||||
(define seen (make-hasheq))
|
||||
(let recur ([e expr])
|
||||
(when (zo? e) ; i.e., not a literal
|
||||
(if (hash-ref seen e #f)
|
||||
(unless (closure? e)
|
||||
(error 'cycle-refs "illegal cycle through ~s" e))
|
||||
(begin
|
||||
(hash-set! seen e #t)
|
||||
(match e
|
||||
[(compilation-top _ _ e)
|
||||
(recur e)]
|
||||
[(localref _ _ _ _ _)
|
||||
(void)]
|
||||
[(let-one r b _ _)
|
||||
(recur r)
|
||||
(recur b)]
|
||||
[(let-void _ _ b)
|
||||
(recur b)]
|
||||
[(install-value _ _ _ r b)
|
||||
(recur r)
|
||||
(recur b)]
|
||||
[(boxenv _ b)
|
||||
(recur b)]
|
||||
[(application f as)
|
||||
(recur f)
|
||||
(for-each recur as)]
|
||||
[(seq es)
|
||||
(for-each recur es)]
|
||||
[(branch c t e)
|
||||
(recur c)
|
||||
(recur t)
|
||||
(recur e)]
|
||||
[(let-rec rs b)
|
||||
(for-each recur rs)
|
||||
(recur b)]
|
||||
[(lam _ _ _ _ _ _ _ _ b)
|
||||
(recur b)]
|
||||
[(closure l _)
|
||||
(recur l)]
|
||||
[(case-lam _ ls)
|
||||
(for-each recur ls)]
|
||||
[_ (void)])))))
|
||||
seen)
|
||||
|
||||
(define (model->impl expr [cycles '()])
|
||||
(let ([cycle-places (make-immutable-hash
|
||||
(map (match-lambda
|
||||
[(cons x _)
|
||||
(cons x (make-placeholder #f))])
|
||||
cycles))])
|
||||
(letrec ([recur (λ (e)
|
||||
(match e
|
||||
[`(loc ,n) (cons (localref #f n #f #t #f) 0)]
|
||||
[`(loc-clr ,n) (cons (localref #f n #t #t #f) 0)]
|
||||
[`(loc-noclr ,n) (cons (localref #f n #f #f #f) 0)]
|
||||
[`(loc-box ,n) (cons (localref #t n #f #t #f) 0)]
|
||||
[`(loc-box-clr ,n) (cons (localref #t n #t #t #f) 0)]
|
||||
[`(loc-box-noclr ,n) (cons (localref #t n #f #f #f) 0)]
|
||||
[`(let-one ,r ,b)
|
||||
(match-let ([(cons rr dr) (recur r)]
|
||||
[(cons rb db) (recur b)])
|
||||
(cons (let-one rr rb #f #f)
|
||||
(add1 (max dr db))))]
|
||||
[`(,(and (or 'let-void 'let-void-box) i) ,n ,b)
|
||||
(match-let ([(cons rb db) (recur b)])
|
||||
(let ([b? (match i ['let-void #f] ['let-void-box #t])])
|
||||
(cons (let-void n b? rb)
|
||||
(+ n db))))]
|
||||
[`(,(and (or 'install-value 'install-value-box) i) ,n ,r ,b)
|
||||
(match-let ([(cons rr dr) (recur r)]
|
||||
[(cons rb db) (recur b)])
|
||||
(let ([b? (match i ['install-value #f] ['install-value-box #t])])
|
||||
(cons (install-value 1 n b? rr rb)
|
||||
(max dr db))))]
|
||||
[`(boxenv ,n ,e)
|
||||
(match-let ([(cons re de) (recur e)])
|
||||
(cons (boxenv n re) de))]
|
||||
[`(application ,f . ,as)
|
||||
(match-let ([`((,rf . ,df) (,ras . ,das) ...)
|
||||
(map recur (cons f as))])
|
||||
(cons (application rf ras)
|
||||
(+ (length as) (apply max df das))))]
|
||||
[`(seq ,e ,es ...)
|
||||
(match-let ([`((,re . ,de) (,res . ,des) ...)
|
||||
(map recur (cons e es))])
|
||||
(cons (seq (cons re res))
|
||||
(apply max de des)))]
|
||||
[`(branch ,c ,t ,f)
|
||||
(match-let ([(cons rc dc) (recur c)]
|
||||
[(cons rt dt) (recur t)]
|
||||
[(cons rf df) (recur f)])
|
||||
(cons (branch rc rt rf)
|
||||
(max dc dt df)))]
|
||||
[`(let-rec (,rs ...) ,b)
|
||||
(match-let ([`((,rrs . 0) ...) (map recur rs)]
|
||||
[(cons rb db) (recur b)])
|
||||
(cons (let-rec rrs rb) db))]
|
||||
[`(lam (,τs ...) (,ns ...) ,b)
|
||||
(match-let ([(cons rb db) (recur b)])
|
||||
(cons (lam (gensym) '()
|
||||
(length τs) τs #f
|
||||
(list->vector ns) (for/list ([_ ns]) 'val/ref)
|
||||
(+ (length τs) (length ns) db) rb)
|
||||
0))]
|
||||
[`(proc-const (,τs ...) ,b)
|
||||
(match-let ([(cons re 0) (recur `(lam ,τs () ,b))])
|
||||
(cons (closure re (gensym)) 0))]
|
||||
[`(case-lam ,cs ...)
|
||||
(match-let ([`((,rcs . 0) ...) (map recur cs)])
|
||||
(cons (case-lam (gensym) rcs) 0))]
|
||||
[`(indirect ,x)
|
||||
(cons (hash-ref cycle-places x) 0)]
|
||||
['void (cons (void) 0)]
|
||||
[else (cons e 0)]))])
|
||||
(match-let ([(cons rep-expr dep-expr) (recur expr)])
|
||||
(for-each
|
||||
(match-lambda
|
||||
[(list x e)
|
||||
(placeholder-set! (hash-ref cycle-places x) (car (recur e)))])
|
||||
cycles)
|
||||
(make-reader-graph
|
||||
(compilation-top dep-expr (prefix 0 '() '()) rep-expr))))))
|
|
@ -0,0 +1,44 @@
|
|||
#lang racket
|
||||
|
||||
(require redex/reduction-semantics "randomized-tests.rkt")
|
||||
|
||||
(let ([r (run (term (application (lam (val) () (loc-noclr 0)) 'x)) (term ()) 100)])
|
||||
(test-equal
|
||||
(and (answer? r)
|
||||
(equal? (answer-value r) ''x))
|
||||
#t))
|
||||
|
||||
(test-predicate
|
||||
cutoff?
|
||||
(run (term (let-void 1 (let-rec ((lam () (0) (application (loc-noclr 0)))) (application (loc-noclr 0))))) (term ()) 100))
|
||||
|
||||
(test-predicate
|
||||
non-conf?
|
||||
(run
|
||||
(term
|
||||
(let-one
|
||||
(lam (val) () (loc-noclr 0))
|
||||
(application
|
||||
(loc-noclr 1)
|
||||
(install-value 1 'non-proc 'x))))
|
||||
(term ())
|
||||
100))
|
||||
|
||||
(test-predicate
|
||||
stuck?
|
||||
(run
|
||||
(term
|
||||
(let-one
|
||||
'x
|
||||
(let-void
|
||||
1
|
||||
(let-rec
|
||||
((lam () (0 1)
|
||||
(branch (loc-noclr 1)
|
||||
(boxenv 1 (application (loc-noclr 0)))
|
||||
'y)))
|
||||
(application (loc-noclr 0))))))
|
||||
(term ())
|
||||
100))
|
||||
|
||||
(test-results)
|
342
collects/redex/examples/racket-machine/randomized-tests.rkt
Normal file
342
collects/redex/examples/racket-machine/randomized-tests.rkt
Normal file
|
@ -0,0 +1,342 @@
|
|||
#lang racket
|
||||
|
||||
(require redex/reduction-semantics
|
||||
(only-in "grammar.rkt" bytecode)
|
||||
(only-in "reduction.rkt" -> load runtime)
|
||||
(only-in "verification.rkt" bytecode-ok?)
|
||||
"model-impl.rkt"
|
||||
compiler/zo-parse compiler/zo-marshal)
|
||||
|
||||
(provide (all-defined-out))
|
||||
|
||||
;; Test the internal properties (verifier totality, safety, and confluence)
|
||||
;; on acyclic expressions. The verifier's totality is tested implicitly by
|
||||
;; treating a "no clauses matched" exception as a test failure.
|
||||
(define (test-internal-properties
|
||||
#:verifier [verified? bytecode-ok?]
|
||||
#:reduction [-> ->]
|
||||
#:prepare [prepare fix]
|
||||
#:steps [steps 100]
|
||||
#:attempts [attempts 5000])
|
||||
(redex-check
|
||||
bytecode e (safe-and-confluent? (term e) (term ()) verified? -> steps)
|
||||
#:prepare prepare
|
||||
#:attempts attempts))
|
||||
|
||||
;; Tests the internal properties on cyclic expressions.
|
||||
(define (test-internal-properties/cycles
|
||||
#:steps [steps 100]
|
||||
#:attempts [attempts 5000]
|
||||
#:print? [print? #t])
|
||||
(redex-check
|
||||
bytecode (side-condition (e (x_0 (name e_0 (proc-const (τ ...) e_0*))) ...)
|
||||
(equal? (term (x_0 ...))
|
||||
(remove-duplicates (term (x_0 ...)))))
|
||||
(safe-and-confluent? (term e) (term ((x_0 e_0) ...)) bytecode-ok? -> steps)
|
||||
#:attempts attempts
|
||||
#:prepare fix-cyclic
|
||||
#:print? print?))
|
||||
|
||||
;; Tests the external properties (the model and implementation agree on
|
||||
;; verification and evaluation questions).
|
||||
(define (test-external-properties
|
||||
#:prepare [prepare (compose optimize fix)]
|
||||
#:model-verifier [model-verified? bytecode-ok?]
|
||||
#:steps [steps 100]
|
||||
#:timeout [timeout 10]
|
||||
#:attempts [attempts 5000]
|
||||
#:print? [print? #t])
|
||||
(redex-check
|
||||
bytecode e
|
||||
(model-impl-consistent? (term e) '() steps timeout model-verified?)
|
||||
#:prepare prepare
|
||||
#:attempts attempts
|
||||
#:print? print?))
|
||||
|
||||
; result = answer | stuck | cutoff | non-conf
|
||||
(define-struct cutoff ())
|
||||
(define-struct stuck (state))
|
||||
(define-struct answer (value))
|
||||
(define-struct non-conf (values))
|
||||
|
||||
; run: e ((x e) ...) nat -> result
|
||||
(define (run e cycles cutoff #:reduction [-> ->])
|
||||
(let ([cache (make-hash)])
|
||||
(let loop ([s (term (load ,e ,cycles))]
|
||||
[c cutoff])
|
||||
(let ([r (hash-ref cache s #f)])
|
||||
(if (and r (>= (car r) c))
|
||||
(cdr r)
|
||||
(begin
|
||||
; If we see this state again while it's marked pending,
|
||||
; it will be with a lesser cutoff, and it will indicate a
|
||||
; cycle in the reduction graph. Without pruning, a cycle
|
||||
; the reduction graph produces a cutoff result; with it
|
||||
; a cylce produces a pending, which is treated identically.
|
||||
(hash-set! cache s (cons c 'pending))
|
||||
(let ([r (cond [(term (halted? ,s))
|
||||
(make-answer
|
||||
(if (eq? s 'error)
|
||||
'error
|
||||
(car s)))]
|
||||
[(zero? c) (make-cutoff)]
|
||||
[else
|
||||
(let ([nexts (map (curryr loop (sub1 c)) (apply-reduction-relation -> s))])
|
||||
(if (null? nexts)
|
||||
(make-stuck s)
|
||||
(or (findf non-conf? nexts)
|
||||
(findf stuck? nexts)
|
||||
(let ([answers (filter answer? nexts)])
|
||||
(if (null? answers)
|
||||
(make-cutoff)
|
||||
(let cmp ([others (cdr answers)])
|
||||
(if (null? others)
|
||||
(car answers)
|
||||
(if (equal? (answer-value (car answers))
|
||||
(answer-value (car others)))
|
||||
(cmp (cdr others))
|
||||
(make-non-conf
|
||||
(list (answer-value (car answers))
|
||||
(answer-value (car others))))))))))))])])
|
||||
(begin
|
||||
(hash-set! cache s (cons c r))
|
||||
r))))))))
|
||||
|
||||
(define (verified/cycles? expr cycles verified?)
|
||||
(and (verified? expr)
|
||||
(andmap (match-lambda [`(,_ ,e) (verified? e)])
|
||||
cycles)))
|
||||
|
||||
(define (safe-and-confluent? expr cycles verified? -> steps)
|
||||
(with-handlers ([exn:fail? (λ (_) #f)])
|
||||
(or (not (verified/cycles? expr cycles verified?))
|
||||
(match (run expr cycles steps #:reduction ->)
|
||||
[(cutoff) #t]
|
||||
[(answer _) #t]
|
||||
[(stuck _) #f]
|
||||
[(non-conf _) #f]))))
|
||||
|
||||
(define (model-impl-consistent? expr cycles steps timeout model-verified?)
|
||||
(define (equiv-results? m i)
|
||||
(match m
|
||||
['uninit #f]
|
||||
[`(box ,_) #f]
|
||||
['undefined (impl-undefined-val? i)]
|
||||
[`(clos ,_) (impl-clos-val? i)]
|
||||
['void (void? i)]
|
||||
[else (equal? m i)]))
|
||||
(with-handlers ([exn:fail? (λ (_) #f)])
|
||||
(let ([model-verified? (verified/cycles? expr cycles model-verified?)]
|
||||
[impl-result (eval-impl-external (model->impl expr cycles) timeout)])
|
||||
(and
|
||||
(if model-verified?
|
||||
(not (impl-rejected? impl-result))
|
||||
(impl-rejected? impl-result))
|
||||
(or (not model-verified?)
|
||||
(match (run expr cycles steps)
|
||||
[(cutoff) #t]
|
||||
[(stuck _) #f]
|
||||
[(non-conf _) #f]
|
||||
[(answer a) (equiv-results?
|
||||
a
|
||||
(match impl-result
|
||||
[(impl-answer v) v]
|
||||
[(impl-exception _) 'error]))]))))))
|
||||
|
||||
;; A reimplementation of the optimizations in the implementation's
|
||||
;; bytecode reader
|
||||
(define (optimize expr)
|
||||
(define value?
|
||||
(let ([v? (redex-match bytecode v)])
|
||||
(λ (e)
|
||||
(or (v? e)
|
||||
(match e
|
||||
[`(proc-const ,_ ,_) #t]
|
||||
[`(lam ,_ ,_ ,_) #t]
|
||||
[`(case-lam ,_ ...) #t]
|
||||
[else #f])))))
|
||||
(define omittable?
|
||||
(match-lambda
|
||||
[`(loc ,_) #t]
|
||||
[`(loc-noclr ,_) #t]
|
||||
[`(loc-box ,_) #t]
|
||||
[`(loc-box-noclr ,_) #t]
|
||||
[`(proc-const ,_ ,_) #t]
|
||||
[`(lam ,_ ,_ ,_) #t]
|
||||
[`(case-lam ,_ ...) #t]
|
||||
[(? (redex-match bytecode v)) #t]
|
||||
[`(branch ,c ,t ,e)
|
||||
(and (omittable? c)
|
||||
(omittable? t)
|
||||
(omittable? e))]
|
||||
[`(let-one ,r ,b)
|
||||
(and (omittable? r)
|
||||
(omittable? b))]
|
||||
[`(,(or 'let-void 'let-void-box)
|
||||
,_
|
||||
(,(or 'install-value 'install-value-box) 0 ,r ,b))
|
||||
(and (omittable? r)
|
||||
(omittable? b))]
|
||||
[`(,(or 'let-void 'let-void-box) ,_ ,b)
|
||||
(omittable? b)]
|
||||
[`(let-rec ,_ ,b)
|
||||
(omittable? b)]
|
||||
[`(application void ,es ...)
|
||||
(andmap omittable? es)]
|
||||
[else #f]))
|
||||
(let recur ([e expr])
|
||||
(match e
|
||||
[`(branch ,c ,t ,e)
|
||||
(let ([c* (recur c)])
|
||||
(if (value? c*)
|
||||
(if c* (recur t) (recur e))
|
||||
`(branch ,c* ,(recur t) ,(recur e))))]
|
||||
[`(seq ,es ...)
|
||||
(letrec ([flatten (λ (es)
|
||||
(foldr (λ (e a)
|
||||
(match e
|
||||
[`(seq ,es ...)
|
||||
(append es a)]
|
||||
[else (cons e a)]))
|
||||
'() es))]
|
||||
; preserves tail position
|
||||
[omit (λ (es kept?)
|
||||
(if (null? es)
|
||||
'()
|
||||
(if (and (omittable? (car es))
|
||||
(not (null? (cdr es))))
|
||||
(omit (cdr es) kept?)
|
||||
(cons (car es) (omit (cdr es) #t)))))])
|
||||
(match (omit (map recur (flatten es)) #f)
|
||||
['() 'void]
|
||||
[`(,e) e]
|
||||
[es `(seq ,@es)]))]
|
||||
[(? list?) (map recur e)]
|
||||
[else e])))
|
||||
|
||||
;; Performs a write-read round trip to see the optimizations performed
|
||||
;; by the implementation's bytecode reader
|
||||
(define (write-read expr)
|
||||
(let-values ([(in out) (make-pipe)]
|
||||
[(tmp) (make-temporary-file)])
|
||||
(zo-marshal-to expr out)
|
||||
(let ([optimized (parameterize ([read-accept-compiled #t])
|
||||
(read in))])
|
||||
(call-with-output-file tmp #:exists 'truncate
|
||||
(λ (p) (write optimized p))))
|
||||
(begin0
|
||||
(call-with-input-file tmp zo-parse)
|
||||
(delete-file tmp))))
|
||||
|
||||
(define-metafunction runtime
|
||||
halted? : p -> b
|
||||
[(halted? (V S H T ())) #t]
|
||||
[(halted? error) #t]
|
||||
[(halted? (V S H T (i_0 i_1 ...))) #f])
|
||||
|
||||
(define random-expr
|
||||
(let ([generator (generate-term bytecode e)])
|
||||
(λ (attempt)
|
||||
(generator (inexact->exact (round (/ (log attempt) (log 5))))))))
|
||||
(define random-value
|
||||
(let ([generator (generate-term bytecode v)])
|
||||
(λ () (generator 3))))
|
||||
(define-syntax-rule (ref-or-else n e e*)
|
||||
(if (zero? n) e* e))
|
||||
|
||||
(define cycle-targets (make-parameter '()))
|
||||
|
||||
;; Makes three classes of corrections:
|
||||
;; 1. replaces out-of-bounds stack offsets with random in-bounds
|
||||
;; ones (without checking that the new target contains an
|
||||
;; appropriate value),
|
||||
;; 2. replaces `ref' argument annotations with `val' annotations
|
||||
;; when the procedure appears in a context that does not allow
|
||||
;; `ref' arguments (but does not alter the procedure's body), and
|
||||
;; 3. replaces `indirect' targets with ones in the `cycle-targets'
|
||||
;; parameter (and replaces the entire `indirect' expression
|
||||
;; with a random value if `cycle-targets' is empty).
|
||||
(define (fix expr)
|
||||
(define (localref? i)
|
||||
(memq i '(loc loc-noclr loc-clr loc-box loc-box-noclr loc-box-clr)))
|
||||
(let recur ([depth 0] [refs? #f] [expr expr])
|
||||
(match expr
|
||||
[`(,(? localref? i) ,n)
|
||||
(ref-or-else depth `(,i ,(modulo n depth)) (random-value))]
|
||||
|
||||
[`(let-one ,e1 ,e2)
|
||||
`(let-one ,(recur (add1 depth) #f e1)
|
||||
,(recur (add1 depth) #f e2))]
|
||||
[`(,(and (or 'let-void 'let-void-box) i) ,n ,e)
|
||||
`(,i ,n ,(recur (+ depth n) #f e))]
|
||||
|
||||
[`(boxenv ,n ,e)
|
||||
(let ([e* (recur depth #f e)])
|
||||
(ref-or-else depth `(boxenv ,(modulo n depth) ,e*) e*))]
|
||||
[`(,(and (or 'install-value 'install-value-box) i) ,n ,e1 ,e2)
|
||||
(let ([e1* (recur depth #f e1)]
|
||||
[e2* (recur depth #f e2)])
|
||||
(ref-or-else depth `(,i ,(modulo n depth) ,e1* ,e2*) `(seq ,e1* ,e2*)))]
|
||||
|
||||
[`(application ,e ,es ...)
|
||||
(let ([m (length es)])
|
||||
`(application
|
||||
,(recur depth #t e)
|
||||
,@(map (curry recur (+ depth m) #f) es)))]
|
||||
[`(,(and (or 'branch 'seq) i) ,es ...)
|
||||
`(,i ,@(map (curry recur depth #f) es))]
|
||||
[`(let-rec (,ls ...) ,e)
|
||||
(let ([n (min depth (length ls))]
|
||||
[ls* (map (curry recur depth #f) ls)])
|
||||
`(let-rec ,(map (curry recur depth #f) (take ls* n))
|
||||
,(recur depth #f e)))]
|
||||
[`(indirect ,c)
|
||||
(cond [(memq c (cycle-targets))
|
||||
`(indirect ,c)]
|
||||
[(not (null? (cycle-targets)))
|
||||
`(indirect ,(list-ref (cycle-targets) (random (length (cycle-targets)))))]
|
||||
[else
|
||||
(random-value)])]
|
||||
[`(proc-const (,τs ...) ,e)
|
||||
(let ([n (length τs)])
|
||||
`(proc-const ,(if refs? τs (build-list n (λ (_) 'val)))
|
||||
,(recur n #f e)))]
|
||||
[`(case-lam ,ls ...)
|
||||
`(case-lam ,@(map (curry recur depth #f) ls))]
|
||||
[`(lam (,τs ...) (,ns ...) ,e)
|
||||
(let ([m (length τs)])
|
||||
`(lam ,(if refs? τs (build-list m (λ (_) 'val)))
|
||||
,(if (zero? depth)
|
||||
'()
|
||||
(map (curryr modulo depth) ns))
|
||||
,(recur (+ m (if (zero? depth) 0 (length ns))) #f e)))]
|
||||
[(? number?) expr]
|
||||
['void expr]
|
||||
[`(quote ,_) expr]
|
||||
[(? boolean?) expr])))
|
||||
|
||||
(define fix-cyclic
|
||||
(match-lambda
|
||||
[`(,e (,xs ,es) ...)
|
||||
(parameterize ([cycle-targets xs])
|
||||
(cons (fix e)
|
||||
(map (λ (x e) (list x (fix e)))
|
||||
xs es)))]))
|
||||
|
||||
;; Replaces all `indirect' expressions with random values
|
||||
(define no-indirects
|
||||
(match-lambda
|
||||
[`(indirect ,_) (random-value)]
|
||||
[(? list? l) (map no-indirects l)]
|
||||
[e e]))
|
||||
|
||||
(define (main)
|
||||
(define-syntax-rule (test t k)
|
||||
(match t
|
||||
[#t k]
|
||||
[(counterexample p)
|
||||
(pretty-print p)
|
||||
(exit 1)]))
|
||||
(test (time (test-internal-properties/cycles #:attempts 4000 #:print? #f))
|
||||
(test (time (test-external-properties #:attempts 250 #:print? #f))
|
||||
(void))))
|
Loading…
Reference in New Issue
Block a user