Symbolic Execution + Merging

Abstract

The Path explosion problem is a bane that haunts all symbolic execution engines. Too many programming constructs contribute to it, from the humble if statement to the noble fork statement. There are multiple methods to try and reduce it, heuristics for choosing paths, diagonalizing the search space of paths, pruning paths early, and the one we will be focusing on: State Merging.

In state merging the paths get fused back together at ‘join points’, but the merging of the states causes the final state to be bigger, to contain a disjunction within its premise, and as a result its not always a win. Often, its a loss, where the combined state is harder to solve for a SMT-solver than the separate states would’ve been. So again we are forced to use heuristics to decide whether we merge or not, or prune paths. Introducing State Merging without anything is not enough.

We extend state merging with abstraction, in the hope that this provides fruitful, but find that it does not. State merging in general performs quite a bit better than initially expected, however, even without the abstraction.