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 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.

翻译：我们针对约束编码爆炸问题展开研究，该问题制约了符号执行中状态合并技术的应用可行性。具体而言，我们的目标是减少状态合并过程中引入的析取式与条件表达式数量。核心思路是根据路径约束中检测到的相似统一结构，将符号状态动态划分为合并组，从而能够使用量词对合并后的路径约束与内存进行高效编码。针对量化约束求解带来的额外复杂度，我们提出一种专用求解程序，可在多数情况下缩短求解时间。实验评估表明，该方法能实现显著的性能提升。