实现静态分析和符号执行的区别是什么？
2个回答
7
我非常喜欢Julian Cohen's Contemporary Automatic Program Analysis talk中的这个幻灯片。简而言之，人们喜欢将程序分析分为静态和动态两大类。但实际上，从静态到动态、从手动到完全自动化，存在着广泛的程序分析技术谱系。符号执行是一种有趣的技术，介于静态和动态分析之间，并通常作为完全自动化方法应用。
- Ben Holland
3
1谢谢。你知道静态分析（例如编译器）可以检测到哪些错误，而符号执行无法检测到的吗？ - undefined
很难说（尤其是在评论中）。静态分析处理路径可行性问题，而动态分析更倾向于处理路径覆盖。符号分析介于两者之间，并通过逻辑地在分支处进行分析并求解一组可满足的约束来处理状态空间爆炸。我见过的大多数实现在SAT/SMT求解器上花费了大量的处理时间。这也很难回答，因为许多实现是技术的综合。例如，静态分析可以是完全自动的。 - undefined
我在这个链接上创建了一个关于此的新问题：http://stackoverflow.com/questions/38540082/error-detection-in-static-analysis-and-symbolic-execution - undefined
4
静态分析是指对代码进行离线计算，以评估代码质量的任何计算过程。它可以应用于源代码、Java/C#等虚拟机代码或虚拟机指令集，甚至二进制目标代码。没有“一种”静态分析方法（尽管经典编译器控制和数据流通常作为SA的基础机制），该术语集体适用于可能在离线使用的所有类型的机制。
符号执行是一种特定类型的离线计算，通过构建表示程序状态的公式来计算程序实际执行的某种近似值。之所以称其为“符号”，是因为该近似值通常是涉及程序变量及其值约束的某种公式。
静态分析可能会使用符号执行并检查生成的公式。或者它可能使用其他技术（正则表达式、经典编译器流分析等）或某种组合。但静态分析不一定要使用符号执行。
符号执行可能仅用于显示计算的预期符号结果。根据上述定义，这不是静态分析，因为没有形成关于该结果好坏的意见。或者，该公式可能会接受分析，此时它成为静态分析的一部分。从实际角度出发，人们可能使用其他程序分析技术来支持符号执行（“变量的此公式是否传递到读取变量x的哪些位置？”通常由流分析很好地回答）。
您可以坚持认为静态分析是对源代码进行的任何离线计算，此时符号执行只是一个特例。我不认为这个定义有用，因为它不能很好地区分使用情况。
符号执行是一种特定类型的离线计算，通过构建表示程序状态的公式来计算程序实际执行的某种近似值。之所以称其为“符号”，是因为该近似值通常是涉及程序变量及其值约束的某种公式。
静态分析可能会使用符号执行并检查生成的公式。或者它可能使用其他技术（正则表达式、经典编译器流分析等）或某种组合。但静态分析不一定要使用符号执行。
符号执行可能仅用于显示计算的预期符号结果。根据上述定义，这不是静态分析，因为没有形成关于该结果好坏的意见。或者，该公式可能会接受分析，此时它成为静态分析的一部分。从实际角度出发，人们可能使用其他程序分析技术来支持符号执行（“变量的此公式是否传递到读取变量x的哪些位置？”通常由流分析很好地回答）。
您可以坚持认为静态分析是对源代码进行的任何离线计算，此时符号执行只是一个特例。我不认为这个定义有用，因为它不能很好地区分使用情况。
- Ira Baxter
12
一般情况下，哪种实现方式耗时较少？谢谢。 - undefined
哪个花费的时间较少？这与实施的努力无关。你选择一种技术/架构来实现一个目标，从你所拥有的选择中选择。但是如果没有明确的目标陈述，你就无法确定哪种方法更合理。如果你没有具体的目标并且想要做最少的工作，那么你只需什么都不做。 - undefined
现在，您可能已经有一个具体的任务想法。您将发现，无论您想使用哪种技术，都需要很长时间才能从零开始构建。如果您想实现您的目标，您应该以一种整洁地集成所需的技术的方式，这样您就可以专注于调整它们来解决您的特定问题。我的经验是，大多数情况下您无法找到这些技术的完美组合，因此我着手解决了这个问题。请参阅http://www.semdesigns.com/Products/DMS/LifeAfterParsing.html - undefined
我之所以这么说是因为我的时间有限。当我阅读关于静态分析的文章时，例如http://modeling-languages.com/anatlyzer-static-analysis-atl-transformations-uncover-errors/链接，并将其与你在http://stackoverflow.com/questions/39490607/implement-symbolic-execution-without-model-checking/39493738?noredirect=1#comment66515194_39493738中所说的进行比较，我发现了一些相似之处，例如它们都使用了抽象语法树。从实现和技术使用的角度来看（而不是目标），对于它们之间的确切区别还不清楚。 - undefined
如果你真的想要验证前/后置条件，你可能需要考虑定理证明（这就是术语的来源）。定理证明与符号执行有很多相似之处，因为你正在构建关于程序状态的公式，但它也涉及到证明定理，实际上相当困难。但是符号执行将为你提供程序状态沿着特定路径（如果你对所有路径都进行符号执行的话，可能是所有路径）的公式，现在你有了可以与后置条件进行匹配的东西。你没有回答过你是否阅读过《解析之后的生活》这本书的问题。 - undefined
显示剩余7条评论
网页内容由stack overflow 提供, 点击上面的可以查看英文原文，
原文链接
原文链接