Generalized Points-to Graphs: A New Abstraction of Memory in the Presence of Pointers
Pritam M. Gharat, Uday P. Khedker, Alan Mycroft

TL;DR
The paper introduces Generalized Points-to Graphs (GPGs), a novel memory abstraction that improves the scalability of flow- and context-sensitive points-to analysis by compactly representing procedure summaries through memory updates and control flow optimizations.
Contribution
It presents GPGs as a scalable, precise abstraction for points-to analysis, incorporating new optimizations like strength reduction, redundancy elimination, and call inlining.
Findings
GPGs are significantly smaller than traditional summaries.
The approach scales to 158kLoC C programs.
GPGs maintain precision while discarding unnecessary control flow.
Abstract
Flow- and context-sensitive points-to analysis is difficult to scale; for top-down approaches, the problem centers on repeated analysis of the same procedure; for bottom-up approaches, the abstractions used to represent procedure summaries have not scaled while preserving precision. We propose a novel abstraction called the Generalized Points-to Graph (GPG) which views points-to relations as memory updates and generalizes them using the counts of indirection levels leaving the unknown pointees implicit. This allows us to construct GPGs as compact representations of bottom-up procedure summaries in terms of memory updates and control flow between them. Their compactness is ensured by the following optimizations: strength reduction reduces the indirection levels, redundancy elimination removes redundant memory updates and minimizes control flow (without over-approximating data…
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
TopicsParallel Computing and Optimization Techniques · Logic, programming, and type systems · Formal Methods in Verification
