From bb74d26ddc90b7db4213d46f088a5e4f1190a133 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Fri, 22 Jul 2016 16:48:08 -0400 Subject: [PATCH] start typed ifc --- turnstile/examples/rosette/ifc.rkt | 48 ++++++++++ .../examples/tests/rosette/ifc-tests.rkt | 92 +++++++++++++++++++ 2 files changed, 140 insertions(+) create mode 100644 turnstile/examples/rosette/ifc.rkt create mode 100644 turnstile/examples/tests/rosette/ifc-tests.rkt diff --git a/turnstile/examples/rosette/ifc.rkt b/turnstile/examples/rosette/ifc.rkt new file mode 100644 index 0000000..ccfb813 --- /dev/null +++ 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 new file mode 100644 index 0000000..7de9fb8 --- /dev/null +++ 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))