This project explores novel heap abstractions and analyses that use local reasoning about single heap cells. Our approach uses local heap abstractions to describe the state of single heap cells, instead of global heap abstractions (such as shape graphs) that describe entire heaps. This makes it possible to build scalable, but accurate intra-procedural and inter-procedural heap analyses. Our shape analysis implementations have been successfully applied to programs of tens of thousands of lines of C and Java code. We investigate the application of this technology to problems that require reasoning about memory and aliases, including memory error detection, memory management, and verification of safety properties properties.
Software
Download shape-suif.tgz, a heap error detection tool for C programs that uses shape analysis with tracked cells. This is an implementation in the SUIF1 compiler infrastructure. An implementation of shape analysis for C in the Crystal framework is currently under development.
Publications
- Region-Based Shape Analysis with Tracked Locations
B. Hackett and R. Rugina, POPL'05
This paper presents a formulation of shape analysis with tracked cells for C programs. The analysis uses a region partitioning of the memory using a unification-based pointer analysis. The analysis has been used to verify heap shapes and to implement a heap error-detection tool that finds memory leaks, double frees, dangling pointer violations. The implementation used in this paper can be downloaded above.
- Maintaining Doubly-Linked List Invariants in Shape Analysis with Local
Reasoning
S. Cherem and R. Rugina. VMCAI '07
This paper shows how to use shape analysis with tracked cells to analyze structures with local invariants, such as doubly-linked lists. The analysis uses a more advanced local abstraction that captures information about the neighbors of the tracked cell. This includes points-to information between the tracked cell and its neighbors, allowing the analysis to express local invariants such as doubly-linked list invariants.
- Compile-Time Deallocation of Individual Objects
S. Cherem and R. Rugina, ISMM'06.
The paper presents a formulation of shape analysis with tracked cells for Java programs, and its application to compile-time memory management. The analysis is used in a compiler that automatically inserts free() statements in Java programs. Shape analysis identifies where heap objects lose their last reference, and directs the compiler to insert frees at those points. The analysis relies on type-safety and uses types to provide a region partitioning. An implementation is available on the Jfree project website.
- Memory
Leak Analysis by Contradiction
M. Orlovich and R. Rugina, SAS'06.
This paper describes a heap analysis that aims at identifying memory leaks by disproving their presence. For heap pointer assignment, the analysis assumes that the assignment might cause a leak, and then performs a backward dataflow analysis to disprove the assumption. The analysis uses local reasoning about the error cell, the cell that is assumed to leak, and performs a backward analysis of this single cell. An implementation is available on the Leak Contradictor project website.
Related projects
- Shape analysis:
- TVLA : shape analysis using 3-valued logic
- Space
Invader: shape analysis using separation logic
- Error detection (with focus on heap error detection):
Current and Past Members:
- Radu Rugina
- Siggi Cherem
- Maksim Orlovich
- Brian Hackett (now at Stanford)