Rice’s Theorem

“Any non-trivial property of the behavior of programs in a r.e. language is undecidable.”

r.e.(recursively enumerable) = recognizable by a Turing-machine

所有我们感兴趣的，需要静态分析的部分，都是non-trivial的。
这句话的意思就是，没有一个完美的静态分析算法可以对一个non-trivial的程序给出一个绝对准确的结果。
完美的静态分析要求既Sound，又Complete。Sound可以理解为全面，Complete可以理解为准确。

注：这里与原作者的图稍有出入，原作者将False Negatives放在了Truth下边，我认为是不对的，本图是按我自己的理解绘制的

虽然根据Rice’s Theorem我们无法实现一个perfect的静态分析，但我们还是可以实现一个userful的静态分析算法。
一般来说，如果说某一个静态分析算法是userful的，那他要么Compromise soundness,要么Compromise completeness。

  • Compromise soundness(false positives)
  • Compromise completeness(false negatives)

A false positive is an error in binary classification in which a test result incorrectly indicates the presence of a condition (such as a disease when the disease is not present), while a false negative is the opposite error, where the test result incorrectly indicates the absence of a condition when it is actually present. These are the two kinds of errors in a binary test.

而市面上的静态分析，大多数都是sound的。

Static Analysis: ensure(or get close to)soundness, while making good trade-offs between analysis precision and analysis speed.

Abstraction + Over-approximation

静态分析可以分为may analysis和must analysis。
may analysis可以用两个单词来概括，分别是abstraction和over-approximation
abstraction是may analysis和must analysis两者公有的特性，既然over-approximation是may analysis的特性，那参考上图，under-approximation就是must-analysis的特性呗。

Abstraction

抽象就是将程序里的具体的值转变为特定的几个符号，这样做的意义是减少状态空间的域，加快分析的速度。举个栗子。