# Presentation: 482782

## Symbolic Execution and Test-input Generation

- Willem Visser
- &
- Corina Pasareanu and Peter Mehlitz
- RIACS/Kestrel Technology/CSC
- NASA Ames Research Center
- wvisser@email.arc.nasa.gov

## Overview

- Motivation for Model Checking Programs
- Introduction to Java PathFinder
- Symbolic Execution
- Coverage based Test-input generation
- Conclusions

## Motivation

- Ariane 501

- Mars Polar Lander

- Software Errors can be very costly

## More Recently

**Software problem with Spirit**

## Model Checking

- OK

- Error trace

- or

- Finite-state model

- Temporal logic formula

- Model Checker

- 

- Line 5: ...
- Line 12: ...
- Line 15:...
- Line 21:...
- Line 25:...
- Line 27:...
-    ...
- Line 41:...
- Line 47:...

## The Dream

- Program

- Requirement

- Checker

- OK

- Error trace

- or

- void add(Object o) {
-  buffer[head] = o;
-  head = (head+1)%size;
- }
- Object take() {
-  ...
-  tail=(tail+1)%size;
-  return buffer[tail];
- }

- Property 1: ...
- Property 2: ...
- ...

## Overview

- Motivation for Model Checking Programs
- Introduction to Java PathFinder
- Symbolic Execution
- Coverage based Test-input generation
- Conclusions

## Java PathFinder (JPF)

## Demo

- “oldclassic.java”
- Simplified version of the deadlock encountered in the Remote Agent
- Fixing oldclassic!
- Or rather trying to fix...

## 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.
- Uses dynamic independence analysis to determine atomicity levels
- http://ase.arc.nasa.gov/jpf

## Example Annotations

**public** **static** **void** m(**int** N) {
**   ****int** x = 0; **int** y = 0;
**   ****while** (x < N) {
-      x++; y++;
-    }
**   ****while** (x != 0) {
-       x--; y--;
-    }
**   ****assert** (y == 0);
- }

- Verify.ignoreIf(N > 10);

## Overview

- Motivation for Model Checking Programs
- Introduction to Java PathFinder
- Symbolic Execution
- Coverage based Test-input generation
- Conclusions

## Concrete Execution Path (example)

- x = 1, y = 0
- 1 >? 0
- x = 1 + 0 = 1
- y = 1 – 0 = 1
- x = 1 – 1 = 0
- 0 – 1 >? 0

- int x, y;
- if (x > y) {
-     x = x + y;
-     y = x – y;
-     x = x – y;
-     if (x – y > 0)
-         assert(false);
- }

## Symbolic Execution Tree (example)

- x = X, y = Y

- int x, y;
- if (x > y) {
-     x = x + y;
-     y = x – y;
-     x = x – y;
-     if (x – y > 0)
-         assert(false);
- }

## 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

## 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

## 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;}
- }

## 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

## Algorithm (aliasing)

- when method execution accesses field fif (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 }

## Algorithm (illustration)

- consider executingnext = t.next;

## Implementation via Instrumentation

- program
-  instrumentation

- counterexample(s)/test suite
- [heap+constraint+thread scheduling]

**Implementation via Instrumentation**

- model
-  checking

- decision
-  procedure

-   instrumented      program

- correctness specification

- continue/
- backtrack

- state:

-   original      program

## Overview

- Motivation for Model Checking Programs
- Introduction to Java PathFinder
- Symbolic Execution
- Coverage based Test-input generation (TIG)
- Conclusions

## White- & Black-Box Testing

**void add(Object o) {**
** ****buffer[head] = o;**
** ****head = (head+1)%size;**
**}**
**Object take() {**
** ...**
** ****tail=(tail+1)%size;**
** ****return buffer[tail];**
**}**

**void add(Object o) {**
** ****buffer[head] = o;**
** ****head = (head+1)%size;**
**}**
**Object take() {**
** ...**
** ****tail=(tail+1)%size;**
** ****return buffer[tail];**
**}**

- Requirements
- Specification

- Input Generator

- Input Generator

- Oracle

- Oracle

_**Testing Criteria**_
**Coverage of**
**Specification & Code**

_**Testing Criteria**_
**Specification** **Coverage**

## White- & Black-Box Testing

- Functional Spec

**White- & Black-Box Testing**

**void add(Object o) {**
** ****buffer[head] = o;**
** ****head = (head+1)%size;**
**}**
**Object take() {**
** ...**
** ****tail=(tail+1)%size;**
** ****return buffer[tail];**
**}**

**void add(Object o) {**
** ****buffer[head] = o;**
** ****head = (head+1)%size;**
**}**
**Object take() {**
** ...**
** ****tail=(tail+1)%size;**
** ****return buffer[tail];**
**}**

- Input Generator

- Input Generator

- Oracle

- Oracle

_**Testing Criteria**_
**Coverage of**
**Specification & Code**

_**Testing Criteria**_
**Specification** **Coverage**

- Input Spec

## Model Checking & TIG

- OK

- Error trace

- or

- Executable Specification

- Property specifying
- coverage cannot be achieved

- Model Checker

- 

- Line 5: ...
- Line 12: ...
- Line 15:...
- Line 21:...
- Line 25:...
- Line 27:...
-    ...
- Line 41:...
- Line 47:...

- No test-input
- can achieve
- desired coverage

- Test-input to achieve coverage

## Test-Input Generation (TIG)with Symbolic Execution

*... **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?

- “... 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*

## White- & Black-Box Testingfor Complex Data

- Functional Spec

**White- & Black-Box Testing****for Complex Data**

**void add(Object o) {**
** ****buffer[head] = o;**
** ****head = (head+1)%size;**
**}**
**Object take() {**
** ...**
** ****tail=(tail+1)%size;**
** ****return buffer[tail];**
**}**

**void add(Object o) {**
** ****buffer[head] = o;**
** ****head = (head+1)%size;**
**}**
**Object take() {**
** ...**
** ****tail=(tail+1)%size;**
** ****return buffer[tail];**
**}**

- Input Generator

- Input Generator

- Oracle

- Oracle

_**Testing Criteria**_
**Coverage of**
**Input Specification & Code**

_**Testing Criteria**_
**Input Specification** **Coverage**

- Input Spec

**Class Invariant**
- Pre-condition to every method
*boolean repOk()*

- no runtime errors exist

## Red-Black Trees

- (1) The root is BLACK

- (2) Red nodes can only have black children

- (3) All paths from a node to its leaves contain the same
- number of black nodes.

**Self-balancing Binary Search Trees**
- Java *SortedMap* Implementation

- (4) Acyclic
- (5) Consistent Parents

- repOk(): conditions (1)-(5)

## 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;**
**}**

## 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

## 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

## Symbolic Execution of repOk()Example

**public** **static** **boolean** repOk(Entry e) {
**   ****if** (e == **null**)
**     ****return** **true**;
**   ****if** (e.color == RED)
**      ****return** false;
-    ...

## 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

## 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 -

## 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); ...**

## Symbolic Execution for white-box TIG

## 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.

## 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;**

## 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);...**

## Lazy Initialization from Partial Structures

**Partial structure satisfying **
**conservative_RepOk()**

**Solution that satisfies ****repOk()**

**Not a solution!**

- _Concretization_
- By lazy initialization of
- repOK()

## Black Box Results

| N | Time | Structs | CandidateStructures | Tests | delEnt%BC | fixD%BC | fixIns%BC |
| --- | --- | --- | --- | --- | --- | --- | --- |
| 1 | 3 | 1(1) | 5 | 2 | 18 | 0 | 6 |
| 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**

## White-box

| Time | Mem | CandidateStructures | Tests | delEnt%BC | fixD%BC | fixIns%BC |
| --- | --- | --- | --- | --- | --- | --- |
| 92 | 7.3 | 11062 | 11(53) | 86 | 100 | 88 |

## 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