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

fixes suggested by latest reviewer of the hosc submission

Browse Source
This commit is contained in:
Robby Findler 2012-09-27 09:35:37 -05:00
parent 3f59309634
commit c5b5c6f9b5
3 changed files with 31 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

34
collects/redex/examples/racket-machine/reduction.rkt
View File

@ -31,7 +31,7 @@
undefined undefined
(clos x)) (clos x))
(e .... (e ....
(self-app x e_0 e_1 ...)) (self-app x e e ...))
(m n ?)) (m n ?))
(define procedure-rules (define procedure-rules
@ -41,8 +41,8 @@
((clos x) S ((x ((clos n ((stack-ref n_0 S) ...) x_i))) (x_0 h_0) ...) T (i ...)) ((clos x) S ((x ((clos n ((stack-ref n_0 S) ...) x_i))) (x_0 h_0) ...) T (i ...))
(fresh x) (fresh x)
"lam") "lam")
(--> (V S ((x_0 h_0) ...) T ((case-lam (lam n (n_0 ...) x_i) ...) i ...)) (--> (V S ((x_0 h_0) ...) T ((case-lam (lam n (n_0 ...) x_j) ...) i ...))
((clos x) S ((x ((clos n ((stack-ref n_0 S) ...) x_i) ...)) (x_0 h_0) ...) T (i ...)) ((clos x) S ((x ((clos n ((stack-ref n_0 S) ...) x_j) ...)) (x_0 h_0) ...) T (i ...))
(fresh x) (fresh x)
"case-lam") "case-lam")
(--> (V S ((x_0 h_0) ...) T ((let-rec ((name l_0 (lam n_0 (n_00 ...) y_0)) ...) e) i ...)) (--> (V S ((x_0 h_0) ...) T ((let-rec ((name l_0 (lam n_0 (n_00 ...) y_0)) ...) e) i ...))
@ -76,6 +76,10 @@
(--> (V S H T ((reorder i_r (e_0 m_1) ... ((loc-noclr n) m_i) (e_i+1 m_i+1) (e_i+2 m_i+2) ...) i ...)) (--> (V S H T ((reorder i_r (e_0 m_1) ... ((loc-noclr n) m_i) (e_i+1 m_i+1) (e_i+2 m_i+2) ...) i ...))
(V S H T ((reorder i_r (e_0 m_1) ... (e_i+1 m_i+1) (e_i+2 m_i+2) ... ((loc-noclr n) m_i)) i ...)) (V S H T ((reorder i_r (e_0 m_1) ... (e_i+1 m_i+1) (e_i+2 m_i+2) ... ((loc-noclr n) m_i)) i ...))
"reorder") "reorder")
(--> (V S H T ((reorder (call n) (e_0 n_0) ... (e_n ?)) i ...))
(V S H T (,@(term (flatten ((framepush e_0 framepop (set n_0)) ...)))
framepush e_n framepop (call n) i ...))
"finalize-app-is-last")
(--> (V S H T ((reorder (call n) (e_0 n_0) ... (e_i ?) (e_i+1 n_i+1) ... (e_j n_j)) i ...)) (--> (V S H T ((reorder (call n) (e_0 n_0) ... (e_i ?) (e_i+1 n_i+1) ... (e_j n_j)) i ...))
(V S H T (,@(term (flatten ((framepush e_0 framepop (set n_0)) ...))) (V S H T (,@(term (flatten ((framepush e_0 framepop (set n_0)) ...)))
framepush e_i framepop (set n_j) framepush e_i framepop (set n_j)
@ -83,18 +87,10 @@
framepush e_j framepop framepush e_j framepop
(swap n_j) (call n) i ...)) (swap n_j) (call n) i ...))
"finalize-app-not-last") "finalize-app-not-last")
(--> (V S H T ((reorder (call n) (e_0 n_0) ... (e_n ?)) i ...))
(V S H T (,@(term (flatten ((framepush e_0 framepop (set n_0)) ...)))
framepush e_n framepop (call n) i ...))
"finalize-app-is-last")
(--> (V S H T ((reorder (self-call x) (e_0 n_0) ...) i ...)) (--> (V S H T ((reorder (self-call x) (e_0 n_0) ...) i ...))
(V S H T (,@(term (flatten ((framepush e_0 framepop (set n_0)) ...))) (V S H T (,@(term (flatten ((framepush e_0 framepop (set n_0)) ...)))
(self-call x) i ...)) (self-call x) i ...))
"finalize-self-app") "finalize-self-app")
(--> (V (u_0 ... u_i ... (u_j ... (u_k ... s))) H (name T ((x_0 e_0) ... (x_i e_i) (x_i+1 e_i+1) ...)) ((self-call x_i) i ...))
(V ((u_j ... (u_0 ... s))) H T (e_i i ...))
(side-condition (= (length (term (u_0 ...))) (length (term (u_k ...)))))
"self-call")
(--> ((clos x_i) (u_1 ... u_n+1 ... (u_m ... (u_k ... s))) (name H ((x_0 h_0) ... (--> ((clos x_i) (u_1 ... u_n+1 ... (u_m ... (u_k ... s))) (name H ((x_0 h_0) ...
(x_i ((clos n_0 (u_0 ...) y_0) ... (x_i ((clos n_0 (u_0 ...) y_0) ...
(clos n_i (u_i ...) y_i) (clos n_i (u_i ...) y_i)
@ -104,6 +100,10 @@
(side-condition (not (memq (term n_i) (term (n_0 ...))))) (side-condition (not (memq (term n_i) (term (n_0 ...)))))
(side-condition (= (term n_i) (length (term (u_1 ...))))) (side-condition (= (term n_i) (length (term (u_1 ...)))))
"call") "call")
(--> (V (u_0 ... u_i ... (u_j ... (u_k ... s))) H (name T ((x_0 e_0) ... (x_i e_i) (x_i+1 e_i+1) ...)) ((self-call x_i) i ...))
(V ((u_j ... (u_0 ... s))) H T (e_i i ...))
(side-condition (= (length (term (u_0 ...))) (length (term (u_k ...)))))
"self-call")
(--> (v S H T ((call n) i ...)) (--> (v S H T ((call n) i ...))
error error
"non-closure" "non-closure"
@ -152,7 +152,7 @@
(--> (V S H T ((swap n) i ...)) (--> (V S H T ((swap n) i ...))
((stack-ref n S) (stack-set V n S) H T (i ...)) ((stack-ref n S) (stack-set V n S) H T (i ...))
"swap") "swap")
(--> (V (u_0 ... (u_i ... (u_j ... s))) H T (framepop i ...)) (--> (V (u_0 ... (u_1 ... (u_2 ... s))) H T (framepop i ...))
(V s H T (i ...)) (V s H T (i ...))
"framepop") "framepop")
(--> (V S H T (framepush i ...)) (--> (V S H T (framepush i ...))
@ -248,8 +248,8 @@
(load’* ((e -) (e_0 -) ...) (x_0 ...)))]) (load’* ((e -) (e_0 -) ...) (x_0 ...)))])
(define-metafunction loader (define-metafunction loader
[(φ+ - n) -] [(incφ - n) -]
[(φ+ (n_p n_a x) n) (,(+ (term n) (term n_p)) n_a x)]) [(incφ (n_p n_a x) n) (,(+ (term n) (term n_p)) n_a x)])
(define-metafunction loader (define-metafunction loader
[(load-lam-rec (lam (τ_0 ...) (n_0 ... n_i n_i+1 ...) e) n_i (y ...)) [(load-lam-rec (lam (τ_0 ...) (n_0 ... n_i n_i+1 ...) e) n_i (y ...))
@ -297,14 +297,14 @@
[(load’ (let-one e_r e_b) φ (y ...)) [(load’ (let-one e_r e_b) φ (y ...))
((let-one e_r* e_b*) (concat H_r H_b) (concat T_r T_b) (y_** ...)) ((let-one e_r* e_b*) (concat H_r H_b) (concat T_r T_b) (y_** ...))
(where (e_r* H_r T_r (y_* ...)) (load’ e_r - (y ...))) (where (e_r* H_r T_r (y_* ...)) (load’ e_r - (y ...)))
(where (e_b* H_b T_b (y_** ...)) (load’ e_b (φ+ φ 1) (y_* ...)))] (where (e_b* H_b T_b (y_** ...)) (load’ e_b (incφ φ 1) (y_* ...)))]
[(load’ (let-void n e) φ (y ...)) [(load’ (let-void n e) φ (y ...))
((let-void n e_*) H T (y_* ...)) ((let-void n e_*) H T (y_* ...))
(where (e_* H T (y_* ...)) (load’ e (φ+ φ n) (y ...)))] (where (e_* H T (y_* ...)) (load’ e (incφ φ n) (y ...)))]
[(load’ (let-void-box n e) φ (y ...)) [(load’ (let-void-box n e) φ (y ...))
((let-void-box n e_*) H T (y_* ...)) ((let-void-box n e_*) H T (y_* ...))
(where (e_* H T (y_* ...)) (load’ e (φ+ φ n) (y ...)))] (where (e_* H T (y_* ...)) (load’ e (incφ φ n) (y ...)))]
[(load’ (boxenv n e) φ (y ...)) [(load’ (boxenv n e) φ (y ...))
((boxenv n e_*) H T (y_* ...)) ((boxenv n e_*) H T (y_* ...))

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

@ -3,6 +3,16 @@
(require redex/reduction-semantics) (require redex/reduction-semantics)
(require "grammar.rkt" "verification.rkt") (require "grammar.rkt" "verification.rkt")
;; trim test cases: just test length-related stuff
;; the contents of the stack itself may be completely bogus
(test-equal (term (trim invalid ())) (term invalid))
(test-equal (term (trim (uninit imm box imm-nc box-nc not) (uninit imm box imm-nc box-nc not)))
(term (uninit imm box imm-nc box-nc not)))
(test-equal (term (trim (uninit imm box imm-nc box-nc not) (imm-nc box-nc not)))
(term (imm-nc box-nc not)))
(test-equal (term (trim (uninit imm box imm-nc box-nc not) ()))
(term ()))
;; localrefs ;; localrefs
(test-predicate (test-predicate
(negate bytecode-ok?) (negate bytecode-ok?)

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

@ -199,7 +199,7 @@
(where (ṽ ...) ((drop-noclr (stack-ref n_0 s)) ...)) (where (ṽ ...) ((drop-noclr (stack-ref n_0 s)) ...))
(where f (extract-self m (n_0 ...) (τ_0 ...) (ṽ ...))) (where f (extract-self m (n_0 ...) (τ_0 ...) (ṽ ...)))
(where (s_1 γ_1 η_1) (verify e (ṽ ... (arg τ_0) ...) n_d* #f () () f))] (where (s_1 γ_1 η_1) (verify e (ṽ ... (arg τ_0) ...) n_d* #f () () f))]
[(lam-verified? any s m) #f]) [(lam-verified? l s m) #f])
(define-metafunction verification (define-metafunction verification
[(extract-self ? (n_0 ...) (τ_0 ...) (ṽ_0 ...)) ∅] [(extract-self ? (n_0 ...) (τ_0 ...) (ṽ_0 ...)) ∅]
@ -329,9 +329,9 @@
(define-metafunction verification (define-metafunction verification
trim : s s -> s trim : s s -> s
[(trim invalid s) invalid] [(trim invalid s) invalid]
[(trim (ṽ_f ...) (ṽ_t ...)) [(trim (ṽ_1 ... ṽ_2 ...) (ṽ_3 ...))
,(take-right (term (ṽ_f ...)) (ṽ_2 ...)
(length (term (ṽ_t ...))))]) (side-condition (= (length (term (ṽ_2 ...))) (length (term (ṽ_3 ...)))))])
(define-metafunction verification (define-metafunction verification
[(valid? invalid) #f] [(valid? invalid) #f]