# Presentation: 101662

## Symbolic Execution with Abstract Subsumption Checking

- Saswat Anand
*College of Computing, Georgia Institute of Technology*
- Corina Păsăreanu
*QSS, NASA Ames Research Center*
- Willem Visser
*RIACS/USRA, NASA Ames Research Center*

## Introduction

- Goal
- Error detection in programs with complex input data structures
- Unbounded state space
- Approaches
- Model checking with (predicate) abstraction, shape analysis
- Over-approximations of program behavior
- Preserve true results; reported errors may be spurious
- Our approach
- Symbolic execution and model checking (TACAS’03)
- Contribution
- State matching to limit the searched state space
- Subsumption checking for symbolic states
- Abstractions to further reduce the searched state space
- Under-approximations of program behavior
- Preserve errors of safety properties; explore only feasible behaviors

## Symbolic Execution

- Analysis of programs with unspecified inputs
- Execute a program on symbolic inputs
- Symbolic states represent sets of concrete states
- For each path, build a path condition
- Condition on inputs – for the execution to follow that path
- Check path condition satisfiability – explore only feasible paths
- Symbolic state
- Symbolic values/expressions for variables
- Path condition
- Program counter

**Notes:**
Say we use Omega lib

## Example – Explicit Execution

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

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

**Concrete Execution Path**

**Code that swaps 2 integers**

**Example – Explicit Execution**

## Example – Symbolic Execution

- [PC:true]x = X,y = Y

- [PC:true] X > Y ?

- [PC:X>Y]y = X+Y–Y = X

- [PC:X>Y]Y>X ?

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

**Code that swaps 2 integers**

**Symbolic Execution Tree**

- [PC:X≤Y]END

- [PC:X>Y]x= X+Y

- false

- true

- [PC:X>YY≤X]END

- [PC:X>YY>X]END

- false

- true

**Example – Symbolic Execution**

**Notes:**
Say what PC represents: precondition for the inputs to follow a particular path

## Handles
Dynamically allocated data structures, arrays
Preconditions, concurrency
Lazy initialization for arrays and structures
Java PathFinder (JPF) model checker used
To generate and explore the symbolic execution tree
Implementation via instrumentation
Programs instrumented to enable JPF to perform symbolic execution
Omega library used to check satisfiability of numeric path conditions – for linear integer constraints

- Dynamically allocated data structures, arrays
- Preconditions, concurrency
- Lazy initialization for arrays and structures
- Java PathFinder (JPF) model checker used
- To generate and explore the symbolic execution tree
- Implementation via instrumentation
- Programs instrumented to enable JPF to perform symbolic execution
- Omega library used to check satisfiability of numeric path conditions – for linear integer constraints

**Generalized Symbolic Execution**

**Notes:**
Say we use omega library

## Symbolic Execution with Lazy Initialization

**Code**

**class** Node {
-    **int** elem;
-    **Node** next;
-    **Node** find(**int** v) {
-        Node n = this;
-        **while** (n != null) {
-            **if **(n.elem > v)
-              ** ****return** n;
-            n = n.next;
-        }
-        **return** null;
-    } }

**Notes:**
Segment of the list pointed to by n is  not yet initialized.

Say that first config represents all possible concrete lists that have at least one non-null element such that n points to the head of the list.

Branching: nondet choice introduced to build path condition or to handle aliasing for lazy initialization.

## State Matching

- Symbolic state
- Represents a set of concrete states
- State matching
- Subsumption checking between symbolic states
- 		Symbolic state S1 is subsumed by symbolic state S2 iff
- 		set of concrete states represented by S1 
- 		set of concrete states represented by S2
- Model checking
- Examine if a symbolic state is subsumed by previously stored symbolic state
- Continue or backtrack
- Method handles
- Un-initialized data structures (lists, trees), arrays
- Numeric constraints

## Symbolic State

- E1

- E2

- E3

- E4

- E1 > E2 
- E2 > E3 
- E2 < E4 
- E1 > E4

- Heap Configuration

- Numeric Constraints

- left

- left

- right

- right

**Notes:**
Say what concrete trees it represents

## Subsumption for Symbolic States

- Two steps (same program counter):
- Subsumption checking for heap configurations
- Obtained through DFS traversal of “rooted” heap configurations
- Roots are program variables pointing to the heap
- Unique labeling for “matched” nodes
- Considers only the heap shape, ignores numeric data
- Subsumption checking for numeric constraints
- Heap subsumption is only a pre-requisite of state subsumption
- Check logical implication between numeric constraints
- Existential quantifier elimination to “normalize” the constraints
- Uses Omega library

**Notes:**
Same program counter

## Subsumption for Heap Configurations 

****

- left

- left

- left

- right

- right

- right

- root

- root

- right

- right

- left

- left

**Notes:**
More general (represents more concrete heap configurations).

Blob – used as a wildcard

## Subsumption for Numeric Constraints

- E1

- E2

- E3

- E4

- E1 > E2 
- E2 > E3 
- E2 ≤ E4 
- E1 > E4

- E1

- E2

- E3

- E4

- Stored state:

- New state:

****

- Set of concrete
- states represented
- by stored state

- Set of concrete
- states represented
- by new state

****

****

- E1 > E2 
- E2 > E3 
- E2 < E4 
- E1 > E4

- 1:

- 2:

- 4:

- 3:

- 1:

- 2:

- 3:

- 4:

**Notes:**
We handle only integer constraints

## Subsumption for Numeric Constraints

- E1:V1

- E2:V4

- E3:V3

- E4:V5

- V2

- _Valuation:_
- E1 = V1  E2 = V4  E3 = V3  E4 = V5
- _PC:_
- V1 < V2  V4 > V3  V4 < V1  V4 < V5  V6 < V2  V7 > V2

- Existential Quantifier Elimination

- 1:

- 2:

- 3:

- 4:

- V6

- V7

**Notes:**
More tricks to implement subsumption – we can discuss off-line

Intuitively – we are only interested in the relative order of elements stored in matched nodes 

## Abstract Subsumption

- Symbolic execution with subsumption checking
- Not enough to ensure termination
- An infinite number of symbolic states
- Our solution
- Abstraction
- Store abstract versions of explored symbolic states
- Subsumption checking to determine if an abstract state is re-visited
- Decide if the search should continue or backtrack
- Enables analysis of under-approximation of program behavior
- Preserves errors to safety properties
- Automated support for two abstractions:
- Shape abstraction for singly linked lists
- Shape abstraction for arrays

## Abstractions for Lists and Arrays

- Shape abstraction for singly linked lists
- Summarize contiguous list elements not pointed to by program variables into summary nodes
- Valuation of a summary node
- Union of valuations of summarized nodes
- Subsumption checking between abstracted states
- Same algorithm as subsumption checking for symbolic states
- Treat summary node as an “ordinary” node
- Abstraction for arrays
- Represent array as a singly linked list
- Abstraction similar to shape abstraction for linked lists

## Abstraction for Lists

- E1 = V0  (E2 = V1  E2 = V2)  E3 = V3
- PC:  V0 ≤ v  V1 ≤ v  V2 ≤ v

****

- Symbolic states

- Abstracted states

**2:**

**3:**

**1:**

**1:**

**2:**

**3:**

- PC:  V0 ≤ v  V1 ≤ v

- PC:  V0 ≤ v  V1 ≤ v  V2 ≤ v

- E1 = V0  E2 = V1   E3 = V2
- PC:  V0 ≤ v  V1 ≤ v

**Unmatched!**

**Notes:**
From the list example that I showed before

## Experience

- Implementation
- Subsumption checking
- Shape abstractions for singly linked lists and arrays
- Error detection in Java programs
- List partition: 10 step counterexample
- Array partition: 30 step counterexample
- Analyzed corrected programs
- Abstraction effective in limiting the state space

## Related Work

- Under-approximation based abstraction for property falsification
- Ball et al. [CAV’05]
- Our previous work
- Choice free search [TACAS’01]
- Concrete model checking with abstract matching and refinement [CAV’05]
- Model driven software verification
- Use abstraction mappings during concrete model checking – Holzmann and Joshi [SPIN’04]
- Symbolic execution
- [King’76], Symstra [TACAS’05]
- Shape analysis
- TVLA, ...

## Conclusion and Future Work

- Symbolic execution with subsumption checking
- Explores only feasible program behavior
- Handles heap structures and arrays
- Abstractions for lists and arrays
- Explore an under-approximation of feasible behavior
- Complementary to over-approximation based abstraction
- Implementation
- Uses Java PathFinder model checker
- Applied for error detection in Java programs
- Future Work
- Investigate other shape abstractions, combine with predicate abstraction
- Test input generation, property verification (rather than refutation)
- Automatic abstraction refinement, compositional analysis

**Notes:**
Still fairly preliminary work

Not necessarily finite (because of the  numeric constraints)