Finding Code That Explodes Under Symbolic Evaluation

on YouTube ↗23m

" summary

A profiler called SymPro constructs a symbolic evaluation graph and a symbolic heap to locate where symbolic evaluation explodes, implemented for Rosette and Jalangi. Running it on 15 published solver-aided tools finds eight previously undiagnosed bottlenecks; fixes are local program edits that yield up to 300× speedups and were accepted by developers. The work also catalogs three actionable anti‑patterns (algorithmic mismatch, irregular representation, mistaken concretization) and shows users find performance bugs faster with the profiler.

AI-written summary · about

" chapters (12)

1. 0:00Intro
2. 0:16Automated reasoning tools help us solve hard programming problems
3. 2:10Symbolic evaluators: no free lunch
4. 4:09Symbolic evaluation executes all paths through a program
5. 8:09Two data structures to summarize symbolic evaluation
6. 9:10The symbolic evaluation graph summarizes branching and merging
7. 11:33The symbolic heap shows how symbolic values are used
8. 12:49Analyzing symbolic data structures
9. 13:53Common anti-patterns and repairs in symbolic evaluation
10. 17:33Three symbolic profilers We developed two implementations
11. 18:21Actionable: real-world bugs Case studies on published Rosette-based tools
12. 20:30Symbolic profiling identifies performance issues in symbolic evaluation