3 简单类型检查器

类型系统

本节引用的文法

P → D; S
D → D; D | id : T
T → boolean | integer | array [num] of T | ↑T | T '→' T
S → id := E | if E then S | while E do S | S; S
E → truth | num | id | E mod E | E[E] | E↑ | E(E)

这个文法是二义的，但是比较简洁，容易分析

环境规则

$\displaystyle(Env\quad\varnothing)\quad\frac{}{\varnothing\vdash\diamondsuit}$

$\displaystyle(Decl\ Var)\quad\frac{\Gamma\vdash T,id\not\in dom(\Gamma)}{\Gamma,(id:T)\vdash\diamondsuit}$

id : T 是该简单语言的一个声明语句
遇到一个变量声明语句，若该变量在此之前未被声明过，即 $id\not\in dom(\Gamma)$ ，则向定型环境（符号表）中增加一个符号定型，即 id : T

语法规则

在定型规则中使用的类型表达式的语法

$\displaystyle(Type\ Bool)\quad\frac{\Gamma\vdash\diamondsuit}{\Gamma\vdash boolean}$

$\displaystyle(Type\ Int)\quad\frac{\Gamma\vdash\diamondsuit}{\Gamma\vdash integer}$

$\displaystyle(Type\ Void)\quad\frac{\Gamma\vdash\diamondsuit}{\Gamma\vdash void}$

void 用于表示语句类型

$\displaystyle(Type\ Ref)\quad\frac{\Gamma\vdash T}{\Gamma\vdash pointer(T)}$

具体语法： $↑T$
$T\neq void$
如果 $T$ 是类型，则 $pointer(T)$ 是类型

$\displaystyle(Type\ Array)\quad\frac{\Gamma\vdash T,\Gamma\vdash(N:integer)}{\Gamma\vdash array(N,T)}$

具体语法： $array\ [N]\ \textbf{of}\ T$
$T\neq void,N>0$

$\displaystyle(Type\ Function)\quad\frac{\Gamma\vdash T_1,\Gamma\vdash T_2}{\Gamma\vdash (T_1\to T_2)}$

$T_1,T_2\neq void$
$T_1,T_2$ 分别是函数的参数类型、返回类型

像 ↑、pointer(·)、array(·,·) 这样作用于类型表达式可以构造出新的类型表达式的记号叫做类型构造算子

定型规则

给各种形式的表达式和语句指派类型

表达式

$\displaystyle(Exp\ Truth)\quad\frac{\Gamma\vdash\diamondsuit}{\Gamma\vdash truth:boolean}$ （下面表示一个类似符号表条目的记录）

$\displaystyle(Exp\ Num)\quad\frac{\Gamma\vdash\diamondsuit}{\Gamma\vdash num:integer}$

$\displaystyle(Exp\ Id)\quad\frac{\Gamma_1,\textbf{id}:T,\Gamma_2\vdash\diamondsuit}{\Gamma_1,\textbf{id}:T,\Gamma_2\vdash \textbf{id}:T}$

$\displaystyle(Exp\ Mod)\quad\frac{\Gamma\vdash E_1:interger,\ \Gamma\vdash E_2:integer}{\Gamma\vdash E_1\textbf{mod}E_2:integer}$

$\displaystyle(Exp\ Index)\quad\frac{\Gamma\vdash E_1:array(N,T),\ \Gamma\vdash E_2:integer}{\Gamma\vdash E_1[E_2]:T}$ （ $0\le E_2.val\le N-1$ ）

$\displaystyle(Exp\ Deref)\quad\frac{\Gamma\vdash E:pointer(T)}{\Gamma\vdash E↑:T}$

$\displaystyle(Exp\ FunCall)\quad\frac{\Gamma\vdash E_1:T_1→T_2,\ \Gamma\vdash E_2:T_1}{\Gamma\vdash E_1(E_2):T_2}$

语句

$\displaystyle(Stmt\ Assign)\quad\frac{\Gamma\vdash \textbf{id}:T,\ \Gamma\vdash E:T}{\Gamma\vdash (\textbf{id}:=E):void}$

$\displaystyle(Stmt\ If)\quad\frac{\Gamma\vdash E:boolean,\ \Gamma\vdash S:void}{\Gamma\vdash (\textbf{if }E\textbf{ then }S):void}$ （while 类似）

$\displaystyle(Stmt\ Seq)\quad\frac{\Gamma\vdash S_1:void,\ \Gamma\vdash S_2:void}{\Gamma\vdash (S_1;S_2):void}$

拓展类型

积类型

构造算子： $\times$

匿名地位： $T_1,T_2$ 为成员类型， $T_1\times T_2$ 可表示列表、元组。

有名地位： $T_1,T_2$ 各具有名字 $f_1,f_2$ ，则 $f_1:T_1\times f_2:T_2$ 可用于表示结构体、记录类型。

上面两种情况也可以混搭。

和类型

构造算子： $+$

可用于表示两种类型共存的情况（比如共用体）。

语法制导的类型检查器

本节引用的文法

P → D; S
D → D; D | id : T （声明）
T → boolean | integer | array [num] of T | ↑T | T '→' T （类型）
S → id := E | if E then S | while E do S | S; S （语句）
E → truth | num | id | E mod E | E[E] | E↑ | E(E) （表达式）

声明

用语法制导的翻译方案实现类型检查，或者在访问 AST 时进行类型检查

addType 函数将 id 的类型添加到符号表中

lookup 函数取符号表中 id 的类型，若找不到则 error

如果表达式 E 的某个子表达式的类型是 error，则 error 从这个子构造一直传到 E

表达式 E 的综合属性 type 给出了 E 产生的表达式的类型表达式

方法1：用语法制导的翻译方案实现类型检查

D → D; D
D → id: T　　　{ addType (id.entry, T.type) } // D2，把 id 的类型信息填入符号表
T → boolean　　　　　　　{ T.type = boolean }
T → integer　　　　　　　{ T.type = interger }
T → ↑T~1~　　　　　　　　　{ T.type = pointer (T~1~.type) }
T → array [num] of T~1~　　{ T.type = array (num.val, T.type) }
T → T~1~ '→' T~2~　　　　　　　{ T.type = T~1~.type → T~2~.type }

方法2：在访问 AST 时进行类型检查

在 exitD2( ast ) 中增加对 addType 的调用。

如何实现对各种类型的表示？（编译器的符号表）

——用记录类型：（kind, Other Information），如（Func, T1, T2），（Array, T1, num），（Pointer, T1），（Bool, --）等。

表达式

E → truth　　　　　{ E.type = boolean }
E → num　　　　　　{ E.type = integer }
E → id　　　　　　　{ E.type = lookup (id.entry) } // 查符号表，获取 id 的类型
E → E~1~ mod E~2~　　　{ E.type = (E~1~.type == E~2~.type == integer) ? integer : error}
E → E~1~ [E~2~]　　　　　{ E.type = (E~1~.type = array(s,t) && E~2~.type == integer) ? t : error}
E → E~1~↑　　　　　　{ E.type = (E~1~.type == pointer(t)) ? t : error}
E → E~1~ (E~2~)　　　　　{ E.type = (E~1~.type = s → t && E~2~.type == s) ? t : error}

类型转换

E → E~1~ op E~2~

if (E1.type == int && E2.type == int) E.type = int;
else if (E1.type == int && E2.type == float) E.type = float;
else if (E1.type == float && E2.type == int) E.type = float;
else if (E1.type == float && E2.type == float) E.type = float;
else E.type = error;

语句

S → id := E

if ((id.type == E.type) && E.type ∈ {bool, int}) S.type = void;
else S.type = error;

S → if E then S~1~（while 同理）

if (E.type == bool) S.type = S1.type;
else S.type = error;

S → S~1~ ; S~2~

if (S1.type == void && S2.type == void) S.type = void;
else S.type = error;

程序

先声明，后语句

P → D；S

if (S.type == void) P.type = void;
else P.type = error;

现代编译器的主流实现

从分析树构造 AST，对语法树进行类型检查。

设计实现的关键

符号表的设计：如何表示不同的类型
语法树 Visitor 设计：比如 ANTLR 会生成与标签对应的语法结构的 ENTER 和 EXIT 方法

一个结论

对一个 $t$ 类型的数组 $a[i_1][i_2]...[i_n]$ 来说，表达式 $a$ 的类型是： $$ pointer(array(i_2-1,...array(i_n-1,t)...)) $$ 表达式 $\&a$ 的类型是： $$ pointer(array(i_1-1,...array(i_n-1,t)...)) $$

本文阅读量