A lightweight symbolic virtual machine for solver-aided host languages

Emina Torlak, Rastislav Bodik
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer]
Read: 16 November 2019

Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation
PLDI'14
Edinburgh, United Kingdom
ACM
New York, NY, USA
Pages 530-541
2014
Topic(s): tools verification
Note(s): Rosette solver, symbolic evaluation, symbolic execution, bounded model checking, state merging, case splitting
Papers: nelson:sosp:2019

Rosette is a Racket DSL for implementing Solver-aided Domain Specific Languages (SDSLs): tools based on solvers that support angelic execution, debugging, verifying properties and synthesis. A key feature of Rosette is “symbolic reflection” – that allows Racket code to be symbolically evaluated (in addition to being executable in the normal way).

Rosette lies somewhere between symbolic execution (that enumerates all paths and solves constraints along each path) and bounded model checking. Like bounded model checking, Rosette depends on finitizing the program being reasoned about but it differs in that the program may be “self-finitizing”: instead of simply unrolling loops to some limit, any constant parts of the input/program, are used to determine how much to unroll loops. Indeed, a key insight seems to be that SDSL’s have a significant amount of concrete evaluation in loops/recursion.

Rosette also differs from [bounded model-checking] in how it merges symbolic values: for each shape of the values, a separate symbolic value is constructed.

Rosette is demonstrated/evaluated on an OpenCL synthesis task, an XPath synthesis task and an information flow verification task.

This forms the basis of a number of other projects including Serval.

There are a number of optimizations to make Rosette perform well: type-driven state merging (using the shape of data structures to determine which states to merge); [case-splitting] using the for/all construct. More broadly, Rosette introduced “symbolic reflection”: an API for inspecting and manipulating symbolic values, the term cache, etc. to enable efficient implementation.

Rosette solver

  • Finding code that explodes under symbolic evaluation [bornholt:oopsla:2018]
  • Scaling symbolic evaluation for automated verification of systems code with Serval [nelson:sosp:2019]
  • SpaceSearch: A library for building and verifying solver-aided tools [weitz:icfp:2017]