Abstract:
There are many operations about shared and mutable data structures in heap-manipulating programs, such as allocation, combination, separation, deletion, and so on. Therefore, memory leak detection for these programs requires precise field-sensitive pointer alias information, which becomes more complex and harder to deal with. A novel field-sensitive heap abstraction approach based on extended pointer types is proposed for heap-manipulating programs in this paper. The approach computes the local layout around pointer variables in the heap, and therefore supports local reasoning for heap. The pointer alias sets are computed about the memory cells, which are reached by the pointer along various pointer fields in the given abstract distance domain. Various operation semantics about all basic statements based on extended pointer types are defined and a new algorithm runs typical forward dataflow iteration analysis to see whether there are any memory leaks. Our algorithm also supports both intra- and inter- procedural analysis. We have implemented the prototype tool (Heapcheck) for C programs in the Crystal open compiler framework to support detecting memory leaks about different pointer fields in complex data structures. Experimental evaluation about a set of C benchmark programs shows that the proposed approach has better scalability and precision than current work.