可达性和符号执行

Question

现在我对符号执行(SE)和可达性分析(RA)感到困惑。据我所知，SE使用符号来执行一些代码，以到达具有分支条件的每个分支。RA可以用来找出每个分支的可达性，对吧？当使用RA时，我们可以提取每个分支的分支条件。如果是这样，它们之间的区别是什么？他们能迅速行动吗？它们都是静态分析吗？

谢谢你，夏娃

Answer 1

符号执行是不执行程序而完成的。因此，它是静态分析。

一个好的符号分析将计算每个程序点的路径条件。更好的一个将能够推理路径公式，以证明它是可行的(程序点是可到达的)或不是(程序点是死的)。

与编译代码的执行速度相比，符号执行往往相当慢。

Answer 2

可达性分析主要用于查看模型是否可以达到某种状态。然而，符号执行是一种静态分析技术(有时也是动态的，就像KLEE所做的那样)来查找程序/源代码中的所有路径。

Answer 3

符号执行不是静态的，它象征性地执行程序。出于对性能的考虑，像klee这样的符号执行工具在遇到分支时不能解决分支条件。它使用一种廉价的分析来查看它是否可能达到。当到达程序的出口时，它将尝试生成测试用例。如果从起点(主函数)到出口的收集的约束是可满足的，那么将给出一个测试用例，否则出口是不可达的。SE使用可达性分析来生成覆盖代码的测试用例。