Solving Shape-Analysis Problems in Languages with Destructive Updating

Abstract

This paper concerns the static analysis of programs that perform destructive updating on heap-allocated storage. We give an algorithm that conservatively solves this problem by using a finite shape-graph to approximate the possible "shapes" that heap-allocated structures in a program can take on. In contrast with previous work, our method is even accurate for certain programs that update cyclic data structures. For example, our method can determine that when the input to a program that searches a list and splices in a new element is a possibly circular list, the output is a possibly circular list.