Taking out the Toxic Trash: Recovering Precision in Mixed Flow-Sensitive Static Analyses
summary
Proposes three concrete fixes — narrowing per origin, reluctant widening, and abstract garbage collection — that decouple global updates via an update rules interface, implement them in the Goblin analyzer for multithreaded C, and measure effects on SV-COMP and real-world suites: 52% of tasks see net precision gain (20% substantial), 2% net loss, and roughly 3% average runtime overhead; precision losses largely disappear when combined with widening delay.
AI-written summary · about
chapters (16)
- 0:00Mixed flow sensitivity intro
- 1:02Flow sensitivity applications
- 2:27Widening problem with globals
- 3:50Precision loss from widening
- 4:50Widening and narrowing per origin
- 5:55Decoupling globals with rules
- 7:21Soundness of solvers and rules
- 8:23Implementing widening/narrowing
- 9:06Update rule example
- 12:17Toxic trash problem
- 13:39Abstract garbage collection
- 14:00Paper contributions and theorem
- 14:43SV-COMP benchmarks eval
- 15:44Precision and runtime results
- 16:27Summary of findings
- 17:11Q&A
related talks
15mNot So Fast: Understanding and Mitigating Negative Impacts of Compiler Optimizations on Code Reuse G
22mReconciling Progress-Intensive Noninterference and Declassification
01h 01mClosing the Gap between Rust and C++ Using Principles of Static Analysis
40mCatching More Bugs with Fewer False Alarms
38mFixing your performance and concurrency bugs
01h 00mSanitize for your Sanity: Sanitizers tools for Modern C++
24mSNIP: Speculative Execution and Non-Interference Preservation for Compiler(…)
01h 01mSecurity: from Transistors to Compilers