Symbolic profiling and repair

Many tools rely on symbolic evaluation to reduce programming tasks, such as verification and synthesis, to satisfiability queries. Using a symbolic evaluator effectively requires tool developers to be able to identify and repair performance bottlenecks in code under all-path evaluation, a difficult task, even for experts. SymPro and SymFix are systems that automate this task.

SymPro implements symbolic profiling, a new approach to identifying performance bottlenecks in programs under symbolic evaluation. SymPro identifies bottlenecks by analyzing two implicit resources at the core of every symbolic evaluation engine, the symbolic heap and symbolic evaluation graph. These resources form a general performance model of symbolic evaluation.

SymFix implements a new method for repairing bottlenecks found by SymPro. The key idea is to formulate the symbolic performance repair problem as combinatorial search through a space of semantics-preserving transformations, or repairs, to find an equivalent program with minimal cost under symbolic evaluation. SymFix uses symbolic profiling to guide the search for repairs.

Applications

SymPro is integrated into the Rosette solver-aided language and the Crucible symbolic evaluation engine developed by Galois. It has been used to develop the Serval verification framework, and find and repair performance bottlenecks in many existing Rosette-based tools.

Publications

• Sorawee Porncharoenwase, James Bornholt, and Emina Torlak. Fixing Code That Explodes Under Symbolic Evaluation. In Proc. of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), Jan 2020. [pdf]

• James Bornholt and Emina Torlak. Finding Code That Explodes Under Symbolic Evaluation. In Proc. of the 33rd Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), Nov 2018. [pdf] Distinguished artifact award

Documentation

The Rosette Guide: Performance

Software

SymPro is integrated into Rosette at https://github.com/emina/rosette. The artifact for the OOPSLA 2018 paper is available here.

SymFix is available at https://github.com/uw-unsat/symfix-vmcai20.