From dfe144e3b88393ee64cf91b9ceac20d412305ef5 Mon Sep 17 00:00:00 2001 From: Burke Fetscher Date: Wed, 19 Mar 2014 16:23:34 -0500 Subject: [PATCH] add bug6 to verifier benchmark --- .../redex/examples/benchmark/f.rkt | 25 + .../redex/examples/benchmark/nohup.out | 93 ++++ .../redex/examples/benchmark/rvm/14.diff | 2 +- .../redex/examples/benchmark/rvm/15.diff | 2 +- .../redex/examples/benchmark/rvm/3.diff | 2 +- .../redex/examples/benchmark/rvm/4.diff | 2 +- .../redex/examples/benchmark/rvm/5.diff | 2 +- .../redex/examples/benchmark/rvm/6.diff | 11 + .../examples/benchmark/rvm/verification-6.rkt | 481 ++++++++++++++++++ 9 files changed, 615 insertions(+), 5 deletions(-) create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/f.rkt create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/nohup.out create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/f.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/f.rkt new file mode 100644 index 0000000000..4ac452ca70 --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/f.rkt @@ -0,0 +1,25 @@ +#lang racket + +(require (prefix-in d: "list-machine/list-machine-base.rkt")) + +(define (f make-term) + (define (depth x) + (let loop ([x x]) + (cond + [(list? x) + (if (empty? x) + 0 + (+ 1 (apply max (map loop x))))] + [else 0]))) + (define depths + (build-list 1000 + (λ (i) + (when (zero? (modulo i 20)) + (printf "~a " i) + (flush-output)) + (depth (make-term))))) + (printf "done\n") + (values (/ (apply + depths) (length depths) 1.) + (apply max depths))) + +(f d:generate-enum-term) \ No newline at end of file diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/nohup.out b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/nohup.out new file mode 100644 index 0000000000..c4a6564713 --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/nohup.out @@ -0,0 +1,93 @@ + +------------------------------------------------------------------- +stlc-sub/stlc-sub-1.rkt has the error: forgot the variable case + +Running stlc-sub/stlc-sub-1.rkt.... +Using generator: ordered + +------------------------------------------------------------------- +stlc-sub/stlc-sub-1.rkt has the error: forgot the variable case + +Running stlc-sub/stlc-sub-1.rkt.... +Using generator: grammar + +------------------------------------------------------------------- +stlc-sub/stlc-sub-1.rkt has the error: forgot the variable case + +Running stlc-sub/stlc-sub-1.rkt.... +Using generator: enum + +------------------------------------------------------------------- +stlc-sub/stlc-sub-2.rkt has the error: wrong order of arguments to replace call + +Running stlc-sub/stlc-sub-2.rkt.... +Using generator: ordered + +------------------------------------------------------------------- +stlc-sub/stlc-sub-2.rkt has the error: wrong order of arguments to replace call + +Running stlc-sub/stlc-sub-2.rkt.... +Using generator: grammar + +------------------------------------------------------------------- +stlc-sub/stlc-sub-2.rkt has the error: wrong order of arguments to replace call + +Running stlc-sub/stlc-sub-2.rkt.... +Using generator: enum + +------------------------------------------------------------------- +stlc-sub/stlc-sub-3.rkt has the error: swaps function and argument position in application + +Running stlc-sub/stlc-sub-3.rkt.... +Using generator: ordered + +------------------------------------------------------------------- +stlc-sub/stlc-sub-3.rkt has the error: swaps function and argument position in application + +Running stlc-sub/stlc-sub-3.rkt.... +Using generator: grammar + +------------------------------------------------------------------- +stlc-sub/stlc-sub-3.rkt has the error: swaps function and argument position in application + +Running stlc-sub/stlc-sub-3.rkt.... +Using generator: enum + +------------------------------------------------------------------- +stlc-sub/stlc-sub-4.rkt has the error: variable not fresh enough + +Running stlc-sub/stlc-sub-4.rkt.... +Using generator: ordered + +------------------------------------------------------------------- +stlc-sub/stlc-sub-4.rkt has the error: variable not fresh enough + +Running stlc-sub/stlc-sub-4.rkt.... +Using generator: grammar + +------------------------------------------------------------------- +stlc-sub/stlc-sub-4.rkt has the error: variable not fresh enough + +Running stlc-sub/stlc-sub-4.rkt.... +Using generator: enum + +------------------------------------------------------------------- +stlc-sub/stlc-sub-5.rkt has the error: replace all variables + +Running stlc-sub/stlc-sub-5.rkt.... +Using generator: ordered + +------------------------------------------------------------------- +stlc-sub/stlc-sub-5.rkt has the error: replace all variables + +Running stlc-sub/stlc-sub-5.rkt.... +Using generator: grammar + +------------------------------------------------------------------- +stlc-sub/stlc-sub-5.rkt has the error: replace all variables + +Running stlc-sub/stlc-sub-5.rkt.... +Using generator: enum +worklist: +stlc-sub/stlc-sub-1.rkt: ordered, stlc-sub/stlc-sub-1.rkt: grammar, stlc-sub/stlc-sub-1.rkt: enum, stlc-sub/stlc-sub-2.rkt: ordered, stlc-sub/stlc-sub-2.rkt: grammar, stlc-sub/stlc-sub-2.rkt: enum, stlc-sub/stlc-sub-3.rkt: ordered, stlc-sub/stlc-sub-3.rkt: grammar, stlc-sub/stlc-sub-3.rkt: enum, stlc-sub/stlc-sub-4.rkt: ordered, stlc-sub/stlc-sub-4.rkt: grammar, stlc-sub/stlc-sub-4.rkt: enum, stlc-sub/stlc-sub-5.rkt: ordered, stlc-sub/stlc-sub-5.rkt: grammar, stlc-sub/stlc-sub-5.rkt: enum +all tests finished diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff index 8d3a6892ca..67f3013f7e 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff @@ -16,7 +16,7 @@ > ;; bug 14 > [(closure-intact? (box-nc ṽ_1 ...) (imm ṽ_2 ...)) > (closure-intact? (ṽ_1 ...) (ṽ_2 ...))] -478a484,490 +475a481,487 > (test-equal > (bytecode-ok? > '(let-one 'x diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff index 98b97e8a71..d5d8807c60 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff @@ -13,7 +13,7 @@ < `(case-lam ,@(map (curry recur depth #f) ls))] --- > `(case-lam ,@(map (curry recur depth #t) ls))] -478a481,488 +475a478,485 > (test-equal > (bytecode-ok? > '(let-one 42 diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff index 6dbe67cd82..0a64b78f38 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff @@ -14,7 +14,7 @@ < (where (s_1 γ_1 η_1) (verify* (e_0 e_1 ...) (abs-push n not s) n_l* #f γ η)) --- > (where (s_1 γ_1 η_1) (verify* (e_0 e_1 ...) (abs-push n uninit s) n_l* #f γ η)) -478a479,486 +475a476,483 > (test-equal > (bytecode-ok? > '(application diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff index 90ee697298..c53abfe03a 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff @@ -7,7 +7,7 @@ --- > ;; bug 4 > #;(side-condition (< (term n_p) (term n_l)))] -478a480,485 +475a477,482 > (test-equal > (bytecode-ok? > '(let-one 'x diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/5.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/5.diff index 7183b8509b..c0cb612863 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/5.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/5.diff @@ -7,7 +7,7 @@ --- > ;;bug 5 > ;;(side-condition (<= (term n) (term n_l))) -478a480,487 +475a477,484 > (test-equal > (bytecode-ok? > '(let-void 1 diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff new file mode 100644 index 0000000000..01b96757c7 --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff @@ -0,0 +1,11 @@ +127c127,128 +< (side-condition (term (AND (lam-verified? l s ?) ...)))] +--- +> ;; bug 6 +> #;(side-condition (term (AND (lam-verified? l s ?) ...)))] +474a476,480 +> (test-equal +> (bytecode-ok? +> '(let-one 'x (case-lam (lam (val) () (loc-noclr 34))))) +> #t) +> diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt new file mode 100644 index 0000000000..0c7f4635ab --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt @@ -0,0 +1,481 @@ +#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 γ η) + ;; bug 6 + #;(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))) + (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)))))) + +(test-equal + (bytecode-ok? + '(let-one 'x (case-lam (lam (val) () (loc-noclr 34))))) + #t) + +(define fixed '())