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

RIMATCHTYPEPARTIAL , the call to riBuildQueryKeyFull is erroneous be-
cause the procedure does not handle arguments of this type. Path-aware an-
alysis is critical to deriving these inferences.
9.2.2 Preceded-By and Followed-By Relations
In this chapter, we focus only on precedence properties (\a call to q must
be preceded by a call to p"). Notably, our implementation does not consider
constraints of the form \a call to p is followed-by a call to q." While useful in
certain contexts, we observe that protocols of this form are less precise than
precedence protocols, especially in the presence of non-local jumps, errors, and
exceptions. A precedence relation captures the set of antecedent constraints
(e.g., initialization invariants) that must be satisfied before a procedure call
can be made; a follows relation captures the set of consequent actions (e.g.,
finalization invariants) that must occur after a procedure call is executed.
A precedence relation captures behavior that is guaranteed to occur if
the protocol is properly obeyed (e.g., a call to pthreadmutexlock must be
preceded by a call to pthreadmutexinit ). On the other hand, the fact that
a forward relation is not satisfied does not necessarily imply that program
behavior is incorrect. Consider the following snippet from some procedure p :
if((id=useropen(...))== err ) f
print("error");
return;
g
userclose(id);
Here, we cannot assert that every call to useropen will always be followed
by a call to userclose because an error condition that occurs in the interim
may lead to an abnormal exit from procedure p . On the other hand, if a
call to userclose does take place, it is guaranteed that a preceding call to
useropen would have occurred if the protocol were properly followed. This
is a key insight that enables us to infer precise precedence protocols whose
violation may signal the presence of a bug.
9.2.3 Dataflow Predicates
The other class of specifications we consider here are those involving
dataflow properties. A dataflow property indicates value flow relationships
among executed statements. These properties define constraints on the set
of values a particular variable may contain at a specific program point (e.g.,
whenever f is called, pointer fp must not be null, or x is true whenever y >
10).
We motivate the issues using a real-world example { deriving a specication
for the bind system call in the Linux socket library. While the application of
our approach is in deriving specifications for undocumented procedures, it is