Verifying Array Manipulating Programs with Full-Program Induction
29
Algorithm 1 ComputeRefinedPDG(PN : Program)
1: G(V, DE, CE) := ConstructPDG(PN );
2: if ∃v, n, n
. (n, n
) ∈ DE ∧ is-array(v) ∧ v ∈ def (n) ∧ v ∈ uses(n
) then
3:
if n is part of a loop L then
4:
:= loop counter of L;
5:
Let φ(n) be the constraint (0 ≤ < kL);
6:
else
7:
Let φ(n) be true;
8:
if n
is part of a loop L
then
9:
:= loop counter of L
;
10:
Let φ
(n
) be the constraint (0 ≤
< k L );
11:
else
12:
Let φ
(n
) be true;
13:
if φ(n) ∧ φ(n
) ∧
subscript(v, n) = subscript (v, n
)
is unsatisfiable then
14:
DE = DE \ {(n, n
)};
Remove dependence edges with non-overlapping subscripts
15: return G(V, DE, CE);
Algorithm 2 PeelAllLoops((Locs, Edges, μ) : CFG of PN )
1: P
p
N := (Locs
p , Edges
p , μ
p ), where L
p = Locs, Edges
p = Edges, μ
p = μ;
Copy of PN
2: peelN odes := ∅;
3: for each loop L ∈ Loops(P
p
N ) do
4:
Let kL(N ) be the expression for iteration count of L in P
p
N ;
5:
peelCount := Simplify(kL(N ) − kL(N − 1));
6:
if peelCount is non-constant then throw “Failed to peel non-constant number of iterations”;
7:
p
N , Locs
:= PeelSingleLoop(P
p
N , L, kL(N − 1), peelCount);
Transforms loop L so that last peelCount iterations of L are peeled/unrolled. Updated
CFG and newly created CFG nodes for the peeled iterations are returned by PeelSingleLoop.
8:
peelN odes := peelN odes ∪ Locs
;
9: return
p
N , peelN odes
scalar variable. Note that lines 2-14 of ComputeRefinedPDG removes data
dependence edges between nodes of G that do not satisfy Definition 1.
3.2 Core Modules in the Technique
Peeling the Loops. To relate P N to P N −1 , we first ensure that the corresponding loops in both programs iterate the same number of times by peeling extra
iterations from the loops in P N . This is done by routine PeelAllLoops shown
in Algorithm 2. The algorithm first makes a copy, viz. P
p
N , of the input CFG
P N . Let Loops(P
p
N ) denote the set of loops of P
p
N , and let k L (N ) and k L (N − 1)
denote the number of times loop L iterates in P
p
N and P
p
N −1 respectively. The
difference k L (N ) − k L (N − 1), computed in line 5, gives the extra iterations of
loop L in P
p
N . If this difference is not a constant, we currently report a failure
of our technique (line 6). Otherwise, routine PeelSingleLoop transforms loop
L of P
p
N as follows: it replaces the termination condition ( < k L (N )) of L by
( < k L (N − 1)). It also peels (or unrolls) the last (k L (N ) − k L (N − 1)) iterations of L and adds control flow edges such that the the peeled iterations are
executed immediately after the loop body is iterated k L (N − 1) times. Effectively, PeelSingleLoop unrolls/peels the last (k L (N ) − k L (N − 1)) iterations
of loop L in P
p
N . The transformed CFG is returned as the updated P
p
N in line
7. In addition, PeelSingleLoop also returns the set Locs
of all CFG nodes
newly added while peeling the loop L. The overall updated CFG and the set of
all peeled nodes obtained after peeling all loops in P
p
N is returned in line 9.
Lemma 1. {ϕ N } P N {ψ N } holds iff {ϕ N } P
p
N {ψ N } holds.
29
Algorithm 1 ComputeRefinedPDG(PN : Program)
1: G(V, DE, CE) := ConstructPDG(PN );
2: if ∃v, n, n
. (n, n
) ∈ DE ∧ is-array(v) ∧ v ∈ def (n) ∧ v ∈ uses(n
) then
3:
if n is part of a loop L then
4:
:= loop counter of L;
5:
Let φ(n) be the constraint (0 ≤ < kL);
6:
else
7:
Let φ(n) be true;
8:
if n
is part of a loop L
then
9:
:= loop counter of L
;
10:
Let φ
(n
) be the constraint (0 ≤
< k L );
11:
else
12:
Let φ
(n
) be true;
13:
if φ(n) ∧ φ(n
) ∧
subscript(v, n) = subscript (v, n
)
is unsatisfiable then
14:
DE = DE \ {(n, n
)};
Remove dependence edges with non-overlapping subscripts
15: return G(V, DE, CE);
Algorithm 2 PeelAllLoops((Locs, Edges, μ) : CFG of PN )
1: P
p
N := (Locs
p , Edges
p , μ
p ), where L
p = Locs, Edges
p = Edges, μ
p = μ;
Copy of PN
2: peelN odes := ∅;
3: for each loop L ∈ Loops(P
p
N ) do
4:
Let kL(N ) be the expression for iteration count of L in P
p
N ;
5:
peelCount := Simplify(kL(N ) − kL(N − 1));
6:
if peelCount is non-constant then throw “Failed to peel non-constant number of iterations”;
7:
p
N , Locs
:= PeelSingleLoop(P
p
N , L, kL(N − 1), peelCount);
Transforms loop L so that last peelCount iterations of L are peeled/unrolled. Updated
CFG and newly created CFG nodes for the peeled iterations are returned by PeelSingleLoop.
8:
peelN odes := peelN odes ∪ Locs
;
9: return
p
N , peelN odes
scalar variable. Note that lines 2-14 of ComputeRefinedPDG removes data
dependence edges between nodes of G that do not satisfy Definition 1.
3.2 Core Modules in the Technique
Peeling the Loops. To relate P N to P N −1 , we first ensure that the corresponding loops in both programs iterate the same number of times by peeling extra
iterations from the loops in P N . This is done by routine PeelAllLoops shown
in Algorithm 2. The algorithm first makes a copy, viz. P
p
N , of the input CFG
P N . Let Loops(P
p
N ) denote the set of loops of P
p
N , and let k L (N ) and k L (N − 1)
denote the number of times loop L iterates in P
p
N and P
p
N −1 respectively. The
difference k L (N ) − k L (N − 1), computed in line 5, gives the extra iterations of
loop L in P
p
N . If this difference is not a constant, we currently report a failure
of our technique (line 6). Otherwise, routine PeelSingleLoop transforms loop
L of P
p
N as follows: it replaces the termination condition ( < k L (N )) of L by
( < k L (N − 1)). It also peels (or unrolls) the last (k L (N ) − k L (N − 1)) iterations of L and adds control flow edges such that the the peeled iterations are
executed immediately after the loop body is iterated k L (N − 1) times. Effectively, PeelSingleLoop unrolls/peels the last (k L (N ) − k L (N − 1)) iterations
of loop L in P
p
N . The transformed CFG is returned as the updated P
p
N in line
7. In addition, PeelSingleLoop also returns the set Locs
of all CFG nodes
newly added while peeling the loop L. The overall updated CFG and the set of
all peeled nodes obtained after peeling all loops in P
p
N is returned in line 9.
Lemma 1. {ϕ N } P N {ψ N } holds iff {ϕ N } P
p
N {ψ N } holds.