SOURCE ARCHIVE
EXTRACTED CONTENT
46,400 charsTowards a framework for constraint-based test case generation
Fran¸cois Degrave?2, Tom Schrijvers??1, and Wim Vanhoof2
1 Department of Computer Science
Katholieke Universiteit Leuven
2 Faculty of Computer Science
University of Namur
Abstract. In this paper, we propose an approach for automated test
case generation based on techniques from constraint programming (CP).
We advocate the use of standard CP search strategies in order to express
preferences on the generated test cases and to obtain the desired degree
of coverage. We develop our framework in the concrete context of an
imperative language and show that the technique is sufficiently powerful
to deal with arbitrary pointer-based data-structures allocated on the
heap.
1 Introduction
It is a well-known fact that a substantial part of a software development budget is
spent on the act of correcting errors in the software under development. Arguably
the most commonly applied strategy for finding errors and thus producing (more)
reliable software is testing: running a software component with respect to a well-
chosen set of inputs and comparing the outputs that are produced with the
expected results in order to find errors. In previous work [4], we have developed
a technique that allows to automatically generate a set of test inputs for a given
program written in the logic programming language Mercury. The basic idea
of that technique, itself inspired by [20], is as follows: first, a path through the
control-flow graph of a predicate is transformed into a set of constraints on the
(input) variables of the predicate such that when the predicate is called with
input values satisfying these constraints, its execution is guaranteed to follow
the given path. Next, a dedicated constraint solver is used to compute such
concrete input values. By repeating the process for a carefully constructed finite
subset of all execution paths one can guarantee that the set of generated input
values cover a substantial part of the source code and can as such be used to
perform so-called structural or whitebox testing.
In the current paper, we generalize and extend the approach of [4], reformu-
lating it completely within the framework of constraint programming (CP). This
presents several advantages over [4] and similar proposals:
? Supported by a grant FRIA - Belgium.
?? Post-doctoral researcher of the Fund for Scientific Research - Flanders.
– The whole process – from the construction of an execution path to the gener-
ation of concrete test inputs – is now modeled as a single constraint problem,
rather than as a pair of complementary processes. This presents a cleaner
and more uniform formalisation of the technique.
– More importantly, since the selection of an execution path is modeled within
the constraint problem, one can obtain different degrees of coverage, or even
coverage with respect to different criteria, by using different search strategies
within the solver. In other words, the technique can – at least to a certain
extent – be seen as parametrised with respect to a coverage criterion or a
desired degree of coverage.
– The resulting technique is also more efficient, since it avoids the construc-
tion of constraint sets representing paths that do not correspond to a real
execution.
In order to show the power of our generalized approach, we cast it in the setting
of a (small) deterministic imperative language with pointer-based data struc-
tures and show that our approach is able to generate test cases dealing with
in-place updates of variables, pointers and a variety of potentially cyclic data
structures. As the definition below shows, we only consider integer values and
data structures constructed from simple “cons” cells having two fields that we
will name head and tail. We indicate in Section 2.6 how our technique for test
case generation can easily be extended to deal with a more involved language
having primitive values other than integers and full struct-like data structures.
integers n
variables x
expressions e ::= x | n | nil | new cons(e1, e2) | e.head | e.tail
| e1 == e2 | e /= e2 | e1+e2
1
statements s ::= skip | l := e | s ;s2 | if e then s1 else s2
1
| while e { s }
left-hand sides l ::= x | l.head | l.tail
As usual, expressions are used to syntactically represent values within the
source code of a program. Among the possible expressions are program variables,
integers, the null-pointer nil, a reference to a newly heap-allocated cons cell new
cons(e1,e2), the selection of the head (e.head), respectively tail (e.tail) field of
the cons cell referenced by e, equality and inequality tests (== and /=), and the
arithmetic operator for addition +.3 We will assume that ImpL is simply typed
and only allows comparison of two values belonging to the same type (either
integers or references).4 Moreover, arithmetic is only allowed on integer values;
the language does not support pointer arithmetics.
A program in ImpL is a single statement or a sequence of statements, where a
statement is either a no-op (skip), an assignment, another sequence, a selection
3 Other arithmetic operators are omitted in order to keep the formal definition of the semantics small, but they can be added at will. 4 Integers are also used as booleans: 0 denotes false and all other integers denote true.
2
or a while-loop. The left-hand side of an assignment is either a variable or a
reference to one of the fields in a cons cell. Consider, for example, the following
simple program:
while (x.tail.head /= x.head) {
x := x.tail
};
x.tail := nil
The above program basically manipulates a simply linked list x whose cells consist of two fields: a head containing an integer and a tail containing a pointer to the following cell or nil. It scans the list for two successive identical elements, and severs the list after the first such occurrence. For example, using the notation [1,2,3] for the nil-terminated linked list with successive elements 1,2 and 3, the effect of running this program with x the list [1,2,3,3,4], is that, after the while loop, the list will have the value [1,2,3].
2 Generating test inputs
2.1 Overview
As usual, execution of an imperative program manipulates an environment E
and a heap H . An environment is a finite mapping from variables to values,
where a value is either an integer, nil or a reference to a cons cell represented
by ptr(r) with r a unique value denoting the address of the cons cell on the heap.
Likewise, a heap is a finite mapping from such references r to cons cells of the
form cons(vh,ve) with vh and ve values (possibly including references to other
cons cells). For the example given above (with x initially the list [1,2,3,3,4]),
the environment and heap before and after running the program would look as
follows:
E : x → ptr(r₁) E : x → ptr(r₁)
H : r₁ → cons(1,ptr(r₂)) r₄ → cons(3,ptr(r₅)) H : r₁ → cons(1,ptr(r₂)) r₂ → cons(2,ptr(r₃)) r₅ → cons(4,nil) r₂ → cons(2,ptr(r₃)) r₃ → cons(3,ptr(r₄)) r₃ → cons(3,nil)
Now, in order to generate test inputs for a program, the idea is to symbolically
execute the program, replacing unknown values by constraint variables. During
such a symbolic execution, each test in the program (i.e. the if-then-else and while
conditions) represents a choice; the sequence of choices made determines the
execution path followed. There are many possible execution paths through the
program. Each one of them can be represented by constraints on the introduced
variables and on the environment and heap.
Returning to our example, we would replace the concrete value for x by a
constraint variable, say V, representing an unknown value. Among the infinite
number of possible execution paths, a particular path would execute the while
3
condition three times, and the loop body twice. This would imply that the value represented by V is a list of at least 4 elements, and the third and fourth element are identical, whereas the first differs from the second and the second form the third. This information would be represented by constraints on V and the heap collected along the execution. Solving these constraints could get us for instance the concrete input [1,2,3,3,4] proposed above. However, there are many other concrete inputs that satisfy these constraints: [1,2,3,3], [0,1,0,0], or even the cyclic list that starts with [1,2,1] and then points back the first element. Using our constraint-based approach, we can both capture the many paths and the many solutions for a single path as non-determinism in our constraint- based modelling of test case generation. This allows us to use the search strategies of CP to deal with both of them. For instance, we can find all paths up to length 6 using a simple depth-bounded search. Figure 1 illustrates the search tree for the example.
[x,x,...]
[x,y,y,...] [0]* [1]* [-1]*
[0,0] [0,0]* [0] + [0]* ...
[1,1] [1,1]* [1]+[1]*
[x,y,z,z,...] [-1,-1]... [-1,-1]*... [-1]+[-1]*...
Fig. 1. Tree of paths (left) and tree of value assignments for left-most path (right).
2.2 Constraint Generation
In order to represent unknown input data we add logical (or constraint) vari-
ables to the semantic domain of values and represent the environment and heap
by logical variables as well. In order to model symbolic execution of our lan-
guage, we introduce a semantics in which program state is represented by a
triple 〈E, H, C 〉 where E and H are constraint variables symbolically represent-
ing, respectively, the environment and heap, and C is a set of constraints over
E and H . Constraints are conjunctions of primitive constraints that take the
following form:
– o1 = o2, equality of two syntactic objects,
– o1 = o2, inequality of two syntactic objects,
4
(Var) (x → v) ∈ E 〈E, H〉 x v〈E, H〉 (Int) 〈E, H〉 n ∈ Z n n〈E, H〉 (Nil) 〈E, H〉 nil nil〈E, H〉 (Cons) 〈E, H¹〉 e¹ v₁〈E, H₂〉 〈E, H₂〉 e₂ v₂〈E, H₃〉 r fresh 〈E, H₁〉 new cons(e₁, e₂) ptr(r)〈E, H₃ ] {r → cons(v₁, v₂)}〉 〈E, H₁〉 e ptr(r)〈E, H 2 (Head) 〈E, H₁〉 e.head〉 (rvₕ→ cons(vₕ, vₜ)) ∈ H₂ 〈E, H₂〉 (Tail) 〈E, H¹〉 e ptr(r)〈E, H 2〉 (r → cons(vₕ, vₜ)) ∈ H₂ 〈E, H₁〉 e.tail vₜ〈E, H₂〉 (EqualT) 〈E, H¹〉 e¹ v₁〈E, H₂〉 〈E, H₂〉 e₂ v₂〈E, H₃〉 v₁ ≡ v₂ 〈E, H₁〉 e1 == e₂ 1〈E, H₃〉 (EqualF) 〈E, H¹〉 e¹ v₁〈E, H₂〉 〈E, H₂〉 e₂ v₂〈E, H₃〉 v₁ ≡ v₂ 〈E, H₁〉 e1 == e₂ 0〈E, H₃〉 (NEqualT) 〈E, H¹〉 e¹ v₁〈E, H₂〉 〈E, H₂〉 e₂ v₂〈E, H₃〉 v₁ ≡ v₂ 〈E, H₁〉 e1 /= e₂ 1〈E, H₃〉 (NEqualF) 〈E, H¹〉 e¹ v₁〈E, H₂〉 〈E, H₂〉 e₂ v₂〈E, H₃〉 v₁ ≡ v₂ 〈E, H₁〉 e1 /= e₂ 0〈E, H₃〉
Fig. 2. Semantics of expressions in ImpL
(Skip) 〈E, H〉 skip 〈E, H〉 (VarAss) 〈E, H₁〈E, H¹〉 e v〈E, H₂〉 〉 }x := e 〈E ] {x → v}, H 〉 2 2 ( E, H₂〉 (r → cons(vₕ, vₜ)) ∈ H₂ (HeadAss) 〈E, H¹〉 e v〈E, H₂〉 〈E, H 〉 l ptr r)〈 〈E, H₁〉 l.head := e 〈E, H₂ ] {r → cons(v, vₜ)}〉 2 ptr 〈 2〉 (r → cons(vₕ, vₜ)) ∈ H₂ (TailAss) 〈E, H¹〉 e v〈E, H₂〉 〈E, H 〉 l (r) E, H 〈E, H₁〉 l.tail := e 〈E, H₂ ] {r → cons(vₕ, v)}〉 2 , H 〉 s₂ 〈E₃, H₃〉 (Seq) 〈E¹, H¹〉 s¹ 〈E², H²〉 〈E 2 〈E₁, H₁〉 s₁;s₂ 〈E , H 〉 3 3 (IfThen) 〈E¹, H¹〉 e n〈E₁, H₂〉 n ≡ 0 〈E₁, H₂〉 s₁ 〈E₂, H₃〉 〈E₁, H₁〉 if e then s1 else s₂ 〈E₂, H₄〉 (IfElse) 〈E¹, H¹〉 e n〈E₁, H₂〉 n ≡ 0 〈E₁, H₂〉 s₂ 〈E₂, H₃〉 〈E₁, H₁〉 if e then s1 else s₂ 〈E₂, H₄〉 〈E₁, H 〉 e n〈E₁, H₂〉 1 n ≡ 0 〈E₁, H₂〉 s 〈E₂, H 3 (WhileT) 〈E₁, H₁〉 while〉 e 〈E{ s², H³〉 while e { s } 〈E³, H⁴〉 } 〈E₃, H₄〉 〈E₁, H₁〉 e n〈E₁, H₂〉 n ≡ 0 (WhileF) 〈E₁, H₁〉 while e { s } 〈E₁, H 〉 2
Fig. 3. Semantics of statements in ImpL
5
– (o1 → o2) ∈ M , membership of a mapping M , and
– M1 ] {o1 → o2} = M2, update of a mapping M1.
where a mapping M denotes a constraint variable representing an environment or a heap. Constraint solvers for these constraints are defined in Section 2.4. The symbolic semantics is depicted in Figures 4 and 5. In these figures and in the remainder of the text, we use uppercase characters to syntactically distin- guish constraint variables from ordinary program variables (represented by low- ercase characters). A judgement of the form 〈E0, H0, C0〉 e v〈E0, H1〉C1 de- notes that given a program state 〈E0, H , C 〉, the expression e evaluates to value 0 0 v and transforms the program state into a state represented by 〈E0, H1, C1〉. Note that H1 is a fresh constraint variable that represents the possibly modi- fied heap whose content is defined by the constraints in C1. Likewise, a judge- ment of the form 〈E0, H0, C0〉s〈E1, H , C 〉 denotes the fact that a statement 1 1 s transforms a program state represented by 〈E0, H0, C0〉 into the one repre- sented by 〈E1, H1, C1〉. Since a newly added constraint can introduce incon- sistencies in the set of collected constraints, we define the conditional eval- uation of an expression and a statement as follows: judgements of the form {E, H0, C0} e v〈E, H1, C1〉 and {E0, H0, C0}s〈E1, H1, C1〉 denote, respec- tively, 〈E, H0, C0〉 e v〈E, H1, C1〉 and 〈E0, H0, C0〉s〈E1, H1, C1〉 under the condition that C0 is consistent (represented by T |= C0, where T is the con- straint theory).5 Formally:
T |= C₀ 〈E, H0
(Cond-e) {E, H₀, C , C₀〉 e v〈E, H₁, C₁〉
0} e v〈E, H₁, C₁〉
0, H
0 0〉 s 〈E1, H1 1〉
(Cond-s) T |= C⁰ 〈E , C , C
{E₀, H₀, C } s 〈E₁, H₁, C₁〉
0
The use of conditional evaluation avoids adding further constraints to an already
inconsistent set. This implies that search strategies (see Section 2.5) will only
explore execution paths that can model a real execution.
2.3 Properties
Given environments E, E′ and heaps H , H ′, we use 〈E, H〉 ∼
= 〈E′, H′〉 to denote
the fact that E and E′ define the same program variables and that each such
variable either has the same primitive value (integer or nil) in both environments
or points to identical data structures in both heaps. More formally, this means
that there must exist a bijective mapping σ between (a subset of) the references
used in H and (a subset of) those used in H ′ such that ∀x ∈ dom(E) = dom(E′) :
E(x) =σ E′(x) where =σ is defined as follows: nil=σnil, n =σ n for all integer
constants n and ptr(r) =σ ptr(r′) if r′ = σ(r), H (r) = cons(v1, v2) and H ′(r′) =
cons(v1′ , v2′ ) and v1 =σ v1′ and v2 =σ v′ .
2
5 In practice, the consistency check may be incomplete. Then unreachable execution
paths may be explored.
6
(Var) 〈E, H, C〉 x V V fresh (Int) n ∈ Z
〈E, H, C ∧ {x → V } ∈ E〉 〈E, H, C〉 n n〈E, H, C〉
(Nil) 〈E, H, C〉 nil nil〈E, H, C〉
1 , C 〉 {E, H₁, C₁} e₂ v₂〈E, H₂, C₂〉 H₃, r fresh
(Cons) 〈E, H⁰, C⁰〉 e¹ v₁〈E, H 1 〈E, H₀, C₀〉 new cons(e₁, e2) ptr(r)〈E, H₃, C₂ ∧ H₃ = H₂ ] {r → cons(v₁, v₂)}〉 〈E, H₀, C 0 (Head) 〈E, H₀, C₀〉 e.head Vₕ〈E, H〉 e 1v〈E, H1, C1〉 R, Vₕ, Vₜ fresh , C₁ ∧ v = ptr(R) ∧ (R → cons(Vₕ, Vₜ)) ∈ H₁〉 〈E, H₀, C 0 (Tail) 〈E, H₀, C₀〉 e.tail Vₜ〈E, H〉 e 1 v〈E, H1, C1〉 R, Vₕ, Vₜ fresh , C₁ ∧ v = ptr(R) ∧ (R → cons(Vₕ, Vₜ)) ∈ H₁〉 (EqualT) 〈E, H⁰, C⁰〉 e¹ v 〈E, H₁, C₁〉1 {E, H₁, C₁} e₂ v₂〈E, H₂, C₂〉 〈E, H₀, C 〉 e₁ == e₂ 1〈E, H₂, C₂ ∧ v₁ = v₂〉 0 〈E, H₀, C₀〉 e₁ v 1 (EqualF) 〈E, H₀, C 〈E, H¹, C¹〉 {E, H₁, C₁} e₂ v₂〈E, H₂, C₂〉 0 〉 e₁ == e₂ 0〈E, H₂, C₂ ∧ v₁ = v₂〉 (NEqualT) 〈E, H⁰, C⁰〉 e¹ v 〈E, H₁, C₁〉1 {E, H₁, C₁} e₂ v₂〈E, H₂, C₂〉 〈E, H₀, C 〉 e₁ /= e₂ 1〈E, H₂, C₂ ∧ v₁ = v₂〉 0 〈E, H₀, C₀〉 e₁ v 1 (NEqualF) 〈E, H₀, C 〈E, H¹, C¹〉 {E, H₁, C₁} e₂ v₂〈E, H₂, C₂〉 0 〉 e₁ /= e₂ 0〈E, H₂, C₂ ∧ v₁ = v₂〉 (Add) 〈E, H⁰, C⁰〉 e¹ 1 v₁〈E, H , C₁〉 {E, H₁, C₁} e₂ v₂〈E, H₂, C₂〉 v fresh 〈E, H₀, C 〉 e + e₂ v〈E, H₂, C₂ ∧ v = v₁ + v₂〉 0 1
Fig. 4. Symbolic evaluation of expressions.
Theorem 1 (Completeness). Let E and H be an environment and a heap, and s an instruction manipulating the variables in E. If 〈E, H〉 s 〈E′, H′〉 then there exists a satisfiable set of constraints C such that 〈Ev, Hv, true 〉 s 〈Ev′ , Hv′ , C〉 with ρ a solution for C such that 〈E, H〉 ∼ = 〈ρ(Ev), ρ(Hv)〉 〈E′, H′〉 ∼ = 〈ρ(Ev′ ), ρ(Hv′ )〉
The completeness property states that any concrete execution of a program s with respect to an initial environment E and heap H is modeled by some abstract derivation represented by a set of constraints C such that there exists a solution to C that models both the initial and final environment and heap. In other words, our method is able to capture all executions of a program fragment s. In addition, the soundness property given below states the inverse, namely that our method does not model spurious executions.
Theorem 2 (Soundness). Let s be an instruction. If 〈Ev, Hv, true 〉 s 〈Ev′ , Hv′ , C〉 and if there exists a solution ρ for the set of constraints C then 〈ρ(Ev), ρ(Hv)〉 s 〈E, H〉 such that
〈E, H〉 ∼
= 〈ρ(Ev′ ), ρ(Hv′ )〉.
7
(Skip) 〈E, H, C〉 skip 〈E, H, C〉
(VarAss) 〈E₀ 〈E₀, H₀, C₀〉 e v〈E₀, H₁, C₁〉 E₁ fresh
, H₀, C₀〉 x := e 〈E , H₁, C₁ ∧ E₁ = E₀ ] {x → v}〉
1
〈E, H₀, C₀〉 e v〈E, H 1 , C 〉 {E, H₁, C₁} l vᵣ 〈E, H₁, C₂〉
1
R, Vₕ, Vₜ, H₂ fresh C₃ ≡ C
2
(HeadAss) 〈E, H₀, C₀〉 l.head := e 〈E, H∧ vʳ = ptr(R) ∧ (R → cons(Vʰ, Vᵗ)) ∈ H¹ 2, C₃ ∧ H₂ = H₁ ] {R → cons(v, Vₜ)}〉 〈E, H₀, C₀〉 e v〈E, H 1 , C 〉 {E, H₁, C₁} l vᵣ 〈E, H₁, C₂〉 1 R, Vₕ, Vₜ, H₂ fresh C₃ ≡ C 2 (TailAss) 〈E, H₀, C₀〉 l.tail := e 〈E, H∧ vʳ = ptr(R) ∧ (R → cons(Vʰ, Vᵗ)) ∈ H¹ 2 , C₃ ∧ H₂ = H₁ ] {R → cons(Vₕ, v)}〉 〈E₀, H₀, C₀〉 s₁ 〈E₁, H , C 1 1 (Seq) 〈E₀, H₀, C 〉 {E₁, H₁, C₁} s₂ {E₂, H₂, C₂} 〉 s₁;s₂ 〈E₂, H₂, C₂〉0 〈E₀, H₀, C₀〉 e v〈E₀, H₁, C 1 (IfThen) 〈E₀, H₀, C₀〉 if e〉then{Es₁⁰, H¹, C¹ ∧ v = 0} s¹ {E¹, H², C²} else s₂ 〈E₁, H₂, C₂〉 〈E₀, H₀, C₀〉 e v〈E₀, H₁, C 1 (IfElse) 〈E₀, H₀, C₀〉 if e〉then{Es₁⁰, H¹, C¹ ∧ v = 0} s² {E¹, H², C²} else s₂ 〈E₁, H₂, C₂〉 〈E₀, H , C 〉 e v〈E₀, H₁, C₁〉 0 0 (WhileT) {E⁰, H¹, C¹ ∧ v = 0} s;while e { s } 〈E¹, H², C²〉 〈E₀, H₀, C₀〉 while e { s } 〈E₁, H₂, C₂〉 〈E₀, H , C 0 0 (WhileF) 〈E₀, H₀, C₀〉 while e〉 {e s v〈E, H₁, C₁〉 } 〈E₀, H₁, C₁ ∧ v = 0〉
Fig. 5. Symbolic execution of statements.
8
2.4 Constraint Propagation
Among the four types of primitive constraints (Section 2.2), the equality and in- equality constraints are easily defined as Herbrand equality and inequality, and appropriate implementations can be found in Prolog systems as, respectively, unification and the dif/2 inequality constraint. The constraints on the environ- ment and heap (membership and update of a mapping) on the other hand are specific to our purpose. We define them in terms of the following propagation rules, that allow us to infer additional constraints:
(o → o1) ∈ M ∧ (o → o2) ∈ M =⇒ o1 = o2
M1 ] {o → o1} = M2 =⇒ (o → o1) ∈ M2
o = o′ ∧ M1 ] {o → o1} = M2 ∧ (o′ → o2) ∈ M2 =⇒ (o′ → o2) ∈ M1
The above rules are easily implemented as Constraint Handling Rules (CHR) [9].
2.5 Search
In order to obtain concrete test cases, our constraint solver has to overcome two forms of non-determinism: 1) the non-determinism inherent to the extended op- erational semantics, and 2) the non-determinism associated to the selection of concrete values for the program’s input. Traditionally, in Constraint Program- ming a problem with non-deterministic choices is viewed as a (possibly infinite) tree, where each choice is represented as a fork in the tree. Each path from the root of the tree to a leaf represents a particular set of choices, and has zero or one solution. In our context, a solution is of course a concrete test case. As the tree does not imply a particular order on the solutions, we are free to choose any search strategy, which specifies how the tree is navigated in search of the solutions. Moreover, since the problem tree can be infinite, we may select an incomplete search strategy, i.e. one that only visits a finite part of the tree. Let us have a more detailed look at these two forms of non-determinism and how they can be handled by a solver.
Non-Deterministic semantics. Several of the language constructs have multiple overlapping rules in the definition of the symbolic semantics. In particular those for if-then-else ((IfThen) and (IfElse)) and while ((WhileT) and (WhileF)) constructs imply alternate execution paths through the program. Also, observe that the while-construct is a possible source of infinity in the problem tree as the latter must in general contain a branch for each possible number of iterations of the loop body. This means that a solver is usually forced to use an incomplete search strategy; for example a depth-bounded search strategy which does not explore the tree beyond a given depth. Recall the example in Section 2.1 where the while-loop may iterate an arbi- trary number of times. A depth-bounded search only considers test cases that involve iterations up to a given bound.
9
Non-Deterministic Values As the following example shows, even a single exe- cution path can introduce non-determinism in the solving process. Consider the program y := x.tail, which has only one execution path. This execution path merely restricts the initial environment and heap to E0 = {x ptr(A), y Vy} and (A cons(Vh, Vt)) ∈ H0. There are an infinite number of concrete test cases that satisfy these restrictions. Here are just a few:
E0 H0
{x ptr(a1), y nil} {a1 cons(0, nil)}
{x ptr(a1), y nil} {a1 cons(0, a1)}
{x ptr(a1), y nil} {a1 cons(1, nil)}
{x ptr(a1), y ptr(a1)} {a1 cons(0, nil)}
{x ptr(a1), y nil} {a1 cons(0, ptr(a2)), a2 cons(0, nil)}
There are two kinds of unknown values: unknown integer Vi and unknown
references Vr. Integers are easy: non-deterministically assign any natural number
to an unknown integer: ∨n∈N Vi = n.
For the references the story is more involved. Assume that R is the set of
references created so far, r′ is a fresh reference, and Vi′ and Vr′ are fresh unknown
integer and reference values. Then there are three assignments for an unknown
reference Vr: 1) nil, 2) one of the previous references R, or 3) a new reference
r′. In the last case, the heap must contain an additional cell with fresh unknown
components.
Vr = nil ∨ ( ∨ Vr = ptr(r)) ∨ (Vr = ptr(r′) ∧ (r′ → cons(Vi′, Vr′)) ∈ H0)
r∈R
In practice, we must again restrict ourselves to a finite number of alterna-
tives. We may be interested in only a single solution: an arbitrary one, one that
satisfies additional constraints or one that is minimal according to some cri-
terion. Alternatively, multiple solutions may be desired, each of which differs
sufficiently from the others based on some measure. All of these preferences can
be expressed in terms of suitable search strategies. For instance, the minimality
criterion is captured by a branch-and-bound optimization strategy.
2.6 Generalized Data Structures
So far we have only considered data structures composed of simple cons cells.
However, our constraint-based approach can easily be extended to cope with
arbitrary structures. Consider for instance this C-like struct for binary trees:
struct tree { int value;
tree left;
tree right; }
In order to deal with the tree type defined above, it suffices to extend both the
concrete and the constraint semantics of ImpL with 1) a new tree constructor
10
representing a triple and 2) three field selectors (e.g. value, left, and right) similar to the cons constructor and the head and tail selectors. In addition, the search process employed by the solver needs to be adjusted in order to generate arbitrary tree values. An unknown tree value Vt is assigned as follows:
Vt = nil ∨ ( ∨ Vt = ptr(r)) ∨ (Vr = r′ ∧ (r′ → tree(Vi′, Vl′, Vr′) ∈ H0)
r∈Rt
where Rt is the set of previously created tree references, r′ is a fresh tree ref- erence, and Vi′, Vl′ and Vr′ are respectively a fresh unknown integer value and fresh unknown tree values. It should be clear to the reader that the above ap- proach is easily generalized to arbitrary structures in a datatype-generic manner. Also, other primitive types such as reals and booleans are easily supported by integrating additional off-the-shelf constraint solvers for them. Moreover, note that invariants on the data structures, such as acyclicness, can be imposed on the unknown input in terms of additional constraints, e.g. provided by the programmer. This allows to seamlessly incorporate specification- level constraints into our method – similarly to [21, 18].
3 Applications
In this section we propose two applications of our method for test case gener- ation. The first one consists in providing the programmer with (a visualization of) input/output pairs for the program under test satisfying a certain coverage criterion. We have developed a tool that allows to visualise such input/output pairs involving heap-allocated data structures based on Graphviz.6 This allows the programmer to visually inspect them and verify that the program behaves as expected. For example, Fig. 6 depicts an input/output pair for the example program of Section 2.1. A second application is the automatic creation of a test suite that can be repeatedly evaluated during regression testing, for example after certain parts of the code have been refactored. The main problem is to translate the data structures originating from a solution to a constraint set into executable code that 1) creates the data structures that are input to the program, and that 2) verifies whether the data structures output by the code correspond to the expected output. Hence, a concrete test case for a program P looks like
Setup;P ;Check
where Setup sets up the initial environment and heap, and Check inspects the final environment and heap.
Example 1. Consider the simple program x := nil. One test configuration con- sists of an initial environment E0 = {x ptr(r1)} and an initial heap H0 = {r1 cons(7, ptr(r1))}. The final environment is E1 = {x nil} and the 6 http://www.graphviz.org/
11
x
0
0
x 0 (nil)
(a) Input (b) Output
Fig. 6. Visualization of an input/output pair for the example program
final heap H1 = H0. The concrete test case for this test configuration looks like the code represented on the left of Figure 7. After running this test case, the variable accept contains 1 iff the test succeeds; otherwise it contains 0.
// setup phase
x := new cons(7,nil);
x.tail := x;
// setup phase // program under test
x := new cons(7,nil); if (x == nil) then {
x.tail := x; foundnil := 1;
// program under test x := nil
x := nil; } else {
// check phase foundnil := 0;
if (x == nil) then { x := nil
accept := 1 }
} else { // check phase
accept := 0 if (x == nil) then {
} accept := 1
} else {
accept := 0
}
Fig. 7. Testcase for the original (left) and refactored (right) code of Example 1.
If the program is changed, e.g. due to refactoring, the existing test case can be used to test the modified source code (regression testing). If we replace the pro- gram of Example 1 above by the refactored version if (x == nil) { foundnil := 1; x := nil } else { foundnil := 0; x := nil }, the above test case
12
looks as the code on the right of Figure 7. Observe that we consider neither garbage, i.e. the parts of the heap H1 that are unreachable from the environ- ment E1, nor newly introduced variables such as foundnil in the example.
Setup Phase The inference rules depicted in Figure 8 explain how to construct the setup code of the test case from an initial environment E and heap H . The judgement H, ∅ `s E : s expresses that s is the setup code for environment E and heap H . The set of rules basically defines an algorithm that constructs the setup code by generating code for one element of the environment at a time. Note the role of the set A containing the references generated so far.
(S-Done) H, A `ₛ ∅ : skip
(S-Int) H, A `ₛ H, A `ₛ E : s
{l → n} ∪ E : l := n;s
(S-Nil) H, A `ₛ {l H, A `ˢ E : s
→ nil} ∪ E : l := nil;s
a ∈ domain(A) (a → cons(vₕ, vₜ, )) ∈ H
(S-NRef) H, A `ₛH, A ∪ {a → l} `ˢ {l.tail : vᵗ} ∪ E : s
{l → ptr(a)} ∪ E : l := new cons(vₕ, nil);s
(S-ORef) (a → l′) ∈ A H, A `ₛ E : s
H, A `ₛ {l → ptr(a)} ∪ E : l := l′;s
Fig. 8. Setup Phase Algorithm
Check Phase Likewise, the algorithm given by the inference rules in Figure 9 explains how to construct the check code of the test case from the final environ- ment E and heap H . The judgement H, ∅ `c E : s expresses that s is the setup code for environment E and heap H .
4 Ongoing Work
A large amount of work exists in the field of automatic test case generation for imperative programs. The arguably simplest method is random generation of test data [1, 7]. In symbolic evaluation techniques (e.g. [3, 14, 16]), the input parameters are replaced by symbolic values, in order to derive a symbolic expres- sion representing the values of a program’s variables. This approach is notably used in the ATGen tool for structural coverage of Spark ADA programs [15]. In so-called dynamic approaches, the program is actually executed on input data that is arbitrarily chosen from a given domain. The input data is then iteratively
13
(C-Done) H, A `c ∅ : accept := 1
(C-Int) H, A `c {l → n} ∪ E : H, A `ᶜ E : s
if l == n then s else accept := 0
(C-Nil) H, A `c {l → nil} ∪ E : H, A `ᶜ E : s
if l == nil then s else accept := 0
a ∈ domain(A) (a → cons(vₕ, vₜ, )) ∈ H
H, A ∪ {a → l} `c {l.head : vₕ, l.tail : vₜ} ∪ E : s₁
(C-NRef) H, A `c {l → ptr(a)} ∪l, s¹ `ⁿ range(A) : s²
E : if l /= nil then s₂ else accept := 0
(C-ORef) H, A `c {l → (a → l′) ∈ A H, A `c E : s
ptr(a)} ∪ E : if l == l′ then s else accept := 0
(N-Base) l, s `ₙ ∅ : s
(N-Rec) l, s `ₙ {l′} ∪ R : if l, s `ⁿ R : s′
/= l′ then s′ else accept := 0
Fig. 9. Check Phase Algorithm
refined to obtain a final test input such that the execution follows a chosen path, or reaches a chosen statement [13, 8]. Constraint-based test data generation was originally introduced in [6] in the context of mutation testing [5] and aims at transforming the automatic test data generation problem into a CLP problem over finite domains. This approach has been used in many works, including [11, 12]. It is also used in two different testing tools, Godzilla [17] and InKA [10]. The latter notably generates test data satisfying different criteria such as statement coverage, branches coverage and MC/DC7. In this paper, we have presented a constraint-based approach for generat- ing white-box test cases for a small but representative imperative programming language. Our technique is able to generate complex heap-allocated and pointer- based data structures without any user intervention. The selection of both execu- tion paths and concrete test inputs are modelled uniformly as a single constraint problem. An interesting advantage of our technique over most existing work is that we use parametrizable CP search strategies within the solver in order to express (coverage) criteria the generated test suites must satisfy. Our framework would therefore be able to generate test cases accordingly to any (coverage) criterion, instead of proposing a predefined set of built-in criteria. We have developed an initial prototype in SWI-Prolog, which is available at http://www.cs.kuleuven.be/~toms/Testing/ together with example pro- grams. As we’ve already said, Prolog’s advantage is that it provides most of the required constraints for free, and the missing ones are easily implemented in
7 Modified condition/decision coverage [2]
14
CHR. However, Prolog’s disadvantage is that depth-first search is built in, which makes experimenting with alternative search strategies hard – if not impossible. We are currently working on a new implementation of our approach within the Monadic Constraint Programming framework [19], which is an open frame- work for building complex search strategies as a composition of simpler ones. This system will enable us to investigate the exact relation between the use of particular search strategies for constraint solving and the generation of interest- ing sets of test cases according to different adequacy criteria.
References
D. L. Bird and C. U. Munoz. Automatic generation of random self-checking test cases. IBM Syst. J., 22(3):229–245, 1983.
J.J. Chilenski and S.P. Miller. Applicability of modified condition/decision cover- age to software testing. Software Engineering Journal, 9(5):193–200, Sep 1994.
L. A. Clarke. A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng., 2(3):215–222, 1976.
F. Degrave, T. Schrijvers, and W. Vanhoof. Automatic generation of test inputs for Mercury. In Logic-Based Program Synthesis and Transformation. Springer, 2008.
R.A. DeMillo. Test adequacy and program mutation. In Software Engineering,
- 11th International Conference on, pages 355–356, May 1989.
R.A. DeMillo and A.J. Offutt. Constraint-based automatic test data generation. Software Engineering, IEEE Transactions on, 17(9):900–910, Sep 1991.
J. W. Duran and Simeon C. Ntafos. An evaluation of random testing. IEEE Trans. Software Eng., 10(4):438–444, 1984.
Roger Ferguson and Bogdan Korel. The chaining approach for software test data generation. ACM Trans. Softw. Eng. Methodol., 5(1):63–86, 1996.
Thom Fr¨uhwirth. Theory and practice of Constraint Handling Rules. J. Logic Pro- gramming, Special Issue on Constraint Logic Programming, 37(1–3):95–138, 1998.
Arnaud Gotlieb, Bernard Botella, and Michel Rueher. Automatic test data genera- tion using constraint solving techniques. SIGSOFT Softw. Eng. Notes, 23(2):53–62,
Arnaud Gotlieb, Bernard Botella, and Michel Rueher. A clp framework for com- puting structural test data. In Proceedings of the First International Conference on Computational Logic, pages 399–413, London, UK, 2000. Springer-Verlag.
Arnaud Gotlieb, Tristan Denmat, and Bernard Botella. Goal-oriented test data generation for programs with pointer variables. Computer Software and Applica- tions Conference, Annual International, 1:449–454, 2005.
Neelam Gupta, Aditya P. Mathur, and Mary Lou Soffa. Automated test data generation using an iterative relaxation method. SIGSOFT Softw. Eng. Notes, 23(6):231–244, 1998.
James C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385–394, 1976.
C. Meudec. Atgen: automatic test data generation using constraint logic program- ming and symbolic executionatgen. Software Testing Verification and Reliability, 11(2):81–96, 2001.
Roger A. M¨uller, Christoph Lembeck, and Herbert Kuchen. A symbolic java virtual machine for test case generation. In IASTED Conf. on Software Engineering, pages 365–371, 2004.
15- A. Jefferson Offutt, Zhenyi Jin, and Jie Pan. The dynamic domain reduction procedure for test data generation: Design and algorithms. Software - Practice and Experience, 29:167–193, 1994.
- A. Jefferson Offutt and Shaoying Liu. Generating test data from sofl specifications. The Journal of Systems and Software, 49:49–62, 1999.
- Tom Schrijvers, Peter Stuckey, and Phil Wadler. Monadic Constraint Program- ming, 2009. http://www.cs.kuleuven.be/~toms/Haskell/.
- Nguyen Tran Sy and Y. Deville. Automatic test data generation for programs with integer and float variables. In Proceedings of ASE 01, 2001.
- W. Visser, C. S. P˘as˘areanu, and S. Khurshid. Test input generation with Java pathfinder. SIGSOFT Softw. Eng. Notes, 29(4):97–107, 2004.
A (For referees) Proof of Completeness Theorem
The proof of the completeness theorem of Section 2.4 results directly from the proofs of the following lemmas:
Lemma 1 Let E and H be an environment and a heap, and e an expression. If 〈E, H〉 e v〈E, H′〉, then if θ is a solution for a satisfiable set of constraints C1 such that 〈E, H〉 ∼ = 〈θ(Ev), θ(Hv)〉 for constraint variables Ev and Hv then there exists a satisfiable set of constraints C2 such that 〈Ev, Hv, C1〉 e vv〈Ev, Hv′ , C2〉 with θρ a solution for C2 such that 〈E, H′〉 ∼ = 〈θρ(Ev), θρ(Hv′ )〉 and v = θρ(vv) Proof. The proof is by induction on the structure of the expression e.
The base cases are Var, Int and Nil rules of the expressions. Since neither case updates the heap, we have H ′ = H . In the two last cases (Int and Nil), the proof is direct since those expressions do not imply any constraint on vv, Ev or Hv. That is, C2 = C1, Hv′ = Hv and vv = v. That means we can simply choose ρ = {} and we obtain a solution θρ for C2 verifying θρ(vv) = v and 〈θρ(Ev), θρ(Hv′ )〉 = 〈θ(Ev), θ(Hv)〉 ∼ = 〈E, H〉 = 〈E, H′〉. Moreover, for the Var case, we have vv = V with V a fresh variable and C2 ≡ C1 ∧ {(x → V ) ∈ Ev}. If we choose ρ = {V /E(x)}, we have θρ a solution for C2 such that 〈θρ(Ev), θρ(H ′ )〉 ∼ v = 〈E, H′〉. We arbitrarily choose the Head rule as single inductive case for the proof, for convenience. The proof for the other cases can easily be deducted from this one. Suppose 〈E, H〉e ptr(r)〈E, H2〉 and r → cons(vh, vt) ∈ H2. By induc- tion hypothesis, we have 〈Ev, Hv0, C0〉 e vv〈Ev, Hv1, C1〉 with a solution ρ1 such that 〈E, H2〉 ∼ = 〈ρ1(Ev), ρ1(Hv1〉 and ρ1(vv) = ptr(r). We can construct a solution ρ for C2 where C2 ≡ C1 ∧ v = ptr(R) ∧ (R → cons(Vh, Vt)) ∈ Hv1 as follows: ρ = ρ1 ∪ {R/r, Vt/vt, Vh/vh}. We can easily verify that ρ(Vh) = vh and 〈E, H2〉 ∼ = 〈ρ(Ev), ρ(Hv1)〉.
16
Lemma 2
Let E and H be an environment and a heap, and s an instruction manipulating
the variables in E. If 〈E, H〉 s 〈E′, H′〉, then if θ is a solution for a satisfiable
set of constraints C1 such that 〈E, H〉 ∼
= 〈θ(Ev), θ(Hv)〉 for constraint vari-
ables Ev and Hv then there exists a satisfiable set of constraints C2 such that
〈Ev, Hv, C1〉 s 〈Ev′ , Hv′ , C2〉 with θρ a solution for C2 such that
〈E′, H′〉 ∼
= 〈θρ(Ev′ ), θρ(Hv′ )〉
Proof. The proof is by induction on the structure of the statement s.
The base cases are the Skip, VarAss, HeadAss and TailAss rules; the prop-
erty is only proved for the VarAss rule, for convenience reasons. The proof for
the other cases can easily be deducted from this one.
Suppose 〈E, H1〉e v〈E, H2〉. From Lemma 1 we have 〈Ev0, Hv0, C0〉 e
vv〈Ev0, Hv1, C1〉 with a solution ρ1 such that 〈E, H2〉 ∼
= 〈ρ1(Ev), ρ1(Hv1〉 and
ρ1(vv) = v. We can construct a solution ρ for C1 ∧ Ev1 = Ev0 ] {x → vv} as
follows:
ρ = ρ1 ∪ {Ev1/Ev 0 ] {x → ρ1(vv)}}
We can easily verify that 〈E, H2〉 ∼
= 〈ρ(Ev), ρ(Hv1)〉.
We arbitrarily choose the Seq rule as single inductive case for the proof, for convenience reasons. The proof for the other cases can easily be deducted from this one. Suppose 〈E1, H1〉 s1 〈E2, H2〉 and 〈E2, H2〉 s2 〈E3, H3〉. By induction hy- pothesis, we have 〈Ev0, Hv0, C0〉 s1 〈Ev1, Hv1, C1〉 with a solution ρ1 such that 〈E2, H2〉 ∼ = 〈ρ1(Ev1), ρ1(Hv1〉. We also have 〈Ev1, Hv1, C1〉 s2 〈Ev2, Hv2, C2〉 with a solution ρ2 such that 〈E3, H3〉 ∼ (Ev2), ρ2(Hv2〉. We can construct a = 〈ρ2 solution θρ for C2 verifying the property as follows:
ρ = ρ 1ρ 2
We can directly notice that 〈E3, H3〉 ∼ (Ev2), ρ2(Hv2〉.
= 〈ρ 2
The soundness property can be proved in an analogous way.
17