Precise null-pointer analysis using Global Value Numbering

Automated Technology for Verification and Analysis (ATVA) |

Precise analysis of pointer information plays an important role in many static
analysis tools. The precision, however, must be balanced
against the scalability of the analysis. This paper focusses on improving the
precision of standard context and flow insensitive alias analysis algorithms
at a low scalability cost. In particular, we present a semantics-preserving
program transformation that drastically improves the precision of existing
analyses when deciding if a pointer can alias null.
Our program transformation is based on Global Value Numbering, a scheme
inspired from compiler optimization literature. It allows even a flow-insensitive
analysis to make use of branch conditions such as checking if a pointer is null
and gain precision.

We perform experiments on real-world code and show
that the transformation improves precision (in terms of the number of dereferences proved safe)
from 86.56% to 98.05%, while incurring a small overhead in the running time.