From fd8a59a45f3f9a4b4629c1501dd6f6dd87bdc2b3 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Wed, 2 Nov 2016 23:33:52 -0400 Subject: [PATCH] add ifc3, ifc3-tests --- turnstile/examples/rosette/ifc3.rkt | 135 +++++ turnstile/examples/rosette/rosette3.rkt | 2 +- .../tests/rosette/rosette3/fsm-test.rkt | 43 -- .../tests/rosette/rosette3/ifc-tests.rkt | 92 ---- .../tests/rosette/rosette3/ifc3-tests.rkt | 516 ++++++++++++++++++ 5 files changed, 652 insertions(+), 136 deletions(-) create mode 100644 turnstile/examples/rosette/ifc3.rkt delete mode 100644 turnstile/examples/tests/rosette/rosette3/fsm-test.rkt delete mode 100644 turnstile/examples/tests/rosette/rosette3/ifc-tests.rkt create mode 100644 turnstile/examples/tests/rosette/rosette3/ifc3-tests.rkt diff --git a/turnstile/examples/rosette/ifc3.rkt b/turnstile/examples/rosette/ifc3.rkt new file mode 100644 index 0000000..8916267 --- /dev/null +++ b/turnstile/examples/rosette/ifc3.rkt @@ -0,0 +1,135 @@ +#lang turnstile +(extends "rosette3.rkt" #:except) ; extends typed rosette +(require (prefix-in ro: (except-in rosette read write pc init)) ; untyped + (prefix-in ro: rosette/lib/synthax) + (prefix-in ro: sdsl/ifc/instruction) ; program + (prefix-in ro: sdsl/ifc/basic) ; Halt, Noop, Push, etc + (prefix-in ro: sdsl/ifc/jump) + (prefix-in ro: sdsl/ifc/call) + (prefix-in ro: sdsl/ifc/machine) ; init, halted? + (prefix-in ro: sdsl/ifc/indistinguishable) ; mem≈ + (prefix-in ro: sdsl/ifc/verify)) ; verify-EENI + +(define-base-types + InstrName ; names of instructions like Halt, Noop + Instr ; InstrName + args (recognized by instruction? in untyped rosette) + Machine + Witness + Lvl ; security level, either ⊥ or ⊤ + Val) ; a value is an Int + security level + +(define-named-type-alias InstrNames (CListof InstrName)) +;; TODO: differentiate concrete and symbolic progams +;; - see program constructor +(define-named-type-alias Prog (CListof Instr)) +(define-named-type-alias Stack (CListof Val)) +(define-named-type-alias Mem (CListof Val)) +(define-named-type-alias PC Val) +(define-named-type-alias LoC Int) ; lines of code + +(ro:define ro:1@⊥ (ro:@ (ro:#%datum . 1) ro:⊥)) +(ro:define ro:2@⊥ (ro:@ (ro:#%datum . 2) ro:⊥)) +(ro:define ro:3@⊥ (ro:@ (ro:#%datum . 3) ro:⊥)) +(ro:define ro:4@⊥ (ro:@ (ro:#%datum . 4) ro:⊥)) + +(ro:define ro:0@⊤ (ro:@ (ro:#%datum . 0) ro:⊤)) +(ro:define ro:1@⊤ (ro:@ (ro:#%datum . 1) ro:⊤)) +(ro:define ro:2@⊤ (ro:@ (ro:#%datum . 2) ro:⊤)) +(ro:define ro:3@⊤ (ro:@ (ro:#%datum . 3) ro:⊤)) +(ro:define ro:4@⊤ (ro:@ (ro:#%datum . 4) ro:⊤)) + +(provide InstrName InstrNames Instr Prog Stack Mem Machine Witness + (typed-out + + ;; Security Levels (labels) + [⊥ : Lvl] + [[ro:⊥ : Lvl] public] + [⊤ : Lvl] + [[ro:⊤ : Lvl] secret] + + ;; (labeled) Values + [0@⊥ : Val][1@⊥ : Val][2@⊥ : Val][3@⊥ : Val][4@⊥ : Val] + [0@⊤ : Val][1@⊤ : Val][2@⊤ : Val][3@⊤ : Val][4@⊤ : Val] + [@ : (C→ Int Lvl Val)] + + ;; Machine + [machine : (C→ PC Stack Mem Prog Machine)] + + ;; Machine Instructions + [Halt : InstrName] + [Noop : InstrName] + [Push : InstrName] + [Pop : InstrName] + [Load* : InstrName] + [Load : InstrName] + [Store*AB : InstrName] + [Store*B : InstrName] + [Store : InstrName] + [Add* : InstrName] + [Add : InstrName] + [Jump*AB : InstrName] + [Jump*B : InstrName] + [Jump : InstrName] + [Return*AB : InstrName] + [Return*B : InstrName] + [Return : InstrName] + [Call*B : InstrName] + [Call : InstrName] + [PopCR : InstrName] + [StoreCR : InstrName] + + [instruction : (Ccase-> (C→ InstrName Instr) + (C→ InstrName Val Instr) + (C→ InstrName Val Val Instr))] + + [init : (C→ Prog Machine)] + [halted? : (C→ Machine Bool)] + [halted∩low? : (C→ Machine Bool)] + [mem≈ : (C→ Machine Machine Bool)] + + [program : (Ccase-> + (C→ InstrNames Prog) ; concrete prog + (C→ LoC InstrNames Prog))] ; symbolic prog + + [verify-EENI : (Ccase-> + (C→ (C→ Prog Machine) ; start + (C→ Machine Bool) ; end + (C→ Machine Machine Bool) ; ≈ + Prog + CUnit) + (C→ (C→ Prog Machine) ; start + (C→ Machine Bool) ; end + (C→ Machine Machine Bool) ; ≈ + Prog + (CU CInt CFalse) ; k = steps + CUnit))] + [verify-EENI* : (Ccase-> + (C→ (C→ Prog Machine) ; start + (C→ Machine Bool) ; end + (C→ Machine Machine Bool) ; ≈ + Prog + Witness) + (C→ (C→ Prog Machine) ; start + (C→ Machine Bool) ; end + (C→ Machine Machine Bool) ; ≈ + Prog + (CU CInt CFalse) ; k = steps + Witness) + (C→ (C→ Prog Machine) ; start + (C→ Machine Bool) ; end + (C→ Machine Machine Bool) ; ≈ + Prog + (CU CInt CFalse) ; k = steps + CBool ; verbose? + (CU Witness CTrue)))] + [EENI-witness : (C→ Machine Machine Int (C→ Machine Machine Bool) Witness)] + [EENI-witness-k : (C→ Any CInt)] + [EENI-witness? : CPred])) + +#;(define-typed-syntax program + [(_ n procs) ≫ + [⊢ [n ≫ n- ⇐ : Int]] + [⊢ [procs ≫ procs- ⇐ : (List Instr)]] + -------- + [⊢ [_ ≫ (ifc:program n- procs-) ⇒ : Prog]]]) + diff --git a/turnstile/examples/rosette/rosette3.rkt b/turnstile/examples/rosette/rosette3.rkt index 2d27abe..aeaecdc 100644 --- a/turnstile/examples/rosette/rosette3.rkt +++ b/turnstile/examples/rosette/rosette3.rkt @@ -45,7 +45,7 @@ ;; BV types CBV BV CBVPred BVPred - CSolution CSolver CPict CSyntax CRegexp CSymbol) + CSolution CSolver CPict CSyntax CRegexp CSymbol CPred) (begin-for-syntax (define (mk-ro:-id id) (format-id id "ro:~a" id)) diff --git a/turnstile/examples/tests/rosette/rosette3/fsm-test.rkt b/turnstile/examples/tests/rosette/rosette3/fsm-test.rkt deleted file mode 100644 index 6a9c944..0000000 --- a/turnstile/examples/tests/rosette/rosette3/fsm-test.rkt +++ /dev/null @@ -1,43 +0,0 @@ -#lang s-exp "../../rosette/fsm3.rkt" -(require "../../rackunit-typechecking.rkt") - -(define m - (automaton init - [init : (c → more)] - [more : (a → more) - (d → more) - (r → end)] - [end : ])) - -(define rx #px"^c[ad]+r$") - -(typecheck-fail (automaton init) - #:with-msg "initial state init is not declared state") -(typecheck-fail (automaton init [init : (c → more)]) - #:with-msg "unbound identifier") -(typecheck-fail (automaton init [init : (c → "more")]) - #:with-msg "expected State, given String") - -(define M - (automaton init - [init : (c → (? s1 s2))] - [s1 : (a → (? s1 s2 end reject)) - (d → (? s1 s2 end reject)) - (r → (? s1 s2 end reject))] - [s2 : (a → (? s1 s2 end reject)) - (d → (? s1 s2 end reject)) - (r → (? s1 s2 end reject))] - [end : ])) - - -(check-type (M '(c a r)) : Bool) ; symbolic result -(check-type (if (M '(c a r)) 1 2) : Int) - -;; example commands -(check-type (m '(c a r)) : Bool -> #t) -(check-type (m '(c d r)) : Bool -> #t) -(check-type (m '(c a d a r)) : Bool -> #t) -(check-type (m '(c a d a)) : Bool -> #f) -(check-type (verify-automaton m #px"^c[ad]+r$") : (List Symbol) -> '(c r)) -(check-type (debug-automaton m #px"^c[ad]+r$" '(c r)) : Pict) -(check-type (synthesize-automaton M #px"^c[ad]+r$") : Unit) diff --git a/turnstile/examples/tests/rosette/rosette3/ifc-tests.rkt b/turnstile/examples/tests/rosette/rosette3/ifc-tests.rkt deleted file mode 100644 index 98188b8..0000000 --- a/turnstile/examples/tests/rosette/rosette3/ifc-tests.rkt +++ /dev/null @@ -1,92 +0,0 @@ -#lang s-exp "../../rosette/ifc3.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)) diff --git a/turnstile/examples/tests/rosette/rosette3/ifc3-tests.rkt b/turnstile/examples/tests/rosette/rosette3/ifc3-tests.rkt new file mode 100644 index 0000000..c865d7b --- /dev/null +++ b/turnstile/examples/tests/rosette/rosette3/ifc3-tests.rkt @@ -0,0 +1,516 @@ +#lang s-exp "../../../rosette/ifc3.rkt" +(require "../../rackunit-typechecking.rkt") + +;; verify-EENI-demo.rkt + +;; takes ~90min to run + +(define (verify/halted [p : Prog] -> (CU Witness CTrue)) + (verify-EENI* init halted? mem≈ p)) +(define (verify/halted+low [p : Prog] -> (CU Witness CTrue)) + (verify-EENI* init halted∩low? mem≈ p)) +(define (verify/halted+low/steps [p : Prog] [k : CInt] -> (CU Witness CTrue)) + (verify-EENI* init halted∩low? mem≈ p k)) + +;; basic-bugs -------------------------------------------------- +(define basic-p0 (program 3 (list Halt Noop Push Pop Add* Load* Store*AB))) +(define basic-p1 (program 3 (list Halt Noop Push Pop Add* Load* Store*B))) +(define basic-p2 (program 5 (list Halt Noop Push Pop Add* Load* Store))) +(define basic-p3 (program 7 (list Halt Noop Push Pop Add Load* Store))) +(check-type basic-p0 : Prog) +(check-type basic-p1 : Prog) +(check-type basic-p2 : Prog) +(check-type basic-p3 : Prog) + +(define basic-w0 (verify/halted basic-p0)) +(define basic-w1 (verify/halted basic-p1)) +(define basic-w2 (verify/halted basic-p2)) +(define basic-w3 (verify/halted basic-p3)) +(check-type (EENI-witness? basic-w0) : Bool -> #t) +(check-type (EENI-witness? basic-w1) : Bool -> #t) +(check-type (EENI-witness? basic-w2) : Bool -> #t) +(check-type (EENI-witness? basic-w3) : Bool -> #t) +(check-type basic-w0 + : (CU Witness CTrue) + -> (EENI-witness + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list + (instruction Push (@ -16 ⊥)) + (instruction Push (@ 1 ⊤)) + (instruction Store*AB))) + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list + (instruction Push (@ -16 ⊥)) + (instruction Push (@ 0 ⊤)) + (instruction Store*AB))) + 3 + mem≈)) +(check-type basic-w1 + : (CU Witness CTrue) + -> (EENI-witness + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list + (instruction Push (@ -16 public)) + (instruction Push (@ 1 secret)) + (instruction Store*B))) + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list + (instruction Push (@ -16 public)) + (instruction Push (@ 0 secret)) + (instruction Store*B))) + 3 + mem≈)) +(check-type basic-w2 + : (CU Witness CTrue) + -> (EENI-witness + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list + (instruction Push (@ -16 public)) + (instruction Push (@ 0 secret)) + (instruction Add*) + (instruction Push (@ 1 public)) + (instruction Store))) + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list + (instruction Push (@ -16 public)) + (instruction Push (@ 8 secret)) + (instruction Add*) + (instruction Push (@ 1 public)) + (instruction Store))) + 5 + mem≈)) +(check-type basic-w3 + : (CU Witness CTrue) + -> (EENI-witness + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list + (instruction Push (@ 1 secret)) + (instruction Push (@ 0 secret)) + (instruction Push (@ 1 public)) + (instruction Store) + (instruction Load*) + (instruction Push 0@⊥) + (instruction Store))) + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list + (instruction Push (@ 0 secret)) + (instruction Push (@ 0 secret)) + (instruction Push (@ 1 public)) + (instruction Store) + (instruction Load*) + (instruction Push 0@⊥) + (instruction Store))) + 7 + mem≈)) + +;; basic-correct -------------------------------------------------- +(define basic-p4 (program 7 (list Halt Noop Push Pop Add Load Store))) +(define basic-p5 (program 8 (list Halt Noop Push Pop Add Load Store))) +(check-type basic-p4 : Prog) +(check-type basic-p5 : Prog) + +(define basic-w4 (verify/halted basic-p4)) +(define basic-w5 (verify/halted basic-p5)) +(check-type basic-w4 : (CU Witness CTrue) -> #t) +(check-type basic-w5 : (CU Witness CTrue) -> #t) + + +;; jump-bugs -------------------------------------------------- +(define jump-p0 (program 6 (list Halt Noop Push Pop Add Load Store Jump*AB))) +(define jump-p1 (program 4 (list Halt Noop Push Pop Add Load Store Jump*B))) +(check-type jump-p0 : Prog) +(check-type jump-p1 : Prog) + +(define jump-w0 (verify/halted jump-p0)) +(define jump-w1 (verify/halted jump-p1)) +(check-type jump-w0 : (CU Witness CTrue) + -> (EENI-witness + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Noop) + (instruction Push (@ 0 ⊤)) + (instruction Push (@ 4 ⊤)) + (instruction Jump*AB) + (instruction Push (@ 1 ⊥)) + (instruction Store))) + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Noop) + (instruction Push (@ 6 ⊤)) + (instruction Push (@ 3 ⊤)) + (instruction Jump*AB) + (instruction Push (@ 1 ⊥)) + (instruction Store))) + 6 + mem≈)) +(check-type jump-w1 : (CU Witness CTrue) + -> (EENI-witness + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push (@ 2 ⊤)) + (instruction Jump*B) + (instruction Push (@ 4 ⊥)) + (instruction Jump*B))) + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push (@ 4 ⊤)) + (instruction Jump*B) + (instruction Push (@ 4 ⊥)) + (instruction Jump*B))) + 4 + mem≈)) + +;; jump-correct -------------------------------------------------- +(define jump-p2 (program 7 (list Halt Noop Push Pop Add Load Store Jump))) +(define jump-p3 (program 8 (list Halt Noop Push Pop Add Load Store Jump))) +(check-type jump-p2 : Prog) +(check-type jump-p3 : Prog) + +(define jump-w2 (verify/halted jump-p2)) +(define jump-w3 (verify/halted jump-p3)) +(check-type jump-w2 : (CU Witness CTrue) -> #t) +(check-type jump-w3 : (CU Witness CTrue) -> #t) + +;; call-return-bugs -------------------------------------------------- +(define call-return-p0 + (program 7 (list Halt Noop Push Pop Add Load Store Call*B Return*AB))) +(define call-return-p1 + (program 8 (list Halt Noop Push Pop Add Load StoreCR Call*B Return*AB))) +(define call-return-p2 + (program 8 (list Halt Noop Push Pop Add Load StoreCR Call*B Return*B))) +(define call-return-p3 + (program 10 (list Halt Noop Push Pop Add Load StoreCR Call Return))) +(check-type call-return-p0 : Prog) +(check-type call-return-p1 : Prog) +(check-type call-return-p2 : Prog) +(check-type call-return-p3 : Prog) + +(define call-return-w0 (verify/halted+low call-return-p0)) +(define call-return-w1 (verify/halted+low call-return-p1)) +(define call-return-w2 (verify/halted+low call-return-p2)) +(define call-return-w3 (verify/halted+low call-return-p3)) +(check-type call-return-w0 : (CU Witness CTrue) + -> (EENI-witness + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push (@ 3 ⊤)) + (instruction Call*B 0@⊥) + (instruction Halt) + (instruction Push (@ 4 ⊥)) + (instruction Push 0@⊥) + (instruction Store) + (instruction Return*AB (@ 1 ⊥)))) + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push (@ 6 ⊤)) + (instruction Call*B 0@⊥) + (instruction Halt) + (instruction Push (@ 4 ⊥)) + (instruction Push 0@⊥) + (instruction Store) + (instruction Return*AB (@ 1 ⊥)))) + 7 + mem≈)) +(check-type call-return-w1 : (CU Witness CTrue) + -> (EENI-witness + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push (@ 0 ⊤)) + (instruction Push (@ 6 ⊤)) + (instruction Call*B (@ 1 ⊥)) + (instruction Push 0@⊥) + (instruction StoreCR) + (instruction Halt) + (instruction Push (@ -9 ⊥)) + (instruction Return*AB (@ 1 ⊥)))) + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push (@ 0 ⊤)) + (instruction Push (@ 7 ⊤)) + (instruction Call*B (@ 1 ⊥)) + (instruction Push 0@⊥) + (instruction StoreCR) + (instruction Halt) + (instruction Push (@ -9 ⊥)) + (instruction Return*AB (@ 1 ⊥)))) + 8 + mem≈)) +(check-type call-return-w2 : (CU Witness CTrue) + -> (EENI-witness + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push (@ 5 ⊥)) + (instruction Call*B 0@⊥) + (instruction Push (@ 1 ⊥)) + (instruction StoreCR) + (instruction Halt) + (instruction Push 0@⊥) + (instruction Push (@ 0 ⊤)) + (instruction Return*B (@ 1 ⊥)))) + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push (@ 5 ⊥)) + (instruction Call*B 0@⊥) + (instruction Push (@ 1 ⊥)) + (instruction StoreCR) + (instruction Halt) + (instruction Push 0@⊥) + (instruction Push (@ -4 ⊤)) + (instruction Return*B (@ 1 ⊥)))) + 8 + mem≈)) + +(check-type call-return-w3 : (CU Witness CTrue) + -> (EENI-witness + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push (@ 6 ⊥)) + (instruction Call 0@⊥ (@ 1 ⊥)) + (instruction Halt) + (instruction Pop) + (instruction Push (@ 4 ⊥)) + (instruction Return) + (instruction Push (@ 3 ⊤)) + (instruction Call (@ 1 ⊥) (@ 1 ⊥)) + (instruction Push 0@⊥) + (instruction StoreCR))) + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push (@ 6 ⊥)) + (instruction Call 0@⊥ (@ 1 ⊥)) + (instruction Halt) + (instruction Pop) + (instruction Push (@ 4 ⊥)) + (instruction Return) + (instruction Push (@ 4 ⊤)) + (instruction Call (@ 1 ⊥) (@ 1 ⊥)) + (instruction Push 0@⊥) + (instruction StoreCR))) + 10 + mem≈)) + +;; call-return-correct -------------------------------------------------- +(define call-return-p4 + (program 10 (list Halt Noop Push PopCR Add Load StoreCR Call Return))) +(check-type call-return-p4 : Prog) +(define call-return-w4 (verify/halted+low call-return-p4)) +(check-type call-return-w4 : (CU Witness CTrue) -> #t) + + +;; reproduce-bugs -------------------------------------------------- +;; ~45sec +(define reproduce-p0 + (program (list Push Call*B Halt Push Push Store Return*AB))) +(define reproduce-p1 + (program (list Push Push Call*B Push StoreCR Halt Push Return*AB))) +(define reproduce-p2 + (program (list Push Push Call*B Push StoreCR Halt Return*B Push Return*B))) +(define reproduce-p3 + (program (list Push Call Push StoreCR Halt Push Push Call Pop Push Return))) +(check-type reproduce-p0 : Prog) +(check-type reproduce-p1 : Prog) +(check-type reproduce-p2 : Prog) +(check-type reproduce-p3 : Prog) + +(define reproduce-w0 (verify/halted+low reproduce-p0)) +(define reproduce-w1 (verify/halted+low reproduce-p1)) +(define reproduce-w2 (verify/halted+low reproduce-p2)) +(define reproduce-w3 (verify/halted+low/steps reproduce-p3 13)) +(check-type reproduce-w0 : (CU Witness CTrue) + -> (EENI-witness + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push (@ 3 ⊤)) + (instruction Call*B 0@⊥) + (instruction Halt) + (instruction Push (@ 4 ⊤)) + (instruction Push 0@⊥) + (instruction Store) + (instruction Return*AB 0@⊥))) + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push (@ 6 ⊤)) + (instruction Call*B 0@⊥) + (instruction Halt) + (instruction Push (@ 4 ⊤)) + (instruction Push 0@⊥) + (instruction Store) + (instruction Return*AB 0@⊥))) + 7 + mem≈)) +(check-type reproduce-w1 : (CU Witness CTrue) + -> (EENI-witness + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push 0@⊥) + (instruction Push (@ 6 ⊤)) + (instruction Call*B (@ 1 ⊥)) + (instruction Push (@ 1 ⊥)) + (instruction StoreCR) + (instruction Halt) + (instruction Push (@ 1 ⊥)) + (instruction Return*AB (@ 1 ⊥)))) + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push 0@⊥) + (instruction Push (@ 7 ⊤)) + (instruction Call*B (@ 1 ⊥)) + (instruction Push (@ 1 ⊥)) + (instruction StoreCR) + (instruction Halt) + (instruction Push (@ 1 ⊥)) + (instruction Return*AB (@ 1 ⊥)))) + 8 + mem≈)) +(check-type reproduce-w2 : (CU Witness CTrue) + -> (EENI-witness + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push 0@⊥) + (instruction Push (@ 7 ⊥)) + (instruction Call*B 1@⊥) + (instruction Push 0@⊥) + (instruction StoreCR) + (instruction Halt) + (instruction Return*B (@ -1 ⊤)) + (instruction Push 1@⊤) + (instruction Return*B 1@⊥))) + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push 0@⊥) + (instruction Push (@ 7 ⊥)) + (instruction Call*B 1@⊥) + (instruction Push 0@⊥) + (instruction StoreCR) + (instruction Halt) + (instruction Return*B (@ 1 ⊤)) + (instruction Push 0@⊤) + (instruction Return*B 1@⊥))) + 9 + mem≈)) +(check-type reproduce-w3 : (CU Witness CTrue) + -> (EENI-witness + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push (@ 6 ⊥)) + (instruction Call 0@⊥ 1@⊥) + (instruction Push 0@⊥) + (instruction StoreCR) + (instruction Halt) + (instruction Push (@ -1 ⊤)) + (instruction Push (@ 9 ⊤)) + (instruction Call 0@⊥ 1@⊥) + (instruction Pop) + (instruction Push 1@⊥) + (instruction Return))) + (machine 0@⊥ + (list) + (list 0@⊥ 0@⊥) + (list (instruction Push (@ 6 ⊥)) + (instruction Call 0@⊥ 1@⊥) + (instruction Push 0@⊥) + (instruction StoreCR) + (instruction Halt) + (instruction Push (@ -3 ⊤)) + (instruction Push (@ 8 ⊤)) + (instruction Call 0@⊥ 1@⊥) + (instruction Pop) + (instruction Push 1@⊥) + (instruction Return))) + 13 + mem≈)) + +;; (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))