A set of semantic-preserving transformations that take advantage of contextual information collected during symbolic execution to speedup array operations.

Overview

Despite significant recent advances, the effectiveness of symbolic execution is limited when used to test complex, real-world software. One of the main scalability challenges is related to constraint solving: large applications and long exploration paths lead to complex constraints, often involving big arrays indexed by symbolic expressions.

In this paper, we propose a set of semantic-preserving transformations for array operations that take advantage of contextual information collected during symbolic execution. Our transformations lead to simpler encodings and hence better performance in constraint solving.

The results we obtain are encouraging: we show, through an extensive experimental analysis, that our transformations help to significantly improve the performance of symbolic execution in the presence of arrays. We also show that our transformations enable the analysis of new code, which would be otherwise out of reach for symbolic execution.

Download

KLEE-Array was integrated into the KLEE symbolic execution engine, via the --optimize-array option.

The original version of KLEE-Array is made available both as source tarball and in a binary form, pre-installed in a virtual machine. For more details, please visit the artifact replication page.

Research Support

This work was supported by the EPSRC through grants EP/N007166/1 and EP/L002795/1.

Publications

• Accelerating Array Constraints in Symbolic Execution

  David M. Perry, Andrea Mattavelli, Xiangyu Zhang, Cristian Cadar

  International Symposium on Software Testing and Analysis (ISSTA 2017)