【问题标题】:Static analysis vs. symbolic execution in implementation静态分析与实现中的符号执行
【发布时间】:2016-08-11 08:42:05
【问题描述】:

静态分析的实现和符号执行有什么区别?

【问题讨论】:

    标签: validation testing static-analysis verification symbolic-execution


    【解决方案1】:

    静态分析是检查代码并就代码质量提出意见的任何离线计算。您可以将其应用于源代码、Java/C#/... 虚拟机指令集的虚拟机代码,甚至二进制目标代码。没有“一个”静态分析(尽管经典的编译器控制和数据流经常作为 SA 的基础机制突出显示);该术语共同适用于可能离线使用的所有类型的机制。

    符号执行是一种特殊的离线计算,它通过构建表示程序在各个点的状态的公式来计算程序实际执行的一些近似值。它被称为“符号”,因为近似值通常是某种涉及程序变量及其值的约束的公式。

    静态分析可以使用符号执行并检查生成的公式。或者它可能会使用一些其他技术(正则表达式、经典编译器流分析......)或某种组合。但静态分析不一定要用符号执行。

    符号执行可能仅用于显示计算的预期符号结果。这不是上述定义的静态分析,因为没有任何关于结果有多好的意见。或者,可以对公式进行分析,此时它成为静态分析的一部分。作为一个实际问题,可以使用其他程序分析技术来支持符号执行(“这个变量公式传播到变量 x 的哪个读取?”这个问题通常可以通过流分析得到很好的回答)。

    您可能会坚持静态分析是对源代码的任何离线计算,此时符号执行只是一种特殊情况。我觉得这个定义没有帮助,因为它不能很好地区分用例。

    【讨论】:

    • 谢谢。一般来说,哪种实现方式耗时较少?
    • "哪个更省时?"这与实施的努力无关。您从您拥有的一组选择中选择一种技术/架构来实现一个目的。但如果没有具体的目的陈述,你就无法对其中哪个更明智进行排名。如果你没有特定的目的,想要做最少的工作,你就什么也不做。
    • 现在,您可能有一个特定的任务。您会发现,无论您想使用这些技术中的哪一种,它们都需要大量时间从头开始构建。如果你想实现你的目的,你应该做的是以一种巧妙集成的方式获得你需要的技术,这样你就可以专注于调整它们来解决你的特定问题。我的经验是,您通常无法同时找到这些,因此我着手解决该问题。见semdesigns.com/Products/DMS/LifeAfterParsing.html
    • 我这么说是因为我的时间有限。当我阅读有关静态分析的文章时,例如 modeling-languages.com/… 链接并将其与您在 stackoverflow.com/questions/39490607/… 中所说的进行比较,我发现了一些相似之处,例如它们都使用抽象语法树。从实施和使用的技术(不是目标)方面来看,这对我来说并不清楚它们之间的确切区别。
    • 您最好的选择是利用社区中其他人痛苦地获得的理解和经验。抽象语法树是一个好主意,但不管你信不信,以大多数人的方式做这件事会增加复杂性,如果您不希望“抽象”部分创建 ,则需要从具体语法树派生抽象语法树更多 工作。见stackoverflow.com/a/1916687/120163。但是到目前为止,树木是容易的部分。解析后的生活告诉你在实践中需要什么,如果你想尊重你的时间有限的事实。否则你会彻底改造这一切,很糟糕。
    【解决方案2】:

    我真的很喜欢Julian Cohen's Contemporary Automatic Program Analysis talk 的这张幻灯片。简而言之,人们喜欢将程序分析分为静态分析和动态分析两大类。但是确实有广泛的程序分析技术,从静态到动态,从手动到全自动。符号执行是一种有趣的技术,介于静态和动态分析之间,通常作为一种全自动方法应用。

    【讨论】:

    • 谢谢。您知道静态分析(例如编译器)可以检测到哪些错误,而符号执行无法检测到吗?
    • 很难说(尤其是在评论中)。静态分析处理路径可行性问题,而动态分析倾向于处理路径覆盖问题。符号分析介于两者之间,通过在分支上逻辑分叉分析并求解一组可满足的约束来处理状态空间爆炸。我见过的大多数实现都在 SAT/SMT 求解器中花费了大量的处理时间。这也很难回答,因为许多实现都是技术的混合。例如,静态分析可以是全自动的。
    • 我在这个链接中创建了新的问题:stackoverflow.com/questions/38540082/…
    猜你喜欢
    • 1970-01-01
    • 1970-01-01
    • 2014-06-26
    • 1970-01-01
    • 1970-01-01
    • 1970-01-01
    • 2010-12-25
    • 1970-01-01
    • 2016-01-19
    相关资源
    最近更新 更多