“Symcrete” memory model with lazy initialization and objects of symbolic sizes in KLEE

Dynamic symbolic execution is a well-known technique for testing applications. It introduces symbolic variables – program data with no concrete value at the moment of instantiation – and uses them to systematically explore the execution paths in a program under analysis. However, not every value can be easily modelled as symbolic: for instance, some values may take values from restricted domains or have complex invariants, hard enough to model using existing logic theories, despite it is not a problem for concrete computations. In this paper, we propose an implementation of infrastructure for dealing with such “hard-to-be-modelled” values. We take the approach known as symcrete execution and implement its robust and scalable version in the well-known KLEE symbolic execution engine. We use this infrastructure to support the symbolic execution of LLVM programs with complex input data structures and input buffers with indeterminate sizes.