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.

翻译：资源泄漏是指程序在不再需要某些有限资源后未能释放它们的情况。这类泄漏是实际系统崩溃和性能问题的重要诱因。近期研究提出了一种基于检查资源管理规范来预防资源泄漏的方法。这些规范以程序注解的形式编写，用于追踪对象与资源之间的所有权关系。尽管这种“规范-检查”方法与先前的技术相比具有若干优势，但需要手动编写注解的要求严重阻碍了其实际部署。本文提出了一种新技术，可自动推断程序的资源管理规范，从而扩展了基于规范检查的资源泄漏验证技术的适用性。该领域的推断面临重大挑战，因为资源管理规范在本质上与大多数推断技术所针对的类型存在显著差异。此外，为了实际有效性，我们需要一种即使在代码未完全遵循规范的情况下，也能推断出开发者意图的资源管理规范的技术。我们通过精心设计一组能捕捉真实编码模式的推断规则来应对这些挑战，从而形成了基于不动点的高效推断算法。我们在两个不同系统中实现了该推断算法，分别针对Java和C#编程语言。实验评估表明，我们的技术能推断出87%为基准程序手动编写的注解。此外，在完全自动推断后运行的验证器对资源泄漏漏洞的检测真阳性率几乎接近代码手动注解后的检测率。