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

100%

80%

>=15 callsites
12−15 callsites
5−9 callsites
2−5 callsites
<2 callsites

60%

40%

20%

0%

apache linux openssh osip postgreSQL procmail zebra

Benchmarks

FIGURE 9.16: Distribution of call-sites.

rive preconditions correctly for 199 of them (77.13% accuracy). Moreover, we
were able to derive preconditions for an additional nine procedures that were
not documented. We observe 12 false-positives (our tool derives preconditions
where none exist) and 31 false negatives (our tool did not derive the precondi-
tions the documented specification claims should hold). These false negatives
are potential sources of bugs. False positives occur primarily because there is
an insucient number of use cases for mining to effectively prune away irrel-
evant predicates. For example, in a few cases, a predicate is included in the
precondition to a procedure call because the procedure was invoked only twice,
and in both cases, the calling context contained similar irrelevant invariants.
Besides being potential sources of bugs, false negatives can also manifest
because of limitations in the implementation. In addition to the obvious ap-
proximations introduced by our heuristics (recall that a precise solution to
structural matching, the heart of the precondition inference problem, is NP-
hard), there are two other limitations in our approach addressed briefly below:

Absence of theorem proving: A precondition for the procedure
BNmodword is that the second parameter must not be equal to zero.
We do not observe any explicit sanity check on the second parameter
in the program source. On further inspection, we notice that there is a
chain of assignments leading to the second parameter, where we may be
able to prove that the second parameter will be non-zero on any invoca-
tion. Automatically formulating this conclusion is possible with the aid
of a theorem prover. The integration of theorem proving to the existing
infrastructure to handle these predicates is part of our ongoing research.

Closed world assumptions: Sometimes preconditions are formulated
with respect to environment variables whose values are directly manifest
in the program source. Since our implementation analyzes the program