Transcript Explaining Errors and Generating Tests with JPF

Symbolic Execution
and
Test-input Generation
Willem Visser
&
Corina Pasareanu and Peter Mehlitz
RIACS/Kestrel Technology/CSC
NASA Ames Research Center
[email protected]
Overview
•
•
•
•
•
Motivation for Model Checking Programs
Introduction to Java PathFinder
Symbolic Execution
Coverage based Test-input generation
Conclusions
2
Motivation
Mars Polar Lander
Ariane 501
Software Errors can be very costly
3
More Recently
Software problem with Spirit
4
Model Checking
OK
Finite-state model
or
Model Checker
(F
W)
Temporal logic formula
Error trace
Line
Line
Line
Line
Line
Line
…
Line
Line
5: …
12: …
15:…
21:…
25:…
27:…
41:…
47:…
5
The Dream
void add(Object o) {
buffer[head] = o;
head = (head+1)%size;
}
Object take() {
…
tail=(tail+1)%size;
return buffer[tail];
}
OK
Program
Property 1: …
Property 2: …
…
or
Checker
Error trace
Requirement
6
Overview
•
•
•
•
•
Motivation for Model Checking Programs
Introduction to Java PathFinder
Symbolic Execution
Coverage based Test-input generation
Conclusions
7
Java PathFinder
(JPF)
Java Code
Bytecode
void add(Object o) {
buffer[head] = o;
head = (head+1)%size;
}
Object take() {
…
tail=(tail+1)%size;
return buffer[tail];
}
JAVAC
0:
1:
2:
5:
8:
9:
10:
iconst_0
istore_2
goto
#39
getstatic
aload_0
iload_2
aaload
JVM
Model
Checker
Special
JVM
8
Demo
• “oldclassic.java”
–Simplified version of the deadlock
encountered in the Remote Agent
notify
T1
signal
if (no_action)
wait();
signal();
T2
signal
notify
• Fixing oldclassic!
–Or rather trying to fix…
9
Key Points
• Models can be infinite state
– Unbounded objects, threads,…
– Depth-first state generation (explicit-state)
– Verification requires abstraction
• Handle full Java language
– mostly only for closed systems
– Cannot handle native code
• no input/output through GUIs, files, Networks, …
• must be modeled by java code instead
• Allows Nondeterministic Environments
– JPF traps special nondeterministic methods
• Checks for user-defined assertions, deadlock and LTL properties
• Incorporates a number of search strategies
– DFS, BFS, A*, Best-first, etc.
• http://ase.arc.nasa.gov/jpf
10
Example Annotations
• Thread making OS calls
If (Verify.randomBool())
Kernel.yieldCPU();
else
Kernel.deleteThread();
• Method returning 5 values
return Verify.random(4);
public static void m(int N) {
int x = 0; int y = 0;
Verify.ignoreIf(N > 10);
while (x < N) {
x++; y++;
}
while (x != 0) {
x--; y--;
}
assert (y == 0);
}
11
Overview
•
•
•
•
•
Motivation for Model Checking Programs
Introduction to Java PathFinder
Symbolic Execution
Coverage based Test-input generation
Conclusions
12
Concrete Execution Path
(example)
int x, y;
x = 1, y = 0
if (x > y) {
1 >? 0
x = x + y;
x=1+0=1
y = x – y;
y=1–0=1
x = x – y;
x=1–1=0
if (x – y > 0)
0 – 1 >? 0
assert(false);
}
13
Symbolic Execution Tree
(example)
int x, y;
x = X, y = Y
X >? Y
if (x > y) {
x = x + y;
[ X <= Y ] END
[X>Y]x=X+Y
y = x – y;
[X>Y]y=X+Y–Y=X
x = x – y;
[X>Y]x=X+Y–X=Y
if (x – y > 0)
assert(false);
[ X > Y ] Y - X >? 0
[ X > Y, Y – X <= 0 ] END
[ X > Y, Y – X > 0 ] END
}
14
Forward
Symbolic Execution
• technique for executing a program on symbolic input values
• explore program paths
– for each path, build a path condition
– check satisfiability of path condition
• state
– symbolic values of variables, path condition, and counter
• various applications
– test generation
– program verification
• traditional use
– programs with fixed number of int variables
15
Challenges in Generalizing
Symbolic Execution
• how to handle fields in dynamic structures?
• how to handle aliasing?
• how to generate tests?
– satisfy criteria
– satisfy precondition
– are in-equivalent
16
Example
class Node {
int elem;
Node next;
Node swapNode() {
if (next != null)
if (elem > next.elem) {
Node t = next;
next = t.next;
t.next = this;
return t;
}
return this;
}
NullPointerException
Input list
+ Constraint
none
null
?
E0
E0
E1
E0
E1
Output list
E0
none
null
E0
E1
E0
E1
null
?
E0 <= E1
E0
E1
E0 > E1
E1
E0
E0 > E1
E0 > E1
null
E1
E0
E1
E0
E0
?
}
E0
E1
?
E0 > E1
E1
17
Generalized
Symbolic Execution
• model checker generates and explores “symbolic”
execution tree
– path conditions are added at each branch point
• off-the-shelf decision procedures check path conditions
• model checker backtracks if not satisfiable
– non-determinism handles aliasing
• explore different heap configurations explicitly
– concurrency
• lazy initialization
– initializes program’s inputs on an “as-needed” basis
– no a priori bound on input sizes
• preconditions to initialize inputs only with valid values
18
Algorithm (aliasing)
• when method execution accesses field f
if (f is uninitialized) {
if (f is reference field of type T) {
non-deterministically initialize f to
 null
 a new object of class T (with uninitialized fields)
 an object created during prior field initialization (alias)
}
if (f is numeric/string field)
initialize f to a new symbolic value
}
19
Algorithm
(illustration)
consider executing
next = t.next;
next
E0
next
E1
t
Precondition: acyclic
list
next next
E0
E1
null
t
next
E0
next
E1
E0
next
t
E1
next
next
next
E0
E1
t
next
next
E1
t
?
t
next
E0
next
next
null
E0
E1
next
?
t
20
Implementation via
Instrumentation
decision
procedure
continue/
backtrack
original
program
program
instrumentation
instrumented
program
model
checking
state:
path condition (data)
heap configuration
thread scheduling
correctness
specification
counterexample(s)/test suite
[heap+constraint+thread scheduling]
21
Overview
•
•
•
•
•
Motivation for Model Checking Programs
Introduction to Java PathFinder
Symbolic Execution
Coverage based Test-input generation
Conclusions
22
White- & Black-Box Testing
Testing Criteria
Specification Coverage
void add(Object o) {
buffer[head] = o;
head = (head+1)%size;
}
Input Generator
Object take() {
…
tail=(tail+1)%size;
return buffer[tail];
}
Oracle
Requirements
Specification
Testing Criteria
Coverage of
Specification & Code
void add(Object o) {
buffer[head] = o;
head = (head+1)%size;
}
Input Generator
Object take() {
…
tail=(tail+1)%size;
return buffer[tail];
}
Oracle
23
White- & Black-Box Testing
Testing Criteria
Specification Coverage
void add(Object o) {
buffer[head] = o;
head = (head+1)%size;
}
Input Generator
Object take() {
…
tail=(tail+1)%size;
return buffer[tail];
}
Oracle
Acyclic Linked List
Input Spec
After removing the last element
the list is empty
Adding to a full list is not allowed
Testing Criteria
Coverage of
Input Generator
Specification & Code
Functional Spec
void add(Object o) {
buffer[head] = o;
head = (head+1)%size;
}
Object take() {
…
tail=(tail+1)%size;
return buffer[tail];
}
Oracle
24
Model Checking & TIG
No test-input
can achieve
desired coverage
OK
Executable
Specification
or
Model Checker
(F
W)
Property specifying
coverage cannot be achieved
Error trace
Line
Line
Line
Line
Line
Line
…
Line
Line
5: …
12: …
15:…
21:…
25:…
27:…
Test-input to
achieve 41:…
coverage
47:…
25
Test-Input Generation (TIG)
with Symbolic Execution
“… symbolic execution for testing programs is a more exploitable technique
in the short term than the more general one of program verification”
James King
CACM 19:7, 1976
• … is it still true?
• White-box versus black-box
– Symbolic execution most often white-box
• Simple data is straightforward
• Complex data
– Black-box is (reasonably) straightforward – Korat (ISSTA’02)
– White-box?
26
White- & Black-Box Testing
for Complex Data
Testing Criteria
Input Specification
Coverage
void add(Object o) {
buffer[head] = o;
head = (head+1)%size;
}
Input Generator
Class Invariant
Pre-condition to every method
Object take() {
…
tail=(tail+1)%size;
return buffer[tail];
}
Input
Spec
Functional
Spec
Oracle
no runtime errors
exist
boolean repOk()
void add(Object o) {
buffer[head] = o;
head = (head+1)%size;
}
Input Generator
Testing Criteria
Coverage of
Input Specification & Code
Object take() {
…
tail=(tail+1)%size;
return buffer[tail];
}
Oracle
27
Red-Black Trees
Self-balancing Binary Search Trees
Java SortedMap Implementation
repOk(): conditions (1)-(5)
(3) All paths from a node to
its leaves contain the same
number of black nodes.
(1) The root is BLACK
(2) Red nodes can only
have black children
(4) Acyclic
(5) Consistent Parents
28
repOk() Fragment
boolean repOk(Entry e) {
// root has no parent, root is black,…
// RedHasOnlyBlackChildren
workList = new LinkedList();
workList.add(e);
while (!workList.isEmpty()) {
Entry current=(Entry)workList.removeFirst();
Entry cl = current.left;
Entry cr = current.right;
if (current.color == RED) {
if(cl != null && cl.color == RED) return false;
if(cr != null && cr.color == RED) return false;
}
if (cl != null) workList.add(cl);
if (cr != null) workList.add(cr);
}
// equal number of black nodes on left and right sub-tree…
return true;
}
29
Black-box TIG
• Generate inputs based on analysis of input structure
– e.g. Rover plan generation, Korat
• 100% “coverage” of input structures up to a predetermined
upper-bound
– e.g. all red-black trees with 6 or less nodes
• Complex data requires that only valid structures be considered
– Use class invariant to reduce number of input structures to consider
• a predicate characterizing all the instances of a class
• boolean repOk()
• Check code coverage using generated structures as input
• Advantage – test code for which no source is available
30
Symbolic execution for
black-box TIG
• Symbolic execution of repOk()
– Generate new structures only when repOk() returns true
– Limit the size of the structures generated
– Only correct structures will be generated
• repOk() returns true after all nodes in the tree have been
visited, hence they must all be concrete
• symbolic (partial) structures can fail repOk()
• Similar to Korat
– Except we can also deal with data constraints
31
Symbolic Execution of repOk()
Example
public static boolean repOk(Entry e) {
if (e == null)
return true;
if (e.color == RED)
return false;
…
32
White-box TIG
• Consider code coverage criterion when generating
test inputs
• Challenge
– Treating complex data with symbolic execution
• Use repOk() as a method precondition during
symbolic execution of source code:
– use repOk() to convert “symbolic” input structures into
concrete structures that cover the code and pass repOk()
– use repOk() also to eliminate “symbolic” structures during
lazy initialization, thus reducing the search space
33
repOk() x 2
abstract and concrete
Symbolic Execution of Code
During Lazy Initialization
check Abstract repOK()
When coverage is achieved,
solve the symbolic constraints
to create concrete inputs
To concretize inputs
by symbolic execution of
Concrete repOk()
over symbolic structures
- as with Black-box TIG -
34
White-box TIG: cover branches in
deleteEntry(Entry p)
/* precondition: p.repOk() */
private void deleteEntry(Entry p) {
if (p.left != null && p.right != null) {
Entry s = successor(p);
swapPosition(s, p);
}
Entry replacement = (p.left != null ? p.left : p.right);
if (replacement != null) {
replacement.parent = p.parent;
if (p.parent == null)
root = replacement;
else if (p == p.parent.left) {
p.parent.left = replacement;
}
else
p.parent.right = replacement;
p.left = p.right = p.parent = null;
if (p.color == BLACK)
fixAfterDeletion(replacement); ...
35
Symbolic Execution for
white-box TIG
Symbolic structure
before executing
branch
if (p.left != null && p.right != null) { ...
Symbolic structure(s)
that cover
the branch
This structure “passes”
the abstract repOk()
Concretize
Concrete structure
that will cover the
code
The symbolic structure
is used as input to
repOk() and lazily
executed to obtain the
concrete structure
36
Conservative repOk()
• Used to eliminate symbolic structures that cannot be converted
to a concrete structure that satisfy repOk() and therefore do not
describe valid inputs
• Because of symbolic structures we use abstraction
– conservative_RepOk() can return TRUE, FALSE or Don’t Know
• if FALSE, ignore that structure by backtracking
• if TRUE or Don’t Know, continue ...
• Example: (2) Red nodes have only black children.
FALSE
TRUE
Don’t Know
37
Conservative repOk()
// root has no parent, root is black,…
// RedHasOnlyBlackChildren
workList = new LinkedList();
workList.add(e);
while (!workList.isEmpty()) {
Entry current=(Entry)workList.removeFirst();
Entry cl = current.left;
Entry cr = current.right;
if (current.color == RED) {
if(current._left_is_initialized && cl != null && cl.color == RED) return false;
if(current._right_is_initialized && cr != null && cr.color == RED) return false;
}
if (current._left_is_initialized && cl != null) workList.add(cl);
if (current._right_is_initialized && cr != null) workList.add(cr);
}
// equal number of black nodes on left and right sub-tree…
return true;
38
Cover branches in
deleteEntry(Entry p)
/* precondition: p.repOk() */
private void deleteEntry(Entry p) {
if (p.left != null && p.right != null) {
Entry s = successor(p);
swapPosition(s, p);
}
Entry replacement = (p.left != null ? p.left : p.right);
if (replacement != null) {
replacement.parent = p.parent;
if (p.parent == null)
root = replacement;
else if (p == p.parent.left) {
p.parent.left = replacement;
}
else
p.parent.right = replacement;
p.left = p.right = p.parent = null;
if (p.color == BLACK)
fixAfterDeletion(replacement);...
39
Lazy Initialization from
Partial Structures
Partial structure satisfying
conservative_RepOk()
Concretization
By lazy initialization of
repOK()
Solution that satisfies repOk()
Not a solution!
40
Black Box Results
N Time Structs
Candidate
Structures
Tests delEnt
%BC
2
18
fixD
%BC
0
fixIns
%BC
6
1
3
1(1)
5
2
3.2
3(2)
24
8
68
5
6
3
5.5
5(2)
103
16
72
50
88
4
15
9(4)
432
36
86
90
88
5
60
17(6)
1830
84
86
100
88
6
292
33(16)
7942
196
86
100
88
Size 7: Korat 256753 candidates vs 35804
41
White-box
Time Mem
92
7.3
Candidate
Structures
11062
Tests
delEnt
%BC
11(53)
86
fixD
%BC
100
fixIns
%BC
88
42
Conclusions
• Other JPF features
– Partial-order reductions
– Observations
• Test-input Generation
– Examples with primitive data as well as complex data
– Make link with Shape Analysis
• Derive conservative repOk() from concrete repOk() automatically
• Symbolic Execution
– Invariant generation
• Combining Test-input generation and runtime
monitoring
– X9 testing framework for a next generation Mars Rover
43