Databases Reference
In-Depth Information
9.3.2 Implementation
Our algorithm takes as input the program source and a user-defined con-
fidence threshold for determining when a predicate should form part of a
pre-condition, and produces as output preconditions (i.e., a set of predicates)
for every procedure. These preconditions indicate the conditions that must
hold prior to any call of the associated procedure.
We first generate the control-flow graph for each procedure. The resulting
graph is processed using the algorithm given in Figure 9.18. The number of
procedureBuildpredicates
.Input:
G(V,E)
, directed, acyclic CFG of ;
V
is topologically sorted;
.Output: Annotated Graph G
.AuxiliaryInformation:
predicates
(u): predicates generated at u;
flow
(u): set of
predicates valid at u;
precond
(u): set of predicates that are used for generating
preconditions associated with procedure at u;
callsite(u):
true
if u is a callsite;return(u):
true
if u is the return node from procedure ;
1 iterate
true
2
while
iterate do
3
iterate
false
4
for
each node u = 1 to jVj
5 oldflow
flow
(u)
6
for
all predecessors v of u
7 n
u
n
u
+ n
v
8
flow
(u)
flow
(u) [
predicates
(v)
9
for
each predicate in
flow
(v)
10 q
u
() q
u
() +
max
(m
v
(), q
v
())
11 m
u
() 0
12
flow
(u)
flow
(u) [
predicates
(u)
13
for
each predicate in
datapredicate
(u)
14 m
u
() n
u
15
if
callsite(u) is
truethen
16
precond(
u
)
flow(
u
)
17
flow(
u
)
flow(
u
)
[
procsummary
[
func
(u)]
18
if
return(u) is
truethen
19
procsummary
[ ]
flow
(u)
20
if
oldflow 6=
flow
(u) then iterate
true
FIGURE 9.18: Algorithm for building predicates. (With kind permission
from Springer Science + Business Media: Protocol Inference Using Static Path
Proles, SAS, 2008, pp. 78{92, M. Ramanthan et al., Figure 4.)
Search WWH ::
Custom Search