PIP: Making Andersen's Points-to Analysis Sound and Practical for Incomplete C Programs
H{\aa}vard Rognebakke Krogstie, Helge Bahmann, Magnus Sj\"alander, Nico Reissmann

TL;DR
This paper introduces PIP, an Andersen-style points-to analysis for incomplete C programs that is both sound and highly efficient, significantly outperforming existing methods in speed and reducing aliasing uncertainty.
Contribution
It presents a novel implicit pointee tracking technique and the PIP method, enabling sound, fast, and scalable points-to analysis for incomplete programs without summary functions.
Findings
Implicit pointee tracking makes the solver 15× faster.
PIP reduces explicit pointees, achieving an additional 1.9× speedup.
Analysis decreases MayAlias-responses by 40% compared to LLVM's BasicAA.
Abstract
Compiling files individually lends itself well to parallelization, but forces the compiler to operate on incomplete programs. State-of-the-art points-to analyses guarantee sound solutions only for complete programs, requiring summary functions to describe any missing program parts. Summary functions are rarely available in production compilers, however, where soundness and efficiency are non-negotiable. This paper presents an Andersen-style points-to analysis that efficiently produces sound solutions for incomplete C programs. The analysis accomplishes soundness by tracking memory locations and pointers that are accessible from external modules, and efficiency by performing this tracking implicitly in the constraint graph. We show that implicit pointee tracking makes the constraint solver 15 faster than any combination of five different state-of-the-art techniques using explicit…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Parallel Computing and Optimization Techniques · Formal Methods in Verification
