Static Program Analysis - Introduction

南京大学《软件分析》课程01(Introduction):https://www.bilibili.com/video/av91858985

学习静态分析的意义

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?

A property is trivial if either it is not satisfied by any r.e. language, or if it is satisfied by all r.e. languages; otherwise it is non-trivial.

简单来说 non-trivial 属性是一些有趣的的属性,这些属性关联到程序的运行时行为。

Sound & Complete

image-20211222175133984

The Truth is sound & complete.

真实是即 sound 又 complete 的。倾向于 sound 的是 over-approximated,倾向于 complete 的是 under-approximated。

image-20211222180409044

完美的静态分析被 Rice 打脸了,是不实际的。但是存在有用的静态分析:

妥协 soundness 被叫做 false negatives,中文为漏报;妥协 completeness 被叫做 false positives,中文为误报。优先选择妥协 completeness,选择 sound。即允许误报不允许漏报。