通过索引化算子扩展符号执行的覆盖范围

传统程序分析分析一种程序语言，即所有可用该语言编写的程序。然而，可编写的所有可能程序与用某语言编写的实际程序语料库之间存在差异。我们试图利用这一差异：对于给定的程序，我们应用定制程序变换 Indexify，将当前 SMT 求解器一般不能处理的表达式（如字符串上的约束）转换为它们可处理的等可满足表达式。为此，Indexify 将难以处理表达式中的算子替换为同态版本，这些版本在原始算子定义域的有限子集上行为相同，并在该子集外返回表示未知的 bottom。通过聚焦于对分析给定程序最有用的字面量与表达式，Indexify 构建了一个小的有限理论，扩展了求解器对目标程序所构造表达式的处理能力。Indexify 的定制性质必然意味着其评估必须是实验性的，依赖于实践中有效性的演示。我们开发了 Indexif}（原文如此）这一 Indexify 工具。我们通过对两个真实基准——coreutils 中的字符串表达式与 fdlibm53 中的浮点数——应用该工具来展示其效用与有效性。Indexify 将 coreutils 上的完成时间从 Klee 平均 49.5m 降至 6.0m。它将 coreutils 上的分支覆盖率从 Klee 的 30.10% 与 Zesti 的 14.79% 提升至 66.83%。在对 fdlibm53 中浮点数进行索引化时，Indexifyl（原文如此）将分支覆盖率较 Klee 从 34.45% 提升至 71.56%。对于一类受限输入，Indexify 允许对先前技术不可达的程序路径进行符号执行：它在 coreutils 中覆盖的分支数超过 Klee 的两倍。