Information Technology Reference
In-Depth Information
and
surjective
in Ex. 4. For simpler examples of preconditions (over a few variables
without quantifiers), no noticeable difference in performances has been recorded.
Late precondition method appears to be more expressive than native precondition
and has a limited overhead. It is more convenient for C developers to write precondition
directly in C, using existing code fragments and/or familiar notation. Unlike in the early
precondition treatment, our late precondition technique does not explore each path in
the function under test several times for each path in the precondition function, that
avoids to uselessly consider again already covered paths.
It is natural to expect that this feature brings a valuable benefit for preconditions with
disjunctions or existential quantifications (like in Ex. 4) since the precondition likely has
multiple accepting paths for a given path in the program under test. Interestingly, even
for programs with only conjunctive and universally quantified preconditions, our tech-
nique may significantly reduce the global number of paths to be explored (cf. Ex. 1). We
also observe that the late precondition treatment appears to be less sensitive to the form
of the precondition: as illustrated by Ex. 3-4, writing logically the same precondition in
a different way can result in a significant loss of performances for the early precondition
while the late precondition treatment is not affected so much. Finally, we notice that a
potentially great number of calls to (an efficient executable version of) the precondition
does not dramatically slow down test generation (cf. Ex. 1-4).
5Conluion
We propose a late-precondition method for dynamic symbolic execution that combines
at least two benefits. First, it takes as input an executable precondition written in the
tested language, i.e., C for P
AT H
C
RAWLER
. Such a precondition is easier to write for
developers and can be very expressive. Second, the method ensures that paths of the
function under test are considered once and only once during test generation. This no-
tably allows high path coverage, where each uncovered path is either infeasible or out-
side chosen limits (e.g., on the number of loop iterations). This article also gives an
initial experimental evaluation of the method. It was made possible through the imple-
mentation of the method in P
AT H
C
RAWLER
. Our experiments report a little overhead
with respect to a native precondition and significantly better performances with respect
to an early precondition.
Moreover, C precondition appears particularly useful when combining static and dy-
namic analysis, notably in the SANTE tool [9] and in treating
E
-
ACSL
, an executable
specification language for C [10]. Indeed, when combining tools with very different
views on the program, the program's own language is often the most suitable common
language to express a precondition. That is why C precondition is used in those works
to encode preconditions given in Pre/Post specifications.
Future work includes further experiments with late precondition and studying the
form of precondition for which it is more or less efficient. In case of a precondition
filtering out a lot of inputs, one may expect that late precondition could be more expen-
sive than the traditional approach since it may lead to the exploration of many irrelevant
program paths. Further improvements (such as a combination with a summarized early
precondition, or early treatment of a conjunctive part of the precondition) could improve
the performances in more cases.
