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

the predicate as a precondition in the non-profile based inference scheme. In
the path-profiling approach, we declare a predicate to be a precondition if it
is valid in 70% of the paths to call-sites of the procedure.
Figure 9.20 presents the percentage of preconditions derived by non-profile
based specification inference as compared to those derived using static path
profiling. For example, for procedures with three to five call-sites in zebra ,
the former discovers roughly only half the predicates discovered by the path
profile analysis. As expected, for procedures with fewer than three call-sites,
the non-profile based inference scheme is not able to derive any preconditions.
For example, in the case of openssh , no precondition is derived for procedures
that have fewer than three statically apparent call-sites.
We also observe that in many cases, the set of preconditions generated
with the non-profile based inference is a proper subset of the preconditions
generated using the static path profiling approach. This is consistent with our
expectation that typical static analyzes can lead to over approximation by
eliminating valid predicates from preconditions. In some cases, however, such
as osip or zebra , this hypothesis does not hold. Path profiling weights pred-
icates based on the number of paths on which they hold across all call-sites.
Consider a predicate which occurs on k paths at n call-sites to procedure
p. Suppose that paths are not evenly distributed among these n call-sites. If
on m call-sites, occurs on all paths, and m is greater than the threshold
cuto, the non-prole based inference will record as a valid precondition.
However, if the number of paths that flow into these m call-sites is much less
than k, then the path prole analysis will nonetheless not include as part of
p's preconditions. In other words, a predicate that does not hold on a majority
of paths may still hold on the paths to a majority of call-sites. Path profiling
thus provides finer control over both the inclusion and exclusion of predicates
than non-profile based inference.
9.3.5 Qualitative Assessment
We want to identify the impact of infeasible paths and approximations
introduced by static path weights in the program on the quality of the spec-
ifications inferred. To do so, we compare our approach with a dynamic in-
ference mechanism. Rather than using an existing test-suite to generate dy-
namic traces, we usecute, an automatic test generation tool, that provides
extended coverage of the program, and thus helps reduce the possibility of
under-approximation (compared to other dynamic analysis systems) as de-
scribed in Section 9.1.
The test generation process initially runs with some random input and
collects constraints fC 1 ;:::;C k1 ;C k g symbolically along the execution. To
explore a previously unexplored path, a new input is generated that satisfies
the constraints fC 1 ;:::C k1 ;:C k g. If this path were explored earlier, then the
set of constraints fC 1 ;::::C k1 g would be used to explore a dierent path.
This process repeats until all paths in the program are explored. There are
several issues that must be handled by the input generation process. Most