2022

[1,2]Divyesh Unadkat

1]Computer Science and Engineering, Indian Institute of Technology Bombay,
Main Gate Rd, IIT Area, Powai, Mumbai, 400076, Maharashtra, India

[2]TCS Research, 54-B Hadapsar Industrial Estate, Hadapsar, Pune, 411013,
Maharashtra, India

# Full-Program Induction: Verifying Array Programs sans Loop Invariants

Supratik Chakraborty<EMAIL_ADDRESS>Ashutosh Gupta
<EMAIL_ADDRESS><EMAIL_ADDRESS>[  *

###### Abstract

Arrays are commonly used in a variety of software to store and process data in
loops. Automatically proving safety properties of such programs that
manipulate arrays is challenging. We present a novel verification technique,
called _full-program induction_ , for proving (a sub-class of) quantified as
well as quantifier-free properties of programs manipulating arrays of
parametric size $N$. Instead of inducting over individual loops, our technique
inducts over the entire program (possibly containing multiple loops) directly
via the program parameter $N$. The technique performs non-trivial
transformations of the given program and pre-conditions during the inductive
step. The transformations assist in effectively reducing the assertion
checking problem by transforming a program with multiple loops to a program
which has fewer and simpler loops or is loop-free. Significantly, _full-
program induction_ does not require generation or use of loop-specific
invariants. To assess the efficacy of our technique, we have developed a
prototype tool called Vajra. We demonstrate the performance of Vajra vis-a-vis
several state-of-the-art tools on a large set of array manipulating benchmarks
from the international software verification competition (SV-COMP) and on
several programs inspired by algebraic functions that perform polynomial
computations.

###### keywords:

Full-program induction, inductive proof, Hoare triple, array programs,
difference program, difference pre-condition, quantified assertions, loop
invariant

##  1 Introduction

Use of software controlled systems in industrial and household appliances is
constantly increasing. Functionalities of such software are programmed with
extensive use of loops and conditional statements that manipulate different
data structures such as arrays, lists, and vectors to store and process data
during its operation. Programs with loops manipulating arrays are quite common
in many such applications. These programs are expected to be of immensely
high-quality as their erroneous functioning can cause adversities to
businesses as well as human lives. Thus, ensuring correctness of these
programs is of paramount importance. Unfortunately, assertion checking in such
programs is, in general, undecidable. Existing tools therefore use a
combination of verification techniques that work well for certain classes of
programs and assertions, and yield conservative results otherwise.

In this paper, we present a new verification technique, called _full-program
induction_ , to add to this arsenal of techniques. Specifically, we focus on
programs with loops manipulating arrays, where the size of each array is a
symbolic integer parameter $N~{}(>0)$. We allow (a sub-class of) quantified
and quantifier-free pre- and post-conditions that may depend on the symbolic
parameter $N$. Thus, the problem we wish to solve can be viewed as checking
the validity of a parameterized Hoare triple
$\\{\varphi(N)\\}\;\mathsf{P}_{N}\;\\{\psi(N)\\}$ for all values of
$N~{}(>0)$, where the program $\mathsf{P}_{N}$ computes with arrays of size
$N$, and $N$ is a free variable in $\varphi(\cdot)$ and $\psi(\cdot)$.

Like earlier verification approaches kind , our technique also relies on
mathematical induction to reason about programs with loops. However, the way
in which the inductive claim is formulated and proved differs significantly
from the previous techniques. Specifically, (i) we _induct on the full
program_ (possibly containing multiple loops) with parameter $N$ and not on
iterations of individual loops in the program, (ii) we perform _non-trivial
correct-by-construction transformation of the given program and the pre-
condition_ , whenever feasible, to simplify the inductive step of reasoning,
(iii) we _strengthen the pre- and post-condition simultaneously during the
inductive step_ using the auxiliary inductive predicates obtained by employing
Dijkstra’s weakest pre-condition computation, (iv) we _recursively apply_ the
technique to prove the inductive step and most importantly (v) we _do not
require explicit or implicit loop-specific inductive invariants_ to be
provided by the user or generated by a solver (viz. by constrained Horn clause
solvers chc ; quic3 ; freqhorn  or recurrence solvers viap ; aligators ). The
combination of these factors often reduces reasoning about a program with
multiple loops to reasoning about one with fewer (sometimes even none) and
“simpler” loops, thereby simplifying proof goals. In this paper, we
demonstrate this, focusing on programs with sequentially composed, but non-
nested loops.

###  1.1 Motivating Examples

We present a couple of examples to illustrate our technique and showcase its
salient features. The first example presents the basic ideas behind full-
program induction. The second example highlights various nuanced features of
the technique and is used as a running example in this paper.

    // assume(

    $\ignorespaces\mathsf{True}$

    )

    1. for (int t1=0; t1<N; t1=t1+1) {
    2.   if (t1==0) { A[t1] = 6; }
    3.   else { A[t1] = A[t1-1] + 6; }
    4. }

    5. for (int t2=0; t2<N; t2=t2+1) {
    6.   if (t2==0) { B[t2] = 1; }
    7.   else { B[t2] = B[t2-1] + A[t2-1]; }
    8. }

    9. for (int t3=0; t3<N; t3=t3+1) {
    10.  if (t3==0) { C[t3] = 0; }
    11.  else { C[t3] = C[t3-1] + B[t3-1]; }
    12.}

    // assert(

    $\ignorespaces\forall$

    i

    $\ignorespaces\in$

     [0,N), C[i] = i

    3

    )

Figure 1: Original Hoare triple

Fig. 1 shows an example of a Hoare triple, where the pre- and post-conditions
are specified using assume and assert statements. This triple effectively
verifies the formula
$\sum\limits_{j=0}^{i-1}\left(1+\sum\limits_{k=0}^{j-1}6\cdot(k+1)\right)=i^{3}$
for all $i\in\\{0\ldots N-1\\}$, and for all $N>0$. Although each loop in Fig.
1 is simple, their sequential composition makes it difficult even for state-
of-the-art tools like VIAP viap , VeriAbs veriabs20 , FreqHorn freqhorn ,
Tiler sas17 , Vaphor vaphor , or Booster booster  to prove the post-condition
correct. In fact, none of the above tools succeed in automatically proving the
quantified post-condition in Fig. 1. In contrast, our technique _full-program
induction_ proves the post-condition in Fig. 1 correct within a few seconds.

    // assume(

    $\ignorespaces\mathsf{True}$

    )

    1.  A[0] = 6;
    2.  B[0] = 1;
    3.  C[0] = 0;

    // assert((C[0] = 0

    3

    )

    $\ignorespaces\wedge$

    //        (B[0] = 1

    3

     - 0

    3

    )

    $\ignorespaces\wedge$

    //        (A[0] = 2

    3

     - 2

    $\ignorespaces\times$

    1

    3

     + 0

    3

    ))

Figure 2: Base-case Hoare triple

Full-program induction reduces checking the validity of the Hoare triple in
Fig. 1 to checking the validity of two “simpler” Hoare triples, represented in
Figs. 2 and 3. The base case of our inductive reasoning is shown in Fig. 2,
where every loop in the program is statically unrolled a fixed number of times
after instantiating the program parameter $N$ to a small constant value (here
$N=1$). As the induction hypothesis, we assume that the Hoare triple
$\\{\varphi(N-1)\\}$ $\;{\mathsf{P}_{N-1}}\;$ $\\{\psi(N-1)\\}$ holds for
values of $N>1$. Note that this assumption does not relate to a specific loop
in the program, but to the entire program ${\mathsf{P}_{N}}$. For the
motivating example, the induction hypothesis states that the entire Hoare
triple in Fig. 1, after substituting $N$ with $N-1$, holds. Notice that the
induction hypothesis is on the entire program including all three loops and
not on individual loops. The inductive step of the reasoning shown in Fig. 3
proves the post-condition, by automatically generating the computation to be
performed after the program with parameter $N-1$ has executed and
strengthening the pre- and post-conditions using auxiliary predicates. Note
that all the program statements in Fig. 3 have syntactic counterparts in Fig.
1, but this may not be the case in general. We conceptualize the computation
in the inductive step using the notions of difference program and difference
pre-condition in the later sections. Effectively, we reasoned about three
sequentially composed loops in Fig. 1 together, without the need for any
implicitly or explicitly specified loop invariants. We defer a discussion of
how our technique computes these Hoare triples and how auxiliary predicates
are generated to iteratively strengthen the pre- and post-conditions to Sect.
5, where we present the details of our algorithms.

    // assume(
    //  (N > 1)

    $\ignorespaces\wedge$

     (C_Nm1[N-2] = (N-2)

    3

    )

    $\ignorespaces\wedge$

    //  (B_Nm1[N-2] = (N-1)

    3

     - (N-2)

    3

    )

    $\ignorespaces\wedge$

    //  (A_Nm1[N-2] = N

    3

     - 2

    $\ignorespaces\times$

    (N-1)

    3

     + (N-2)

    3

    )
    // )

    1.  A[N-1] = A_Nm1[N-2] + 6;
    2.  B[N-1] = B_Nm1[N-2] + A_Nm1[N-2];
    3.  C[N-1] = C_Nm1[N-2] + B_Nm1[N-2];

    // assert(
    //  (C[N-1] = (N-1)

    3

    )

    $\ignorespaces\wedge$

    //  (B[N-1] = N

    3

     - (N-1)

    3

    )

    $\ignorespaces\wedge$

    //  (A[N-1] = (N+1)

    3

     - 2

    $\ignorespaces\times$

    N

    3

     + (N-1)

    3

    )
    // )

Figure 3: Inductive-step Hoare triple

It is important to mention a few things here to highlight the simplifications
illustrated by the Hoare triples in Figs. 2 and 3 that resulted from the
application of the full-program induction technique on the problem in Fig. 1.
First, the programs in Figs. 2 and 3 are loop-free. Second, their pre- and
post-conditions are quantifier-free. Third, the validity of these Hoare
triples (Figs. 2 and 3) can be easily proved, e.g. by bounded model checking
bmc  with a back-end SMT solver like Z3 z3 . Fourth, the value computed in
each iteration of each loop in Fig. 1 is data-dependent on previous iterations
of the respective loops as well as on the value computed in previous loops.
Even though none of these loops can be trivially translated to a set of
parallel assignments, our method still succeeds in automating the inductive
step of the analysis. Last, we did not require any specialized constraint
solving techniques like recurrence solving, theory of uninterpreted functions
or constrained Horn clause solving to verify these Hoare triples, thus making
our technique orthogonal to these approaches when proving properties of array
programs.

Now consider the Hoare triple shown in Fig. 4. The program updates a scalar
variable S and an array variable A. The first loop adds the value of each
element in array A to variable S. The second loop adds the value of S to each
element of A. The last loop aggregates the updated content of A in S. The pre-
condition $\varphi(N)$ is a universally quantified formula on array A stating
that each element has the value $1$. We need to establish the post-condition
$\psi(N)$, which is a predicate on S and N. Note that the post-condition has
non-linear terms making it quite challenging to prove. We will use the Hoare
triple in Fig. 4 as our running example to illustrate important aspects of the
full-program induction technique.

    // assume(

    $\ignorespaces\forall$

    i

    $\ignorespaces\in$

    [0,N) A[i] = 1)

    1.  S = 0;
    2.  for(i=0; i<N; i++) {
    3.    S = S + A[i];
    4.  }

    5.  for(i=0; i<N; i++) {
    6.    A[i] = A[i] + S;
    7.  }

    8.  for(i=0; i<N; i++) {
    9.    S = S + A[i];
    10. }

    // assert(S = N

    $\ignorespaces\times$

     (N+2))

Figure 4: Running example

Since the program $\mathsf{P}_{N}$ updates the same scalar variable S and the
array A in multiple sequentially composed loops, we rename these scalars and
arrays such that each loop in $\mathsf{P}_{N}$ updates its own copy of scalar
variables and arrays. This ensures that when $\mathsf{P}_{N-1}$ terminates we
have access to the values of these variables after each loop in the program.
The renamed program is shown in the Hoare triple in Fig. 5(a).

In the base case of our inductive reasoning, we instantiate the parameter $N$
to a small constant value (say $N=1$). As a result, every loop in the program
$\mathsf{P}_{N}$ in Fig. 5(a) can be statically unrolled a fixed number of
times. The resulting Hoare triple can be easily compiled to a first-order
logic formula and verified using an SMT solver. As the induction hypothesis,
we assume that the Hoare triple $\\{\varphi(N-1)\\}$ $\;{\mathsf{P}_{N-1}}\;$
$\\{\psi(N-1)\\}$, shown in Fig. 5(b), holds for values of $N>1$. This Hoare
triple is obtained by substituting $N$ with $N-1$ in the entire Hoare triple
in Fig. 5(a).

    // assume(

    $\ignorespaces\forall$

    i

    $\ignorespaces\in$

    [0,N) A[i]=1)

    1.  S = 0;
    2.  for(i=0; i<N; i++) {
    3.    S = S + A[i];
    4.  }

    5.  for(i=0; i<N; i++) {
    6.    A1[i] = A[i] + S;
    7.  }

    8.  S1 = S;
    9.  for(i=0; i<N; i++) {
    10.   S1 = S1 + A1[i];
    11. }

    // assert(S1=N

    $\ignorespaces\times$

    (N+2))

(a)

    // assume(

    $\ignorespaces\forall$

    i

    $\ignorespaces\in$

    [0,N-1) A[i]=1)

    1.  S_Nm1 = 0;
    2.  for(i=0; i<N-1; i++) {
    3.    S_Nm1 = S_Nm1 + A[i];
    4.  }

    5.  for(i=0; i<N-1; i++) {
    6.    A1_Nm1[i] = A[i]+S_Nm1;
    7.  }

    8.  S1 = S;
    9.  for(i=0; i<N-1; i++) {
    10.   S1_Nm1=S1_Nm1+A1_Nm1[i];
    11. }

    // assert(S1_Nm1=(N-1)

    $\ignorespaces\times$

    (N+1))

(b)

    // assume(N>1

    $\ignorespaces\wedge$

     A[N-1]=1
    //

    $\ignorespaces\wedge$

     S1_Nm1=(N-1)

    $\ignorespaces\times$

    (N+1)
    //

    $\ignorespaces\wedge$

    $\ignorespaces\forall$

    i

    $\ignorespaces\in$

    [0,N-1) A1_Nm1[i]=N
    //

    $\ignorespaces\wedge$

     S_Nm1=N-1)

    1.  S = S_Nm1 + A[N-1];

    2.  for(i=0; i<N-1; i++) {
    3.    A1[i] = A1_Nm1[i] + 1;
    4.  }
    5.  A1[N-1] = A[N-1] + S;

    6.  S1 = S1_Nm1 + A[N-1];
    7.  S1 = S1 + (N-1);
    8.  S1 = S1 + A1[N-1];

    // assert(S1=N

    $\ignorespaces\times$

    (N+2)

    $\ignorespaces\wedge$

     S=N
    //

    $\ignorespaces\wedge$

    $\ignorespaces\forall$

    i

    $\ignorespaces\in$

    [0,N) A1[i]=N+1)

(c)

Figure 5: (a) Given Hoare triple on $\mathsf{P}_{N}$ (b) induction hypothesis
Hoare triple on $\mathsf{P}_{N-1}$ and (c) inductive step Hoare triple on
$\partial\mathsf{P}_{N}$ after simplification and strengthening

The Hoare triple in Fig. 5(c) is computed for the inductive step. Intuitively,
the difference program $\partial\mathsf{P}_{N}$ recovers the effect of the
computation in $\mathsf{P}_{N}$ on all scalar variables and arrays after the
computation in $\mathsf{P}_{N-1}$ has been performed. It includes the
iterations of a loop in $\mathsf{P}_{N}$ that are missed by
$\mathsf{P}_{N-1}$. When program statements are impervious to the value of
$N$, the values computed in such statements are the same in $\mathsf{P}_{N}$
and $\mathsf{P}_{N-1}$, and hence, they may not need any modification.
However, $\partial\mathsf{P}_{N}$ may contain code to “rectify” values of
variables and arrays that have different values at corresponding statements in
$\mathsf{P}_{N}$ vis-a-vis $\mathsf{P}_{N-1}$. The code, possibly consisting
of loops, to rectify the values of variables and arrays is further simplified
whenever possible. Consequently, not all program statements of
$\mathsf{P}_{N}$ in Fig. 5(a) may have a syntactic counterpart in Fig. 5(c)
and vice-versa. We present in detail the algorithms for the computation and
simplification of the difference program in Sects. 4.5 and 4.6. The inductive
step may not be immediately established, in which case we strengthen the pre-
and post-conditions using automatically inferred auxiliary predicates as shown
in Fig. 5(c).

###  1.2 Beyond Loop-Invariant based Proofs

Techniques based on synthesis and use of loop invariants are popularly used to
reason about programs with loops. These techniques have been successfully
applied to verify different classes of array manipulating programs, viz. Gopan
; Halbwachs ; Rival ; ArrayCousotCL11 ; Gulwani ; Srivastava09 ; Dirk07 ;
Jhala ; freqhorn . If we were to prove the assertion in Fig. 1 using such
techniques, it would be necessary to use appropriate loop-specific invariants
for each of the three loops in Fig. 1. The weakest loop invariants needed to
prove the post-condition in this example are: $\forall
i\in[0,t1)\;(A[i]=6i+6)$ for the first loop (lines $1$-$4$), $\forall
j\in[0,t2)\;(B[j]=3j^{2}+3j+1)\wedge(A[j]=6j+6)$ for the second loop (lines
$5$-$8$), and $\forall k\in[0,t3)\;(C[k]=k^{3})\wedge(B[k]=3k^{2}+3k+1)$ for
the third loop (lines $9$-$12$). Notice that these invariants are quantified
and have non-linear terms. Similarly, the weakest loop invariants needed to
prove the post-condition for the program in Fig. 5(a) are: $\forall
j\in[0,i)\;(A[j]=1)\wedge(S=j)$ for the first loop (lines $2$-$4$), $\forall
k\in[0,i)\;(A1[k]=N+1)\wedge(A[k]=1)\wedge(S=N)$ for the second loop (lines
$5$-$7$), and $\forall l\in[0,i)\;(A1[l]=N+1)\wedge(S1=l\times(N+1)+N)$ for
the third loop (lines $9$-$11$).

Unfortunately, automatically deriving such quantified non-linear inductive
invariants for each loop is far from trivial. Template-based invariant
generators, viz. houdini ; daikon , are among the best-performers when
generating such complex invariants. However, their abilities are fundamentally
limited by the set of templates from which they choose. We therefore choose
not to depend on inductive loop-invariants at all in our work. Instead, we
make use of inductive pre- and post-conditions – a notion that is related to,
yet significantly different from loop-specific invariants. Specifically,
inductive pre- and post-conditions are computed for the entire program,
possibly consisting of multiple loops, instead of for each loop in the
program.

As is clear from the discussion above, the primary difference between a proof
generated by an invariant synthesis technique and the proof generated by our
method is that we no longer need loop-specific safe inductive invariants.
Instead, we generate and verify the Hoare triples shown in Figs. 2 and 3
considering the entire program $\mathsf{P}_{N}$ in Fig. 1 and the Hoare triple
shown in Fig. 5(c) considering the entire program $\mathsf{P}_{N}$ in Fig.
5(a). Automatically generating these Hoare triples in some cases may be more
difficult than automatically generating inductive invariants for each loop and
vice versa. However, as demonstrated by the motivating examples, there are
several complex programs, where it may be easier to generate these Hoare
triples than compute safe inductive invariants for individual loops. It is a
considerable challenge for verification techniques to be able to automatically
generate these invariants and to the best of our knowledge none of the current
state-of-the-art techniques do so.

###  1.3 Effectiveness of Full-Program Induction

We have implemented the full-program induction technique in a prototype tool
called Vajra. Written in C++, the tool is built on top of a compiler framework
(LLVM/CLANG clang ) and uses an off-the-shelf SMT solver (Z3 z3 ) at the back-
end. Our experiments show that the full-program induction technique is able to
solve several difficult problem instances, which other techniques either fail
to solve, or can solve only with the help of sophisticated recurrence solvers.
Vajra is significantly more efficient as compared to other tools on a set of
benchmarks.

Needless to say, each approach has its own strengths and limitations, and the
right choice always depends on the problem at hand. Full-program induction is
no exception, and despite its several strengths, it has its own limitations,
which we discuss in detail in Sect. 7.1.

The full-program induction technique is orthogonal to other verification
approaches proposed in literature, making it suitable to be a part of an
arsenal of verification techniques. It has already been incorporated within a
verification tool, namely VeriAbs veriabs20 . Since the 2020 edition of the
international software verification competition (SV-COMP), VeriAbs invokes
full-program induction (via our tool Vajra) in its pipeline of techniques for
verifying programs with arrays from the set of benchmarks in the verification
competition (refer veriabs20 ).

###  1.4 Primary Contributions of our Work

This paper is a revised and extended version of tacas20 . Our main
contributions can be summarized as follows:

  1. 1.

We introduce _full-program induction_ as a technique for reasoning about
assertions in programs with loops manipulating arrays with parametric size
bounds. Full-program induction does not need loop-specific invariants in order
to prove assertions, even when the program contains multiple sequentially
composed loops.

  2. 2.

We describe practical algorithms for performing _full-program induction_. We
elaborate the generalized algorithms for computing the difference program and
the difference pre-condition.

  3. 3.

We present a new algorithm to compute a progress measure, based on the
characteristics of the difference program. This gives a measure of how easy it
is to prove the inductive step of our technique using constraint solving based
techniques like bounded model checking.

  4. 4.

We give rigorous proofs of correctness for the presented algorithms. We
demonstrate these algorithms using a running example.

  5. 5.

We present generalizations of the full-program induction technique to programs
with multiple parameters and loops with increasing and/or decreasing loop
counters.

  6. 6.

We describe a prototype tool Vajra that implements the algorithms for
performing full-program induction, using (i) the compiler framework LLVM/CLANG
for analysis and transformation of the input program and (ii) an off-the-shelf
SMT solver, viz. Z3, at the back-end to discharge verification conditions.

  7. 7.

We present an extensive experimental evaluation on a large suite of benchmarks
that manipulate arrays. Vajra outperforms the state-of-the-art tools VIAP,
VeriAbs, Booster, Vaphor, and FreqHorn, on the set of benchmark programs.

Several contributions listed above are beyond those presented in tacas20 .
These include the contributions $2$, $3$, $4$, $5$, and $7$.

The remainder of the paper is structured as follows. In Sect. 2, we give a
formal overview of the full-program induction technique. Sect. 3 presents the
syntactic restrictions on the program as well as the pre- and post-conditions
and the representation of programs as control flow graphs. Sect. 4 discusses
the algorithms for computing the difference program and the difference pre-
condition, as well as the pre-requisite analyses and transformations. In Sect.
5, we present the algorithms for full-program induction, prove their
correctness and demonstrate each algorithm on the running example. In Sect. 6,
we give an algorithm to check whether the recursive application of our
technique will eventually be able to verify the given program. Sect. 7 talks
of the generalizations of our technique in different settings. Sect. 8
presents the implementation of our technique in Vajra, its evaluation on a set
of benchmarks and comparison vis-a-vis state-of-the-art tools. In Sect. 9, we
discuss the related techniques from literature. Finally, Sect. 10 presents
concluding remarks on our work and possible future directions.

##  2 Overview of Full-Program Induction

$\boldsymbol{\varphi}$(N)$\boldsymbol{\psi}$(N)$\mathbf{P_{N}}$

Figure 6: Goal

We now elaborate on the core idea behind the full-program induction technique.
Our goal is to check the validity of the parameterized Hoare triple
$\\{\varphi(N)\\}$ $\;\mathsf{P}_{N}\;$ $\\{\psi(N)\\}$ for all $N>0$. A
visual representation of this Hoare triple is shown in Fig. 6, where the
clouds represent (possibly quantified) formulas and boxes represent
programs/code fragments.

Intuitively, at a conceptual level, our approach works like any other
inductive reasoning technique. However, the induction is over the entire
program, via the program parameter $N$, and not on the individual loops in the
program.

We first check the base case, where we verify that the parameterized Hoare
triple holds for some small values of $N$, say $0<N\leq M$. We rely on an
important, yet reasonable, assumption that can be stated as follows: _For
every value of $N~{}(>0)$, every loop in ${\mathsf{P}_{N}}$ can be statically
unrolled a number (say $f(N)$) of times that depends only on $N$, to yield a
loop-free program $\widehat{\mathsf{P}_{N}}$ that is semantically equivalent
to ${\mathsf{P}_{N}}$._ Note that this does not imply that reasoning about
loops can be translated into loop-free reasoning. In general, $f(N)$ is a non-
constant function, and hence, the number of unrollings of loops in
$\mathsf{P}_{N}$ may strongly depend on $N$. In our experience, loops in a
vast majority of array manipulating programs (including Figs. 1 and 4 and all
our benchmarks) satisfy the above assumption. Consequently, the base case of
our induction reduces to checking a Hoare triple for a loop-free program.
Checking a Hoare triple for a loop-free program is easily achieved by
compiling the pre-condition, program and post-condition into an SMT formula,
whose (un)satisfiability can be checked with an off-the-shelf back-end SMT
solver.

$\boldsymbol{\varphi}$(N-1)$\boldsymbol{\psi}$(N-1)$\mathbf{P_{N\text{-}1}}$

Figure 7: Hypothesis

Next we hypothesize that $\\{\varphi(N-1)\\}$ $\;\mathsf{P}_{N-1}\;$
$\\{\psi(N-1)\\}$ holds for some $N>M$, visually depicted in Fig. 7. A few
things are worth mentioning here. First, the entire Hoare triple is assumed
not just the formula in the post-condition. Second, the assumption is not on a
specific loop in the program, but the entire program $\mathsf{P}_{N}$. Third,
the change in the parameter from $N$ to $N-1$ is uniform across the entire
Hoare triple and not on a specific part there-off.

We then try to show that the induction hypothesis implies $\\{\varphi(N)\\}$
$\;\mathsf{P}_{N}\;$ $\\{\psi(N)\\}$. While this sounds simple in principle,
there are several technical difficulties en-route. Our contribution lies in
overcoming these difficulties algorithmically for a large class of programs
and assertions, thereby making full-program induction a viable and competitive
technique for proving properties of array manipulating programs.

The inductive step is the most complex one, and is the focus of the rest of
the paper. Recall that the inductive hypothesis asserts that
$\\{\varphi(N-1)\\}$ $\;{\mathsf{P}_{N-1}}\;$ $\\{\psi(N-1)\\}$ is valid. To
make use of this hypothesis in the inductive step, we must relate the validity
of $\\{\varphi(N)\\}$ $\;{\mathsf{P}_{N}}\;$ $\\{\psi(N)\\}$ to that of
$\\{\varphi(N-1)\\}$ $\;{\mathsf{P}_{N-1}}\;$ $\\{\psi(N-1)\\}$. We propose
doing this, whenever possible, via two key notions – that of “difference”
program and “difference” pre-condition.

$\boldsymbol{\varphi}$(N-1)$\boldsymbol{\psi}$(N-1)$\mathbf{P_{N\text{-}1}}$$\boldsymbol{\psi}$(N)$\boldsymbol{\partial}\mathbf{P_{N}}$$\boldsymbol{\partial\varphi}$(N)$\boldsymbol{\partial\varphi}$(N)

Figure 8: Transformations

Given a parameterized program ${\mathsf{P}_{N}}$, intuitively the “difference”
program ${\partial\mathsf{P}_{N}}$ is one such that $\\{\varphi(N)\\}$
$\;{\mathsf{P}_{N}}\;$ $\\{\psi(N)\\}$ holds iff $\\{\varphi(N)\\}$
$\;{\mathsf{P}_{N-1}}\mathchar 24635\relax\;{\partial\mathsf{P}_{N}}\;$
$\\{\psi(N)\\}$ holds, where “;” denotes sequential composition. Refer to Fig.
8 for a visual representation of the Hoare triple after the decomposition of
$\mathsf{P}_{N}$ into $\mathsf{P}_{N-1}$ and $\partial\mathsf{P}_{N}$. We will
use this interpretation of a “difference” program in the subsequent parts of
this paper.

$\mathbf{P_{N}}$$\mathbf{P_{N\text{-}1}}$$\boldsymbol{\partial}\mathbf{P_{N}}$$\boldsymbol{\equiv}$

Figure 9: Decomposition of $\mathsf{P}_{N}$ and semantic equivalence

A simple way of ensuring the correctness of this transformation is by having a
difference program ${\partial\mathsf{P}_{N}}$ such that the sequential
composition ${\mathsf{P}_{N-1}}\mathchar
24635\relax\;{\partial\mathsf{P}_{N}}$ is semantically equivalent to
${\mathsf{P}_{N}}$. Decomposition of $\mathsf{P}_{N}$ into $\mathsf{P}_{N-1}$
and $\partial\mathsf{P}_{N}$ is visually depicted in Fig. 9. It ensures that,
upon termination, same program state is reached by both $\mathsf{P}_{N}$ and
${\mathsf{P}_{N-1}}\mathchar 24635\relax\;{\partial\mathsf{P}_{N}}$. The given
post-condition may not be impacted by the entire program state, and hence, the
semantic equivalence alluded to here may not be required, in general. Thus,
the semantic equivalence of the decomposition is a strong condition. It is
referred here only for the ease of explaining the inductive setup and for an
intuitive demonstration of soundness of the decomposition. For the purposes of
full-program induction semantic equivalence is not really necessary, and we do
not refer to this interpretation of the “difference” program further due to
its restrictive nature.

$\boldsymbol{\varphi}$(N)$\boldsymbol{\varphi}$(N-1)$\boldsymbol{\partial\varphi}$(N)$\boldsymbol{\rightarrow}$

Figure 10: Difference pre-condition

The “difference” pre-condition ${\partial\varphi(N)}$ is a formula such that
the following conditions hold.

  1. 1.

$\varphi(N)$ $\rightarrow$ $(\varphi(N-1)$ $\odot$ ${\partial\varphi(N)})$,
where the boolean operator $\odot$ is $\wedge$ when $\varphi(N)$ is a
universally quantified formula and it is $\vee$ when $\varphi(N)$ is a
existentially quantified formula. We depict this decomposition of $\varphi(N)$
into $\varphi(N-1)$ and ${\partial\varphi(N)}$ in Fig. 10.

  2. 2.

The execution of $\mathsf{P}_{N-1}$ does not affect the truth of
${\partial\varphi(N)}$. This can be visualized using Fig. 8, where the dashed
line indicates the propagation of the difference pre-condition across
$\mathsf{P}_{N-1}$ when it is not affected.

Computing the “difference” program ${\partial\mathsf{P}_{N}}$ and the
“difference” pre-condition ${\partial\varphi(N)}$ is not easy in general. In
Sect. 5, we discuss ways to overcome these problems and challenges.

$\boldsymbol{\psi}$(N-1)$\boldsymbol{\psi}$(N)$\boldsymbol{\partial}\mathbf{P_{N}}$$\boldsymbol{\partial\varphi}$(N)

Figure 11: Inductive step

Assuming we have ${\partial\mathsf{P}_{N}}$ and ${\partial\varphi(N)}$ with
the properties stated above, the proof obligation $\\{\varphi(N)\\}$
$\;\mathsf{P}_{N}\;$ $\\{\psi(N)\\}$ can now be reduced to proving the Hoare
triples $\\{\varphi(N-1)\\}$ $\;\mathsf{P}_{N-1}\;$ $\\{\psi(N-1)\\}$ and
$\\{\psi(N-1)\wedge{\partial\varphi(N)}\\}$ $\;{\partial\mathsf{P}_{N}}\;$
$\\{\psi(N)\\}$ in the inductive step. Both these Hoare triples can be easily
visualized from Fig. 8. The first Hoare triple follows from the inductive
hypothesis (Fig. 7), and hence, is available for free. Thus, the inductive
step is reduced to proving the second Hoare triple as shown in the Fig. 11.

Proving the inductive step may require strengthening the pre-condition, say by
a formula $\mathsf{Pre}(N-1)$, in general. Since we are in the inductive step
of mathematical induction, we formulate the new proof sub-goal in such a case
as $\\{(\psi(N-1)\wedge\mathsf{Pre}(N-1))\wedge{\partial\varphi(N)}\\}$
${\partial\mathsf{P}_{N}}$ $\\{\psi(N)\wedge\mathsf{Pre}(N)\\}$. While this is
somewhat reminiscent of loop invariants, observe that $\mathsf{Pre}(N)$ is
_not_ really a loop-specific invariant. Instead, it is analogous to computing
an invariant for the entire program, possibly containing multiple loops.
Specifically, the above process strengthens both the pre- and post-condition
of $\\{\psi(N-1)\wedge{\partial\varphi(N)}\\}$ ${\partial\mathsf{P}_{N}}$
$\\{\psi(N)\\}$ simultaneously using $\mathsf{Pre}(N-1)$ and
$\mathsf{Pre}(N)$, respectively. Fig. 12 shows the Hoare triple after the
strengthening step. The strengthened post-condition of the resulting Hoare
triple may, in turn, require a new pre-condition $\mathsf{Pre}^{\prime}(N-1)$
to be satisfied. This process of strengthening the pre- and post-conditions of
the Hoare triple involving $\partial{\mathsf{P}_{N}}$ can be iterated until a
fix-point is reached, i.e. no further pre-conditions are needed for the
parameterized Hoare triple to hold. While the fix-point was quickly reached
for all benchmarks we experimented with, we also discuss how to handle cases
where the above process may not converge easily. Note that since we
effectively strengthen the pre-condition of the Hoare triple in the inductive
step, for the overall induction to go through, it is also necessary to check
that the strengthened assertions hold at the end of each base case check.
Automatically computing $\mathsf{Pre}(N)$ to strengthen the pre- and post-
conditions of the Hoare triple may not always be straight forward, especially
when the difference program ${\partial\mathsf{P}_{N}}$ has loops. In such
cases, we recursively apply our technique on the Hoare triple
$\\{\psi(N-1)\wedge{\partial\varphi(N)}\\}$ ${\partial\mathsf{P}_{N}}$
$\\{\psi(N)\\}$ generated during the inductive step. This helps our technique
converge when the generated difference program has one or more loops. We check
if the recursive invocation of our technique will yield beneficial results
using a progress measure influenced by several characteristics of the
difference program.

$\boldsymbol{\varphi}$(N-1)$\boldsymbol{\psi}$(N-1)$\mathbf{P_{N\text{-}1}}$$\boldsymbol{\psi}$(N)$\boldsymbol{\partial}\mathbf{P_{N}}$$\boldsymbol{\partial\varphi}$(N)$\boldsymbol{\partial\varphi}$(N)$\boldsymbol{\mathsf{Pre}}$(N-1)$\boldsymbol{\mathsf{Pre}}$(N)

Figure 12: Strengthing pre- and post-conditions

The technique outlined above is called _full-program induction_ , and the
following theorem is the basis for the soundness of _full-program induction_.

######  Theorem 1.

Given $\\{\varphi(N)\\}$ $\;\mathsf{P}_{N}\;$ $\\{\psi(N)\\}$, suppose the
following are true:

  1. 1.

For $N>1$, $\\{\varphi(N)\\}$ $\;\mathsf{P}_{N-1}\mathchar
24635\relax\;{\partial\mathsf{P}_{N}}\;$ $\\{\psi(N)\\}$ holds iff
$\\{\varphi(N)\\}$ $\;\mathsf{P}_{N}\;$ $\\{\psi(N)\\}$ holds.

  2. 2.

For $N>1$, there exists a formula ${\partial\varphi(N)}$ such that

     * (a)

${\partial\varphi(N)}$ doesn’t refer to any program variable or array element
modified in $\mathsf{P}_{N-1}$, and

     * (b)

$\varphi(N)$ $\rightarrow$ $\varphi(N-1)$ $\wedge$ ${\partial\varphi(N)}$.

  3. 3.

There exists an integer $M\geq 1$ and a parameterized formula
$\mathsf{Pre}(M)$ such that

     * (a)

$\\{\varphi(N)\\}$ $\;\mathsf{P}_{N}\;$ $\\{\psi(N)\\}$ holds for $0<N\leq M$,

     * (b)

$\\{\varphi(M)\\}$ $\;\mathsf{P}_{M}\;$ $\\{\psi(M)\wedge\mathsf{Pre}(M)\\}$
holds, and

     * (c)

$\\{\psi(N-1)\wedge\mathsf{Pre}(N-1)\wedge{\partial\varphi(N)}\\}$
$\;{\partial\mathsf{P}_{N}}\;$ $\\{\psi(N)\wedge\mathsf{Pre}(N)\\}$ holds for
$N>M$.

Then $\\{\varphi_{N}\\}$ $\;\mathsf{P}_{N}\;$ $\\{\psi_{N}\\}$ holds for all
$N\geq 1$.

Proof: For $0<N\leq M$, condition 3(a) (the base case) ensures that
$\\{\varphi(N)\\}$ $\;\mathsf{P}_{N}\;$ $\\{\psi(N)\\}$ holds. For $N>M$, note
that by virtue of conditions 1 and 2(b), $\\{\varphi(N)\\}$
$\;\mathsf{P}_{N}\;$ $\\{\psi(N)\\}$ holds if
$\\{\varphi(N-1)\wedge{\partial\varphi(N)}\\}$ $\;\mathsf{P}_{N-1}\mathchar
24635\relax\;{\partial\mathsf{P}_{N}}\;$ $\\{\psi(N)\wedge\mathsf{Pre}(N)\\}$
holds. With $\psi(N-1)\wedge\mathsf{Pre}(N-1)$ as a mid-condition, and by
virtue of condition 2(a), the latter Hoare triple holds for $N>M$ if
$\\{\varphi(M)\\}$ $\;\mathsf{P}_{M}\;$ $\\{\psi(M)\wedge\mathsf{Pre}(M)\\}$
holds and $\\{\psi(N-1)\wedge\mathsf{Pre}(N-1)\wedge{\partial\varphi(N)}\\}$
$\;{\partial\mathsf{P}_{N}}\;$ $\\{\psi(N)\wedge\mathsf{Pre}(N)\\}$ holds for
all $N>M$. Both these triples are seen to hold by virtue of conditions 3(b)
and (c).

##  3 Preliminaries

$\mathsf{PB}$ | ::= | $\mathsf{St}$
---|---|---
$\mathsf{St}$ | ::= |  $\mathsf{AssignSt}$ $\mid$ $\mathsf{St}$ ; $\mathsf{St}$ $\mid$ $\mathbf{if}$($\mathsf{BoolE}$) $\mathbf{then}$ $\mathsf{St}$ $\mathbf{else}$ $\mathsf{St}$ $\mid$ $\mathbf{for}$ ($\ell$ := 0; $\ell$ $<$ $\mathsf{LBnd}$; $\ell$ := $\ell$+1) {$\mathsf{StLF}$}
$\mathsf{AssignSt}$ | ::= |  $v$ = $\mathsf{E}$ $\mid$ $A$[$\mathsf{IndE}$] = $\mathsf{E}$
$\mathsf{StLF}$ | ::= |  $\mathsf{AssignSt}$ $\mid$ $\mathsf{StLF}$ ; $\mathsf{StLF}$ $\mid$ $\mathbf{if}$($\mathsf{BoolE}$) $\mathbf{then}$ $\mathsf{StLF}$ $\mathbf{else}$ $\mathsf{StLF}$
$\mathsf{E}$ | ::= |  $\mathsf{E}$ $\mathsf{op}$ $\mathsf{E}$ $\mid$ $A$[$\mathsf{IndE}$] $\mid$ $v$ $\mid$ $\ell$ $\mid$ $\mathsf{c}$ $\mid$ $N$
$\mathsf{IndE}$ | ::= |  $\mathsf{IndE}$ $\mathsf{op}$ $\mathsf{IndE}$ $\mid$ $v$ $\mid$ $\ell$ $\mid$ $\mathsf{c}$ $\mid$ $N$
$\mathsf{LBnd}$ | ::= |  $\mathsf{LBnd}$ $\mathsf{op}$ $\mathsf{LBnd}$ $\mid$ $\mathsf{c}$ $\mid$ $N$
$\mathsf{op}$ | ::= | \+ $\mid$ \- $\mid$ $\times$ $\mid$ $\div$ $\mid$ $\ldots$
$\mathsf{BoolE}$ | ::= |  $\mathsf{E}$ $\mathsf{relop}$ $\mathsf{E}$ $\mid$ $\mathsf{BoolE}$ $\mathsf{AND}$ $\mathsf{BoolE}$ $\mid$ $\mathsf{NOT}$ $\mathsf{BoolE}$ $\mid$ $\mathsf{BoolE}$ $\mathsf{OR}$ $\mathsf{BoolE}$
$\mathsf{relop}$ | ::= |  $==$ $\mid$ $<$ $\mid$ $\leq$ $\mid$ $>$ $\mid$ $\geq$
Figure 13: Program grammar

We consider array manipulating programs generated by the grammar shown in Fig.
13 (adapted from sas17 ). This grammar restricts programs to have non-nested
loops. Specifically, programs generated starting from $\mathsf{StLF}$ are loop
free. The non-terminal $\mathsf{St}$ can generate programs with loops but
their bodies are generated from $\mathsf{StLF}$, thereby forbidding nesting of
loops. Note also that expressions for indexing arrays are generated from the
non-terminal $\mathsf{IndE}$, and such expressions cannot refer to other array
elements. However, this is not really a restriction on the expressive power of
programs since every array index expression that depends on other array
elements, say $A[e]$, can be replaced by an array index expression that
depends on temporary variables, say $v$, that are pre-assigned to the
respective array elements, viz. $A[e]$. For example, A[B[i]] = C[D[i]]; can be
rewritten as v1 = B[i]; v2 = D[i]; A[v1] = C[v2];. Finally, note that loop
bound expressions are generated using the non-terminal $\mathsf{LBnd}$, and
such expressions can only involve constants and the parameter $N$. While the
above restrictions limit the class of programs to which our technique
currently applies, there is still a large collection of useful programs, with
possibly long sequences of loops, that are included in the scope of our work.
In reality, our technique also applies to a sub-class of programs with nested
loops and with loop bound expressions that involve scalar variables. However,
characterizing this sub-class of programs through a grammar is a bit unwieldy,
and we avoid doing so for reasons of clarity.

A program $\mathsf{P}_{N}$ is a tuple
$(\mathcal{V},\mathcal{L},\mathcal{A},{\mathsf{PB}},N)$, where $\mathcal{V}$
is a set of scalar variables, $\mathcal{L}\subseteq\mathcal{V}$ is a set of
loop counter variables, $\mathcal{A}$ is a set of array variables,
${\mathsf{PB}}$ is the program body, and $N$ is a special symbol denoting a
positive integer parameter. In the grammar shown above, we assume
${A}\in\mathcal{A}$, ${v}\in\mathcal{V}\setminus\mathcal{L}$,
${\ell}\in\mathcal{L}$ and ${\mathsf{c}}\in\mathbb{Z}$. Furthermore,
“$\mathsf{relop}$” is assumed to be one of the relational operators and
“$\mathsf{op}$” is an arithmetic operator. We discuss more about the operators
supported by our technique in Sect. 4.5. We also assume that each loop $L$ has
a unique loop counter variable $\ell$ that is initialized at the beginning of
$L$ and is incremented by $1$ at the end of each iteration. Assignments in the
body of $L$ are assumed not to update $\ell$. Finally, for each loop with
termination condition $\ell<\mathsf{LBnd}$, we assume that $\mathsf{LBnd}$ is
an expression in terms of $N$. We denote by $k_{L}(N)$ the number of times
loop $L$ iterates in the program with parameter $N$.

We admit Hoare triples of the form $\\{\varphi(N)\\}$ $\;\mathsf{P}_{N}\;$
$\\{\psi(N)\\}$, where $\varphi(N)$ and $\psi(N)$ are either universally
quantified, existentially quantified or quantifier-free formulas of the form
$\forall I\,$
$\left(\Phi(I,N)\implies\Psi(\mathcal{A},\mathcal{V},I,N)\right)$, $\exists
I\,$ $\left(\Phi(I,N)\wedge\Psi(\mathcal{A},\mathcal{V},I,N)\right)$ and
$\Upsilon(\mathcal{A},\mathcal{V},N)$ respectively. In the above, $I$ is an
array index variable, $\Phi$ is a quantifier-free formula in the theory of
arithmetic over integers, and $\Psi$ and $\Upsilon$ are quantifier-free
formulas in the combined theory of arrays and arithmetic over integers. Our
technique also works for conjunctions and disjunctions of such formulas as
pre- and post-conditions in some cases as discussed in Sect. 4.7.

###  3.1 Tracking Control Flow

We represent a program $\mathsf{P}_{N}$ using its control flow graph (or CFG)
$G_{C}=(\mathit{Locs},CE,\mu)$, where $Locs$ denotes the set of control
locations (nodes) of the program,
$CE\subseteq\mathit{Locs}\times\mathit{Locs}\times\\{\mathbf{tt},\mathbf{ff},\mathsf{U}\\}$
are the control-flow edges, and
$\mu:\mathit{Locs}\rightarrow{\mathsf{AssignSt}}$ $\cup$ ${\mathsf{BoolE}}$
annotates every node in $Locs$ with either an assignment statement (of the
form ${v}=\mathsf{E}$ or ${A}[\mathsf{IndE}]=\mathsf{E}$) from those
represented by $\mathsf{AssignSt}$, or a Boolean expression from those
represented by $\mathsf{BoolE}$. Two distinguished control locations, called
$n_{start}$ and $n_{end}$ in $\mathit{Locs}$ represent the entry and exit
points of the program. An edge $(n_{1},n_{2},label)$ represents flow of
control from $n_{1}$ to $n_{2}$ without any other intervening node. It is
labeled $\mathbf{tt}$ or $\mathbf{ff}$ if $\mu(n_{1})$ is a Boolean condition,
and is labeled $\mathsf{U}$ otherwise. If $\mu(n_{1})$ is a Boolean condition,
there are two outgoing edges from $n_{1}$, labeled $\mathbf{tt}$ and
$\mathbf{ff}$ respectively, and control flows from $n_{1}$ to $n_{2}$ along
$(n_{1},n_{2},label)$ only if $\mu(n_{1})$ evaluates to $label$. If
$\mu(n_{1})$ is an assignment statement, there is a single outgoing edge from
$n_{1}$, and it is labeled $\mathsf{U}$. Henceforth, we use CFG to refer to a
control flow graph, and use $\mathsf{P}_{N}$ to refer to both a program and
its CFG, when there is no confusion.

Start12345678910End$~{}~{}~{}~{}\mathbf{tt}$$\mathbf{ff}~{}~{}~{}~{}$$~{}~{}~{}~{}\mathbf{tt}$$\mathbf{ff}~{}~{}~{}~{}$$~{}~{}~{}~{}\mathbf{tt}$$\mathbf{ff}~{}~{}~{}~{}$
Figure 14: CFG of Fig. 4

A CFG may have cycles due to the presence of loops in the program. A _back-
edge_ of a loop is an edge from the node corresponding to the last statement
in the loop body to the node representing the loop head. An _exit-edge_ is an
edge from the loop head to a node outside the loop body. An _incoming-edge_ is
an edge to the loop head from a node outside the loop body. We assume that
every loop has exactly one _back-edge_ , one _incoming-edge_ and one _exit-
edge_.

A node $n$ in a control flow graph _strictly post-dominates_ a node $m$ if all
control flow paths from node $m$ pass through $n$ before reaching the exit
node and $m$ is not the same as $n$. The _immediate post-dominator_ of node
$n$ is a node that strictly post-dominates $n$ but does not strictly post-
dominate any other node that strictly post-dominates $n$.

For every node $n$ in the CFG, we use $\mathit{def}(n)$ and $\mathit{uses}(n)$
to refer to the set of scalar variables and arrays (not loop counter
variables) that are defined and used, respectively, in the statement or
boolean expression at $n$. We include the symbolic parameter $N$ in the set
$\mathit{uses}(n)$ if the statement at node $n$ makes use of $N$. Since the
parameter $N$ cannot be re-defined by any program generated according to the
grammar in Fig. 13, it never appears in $\mathit{def}(n)$ for any node $n$. If
$A$ represents an array in $\mathit{def}(n)$, we use $\mathit{defIndex}(A,n)$
to refer to the index expression of the element of $A$ updated at $n$.
Similarly, if $A\in\mathit{uses}(n)$, we use $\mathit{useIndexSet}(A,n)$ to
refer to the set of index expression(s) of element(s) of $A$ read at $n$.

######  Example 1.

The CFG of the program in Fig. 4 is shown in Fig. 14. The nodes are numbered
such that they coincide with the line numbers in the program. The graph has
three cycles each corresponding to a loop in the given program. { $(1,2)$,
$(2,5)$, $(5,8)$ } are _incoming-edges_ , { $(4,2)$, $(7,5)$, $(10,8)$ } are
_back-edges_ and { $(2,5)$, $(5,8)$, $(8,End)$ } are _exit-edges_.

Node $2$ strictly post-dominates nodes $1$, $4$ and $Start$. Node $2$ is an
immediate post-dominator of $1$ and $4$. Node $8$ strictly post-dominates all
nodes except itself and $End$. Node $8$ is an immediate post-dominator of $5$
and $10$. $End$ node strictly post-dominates all nodes except itself. $Start$
node does not strictly post-dominate any other node. Similarly, the post-
domination relations for other nodes can be computed.

The set of scalars and arrays defined at nodes $1$, $3$ and $9$ is
$\mathit{def}(n)$ := {S} and the set at node $6$ is $\mathit{def}(n)$ = {A}.
The index of A updated at node $6$ is $\mathit{defIndex}$(A,$6$) = i. The set
of scalars and arrays used at nodes $3$, $6$ and $9$ is $\mathit{uses}(n)$ =
{S, A}. For node $1$, as there are no uses of scalars or arrays,
$\mathit{uses}(n)$ = $\emptyset$. The set of indices of array A used at nodes
$3$, $6$ and $9$ is $\mathit{useIndexSet}$(A,$n$) = {i}.

##  4 Difference Computation

Renaming$\mathsf{P}_{N}$Peeling$\mathsf{P}_{N}^{r}$GeneratingDifferenceProgramSimplified
$\boldsymbol{\partial}\mathsf{P}_{N}$IdentifyingAffectedVariables$\mathsf{P}_{N}^{p}$AffectedVars$\mathsf{P}_{N}^{p}$$G_{D}$$\mathsf{P}_{N}^{p}$ComputingDDGSimplifyingDifferenceProgram$\boldsymbol{\partial}\mathsf{P}_{N}$

Figure 15: Sequence of steps for the computation of the difference program
$\partial\mathsf{P}_{N}$.

In this section, we focus on the generation of two crucial components for
performing _full-program induction_ , namely (i) the _difference program_
${\partial\mathsf{P}_{N}}$ and (ii) the _difference pre-condition_
${\partial\varphi(N)}$.

Computing the _difference program_ ${\partial\mathsf{P}_{N}}$ is a non-trivial
endeavor. Fig. 15 presents a high level overview of the sequence of steps
involved in the generation of a difference program. We first carefully rename
the variables and arrays such that each loop in the renamed program refers to
its own copy of variables/arrays. Note that this is similar in spirit to SSA
renaming, although there are important differences that will become clear in
Sect. 4.1. We next peel the last (in some cases the last few) iteration(s) of
each loop in the program such that the remaining part of each loop in the
peeled version of $\mathsf{P}_{N}$ iterates exactly the same number of times
as the corresponding loop in $\mathsf{P}_{N-1}$. Throughout this paper, we use
the term _peel_ to denote the last (or last few as the case may be)
iteration(s) of a loop that have been removed from the loop. The motivation
for this peeling is that the difference program can often be constructed by
moving the peels of individual loops to the end of the program and stitching
them up in appropriate ways, as will be discussed in detail in Sects. 4.5.4
and 4.5.5. In order to ensure that the semantics of the program is preserved
even after moving the peels to the end of the program, we need to do a careful
analysis of the data dependencies between between variables and array elements
updated/read in statements within loops and those updated/read in the peeled
iterations. This is achieved by computing a customized data dependence graph,
details of which are presented in Sect. 4.3. In general, variables and array
elements in the program $\mathsf{P}_{N}$ can have data/control dependencies on
the parameter $N$ beyond those attributable to the iteration counts of loops
being possibly determined by $N$. We call such variables/array elements as
“affected” by $N$ and identify them using a special data-flow analysis and the
data dependencies computed above. Details of this analysis are presented in
Sect. 4.4. Finally, we move the peels of loops to the end of the program and
use the information about data dependencies and affected variables computed
above to appropriately stitch and modify them to obtain an unoptimized version
of the difference program. In general, this modification may involve adding
carefully constructed loops in the difference program itself. It turns out
that the difference program obtained in this way can often be significantly
optimized using simple optimization techniques. This includes things like
pruning superfluous computational steps and accelerating loops among others.
We include this optimization as the last step in our flow for generating the
difference program.

Our empirical studies show that for the success of full-program induction, it
is very important that the difference program $\partial\mathsf{P}_{N}$ be
“simpler” (defined more precisely later) than the original program
$\mathsf{P}_{N}$. The optimizations enabled by the affected variable analysis
and the simplification of the difference program are crucial to actualize this
requirement. Each of the above steps, depicted in Fig. 15, is elaborated in
Sects. 4.1 \- 4.6.

###  4.1 Renaming Variables and Arrays

Recall that our proposed approach requires us to construct a difference
program $\partial\mathsf{P}_{N}$ such that $\\{\varphi(N)\\}$
$\;{\mathsf{P}_{N}}\;$ $\\{\psi(N)\\}$ holds iff $\\{\varphi(N)\\}$
$\;{\mathsf{P}_{N-1}}\mathchar 24635\relax\;{\partial\mathsf{P}_{N}}\;$
$\\{\psi(N)\\}$ holds (condition $1$ of Theorem 1). A natural (though not
necessary) way to do this is to construct $\partial\mathsf{P}_{N}$ such that
both $\mathsf{P}_{N}$ and $\mathsf{P}_{N-1}\mathchar
24635\relax\;\partial\mathsf{P}_{N}$ modify all relevant scalar variables and
arrays in exactly the same way. Note, however, that $\mathsf{P}_{N}$ may
update the same scalar variable or array in multiple sequentially composed
loops. Therefore, when $\mathsf{P}_{N-1}$ terminates and
$\partial\mathsf{P}_{N}$ starts executing (in $\mathsf{P}_{N-1}\mathchar
24635\relax\;\partial\mathsf{P}_{N}$), we may no longer have access to the
values of scalar variables and arrays that resulted after individual loops in
$\mathsf{P}_{N-1}$ terminated. In general, this makes it difficult to
construct $\partial\mathsf{P}_{N}$ compositionally from the peels of
individual loops while ensuring that $\mathsf{P}_{N-1}\mathchar
24635\relax\;\partial\mathsf{P}_{N}$ has the same effect as $\mathsf{P}_{N}$
on all relevant scalar variables and arrays. To circumvent this problem, we
propose to pre-process $\mathsf{P}_{N}$ such that each loop in
$\mathsf{P}_{N}$ updates its own “private” copy of scalar variables and
arrays. We add _glue code_ to copy the values of these scalar variables and
arrays after one loop ends and before the next one begins. We also rename the
variables/arrays referred in the post-condition $\psi(N)$ to their versions
corresponding to the last loop in the program. As we show later, this eases
the construction of $\partial\mathsf{P}_{N}$, and also helps in inductive
strengthening of the pre- and post-conditions.

It is important to note here that static single assignment (SSA) ssa  is a
well-known technique for renaming scalar variables such that a variable is
updated at most once in a program. Similarly, array SSA renaming has been
studied earlier in the context of compilers to achieve similar goals arrayssa
. Unlike SSA renaming, we do not have the stringent requirement of a single
update in the whole program. For our method to function successfully, we only
require each loop to update its own copy of a scalar/array variable. We note
that these well-studied techniques can be easily adapted for our purposes.

In the following discussion, we define the _collapsed CFG of a program_
$\mathsf{P}_{N}$ as the CFG obtained by collapsing all nodes and edges in the
body of each loop of $\mathsf{P}_{N}$ into a single node identified with the
loop-head. Given the syntactic restrictions on the input programs as discussed
in Sect. 3, the collapsed CFG is a finite directed acyclic graph (DAG). This
DAG has finitely many paths, and along each such path, there is a total
ordering of all collapsed loops appearing along the path. For notational
clarity, we henceforth use $vA$ (as opposed to $v$ for a scalar variable and
$A$ for an array) as a combined symbolic name to refer to a scalar variable or
array, depending on the context. At each node $n$ of the collapsed CFG, we
rename each scalar/array $vA$ to $vA^{n}$. Note that when $n$ is a loop-head,
this amounts to renaming all scalars/arrays in the body of the loop as well
(due to collapsing of nodes in the loop body). To ensure the correct flow of
data values between nodes of the collapsed CFG, we create fresh nodes called
_glue nodes_ whenever required, and add program statements in these glue nodes
that effectively copy values of the appropriate scalars/arrays from one node
of the collapsed CFG to another.

We assume the availability of a function Rename, that generates a program with
the necessary renaming as described, while ensuring correct data flow. For
notational convenience, we call the renamed program corresponding to
$\mathsf{P}_{N}$ as $\mathsf{P}_{N}^{r}$. The interested reader can find a
detailed algorithm for Rename in divyesh-phdthesis .

    // assume(

    $\ignorespaces\forall$

    i

    $\ignorespaces\in$

    [0,N) A[i] = 1)

    1.  S = 0;
    2.  for(i=0; i<N; i++) {
    3.    S = S + A[i];
    4.  }

    5.  for(i=0; i<N; i++) {
    6.    A[i] = A[i] + S;
    7.  }

    8.  for(i=0; i<N; i++) {
    9.    S = S + A[i];
    10. }

    // assert(S = N

    $\ignorespaces\times$

     (N+2))

(a)

    // assume(

    $\ignorespaces\forall$

    i

    $\ignorespaces\in$

    [0,N) A[i] = 1)

    1.  S = 0;
    2.  for(i=0; i<N; i++) {
    3.    S = S + A[i];
    4.  }

    5.  for(i=0; i<N; i++) {
    6.    A1[i] = A[i] + S;
    7.  }

    8.  S1 = S;   // Glue code
    9.  for(i=0; i<N; i++) {
    10.   S1 = S1 + A1[i];
    11. }

    // assert(S1 = N

    $\ignorespaces\times$

     (N+2))

(b)

Figure 16: (a) Running example and (b) Hoare triple with renamed program

######  Lemma 1.

Let $n$ be a node in the collapsed CFG of $\mathsf{P}_{N}$. In every execution
of the renamed program $\mathsf{P}_{N}^{r}$ in which control flows through
$n$, the scalar variable/array $vA^{n}$ is not updated after the execution
exits $n$.

Proof: Since the collapsed CFG of $\mathsf{P}_{N}^{r}$ is acyclic, once
control flow exits node $n$, it cannot come back to either $n$ or to any node
$n^{\prime}$ that has a control flow path to $n$. The proof now follows from
the observation that renaming ensures that any scalar variable/array renamed
$vA^{n}$ can only be updated in glue nodes immediately leading to node $n$ or
in node $n$ itself.

For convenience of exposition, we will henceforth refer to the property
formalized in Lemma 1 as the _“no-overwriting”_ property of renamed programs.
For a node $n$ that corresponds to a collapsed loop in the collapsed CFG of
$\mathsf{P}_{N}$, we will also use the notation $\mu(n)$ to denote the entire
loop represented by $n$ in the subsequent discussion.

######  Lemma 2.

$\\{\varphi(N)\\}$ $\;\mathsf{P}_{N}\;$ $\\{\psi(N)\\}$ holds iff
$\\{\varphi^{r}(N)\\}$ $\;\mathsf{P}^{r}_{N}\;$ $\\{\psi^{r}(N)\\}$ holds.

Proof: (Sketch) Suppose the Hoare triple $\\{\varphi(N)\\}$
$\;\mathsf{P}_{N}\;$ $\\{\psi(N)\\}$ holds. Then, at every node $n$ in the
collapsed CFG of $\mathsf{P}_{N}$ there exists a pre-condition invariant
$\mathsf{Inv}^{pre}_{n}$ and a post-condition invariant
$\mathsf{Inv}^{post}_{n}$, such that (i) the Hoare triple
$\\{\mathsf{Inv}^{pre}_{n}\\}$ $\;\mu(n)\;$ $\\{\mathsf{Inv}^{post}_{n}\\}$ at
node $n$ holds (ii) the composition of these Hoare triples entails
$\\{\varphi(N)\\}$ $\;\mathsf{P}_{N}\;$ $\\{\psi(N)\\}$. Note that once
renaming is done, the Hoare triple obtained by renaming variables/arrays in
$\mathsf{Inv}^{pre}_{n}$ and $\mathsf{Inv}^{post}_{n}$ and by replacing
$\mu(n)$ with the corresponding renamed program statement(s) holds iff
$\\{\mathsf{Inv}^{pre}_{n}\\}$ $\;\mu(n)\;$ $\\{\mathsf{Inv}^{post}_{n}\\}$
holds. Composing these renamed Hoare triples at all the nodes in the collapsed
CFG of $\mathsf{P}^{r}_{N}$ proves the forward direction of the lemma. The
case in the reverse direction is similar.

We end this subsection with an illustration of the program transformation
achieved by applying the renaming strategy mentioned above. For convenience we
replicate our running example from Fig. 4 in Fig. 16(a).

######  Example 2.

Consider the program shown in Fig. 16(a). This program has multiple
sequentially composed loops that update a scalar S and an array A. The
transformed program after renaming the scalar and array variables using
function Rename is shown in Fig. 16(b), where we have used simple names for
the renamed versions of S and A for ease of readability. Notice that we rename
the array A in the second loop to A1, and rename the variable S in the third
loop to S1. The statement at line 8 in Fig. 16(b) is the glue code to copy
values from one version of the renamed scalar/array (variable S in our
program) to another version of the same scalar/array (version S1). We avoid
creating new versions of S and A for statements and loops that do not update
them. Values are read directly from the version of S and A that reaches the
access location. This helps in reducing the glue code required for renaming
quite significantly.

###  4.2 Peeling the Loops

Algorithm 1 PeelAllLoops$\left((\mathit{Locs},\mathit{CE},\mu):\mbox{ program
}\mathsf{P}_{N}\right)$

1:$\mathsf{P}^{p}_{N}:=(\mathit{Locs}^{p},\mathit{CE}^{p},\mu^{p})$, where
$\mathit{Locs}^{p}=\mathit{Locs}$, $\mathit{CE}^{p}=\mathit{CE}$,
$\mu^{p}=\mu$;  $\ignorespaces\triangleright$ $\mathsf{P}^{p}_{N}$ is a copy
of $\mathsf{P}_{N}$

2:$\mathsf{PeelNodes}$ := $\varnothing$;

3:for each loop $L\in\textsc{Loops}(\mathsf{P}^{p}_{N})$ do

4: Let $k_{L}({N})$ be the expression for iteration count of $L$ in
$\mathsf{P}^{p}_{N}$;

5: $\mathsf{PeelCount}:=\textsc{Simplify}(k_{L}({N})-k_{L}({N-1}))$;

6: if $\mathsf{PeelCount}$ is not a constant then

7: throw “Failed to peel non-constant number of iterations”;

8: end if

9:
$\langle\mathsf{P}^{p}_{N},\mathit{Locs}^{\prime}\rangle:=\textsc{PeelSingleLoop}(\mathsf{P}^{p}_{N},L,k_{L}({N-1}),\mathsf{PeelCount})$;
$\triangleright$ We assume availability of function PeelSingleLoop, for
example, from a compiler framework like LLVM.
$\triangleright$ It transforms loop $L$ so that last $\mathsf{PeelCount}$
iterations of $L$ are peeled.
$\triangleright$ Updated CFG and newly created CFG nodes for the peeled
iterations are returned.

10: $\mathsf{PeelNodes}$ := $\mathsf{PeelNodes}$ $\cup$
$\mathit{Locs}^{\prime}$;

11:end for

12:return $\langle\mathsf{P}^{p}_{N},\mathsf{PeelNodes}\rangle$;

Recall from Sect. 2 that our induction strategy requires us to use
$\mathsf{P}_{N-1}\mathchar 24635\relax\;\partial\mathsf{P}_{N}$ in place of
$\mathsf{P}_{N}$ when proving the Hoare triple
$\\{\varphi(N)\\}\;\mathsf{P}_{N}\;\\{\psi(N)\\}$. In general, the parameter
$N$ may determine the number of times each loop in $\mathsf{P}_{N}$ iterates
(see, for example, Fig. 16(b)). Therefore, the count of iterations of a loop
in $\mathsf{P}_{N-1}$ may differ from the corresponding count in
$\mathsf{P}_{N}$. Relating $\mathsf{P}_{N}$ and $\mathsf{P}_{N-1}$ requires
taking into account such differences of loop iterations. Towards this end, we
transform $\mathsf{P}_{N}$ by _peeling_ the last few iterations of each loop
as needed, so that corresponding loops in $\mathsf{P}_{N-1}$ and the
transformed $\mathsf{P}_{N}$ iterate the same number of times. This is done by
function PeelAllLoops shown in Algorithm 1. The algorithm first makes a copy,
viz. $\mathsf{P}^{p}_{N}$, of the non-collapsed input CFG $\mathsf{P}_{N}$.
Let $\textsc{Loops}(\mathsf{P}^{p}_{N})$ denote the set of loops of
$\mathsf{P}^{p}_{N}$, and let $k_{L}(N)$ and $k_{L}(N-1)$ denote the number of
times loop $L$ iterates in $\mathsf{P}^{p}_{N}$ and $\mathsf{P}_{N-1}$
respectively. The difference $k_{L}(N)-k_{L}(N-1)$, computed in line 5, gives
the extra iteration count of loop $L$ in $\mathsf{P}^{p}_{N}$. If this
difference is not a constant, we currently report a failure of our technique
(line 7). For example, consider a loop in $\mathsf{P}_{N}$ with the counter
$i$ initialized to $0$ and the loop termination condition “$i<N^{2}$”. The
corresponding loop in $\mathsf{P}_{N-1}$ has the same initialization but the
termination condition is “$i<(N-1)^{2}$”. Thus, $k_{L}(N)=N^{2}$ and
$k_{L}(N-1)=(N-1)^{2}$ and the difference of these iteration counts is
“$2\times N+1$”. Our technique is unable to handle such cases currently. Note
that such cases cannot arise if the upper bounds of all loops in
$\mathsf{P}_{N}$ are linear functions of $N$.

The routine PeelSingleLoop transforms loop $L$ of $\mathsf{P}^{p}_{N}$ as
follows: it replaces the termination condition $(\ell<k_{L}(N))$ of $L$ by
$(\ell<k_{L}(N-1))$. It also peels the last $(k_{L}(N)-k_{L}(N-1))$ iterations
of $L$ and adds control flow edges such that the peeled iterations are
executed immediately after the loop body is iterated $k_{L}(N-1)$ times.
Effectively, PeelSingleLoop peels the last $(k_{L}(N)-k_{L}(N-1))$ iterations
of loop $L$ in $\mathsf{P}^{p}_{N}$. The transformed CFG is returned as the
updated $\mathsf{P}^{p}_{N}$ in line 9. In addition, PeelSingleLoop also
returns the set $Locs^{\prime}$ of all CFG nodes newly added while peeling the
loop $L$. We accumulate these newly added nodes for loops in the set
$\mathsf{PeelNodes}$ in line 10. Henceforth, we call all nodes in
$\mathsf{PeelNodes}$ as _peeled nodes_ , all other nodes in the CFG as _non-
peeled nodes_ , and the CFG resulting from the invocation of PeelAllLoops as a
_peeled program_. This function PeelAllLoops returns the peeled program
$\mathsf{P}^{p}_{N}$ and the set of peeled nodes $\mathsf{PeelNodes}$ in line
12.

We now state several useful properties of peeled programs.

######  Lemma 3.

Let $n\in\mathit{Locs}^{p}$ be a node in the peel of loop $L$, and let $n_{h}$
be the loop-head of loop $L$. For every $n^{\prime}\in\mathit{Locs}^{p}$ that
is not in the peel, if there is a control flow path in $\mathsf{P}_{N}^{p}$
from $n^{\prime}$ to $n$, the path necessarily passes through $n_{h}$.

Proof: The proof follows from the observation that the peel of a loop $L$ must
necessarily execute after the loop $L$ has itself executed $k_{L}(N-1)$ times.
Hence, the sole predecessor of the first node in the peel must be the loop-
head node $n_{h}$. It follows that every control flow path from $n^{\prime}$
to $n$ where $n^{\prime}$ is not in the peel must pass through $n_{h}$.

Peeling of loops can destroy the no-overwriting property (as mentioned in
Lemma 1), since the same variable/array can get updated in a loop $L$ and also
in its peel. However, a weaker variant of the no-overwriting property
continues to hold, as described below.

######  Lemma 4.

Let $n$ be a node in the collapsed CFG of $\mathsf{P}_{N}$. In every execution
of the renamed and peeled program $\mathsf{P}^{p}_{N}$ in which control flows
through $n$, the following hold.

  1. 1.

If $n$ is not a collapsed node, the no-overwriting property as in Lemma 1
holds for all scalar variables/arrays $vA^{n}$.

  2. 2.

If $n$ is a node representing a collapsed loop $L$, the scalar variable/array
$vA^{n}$ is not updated at any subsequent node along the execution, except
possibly in the peel of $L$.

Proof: Follows from the same reasoning as used in the proof of Lemma 1.

We will henceforth refer to the property formalized in Lemma 4 as the _“no-
overwriting”_ property of the renamed and peeled program $\mathsf{P}_{N}^{p}$.

######  Lemma 5.

In the peeled program $\mathsf{P}_{N}^{p}$, each conditional branch node in a
peel of a loop has an immediate post-dominator in the same peel.

Proof: The syntactic restrictions on the input program, imposed by the grammar
shown in Fig. 13, do not admit _break, continue, goto, exit_ and _return_
statements. Since a loop body is also syntactically a complete program,
conditional branch nodes in the body of the loop, if any, always have an
immediate post-dominator node within the body of the same loop. The peel of a
loop is obtained by creating a copy of the loop body (using the function
PeelSingleLoop invoked on line 9 of routine PeelAllLoops in Algorithm 1).
Thus, the conditional branch nodes, if any, in the peel have an immediate
post-dominator node within the same peel.

Finally, the following lemma asserts that peeling does not change the Hoare
semantics of programs.

######  Lemma 6.

$\\{\varphi_{N}\\}\;\mathsf{P}_{N}\;\\{\psi_{N}\\}$ holds iff
$\\{\varphi_{N}\\}\;\mathsf{P}^{p}_{N}\;\\{\psi_{N}\\}$ holds.

Proof: Follows immediately from the observation that peeling each loop
preserves the semantics of the program.

    // assume(

    $\ignorespaces\forall$

    i

    $\ignorespaces\in$

    [0,N) A[i] = 1)

    1.  S = 0;
    2.  for(i=0; i<N-1; i++) {
    3.    S = S + A[i];
    4.  }
    5.  S = S + A[N-1];

    6.  for(i=0; i<N-1; i++) {
    7.    A1[i] = A[i] + S;
    8.  }
    9.  A1[N-1] = A[N-1] + S;

    10. S1 = S;
    11. for(i=0; i<N-1; i++) {
    12.   S1 = S1 + A1[i];
    13. }
    14. S1 = S1 + A1[N-1];

    // assert(S1 = N

    $\ignorespaces\times$

     (N+2))

Figure 17: Hoare triple containing a program with peeled loops

######  Example 3.

We execute function PeelAllLoops on the renamed version of our running
example, shown in Fig. 16(b). The resulting program is shown in Fig. 17. The
algorithm first computes the number of iterations to be peeled from a loop in
the program, given by $\mathsf{PeelCount}$. The upper bound expression of each
loop in the program is $N$. Hence, the number of iterations to be peeled is
$N-(N-1)$ $=$ $1$. In other words, only the last iteration is to be peeled
from each loop. The function appends the statements in the peeled iteration
after each loop and updates the upper bound expressions of each loop in the
resulting program, as shown in Fig. 17. The algorithm also returns the set of
peeled nodes, i.e. CFG nodes corresponding to the statements at lines $5$,
$9$, and $14$.

###  4.3 Tracking Data Dependencies

As discussed in Sect. 3.1, the flow of control in a program can be
conveniently represented by a CFG. A CFG, however, does not immediately
provide information about data dependencies between program statements. We use
a separate _data dependence graph_ , or DDG, to summarize data dependencies
between relevant statements in a program. Our primary purpose in constructing
such a DDG is to understand the dependencies of and from statements that are
executed in $\mathsf{P}_{N}$ but not in $\mathsf{P}_{N-1}$. These are related
to the peeled statements described in Sect. 4.2, and determine what must
eventually go into the difference program $\partial\mathsf{P}_{N}$, so that
$\mathsf{P}_{N}$ and $\mathsf{P}_{N-1}\mathchar
24635\relax\;\partial\mathsf{P}_{N}$ have the same effect on arrays and scalar
variables.

While there are several notions of data dependence used in the literature (see
ddg1 ; ddg2  for details), we use a fairly simple notion that best serves our
purpose. We say that there is a read-after-write data dependence from $n_{1}$
to $n_{2}$ if the statement at $n_{2}$ uses a data value that is potentially
generated by the statement at $n_{1}$. There is another kind of data
dependence that is peculiar to our approach that also needs special handling.
It may so happen that the glue code inserted between two nodes during renaming
has a loop, say $L_{1}$, that updates an array $A$ that is also subsequently
updated in another loop, say $L_{2}$ in non-glue code. If the peel of $L_{1}$
potentially updates an element of $A$ that is also updated in the non-peeled
part of $L_{2}$, then we have a write-after-write dependence between a
statement in the peel of a (glue) loop and subsequent statement in the non-
peeled part of another (non-glue) loop. We call such a dependence _non-peeled-
write-after-peeled-write_ dependence. Since we intend to move peels to the end
of the program to construct a difference program, this kind of dependence
poses a problem. Therefore, we explicitly identify such _non-peeled-write-
after-peeled-write_ dependencies below. Given the way our renaming operates,
it is easy to see that such a dependence can only arise for arrays and not for
scalars.

Note that in the above case when we have a glue loop followed by a non-glue
loop updating the same array, there may also be write-after-write dependencies
between the non-peeled (resp. peeled) part of the glue loop and the non-peeled
(resp. peeled) part of the non-glue loop. However, such dependencies are
preserved if we move peels of all loops to the end of the program to construct
a difference program. Therefore, such write-after-write dependencies do not
pose any problem for our purposes, and hence we do not keep track of them.
Furthermore, due to the way our renaming operates, it can be seen that write-
after-read dependencies can never arise between nodes of the collapsed CFG.

Formally, a DDG is a directed graph $G_{D}=(\mathit{Locs},\mathit{DE},\mu)$,
where $\mathit{Locs}$ and $\mu$ are exactly as in the definition of a CFG, and
$\mathit{DE}\subseteq\mathit{Locs}\times\mathit{Locs}$ represents _read-after-
write_ and _non-peeled-write-after-peeled-write_ dependencies between
statements in the program. Since our primary interest is in using data
dependencies to and from peeled statements for purposes of constructing
difference programs, and since loops have a very specific form in our programs
of interest (the grammar in Fig. 13 allows only loop counter to be updated in
a loop-head node), it suffices to restrict our attention to data dependencies
between distinct non-loop-head nodes in the peeled program.

Several existing compilers generate _program dependence graph_ , or PDG from a
given input program, and a DDG can be extracted from such a PDG pdg . Standard
dataflow analysis techniques are usually used to identify data dependencies
when constructing a PDG pdg ; pdg2 . One needs to be particularly careful when
identifying dependence between statements updating and accessing array
elements, since it is not only the same array name that must be involved in
the update and access, but also the same element in the array. The problem is
further compounded by the fact that array indices can be arbitrary expressions
in general. While vectorizing compilers can compute precise dependencies with
array index expressions using sophisticated dependence tests kennedy-book , it
is not always the case that these are implemented in non-vectorizing
compilers. A conservative generation of DDG may contain spurious data
dependence edges, which, in our context, can lead to the construction of a
difference program that is more complex than what is needed.

Let $n$ and $n^{\prime}$ be two CFG (hence also DDG) nodes. A conservative way
of generating DDG edges is to add the edge $(n,n^{\prime})$ to $\mathit{DE}$
if there is a control flow path
$\pi:(n=n_{1},n_{2},\ldots,n_{t-1},n_{t}=n^{\prime})$ in the CFG such that one
of the following conditions hold.

  1. D1:

$\big{(}\mathit{def}(n)\cap\mathit{uses}(n^{\prime})\big{)}\setminus\bigcup_{i=2}^{t-1}\mathit{def}(n_{i})$
contains a scalar variable $v$, or

  2. D2:

$\mathit{def}(n)$ contains an array $A$ such that

    1. (a)

Either of the following conditions hold:

      1. i.

$A\in\mathit{uses}(n^{\prime})$ and there is a common value that the index
expression $\mathit{defIndex}(A,n)$ and some index expression in
$\mathit{useIndexSet}(A,n^{\prime})$ can have.

      2. ii.

$n$ $\in$ $\mathsf{PeelNodes}$ and $n^{\prime}$ $\not\in$ $\mathsf{PeelNodes}$
and $A\in\mathit{def}(n^{\prime})$ and there is a common value that both the
index expressions $\mathit{defIndex}(A,n)$ and
$\mathit{defIndex}(A,n^{\prime})$ can have.

    2. (b)

Some elements of $A$ are potentially not updated along the path $\pi$.

######  Lemma 7.

For $n,n^{\prime}\in\mathit{Locs}$ such that $n^{\prime}$ is reachable from
$n$ in the CFG, if neither condition D1 nor condition D2 holds, then there is
no read-after-write or non-peeled-write-after-peeled-write dependence from $n$
to $n^{\prime}$.

Proof: We prove the lemma by contradiction. Suppose, if possible, neither D1
nor D2 holds and yet there is a _read-after-write_ dependence due to the data
value generated at $n$ being potentially used at $n^{\prime}$. There are two
cases to consider.

  * •

If the data value pertains to a scalar variable $v$ that is updated at $n$ and
accessed at $n^{\prime}$, then there must be a control flow path $\pi$ from
$n$ to $n^{\prime}$ along which $v$ is not updated at any intermediate node.
This implies condition D1 is satisfied – a contradiction!

  * •

Suppose the data value pertains to an element of array $A$ that is updated at
$n$ and accessed at $n^{\prime}$. Let the index expression of the array
element updated at $n$ be $e$, and let the corresponding index expression of
the same element accessed at $n^{\prime}$ be $e^{\prime}$. Clearly, both $e$
and $e^{\prime}$ can assume the same value (the concrete index of the element
of $A$ under consideration), and there is a control flow path $\pi$ from $n$
to $n^{\prime}$ along which this specific array element has not been updated.
This implies that both the conditions D2(a)(i) and D2(b) are satisfied, and
hence condition D2 is satisfied – a contradiction!

Suppose, if possible, neither D1 nor D2 holds and yet there is a _non-peeled-
write-after-peeled-write_ dependence from $n$ to $n^{\prime}$. Suppose the
data value pertains to an element of array $A$ that is updated at nodes $n$
and $n^{\prime}$ where $n$ $\in$ $\mathsf{PeelNodes}$ and $n^{\prime}$
$\not\in$ $\mathsf{PeelNodes}$. Let the index expression of the array element
updated at $n$ be $e$, and let the corresponding index expression of the same
element updated at $n^{\prime}$ be $e^{\prime}$. Clearly, both $e$ and
$e^{\prime}$ can assume the same value (the concrete index of the element of
$A$ under consideration), and there is a control flow path $\pi$ from $n$ to
$n^{\prime}$ along which this specific array element has not been updated.
This implies that both the conditions D2(a)(ii) and D2(b) are satisfied, and
hence, condition D2 is satisfied – a contradiction!

Condition D2(b) above is not easy to check in general. However, for programs
generated by the grammar in Fig. 13, it is possible to detect that condition
D2(b) is violated in special cases. As an example, if there is a loop that
updates all elements of array $A$ in every control flow path from $n$ to
$n^{\prime}$, then indeed condition D2(b) is violated. For purposes of this
paper, we use this special case as a sufficient condition to detect violation
of condition D2(b), and conservatively assume that the condition is
potentially satisfied in all other cases. Needless to say, a more precise
analysis can be done with additional computational effort to reduce the degree
of conservativeness in the above check for condition D2(b). We defer such an
improved analysis to future work. We now look at how condition D2(a) is
checked. Recall from Sect. 3 that the array indices in our programs can only
be expressions in terms of constants, scalar variables, the loop counter
variables and the parameter $N$. Furthermore, our programs do not have nested
loops. Therefore, at most one loop counter variable can appear in an array
index expression. Specifically, if $e$ is the index expression
$\mathit{defIndex}(A,n)$, and if node $n$ is part of a loop $L$ with loop
counter $\ell$, then $e$ depends in general on $\ell$, $N$ and a set of scalar
constants. Otherwise, i.e. if node $n$ is not part of a loop, $e$ depends on
$N$ and a set of scalar constants. A similar reasoning applies for array index
expression(s) in $\mathit{useIndexSet}(A,n^{\prime})$ as well. Condition D2(a)
is satisfied if the constraint $(e=e^{\prime})$ has a model, i.e. is
satisfiable, for some index expression
$e^{\prime}\in\mathit{useIndexSet}(A,n^{\prime})$, subject to the following
conditions:

  * •

Loop counters $\ell$ and $\ell^{\prime}$ must have values within their
respective loop bounds.

  * •

If both $n$ and $n^{\prime}$ are part of the same loop, then
$\ell\leq\ell^{\prime}$ (update at $n$ cannot happen in an iteration after
access at $n^{\prime}$).

  * •

Every scalar variable $v$ that appears in both $e$ and $e^{\prime}$ and is
updated along some control flow path from $n$ to $n^{\prime}$ is renamed in
$e^{\prime}$ to a fresh variable (since the values of $v$ in $e$ and
$e^{\prime}$ may be different).

Algorithm 2 ComputeDDG($(\mathit{Locs},\mathit{CE},\mu)$: program
$\mathsf{P}_{N}$, $\mathsf{PeelNodes}$: peeled statements)

1:$\mathit{DE}$ := $\emptyset$;

2:for each $n,n^{\prime}\in\mathit{Locs}\setminus\mathit{LoopHeads}$ s.t.
$n\neq n^{\prime}$ and
$n\stackrel{{\scriptstyle\mathit{Locs}}}{{\rightsquigarrow}}n^{\prime}$ do
$\ignorespaces\triangleright$ $n^{\prime}$ reachable from $n$ in CFG

3: $\mathit{D1Sat}$ := $\mathsf{False}$; $\mathit{D2Sat}$ := $\mathsf{False}$;
$\ignorespaces\triangleright$ Initializing flags to indicate if condition
D1/D2 holds

4: $S$ := $\mathit{def}(n)\cap\mathit{uses}(n^{\prime})$;
$\ignorespaces\triangleright$ Set of scalar variables/arrays that potentially
introduce data dependence between $n$ and $n^{\prime}$

5: if $n\in\mathsf{PeelNodes}\wedge n^{\prime}\not\in\mathsf{PeelNodes}$ then
$S:=S\cup\big{(}\mathit{def}(n)\cap\mathit{def}(n^{\prime})\big{)}$;

6: end if $\ignorespaces\triangleright$ For non-peeled-write-after-peeled-
write dependence
$\triangleright$ Check for condition D1

7: for each scalar variable $v\in S$ do

8: $\mathit{NDefV}$ := $\\{n^{\prime\prime}\mid n^{\prime\prime}\neq
n,n^{\prime\prime}\neq n^{\prime},v\not\in\mathit{def}(n^{\prime\prime})\\}$;
$\ignorespaces\triangleright$ Nodes other than $n$, $n^{\prime}$ that don’t
define $v$

9: if $n\stackrel{{\scriptstyle\mathit{NDefV}}}{{\rightsquigarrow}}n^{\prime}$
then $\ignorespaces\triangleright$ Potential data dependence $(n,n^{\prime})$
due to variable $v$

10: $\mathit{D1Sat}$ := $\mathsf{True}$; break;

11: end if

12: end for
$\triangleright$ Check for condition D2 if D1 isn’t already satisfied

13: if (not $\mathit{D1Sat}$) then

14: for each array $A\in S$ do

15: $\phi_{n}$ := $\mathsf{True}$; $\phi_{n^{\prime}}$ := $\mathsf{True}$;
$\ignorespaces\triangleright$ Initializing loop bound constraints for $n$ and
$n^{\prime}$

16: if $n$ is part of loop $L$ with loop counter $\ell$ then $\phi_{n}$ :=
$(0\leq\ell<k_{L})$;

17: end if

18: if $n^{\prime}$ is part of a loop $L^{\prime}$ with loop counter
$\ell^{\prime}$ then $\phi_{n^{\prime}}$ :=
$(0\leq\ell^{\prime}<k_{L^{\prime}})$;

19: if $L^{\prime}$ same as $L$ then $\phi_{n^{\prime}}$ :=
$\phi_{n^{\prime}}\wedge(\ell\leq\ell^{\prime})$;
$\ignorespaces\triangleright$ $n$ and $n^{\prime}$ in the same loop

20: end if

21: end if

22: $e$ := $\mathit{defIndex}(A,n)$;  $\ignorespaces\triangleright$ Index
expression used to update element of $A$ at $n$

23: $U:=\mathit{useIndexSet}(A,n^{\prime})$;

24: if $n\in\mathsf{PeelNodes}\wedge n^{\prime}\not\in\mathsf{PeelNodes}$ then
$U:=U\cup\\{\mathit{defIndex}(A,n^{\prime})\\}$;

25: end if

26: for each scalar variable $v$ that appears in both $e$ and some
$e^{\prime}\in U$ do

27: $\mathit{DefV}$ := $\\{n^{\prime\prime}\mid n^{\prime\prime}\neq
n,n^{\prime\prime}\neq n^{\prime},v\in\mathit{def}(n^{\prime\prime})\\}$;
$\ignorespaces\triangleright$ Nodes other than $n$, $n^{\prime}$ that define
$v$

28: if $\exists n^{\prime\prime}\in\mathit{DefV}\wedge n\rightsquigarrow
n^{\prime\prime}\wedge n^{\prime\prime}\rightsquigarrow n^{\prime}$ then
$\ignorespaces\triangleright$ $v$ modified along a path from $n$ to
$n^{\prime}$

29: $e^{\prime}$ := $e^{\prime}[v/v_{\mathit{fresh}}]$;
$\ignorespaces\triangleright$ Rename variable $v$ in $e^{\prime}$ with fresh
variable $v_{\mathit{fresh}}$

30: end if

31: end for

32: if not
IsSat$\big{(}\phi_{n}\wedge\phi_{n^{\prime}}\wedge\bigvee_{e^{\prime}\in
U}(e=e^{\prime})\big{)}$ then continue;  $\ignorespaces\triangleright$ D2(a)
violated for array $A$

33: end if

34: if $\exists$ loop $L^{\prime\prime}$ with loop-head $n^{\prime\prime}$
s.t. ($n,n^{\prime}$ not in $L^{\prime\prime}$) $~{}\wedge$
($n\stackrel{{\scriptstyle\mathit{Locs}\setminus\\{n^{\prime\prime}\\}}}{{\not\rightsquigarrow}}n^{\prime}$)
then

35: if $L^{\prime\prime}$ necessarily updates all elements of $A$ then

36: continue;  $\ignorespaces\triangleright$ Condition D2(b) violated for
array $A$

37: end if

38: end if

39: $\mathit{D2Sat}$ := $\mathsf{True}$; break;  $\ignorespaces\triangleright$
Potential data dependence $(n,n^{\prime})$ due to array $A$

40: end for

41: end if

42: if $\big{(}\mathit{D1Sat}\vee\mathit{D2Sat}\big{)}$ then $\mathit{DE}$ :=
$\mathit{DE}\cup\\{(n,n^{\prime})\\}$;

43: end if

44:end for

45:return $(\mathit{Locs},DE,\mu)$;

Function ComputeDDG, shown in Algorithm 2, constructs the DDG for an input
program $\mathsf{P}_{N}$ represented using its CFG
$(\mathit{Locs},\mathit{CE},\mu)$. We use the notation
$n\stackrel{{\scriptstyle X}}{{\rightsquigarrow}}n^{\prime}$ to denote that
there is a control flow path from $n$ to $n^{\prime}$ in the CFG that passes
through intermediate nodes in $X\subseteq\mathit{Locs}$. ComputeDDG proceeds
by initializing the set of data dependence edges $DE$ to $\emptyset$, and by
checking for every pair of distinct non-loop-head nodes $(n,n^{\prime})$ such
that $n\stackrel{{\scriptstyle\mathit{Locs}}}{{\rightsquigarrow}}n^{\prime}$,
whether condition D1 or D2 referred to above is satisfied. If either one of
the conditions is satisfied, it adds $(n,n^{\prime})$ to $DE$ (lines 42–43).

The set $S$ of scalar variables and arrays that potentially introduce data
dependence from $n$ to $n^{\prime}$ is initialized to
$\mathit{def}(n)\cap\mathit{uses}(n^{\prime})$ in line 4. If $n$ is a peeled
node and $n^{\prime}$ is a non-peeled node, then we append $S$ with
$\mathit{def}(n)\cap\mathit{def}(n^{\prime})$ in line 5. Subsequently, the
check for D1 is done in the loop in lines 7–12. In each iteration of this
loop, we choose a scalar variable $v$ from the set $S$ and check whether there
exists a control flow path from $n$ to $n^{\prime}$ such that no intermediate
node along the path updates $v$. The latter check is implemented by first
collecting all nodes $n^{\prime\prime}$ (other than $n$ and $n^{\prime}$) that
doesn’t update $v$ in the set $\mathit{NDefV}$ (line 8). If there is a control
flow path from $n$ to $n^{\prime}$ that passes through intermediate nodes in
$\mathit{NDefV}$, the value of $v$ updated at $n$ can reach the use of $v$ at
$n^{\prime}$. In this case, there is a potential data dependence of
$n^{\prime}$ on $n$ through $v$ and condition D1 is satisfied. We therefore
set $\mathit{D1Sat}$ to $\mathsf{True}$ and abort the search over additional
scalar variables $v$ in $S$ (line 10). Otherwise, there is no dependence of
$n^{\prime}$ on $n$ through $v$.

If the flag $\mathit{D1Sat}$ is not set to $\mathsf{True}$ even after
iterating over all scalar variables in $S$, we turn to checking if condition
D2 can be satisfied. Towards this end, we iterate over all array names $A$
remaining in $S$, and formulate a constraint to check if condition D2(a) is
satisfied (lines 15–33). This condition effectively checks if it is possible
for the index expression $\mathit{defIndex}(A,n)$ to have the same value as
any index expression $e^{\prime}\in\mathit{useIndexSet}(A,n^{\prime})$ or if
it is possible for the index expression $\mathit{defIndex}(A,n)$ to have the
same value as the index expression $\mathit{defIndex}(A,n^{\prime})$ when $n$
is a peeled node and $n^{\prime}$ is a non-peeled node. If not, the
update/read of array $A$ at $n$ and $n^{\prime}$, cannot be for the same
element, and hence, there is no data dependence $(n,n^{\prime})$ through $A$.
As discussed above, to check if condition D2(a) is satisfied, we must conjoin
loop bound constraints for loop counter variables in case $n$ or $n^{\prime}$
is present in a loop (lines 15–21), and rename every scalar variable $v$ in
expressions $e^{\prime}\in\mathit{useIndexSet}(A,n^{\prime})$ that also
appears in the index expression $\mathit{defIndex}(A,n)$, if $v$ is
potentially re-defined in a control flow path from $n$ to $n^{\prime}$. The
renaming of scalar variables, if needed, is done in lines 22–31. The call to
IsSat in line 32 is an invocation of an SMT solver that tells us whether the
constraint fed to it as argument is satisfiable, i.e. has a model. If not,
condition D2(a), and hence D2, is violated. Otherwise, we check in lines 34
and 35 if there exists a loop $L^{\prime\prime}$ not containing $n$ and
$n^{\prime}$ that necessarily executes as control flows from $n$ to
$n^{\prime}$
($n\stackrel{{\scriptstyle\mathit{Locs}\setminus\\{n^{\prime\prime}\\}}}{{\not\rightsquigarrow}}n^{\prime}$
checks this), and in which all elements of the array $A$ are updated. Recall
from the grammar in Fig. 13 that all loops in our programs are for loops with
a loop counter that increments by $1$ in each operation, and cannot be updated
in the body of the loop. For such programs, it is sometimes easy to identify
if a loop $L^{\prime\prime}$ is indeed updating all elements of an array $A$.
If we cannot determine whether $L^{\prime\prime}$ necessarily updates all
elements of $A$, we conservatively assume that it does not and the check in
line 35 fails. If both the checks in lines 34 and 35 succeed, we conclude that
condition D2(b), and hence D2, has been violated. In all other cases, we
conservatively assume that D2 is satisfied, and set $\mathit{D2Sat}$ to
$\mathsf{True}$ in line 39. In such cases, we also abort the search over
additional array variables $A$ in $S$.

######  Lemma 8.

Given a program represented as $(\mathit{Locs},CE,\mu)$, let
$(\mathit{Locs},DE,\mu)$ be the DDG computed by ComputeDDG. For every pair of
distinct non-loop-head nodes $n,n^{\prime}\in\mathit{Locs}$, if
$(n,n^{\prime})\not\in DE$, there is no read-after-write or non-peeled-write-
after-peeled-write data dependence from $n$ to $n^{\prime}$.

Proof: Since function ComputeDDG implements the checks for conditions D1,
D2(a) and D2(b) in a straightforward manner, the proof follows from Lemma 7.

We conclude this subsection with an illustration of DDG edges computed by
ComputeDDG for our running example.

Start1234567891011121314End$~{}~{}~{}\mathbf{tt}$$\mathbf{ff}$$~{}~{}~{}\mathbf{tt}$$\mathbf{ff}$$~{}~{}~{}\mathbf{tt}$$\mathbf{ff}$SSSSSSA1A1S1S1S1

Figure 18: CFG (solid edges) and DDG (dashed edges) of peeled program in Fig.
17

######  Example 4.

Our running example with peeled loops is shown in Fig. 17. The CFG for this
program is shown using solid edges in Fig. 18. For convenience of exposition,
we have named nodes such that node $n_{i}$ in the CFG of this program
corresponds to the statement at line $i$ of the peeled program, with two
special nodes $n_{start}$ and $n_{end}$, as usual. If we execute function
ComputeDDG on this CFG, we obtain the data dependence edges shown using dashed
edges in Fig. 18. For ease of understanding, each DDG edge $(n,n^{\prime})$ is
also labeled by a scalar variable/array that is responsible for the data
dependence of $n^{\prime}$ on $n$. Thus, DDG edges
$(n_{1},n_{3}),(n_{1},n_{5}),(n_{3},n_{5}),(n_{5},n_{7}),(n_{5},n_{9})$ and
$(n_{5},n_{10})$ represent data dependence through the scalar variable S and
edges $(n_{10},n_{12}),(n_{10},n_{14}),(n_{12},n_{14})$ represent data
dependence through the scalar variable S1. In all these cases, condition $D1$
holds. Similarly, DDG edges $(n_{7},n_{12}),(n_{9},n_{14})$ represent data
dependence through the array A1, since conditions D2(a) and D2(b) hold in
these cases. Note that edge $(n_{7},n_{14})$ (resp. $(n_{9},n_{12})$) is not
added although ${\mathtt{A}1}\in\mathit{def}(n_{7})\cap\mathit{uses}(n_{14})$
(resp. $\in\mathit{def}(n_{9})\cap\mathit{uses}(n_{12})$) because condition
D2(a) fails in this case. To see why D2(a) fails, notice that
$\phi_{7}:=0\leq\mathtt{i}<\mathtt{N}-1$ and $\phi_{14}:=\mathsf{True}$. The
expressions used to define and access array $\mathtt{A}$ are
$\mathit{defIndex}(\mathtt{A},7):=\mathtt{i}$ and
$\mathit{useIndexSet}(\mathtt{A},14):=\\{\mathtt{N}-1\\}$. The constraint
$0\leq\mathtt{i}<\mathtt{N}-1\wedge\mathtt{i}=\mathtt{N}-1$, computed in line
32 of Algorithm 2, is unsatisfiable. This violates D2(a)(i). Note that, in
this example there are no non-peeled-write-after-peeled-write dependencies.

###  4.4 Identifying “Affected” Variables

Recall that every loop $L$ originally present in $\mathsf{P}_{N}$ iterates
$k_{L}(N-1)$ times in $\mathsf{P}_{N-1}$ and $k_{L}(N)$ times in
$\mathsf{P}_{N}$. The iterations missed by $\mathsf{P}_{N-1}$ are represented
by the peeled statements computed by function PeelAllLoops. It is natural to
expect the difference program $\partial\mathsf{P}_{N}$ to contain the peeled
statements, perhaps with some adaptations, if $\mathsf{P}_{N-1}\mathchar
24635\relax\;\partial\mathsf{P}_{N}$ is to have the same effect as
$\mathsf{P}_{N}$ on all relevant scalar variables and arrays. However,
statements that are present in both $\mathsf{P}_{N}$ and $\mathsf{P}_{N-1}$
may also differ in their semantics, and therefore require “rectification” in
$\partial\mathsf{P}_{N}$. For example, statements like x = N; and if (x > N)
in $\mathsf{P}_{N}$ become x = N-1; and if (x > N-1) respectively, in
$\mathsf{P}_{N-1}$. Clearly, the corresponding statements in $\mathsf{P}_{N}$
and $\mathsf{P}_{N-1}$ in the above examples have different semantics. We say
that such statements, though present in both $\mathsf{P}_{N-1}$ and
$\mathsf{P}_{N}$, are “affected” by the parameter $N$, and potentially need to
be “rectified” in $\partial\mathsf{P}_{N}$. Our goal in this subsection is to
identify all relevant scalar variables/arrays that are potentially affected in
this sense, i.e. they are updated by versions of the same statement in
$\mathsf{P}_{N}$ and $\mathsf{P}_{N-1}$ but can potentially result in
different values being assigned due to the change in the parameter $N$. We use
the data dependence information computed in the previous subsection to
identify such variables and arrays, which we also call _affected
variables/arrays_. Once these variables/arrays are identified, we can proceed
to generate the difference program $\partial\mathsf{P}_{N}$ for effecting any
rectification that may be needed.

Algorithm 3 ComputeAffected($(\mathit{Locs}^{p},CE^{p},\mu^{p})$: peeled
program $\mathsf{P}_{N}^{p}$, $\mathsf{PeelNodes}$: peeled statements)

1:$(\mathit{Locs}^{p},DE^{p},\mu^{p})$ :=
ComputeDDG($(\mathit{Locs}^{p},CE^{p},\mu^{p})$, $\mathsf{PeelNodes}$);

2:$\mathsf{AffectedVars}$ := $\emptyset$;  $\ignorespaces\triangleright$
Initialize $\mathsf{AffectedVars}$
$\triangleright$ Initialize $\mathsf{WorkList}$ with non-peeled nodes of CFG
that either use $N$ directly or have data dependence on peeled nodes

3:$\mathsf{WorkList}$ := $\\{n\mid
n\in\mathit{Locs}^{p}\setminus\mathsf{PeelNodes},N\in\mathit{uses}(n)$ or
$\exists n^{\prime}.\;n^{\prime}\in\mathsf{PeelNodes}\wedge(n^{\prime},n)\in
DE^{p}\\}$;

4:$\mathsf{ProcessedNodes}$ := $\emptyset$;

5:while $\mathsf{WorkList}$ is not empty do

6: Remove a node $n$ from the head of $\mathsf{WorkList}$;

7: $\mathsf{ProcessedNodes}$ := $\mathsf{ProcessedNodes}\cup\\{n\\}$;

8: if $\mu(n)$ is an assignment statement then

9: $\mathsf{AffectedVars}$ := $\mathsf{AffectedVars}\cup\mathit{def}(n)$;
$\ignorespaces\triangleright$ $\mathit{def}(n)$ potentially affected by $N$

10: for all nodes $n^{\prime}$ s.t.
$n^{\prime}\in\mathit{Locs}^{p}\setminus\mathsf{PeelNodes}$,
$n^{\prime}\not\in\mathsf{ProcessedNodes}$ and $(n,n^{\prime})\in DE^{p}$ do

11: $\mathsf{WorkList}$ := AppendToList($\mathsf{WorkList}$, $n^{\prime}$);

12: end for

13: else if $\mu(n)$ is a branch condition then

14: for all nodes $n^{\prime}$ s.t.
$n^{\prime}\in\mathit{Locs}^{p}\setminus\mathsf{PeelNodes}$,
$n^{\prime}\not\in\mathsf{ProcessedNodes}$ and
$n\stackrel{{\scriptstyle\mathit{Locs}^{p}}}{{\rightsquigarrow}}n^{\prime}$ do

15: $\mathsf{WorkList}$ := AppendToList($\mathsf{WorkList}$, $n^{\prime}$);

16: end for

17: else continue;  $\ignorespaces\triangleright$ $n$ is a loop-head; don’t do
anything for loop-heads

18: end if

19:end while $\ignorespaces\triangleright$ end of while loop processing
elements of $\mathsf{WorkList}$

20:return $\mathsf{AffectedVars}$;

Function ComputeAffected, shown in Algorithm 3, computes the set of affected
scalar variables/arrays of a peeled program $\mathsf{P}_{N}^{p}$, represented
by its CFG $(\mathit{Locs}^{p},CE^{p},\mu^{p})$. Besides the CFG, the function
also takes as input the set of CFG nodes corresponding to peeled statements,
denoted $\mathsf{PeelNodes}$. Recall that such a set is obtained when function
PeelAllLoops is invoked. ComputeAffected starts by constructing the data
dependence graph using function ComputeDDG (line 1). The set of data
dependence edges thus obtained is represented by $DE^{p}$. We use
$\mathsf{AffectedVars}$ to denote the set of affected variables and arrays of
$\mathsf{P}_{N}$, and initialize it to the empty set in line 2. We also
maintain a list of nodes $n$ in $\mathsf{WorkList}$ such that the semantics of
the program statement in $\mu(n)$ is potentially affected (directly or
indirectly) by $N$. This worklist is initialized in line 3 with all non-peeled
nodes $n$ that either (i) have $N$ in $\mathit{uses}(n)$, or (ii) are
potentially data dependent on a peeled node, i.e. $\exists
n^{\prime}.\;n^{\prime}\in\mathsf{PeelNodes}$ and $(n^{\prime},n)\in DE^{p}$.
The exclusion of peeled nodes from the worklist is justified by the
observation that these statements are present in $\mathsf{P}^{p}_{N}$ but not
in $\mathsf{P}_{N-1}$. Therefore, these must necessarily appear (possibly with
modifications) in $\partial\mathsf{P}_{N}$, and no additional analysis is
needed to identify these statements or variables/arrays updated by them. We
also keep track of all non-peeled nodes that have been processed so far in the
set $\mathsf{ProcessedNodes}$, initialized in line 4.

The loop in lines 5–19 iterates over the worklist, processing one node at a
time to identify affected scalar variables and arrays. We remove the node $n$
at the head of the worklist and add it to $\mathsf{ProcessedNodes}$ in lines
6–7. If $\mu^{p}(n)$ is an assignment statement, we conservatively consider
the scalar variable or array updated at $n$ to be potentially affected (marked
in line 9). We also add all as-yet unprocessed nodes $n^{\prime}$ that have a
data dependence on $n$ to the worklist in line 11. This accounts for nodes
that are potentially affected because they use a value that is generated at
node $n$. If node $n$ corresponds to a conditional branch statement, we
conservatively consider all non-peeled nodes $n^{\prime}$ that are reachable
from $n$ in the CFG of $\mathsf{P}_{N}^{p}$ as potentially affected by $N$. If
such a node $n^{\prime}$ hasn’t been processed yet, we add it to the worklist
in line 15. Finally, if $n$ corresponds to a loop-head, we skip the
identification of affected variables from $n$ (line 17). This is justified
since the special form of loops allowed by the grammar in Fig. 13 permits only
loop counter variables to be updated in a loop-head, and loop counter
variables are not relevant for the post-conditions we wish to prove. The
overall set of affected scalar variables/arrays is iteratively computed until
there are no nodes left in the worklist to process. Since the CFG of
$\mathsf{P}_{N}^{p}$ has only a finite number of nodes, and since no node is
processed more than once (thanks to the book-keeping done using the set
$\mathsf{ProcessedNodes}$), the loop in lines 5–19 is guaranteed to terminate.

######  Lemma 9.

Let $\mathsf{P}_{N}^{p}$ be a peeled program fed as input to the function
ComputeAffected. Let $n$ be a node in $\mathsf{P}_{N}^{p}$ such that some
scalar variable/array in $\mathit{uses}(n)$ is transitively data/control
dependent on $N$ or on a peeled node in $\mathsf{P}_{N}^{p}$. Then $n$ is
added to $\mathsf{WorkList}$ during the execution of function ComputeAffected.

Proof: A transitive data/control dependence as referred to in the lemma can be
represented by a sequence of nodes $n_{i_{1}},n_{i_{2}},\ldots,n_{i_{k}}(=n)$,
where either (i) $k=1$ and $N\in\mathit{uses}(n)$ or (ii) $k>1$ and
$\mathit{uses}(n_{i_{j}})$ is data/control dependent on $n_{i_{j-1}}$, for
$2\leq j\leq k$. By Lemma 8, in case (ii), there is an edge from $n_{i_{j}-1}$
to $n_{i_{j}}$, for $2\leq j\leq k$, in the data dependence graph computed at
line 1 of function ComputeAffected. We now prove the claim by induction on
$k$.

We consider two base cases of the induction. If $k=1$, we know that
$N\in\mathit{uses}(n)$. Hence, $n$ is added to $\mathsf{WorkList}$ in line 3
of the function ComputeAffected. If $k=2$, either $n_{i_{1}}$ is a peeled node
or $N\in\mathit{uses}(n_{i_{1}})$. In the former case, $n=n_{i_{2}}$ is added
to $\mathsf{WorkList}$ in line 3 of ComputeAffected. Otherwise, $n_{i_{1}}$ is
added to $\mathsf{WorkList}$ in line 3 and must be removed from
$\mathsf{WorkList}$ in a later iteration before function ComputeAffected
terminates. In the iteration in which $n_{i_{1}}$ is removed from
$\mathsf{WorkList}$, the node $n=n_{i_{2}}$ is added to $\mathsf{WorkList}$
either due to data dependence (line 11 of ComputeAffected) or control
dependence (line 15 of ComputeAffected) of $\mathit{uses}(n)$ on $n_{i_{1}}$.

We next hypothesize that, for every transitive data/control dependence on $N$
or on a peeled node, represented by the sequence of nodes
$(n_{i_{1}},n_{i_{2}},\ldots,n_{i_{j}})$, where $2\leq j\leq k-1$, the node
$n_{i_{j}}$ is added to $\mathsf{WorkList}$ during the execution of
ComputedAffected.

For the inductive step, consider a transitive data/control dependence on $N$
or on a peeled node, represented by the sequence of nodes
$(n_{i_{1}},n_{i_{2}},\ldots,n_{i_{k}})$, where $n_{i_{k}}=n$. This implies
that $\mathit{uses}(n_{i_{k-1}})$ is also data/control dependence on $N$ or on
a peeled node. Now by the inductive hypothesis, $n_{i_{k-1}}$ must be added to
$\mathsf{WorkList}$ in some iteration of the loop in lines 5 – 19 of
ComputedAffected. In the iteration in which $n_{i_{k-1}}$ is removed from
$\mathsf{WorkList}$, the node $n=n_{i_{k}}$ is added to $\mathsf{WorkList}$
either due to data dependence (line 11 of ComputeAffected) or control
dependence (line 15 of ComputeAffected) of $\mathit{uses}(n_{i_{k}})$ on
$n_{i_{k-1}}$.

In order to study additional properties of function ComputeAffected, we need
to introduce some additional notation. Given a peeled program
$\mathsf{P}_{N}^{p}$ generated by PeelAllLoops, let $\mathsf{P}_{{N}}^{\star}$
denote the program obtained by removing the peels of all loops from
$\mathsf{P}_{N}^{p}$. Clearly, $\mathsf{P}_{{N}}^{\star}$ is identical to the
un-peeled program $\mathsf{P}_{N}$ (fed as input to PeelAllLoops), but with
all instances of $N$ in upper bound expressions of loops replaced by $N-1$.
The program $\mathsf{P}_{{N}}^{\star}$ is also closely related, but not
identical, to $\mathsf{P}_{N-1}$. Indeed, $\mathsf{P}_{N-1}$ has all
occurrences of $N$ (not just those appearing in upper bound expressions of
loops) in $\mathsf{P}_{N}$ replaced by $N-1$, whereas only upper bound
expressions of loops are modified to obtain $\mathsf{P}_{{N}}^{\star}$. As an
example, the loop in Fig. 19(a) in the program $\mathsf{P}_{N}$ transforms to
the loop in Fig. 19(b) in the program $\mathsf{P}_{{N}}^{\star}$ and to the
loop in Fig. 19(c) in the program $\mathsf{P}_{N-1}$.

      for (l=0; l<N; l=l+1) {
        if (x < N) { x = x + N; }
      }

(a)

      for (l=0; l<N-1; l=l+1) {
        if (x < N) { x = x + N; }
      }

(b)

      for (l=0; l<N-1; l=l+1) {
        if (x < N-1) { x = x + N-1; }
      }

(c)

Figure 19: A loop in (a) $\mathsf{P}_{N}$, (b) $\mathsf{P}_{{N}}^{\star}$, and
(c) $\mathsf{P}_{N-1}$

Since there is a bijection between the nodes in the CFGs of $\mathsf{P}_{N}$
and $\mathsf{P}_{N-1}$, and similarly between the nodes in the CFGs of
$\mathsf{P}_{N}$ and $\mathsf{P}_{{N}}^{\star}$, there exists a bijection
between the nodes in the CFGs of $\mathsf{P}_{N-1}$ and
$\mathsf{P}_{{N}}^{\star}$ as well. It is also easy to see that since programs
generated by the grammar in Fig. 13 only allow loop bound expressions that
depend on constants and $N$, if $L$ and $L^{\prime}$ are corresponding loops
in $\mathsf{P}_{N-1}$ and $\mathsf{P}_{{N}}^{\star}$ respectively, then both
$L$ and $L^{\prime}$ iterate exactly the same number, i.e. $k_{L}(N-1)$,
times.

Let $n_{0},n_{1},n_{2},\ldots,n_{t}$ denote nodes in the CFG of
$\mathsf{P}_{N-1}$, and let
$n_{0}^{\prime},n_{1}^{\prime},n_{2}^{\prime},\ldots,n_{t}^{\prime}$ denote
the corresponding nodes (per the bijection) in the CFG of
$\mathsf{P}_{{N}}^{\star}$. For notational convenience, we let $n_{0}$ and
$n_{t}$ be the start and end nodes respectively of the CFG of
$\mathsf{P}_{N-1}$, and similarly for $n_{0}^{\prime}$ and $n_{t}^{\prime}$.
Let $\sigma$ denote an arbitrary initial state, i.e. valuation of all scalar
variables and arrays, from which we wish to start executing $\mathsf{P}_{N-1}$
and $\mathsf{P}_{{N}}^{\star}$. Since programs generated by the grammar in
Fig. 13 are deterministic, there is exactly one control flow path, say $\pi$,
in the CFG of $\mathsf{P}_{N-1}$ that corresponds to the execution of
$\mathsf{P}_{N-1}$ starting from $\sigma$. A similar argument holds for
$\mathsf{P}_{{N}}^{\star}$, and let $\pi^{\prime}$ be the corresponding path
in its CFG. In the following discussion, we use $n_{i_{j}}$ to denote the
$j^{th}$ node starting from $n_{i_{0}}$ in $\pi$, where $i_{0}=0$ and $0\leq
j<|\pi|$. The interpretation of $n_{i_{j}}^{\prime}$ in the context of
$\pi^{\prime}$ is analogous.

######  Lemma 10.

Let $\pi$ (resp. $\pi^{\prime}$) be the path in the CFG of $\mathsf{P}_{N-1}$
(resp. $\mathsf{P}_{{N}}^{\star}$) that corresponds to the execution of
$\mathsf{P}_{N-1}$ (resp. $\mathsf{P}_{{N}}^{\star}$) starting from the state
$\sigma$. Let $\widehat{\pi}:(n_{i_{0}},n_{i_{1}},\ldots,n_{i_{j}})$ be a
prefix of the path $\pi$. Suppose, upon termination of ComputeAffected, no
conditional branch node in $\widehat{\pi}$ is present in
$\mathsf{ProcessedNodes}$. Then,
$(n_{i_{0}}^{\prime},n_{i_{1}}^{\prime},\ldots,n_{i_{j}}^{\prime})$ must be a
prefix of $\pi^{\prime}$.

Proof: Recall that the CFGs of $\mathsf{P}_{N-1}$ and
$\mathsf{P}_{{N}}^{\star}$ are identical (including all loop bounds) except
possibly for the usage of $N$ or an expression involving $N$ in some
conditional branches and/or assignment statements. Note that by definition,
none of these CFGs contain any peeled nodes. Since $\pi$ and $\pi^{\prime}$
start at corresponding nodes $n_{0}$ and $n_{0}^{\prime}$ in the respective
CFGs, every subsequent node $n_{i_{j}}$ in $\pi$ must be matched by the
corresponding node $n_{i_{j}}^{\prime}$ in $\pi^{\prime}$, until a branch node
is encountered along one of the paths and the branch condition potentially
depends on $N$. To prove the lemma, it therefore suffices to show that no
conditional branch node $n_{i_{k}}$ in $\widehat{\pi}$ has any transitive
data/control dependence on $N$.

Let $n_{i_{k}}$ be a conditional branch node in $\widehat{\pi}$. By Lemma 9,
if any scalar variable/array in $\mathit{uses}(n_{i_{k}})$ is transitively
data/control dependent on $N$, then $n_{i_{k}}$ must be added to
$\mathsf{WorkList}$ at some point during the execution of function
ComputeAffected. Consequently, $n_{i_{k}}$ must also be removed from
$\mathsf{WorkList}$ (line 6) and added to $\mathsf{ProcessedNodes}$ (line 7)
before ComputeAffected terminates. However, this violates the premise of the
claim, i.e. $n_{i_{k}}$ is not present in $\mathsf{ProcessedNodes}$ on
termination of ComputeAffected. Therefore, no scalar variable/array in
$\mathit{uses}(n_{i_{k}})$ can be transitively data/control dependent on $N$.
This completes the proof of the lemma.

######  Lemma 11.

Let $\mathsf{P}_{N}^{p}$ be a peeled program fed as input to the function
ComputeAffected. Let $vA$ be a scalar variable/array that is absent in
$\mathsf{AffectedVars}$ when ComputeAffected terminates. If $\mathsf{P}_{N-1}$
and $\mathsf{P}_{{N}}^{\star}$ are executed starting from the same state
$\sigma$, then $vA$ has the same value on termination of both programs.

Proof: We prove the lemma by contradiction. If possible, let $\sigma$ be a
state (i.e, valuation of variables and arrays) such that $vA$ has different
values on termination of $\mathsf{P}_{N-1}$ and $\mathsf{P}_{{N}}^{\star}$,
when both programs are executed starting from $\sigma$. As before, we use
$\pi$ and $\pi^{\prime}$ to denote the paths in the CFGs of $\mathsf{P}_{N-1}$
and $\mathsf{P}_{{N}}^{\star}$ respectively, that correspond to the execution
of the respective programs starting from $\sigma$. Note that by definition,
none of these CFGs contain any peeled nodes. We consider the following cases.

  * •

If none of $\pi$ and $\pi^{\prime}$ updates $vA$, the value of $vA$ at the end
of execution of the two programs is the same as the value it had in $\sigma$.
Clearly, the lemma holds in this case.

  * •

Suppose node $n_{i_{j}}$ in $\pi$ updates $vA$. We define
$\mathit{Branch}({\pi},{n_{i_{j}}})$ to be the set of all nodes $n_{i_{k}}$ in
the prefix of $\pi$ ending at $n_{i_{j}}$ such that $n_{i_{k}}$ corresponds to
a conditional branch statement. Similarly, $\mathit{Dep}({\pi},{n_{i_{j}}})$
is defined to be the set of all nodes $n_{i_{k}}$ in the same prefix of $\pi$
such that there is a path through data dependency edges in $DE^{p}$ from node
$n_{i_{k}}$ to either $n_{i_{j}}$ or to one of the nodes in
$\mathit{Branch}({\pi},{n_{i_{j}}})$.

If possible, let $n_{i_{k}}$ be a node in $\mathit{Branch}({\pi},{n_{i_{j}}})$
such that the branch condition in $\mu^{p}(n_{i_{k}})$ has a (possibly
transitive) data dependence on $N$. By Lemma 9, $n_{i_{k}}$ must be added to
$\mathsf{WorkList}$ sometime during the execution of ComputeAffected. Since
$n_{i_{j}}$ is reachable from $n_{i_{k}}$ along $\pi$, this further implies
that $n_{i_{j}}$ must be added to $\mathsf{WorkList}$, and subsequently
$vA\in\mathit{def}(n_{i_{j}})$ must be added to $\mathsf{AffectedVars}$ during
the execution of ComputeAffected. However, we know that $vA$ is not present in
$\mathsf{AffectedVars}$ on termination of ComputeAffected. Therefore, no
branch condition in any node $n_{i_{k}}$ in
$\mathit{Branch}({\pi},{n_{i_{j}}})$ can be transitively data dependent on
$N$. It follows that no node in $\mathit{Branch}({\pi},{n_{i_{j}}})$ can be
added to $\mathsf{WorkList}$ during the execution of ComputeAffected. Hence,
none of them can be present in $\mathsf{ProcessedNodes}$ on termination of
ComputeAffected. By Lemma 10, it now follows that if
$(n_{i_{0}},n_{i_{1}},\ldots,n_{i_{j}})$ is a prefix of $\pi$, then
$(n_{i_{0}}^{\prime},n_{i_{1}}^{\prime},\ldots,n_{i_{j}}^{\prime})$ must be a
prefix of $\pi^{\prime}$.

Since the scalar variable/array $vA$ is updated at $n_{i_{j}}$ in $\pi$, the
statement at $n_{i_{j}}^{\prime}$ in $\pi^{\prime}$ must also update $vA$.
Therefore, (i) $vA$ is updated at $n_{i_{j}}^{\prime}$ in $\pi^{\prime}$, and
(ii) for every node $n_{i_{k}}$ in
$\mathit{Dep}({\pi},{n_{i_{j}}})\cup\mathit{Branch}({\pi},{n_{i_{j}}})$, the
corresponding node $n_{i_{k}}^{\prime}$ is present in
$\mathit{Dep}({\pi^{\prime}},{n_{i_{j}}^{\prime}})\cup\mathit{Branch}({\pi^{\prime}},{n_{i_{j}}^{\prime}})$.

Finally, we argue that no node in $\mathit{Dep}({\pi},{n_{i_{j}}})$ can be
transitively data dependent on $N$. Indeed, if this was not the case, by Lemma
9, $n_{i_{j}}$ would be added to $\mathsf{WorkList}$ during the execution of
ComputeAffected, and hence $vA$ would be added to $\mathsf{AffectedVars}$.
However, this violates the premise that $vA$ is absent in
$\mathsf{AffectedVars}$. Combining this with the result obtained above, we
find that as far as path $\pi$ is concerned, no node in
$\mathit{Dep}({\pi},{n_{i_{j}}})\cup\mathit{Branch}({\pi},{n_{i_{j}}})$ is
transitively data dependent on $N$. Since modifications, if any, in statements
at corresponding nodes of $\mathsf{P}_{N-1}$ and $\mathsf{P}_{{N}}^{\star}$
only involve replacing $N-1$ by $N$, such modifications preserve the
dependence of every node on $N$. Therefore, no node in
$\mathit{Dep}({\pi^{\prime}},{n_{i_{j}}^{\prime}})\cup\mathit{Branch}({\pi^{\prime}},{n_{i_{j}}^{\prime}})$
transitively depends on $N$. This implies that the statements labeling nodes
in $\mathit{Dep}({\pi},{n_{i_{j}}})\cup\mathit{Branch}({\pi},{n_{i_{j}}})$ in
$\pi$ are identical to the statements labeling the corresponding nodes in
$\mathit{Dep}({\pi^{\prime}},{n_{i_{j}}^{\prime}})\cup\mathit{Branch}({\pi^{\prime}},{n_{i_{j}}^{\prime}})$.

Since both $\mathsf{P}_{N-1}$ and $\mathsf{P}_{{N}}^{\star}$ start from the
same state $\sigma$, the values of $vA$ computed by $\mathsf{P}_{N-1}$ after
executing the sequence of statements corresponding to
$(n_{i_{0}},n_{i_{1}},\ldots,n_{i_{j}})$ must therefore be identical to that
computed by $\mathsf{P}_{{N}}^{\star}$ after executing the sequence of
statements corresponding to
$(n_{i_{0}}^{\prime},n_{i_{1}}^{\prime},\ldots,n_{i_{j}}^{\prime})$. This
proves the lemma.

  * •

The case when node $n_{i_{j}}^{\prime}$ in $\pi^{\prime}$ updates $vA$ is
analogous to the above case.

For a variable/array $vA$ that is not identified as affected, $vA$ cannot be
in the $\mathit{def}$ set of a non-peeled node that either (i) has a
transitive data dependence on $N$ or on a peeled node, or (ii) has a control
flow path from a branch node that, in turn, has a transitive data dependence
on $N$ or on a peeled node. The following lemma formalizes this property.

######  Lemma 12.

Let $\mathsf{P}_{N}^{p}$ be a peeled program fed as input to the function
ComputeAffected. Let $vA$ be a scalar variable/array that is absent in
$\mathsf{AffectedVars}$ after ComputeAffected terminates. Then, $vA$ $\not\in$
$\mathit{def}(n)$ for every non-peeled node $n$ in $\mathsf{P}_{N}^{p}$ such
that some scalar variable/array in $\mathit{uses}(n)$ is transitively
data/control dependent on $N$ or on a peeled node in $\mathsf{P}_{N}^{p}$.

Proof: Consider an arbitrary non-peeled node $n$ in $\mathsf{P}_{N}^{p}$ such
that some scalar variable/array in $\mathit{uses}(n)$ has a transitive
data/control dependence on $N$ or on a peeled node. Then, by Lemma 9, $n$ must
be added to $\mathsf{WorkList}$ sometime during the execution of
ComputeAffected. Consequently, $n$ must also be removed from
$\mathsf{WorkList}$ (line 6 of ComputeAffected). If $n$ is an assignment node,
then $\mathit{def}(n)$ is added to the set $\mathsf{AffectedVars}$ (line 9 of
ComputeAffected). But since $vA$ is absent in $\mathsf{AffectedVars}$, it
follows that $vA$ $\not\in$ $\mathit{def}(n)$.

For clarity of exposition, we will henceforth refer to the property formalized
in Lemma 12 as the _“not-affected”_ property in our arguments.

######  Example 5.

Consider the peeled program in Fig. 17 along with its DDG in Fig. 18. Recall
that nodes in the DDG are named such that node $n_{i}$ corresponds to the
statement at line $i$ of the peeled program. The value of variable S computed
in the peeled node (line $5$ in Fig. 17) of the first loop is used to define
array A1 in the body of the second loop (line $7$). Furthermore, the value of
variable S computed in line $5$ is used to initialize the value of S1 in line
$10$. Thus, the algorithm initializes the worklist with the non-peeled nodes
$n_{7}$ and $n_{10}$ that are data dependent on the peeled node $n_{5}$. Array
A1 and variable S1 updated at $n_{7}$ and $n_{10}$ respectively are marked as
affected in line 9 of ComputeAffected. We then add non-peeled nodes that have
a data dependence on $n_{7}$ and $n_{10}$ to the worklist in line 11 of the
algorithm. Since array A1 is used in node $n_{12}$ in the third loop to define
the variable S1, $n_{12}$ is added to the worklist. Subsequently, the variable
S1 updated at $n_{12}$ is marked as affected. No further non-peeled nodes have
any data dependence on $n_{12}$ and the worklist therefore becomes empty.
Function ComputeAffected therefore terminates with $\\{$A1, S1$\\}$ as the set
of potentially affected variables/arrays. Note that variable S updated in the
first loop (line 3 of Fig. 17) is not marked as affected since its value
doesn’t transitively depend on $N$ or on any variable/array updated in peeled
nodes.

###  4.5 Generating the Difference Program $\mathbf{\partial\mathsf{P}_{N}}$

We now have most of the ingredients to generate $\partial\mathsf{P}_{N}$ from
$\mathsf{P}_{N}$ such that $\mathsf{P}_{N}$ and $\mathsf{P}_{N-1}\mathchar
24635\relax\;\partial\mathsf{P}_{N}$ have the same effect on scalar variables
and arrays of interest. For notational convenience, in the remainder of this
subsection, we use $\mathsf{P}_{N}$ to denote the renamed version of a given
program, and $\mathsf{P}_{N}^{p}$ to denote the peeled version of the renamed
program.

Generating the difference program ${\partial\mathsf{P}_{N}}$ from the renamed
and peeled program using the set of affected variables computed previously is
still a daunting task. In order to help the reader better visualize the
computation of difference program as well as to simplify the proof of
correctness, we present steps involved in the computation of
$\partial\mathsf{P}_{N}$ as a sequence of simple program transformations. Fig.
20 presents a high level overview of this sequence of transformations. We
start with a peeled program $\mathsf{P}_{N}^{p}$. We first canonicalize it to
a program $\mathsf{T}_{N}^{p}$ that consists of a sequence of statements of a
specific form (explained in Sect. 4.5.1). The statements in
$\mathsf{T}_{N}^{p}$ corresponding to the peels of loops in
$\mathsf{P}_{N}^{p}$ are then moved to the end of $\mathsf{T}_{N}^{p}$ to
obtain the program $\mathsf{T}_{N}^{o}$. The resulting program
$\mathsf{T}_{N}^{o}$ can be viewed as the program $\mathsf{P}_{{N}}^{\star}$
followed by the peels of all loops in $\mathsf{P}_{N}^{p}$. We call the block
of statements corresponding to the peels of all loops as
$\mathsf{Peel}({\mathsf{P}_{N}})$. Finally, if variables/arrays of interest
are not those identified as affected by ComputeAffected,
$\mathsf{P}_{{N}}^{\star}$ can be replaced with $\mathsf{P}_{N-1}$. This
allows us to obtain the difference program as
$\mathsf{Peel}({\mathsf{P}_{N}})$. In the subsequent sections, we present each
transformation in detail, describe the programs generated by them and prove
that they preserve the overall semantics of the program as far as the
variables/arrays of interest are concerned. This allows us to show that for a
large class of programs wherein the variables/arrays of interest have specific
properties, it is possible to use just the peels of loops in
$\mathsf{P}_{N}^{p}$ as the difference program. This simplifies the
computation of $\partial\mathsf{P}_{N}$ significantly.

$\mathsf{P}_{N-1}$$\mathsf{Peel}({\mathsf{P}_{N}^{p}})$$\mathsf{P}_{N}^{p}$$\mathsf{P}_{{N}}^{\star}$$\mathsf{Peel}({\mathsf{P}_{N}^{p}})$$\mathsf{T}_{N}^{p}$$\mathsf{T}_{N}^{o}$$\mathsf{P}_{N}^{o}$

Figure 20: Sequence of program transformations to decompose
$\mathsf{P}_{N}^{p}$ into $\mathsf{P}_{N-1}\mathchar
24635\relax\;\mathsf{Peel}({\mathsf{P}_{N}^{p}})$

We continue to use $vA$ to denote a scalar variable or an array depending on
the context. If $vA$ is an array, the discussion below applies to every
individual element $vA[j]$, where $j$ is an index in the allowed range of
indices of array $vA$. However, for notational convenience, we use $vA$ (and
not $vA[j]$) to refer to such an array element in the lemmas below. Note that
this implies that the proof, once completed, applies to an arbitrary element
of the array $vA$, and hence to the whole of $vA$.

####  4.5.1 Canonicalizing the Program

In this section, we describe a simple transformation of the program
$\mathsf{P}_{N}^{p}$ that allows us to view the program as a _linear sequence
of statements_ of a specific form. The transformation is only meant for
purposes of simplifying the proofs of lemmas in the subsequent subsections and
making them more approachable.

For every program $\mathsf{P}_{N}$ that can be generated by the grammar shown
in Sect. 3, we rewrite the corresponding peeled program $\mathsf{P}_{N}^{p}$
as a linear sequence of statements of the form:

${\mathbf{if}}(\mathsf{C})~{}{\mathbf{then}}~{}{\mathsf{S}}~{}{\mathbf{else}}~{}{\mathsf{skip}},$

where $\mathsf{skip}$ is shorthand for the assignment statement x = x; for an
arbitrary scalar variable x in $\mathsf{P}_{N}^{p}$. The program fragment
$\mathsf{S}$ is either (i) a loop, or (ii) a peel of a loop, or (iii) an
assignment statement outside loops and peels in $\mathsf{P}_{N}^{p}$. The
conditional expression $\mathsf{C}$ is a conjunction of boolean expressions
along the $\mathsf{True}$ (resp. $\mathsf{False}$) branches of all the
conditional branch nodes $b$ within the scope of which the program fragment
$\mathsf{S}$ occurs in the program $\mathsf{P}_{N}^{p}$. Since $\mathsf{skip}$
does not change values of any variables or arrays, we omit the else part in
our subsequent discussion for notational clarity. Henceforth, we refer to
statements in this form as guarded statements.

We now describe how to construct a program $\mathsf{T}_{N}^{p}$ consisting of
a sequence of guarded statements starting from a given peeled program
$\mathsf{P}_{N}^{p}$. We have already seen earlier how to construct the
collapsed CFG of $\mathsf{P}_{N}^{p}$. For each loop that has been peeled, we
additionally collapse all nodes in the peel of the loop to a single node to
obtain an even more collapsed CFG $G_{C}$. By the restrictions imposed by our
grammar, $G_{C}$ is necessarily a directed acyclic graph. We first assign a
topological index to all nodes of $G_{C}$ such that the index of a node $n$ is
strictly larger than the indices of all nodes that have edges to $n$ in
$G_{C}$. For each node $n$ in order of its topological index, we now construct
a guarded statement for it as follows. If $n$ does not lie within the scope of
any branch statements, we construct the guarded statement
‘$\mathbf{if}$($\mathsf{True}$) $\mathbf{then}$ $\mathsf{S}$’ where
$\mathsf{S}$ corresponds to the loop, peel or assignment statement at node
$n$. Otherwise, we conjoin the conditional expressions along the
$\mathsf{True}$ (resp. $\mathsf{False}$) branches of all the conditional
branch nodes $b$ within the scope of which node $n$ lies in $G_{C}$. If this
conjoined expression is $\mathsf{C}$, then we generate the guarded statement
‘$\mathbf{if}$($\mathsf{C}$) $\mathbf{then}$ $\mathsf{S}$’ where $\mathsf{S}$
is as previously defined. We illustrate the above construction on an example
program with loops and branches.

Table 1: (a) Program $\mathsf{P}_{N}^{p}$, (b) Transformed Program
$\mathsf{T}_{N}^{p}$, (c) Transformed & Reordered Program $\mathsf{T}_{N}^{o}$
and (d) Program $\mathsf{P}_{N}^{o}$ / Program
$\mathsf{P}_{{N}}^{\star}\mathchar
24635\relax\;\mathsf{Peel}({\mathsf{P}_{N}^{p}})$

    1.   S = 10;
    2.   if(S > 5) {
    3.     S1 = 1;

    4a.    for(i=0; i<N-1; i++)  //Loop L1
    4b.      A1[i] = A[i] + 1;

    5.     A1[N-1] = A[N-1] + 1; //Peel of L1
    6.   } else {
    7.     S1 = 20;

    8a.    for(i=0; i<N-1; i++)  //Loop L2
    8b.      A1[i] = A[i];

    9.     A1[N-1] = A[N-1];     //Peel of L2
    10.  }

    11a. for(i=0; i<N-1; i++)    //Loop L3
    11b.   A2[i] = A1[i] + S1;

    12.  A2[N-1] = A1[N-1] + S1; //Peel of L3

|

    1’.  if(

    $\ignorespaces\mathsf{True}$

    ) S = 10;
    3’.  if(S > 5) S1 = 1;
    4’.  if(S > 5) Loop L1;
    5’.  if(S > 5) Peel of L1;
    7’.  if(!(S > 5)) S1 = 20;
    8’.  if(!(S > 5)) Loop L2;
    9’.  if(!(S > 5)) Peel of L2;
    11’. if(

    $\ignorespaces\mathsf{True}$

    ) Loop L3;
    12’. if(

    $\ignorespaces\mathsf{True}$

    ) Peel of L3;

---|---
(a) |  (b)

    1’.  if(

    $\ignorespaces\mathsf{True}$

    ) S = 10;
    3’.  if(S > 5) S1 = 1;
    4’.  if(S > 5) Loop L1;
    7’.  if(!(S > 5)) S1 = 20;
    8’.  if(!(S > 5)) Loop L2;
    11’. if(

    $\ignorespaces\mathsf{True}$

    ) Loop L3;

    5’.  if(S > 5) Peel of L1;
    9’.  if(!(S > 5)) Peel of L2;
    12’. if(

    $\ignorespaces\mathsf{True}$

    ) Peel of L3;

|

    1.   S = 10;
    2a.  if(S > 5) {
    3.     S1 = 1;
    4a.    for(i=0; i<N-1; i++)  //Loop L1
    4b.      A1[i] = A[i] + 1;
    6a.  } else {
    7.     S1 = 20;
    8a.    for(i=0; i<N-1; i++)  //Loop L2
    8b.      A1[i] = A[i];
    10a. }
    11a. for(i=0; i<N-1; i++)    //Loop L3
    11b.   A2[i] = A1[i] + S1;

    2b.  if(S > 5) {
    5.     A1[N-1] = A[N-1] + 1; //Peel of L1
    6b.  } else {
    9.     A1[N-1] = A[N-1];     //Peel of L2
    10b. }
    12.  A2[N-1] = A1[N-1] + S1; //Peel of L3

(c) |  (d)

######  Example 6.

Consider the peeled program $\mathsf{P}_{N}^{p}$ shown in Tab. 1(a). The
variables and arrays of the input program are renamed (as described in Sect.
4.1) ensuring that along each path of the program the value of a variable or
an array element is accessible till the end of the path and all the loops in
the program are peeled (as described in Sect. 4.2). We number the lines in the
program such that the statements in loops (and in peels) have the same line
number but with an alphabet appended when multiple statements are present.
This numbering allows us to refer to the program statements with a consistent
line number even after collapsing loops and peels. $\mathsf{P}_{N}^{p}$ has
three peeled loops, L1 (lines $4a$ and $4b$), L2 (lines $8a$ and $8b$) and L3
(lines $11a$ and $11b$). Loops L1 and L2 along with their peels are within the
scope of the conditional branch statement in line $2$. Loop L3 and its peel
are not within the scope of any branch statement.

Tab. 1(b) shows the program $\mathsf{T}_{N}^{p}$ generated by our
transformation. To distinguish the statements in $\mathsf{P}_{N}^{p}$ from
those in $\mathsf{T}_{N}^{p}$, the line numbers of statements in
$\mathsf{T}_{N}^{p}$ are suffixed with a prime symbol. As can be seen,
$\mathsf{T}_{N}^{p}$ is a linear sequence of guarded statements. The line
numbers of each guarded statement in $\mathsf{T}_{N}^{p}$ matches the line
number of the corresponding statement in $\mathsf{P}_{N}^{p}$. Notice that
every assignment statement in $\mathsf{P}_{N}^{p}$ appears exactly at one
unique location in $\mathsf{T}_{N}^{p}$.

Note that if a variable/array element is used in the conditional expression at
a branch node $b$, then it must have been updated (if at all) in an assignment
node that has a control flow path to $b$. From the no-overwriting property as
stated in Lemma 4, it now follows that the same variable/array element cannot
be updated in any node that has a control flow path from $b$. This includes
all nodes within the scope of branch $b$. This interesting property allows us
to prove the following lemma.

######  Lemma 13.

Let $\mathsf{T}_{N}^{p}$ be the canonicalized version of $\mathsf{P}_{N}^{p}$.
Let $n$ be a node corresponding an assignment statement in the CFG of
$\mathsf{P}_{N}^{p}$ (and hence $\mathsf{T}_{N}^{p}$). Let $\pi$ (resp.
$\pi^{\prime}$) be a path in the collapsed CFG of $\mathsf{P}_{N}^{p}$ (resp.
$\mathsf{T}_{N}^{p}$) starting from the state $\sigma$. Then the following
hold.

  1. 1.

$n$ is reached along $\pi$ iff $n$ is also reached along $\pi^{\prime}$.

  2. 2.

The program state $\sigma_{n}$ is computed at node $n$ along $\pi$ iff the
program state $\sigma_{n}$ is computed at node $n$ along $\pi^{\prime}$.

Proof: (Sketch) We consider a path $\pi$ in the collapsed CFG of
$\mathsf{P}_{N}^{p}$ corresponding to an execution starting from $\sigma$. Let
$n$ be a node corresponding to an assignment statement along path $\pi$. Let