Abstract
Decision procedures have helped automate key aspects of programming: coming up with a code fragment that implements a desired behavior (synthesis); establishing that an implementation satisfies a desired property (code checking); locating code fragments that cause an undesirable behavior (fault localization); and running a partially implemented program to test its existing behaviors (angelic execution). Each of these aspects is supported, at least in part, by a family of formal tools. Most such tools are built on infrastructures that are tailored for a particular language or purpose, e.g., Boogie for verification and Sketch for synthesis of C-like languages. But so far, no single infrastructure provides a platform for automating the full spectrum of programming activities, or for making such automation easily available in new languages and programming models.
This talk introduces Rosette, a new shared infrastructure for designing and growing solver-aided languages. The Rosette system is itself a solver-aided EDSL (embedded domain-specific language), which inherits and exposes extensive support for meta programming from its host language, Racket. The system works through a combination of program transformation (enabled by Racket’s meta-programming facilities) and symbolic execution, in which programming constructs and operators accept both concrete and symbolic values. With our framework, a designer defines a new solver-aided language by simply writing an interpreter for it in Rosette. Such a language will allow some constructs to be underspecified---that is, to produce symbolic "holes" rather than just concrete values. When a program with holes and the language interpreter are compiled with Rosette, the result is a custom symbolic execution engine for the given program and language. Executing this engine yields an encoding of the program’s semantics as a set of constraints, which are then solved by an off-the-shelf decision procedure to discharge synthesis, verification, and other queries about the program. We show how to use Rosette to prototype a tiny DSL with a program checker, a fault localizer, an angelic oracle, and
an inductive synthesizer.
