www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

ifc-tests.rkt (4264B)

      1 #lang s-exp "../../rosette/ifc.rkt"
      2 (require "../rackunit-typechecking.rkt")
      3 
      4 #;(define (cex-case name ended? prog [k #f])
      5   (test-case name (check-pred EENI-witness? (verify-EENI* init ended? mem≈ prog k))))
      6 (define p0 (program 3 (list Halt Noop Push Pop Add* Load* Store*AB))) 
      7 (check-type p0 : Prog)
      8 
      9 ;; expected:
     10 ;; m0 initial:
     11 ;; (machine [pc = 0@⊥]
     12 ;;          [stack = ()]
     13 ;;          [mem = (0@⊥ 0@⊥)]
     14 ;;          [insts = ((Push -16@⊥) (Push 1@⊤) (Store*AB))]
     15 ;; m0 final:
     16 ;; (machine [pc = 3@⊥]
     17 ;;          [stack = ()]
     18 ;;          [mem = (0@⊥ -16@⊥)]
     19 ;;          [insts = ((Push -16@⊥) (Push 1@⊤) (Store*AB))]
     20 ;; m1 initial:
     21 ;; (machine [pc = 0@⊥]
     22 ;;          [stack = ()]
     23 ;;          [mem = (0@⊥ 0@⊥)]
     24 ;;          [insts = ((Push -16@⊥) (Push 0@⊤) (Store*AB))]
     25 ;; m1 final:
     26 ;; (machine [pc = 3@⊥]
     27 ;;          [stack = ()]
     28 ;;          [mem = (-16@⊥ 0@⊥)]
     29 ;;          [insts = ((Push -16@⊥) (Push 0@⊤) (Store*AB))]
     30 (define w0 (verify-EENI* init halted? mem≈ p0 #f))
     31 (check-type w0 : Witness)
     32 (check-type (EENI-witness? w0) : Bool -> #t)
     33 
     34 ;; (define (valid-case name ended? prog [k #f])
     35 ;;   (test-case name (check-true (verify-EENI* init ended? mem≈ prog k))))
     36 
     37 ;; (define-syntax-rule (define-tests id desc expr ...)
     38 ;;   (define id
     39 ;;     (test-suite+ 
     40 ;;      desc 
     41 ;;      (begin expr ...))))
     42 
     43 ;; ; Checks for counterexamples for bugs in basic semantics. 
     44 ;; (define-tests basic-bugs "IFC: counterexamples for bugs in basic semantics"
     45 ;;   (cex-case "Fig. 1" halted? (program 3 (list Halt Noop Push Pop Add* Load* Store*AB))) 
     46 ;;   (cex-case "Fig. 2" halted? (program 3 (list Halt Noop Push Pop Add* Load* Store*B)))  
     47 ;;   (cex-case "Fig. 3" halted? (program 5 (list Halt Noop Push Pop Add* Load* Store)))  
     48 ;;   (cex-case "Fig. 4" halted? (program 7 (list Halt Noop Push Pop Add Load* Store))))  
     49 
     50 ;; (define-tests basic-correct "IFC: no bounded counterexamples for correct basic semantics"
     51 ;;   (valid-case "*" halted? (program 7 (list Halt Noop Push Pop Add Load Store)))  
     52 ;;   (valid-case "+" halted? (program 8 (list Halt Noop Push Pop Add Load Store))))  
     53 
     54 ;; (define-tests jump-bugs "IFC: counterexamples for bugs in jump+basic semantics"
     55 ;;   (cex-case "11" halted? (program 6 (list Halt Noop Push Pop Add Load Store Jump*AB)))  
     56 ;;   (cex-case "12" halted? (program 4 (list Halt Noop Push Pop Add Load Store Jump*B)))) 
     57 
     58 ;; (define-tests jump-correct "IFC: no bounded counterexamples for correct jump+basic semantics"
     59 ;;   (valid-case "**" halted? (program 7 (list Halt Noop Push Pop Add Load Store Jump)))    
     60 ;;   (valid-case "++" halted? (program 8 (list Halt Noop Push Pop Add Load Store Jump))))    
     61 
     62 ;; (define-tests call-return-bugs "IFC: counterexamples for buggy call+return+basic semantics"
     63 ;;   (cex-case "Fig. 13" halted∩low? (program 7 (list Halt Noop Push Pop Add Load Store Call*B Return*AB)))
     64 ;;   (cex-case "Fig. 15" halted∩low? (program 8 (list Halt Noop Push Pop Add Load StoreCR Call*B Return*AB)))
     65 ;;   (cex-case "Fig. 16" halted∩low? (program 8 (list Halt Noop Push Pop Add Load StoreCR Call*B Return*B)))
     66 ;;   (cex-case "Fig. 17" halted∩low? (program 10 (list Halt Noop Push Pop Add Load StoreCR Call Return))))
     67 
     68 ;; (define-tests reproduce-bugs "IFC: counterexamples that are structurally similar to those in prior work"
     69 ;;   (cex-case "Fig. 13*" halted∩low? (program (list Push Call*B Halt Push Push Store Return*AB)))
     70 ;;   (cex-case "Fig. 15*" halted∩low? (program (list Push Push Call*B Push StoreCR Halt Push Return*AB)))
     71 ;;   (cex-case "Fig. 16*" halted∩low? (program (list Push Push Call*B Push StoreCR Halt Return*B Push Return*B)))
     72 ;;   (cex-case "Fig. 17*" 
     73 ;;             halted∩low? 
     74 ;;             (program (list Push Call Push StoreCR Halt Push Push Call Pop Push Return))
     75 ;;             13))
     76 
     77 ;; (define (fast-tests)
     78 ;;   (time (run-tests basic-bugs))       ; ~10 sec
     79 ;;   (time (run-tests basic-correct))    ; ~20 sec
     80 ;;   (time (run-tests jump-bugs)))       ; ~7 sec
     81 
     82 ;; (define (slow-tests)
     83 ;;   (time (run-tests jump-correct))     ; ~52 sec
     84 ;;   (time (run-tests call-return-bugs)) ; ~440 sec
     85 ;;   (time (run-tests reproduce-bugs)))  ; ~256 sec
     86 
     87 ;; (module+ fast
     88 ;;   (fast-tests))
     89 
     90 ;; (module+ test
     91 ;;   (fast-tests)
     92 ;;   (slow-tests))