We address the problem of constraint encoding explosion which hinders the applicability of state merging in symbolic execution. Specifically, our goal is to reduce the number of disjunctions and \emph{if-then-else} expressions introduced during state merging. The main idea is to dynamically partition the symbolic states into merging groups according to a similar uniform structure detected in their path constraints, which allows to efficiently encode the merged path constraint and memory using quantifiers. To address the added complexity of solving quantified constraints, we propose a specialized solving procedure that reduces the solving time in many cases. Our evaluation shows that our approach can lead to significant performance gains.

翻译：我们解决了约束编码爆炸问题，该问题阻碍了符号执行中状态合并的适用性。具体而言，我们的目标是减少状态合并过程中引入的析取与“if-then-else”表达式的数量。主要思路是根据路径约束中检测到的相似统一结构，将符号状态动态划分为合并组，从而能够利用量词高效编码合并后的路径约束和内存。为应对求解量化约束带来的额外复杂性，我们提出了一种专用求解过程，可在许多情况下减少求解时间。评估表明，我们的方法能够显著提升性能。