Global Sparse Analysis Framework

• Published in: ACM transactions on programming languages and systems 2014-09, Vol.36 (3), p.1-44, Article 8
• Main Authors: Oh, Hakjoo, Heo, Kihong, Lee, Wonchan, Lee, Woosuk, Park, Daejun, Kang, Jeehoon, Yi, Kwangkeun
• Format: Article
• Language: English
• Subjects: Analyzers; C (programming language); Design engineering; Economic analysis; Preserves; Program semantics; Programming languages; Semantics; Semantics and reasoning; Sound; Theory of computation
• ISSN: 0164-0925; 1558-4593
• DOI: 10.1145/2590811

In this article, we present a general method for achieving global static analyzers that are precise and sound, yet also scalable. Our method, on top of the abstract interpretation framework, is a general sparse analysis technique that supports relational as well as nonrelational semantics properties for various programming languages. Analysis designers first use the abstract interpretation framework to have a global and correct static analyzer whose scalability is unattended. Upon this underlying sound static analyzer, analysis designers add our generalized sparse analysis techniques to improve its scalability while preserving the precision of the underlying analysis. Our method prescribes what to prove to guarantee that the resulting sparse version should preserve the precision of the underlying analyzer. We formally present our framework and show that existing sparse analyses are all restricted instances of our framework. In addition, we show more semantically elaborate design examples of sparse nonrelational and relational static analyses. We then present their implementation results that scale to globally analyze up to one million lines of C programs. We also show a set of implementation techniques that turn out to be critical to economically support the sparse analysis process.