Automatic Inference of Resource Leak Specifications

A resource leak occurs when a program fails to free some finite resource after it is no longer needed. Such leaks are a significant cause of real-world crashes and performance problems. Recent work proposed an approach to prevent resource leaks based on checking resource management specifications. These specifications are written in the form of program annotations that track the ownership relationship between objects and resources. While this specify-and-check approach has several advantages compared to prior techniques, the need to manually write annotations presents a significant barrier to its practical adoption. This paper presents a novel technique to automatically infer a resource management specification for a program, broadening the applicability of specify-and-check verification for resource leaks. Inference in this domain poses significant challenges because resource management specifications differ significantly in nature from the types that most inference techniques target. Further, for practical effectiveness, we desire a technique that can infer the resource management specification intended by the developer, even in cases when the code does not fully adhere to this specification. We address these challenges through a set of inference rules carefully designed to capture real-world coding patterns, yielding an effective fixed-point-based inference algorithm. We have implemented our inference algorithm in two different systems, targeting programs in the Java and C# programming languages. An experimental evaluation showed that our technique could infer 87% of the annotations written manually for the benchmarks. Further, the true positive rate for resource leak bugs achieved by the verifier when run after our fully-automatic inference nearly matched the rate achieved after manual annotation of the code.