【发布时间】:2016-08-11 08:42:05
【问题描述】:
静态分析的实现和符号执行有什么区别?
【问题讨论】:
标签: validation testing static-analysis verification symbolic-execution
静态分析的实现和符号执行有什么区别?
【问题讨论】:
标签: validation testing static-analysis verification symbolic-execution
静态分析是检查代码并就代码质量提出意见的任何离线计算。您可以将其应用于源代码、Java/C#/... 虚拟机指令集的虚拟机代码,甚至二进制目标代码。没有“一个”静态分析(尽管经典的编译器控制和数据流经常作为 SA 的基础机制突出显示);该术语共同适用于可能离线使用的所有类型的机制。
符号执行是一种特殊的离线计算,它通过构建表示程序在各个点的状态的公式来计算程序实际执行的一些近似值。它被称为“符号”,因为近似值通常是某种涉及程序变量及其值的约束的公式。
静态分析可以使用符号执行并检查生成的公式。或者它可能会使用一些其他技术(正则表达式、经典编译器流分析......)或某种组合。但静态分析不一定要用符号执行。
符号执行可能仅用于显示计算的预期符号结果。这不是上述定义的静态分析,因为没有任何关于结果有多好的意见。或者,可以对公式进行分析,此时它成为静态分析的一部分。作为一个实际问题,可以使用其他程序分析技术来支持符号执行(“这个变量公式传播到变量 x 的哪个读取?”这个问题通常可以通过流分析得到很好的回答)。
您可能会坚持静态分析是对源代码的任何离线计算,此时符号执行只是一种特殊情况。我觉得这个定义没有帮助,因为它不能很好地区分用例。
【讨论】:
我真的很喜欢Julian Cohen's Contemporary Automatic Program Analysis talk 的这张幻灯片。简而言之,人们喜欢将程序分析分为静态分析和动态分析两大类。但是确实有广泛的程序分析技术,从静态到动态,从手动到全自动。符号执行是一种有趣的技术,介于静态和动态分析之间,通常作为一种全自动方法应用。
【讨论】: