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

Fixes bug with "noclear" rewind.

Browse Source
This commit is contained in:
Casey Klein 2010-07-01 17:32:42 -05:00
parent f786f24ac5
commit 2025c27475
2 changed files with 12 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
collects/redex/examples/racket-machine/verification-test.rkt
View File

@ -370,6 +370,10 @@
(negate bytecode-ok?) (negate bytecode-ok?)
'(let-one 'w (branch 'x (boxenv 0 'y) (loc-clr 0)))) '(let-one 'w (branch 'x (boxenv 0 'y) (loc-clr 0))))
(test-predicate
(negate bytecode-ok?)
'(let-one 'x (branch (loc-noclr 0) (loc-noclr 0) (loc-clr 0))))
; let-rec ; let-rec
(test-predicate (test-predicate
bytecode-ok? bytecode-ok?

15
collects/redex/examples/racket-machine/verification.rkt
View File

@ -33,15 +33,15 @@
(side-condition (memq (term ṽ_n) '(box box-nc)))] (side-condition (memq (term ṽ_n) '(box box-nc)))]
[(verify (loc-noclr n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l #f γ η f) [(verify (loc-noclr n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l #f γ η f)
((ṽ_0 ... (nc ṽ_n) ṽ_n+1 ...) γ (log-noclear n n_l η)) ((ṽ_0 ... (nc ṽ_n) ṽ_n+1 ...) γ (log-noclear n n_l ṽ_n η))
(side-condition (= (length (term (ṽ_0 ...))) (term n))) (side-condition (= (length (term (ṽ_0 ...))) (term n)))
(side-condition (memq (term ṽ_n) '(imm imm-nc)))] (side-condition (memq (term ṽ_n) '(imm imm-nc)))]
[(verify (loc-noclr n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l #t γ η f) [(verify (loc-noclr n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l #t γ η f)
((ṽ_0 ... (nc ṽ_n) ṽ_n+1 ...) γ (log-noclear n n_l η)) ((ṽ_0 ... (nc ṽ_n) ṽ_n+1 ...) γ (log-noclear n n_l ṽ_n η))
(side-condition (= (length (term (ṽ_0 ...))) (term n))) (side-condition (= (length (term (ṽ_0 ...))) (term n)))
(side-condition (memq (term ṽ_n) '(imm imm-nc box box-nc)))] (side-condition (memq (term ṽ_n) '(imm imm-nc box box-nc)))]
[(verify (loc-box-noclr n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l b γ η f) [(verify (loc-box-noclr n) (ṽ_0 ... ṽ_n ṽ_n+1 ...) n_l b γ η f)
((ṽ_0 ... box-nc ṽ_n+1 ...) γ (log-noclear n n_l η)) ((ṽ_0 ... box-nc ṽ_n+1 ...) γ (log-noclear n n_l ṽ_n η))
(side-condition (= (length (term (ṽ_0 ...))) (term n))) (side-condition (= (length (term (ṽ_0 ...))) (term n)))
(side-condition (memq (term ṽ_n) '(box box-nc)))] (side-condition (memq (term ṽ_n) '(box box-nc)))]
@ -272,11 +272,12 @@
[(nc box-nc) box-nc]) [(nc box-nc) box-nc])
(define-metafunction verification (define-metafunction verification
log-noclear : n n η -> η log-noclear : n n ṽ η -> η
[(log-noclear n_p n_l (n_0 ...)) [(log-noclear n_p n_l ṽ_p (n_0 ...))
(,(- (term n_p) (term n_l)) n_0 ...) (,(- (term n_p) (term n_l)) n_0 ...)
(side-condition (>= (term n_p) (term n_l)))] (side-condition (>= (term n_p) (term n_l)))
[(log-noclear n_p n_l η) η]) (side-condition (memq (term ṽ_p) '(imm box)))]
[(log-noclear n_p n_l ṽ_p η) η])
(define-metafunction verification (define-metafunction verification
undo-noclears : η s -> s undo-noclears : η s -> s