Toward a practical, path-based framework for detecting and diagnosing software faults
Mary Lou Soffa, Wei Le · 2010
One of the important challenges of developing software is the avoidance of software faults. Since a fault occurs along an execution path, program path information is essential for detecting and diagnosing a fault. Manual inspection can identify a path where a fault occurs; however, the approach does not scale. Dynamic techniques, such as testing, are also effective to find faulty paths, but only in a sampled space. This thesis develops a practical, path-based framework to statically detect and then diagnose software faults. The techniques are path-based in that both detecting and reporting faults use path information. An important contribution of the work is the development of a demand-driven analysis that effectively addresses scalability challenges faced by traditional path-sensitive fault detection. A prototype tool, Marple, was developed to experimentally evaluate the research. Foundations of the thesis are the discoveries of path diversity and fault locality. Path diversity says that paths of safe, infeasible, faulty with various severities and root causes, and don't-know can traverse the same program point. Given the path type, fault diagnosis can take action accordingly. Fault locality demonstrates that a fault is often related to only a path segment of 1–4 procedures. By only focusing on such path segments, fault detection and diagnosis can be more efficient. To detect path types and path segments, an interprocedural, path-sensitive, demand-driven analysis was developed, which scales up to 570,000 lines of code. Evaluation of buffer overflow detection shows that the analysis is about 2 times faster than an exhaustive path-sensitive tool. Generality is achieved via a specification technique and an algorithm that automatically generates analyses for user-specified faults. The framework handles both control- and data-centric faults, including buffer overflow, integer fault, null-pointer dereference and memory leak. The usefulness of the path information is demonstrated for computing fault correlation, a causal relationship between faults, and for guiding software testing to exploit faults. The correlations reveal that the propagation of integer faults can lead to not only buffer overflows but also null-pointer dereferences, and resource leaks can cause infinite loops. Our path-guided concolic testing successfully triggers 73% of statically identified faults.