Combining range and inequality information for pointer disambiguation

Pentagons is an abstract domain invented by Logozzo and Fähndrich to validate array accesses in low-level programming languages. This algebraic structure provides a cheap “less-than check”, which builds a partial order between the integer variables used in a program. In this paper, we show how we ha...

Full description

Saved in:
Bibliographic Details
Published in:Science of computer programming 2018-01, Vol.152, p.161-184
Main Authors: Maalej, Maroua, Paisante, Vitor, Magno Quintão Pereira, Fernando, Gonnord, Laure
Format: Article
Language:English
Subjects:
Abstract interpretation
Compiler construction
Less-than check
Pentagons
Points-to analysis
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Pentagons is an abstract domain invented by Logozzo and Fähndrich to validate array accesses in low-level programming languages. This algebraic structure provides a cheap “less-than check”, which builds a partial order between the integer variables used in a program. In this paper, we show how we have used the ideas available in Pentagons to design and implement a novel alias analysis. With this new algorithm, we are able to disambiguate pointers with offsets, that commonly occur in C programs, in a precise and efficient way. Together with this new abstract domain we describe several implementation decisions that let us produce a practical pointer disambiguation algorithm on top of the LLVM compiler. Our alias analysis is able to handle programs as large as SPEC CPU2006's gcc in a few minutes. Furthermore, it improves on LLVM's industrial quality analyses. As an extreme example, we have observed a 4x improvement when analyzing SPEC's lbm.
ISSN:0167-6423
1872-7964
DOI:10.1016/j.scico.2017.10.014