Transcription
Solver-aided programming:going proEmina TorlakUniversity of on.edu/ emina/
A programming model thatintegrates solvers into thelanguage, providing constructsfor program verification,synthesis, and more.R SETTESolver-aided programming in two parts:(1) getting started and (2) going proHow to use a solver-aidedlanguage: the workflow,constructs, and gotchas.How to build your ownsolver-aided toollanguagevia directsymbolic evaluation orlanguage embedding.
How to build your own solver-aided tool or languageThe classic (hard) way to build a toolWhat is hard about building a solver-aided tool?SDSLSVMSMTAn easier way: tools as languagesHow to build tools by stacking layers of languages.Behind the scenes: symbolic virtual machineHow Rosette works so you don’t have to.A last look: a few recent applicationsCool tools built with Rosette!
How to build your own solver-aided tool or languageThe classic (hard) way to build a toolWhat is hard about building a solver-aided tool?SDSLSVMSMTAn easier way: tools as languagesHow to build tools by stacking layers of languages.Behind the scenes: symbolic virtual machineHow Rosette works so you don’t have to.A last look: a few recent applicationsCool tools built with Rosette!
The classic (hard) way to build a toolverifydebugsolvesynthesizeP(x) { }assert safe(x, P(x))Recall the solver-aided programming toolchain: the tool reduces a query aboutprogram behavior to an SMT problem.solver-aided toolSMT solver x . safe(x, P(x))x 42 safe(x, P(x)) v . safe(42, Pv(42)) e. x. safe(x, Pe(x))
The classic (hard) way to build a toolverifydebugsolvesynthesizeP(x) { }assert safe(x, P(x))Recall the solver-aided programming toolchain: the tool reduces a query aboutprogram behavior to an SMT problem.What all queries have in common: theyneed to translate programs to constraints!solver-aided toolSMT solversymboliccompilerP(x)
The classic (hard) way to build a toolexpeverifydebugsolvesynthesizeP(x) { }assert safe(x, P(x))rtisein PL,FM, SEsymboliccompilerSMT solverP(x)
Wanted: an easier way to build toolsprog ra mmverifydebugsolvesynthesizeP(x) { }assert safe(x, P(x))an interpreterSDSLfor the sourcelanguageing
Wanted: an easier way to build toolsprog ra mmverifydebugsolvesynthesizeP(x) { }assert safe(x, P(x))ingan interpreterSDSLfor the sourcelanguageR SETTEsymbolic virtualSVMmachineSMTsolverSMT
Wanted: an easier way to build toolsverifydebugsolvesynthesizeP(x) { }assert safe(x, P(x))Technical challenge:how to efficientlytranslate a programand its interpreter?[Torlak & Bodik, PLDI’14]an interpreterSDSLfor the sourcelanguageR SETTEsymbolic virtualSVMmachineSMTsolverSMT
How to build your own solver-aided tool or languageThe classic (hard) way to build a toolWhat is hard about building a solver-aided tool?SDSLSVMSMTAn easier way: tools as languagesHow to build tools by stacking layers of languages.Behind the scenes: symbolic virtual machineHow Rosette works so you don’t have to.A last look: a few recent applicationsCool tools built with Rosette!
Layers of classic languages: DSLs and hostsdomain-specific language(DSL)host languageA formal language that isspecialized to a particularapplication domain and oftenlimited in capability.A high-level language forimplementing DSLs, usuallywith meta-programmingfeatures.
Layers of classic languages: DSLs and hostsdomain-specific language(DSL)library(shallow)embeddingA formal language that isspecialized to a particularapplication domain and oftenlimited in capability.interpreter(deep)embeddinghost languageA high-level language forimplementing DSLs, usuallywith meta-programmingfeatures.
Layers of classic languages: many DSLs and hostsartificial intelligenceChurch, BLOGdomain-specific deep)embeddingdatabasesSQL, Dataloghardware designBluespec, Chisel,Verilog,VHDLmath and statisticsEigen, Matlab, Rlayout and visualizationLaTex, dot, dygraphs, D3host languageRacket, Scala, JavaScript,
Layers of classic languages: why DSLs?domain-specific deep)embeddinghost languageEigen / MatlabC A * BC / Javafor (i 0; i n; i )for (j 0; j m; j )for (k 0; k p; k )C[i][k] A[i][j] * B[j][k]
Layers of classic languages: why DSLs?Easier for people to read,write, and get right.domain-specific deep)embeddinghost languageEigen / MatlabC A * BC / Javafor (i 0; i n; i )for (j 0; j m; j )for (k 0; k p; k )C[i][k] A[i][j] * B[j][k]
Layers of classic languages: why DSLs?Easier for people to read,write, and get right.domain-specific deep)embeddinghost languageEigen / MatlabC A * B[associativity]Easier for tools to analyze.C / Javafor (i 0; i n; i )for (j 0; j m; j )for (k 0; k p; k )C[i][k] A[i][j] * B[j][k]
Layers of solver-aided languagessolver-aided domainspecific language beddingsolver-aided host language
Layers of solver-aided languages: tools as SDSLssolver-aided domainspecific language beddingR SETTEeducation and gamesEnlearn, RuleSy (VMCAI’18),Nonograms (FDG’17), UCB feedbackgenerator (ITiCSE'17)synthesis-aided compilationLinkiTools, Chlorophyll (PLDI’14),GreenThumb (ASPLOS’16)type system soundnessBonsai (POPL’18)systems softwareServal (under submission)computer architectureMemSynth (PLDI’17)radiation therapy controlNeutrons (CAV’16) and more
Layers of solver-aided languages: tools as SDSLssolver-aided domainspecific language beddingR SETTEeducation and gamesEnlearn, RuleSy (VMCAI’18),Nonograms (FDG’17), UCB feedbackgenerator (ITiCSE'17)synthesis-aided compilationLinkiTools, Chlorophyll (PLDI’14),GreenThumb (ASPLOS’16)type system soundnessBonsai (POPL’18)systems softwareServal (under submission)computer architectureMemSynth (PLDI’17(PLDI’17)radiation therapy controlNeutrons (CAV’16) and more
A tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6BV: A tiny assembly-likelanguage for writing fast, lowlevel library functions.
A tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6We want to test, verify,debug, and synthesizeprograms in the BV SDSL.BV: A tiny assembly-likelanguage for writing fast, lowlevel library functions.
A tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6We want to test, verify,debug, and synthesizeprograms in the BV SDSL.BV: A tiny assembly-likelanguage for writing fast, lowlevel library functions.1.interpreter[10 LOC]2. verifier[free]3. debugger[free]4.[free]synthesizer
A tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 bvmax(-2, -1)R SETTE
R SETTEA tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 bvmax(-2, -1)parse(define bvmax ((2 bvsge 0 1)(3 bvneg 2)(4 bvxor 0 2)(5 bvand 3 4)(6 bvxor 1 5)))
R SETTEA tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 bvmax(-2, -1)parse(define bvmax ((2 bvsge 0 1)(3 bvneg 2)(4 bvxor 0 2)(5 bvand 3 4)(6 bvxor 1 5)))(out opcode in .)
A tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 bvmax(-2, -1)-1R SETTE(define bvmax ((2 bvsge 0 1)(3 bvneg 2)(4 bvxor 0 2)(5 bvand 3 4)(6 bvxor 1 5)))interpret (-2 -1)(define (interpret prog inputs)(make-registers prog inputs)(for ([stmt prog])(match stmt[(list out opcode in .)(define op (eval opcode))(define args (map load in))(store out (apply op args))]))(load (last)))
A tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 bvmax(-2, -1)-1R SETTE(define bvmax ((2 bvsge 0 1)(3 bvneg 2)(4 bvxor 0 2)(5 bvand 3 4)(6 bvxor 1 5)))interpret0123456-2-100-20-1(define (interpret prog inputs)(make-registers prog inputs)(for ([stmt prog])(match stmt[(list out opcode in .)(define op (eval opcode))(define args (map load in))(store out (apply op args))]))(load (last)))
A tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 bvmax(-2, -1)-1R SETTE(define bvmax ((2(2 bvsge 0 1)(3 bvneg 2)(4 bvxor 0 2)(5 bvand 3 4)(6 bvxor 1 5)))interpret0123456-2-100-20-1(define (interpret prog inputs)(make-registers prog inputs)(for ([stmt prog])(match stmt[(list out opcode in .)(define op (eval opcode))(define args (map load in))(store out (apply op args))]))(load (last)))
A tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 bvmax(-2, -1)-1R SETTE(define bvmax ((2(2 bvsge 0 1)(3 bvneg 2)(4 bvxor 0 2)(5 bvand 3 4)(6 bvxor 1 5)))interpret0123456-2-100-20-1(define (interpret prog inputs)(make-registers prog inputs)(for ([stmt prog])(match stmt[(list out opcode in .)(define op (eval opcode))(define args (map load in))(store out (apply op args))]))(load (last)))
A tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 bvmax(-2, -1)-1R SETTE(define bvmax ((2(2 bvsge 0 1)(3 bvneg 2)(4 bvxor 0 2)(5 bvand 3 4)(6 bvxor 1 5)))interpret0123456-2-100-20-1(define (interpret prog inputs)(make-registers prog inputs)(for ([stmt prog])(match stmt[(list out opcode in .)(define op (eval opcode))(define args (map load in))(store out (apply op args))]))(load (last)))
A tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 bvmax(-2, -1)-1R SETTE(define bvmax ((2(2 bvsge 0 1)(3 bvneg 2)(4 bvxor 0 2)(5 bvand 3 4)(6 bvxor 1 5)))interpret0123456-2-100-20-1(define (interpret prog inputs)(make-registers prog inputs)(for ([stmt prog])(match stmt[(list out opcode in .)(define op (eval opcode))(define args (map load in))(store out (apply op args))]))(load (last)))
A tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 bvmax(-2, -1)-1R SETTE(define bvmax ((2(2 bvsge 0 1)(3 bvneg 2)(4 bvxor 0 2)(5 bvand 3 4)(6 bvxor 1 5)))interpret0123456-2-100-20-1(define (interpret prog inputs)(make-registers prog inputs)(for ([stmt prog])(match stmt[(list out opcode in .)(define op (eval opcode))(define args (map load in))(store out (apply op args))]))(load (last)))
A tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 bvmax(-2, -1)-1R SETTE(define bvmax ((2(2 bvsge 0 1)(3 bvneg 2)(4 bvxor 0 2)(5 bvand 3 4)(6 bvxor 1 5)))interpret0123456-2-100-20-1(define (interpret prog inputs)(make-registers prog inputs)(for ([stmt prog])(match stmt[(list out opcode in .)(define op (eval opcode))(define args (map load in))(store out (apply op args))]))(load (last)))
A tiny example SDSLR SETTEdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6(define bvmax ((2 bvsge 0 1)(3 bvneg 2)(4 bvxor 0 2)(5 bvand 3 4)(6 bvxor 1 5))) bvmax(-2, -1)-1(define (interpret prog inputs)(make-registers prog inputs)(for ([stmt prog])(match stmt[(list out opcode in .)(define op (eval opcode))(define args (map load in))(store out (apply op args))]))(load (last)))‣‣‣‣pattern matchingdynamic evaluationfirst-class & higherorder proceduresside effects
R SETTEA tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 verify(bvmax, max)query(define-symbolic x y int32?)(define in (list x y))(verify(assert (equal? (interpret bvmax in)(interpret max in))))
R SETTEA tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 verify(bvmax, max)Creates two fresh symbolicvalues of type 32-bitinteger and binds them tothe variables x and y.query(define-symbolic x y int32?)(define in (list x y))(verify(assert (equal? (interpret bvmax in)(interpret max in))))
R SETTEA tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 verify(bvmax, max)Creates two fresh symbolicvalues of type 32-bitinteger and binds them tothe variables x and y.query(define-symbolic x y int32?)(define in (list x y))(verify(assert (equal? (interpret bvmax in)(interpret max in))))Symbolic values can beused just like concretevalues of the same type.
R SETTEA tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 verify(bvmax, max)Creates two fresh symbolicvalues of type 32-bitinteger and binds them tothe variables x and y.query(define-symbolic x y int32?)(define in (list x y))(verify(assert (equal? (interpret bvmax in)(interpret max in))))(verify expr) searchesfor a concreteinterpretation ofsymbolic values thatcauses expr to fail.Symbolic values can beused just like concretevalues of the same type.
R SETTEA tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 verify(bvmax, max)[0, -2] bvmax(0, -2)-1query(define-symbolic x y int32?)(define in (list x y))(verify(assert (equal? (interpret bvmax in)(interpret max in))))
R SETTEA tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 verify(bvmax, max)[0, -2] bvmax(0, -2)-1query(define-symbolic x y int32?)(define in (list x y))(verify(assert (equal? (interpret bvmax in)(interpret max in))))
R SETTEA tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 debug(bvmax, max,[0, -2])query(define in (list (int32 0) (int32 -2)))(debug [register?](assert (equal? (interpret bvmax in)(interpret max in))))
R SETTEA tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0, r2)r5 bvand(r3, r4)r6 bvxor(r1, r5)return r6 debug(bvmax, max,[0, -2])query(define in (list (int32 0) (int32 -2)))(debug [register?](assert (equal? (interpret bvmax in)(interpret max in))))
R SETTEA tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(?, ?)r5 bvand(r3, ?)r6 bvxor(?, ?)return r6 synthesize(bvmax, max)query(define-symbolic x y int32?)(define in (list x y))(synthesize#:forall in#:guarantee(assert (equal? (interpret bvmax in)(interpret max in)))))
R SETTEA tiny example SDSLdef bvmax(r0, r1) :r2 bvsge(r0, r1)r3 bvneg(r2)r4 bvxor(r0,bvxor(?, r1)?)r5 bvand(r3, r4)?)r6 bvxor(r1,bvxor(?, r5)?)return r6 synthesize(bvmax, max)query(define-symbolic x y int32?)(define in (list x y))(synthesize#:forall in#:guarantee(assert (equal? (interpret bvmax in)(interpret max in)))))
How to build your own solver-aided tool or languageThe classic (hard) way to build a toolWhat is hard about building a solver-aided tool?SDSLSVMSMTAn easier way: tools as languagesHow to build tools by stacking layers of languages.Behind the scenes: symbolic virtual machineHow Rosette works so you don’t have to.A last look: a few recent applicationsCool tools built with Rosette!
How it all works: a big picture viewqueryprogramSDSLR SETTESymbolicVirtualMachineSMT solverZ3
How it all works: a big picture viewquery resultprogramSDSLR SETTESymbolicVirtualMachineSMT solverZ3
How it all works: a big picture viewquery resultprogram‣‣‣‣‣SDSLR SETTE‣pattern matchingdynamic evaluationfirst-class procedureshigher-order proceduresside effectsmacrosSymbolicVirtualMachinetheories of bitvectors,integers, reals, anduninterpreted functionsSMT solverZ3
Translation to constraints by examplevs(3, 1, -2)solve:ps ()forv inandvs:reversefilter, keepingif positivev 0: numbersonlyps insert(v, ps)assert len(ps) len(vs)ps(1, 3)
Translation to constraints by examplevs(3, 1, -2)solve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)ps(1, 3)
Translation to constraints by examplevssolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)psconstraints
Translation to constraints by examplevs(a, b)solve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)psconstraints
Translation to constraints by examplevs(a, b)solve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)psconstraintsa 0 b 0
Design space of precise symbolic encodingssolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)symbolic executionbounded model checking
Design space of precise symbolic encodingsbounded model checkingsolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)symbolic executionvs (a, b)ps ( )a 0ps (a)b 0ps (a){ }a 0b 0false
Design space of precise symbolic encodingsbounded model checkingsolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)symbolic executiona 0vs (a, b)ps ( )a 0ps (a)ps ( )b 0ps ( )b 0ps (a)b 0ps (b)b 0ps (b, a){ }{ } { }{ }a 0b 0false a 0b 0false a 0b 0false a 0b 0true
Design space of precise symbolic encodingsbounded model checkingsolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)vs (a, b)ps ( )a 0ps ( )symbolic executiona 0a 0ps (a)b 0ps (a)b 0ps (b)b 0ps (b, a){ }{ } { }{ }a 0b 0false a 0b 0falseps (a)ps ps0vs (a, b)ps ( )ps ( )b 0ps ( )a 0 a 0b 0false a 0b 0trueps0 ite(a 0, (a), ( ))ps1 insert(b, ps0)ps2 ite(b 0, ps0, ps1)assert len(ps2) 2
Design space of precise symbolic encodingsbounded model checkingsolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)vs (a, b)ps ( )a 0ps ( )symbolic executiona 0ps (a)b 0ps (a)b 0ps (b) a 0b 0falseb 0ps ps1a 0b 0ps (b, a){ }{ } { }{ }a 0b 0falseps (a)ps ps0vs (a, b)ps ( )ps ( )b 0ps ( )a 0 a 0b 0false a 0b 0trueps0 ite(a 0, (a), ( ))ps1 insert(b, ps0)ps2 ite(b 0, ps0, ps1)assert len(ps2) 2
Design space of precise symbolic encodingsbounded model checkingsolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)vs (a, b)ps ( )a 0ps ( )symbolic executiona 0vs (a, b)ps ( )b 0ps (a)b 0ps (a)b 0ps (b)b 0ps (b, a){ }{ } { }{ }a 0b 0false a 0b 0false a 0b 0false ps (a)ps ps0ps ps0a 0ps ( )b 0ps ( )a 0a 0b 0trueb 0ps ps1ps ps2ps0 ite(a 0, (a), ( ))ps1 insert(b, ps0)ps2 ite(b 0, ps0, ps1)assert len(ps2) 2
A new design: type-driven state mergingsolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs){ }a 0b 0true
A new design: type-driven state mergingsolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)Merge instances of‣ primitive types: symbolically‣ value types:structurally‣ all other types:via unions{ }a 0b 0true
A new design: type-driven state mergingsolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)Merge instances of‣ primitive types: symbolically‣ value types:structurally‣ all other types:via unions⁊ggabc{ }a 0b 0true
A new design: type-driven state mergingsolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)⁊gg(a,ab)Merge instances of‣ primitive types: symbolically‣ value types:structurally‣ all other types:via unions(c,bd)(e,c f){ }a 0b 0true
A new design: type-driven state mergingsolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)Merge instances of‣ primitive types: symbolically‣ value types:structurally‣ all other types:via unions⁊gga(c,()bd){ g (e,a,c f)g () }{ }a 0b 0true
A new design: type-driven state mergingsolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)symbolic virtual machine
A new design: type-driven state mergingsolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)symbolic virtual machinevs (a, b)ps ( )a 0ps ( )a 0ps (a)
A new design: type-driven state mergingsymbolic virtual machinesolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)vs (a, b)ps ( ) g00a ps ( )ga0 0ps (a)ps { g0 (a), g0 ( ) }Symbolic union: a set ofguarded values, withdisjoint guards.g0 a 0g1 b 0g2 g0 g1g3 (g0 g1)g4 g0 g1c ite(g1, b, a)assert g2
A new design: type-driven state mergingExecute insertconcretely on alllists in the union.solve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)symbolic virtual machinevs (a, b)ps ( ) g00a ps ( )ga0 0ps (a)ps { g0 (a), g0 ( ) }g1g0 a 0g1 b 0g2 g0 g1g3 (g0 g1)g4 g0 g1c ite(g1, b, a)assert g2ps { g0 (b, a), g0 (b) }
A new design: type-driven state mergingsymbolic virtual machinesolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)vs (a, b)ps ( ) g00a ps ( )ga0 0ps (a)ps { g0 (a), g0 ( ) } g1g0 a 0g1 b 0g2 g0 g1g3 (g0 g1)g4 g0 g1c ite(g1, b, a)assert g2ps { g0 (a), g0 ( ) }g1ps { g0 (b, a), g0 (b) }
A new design: type-driven state mergingsymbolic virtual machinesolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)vs (a, b)ps ( ) g00a ps ( )ga0 0ps (a)ps { g0 (a), g0 ( ) }g1 g1g0 a 0g1 b 0g2 g0 g1g3 (g0 g1)g4 g0 g1c ite(g1, b, a)assert g2ps { g0 (a), g0 ( ) }ps { g0 (b, a), g0 (b) }ps { g2 (b, a),g3 (c),g4 ( ) }
A new design: type-driven state mergingsymbolic virtual machinesolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)vs (a, b)ps ( ) g00a ps ( )ga0 0ps (a)ps { g0 (a), g0 ( ) }Evaluate len concretelyon all lists in the union;assertion true only onthe list guarded by g2.g1 g1g0 a 0g1 b 0g2 g0 g1g3 (g0 g1)g4 g0 g1c ite(g1, b, a)assert g2ps { g0 (a), g0 ( ) }ps { g0 (b, a), g0 (b) }ps { g2 (b, a),g3 (c),g4 ( ) }
A new design: type-driven state mergingsymbolic virtual machinesolve:ps ()for v in vs:if v 0:ps insert(v, ps)assert len(ps) len(vs)vs (a, b)ps ( ) g00a ps ( )gnidocnnoeiltaaiulmaovneyleotg0 a 0eprcg1 b 0ncog2 g0 g1g3 (g0 g1)g4 g0 g1c ite(g1, b, a)assert g2ga0 0ps (a)ps { g0 (a), g0 ( ) }g1 g1ps { g0 (a), g0 ( ) }ps { g0 (b, a), g0 (b) }ps { g2 (b, a),g3 (c),g4 ( ) }
A new design: type-driven state merging(Sym)Pro tip: use symbolicprofiling to find and repairsolve:performance bottlenecks inps ()for v in vs: your Rosette programs.if v 0:ps insert(v, ps)assert len(ps) len(vs)symbolic virtual machinevs (a, b)ps ( ) g00a ps ( )gnidocnnoeiltaaiulmaovneyleotg0 a 0eprcg1 b 0ncog2 g0 g1g3 (g0 g1)g4 g0 g1c ite(g1, b, a)assert g2ga0 0ps (a)ps { g0 (a), g0 ( ) }g1 g1ps { g0 (a), g0 ( ) }ps { g0 (b, a), g0 (b) }ps { g2 (b, a),g3 (c),g4 ( ) }
How to build your own solver-aided tool or languageThe classic (hard) way to build a toolWhat is hard about building a solver-aided tool?SDSLSVMSMTAn easier way: tools as languagesHow to build tools by stacking layers of languages.Behind the scenes: symbolic virtual machineHow Rosette works so you don’t have to.A last look: a few recent applicationsCool tools built with Rosette!
Verifying a radiation therapy systemClinical Neutron TherapySystem (CNTS) at UW 30 years of incident-free service. Controlled by custom software, builtby CNTS engineering staff. Third generation of Therapy Controlsoftware built recently.
Verifying a radiation therapy systemClinical Neutron TherapySystem (CNTS) at UWPrescriptionSensorsTherapy Control SoftwareBeam, motors, etc.
Verifying a radiation therapy systemClinical Neutron TherapySystem (CNTS) at UWExperimental Physics andIndustrial Control System(EPICS) Dataflow LanguageTherapyEPICSControlSoftwareprogram
Verifying a radiation therapy systemClinical Neutron TherapySystem (CNTS) at UWEPICS programsafety propertyEPICS verifierbug report
Verifying a radiation therapy systemEPICS programsafety propertyPrototyped in a fewdays and found bugs.EPICS verifierCalvin Loncaricbug report
Verifying a radiation therapy systemEPICS programsafety propertyEPICS verifier[Pernsteiner et al.,CAV’16,ICALEPCS’17]Found safety-critical defectsin a pre-release version ofthe therapy control software.bug reportUsed by CNTS staff to verifychanges to the controller.
Synthesizing strategies for games and educationNonograms game mechanics:The numbered hints describe howmany contiguous blocks of cells arefilled with true. Cells filled with trueare marked as a black square andcells filled with false as a red X.
Synthesizing strategies for games and educationNonograms game mechanics:The numbered hints describe howmany contiguous blocks of cells arefilled with true. Cells filled with trueare marked as a black square andcells filled with false as a red X.A computer solves puzzles byreducing the game mechanics tobacktracking search, but humanplayers solve puzzles by usingmultiple strategies to makeprogress without guessing.Finding these strategies is a keychallenge in game design, and isusually done through human testing.
Synthesizing strategies for games and educationThe “big hint” strategy.A computer solves puzzles byreducing the game mechanics tobacktracking search, but humanplayers solve puzzles by usingmultiple strategies to makeprogress without guessing.Finding these strategies is a keychallenge in game design, and isusually done through human testing.
Synthesizing strategies for games and educationThe “big hint” strategy.A computer solves puzzles byreducing the game mechanics tobacktracking search, but humanplayers solve puzzles by usingmultiple strategies to makeprogress without guessing.Finding these strategies is a keychallenge in game design, and isusually done through human testing.
Synthesizing strategies for games and educationGamemechanicsGame states fortraining and testingStrategy DSLsynthesizerAn optimal set of most concise,general, and sound strategies
Synthesizing strategies for games and educationGamemechanicsGame states fortraining and testingPrototyped in a fewweeks and synthesizedreal strategies.Strategy DSLsynthesizerEric ButlerAn optimal set of most concise,general, and sound strategies
Synthesizing strategies for games and educationGamemechanicsGame states fortraining and testing[Butler et al., FDG’17, VMCAI’18]Strategy DSLsynthesizerAn optimal set of most concise,general, and sound strategiesSynthesized strategies thatoutperform documented strategiesfor Nonograms, both in terms ofcoverage and quality.Also used to synthesize strategiesfor solving K-12 algebra and proofsfor propositional logic, recoveringand outperforming textbookstrategies for these domains.
Verifying systems softwareAn OS is a set of software componentsthat mediate access to hardware andprovide services to user applications.applicationsJITsecurityfilecompilers monitors systemsOS kernelhardwaredevicedrivers
Verifying systems softwareAn OS is a set of software componentsthat mediate access to hardware andprovide services to user applications.applicationsJITsecurityfilecompilers monitors systemsdevicedriversOS kernelhardwareBugs in OS components are bad newsfor reliability, security, andperformance of computer systems.
Verifying systems softwareAn OS is a set of software componentsthat mediate access to hardware andprovide services to user applications.applicationsJITsecurityfilecompilers monitors systemsdevicedriversOS kernelhardwareBugs in OS components are bad newsfor reliability, security, andperformance of computer systems.Verifying OS components is hard:e.g., the seL4 kernel took 11 personyears to prove, with a proof-toimplementation ratio of 20:1.
Verifying systems softwareAn OS is a set of software componentsthat mediate access to hardware andprovide services to user applications.SystemspecificationSystem ompilers monitors systemsdevicedriversOS kernelServal verifiers(RISCV, x86, )hardwareBugs in OS components are bad newsfor reliability, security, andperformance of computer systems.Bug report or correctnessguarantee
Verifying systems softwareSystemspecificationSystem (binary)implementationEach verifier took acouple of weeks tobuild!Serval verifiers(RISCV, x86, )Luke NelsonBug report or correctnessguarantee
Verifying systems softwareSystemspecificationSystem (binary)implementationServal verifiers(RISCV, x86, )Bug report or correctnessguarantee[Nelson et al., under submission]Verified three existing securitymonitors (CertiKOS, Komodo,Keystone) fully automatically andwith low proof burden.Found and patched 15 bugs inthe Linux BPF JITs for RISCV64and x86-32.
thanks
verifyyour SDSLdebugsolvesynthesizethanksR SETTEsymbolic virtual machine
solver-aided languagesolver-aided tool via direct symbolic evaluation or . program behavior to an SMT problem. SMT solver The classic (hard) way to build a tool solver-aided tool P(x) symbolic compiler assert safe(x, P( x)) verify debug . math and statistics Eigen, Matlab, R
