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

clean up ifc tests

Browse Source
This commit is contained in:
Stephen Chang 2016-11-03 10:53:50 -04:00
parent 6d33532aab
commit 5d8557bbca
2 changed files with 2 additions and 61 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

62
turnstile/examples/tests/rosette/rosette3/ifc3-tests.rkt
View File

@ -1,7 +1,7 @@
#lang s-exp "../../../rosette/ifc3.rkt"
(require "../../rackunit-typechecking.rkt")
;; verify-EENI-demo.rkt
;; tests from verify-EENI-demo.rkt (same as rosette/sdsl/ifc/test.rkt)
;; takes ~90min to run
@ -515,63 +515,3 @@
(check-type (mem≈ (step (init fig17-p0) 13)
(step (init fig17-p1) 13)) : CBool -> #f)
;; (define (valid-case name ended? prog [k #f])
;; (test-case name (check-true (verify-EENI* init ended? mem≈ prog k))))
;; (define-syntax-rule (define-tests id desc expr ...)
;; (define id
;; (test-suite+
;; desc
;; (begin expr ...))))
;; ; Checks for counterexamples for bugs in basic semantics.
;; (define-tests basic-bugs "IFC: counterexamples for bugs in basic semantics"
;; (cex-case "Fig. 1" halted? (program 3 (list Halt Noop Push Pop Add* Load* Store*AB)))
;; (cex-case "Fig. 2" halted? (program 3 (list Halt Noop Push Pop Add* Load* Store*B)))
;; (cex-case "Fig. 3" halted? (program 5 (list Halt Noop Push Pop Add* Load* Store)))
;; (cex-case "Fig. 4" halted? (program 7 (list Halt Noop Push Pop Add Load* Store))))
;; (define-tests basic-correct "IFC: no bounded counterexamples for correct basic semantics"
;; (valid-case "*" halted? (program 7 (list Halt Noop Push Pop Add Load Store)))
;; (valid-case "+" halted? (program 8 (list Halt Noop Push Pop Add Load Store))))
;; (define-tests jump-bugs "IFC: counterexamples for bugs in jump+basic semantics"
;; (cex-case "11" halted? (program 6 (list Halt Noop Push Pop Add Load Store Jump*AB)))
;; (cex-case "12" halted? (program 4 (list Halt Noop Push Pop Add Load Store Jump*B))))
;; (define-tests jump-correct "IFC: no bounded counterexamples for correct jump+basic semantics"
;; (valid-case "**" halted? (program 7 (list Halt Noop Push Pop Add Load Store Jump)))
;; (valid-case "++" halted? (program 8 (list Halt Noop Push Pop Add Load Store Jump))))
;; (define-tests call-return-bugs "IFC: counterexamples for buggy call+return+basic semantics"
;; (cex-case "Fig. 13" halted∩low? (program 7 (list Halt Noop Push Pop Add Load Store Call*B Return*AB)))
;; (cex-case "Fig. 15" halted∩low? (program 8 (list Halt Noop Push Pop Add Load StoreCR Call*B Return*AB)))
;; (cex-case "Fig. 16" halted∩low? (program 8 (list Halt Noop Push Pop Add Load StoreCR Call*B Return*B)))
;; (cex-case "Fig. 17" halted∩low? (program 10 (list Halt Noop Push Pop Add Load StoreCR Call Return))))
;; (define-tests reproduce-bugs "IFC: counterexamples that are structurally similar to those in prior work"
;; (cex-case "Fig. 13*" halted∩low? (program (list Push Call*B Halt Push Push Store Return*AB)))
;; (cex-case "Fig. 15*" halted∩low? (program (list Push Push Call*B Push StoreCR Halt Push Return*AB)))
;; (cex-case "Fig. 16*" halted∩low? (program (list Push Push Call*B Push StoreCR Halt Return*B Push Return*B)))
;; (cex-case "Fig. 17*"
;; halted∩low?
;; (program (list Push Call Push StoreCR Halt Push Push Call Pop Push Return))
;; 13))
;; (define (fast-tests)
;; (time (run-tests basic-bugs)) ; ~10 sec
;; (time (run-tests basic-correct)) ; ~20 sec
;; (time (run-tests jump-bugs))) ; ~7 sec
;; (define (slow-tests)
;; (time (run-tests jump-correct)) ; ~52 sec
;; (time (run-tests call-return-bugs)) ; ~440 sec
;; (time (run-tests reproduce-bugs))) ; ~256 sec
;; (module+ fast
;; (fast-tests))
;; (module+ test
;; (fast-tests)
;; (slow-tests))

1
turnstile/examples/tests/rosette/rosette3/run-all-rosette-tests-script.rkt
View File

@ -20,5 +20,6 @@
(do-tests "bv-tests.rkt" "BV SDSL - General"
"fsm3-tests.rkt" "FSM"
"ifc3-tests.rkt" "IFC"
"bv-ref-tests.rkt" "BV SDSL - Hacker's Delight synthesis")