Path-Aware Static Program Analyses for Specification Mining* - Mining Software Specifications: Methodologies and Applications - page 350

pairs of functions, and Kremenek et al. [28] significantly generalize these earlier
ideas. However, [28] is domain specific, and requires either machine learning
or user specifications to generate initial annotation probabilities, and employs
naming conventions for identifying interesting procedures to improve accuracy.
As a result, their approach would be ineffective in deriving the specifications
for the example programs in Figures 9.2, 9.3, or Section 9.2.9.
Apart from mining based approaches, many other interesting techniques
have been devised for bug detection in software systems [21,32,47]. For exam-
ple, in [21], Godefroid et al. present a technique for automatically generating
test cases so that the coverage of the program is increased. Liblit et al. [32]
present a technique in which predicate information is collected on actual runs
of the software and statistical analysis is employed to find correlation between
bugs and causes. Yang et al. [47] use model checking to detect bugs in systems
code. Rinard et al. [38] present an approach on failure oblivious computing
that enables servers to run even in the presence of memory errors. Castro et
al. [12] present an approach where a data flow graph is generated and ensures
that the data flow integrity is preserved at run time. Because our work focuses
on an entirely new dimension, namely, statically extracting preconditions from
program source transparently, it is conceivable that it could be used in con-
junction with these other approaches to operate with even greater precision
and scale.
Cortes et al. [14] present a domain- specific languageHancockfor writing
mining applications.
Ball and Larus [7] propose an approach for ecient path profiling. In their
approach, dynamic runs of a program are profiled to gather information about
different path executions. Recently, Vaswani et al. [41], present a scheme to
identify a subset of interesting paths and use a compact numbering scheme us-
ing arithmetic coding techniques. Our approach is motivated by the algorithm
presented by Ball and Larus [7] and is applied statically.
9.5 Conclusions
This chapter discusses the problem of statically deriving specifications us-
ing predicate mining. We describe an inference mechanism for detecting the
preconditions that must be valid whenever a procedure is invoked. We derive
these preconditions using an inter-procedural path-sensitive dataflow analysis
that gathers predicates at each program point. We apply mining techniques
to these predicates to make specification inference robust to errors. Experi-
mental results on large open-source C programs validate the practicality of
our techniques. To gain greater precision, and have static analysis more closely
emulate properties that would be revealed under a dynamic evaluation, we also