suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

adjust vm correctness property, update diffs

Browse Source
This commit is contained in:
Burke Fetscher 2014-03-20 23:45:46 -05:00
parent bb1d23cb1d
commit 9d70f35ec4
15 changed files with 317 additions and 241 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/14.diff
View File

@ -16,11 +16,13 @@
> ;; bug 14
> [(closure-intact? (box-nc ṽ_1 ...) (imm ṽ_2 ...))
> (closure-intact? (ṽ_1 ...) (ṽ_2 ...))]
475a481,487
> (test-equal
> (bytecode-ok?
> '(let-one 'x
> (let-rec ((lam () (0) (application (loc-noclr 0))))
> 'x)))
> #t)
475a481,489
>
> (define small-counter-example
> '(let-one 'x
> (application (proc-const (val val) (loc 0))
> (loc-noclr 2)
> (install-value 2 'y 'z))))
>
> (test-equal (check small-counter-example) #f)
>

6
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/15.diff
View File

@ -14,11 +14,11 @@
---
> `(case-lam ,@(map (curry recur depth #t) ls))]
475a478,485
> (test-equal
> (bytecode-ok?
>
> (define small-counter-example
> '(let-one 42
> (boxenv 0
> (application (case-lam (lam (ref) () (loc-box 0)))
> (loc-box 1)))))
> #t)
>
> (test-equal (check small-counter-example) #f)

18
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/2.diff Normal file
View File

@ -0,0 +1,18 @@
338c338,339
< (side-condition (< (term n_0) (term n_h)))]
---
> ;; bug 2
> #;(side-condition (< (term n_0) (term n_h)))]
475a477,487
>
> (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)
\ No newline at end of file

9
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/3.diff
View File

@ -14,12 +14,13 @@
< (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 γ η))
475a476,483
> (test-equal
> (bytecode-ok?
475a476,484
>
> (define small-counter-example
> '(application
> (proc-const (val val) (branch (loc-noclr 0) 'a 'b))
> 'x
> (install-value 0 'y (boxenv 0 'z))))
> #t)
>
> (test-equal (check small-counter-example) #f)
>

10
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/4.diff
View File

@ -7,10 +7,12 @@
---
> ;; bug 4
> #;(side-condition (< (term n_p) (term n_l)))]
475a477,482
> (test-equal
> (bytecode-ok?
475a477,484
>
> (define small-counter-example
> '(let-one 'x
> (branch #f (boxenv 0 'y) (loc-box 0))))
> #t)
>
> (test-equal (check small-counter-example) #f)
>
>

10
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/5.diff
View File

@ -7,12 +7,14 @@
---
> ;;bug 5
> ;;(side-condition (<= (term n) (term n_l)))
475a477,484
> (test-equal
> (bytecode-ok?
475a477,486
>
> (define small-counter-example
> '(let-void 1
> (branch #f
> (let-rec ((lam () (0) 'x)) 'y)
> (loc-noclr 0))))
> #t)
>
> (test-equal (check small-counter-example) #f)
>
>

13
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/6.diff
View File

@ -3,9 +3,12 @@
---
> ;; 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)
475a477,483
>
> (define small-counter-example
> '(application
> (case-lam (lam (val) () (loc-noclr 34)))
> 'x))
>
> (test-equal (check small-counter-example) #f)
\ No newline at end of file

42
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-14.rkt
View File

@ -435,49 +435,49 @@
[`(quote ,_) expr]
[(? boolean?) expr])))
(define (check e0)
(define e (fix e0))
(define (check e)
(let/ec fail
(or (not e)
(not (bytecode-ok? e))
(implies (with-handlers ([exn:fail? (λ (exc)
(maybe-log-exn exc e)
(fail #f))])
(bytecode-ok? e))
(match
(with-handlers
([exn:fail? (λ (exc)
(maybe-log-exn exc e)
#f)])
(run e '() 100))
[(cutoff) #t]
[(answer _) #t]
[_ #f])))))
(define (maybe-log-exn exc e)
(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])))
(exn-message exc))))
(define (generate-M-term)
(generate-term bytecode e 5))
(fix (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)))
(bytecode-ok? 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)))
(fix (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
'(let-one 'x
@ -487,3 +487,9 @@
(test-equal (check small-counter-example) #f)
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define fixed '())

42
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-15.rkt
View File

@ -432,49 +432,49 @@
[`(quote ,_) expr]
[(? boolean?) expr])))
(define (check e0)
(define e (fix e0))
(define (check e)
(let/ec fail
(or (not e)
(not (bytecode-ok? e))
(implies (with-handlers ([exn:fail? (λ (exc)
(maybe-log-exn exc e)
(fail #f))])
(bytecode-ok? e))
(match
(with-handlers
([exn:fail? (λ (exc)
(maybe-log-exn exc e)
#f)])
(run e '() 100))
[(cutoff) #t]
[(answer _) #t]
[_ #f])))))
(define (maybe-log-exn exc e)
(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])))
(exn-message exc))))
(define (generate-M-term)
(generate-term bytecode e 5))
(fix (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)))
(bytecode-ok? 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)))
(fix (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
'(let-one 42
@ -483,3 +483,9 @@
(loc-box 1)))))
(test-equal (check small-counter-example) #f)
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define fixed '())

42
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-2.rkt
View File

@ -431,49 +431,49 @@
[`(quote ,_) expr]
[(? boolean?) expr])))
(define (check e0)
(define e (fix e0))
(define (check e)
(let/ec fail
(or (not e)
(not (bytecode-ok? e))
(implies (with-handlers ([exn:fail? (λ (exc)
(maybe-log-exn exc e)
(fail #f))])
(bytecode-ok? e))
(match
(with-handlers
([exn:fail? (λ (exc)
(maybe-log-exn exc e)
#f)])
(run e '() 100))
[(cutoff) #t]
[(answer _) #t]
[_ #f])))))
(define (maybe-log-exn exc e)
(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])))
(exn-message exc))))
(define (generate-M-term)
(generate-term bytecode e 5))
(fix (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)))
(bytecode-ok? 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)))
(fix (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)
@ -485,3 +485,9 @@
void)))
(test-equal (check small-counter-example) #f)
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define fixed '())

42
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-3.rkt
View File

@ -430,49 +430,49 @@
[`(quote ,_) expr]
[(? boolean?) expr])))
(define (check e0)
(define e (fix e0))
(define (check e)
(let/ec fail
(or (not e)
(not (bytecode-ok? e))
(implies (with-handlers ([exn:fail? (λ (exc)
(maybe-log-exn exc e)
(fail #f))])
(bytecode-ok? e))
(match
(with-handlers
([exn:fail? (λ (exc)
(maybe-log-exn exc e)
#f)])
(run e '() 100))
[(cutoff) #t]
[(answer _) #t]
[_ #f])))))
(define (maybe-log-exn exc e)
(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])))
(exn-message exc))))
(define (generate-M-term)
(generate-term bytecode e 5))
(fix (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)))
(bytecode-ok? 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)))
(fix (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
'(application
@ -482,3 +482,9 @@
(test-equal (check small-counter-example) #f)
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define fixed '())

42
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-4.rkt
View File

@ -431,49 +431,49 @@
[`(quote ,_) expr]
[(? boolean?) expr])))
(define (check e0)
(define e (fix e0))
(define (check e)
(let/ec fail
(or (not e)
(not (bytecode-ok? e))
(implies (with-handlers ([exn:fail? (λ (exc)
(maybe-log-exn exc e)
(fail #f))])
(bytecode-ok? e))
(match
(with-handlers
([exn:fail? (λ (exc)
(maybe-log-exn exc e)
#f)])
(run e '() 100))
[(cutoff) #t]
[(answer _) #t]
[_ #f])))))
(define (maybe-log-exn exc e)
(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])))
(exn-message exc))))
(define (generate-M-term)
(generate-term bytecode e 5))
(fix (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)))
(bytecode-ok? 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)))
(fix (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
'(let-one 'x
@ -482,3 +482,9 @@
(test-equal (check small-counter-example) #f)
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define fixed '())

42
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-5.rkt
View File

@ -431,49 +431,49 @@
[`(quote ,_) expr]
[(? boolean?) expr])))
(define (check e0)
(define e (fix e0))
(define (check e)
(let/ec fail
(or (not e)
(not (bytecode-ok? e))
(implies (with-handlers ([exn:fail? (λ (exc)
(maybe-log-exn exc e)
(fail #f))])
(bytecode-ok? e))
(match
(with-handlers
([exn:fail? (λ (exc)
(maybe-log-exn exc e)
#f)])
(run e '() 100))
[(cutoff) #t]
[(answer _) #t]
[_ #f])))))
(define (maybe-log-exn exc e)
(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])))
(exn-message exc))))
(define (generate-M-term)
(generate-term bytecode e 5))
(fix (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)))
(bytecode-ok? 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)))
(fix (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
'(let-void 1
@ -484,3 +484,9 @@
(test-equal (check small-counter-example) #f)
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define fixed '())

42
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-6.rkt
View File

@ -431,49 +431,49 @@
[`(quote ,_) expr]
[(? boolean?) expr])))
(define (check e0)
(define e (fix e0))
(define (check e)
(let/ec fail
(or (not e)
(not (bytecode-ok? e))
(implies (with-handlers ([exn:fail? (λ (exc)
(maybe-log-exn exc e)
(fail #f))])
(bytecode-ok? e))
(match
(with-handlers
([exn:fail? (λ (exc)
(maybe-log-exn exc e)
#f)])
(run e '() 100))
[(cutoff) #t]
[(answer _) #t]
[_ #f])))))
(define (maybe-log-exn exc e)
(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])))
(exn-message exc))))
(define (generate-M-term)
(generate-term bytecode e 5))
(fix (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)))
(bytecode-ok? 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)))
(fix (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
'(application
@ -481,3 +481,9 @@
'x))
(test-equal (check small-counter-example) #f)
(λ ()
(begin0
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define fixed '())

32
pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/rvm/verification-base.rkt
View File

@ -430,46 +430,52 @@
[`(quote ,_) expr]
[(? boolean?) expr])))
(define (check e0)
(define e (fix e0))
(define (check e)
(let/ec fail
(or (not e)
(not (bytecode-ok? e))
(implies (with-handlers ([exn:fail? (λ (exc)
(maybe-log-exn exc e)
(fail #f))])
(bytecode-ok? e))
(match
(with-handlers
([exn:fail? (λ (exc)
(maybe-log-exn exc e)
#f)])
(run e '() 100))
[(cutoff) #t]
[(answer _) #t]
[_ #f])))))
(define (maybe-log-exn exc e)
(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])))
(exn-message exc))))
(define (generate-M-term)
(generate-term bytecode e 5))
(fix (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)))
(bytecode-ok? 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)))
(fix (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)
(fix (generate-term bytecode e #:i-th index))
(set! index (add1 index))))))
(define fixed '())