Verifying Array Manipulating Programs with Full-Program Induction
27
3.1 Preliminaries
We consider array manipulating programs generated by the grammar shown
below (adapted from [4]).
PB ::= St
St ::= v := E | A[E] := E | if (BoolE) then St else St | St ; St |
for ( := 0; < E; := +1) {St1}
St1 ::= v := E | A[E] := E | if (BoolE) then St1 else St1 | St1 ; St1
E ::= E op E | A[E] | v | | c | N
op ::= + | - | * | /
BoolE ::= E relop E | BoolE AND BoolE | NOT BoolE | BoolE OR BoolE
This grammar restricts programs to have non-nested loops. While this limits
the set of programs to which our technique currently applies, there is a large
class 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 subclass
of programs with nested loops. However, characterizing this class of programs
through a grammar is a bit unwieldy, and we avoid doing so for reasons of clarity.
A program P N is a tuple (V, L, A, PB, N), where V is a set of scalar variables,
L ⊆ V is a set of scalar loop counter variables, A is a set of array variables,
PB is the program body, and N is a special symbol denoting a positive integer
parameter. In the grammar shown above, we assume A ∈ A, v ∈ V \L, ∈ L and
c ∈ Z. Furthermore, “relop” is assumed to be one of the relational operators and
“op”is an arithmetic operator from the set {+, -, *, /}. We also assume that each
loop L has a unique loop counter variable which 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 . Finally, for each loop with termination condition
< E, we assume that E 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 verify
Hoare triples of the form {ϕ(N )} P N {ψ(N )}, where ϕ(N ) and ψ(N ) are either
universally quantified formulas of the form ∀I (Φ(I, N ) =⇒ Ψ (A, V, I, N)) or
quantifier-free formulas of the form Ξ(A, V, N). In the above, I is a sequence of
array index variables, Φ is a quantifier-free formula in the theory of arithmetic
over integers, and Ψ and Ξ are quantifier-free formulas in the combined theory
of arrays and arithmetic over integers.
Static single assignment (SSA) [27] is a well-known technique for renaming
scalar variables such that a variable is written at most once in a program. For
our purposes, we also wish to rename arrays so that each loop updates its own
version of an array and multiple writes to an array element within the same loop
happen on different versions of the array. Array SSA [20] renaming has been
studied earlier in the context of compilers to achieve this goal. We propose using
SSA renaming for both scalars and arrays as a pre-processing step of our analysis.
Therefore, we assume henceforth that the input program is SSA renamed (for
both scalars and arrays). We also assume that the post-condition is expressed in
terms of these SSA renamed scalar and array variables.
27
3.1 Preliminaries
We consider array manipulating programs generated by the grammar shown
below (adapted from [4]).
PB ::= St
St ::= v := E | A[E] := E | if (BoolE) then St else St | St ; St |
for ( := 0; < E; := +1) {St1}
St1 ::= v := E | A[E] := E | if (BoolE) then St1 else St1 | St1 ; St1
E ::= E op E | A[E] | v | | c | N
op ::= + | - | * | /
BoolE ::= E relop E | BoolE AND BoolE | NOT BoolE | BoolE OR BoolE
This grammar restricts programs to have non-nested loops. While this limits
the set of programs to which our technique currently applies, there is a large
class 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 subclass
of programs with nested loops. However, characterizing this class of programs
through a grammar is a bit unwieldy, and we avoid doing so for reasons of clarity.
A program P N is a tuple (V, L, A, PB, N), where V is a set of scalar variables,
L ⊆ V is a set of scalar loop counter variables, A is a set of array variables,
PB is the program body, and N is a special symbol denoting a positive integer
parameter. In the grammar shown above, we assume A ∈ A, v ∈ V \L, ∈ L and
c ∈ Z. Furthermore, “relop” is assumed to be one of the relational operators and
“op”is an arithmetic operator from the set {+, -, *, /}. We also assume that each
loop L has a unique loop counter variable which 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 . Finally, for each loop with termination condition
< E, we assume that E 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 verify
Hoare triples of the form {ϕ(N )} P N {ψ(N )}, where ϕ(N ) and ψ(N ) are either
universally quantified formulas of the form ∀I (Φ(I, N ) =⇒ Ψ (A, V, I, N)) or
quantifier-free formulas of the form Ξ(A, V, N). In the above, I is a sequence of
array index variables, Φ is a quantifier-free formula in the theory of arithmetic
over integers, and Ψ and Ξ are quantifier-free formulas in the combined theory
of arrays and arithmetic over integers.
Static single assignment (SSA) [27] is a well-known technique for renaming
scalar variables such that a variable is written at most once in a program. For
our purposes, we also wish to rename arrays so that each loop updates its own
version of an array and multiple writes to an array element within the same loop
happen on different versions of the array. Array SSA [20] renaming has been
studied earlier in the context of compilers to achieve this goal. We propose using
SSA renaming for both scalars and arrays as a pre-processing step of our analysis.
Therefore, we assume henceforth that the input program is SSA renamed (for
both scalars and arrays). We also assume that the post-condition is expressed in
terms of these SSA renamed scalar and array variables.