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

add ifc3, ifc3-tests

Browse Source
This commit is contained in:
Stephen Chang 2016-11-02 23:33:52 -04:00
parent ad6978a432
commit fd8a59a45f
5 changed files with 652 additions and 136 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

135
turnstile/examples/rosette/ifc3.rkt Normal file
View File

@ -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]]])

2
turnstile/examples/rosette/rosette3.rkt
View File

@ -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))

43
turnstile/examples/tests/rosette/rosette3/fsm-test.rkt
View File

@ -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)

92
turnstile/examples/tests/rosette/rosette3/ifc-tests.rkt
View File

@ -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))

516
turnstile/examples/tests/rosette/rosette3/ifc3-tests.rkt Normal file
View File

@ -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))