Sound 和 Complete
Sound: 表示全面(例如，考虑了所有路径)，误报 Complete: 表示精确，漏报
大部分静态分析都是Sound。Soundness对于优化和验证非常重要
静态分析的概念
if (inout)
x = 1;
else
x = 0;
// x=?
结论 x = 1, 2 or 3 是Sound的，但不Complete。再加个-1就不Sound了。
precise, expensive vs imprecise, cheap
静态分析要在确保Soundness的情况下，在精度和速度间取舍。
例子
分析所有变量的正负
步骤：
- 抽象： Concrete Domain → Abstract Domain
- ints → signs (+, -, 零, unknown(但不可能是undefined) , undefined)
- 过近似
- Transfer Functions
- 对于每一个语句，抽象值的转换规则
- 根据分析的目标和每个语句的语义定义
- 控制流
- Flow merging
- Transfer Functions