Junior Submission
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 work, we propose a technique that avoids this expensive forking scheme by using a flat memory scheme instead, i.e. essentially merging all memory objects into one. To make this approach feasible, we use alias analysis to split the flat memory into multiple memory pools, and also implement a hybrid approach in which the flat memory and forking schemes co-exist. We evaluate our technique on a mix of synthetic benchmarks (which manipulate standard data structures such as matrices and hash tables) and real programs (such as m4 and make), and observe significant gains in terms of performance and memory usage, respectively.