TY - GEN
T1 - Design and implementation of sparse global analyses for C-like languages
AU - Oh, Hakjoo
AU - Heo, Kihong
AU - Lee, Wonchan
AU - Lee, Woosuk
AU - Yi, Kwangkeun
PY - 2012
Y1 - 2012
N2 - In this article we present a general method for achieving global static analyzers that are precise, sound, yet also scalable. Our method generalizes the sparse analysis techniques on top of the abstract interpretation framework to support relational as well as non-relational semantics properties for C-like languages. We first use the abstract interpretation framework to have a global static analyzer whose scalability is unattended. Upon this underlying sound static analyzer, we add our generalized sparse analysis techniques to improve its scalability while preserving the precision of the underlying analysis. Our framework determines what to prove to guarantee that the resulting sparse version should preserve the precision of the underlying analyzer. We formally present our framework; we present that existing sparse analyses are all restricted instances of our framework; we show more semantically elaborate design examples of sparse nonrelational and relational static analyses; we present their implementation results that scale to 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.
AB - In this article we present a general method for achieving global static analyzers that are precise, sound, yet also scalable. Our method generalizes the sparse analysis techniques on top of the abstract interpretation framework to support relational as well as non-relational semantics properties for C-like languages. We first use the abstract interpretation framework to have a global static analyzer whose scalability is unattended. Upon this underlying sound static analyzer, we add our generalized sparse analysis techniques to improve its scalability while preserving the precision of the underlying analysis. Our framework determines what to prove to guarantee that the resulting sparse version should preserve the precision of the underlying analyzer. We formally present our framework; we present that existing sparse analyses are all restricted instances of our framework; we show more semantically elaborate design examples of sparse nonrelational and relational static analyses; we present their implementation results that scale to 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.
KW - Abstract interpretation
KW - Sparse analysis
KW - Static analysis
UR - http://www.scopus.com/inward/record.url?scp=84863422824&partnerID=8YFLogxK
U2 - 10.1145/2254064.2254092
DO - 10.1145/2254064.2254092
M3 - Conference contribution
AN - SCOPUS:84863422824
SN - 9781450312059
T3 - Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
SP - 229
EP - 238
BT - PLDI'12 - Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation
T2 - 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI'12
Y2 - 11 June 2012 through 16 June 2012
ER -