Lightweight and modular resource leak checking (extended version)

A resource leak occurs when a program allocates a resource but fails to deallocate it. Resource leaks cause resource starvation, slowdowns, and crashes. Previous techniques to prevent resource leaks are either unsound, imprecise, inapplicable to existing code, slow, or a combination of these. We present a resource leak checking approach that is applicable, sound, precise, and fast. Our key insight is that leak detection can be reduced to an accumulation problem, a class of typestate problems amenable to sound and modular checking without whole-program alias analysis. The precision of an accumulation analysis can be improved with targeted aliasing information, and we augmented our baseline checker with three such novel techniques: a lightweight ownership transfer system; a specialized resource alias analysis; and a system to create a fresh obligation when a nonfinal resource field is updated. Our approach occupies a unique slice of the design space: it is sound and runs relatively quickly (taking minutes on programs that a state-of-the-art approach took hours to analyze). Moreover, our approach generalizes to multiple analysis backends. The Resource Leak Checker revealed 49 real resource leaks in widely-deployed software; RLC# revealed 24 real resource leaks in five programs, including three Azure microservices. Both implementations scale well, have manageable false positive rates (comparable to heuristic bug-finders), and impose only a small annotation burden (about 1/6000 LoC) for developers. This is an extended version of an ESEC/FSE 2021 publication. The key new contribution of this work is the introduction of the RLC# tool for checking of C# code. We describe the implementation of RLC# as a reachability-based analysis built on CodeQL (quite different than the previous approach) and present an evaluation of its effectiveness.