Verifying Array Manipulating Programs with Full-Program Induction
31
15). Finally, a variable definition that is control dependent on an affected variable
is also considered affected (lines 16-18). The computation of affected variables
is iterated until the set AffectedVars saturates.
Lemma 2. Variables/Array elements not present in AffectedVars have the same
value after k L (N − 1) iterations of its enclosing loop (if any) in P N −1 as in P N .
Generating the Difference Program ∂P N . The routine ProgramDiff in
Algorithm 4 shows how the difference program is computed. We peel each loop
in the program and collect the list of peeled nodes (line 1) using Algorithm 2.
We then compute the set of affected variables (line 2) using Algorithm 3. The
difference program ∂P N inherits the skeletal structure of the program P N after
peeling each loop (line 4). The algorithm then traverses the CFG of each loop in
P N and removes the loops (lines 16-17) that do not update any affected variables
from ∂P N . For every CFG node in other loops, it determines the corresponding
node type (assignment or branch) and acts accordingly (lines 7-14). To explain
the intuition behind the steps of this algorithm, we use the convention that all
variables and arrays of P N −1 have the suffix Nm1 (for N-minus-1), while those of
P N have the suffix N. This allows us to express variables/array elements of P N
in terms of the corresponding variables/array elements of P N −1 in a systematic
way in ∂P N , given that the intended composition is P N −1 ; ∂P N .
For assignment statements using simple arithmetic operators (+,-,*,/), the
sub-routine AssignmentDiff in Algorithm 4 computes a “difference” statement
as follows. We assume that Nodes(L) returns the set of CFG nodes in loop L. For
every assignment statement of the form v = E; in L, a corresponding statement
is generated in ∂P N that expresses v N in terms of v Nm1 and the difference (or
ratio) between versions of variables/arrays that appear as sub-expressions in E in
P N −1 and P N . For example, the statement A N[i] = B N[i] + v N; in P N gives
rise to the “difference” statement A N[i] = A Nm1[i] + (B N[i] - B Nm1[i])
+ (v N - v Nm1); in ∂P N . Similarly, the statement A N[i] = B N[i] * v N;
in P N gives rise to the “difference” statement A N[i] = A Nm1[i] * (B N[i] /
B Nm1[i]) * (v N / v Nm1); under the assumption B Nm1[i] * v Nm1 = 0.
There are additional kinds of statements that need special processing when
generating ∂P N . These relate to accumulation of differences (or ratios). For
example, if P N has a loop for(i = 0; i < N; i++) sum N = sum N + A N[i];
then the difference A N[i] - A Nm1[i] is aggregated over all indices from 0
through N − 2. In this case, the corresponding “difference” loop in ∂P N has
the following form: sum N = sum Nm1; for(i = 0; i < N-1; i++) sum N =
sum N + (A N[i] - A Nm1[i]);. A similar aggregation for multiplicative ratios
can also be defined. Sub-routine AggregateAssignmentDiff in Algorithm 4
generates these “difference” statements.
Note that expressions like (B N[i] - B Nm1[i]) or (v N/v Nm1) can often be
simplified from the already generated part of ∂P N . For example, if the already
generated part has a statement of the form B N[i] = B Nm1[i] + expr1; or
v N = expr2*v Nm1;, and if expr1 and expr2 are constants or functions of N
and loop counters, then we can use expr1 for B N[i] - B Nm1[i] and expr2 for
31
15). Finally, a variable definition that is control dependent on an affected variable
is also considered affected (lines 16-18). The computation of affected variables
is iterated until the set AffectedVars saturates.
Lemma 2. Variables/Array elements not present in AffectedVars have the same
value after k L (N − 1) iterations of its enclosing loop (if any) in P N −1 as in P N .
Generating the Difference Program ∂P N . The routine ProgramDiff in
Algorithm 4 shows how the difference program is computed. We peel each loop
in the program and collect the list of peeled nodes (line 1) using Algorithm 2.
We then compute the set of affected variables (line 2) using Algorithm 3. The
difference program ∂P N inherits the skeletal structure of the program P N after
peeling each loop (line 4). The algorithm then traverses the CFG of each loop in
P N and removes the loops (lines 16-17) that do not update any affected variables
from ∂P N . For every CFG node in other loops, it determines the corresponding
node type (assignment or branch) and acts accordingly (lines 7-14). To explain
the intuition behind the steps of this algorithm, we use the convention that all
variables and arrays of P N −1 have the suffix Nm1 (for N-minus-1), while those of
P N have the suffix N. This allows us to express variables/array elements of P N
in terms of the corresponding variables/array elements of P N −1 in a systematic
way in ∂P N , given that the intended composition is P N −1 ; ∂P N .
For assignment statements using simple arithmetic operators (+,-,*,/), the
sub-routine AssignmentDiff in Algorithm 4 computes a “difference” statement
as follows. We assume that Nodes(L) returns the set of CFG nodes in loop L. For
every assignment statement of the form v = E; in L, a corresponding statement
is generated in ∂P N that expresses v N in terms of v Nm1 and the difference (or
ratio) between versions of variables/arrays that appear as sub-expressions in E in
P N −1 and P N . For example, the statement A N[i] = B N[i] + v N; in P N gives
rise to the “difference” statement A N[i] = A Nm1[i] + (B N[i] - B Nm1[i])
+ (v N - v Nm1); in ∂P N . Similarly, the statement A N[i] = B N[i] * v N;
in P N gives rise to the “difference” statement A N[i] = A Nm1[i] * (B N[i] /
B Nm1[i]) * (v N / v Nm1); under the assumption B Nm1[i] * v Nm1 = 0.
There are additional kinds of statements that need special processing when
generating ∂P N . These relate to accumulation of differences (or ratios). For
example, if P N has a loop for(i = 0; i < N; i++) sum N = sum N + A N[i];
then the difference A N[i] - A Nm1[i] is aggregated over all indices from 0
through N − 2. In this case, the corresponding “difference” loop in ∂P N has
the following form: sum N = sum Nm1; for(i = 0; i < N-1; i++) sum N =
sum N + (A N[i] - A Nm1[i]);. A similar aggregation for multiplicative ratios
can also be defined. Sub-routine AggregateAssignmentDiff in Algorithm 4
generates these “difference” statements.
Note that expressions like (B N[i] - B Nm1[i]) or (v N/v Nm1) can often be
simplified from the already generated part of ∂P N . For example, if the already
generated part has a statement of the form B N[i] = B Nm1[i] + expr1; or
v N = expr2*v Nm1;, and if expr1 and expr2 are constants or functions of N
and loop counters, then we can use expr1 for B N[i] - B Nm1[i] and expr2 for