On Scalable Shape Analysis
Hongseok Yang, Oukseh Lee, Cristiano Calcagno, Dino Distefano, Peter W. O’Hearn · 2007
Shape analysis is a precise form of pointer analysis, which can be used to verify deep properties of data structures such as whether or not they are cyclic, whether they are nested, etc. Shape analyses are also expensive, and the tremendous number of abstract states they generate is an impediment to their use in verification of sizeable programs. We start with an analysis that is able to analyze programs up to 1000 lines manipulating complex, nested structures, and progressively improve it until it is capable of analyzing programs of up to 10,000 lines. By experimental results we show that our analysis is precise. It identifies memory safety errors and memory leaks in several Windows and Linux device drivers and, after these bugs are fixed, it automatically proves integrity of pointer manipulation for these drivers. This order of magnitude improvement in sizes of programs verified is obtained by combining several ideas. One is the local reasoning idea of separation logic, which reduces recomputation of analysis of procedure bodies, and which allows efficient transfer functions for primitive program statements. Another is an interprocedural analysis algorithm which aggressively discards intermediate states. The most important new technical contribution of the work is a new join operator, which greatly reduces the number of