【Static Program Analysis - Chapter 3】Type Analysis

類型分析，我的理解就是（經過靜態分析技術）分析出代碼中，哪些地方只能是某種或某幾種數據類型，這是一種約束。

 

例如，給定一個程序:

其中，咱們能夠很直接地獲得一些約束：

最後，通過簡化能夠獲得：

對於給定的變量類型，若是他們不符合這個約束，則說明，他們是不合法的。

那麼，怎麼去提取以及維護這些約束呢？

採用一種「並查集」的結構：一個有向圖，每一個節點有一條邊指向父節點（父節點則指向本身）。若是兩個節點具備相同的父節點，那麼，這個兩節點就認爲是等價的，即含有相同的數據類型。

如下是並查集的基本算法：

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型。

另外一個例子：