A memory model for KLEE that tackles the issue of symbolic dereference by leveraging static pointer alias analysis.

Overview

Symbolic execution is an effective technique for exploring paths in a program and reasoning about all possible values on those paths. However, the technique still struggles with code that uses complex heap data structures, in which a pointer is allowed to refer to more than one memory object. In such cases, symbolic execution typically forks execution into multiple states, one for each object to which the pointer could refer.

In this paper, we propose a technique that avoids this expensive forking by using a segmented memory model. In this model, memory is split into segments, so that each symbolic pointer refers to objects in a single segment. The size of the segments are bound by a threshold, in order to avoid expensive constraints. This results in a memory model where forking due to symbolic pointer dereferences is significantly reduced, often completely.

We evaluate our segmented memory model on a mix of whole program benchmarks (such as m4 and make) and library benchmarks (such as SQLite), and observe significant decreases in execution time and memory usage.

Artefact

The artefact page is available here.

Research Support

This research was supported in part by the UK EPSRC via grants EP/N007166/1,EP/L002795/1 and a PhD studentship.

Publications

  • A Segmented Memory Model for Symbolic Execution

    Timotej Kapus, Cristian Cadar

    European Software Engineering Conference / ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2019)