增强约束解复用以改进符号执行

约束解复用是节省符号执行中约束求解时间的有效方法。大多数现有的复用方法基于约束的语法或语义等价性；例如，Green 框架能够通过将约束规范化为语法等价的范式，来复用具有不同表示但语义等价的约束。然而，语法/语义等价并非复用的必要条件——某些约束在语法或语义上并不等价，但其解仍具有复用潜力。现有方法无法识别和复用此类约束。在本文中，我们提出了 GreenTrie，这是 Green 框架的一个扩展，支持基于约束间逻辑蕴含关系的约束复用。GreenTrie 提供了一个名为 L-Trie 的组件，它将约束和解存储到 Trie 树中，并按约束的蕴含偏序图进行索引。L-Trie 能够对给定约束执行逻辑归约以及逻辑子集和超集查询，以检查先前已解约束的复用情况。我们报告了针对原始 Green 框架对 GreenTrie 进行的实验评估结果，表明我们的扩展实现了更好的约束求解结果复用，并显著节省了符号执行时间。