commit bb74d26ddc90b7db4213d46f088a5e4f1190a133
parent 541c1e64a923cc64c84e08a5fcac7593b69a82a6
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Fri, 22 Jul 2016 16:48:08 -0400
start typed ifc
Diffstat:
2 files changed, 140 insertions(+), 0 deletions(-)
diff --git a/turnstile/examples/rosette/ifc.rkt b/turnstile/examples/rosette/ifc.rkt
@@ -0,0 +1,48 @@
+;#lang turnstile
+#lang racket/base
+(require (except-in "../../../turnstile/turnstile.rkt"
+ #%module-begin
+ zero? void sub1 or and not add1 = - * + boolean? integer? string? quote pregexp make-parameter equal? list)
+ (for-syntax (except-in "../../../turnstile/turnstile.rkt")))
+(extends "rosette.rkt" #:except) ; extends typed rosette
+(require (prefix-in ro: rosette)) ; untyped
+(require (prefix-in ro: rosette/lib/synthax))
+;(require (prefix-in ifc: sdsl/ifc/instruction))
+(require sdsl/ifc/instruction) ; program
+(require sdsl/ifc/basic) ; Halt, Noop, Push, etc
+(require (except-in sdsl/ifc/machine write read)) ; init, halted?
+(require sdsl/ifc/indistinguishable) ; mem≈
+(require sdsl/ifc/verify) ; verify-EENI
+
+(define-base-types Prog Instr Machine Witness)
+
+(define-primop Halt : Instr)
+(define-primop Noop : Instr)
+(define-primop Push : Instr)
+(define-primop Pop : Instr)
+(define-primop Load* : Instr)
+(define-primop Store*AB : Instr)
+(define-primop Store*B : Instr)
+(define-primop Add* : Instr)
+(define-primop Load : Instr)
+(define-primop Store : Instr)
+(define-primop Add : Instr)
+
+(define-primop init : (→ Prog Machine))
+(define-primop halted? : (→ Machine Bool))
+(define-primop mem≈ : (→ Machine Machine Bool))
+
+(define-primop program : (→ Int (List Instr) Prog))
+#;(define-typed-syntax program
+ [(_ n procs) ≫
+ [⊢ [n ≫ n- ⇐ : Int]]
+ [⊢ [procs ≫ procs- ⇐ : (List Instr)]]
+ --------
+ [⊢ [_ ≫ (ifc:program n- procs-) ⇒ : Prog]]])
+
+(define-primop verify-EENI* : (→ (→ Prog Machine)
+ (→ Machine Bool)
+ (→ Machine Machine Bool)
+ Prog Bool
+ Witness))
+(define-primop EENI-witness? : (→ Witness Bool))
diff --git a/turnstile/examples/tests/rosette/ifc-tests.rkt b/turnstile/examples/tests/rosette/ifc-tests.rkt
@@ -0,0 +1,92 @@
+#lang s-exp "../../rosette/ifc.rkt"
+(require "../rackunit-typechecking.rkt")
+
+#;(define (cex-case name ended? prog [k #f])
+ (test-case name (check-pred EENI-witness? (verify-EENI* init ended? mem≈ prog k))))
+(define p0 (program 3 (list Halt Noop Push Pop Add* Load* Store*AB)))
+(check-type p0 : Prog)
+
+;; expected:
+;; m0 initial:
+;; (machine [pc = 0@⊥]
+;; [stack = ()]
+;; [mem = (0@⊥ 0@⊥)]
+;; [insts = ((Push -16@⊥) (Push 1@⊤) (Store*AB))]
+;; m0 final:
+;; (machine [pc = 3@⊥]
+;; [stack = ()]
+;; [mem = (0@⊥ -16@⊥)]
+;; [insts = ((Push -16@⊥) (Push 1@⊤) (Store*AB))]
+;; m1 initial:
+;; (machine [pc = 0@⊥]
+;; [stack = ()]
+;; [mem = (0@⊥ 0@⊥)]
+;; [insts = ((Push -16@⊥) (Push 0@⊤) (Store*AB))]
+;; m1 final:
+;; (machine [pc = 3@⊥]
+;; [stack = ()]
+;; [mem = (-16@⊥ 0@⊥)]
+;; [insts = ((Push -16@⊥) (Push 0@⊤) (Store*AB))]
+(define w0 (verify-EENI* init halted? mem≈ p0 #f))
+(check-type w0 : Witness)
+(check-type (EENI-witness? w0) : Bool -> #t)
+
+;; (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))
