Static Program Analysis - Chapter 3Type Analysis

Posted 2020-10-16 max_xbw

类型分析，个人理解就是（通过静态分析技术）分析出代码中，哪些地方只能是某种或某几种数据类型，这是一种约束。

 

例如，给定一个程序:

其中，我们可以很直接地得到一些约束：

最后，经过简化可以得到：

对于给定的变量类型，如果他们不符合这个约束，则说明，他们是不合法的。

那么，怎么去提取以及维护这些约束呢？

采用一种“并查集”的结构：一个有向图，每个节点有一条边指向父节点（父节点则指向自己）。如果两个节点具有相同的父节点，那么，这个两节点就认为是等价的，即含有相同的数据类型。

以下是并查集的基本算法：

The unification algorithm uses union-find by associating a node with each term (including sub-terms) in the constraint system.

For each term τ we initially invoke MakeSet(τ ).

Note that each term at this point is either a type variable or a proper type (i.e. integer, heap pointer, or function); μ terms are only produced for presenting solutions to constraints, as explained below.

For each constraint τ1 = τ2 we invoke Unify(τ1, τ2), which unifies the two terms if possible and enforces the general term equality axiom by unifiying sub-terms recursively: 

Unification fails if attempting to unify two terms with different constructor (where function constructors are considered different if they have different arity). 

再来看个例子：

对于递归：

Limitations of the Type Analysis 

例子：

 

运行的时候没问题，但是，遵循之前的方法会报错，之前的方法并不考虑程序的顺序执行给数据类型转换的影响。即X=42在X=alloc之后，因此，最终返回的一定是int型。

另一个例子：