Effective bug finding in C programs with shape and effect abstractions

Abstract

Software tends to suffer from simple resource mismanipulation bugs, such as double-locks. Code scanners are used extensively to remove these bugs from projects like the Linux kernel. Yet, these tools are not effective when the manipulation of resources spans multiple functions. We present a shape-and-effect analysis for C, that enables efficient and scalable inter-procedural reasoning about resource manipulation. This analysis builds a program abstraction based on the observable side-effects of functions. Bugs are found by model checking this abstraction, matching undesirable sequences of operations. We implement this approach in the Eba tool, and evaluate it on a collection of historical double-lock bugs from the Linux kernel. Our results show that our tool is more effective at finding bugs than similar code-scanning tools. Eba analyzes nine thousand Linux files in less than half an hour, and uncovers double-lock bugs in various drivers.