Databases Reference
In-Depth Information
Definition 12.4.1. An event is a combination of a function name and a
variable used in a call to that function, together with dataflow information
that describes the way the variable is used in the call.
Let us clarify this abstract denition by several examples: \ <temp1> is a
retval of nextInt() " is an event, because it is a combination of a function
name ( nextInt() ) and a variable ( <temp1> ) together with data flow informa-
tion (\is a retval of"). So are \ stack is a target of push() " and \ <temp1> is
a 1st arg of push() ." Based on the denition of an event, we can dene what
a sequential constraint is.
Definition 12.4.2. A sequential constraint is an ordered pair of two related
events with the variable information abstracted away. Two events are related
if they describe the usage of the same variable.
The denition above tell us that \retval of nextInt() 1st arg of push() "
is a valid sequential constraint, because \ <temp1> is a retval of nextInt() "
and \ <temp1> is a 1st arg of push() " are related events (both describe the
usage of <temp1> ).
Not all valid sequential constraints are correct with respect to a function
model. For example, \retval of nextInt() retval of nextInt() " obviously
does not make any sense. However, even some sensible sequential constraints
are incorrect. Consider the following one: \1st arg of push() $prec 1st arg
of push() ." This is a valid sequential constraint, because there is an event
\ <temp1> is a 1st arg of push() " in the function model in Figure 12.3, and
yet it is clear that the sequential constraint describes a dataflow that does
not happen. For a sequential constraint to be correct with respect to a func-
tion model, it must be supported by the dataflow represented by that func-
tion model. To put it more formally, there must exist a path through the
model, leading from the first event to the second one, with the variable relat-
ing the two events not being \killed" by any transition on that path, including
the transition that corresponds to the second event. Intuitively, a variable is
\killed" if it is assigned to (perhaps by being a return value of a function call).
The algorithm that extracts sequential constraints from a function model
looks as follows:
Extract-Sequential-Constraints(M)
1 I =Get-Incoming-Events(M)
2 O =Get-Outgoing-Events(M)
3 C = ;
4
for each node n in M
5
for each event e i 2 I[n]
6
for each event e o 2 O[n]
7
if e i :var name = = e o :var name
8
C = C [fe i :data ow e o :data owg
9
return C
 
Search WWH ::




Custom Search