Transcript Document

272: Software Engineering
Fall 2012
Instructor: Tevfik Bultan
Lecture 8: Semi-automated test generation
via UDITA
Testing
•
It is widely acknowledged both in academia and industry that testing is crucial
•
Test driven development supported by testing tools such as Junit are very
popular in practice
•
However, tools like JUnit automate test execution they do not automate test
generation
•
In practice, test generation is still a manual activity
•
We have discussed several novel techniques for automated test generation:
– Bounded exhaustive test generation based on class invartiants (Korat)
– Random test generation that uses the methods in the program to
construct random method sequences in order to generate test cases
(Randoop)
– Dynamic symbolic execution (aka, concolic execution, CUTE, DART)
A Semi-automated Approach
• The UDITA approach is a semi-automated approach
• Let the user specify how the tests should be generated but provide
some support for automating the test generation process
• Basic idea: Allow the user to write a set of test cases using nondeterministic choice operators
– During test specification, the user can specify a range of values
instead of a particular input value
– During automated test generation, each value from that range will
be selected
• UDITA follows the bounded exhaustive testing approach
– It allows the user to guide the exhaustive exploration
UDITA
Contributions:
• A language that extends Java with non-deterministic choice primitives
• Lazy non-deterministic evaluation: During test generation the choices
made using the non-deterministic choice primitives are delayed until
they are first accessed
• Implementation of the UDITA approach on top of the JPF model
checker
• Demonstration of the efficiency of the proposed approach by
comparing with earlier approaches
Specification of tests
Two basic approaches for test generation:
Declarative (filtering) style
• Write predicates which specify what a valid test case is
– This is like the repOK methods from the KORAT approach
– Write a method that returns true if the input is a valid test case,
and false otherwise
– Generate all the inputs (within in a bound) for which the method
would return true
Imperative (generating) style
• Write generators which construct the test cases
– Can use non-determinism to define multiple test cases with one
method
UDITA primitives for test generation
UDITA provides a set of basic generators (these are the primitives that
introduce the non-determinism in the specifications)
• getInt(int lo, int hi): returns an integer between lo and hi inclusively
• getBoolean(): returns true or false
• getNew: returns an object that was not returned by any previous calls
and which is not null
• getAny: returns an object from the object pool (and optionally null)
UDITA provides an assume primitive
• assume: restricts the generated test cases to only the ones that
satisfy the assumption
UDITA provides an interface for encapsulating generators:
• IGenerator interface
Example Java Inheritence Graphs
class IG { Node[] nodes; int size;
static class Node {
Node[] supertypes;
boolean isClass; } }
Constraints:
• DAG (directed acyclic graph): The nodes in the graph should have no
directed cycle along the references of supertypes
• JavaInheritance: All supertypes of an interface are interfaces, and
each class has at most one supertype class
Goal: Generate Java programs based on Java inheritance graphs to test
programs that take Java programs as input (such as compilers,
refactoring tools, IDEs etc.)
Filtering approach for inheritance graphs
boolean isDAG(IG ig) {
Set<Node> visited = new HashSet<Node>();
Set<Node> path = new HashSet<Node>();
if (ig.nodes == null || ig.size != ig.nodes.length) return false;
for (Node n : ig.nodes)
if (!visited.contains(n))
if (!isAcyclic(n, path, visited)) return false;
return true; }
boolean isAcyclic(Node node, Set<Node> path, Set<Node> visited) {
if (path.contains(node)) return false;
path.add(node);
visited.add(node);
for (int i = 0; i < supertypes.length; i++) {
Node s = supertypes[i];
// two supertypes cannot be the same
for (int j = 0; j < i; j++)
if (s == supertypes[j]) return false;
// check property on every supertype of this node
if (!isAcyclic(s, path, visited)) return false;
}
path.remove(node);
return true; }
Filtering approach for inheritance graphs
boolean isJavaInheritance(IG ig) {
for (Node n : ig.nodes) {
boolean doesExtend = false;
for (Node s : n.supertypes)
if (s.isClass) {
// interface must not extend any class
if (!n.isClass) return false;
if (!doesExtend) { doesExtend = true;
// class must not extend more than one class
} else { return false; }
} } }
Generating approach for inheritance graphs
void generateDAGBackbone(IG ig) {
for (int i = 0; i < ig.nodes.length; i++) {
int num = getInt(0, i); // pick number of supertypes
ig.nodes[i].supertypes = new Node[num];
for (int j = 0, k = −1; j < num; j++) {
k = getInt(k + 1, i − (num − j));
// supertypes of ”i” can be only those ”k” generated before
ig.nodes[i].supertypes[j] = ig.nodes[k];
} } }
void generateJavaInheritance(IG ig) {
// not shown imperatively because it is complex:
// topologically sorts ”ig” to find what nodes
// can be classes or interfaces
}
Bounded exhaustive generation
IG initialize(int N) {
IG ig = new IG(); ig.size = N;
ObjectPool Node pool = new ObjectPool Node (N);
ig.nodes = new Node[N];
for (int i = 0; i < N; i++) ig.nodes[i] = pool.getNew();
for (Node n : nodes) {
// next 3 lines unnecessary when using generateDAGBackbone
int num = getInt(0, N − 1);
n.supertypes = new Node[num];
for (int j = 0; j < num; j++) n.supertypes[j] = pool.getAny();
// next line unnecessary when using generateJavaInheritance
n.isClass = getBoolean(); }
return ig; }
static void mainFilt(int N) {
IG ig = initialize(N);
assume(isDAG(ig));
assume(isJavaInheritance(ig));
println(ig); }
static void mainGen(int N) {
IG ig = initialize(N);
generateDAGBackbone(ig);
generateJavaInheritance(ig);
println(ig); }
Combining declarative and imperative styles
• In the inheritance graph generation
– DAG property is easier to specify using the imperative style
– Java inheritance property is easier to specify using the declarative
style
• In an UDITA generator, these styles can be combined
• This leads to more compact test specifications
Automated test case generation
• Given the generator specification, UDITA automatically generates test
cases using bounded-exhaustive test generation
• It uses JPF model checker to do this
– JPF model checker backtracks on all non-deterministic choices
• UDITA uses two techniques:
– Isomorphism avoidence
• It achieves this using the approach used in Korat by ordering
the generated objects
– Delayed execution
• Postpones the branching in the computation tree generated by
the program
– Do not make the non-deterministic choice until the
generated value is used
– There is no reason to execute the statements that do not
depend on a non-deterministic value for different choices
(since they do not depend on that choice)
Evaluation
• UDITA performed better than earlier bounded-exhaustive testing
approaches
– Delaying non-deterministic choices improves the run time
exponentially
– Test generation using JPF (which stores the visited states) is
more efficient than stateless test generation using a standard JVM
(which was the case for an earlier tool called ASTGen)
• UDITA found bugs in Eclipse and Java compilers
– Differential testing
• They generated test cases and ran both compilers to see if the
output differed
• This way they avoid the oracle specification problem, each
compiler serves as an oracle to the other compiler
• UDITA approach is more effective than dynamic symbolic execution
for generating test cases that require complex structures (like
generating programs as test cases for compilers)