Prototyping symbolic execution engines for interpreted languages. / Bucur, Stefan; Kinder, Johannes; Candea, George.

Proc. Architectural Support for Programming Languages and Operating Systems (ASPLOS 2014). ACM, 2014. p. 239-254.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Published

Documents

  • asplos14

    Accepted author manuscript, 780 KB, PDF document

Abstract

Symbolic execution is being successfully used to automatically test statically compiled code. However, increasingly more systems and applications are written in dynamic interpreted languages like Python. Building a new symbolic execution engine is a monumental effort, and so is keeping it up-to-date as the target language evolves. Furthermore, ambiguous language specifications lead to their implementation in a symbolic execution engine potentially differing from the production interpreter in subtle ways.

We address these challenges by flipping the problem and using the interpreter itself as a specification of the language semantics. We present a recipe and tool (called Chef) for turning a vanilla interpreter into a sound and complete symbolic execution engine. Chef symbolically executes the target program by symbolically executing the interpreter's binary while exploiting inferred knowledge about the program's high-level structure.

Using Chef, we developed a symbolic execution engine for Python in 5 person-days and one for Lua in 3 person-days. They offer complete and faithful coverage of language features in a way that keeps up with future language versions at near-zero cost. Chef-produced engines are up to 1000 times more performant than if directly executing the interpreter symbolically without Chef.
Original languageEnglish
Title of host publicationProc. Architectural Support for Programming Languages and Operating Systems (ASPLOS 2014)
PublisherACM
Pages239-254
ISBN (Electronic)978-1-4503-2305-5
DOIs
Publication statusPublished - 2014
This open access research output is licenced under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.

ID: 19287939