This paper provides a different solution to the problem in coppa:ase:2017: how to handle symbolic addresses during symbolic execution. Forking (the default behaviour of KLEE) every time the pointer target could refer to multiple objects (“multi-resolution”) causes a path explosion while treating the entire memory as a single flat object is inefficient.
Their solution is to use a pointer analysis to partition all objects/pointers into equivalence classes of objects that may alias. A separate segment with its own memory management (including its own free list) is created for each equivalence class and allocation is performed in the appropriate segment. They allow for possible bugs in the pointer analysis by performing a search in each segment: the performance benefit comes from the fact that only one will hit (in the absence of bugs).
They evaluate on the Apache Portable Runtime (a sort of portability middleware layer), GNU m4, GNU make and SQLite. The new model is (significantly?) slower than standard KLEE on benchmarks that do not suffer from multiresolution. An alternative model that (aggressively?) merges paths is competitive with segmented memory but it times out on some of the benchmarks. They evaluate the impact of pointer analysis precision – sometimes it matters.