add vm bug 2 and update counterexamples
This commit is contained in:
Burke Fetscher
parent
a7f0be7165
commit
bb1d23cb1d
|
|
@ -478,10 +478,12 @@
|
||||||
(set! index (add1 index))))))
|
(set! index (add1 index))))))
|
||||||
|
|
||||||
(define fixed '())
|
(define fixed '())
|
||||||
(test-equal
|
|
||||||
(bytecode-ok?
|
(define small-counter-example
|
||||||
'(let-one 'x
|
'(let-one 'x
|
||||||
(let-rec ((lam () (0) (application (loc-noclr 0))))
|
(application (proc-const (val val) (loc 0))
|
||||||
'x)))
|
(loc-noclr 2)
|
||||||
#t)
|
(install-value 2 'y 'z))))
|
||||||
|
|
||||||
|
(test-equal (check small-counter-example) #f)
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -475,11 +475,11 @@
|
||||||
(set! index (add1 index))))))
|
(set! index (add1 index))))))
|
||||||
|
|
||||||
(define fixed '())
|
(define fixed '())
|
||||||
(test-equal
|
|
||||||
(bytecode-ok?
|
(define small-counter-example
|
||||||
'(let-one 42
|
'(let-one 42
|
||||||
(boxenv 0
|
(boxenv 0
|
||||||
(application (case-lam (lam (ref) () (loc-box 0)))
|
(application (case-lam (lam (ref) () (loc-box 0)))
|
||||||
(loc-box 1)))))
|
(loc-box 1)))))
|
||||||
#t)
|
|
||||||
|
|
||||||
|
(test-equal (check small-counter-example) #f)
|
||||||
|
|
|
||||||
|
|
@ -0,0 +1,487 @@
|
||||||
|
#lang racket
|
||||||
|
|
||||||
|
(define the-error "no-error")
|
||||||
|
|
||||||
|
(require redex/reduction-semantics)
|
||||||
|
(require "../../racket-machine/grammar.rkt"
|
||||||
|
"../../racket-machine/util.rkt"
|
||||||
|
(only-in redex/private/generate-term pick-an-index)
|
||||||
|
(only-in "../../racket-machine/randomized-tests.rkt"
|
||||||
|
cycle-targets
|
||||||
|
random-value
|
||||||
|
ref-or-else
|
||||||
|
cutoff
|
||||||
|
answer
|
||||||
|
run))
|
||||||
|
|
||||||
|
(provide (all-defined-out))
|
||||||
|
|
||||||
|
(define (bytecode-ok? e)
|
||||||
|
(not (eq? 'invalid (car (term (verify ,e () 0 #f () () ∅))))))
|
||||||
|
|
||||||
|
(define-extended-language verification
|
||||||
|
bytecode
|
||||||
|
(s (ṽ ...) invalid)
|
||||||
|
(ṽ uninit imm box imm-nc box-nc not)
|
||||||
|
(γ ((n ṽ) ...))
|
||||||
|
(η (n ...))
|
||||||
|
(f (n n (ṽ ...)) ∅)
|
||||||
|
(m n ?))
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
verify : e s n b γ η f -> (s γ η)
|
||||||
|
|
||||||
|
; localrefs
|
||||||
|
[(verify (loc n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l #f γ η f)
|
||||||
|
((ṽ_0 ... ṽ_n ṽ_n+1 ...) γ η)
|
||||||
|
(side-condition (= (length (term (ṽ_0 ...))) (term n)))
|
||||||
|
(side-condition (memq (term ṽ_n) '(imm imm-nc)))]
|
||||||
|
[(verify (loc n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l #t γ η f)
|
||||||
|
((ṽ_0 ... ṽ_n ṽ_n+1 ...) γ η)
|
||||||
|
(side-condition (= (length (term (ṽ_0 ...))) (term n)))
|
||||||
|
(side-condition (memq (term ṽ_n) '(imm imm-nc box box-nc)))]
|
||||||
|
[(verify (loc-box n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l b γ η f)
|
||||||
|
((ṽ_0 ... ṽ_n ṽ_n+1 ...) γ η)
|
||||||
|
(side-condition (= (length (term (ṽ_0 ...))) (term n)))
|
||||||
|
(side-condition (memq (term ṽ_n) '(box box-nc)))]
|
||||||
|
|
||||||
|
[(verify (loc-noclr n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l #f γ η f)
|
||||||
|
((ṽ_0 ... (nc ṽ_n) ṽ_n+1 ...) γ (log-noclr n n_l ṽ_n η))
|
||||||
|
(side-condition (= (length (term (ṽ_0 ...))) (term n)))
|
||||||
|
(side-condition (memq (term ṽ_n) '(imm imm-nc)))]
|
||||||
|
[(verify (loc-noclr n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l #t γ η f)
|
||||||
|
((ṽ_0 ... (nc ṽ_n) ṽ_n+1 ...) γ (log-noclr n n_l ṽ_n η))
|
||||||
|
(side-condition (= (length (term (ṽ_0 ...))) (term n)))
|
||||||
|
(side-condition (memq (term ṽ_n) '(imm imm-nc box box-nc)))]
|
||||||
|
[(verify (loc-box-noclr n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l b γ η f)
|
||||||
|
((ṽ_0 ... box-nc ṽ_n+1 ...) γ (log-noclr n n_l ṽ_n η))
|
||||||
|
(side-condition (= (length (term (ṽ_0 ...))) (term n)))
|
||||||
|
(side-condition (memq (term ṽ_n) '(box box-nc)))]
|
||||||
|
|
||||||
|
[(verify (loc-clr n) (name s (ṽ_0 ... imm ṽ_n+1 ...)) n_l #f γ η f)
|
||||||
|
((ṽ_0 ... not ṽ_n+1 ...) (log-clr n s n_l γ) η)
|
||||||
|
(side-condition (= (length (term (ṽ_0 ...))) (term n)))]
|
||||||
|
[(verify (loc-clr n) (name s (ṽ_0 ... ṽ_n ṽ_n+1 ...)) n_l #t γ η f)
|
||||||
|
((ṽ_0 ... not ṽ_n+1 ...) (log-clr n s n_l γ) η)
|
||||||
|
(side-condition (= (length (term (ṽ_0 ...))) (term n)))
|
||||||
|
(side-condition (memq (term ṽ_n) '(imm box)))]
|
||||||
|
[(verify (loc-box-clr n) (name s (ṽ_0 ... box ṽ_n+1 ...)) n_l b γ η f)
|
||||||
|
((ṽ_0 ... not ṽ_n+1 ...) (log-clr n s n_l γ) η)
|
||||||
|
(side-condition (= (length (term (ṽ_0 ...))) (term n)))]
|
||||||
|
|
||||||
|
; branch
|
||||||
|
[(verify (branch e_c e_t e_e) s n_l b γ η f)
|
||||||
|
((redo-clrs γ_2 (trim s_3 s)) (concat γ_2 γ_3) η_3)
|
||||||
|
(where (s_1 γ_1 η_1) (verify e_c s n_l #f γ η ∅))
|
||||||
|
(where (s_2 γ_2 η_2) (verify e_t (trim s_1 s) 0 b () () f))
|
||||||
|
(where (s_3 γ_3 η_3) (verify e_e (undo-noclrs η_2 (undo-clrs γ_2 (trim s_2 s))) 0 b γ_1 η_1 f))]
|
||||||
|
|
||||||
|
; let-one
|
||||||
|
[(verify (let-one e_r e_b) (ṽ_1 ...) n_l b γ η f)
|
||||||
|
(verify e_b (imm ṽ_1* ...) ,(+ (term n_l) (term 1)) b γ_1 η_1
|
||||||
|
(shift 1 f))
|
||||||
|
(where s_0 (uninit ṽ_1 ...))
|
||||||
|
(where (s_1 γ_1 η_1) (verify e_r s_0 ,(add1 (term n_l)) #f γ η ∅))
|
||||||
|
(where (uninit ṽ_1* ...) (trim s_1 s_0))]
|
||||||
|
|
||||||
|
; seq
|
||||||
|
[(verify (seq e_0 ... e_n) s n_l b γ η f)
|
||||||
|
(verify e_n s_1 n_l b γ_1 η_1 f)
|
||||||
|
(where (s_1 γ_1 η_1) (verify* (e_0 ...) s n_l #t γ η))]
|
||||||
|
|
||||||
|
; application
|
||||||
|
[(verify (application (name e_0 (loc-noclr n)) e_1 ...) s n_l b_i γ η (n_f n_s (ṽ ...)))
|
||||||
|
(verify-self-app (application e_0 e_1 ...) s n_l γ η (n_f n_s (ṽ ...)))
|
||||||
|
(side-condition (= (term n) (+ (term n_f) (length (term (e_1 ...))))))]
|
||||||
|
[(verify (application (lam (τ_0 ...) (n_0 ...) e) e_0 ...) (name s (ṽ_0 ...)) n_l b γ η f)
|
||||||
|
(verify*-ref (e_0 ...) (τ_0 ...) s_1 n_l* γ η)
|
||||||
|
(where n ,(length (term (e_0 ...))))
|
||||||
|
(where n_l* ,(+ (term n) (term n_l)))
|
||||||
|
(where s_1 (abs-push n not s))
|
||||||
|
(side-condition (term (lam-verified? (lam (τ_0 ...) (n_0 ...) e) s_1 ?)))]
|
||||||
|
[(verify (application (proc-const (τ_0 ...) e) e_0 ...) s n_l b γ η f)
|
||||||
|
(verify (application (lam (τ_0 ...) () e) e_0 ...) s n_l b γ η f)]
|
||||||
|
[(verify (application e_0 e_1 ...) (name s (ṽ_0 ...)) n_l b γ η f)
|
||||||
|
(verify* (e_0 e_1 ...) (abs-push n not s) n_l* #f γ η)
|
||||||
|
(where n ,(length (term (e_1 ...))))
|
||||||
|
(where n_l* ,(+ (term n) (term n_l)))]
|
||||||
|
|
||||||
|
; let-void
|
||||||
|
[(verify (let-void n e) (name s (ṽ_0 ...)) n_l b_i γ η f)
|
||||||
|
(verify e (abs-push n uninit s) ,(+ (term n) (term n_l))
|
||||||
|
b_i γ η (shift n f))]
|
||||||
|
[(verify (let-void-box n e) (name s (ṽ_0 ...)) n_l b_i γ η f)
|
||||||
|
(verify e (abs-push n box s) ,(+ (term n) (term n_l))
|
||||||
|
b_i γ η (shift n f))]
|
||||||
|
|
||||||
|
; procedures in arbitrary context
|
||||||
|
[(verify (lam ((name τ val) ...) (n_0 ...) e) s n_l b γ η f)
|
||||||
|
(s γ η)
|
||||||
|
(side-condition (term (lam-verified? (lam (τ ...) (n_0 ...) e) s ?)))]
|
||||||
|
[(verify (proc-const ((name τ val) ...) e) s n_l b γ η f)
|
||||||
|
(verify (lam (τ ...) () e) s n_l b γ η f)]
|
||||||
|
|
||||||
|
; case-lam
|
||||||
|
[(verify (case-lam (name l (lam (val ...) (n ...) e)) ...) s n_l b γ η f)
|
||||||
|
(s γ η)
|
||||||
|
(side-condition (term (AND (lam-verified? l s ?) ...)))]
|
||||||
|
|
||||||
|
; literals
|
||||||
|
[(verify number s n_l b γ η f) (s γ η)]
|
||||||
|
[(verify b s n_l b_i γ η f) (s γ η)]
|
||||||
|
[(verify (quote variable) s n_l b γ η f) (s γ η)]
|
||||||
|
[(verify void s n_l b γ η f) (s γ η)]
|
||||||
|
|
||||||
|
; install-value
|
||||||
|
[(verify (install-value n e_r e_b) s n_l b γ η f)
|
||||||
|
(verify e_b (set imm n s_2) n_l b γ η f)
|
||||||
|
(side-condition (< (term n) (term n_l)))
|
||||||
|
(where (s_1 γ_1 η_1) (verify e_r s n_l #f γ η ∅))
|
||||||
|
(where s_2 (trim s_1 s))
|
||||||
|
(side-condition (term (valid? s_2)))
|
||||||
|
(where uninit (stack-ref n s_2))]
|
||||||
|
[(verify (install-value-box n e_r e_b) (name s (ṽ_0 ...)) n_l b γ η f)
|
||||||
|
(verify e_b s_2 n_l b γ_1 η_1 f)
|
||||||
|
(side-condition (< (term n) (length (term s))))
|
||||||
|
(where (s_1 γ_1 η_1) (verify e_r s n_l #f γ η ∅))
|
||||||
|
(where s_2 (trim s_1 s))
|
||||||
|
(side-condition (term (valid? s_2)))
|
||||||
|
(side-condition (memq (term (stack-ref n s_2)) '(box box-nc)))]
|
||||||
|
|
||||||
|
; boxenv
|
||||||
|
[(verify (boxenv n_p e) (ṽ_0 ... imm ṽ_n+1 ...) n_l b γ η f)
|
||||||
|
(verify e (ṽ_0 ... box ṽ_n+1 ...) n_l b γ η f)
|
||||||
|
(side-condition (= (length (term (ṽ_0 ...))) (term n_p)))
|
||||||
|
(side-condition (< (term n_p) (term n_l)))]
|
||||||
|
|
||||||
|
; let-rec
|
||||||
|
[(verify (let-rec ((name l (lam ((name v val) ...) (n_0 n_1 ...) e_0)) ...) e) (ṽ_0 ... ṽ_n ...) n_l b γ η f)
|
||||||
|
(verify e s_1 n_l b γ η f)
|
||||||
|
(where n ,(length (term (l ...))))
|
||||||
|
(side-condition (= (length (term (ṽ_0 ...))) (term n)))
|
||||||
|
(side-condition (term (AND (same? ṽ_0 uninit) ...)))
|
||||||
|
(side-condition (<= (term n) (term n_l)))
|
||||||
|
(where s_1 (abs-push n imm (ṽ_n ...)))
|
||||||
|
(where (n_i ...) (count-up ,(length (term (l ...)))))
|
||||||
|
(side-condition (term (AND (lam-verified? l s_1 n_i) ...)))]
|
||||||
|
|
||||||
|
; indirect
|
||||||
|
[(verify (indirect x) s n_l b γ η f) (s γ η)]
|
||||||
|
|
||||||
|
; else
|
||||||
|
[(verify e s n_l b γ η f) (invalid γ η)])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
verify* : (e ...) s n_l b γ η -> (s γ η)
|
||||||
|
[(verify* () s n_l b γ η) (s γ η)]
|
||||||
|
[(verify* (e_0 e_1 ...) s n_l b γ η)
|
||||||
|
(verify* (e_1 ...) (trim s_1 s) n_l b γ_1 η_1)
|
||||||
|
(where (s_1 γ_1 η_1) (verify e_0 s n_l b γ η ∅))])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
verify*-ref : (e ...) (τ ...) s n_l γ η -> (s γ η)
|
||||||
|
[(verify*-ref () () s n_l γ η) (s γ η)]
|
||||||
|
[(verify*-ref (e_0 e_1 ...) (val τ_1 ...) s n_l γ η)
|
||||||
|
(verify*-ref (e_1 ...) (τ_1 ...)
|
||||||
|
(trim s_1 s) n_l γ_1 η_1)
|
||||||
|
(where (s_1 γ_1 η_1) (verify e_0 s n_l #f γ η ∅))]
|
||||||
|
[(verify*-ref (e_0 e_1 ...) () s n_l γ η)
|
||||||
|
(verify* (e_0 e_1 ...) s n_l #f γ η)]
|
||||||
|
[(verify*-ref () (τ_0 τ_1 ...) s n_l γ η) (s γ η)]
|
||||||
|
[(verify*-ref ((loc n) e_1 ...) (ref τ_1 ...) s n_l γ η)
|
||||||
|
(verify*-ref (e_1 ...) (τ_1 ...) s_1 n_l γ_1 η_1)
|
||||||
|
; Require the reference to load a box.
|
||||||
|
(where (s_1 γ_1 η_1) (verify (loc-box n) s n_l #f γ η ∅))]
|
||||||
|
[(verify*-ref ((loc-noclr n) e_1 ...) (ref τ_1 ...) s n_l γ η)
|
||||||
|
(verify*-ref (e_1 ...) (τ_1 ...) s_1 n_l γ_1 η_1)
|
||||||
|
; Require the reference to load a box.
|
||||||
|
(where (s_1 γ_1 η_1) (verify (loc-box-noclr n) s n_l #f γ η ∅))]
|
||||||
|
[(verify*-ref ((loc-clr n) e_1 ...) (ref τ_1 ...) s n_l γ η)
|
||||||
|
(verify*-ref (e_1 ...) (τ_1 ...) s_1 n_l γ_1 η_1)
|
||||||
|
; Require the reference to load a box.
|
||||||
|
(where (s_1 γ_1 η_1) (verify (loc-box-clr n) s n_l #f γ η ∅))]
|
||||||
|
[(verify*-ref (e ...) (τ ...) s n_l γ η) (invalid γ η)])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
[(lam-verified? (lam (τ_0 ...) (n_0 ...) e) (name s (ṽ_0 ...)) m)
|
||||||
|
(valid? s_1)
|
||||||
|
(where n_d ,(length (term s)))
|
||||||
|
(where n_d* ,(+ (length (term (τ_0 ...))) (length (term (n_0 ...)))))
|
||||||
|
(side-condition (term (AND (less-than? n_0 n_d) ...)))
|
||||||
|
(side-condition (term (AND (not-member? (stack-ref n_0 s) (uninit not)) ...)))
|
||||||
|
(where (ṽ ...) ((drop-noclr (stack-ref n_0 s)) ...))
|
||||||
|
(where f (extract-self m (n_0 ...) (τ_0 ...) (ṽ ...)))
|
||||||
|
(where (s_1 γ_1 η_1) (verify e (ṽ ... (arg τ_0) ...) n_d* #f () () f))]
|
||||||
|
[(lam-verified? l s m) #f])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
[(extract-self ? (n_0 ...) (τ_0 ...) (ṽ_0 ...)) ∅]
|
||||||
|
[(extract-self n_i (n_0 ... n_i n_i+1 ...) (τ_0 ...) (ṽ_0 ...))
|
||||||
|
(,(length (term (n_0 ...))) ,(length (term (τ_0 ...))) (ṽ_0 ...))
|
||||||
|
; When a closure captures itself multiple times, only the last
|
||||||
|
; occurrence is considered a self-reference.
|
||||||
|
(side-condition (term (not-member? n_i (n_i+1 ...))))]
|
||||||
|
[(extract-self n (n_0 ...) (τ_0 ...) (ṽ_0 ...)) ∅])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
drop-noclr : ṽ -> ṽ
|
||||||
|
[(drop-noclr imm-nc) imm]
|
||||||
|
[(drop-noclr box-nc) box]
|
||||||
|
[(drop-noclr ṽ) ṽ])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
[(verify-self-app (application e_0 e_1 ...) (name s (ṽ_0 ...)) n_l γ η (n_f n_s (ṽ_j ...)))
|
||||||
|
(s_1 γ_1 η_1)
|
||||||
|
(where n ,(length (term (e_1 ...))))
|
||||||
|
(where n_l* ,(+ (term n) (term n_l)))
|
||||||
|
(where (s_1 γ_1 η_1) (verify* (e_0 e_1 ...) (abs-push n not s) n_l* #f γ η))
|
||||||
|
(side-condition (term (valid? s_1)))
|
||||||
|
(where (n_j ...) (count-up ,(length (term (ṽ_j ...)))))
|
||||||
|
(side-condition (term (closure-intact? ((stack-ref (plus n_j n_s) s_1) ...) (ṽ_j ...))))]
|
||||||
|
[(verify-self-app e s n_l γ η f) (invalid γ η)])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
closure-intact? : (ṽ ...) (ṽ ...) -> b
|
||||||
|
[(closure-intact? () ()) #t]
|
||||||
|
[(closure-intact? (imm-nc ṽ_1 ...) (imm ṽ_2 ...))
|
||||||
|
(closure-intact? (ṽ_1 ...) (ṽ_2 ...))]
|
||||||
|
[(closure-intact? (box-nc ṽ_1 ...) (box ṽ_2 ...))
|
||||||
|
(closure-intact? (ṽ_1 ...) (ṽ_2 ...))]
|
||||||
|
[(closure-intact? (ṽ ṽ_1 ...) (ṽ ṽ_2 ...))
|
||||||
|
(closure-intact? (ṽ_1 ...) (ṽ_2 ...))]
|
||||||
|
[(closure-intact? (ṽ_1 ...) (ṽ_2 ...)) #f])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
shift : n f -> f
|
||||||
|
[(shift n ∅) ∅]
|
||||||
|
[(shift n (n_f n_s (ṽ ...)))
|
||||||
|
(,(+ (term n) (term n_f)) ,(+ (term n) (term n_s)) (ṽ ...))])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
arg : τ -> ṽ
|
||||||
|
[(arg val) imm]
|
||||||
|
[(arg ref) box])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
abs-push : n ṽ (ṽ ...) -> s
|
||||||
|
[(abs-push 0 ṽ (ṽ_0 ...)) (ṽ_0 ...)]
|
||||||
|
[(abs-push n ṽ (ṽ_0 ...))
|
||||||
|
(abs-push ,(sub1 (term n)) ṽ (ṽ ṽ_0 ...))])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
stack-ref : n (ṽ ...) -> ṽ
|
||||||
|
[(stack-ref n (ṽ_0 ... ṽ_n ṽ_n+1 ...))
|
||||||
|
ṽ_n
|
||||||
|
(side-condition (= (length (term (ṽ_0 ...))) (term n)))])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
set : ṽ n (ṽ ...) -> (ṽ ...)
|
||||||
|
[(set ṽ n (ṽ_0 ... ṽ_n ṽ_n+1 ...))
|
||||||
|
(ṽ_0 ... ṽ ṽ_n+1 ...)
|
||||||
|
(side-condition (= (length (term (ṽ_0 ...))) (term n)))])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
nc : ṽ -> ṽ
|
||||||
|
[(nc imm) imm-nc]
|
||||||
|
[(nc imm-nc) imm-nc]
|
||||||
|
[(nc box) box-nc]
|
||||||
|
[(nc box-nc) box-nc])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
log-noclr : n n ṽ η -> η
|
||||||
|
[(log-noclr n_p n_l ṽ_p (n_0 ...))
|
||||||
|
(,(- (term n_p) (term n_l)) n_0 ...)
|
||||||
|
(side-condition (>= (term n_p) (term n_l)))
|
||||||
|
(side-condition (memq (term ṽ_p) '(imm box)))]
|
||||||
|
[(log-noclr n_p n_l ṽ_p η) η])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
undo-noclrs : η s -> s
|
||||||
|
[(undo-noclrs η invalid) invalid]
|
||||||
|
[(undo-noclrs () s) s]
|
||||||
|
[(undo-noclrs (n_0 n_1 ...) (ṽ_0 ... imm-nc ṽ_i ...))
|
||||||
|
(undo-noclrs (n_1 ...) (ṽ_0 ... imm ṽ_i ...))
|
||||||
|
(side-condition (= (length (term (ṽ_0 ...))) (term n_0)))]
|
||||||
|
[(undo-noclrs (n_0 n_1 ...) (ṽ_0 ... box-nc ṽ_i ...))
|
||||||
|
(undo-noclrs (n_1 ...) (ṽ_0 ... box ṽ_i ...))
|
||||||
|
(side-condition (= (length (term (ṽ_0 ...))) (term n_0)))]
|
||||||
|
[(undo-noclrs (n_0 n_1 ...) s)
|
||||||
|
(undo-noclrs (n_1 ...) s)])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
log-clr : n s n γ -> γ
|
||||||
|
[(log-clr n_p (name s (ṽ_0 ... ṽ_p ṽ_p+1 ...)) n_l ((n_i ṽ_i) ...))
|
||||||
|
((,(- (- (term n_h) (term n_p)) (term 1)) ṽ_p) (n_i ṽ_i) ...)
|
||||||
|
(where n_h ,(length (term s)))
|
||||||
|
(side-condition (>= (term n_p) (term n_l)))
|
||||||
|
(side-condition (= (length (term (ṽ_0 ...))) (term n_p)))]
|
||||||
|
[(log-clr n_p s n_l γ) γ])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
undo-clrs : γ s -> s
|
||||||
|
[(undo-clrs γ invalid) invalid]
|
||||||
|
[(undo-clrs () s) s]
|
||||||
|
[(undo-clrs ((n_0 ṽ_0) (n_1 ṽ_1) ...) s)
|
||||||
|
(undo-clrs ((n_1 ṽ_1) ...) (set ṽ_0 ,(- (- (term n_h) (term n_0)) (term 1)) s))
|
||||||
|
(where n_h ,(length (term s)))
|
||||||
|
(side-condition (< (term n_0) (term n_h)))]
|
||||||
|
[(undo-clrs ((n_0 ṽ_0) (n_1 ṽ_1) ...) s)
|
||||||
|
(undo-clrs ((n_1 ṽ_1) ...) s)])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
redo-clrs : γ s -> s
|
||||||
|
[(redo-clrs γ invalid) invalid]
|
||||||
|
[(redo-clrs () s) s]
|
||||||
|
[(redo-clrs ((n_0 ṽ_0) (n_1 ṽ_1) ...) s)
|
||||||
|
(redo-clrs ((n_1 ṽ_1) ...) (set not ,(- (- (term n_h) (term n_0)) (term 1)) s))
|
||||||
|
(where n_h ,(length (term s)))
|
||||||
|
;; bug 2
|
||||||
|
#;(side-condition (< (term n_0) (term n_h)))]
|
||||||
|
[(redo-clrs ((n_0 ṽ_0) (n_1 ṽ_1) ...) s)
|
||||||
|
(redo-clrs ((n_1 ṽ_1) ...) s)])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
trim : s s -> s
|
||||||
|
[(trim invalid s) invalid]
|
||||||
|
[(trim (ṽ_1 ... ṽ_2 ...) (ṽ_3 ...))
|
||||||
|
(ṽ_2 ...)
|
||||||
|
(side-condition (= (length (term (ṽ_2 ...))) (length (term (ṽ_3 ...)))))])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
[(valid? invalid) #f]
|
||||||
|
[(valid? (ṽ ...)) #t])
|
||||||
|
|
||||||
|
;; Typsetting tricks:
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
[(AND) #t]
|
||||||
|
[(AND #t any_1 ...) (AND any_1 ...)]
|
||||||
|
[(AND any_0 any_1 ...) #f])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
[(same? any_1 any_1) #t]
|
||||||
|
[(same? any_1 any_2) #f])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
[(less-than? n_1 n_2) ,(< (term n_1) (term n_2))])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
[(plus n_1 n_2) ,(+ (term n_1) (term n_2))])
|
||||||
|
|
||||||
|
(define-metafunction verification
|
||||||
|
[(not-member? any_1 (any_2 ...))
|
||||||
|
,(not (member (term any_1) (term (any_2 ...))))])
|
||||||
|
|
||||||
|
(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 ,(modulo n 20) ,(recur (+ depth (modulo n 20)) #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 (check e0)
|
||||||
|
(define e (fix e0))
|
||||||
|
(or (not e)
|
||||||
|
(not (bytecode-ok? e))
|
||||||
|
(match
|
||||||
|
(with-handlers
|
||||||
|
([exn:fail? (λ (exc)
|
||||||
|
(unless
|
||||||
|
(regexp-match?
|
||||||
|
#"counterexample|domain|clauses"
|
||||||
|
(exn-message exc))
|
||||||
|
(printf "exception on ~s\n~s\n" e
|
||||||
|
(exn-message exc)))
|
||||||
|
#f)])
|
||||||
|
(run e '() 100))
|
||||||
|
[(cutoff) #t]
|
||||||
|
[(answer _) #t]
|
||||||
|
[_ #f])))
|
||||||
|
|
||||||
|
|
||||||
|
(define (generate-M-term)
|
||||||
|
(generate-term bytecode e 5))
|
||||||
|
|
||||||
|
(define (generate-typed-term)
|
||||||
|
(error "not currently implemented for rvm in the benchmark"))
|
||||||
|
|
||||||
|
(define (type-check e)
|
||||||
|
(bytecode-ok? (fix e)))
|
||||||
|
|
||||||
|
(define (typed-generator)
|
||||||
|
(error "not currently implemented for rvm in the benchmark"))
|
||||||
|
|
||||||
|
(define (generate-enum-term)
|
||||||
|
(generate-term bytecode e #:i-th (pick-an-index 0.03)))
|
||||||
|
|
||||||
|
(define (ordered-enum-generator)
|
||||||
|
(let ([index 0])
|
||||||
|
(λ ()
|
||||||
|
(begin0
|
||||||
|
(generate-term bytecode e #:i-th index)
|
||||||
|
(set! index (add1 index))))))
|
||||||
|
|
||||||
|
(define fixed '())
|
||||||
|
|
||||||
|
(define small-counter-example
|
||||||
|
'(proc-const (val)
|
||||||
|
(branch (loc 0)
|
||||||
|
(let-one 'x
|
||||||
|
(branch (loc 1)
|
||||||
|
(loc-clr 0)
|
||||||
|
void))
|
||||||
|
void)))
|
||||||
|
|
||||||
|
(test-equal (check small-counter-example) #f)
|
||||||
|
|
@ -473,11 +473,12 @@
|
||||||
(set! index (add1 index))))))
|
(set! index (add1 index))))))
|
||||||
|
|
||||||
(define fixed '())
|
(define fixed '())
|
||||||
(test-equal
|
|
||||||
(bytecode-ok?
|
(define small-counter-example
|
||||||
'(application
|
'(application
|
||||||
(proc-const (val val) (branch (loc-noclr 0) 'a 'b))
|
(proc-const (val val) (branch (loc-noclr 0) 'a 'b))
|
||||||
'x
|
'x
|
||||||
(install-value 0 'y (boxenv 0 'z))))
|
(install-value 0 'y (boxenv 0 'z))))
|
||||||
#t)
|
|
||||||
|
(test-equal (check small-counter-example) #f)
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -474,9 +474,11 @@
|
||||||
(set! index (add1 index))))))
|
(set! index (add1 index))))))
|
||||||
|
|
||||||
(define fixed '())
|
(define fixed '())
|
||||||
(test-equal
|
|
||||||
(bytecode-ok?
|
(define small-counter-example
|
||||||
'(let-one 'x
|
'(let-one 'x
|
||||||
(branch #f (boxenv 0 'y) (loc-box 0))))
|
(branch #f (boxenv 0 'y) (loc-box 0))))
|
||||||
#t)
|
|
||||||
|
(test-equal (check small-counter-example) #f)
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -474,11 +474,13 @@
|
||||||
(set! index (add1 index))))))
|
(set! index (add1 index))))))
|
||||||
|
|
||||||
(define fixed '())
|
(define fixed '())
|
||||||
(test-equal
|
|
||||||
(bytecode-ok?
|
(define small-counter-example
|
||||||
'(let-void 1
|
'(let-void 1
|
||||||
(branch #f
|
(branch #f
|
||||||
(let-rec ((lam () (0) 'x)) 'y)
|
(let-rec ((lam () (0) 'x)) 'y)
|
||||||
(loc-noclr 0))))
|
(loc-noclr 0))))
|
||||||
#t)
|
|
||||||
|
(test-equal (check small-counter-example) #f)
|
||||||
|
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -473,9 +473,11 @@
|
||||||
(generate-term bytecode e #:i-th index)
|
(generate-term bytecode e #:i-th index)
|
||||||
(set! index (add1 index))))))
|
(set! index (add1 index))))))
|
||||||
|
|
||||||
(test-equal
|
|
||||||
(bytecode-ok?
|
|
||||||
'(let-one 'x (case-lam (lam (val) () (loc-noclr 34)))))
|
|
||||||
#t)
|
|
||||||
|
|
||||||
(define fixed '())
|
(define fixed '())
|
||||||
|
|
||||||
|
(define small-counter-example
|
||||||
|
'(application
|
||||||
|
(case-lam (lam (val) () (loc-noclr 34)))
|
||||||
|
'x))
|
||||||
|
|
||||||
|
(test-equal (check small-counter-example) #f)
|
||||||
Loading…
Reference in New Issue
Block a user