TY - GEN
T1 - Fast polyhedra abstract domain
AU - Singh, Gagandeep
AU - Püschel, Markus
AU - Vechev, Martin
N1 - Publisher Copyright:
© 2017 ACM.
PY - 2017/1/1
Y1 - 2017/1/1
N2 - Numerical abstract domains are an important ingredient of modern static analyzers used for verifying critical program properties (e.g., absence of buffer overflow or memory safety). Among the many numerical domains introduced over the years, Polyhedra is the most expressive one, but also the most expensive: it has worst-case exponential space and time complexity. As a consequence, static analysis with the Polyhedra domain is thought to be impractical when applied to large scale, real world programs. In this paper, we present a new approach and a complete implementation for speeding up Polyhedra domain analysis. Our approach does not lose precision, and for many practical cases, is orders of magnitude faster than state-of-the-art solutions. The key insight underlying our work is that polyhedra arising during analysis can usually be kept decomposed, thus considerably reducing the overall complexity. We first present the theory underlying our approach, which identifies the interaction between partitions of variables and domain operators. Based on the theory we develop new algorithms for these operators that work with decomposed polyhedra. We implemented these algorithms using the same interface as existing libraries, thus enabling static analyzers to use our implementation with little effort. In our evaluation, we analyze large benchmarks from the popular software verification competition, including Linux device drivers with over 50K lines of code. Our experimental results demonstrate massive gains in both space and time: we show endto- end speedups of two to five orders of magnitude compared to state-of-the-art Polyhedra implementations as well as significant memory gains, on all larger benchmarks. In fact, in many cases our analysis terminates in seconds where prior code runs out of memory or times out after 4 hours. We believe this work is an important step in making the Polyhedra abstract domain both feasible and practically usable for handling large, real-world programs.
AB - Numerical abstract domains are an important ingredient of modern static analyzers used for verifying critical program properties (e.g., absence of buffer overflow or memory safety). Among the many numerical domains introduced over the years, Polyhedra is the most expressive one, but also the most expensive: it has worst-case exponential space and time complexity. As a consequence, static analysis with the Polyhedra domain is thought to be impractical when applied to large scale, real world programs. In this paper, we present a new approach and a complete implementation for speeding up Polyhedra domain analysis. Our approach does not lose precision, and for many practical cases, is orders of magnitude faster than state-of-the-art solutions. The key insight underlying our work is that polyhedra arising during analysis can usually be kept decomposed, thus considerably reducing the overall complexity. We first present the theory underlying our approach, which identifies the interaction between partitions of variables and domain operators. Based on the theory we develop new algorithms for these operators that work with decomposed polyhedra. We implemented these algorithms using the same interface as existing libraries, thus enabling static analyzers to use our implementation with little effort. In our evaluation, we analyze large benchmarks from the popular software verification competition, including Linux device drivers with over 50K lines of code. Our experimental results demonstrate massive gains in both space and time: we show endto- end speedups of two to five orders of magnitude compared to state-of-the-art Polyhedra implementations as well as significant memory gains, on all larger benchmarks. In fact, in many cases our analysis terminates in seconds where prior code runs out of memory or times out after 4 hours. We believe this work is an important step in making the Polyhedra abstract domain both feasible and practically usable for handling large, real-world programs.
KW - Abstract interpretation
KW - Numerical program analysis
KW - Partitions
KW - Performance optimization
KW - Polyhedra decomposition
UR - http://www.scopus.com/inward/record.url?scp=85015296392&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85015296392&partnerID=8YFLogxK
U2 - 10.1145/3009837.3009885
DO - 10.1145/3009837.3009885
M3 - Conference contribution
AN - SCOPUS:85015296392
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 46
EP - 59
BT - POPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
A2 - Gordon, Andrew D.
A2 - Castagna, Giuseppe
PB - Association for Computing Machinery
T2 - 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017
Y2 - 15 January 2017 through 21 January 2017
ER -