Fast polyhedra abstract domain

Gagandeep Singh, Markus Püschel, Martin Vechev

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationPOPL 2017 - Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
EditorsAndrew D. Gordon, Giuseppe Castagna
PublisherAssociation for Computing Machinery
Pages46-59
Number of pages14
ISBN (Electronic)9781450346603
DOIs
StatePublished - Jan 1 2017
Externally publishedYes
Event44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017 - Paris, France
Duration: Jan 15 2017Jan 21 2017

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
ISSN (Print)0730-8566

Conference

Conference44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017
Country/TerritoryFrance
CityParis
Period1/15/171/21/17

Keywords

  • Abstract interpretation
  • Numerical program analysis
  • Partitions
  • Performance optimization
  • Polyhedra decomposition

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Fast polyhedra abstract domain'. Together they form a unique fingerprint.

Cite this