Databases Reference
In-Depth Information
g, h
g, h
g
g, h
h
g, h
g, h
g, h
g, h
g, h
4
1
2
4
1
2
3
5
3
5
p
p
p
p
(a)
Under Approximation
(b)
Correct Pre-conditions
g, h
g, h
g, h
g
g, h
4
1
2
3
5
p
p
(c)
Over Approximation
FIGURE 9.1: An example illustrating under- and over-approximation of
predicates. (With kind permission from Springer Science + Business Media:
Protocol Inference Using Static Path Proles, SAS, 2008, pp. 78{92, M. Ra-
manthan et al., Figure 1.)
among predicates (e.g., procedure p is called immediately after a conditional
test that checks whether some variable v is non-null). We describe an imple-
mentation of these techniques, and validate the effectiveness of the approach
on a number of large open-source benchmarks. Experimental results confirm
that our mining algorithms are ecient, and that the specifications derived
are both precise and useful { the implementation discovers several critical, yet
previously undocumented, preconditions for well-tested libraries.
9.1.4 Path Profiles
We also discuss a specification inference approach that typically mine com-
monalities among states at relevant program points. For example, to infer the
invariants that must hold at all calls to a procedure p requires examining
the state abstractions found at all call-sites to p. Unfortunately, existing ap-
proaches to building these abstractions require being able to explore all paths
(either static or dynamic) to all of p's call-sites to derive specications with
any measure of confidence. Because programs that have complex control-flow
structure may induce a large number of paths, naive path exploration is im-
practical. We examine a specification inference technique that allows us to
eciently explore statically all paths to a program point. Our approach builds
static path profiles, profile information constructed by a static analysis that
accumulates predicates valid along different paths to a program point. These
Search WWH ::
Custom Search