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. A resource management specification expresses how the program allocates resources, passes them around, and releases them; it also tracks the ownership relationship between objects and resources, and aliasing relationships between objects. While this specify-and-verify 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 is challenging 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 that 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 written in Java and C#. In an experimental evaluation, our technique inferred 85.5% of the annotations that programmers had written manually for the benchmarks. Further, the verifier issued nearly the same rate of false alarms with the manually-written and automatically-inferred annotations.

翻译：资源泄漏是指程序在不再需要某些有限资源后未能释放它们的情况。此类泄漏是实际系统崩溃和性能问题的重要原因。近期研究提出了一种基于资源管理规约检查来预防资源泄漏的方法。资源管理规约描述了程序如何分配、传递和释放资源，同时追踪对象与资源之间的所有权关系以及对象之间的别名关系。尽管这种"规约-验证"方法相较于现有技术具有若干优势，但需要手动编写注解的要求显著阻碍了其实际应用。本文提出了一种新颖技术，能够自动推断程序的资源管理规约，从而扩展了基于规约检查的资源泄漏验证方法的适用范围。该领域的推断面临挑战，因为资源管理规约在本质上与多数推断技术所针对的类型存在显著差异。此外，为达到实际有效性，我们需要一种技术能在代码未完全遵循规约的情况下，仍能推断出开发者预期的资源管理规约。我们通过精心设计的一组推断规则来应对这些挑战，这些规则能够捕捉实际编码模式，从而形成基于不动点的有效推断算法。我们已在两个不同系统中实现了该推断算法，分别针对Java和C#编写的程序。实验评估表明，我们的技术能够推断出程序员为基准测试手动编写的85.5%的注解。此外，采用手动编写与自动推断注解的验证器发出的误报率几乎相同。