32
S. Chakraborty et al.
Algorithm 4 ProgramDiff(PN : program)
1: , peelN odes := PeelAllLoops(PN );
2: AffectedVars := ComputeAffected(PN , peelN odes);
3: Let the CFG of PN be (Locs, E, μ);
4: ∂PN := (Locs
, E
, μ
), where Locs
:= Locs, E
:= E, and μ
:= ∅;
5: for each loop L ∈ Loops(PN ) do
6:
if ∃v such that v is updated in L and v ∈ AffectedVars then
7:
for each node n ∈ Nodes(L) do
8:
stN := μ(n);
9:
if stN is of the form wN := r
1
N op r
2
N then
10:
μ
(n) := AssignmentDiff( wN := r
1
N op r
2
N );
11:
else if stN is of the form wN := wN op r
1
N wherein wN is a scalar then
12:
μ
(n) := AggregateAssignmentDiff( L, wN := wN op r
1
N );
13:
else
stN is a conditional statement
14:
μ
(n) := BranchDiff( stN , AffectedVars );
15:
else
Remove loop L from CFG of ∂PN
16:
(n1, n, U) := IncomingEdge(L); (n, n2, ff ) := ExitEdge(L);
17:
E
:= E
\ {(n1, n, U), (n, n2, ff )} ∪ {(n1, n2, U)}; Locs
:= Locs
\ Nodes(L);
18: return ∂PN ;
AssignmentDiff( wN := r
1
N op r
2
N )
1: Let invop be the arithmetic inverse operator of op;
+ and − are inverse operators of each other, and so are × and ÷
2: if op ∈ {+, ×} then
3:
return wN := wNm1 op (Simplify(r
1
N invop r
1
N m1 ) op Simplify(r
2
N invop r
2
N m1 ));
4: else if op ∈ {−, ÷} then
5:
return wN := wNm1 invop (Simplify(r
1
N op r
1
N m1 ) op Simplify(r
2
N op r
2
N m1 ));
6: else
7:
throw “Specified operator not handled”;
AggregateAssignmentDiff( L: loop, wN := wN op r
1
N )
1: n fresh := FreshNode(); μ
(n fresh ) := (wN := wNm1); Locs
:= Locs
∪ {n fresh };
2: (n
, n
, U) := IncomingEdge(L);
3: E
:= E
\ {(n
, n
, U)} ∪ {(n
, n fresh , U), (n fresh , n
, U)};
4: if op ∈ {+, ∗} then
5:
return wN := wN op Simplify(r
1
N invop r
1
N m1 );
6: else if op ∈ {−, ÷} then
7:
return wN := wN op Simplify(r
1
N op r
1
N m1 );
8: else
9:
throw “Specified operator not handled”;
BranchDiff( stN : branch condition, AffectedVars : set of affected variables )
1: Let n be CFG node corresponding to stN ;
2: if (∃v such that v is read in stN and v ∈ AffectedVars) ∨ (stN = stN−1 is satisfiable) then
3:
throw “Branch conditions in PN and PN−1 may not evaluate to same value”;
4: else
5:
return stN−1;
v N/v Nm1 respectively. We use these optimizations aggressively in the function
Simplify used in AssignmentDiff and AggregateAssignmentDiff.
For every CFG node representing a conditional branch in P N , Algorithm
BranchDiff is used to determine if the result of the condition check can differ in P N and P N −1 . If not, the conditional statement can be retained as such
in the “difference” program. Otherwise, our current technique cannot compute
∂P N and we report a failure of our technique (see body of BranchDiff). For
example, the conditional statement if (t3 == 0) in line 10 of Fig. 1(a) behaves identically in P N −1 and P N , and therefore can be used as is in the loop in
the difference program.
Lemma 3. ∂P N generated by ProgramDiff is such that, for all N > 1,
{ϕ(N )} P N −1 ; ∂P N {ψ(N )} holds iff {ϕ(N )} P N {ψ(N )} holds.