Symbolic execution is a powerful program analysis technique which
allows executing programs with symbolic inputs. Modern symbolic
execution tools use a concrete modeling of object sizes, that does
not allow symbolic-size allocations. This leads to concretizations
and enforces the user to set the size of the input ahead of time, thus
potentially leading to loss of coverage during the analysis.
We present a bounded symbolic-size model in which the size
of an object can have a range of values limited by a user-specified
bound. Unfortunately, this model amplifies the problem of path
explosion, due to additional symbolic expressions representing sizes.
To cope with this problem, we propose an approach based on state
merging that reduces the forking by applying special treatment to
symbolic-size dependent loops.
In our evaluation on real-world benchmarks, we show that our
approach can lead in many cases to substantial gains in terms of
performance and coverage, and find previously unknown bugs.