![[15. Type Check - Post-lecture.pdf]]
`백틱` ⟦ ⟧
# Symbol Table
## IDENTIFIER 파악의 중요성
1. 코드가 잘못되었음을 파악
2. 프로그램의 의미를 분석하고, 검사하는 과정에서 함수나 (특히) 변수에 대해 파악하는 것은 필수적임.
```c
// test.c
// 예시 1
int main() {
printf("I'm %d years old!\n", n);
return 0;
}
```
```c
// 예시 2
int n = 260;
int main(int argc, char **argv) {
printf("My foot is %d mm long!\n", n);
return 0;
}
```
## SYMBOL TABLE: 파악한 변수나 함수 등에 대한 정보를 기록하는 테이블
```c
int n = 260;
int main(int argc, char **argv) {
printf("My foot is %d mm long!\n", n);
return 0;
}
```
symbol table은...
| 이름 | 종류 | 타입 | |
| ---- | --- | ------------------ | --- |
| n | 변수 | int | |
| main | 함수 | int x char * → int | |
| argc | 변수 | int | |
| argv | 변수 | char * | |
| … | … | … | |
SCOPE 별로 나누어서 관리하기도 함
```c
/* ===== Global Scope ===== */
int n;
int main() {
/* ===== Block Scope 0 ===== */
int n;
for ( ; ; ) {
/* ===== Block Scope 1 (for-문) ===== */
// ...
int n;
{
/* ===== Block Scope 2 (block-문) ===== */
int n;
// ...
/* ===== End Block Scope 2 ===== */
}
n + 1;
/* ===== End Block Scope 1 ===== */
}
/* ===== End Block Scope 0 ===== */
}
/* ===== End Global Scope ===== */
```
**전역 변수**
| 이름 | 종류 | 타입 | 위치 |
| --- | --- | --- | ------ |
| n | 변수 | int | line 1 |
| … | … | … | |
**main함수의 Block Scope 0**
|이름|종류|타입|위치|
|---|---|---|---|
|n|변수|int|line 4|
|…|…|…||
**main 함수의 Block Scope 1 (line 6 for-문)**
|이름|종류|타입|위치|
|---|---|---|---|
|n|변수|int|line 8|
|…|…|…||
**main 함수의 Block Scope 2 (line 9 block-문)**
|이름|종류|타입|위치|
|---|---|---|---|
|n|변수|int|line 10|
|…|…|…||
## SYMBOL TABLE 구축
- symbol table 구축 $\approx$ Undeclared Identifier 분석
- symbol table $\approx$ Undeclared Identifier 분석의 상태 + 추가 정보
```f#
type Scope =
| Block of int
| Undeclared
type State = (var * Scope) list
```
|이름|종류|타입|위치|
|---|---|---|---|
|n|변수|int|line 4|
|…|…|…||
## SYMBOL TABLE 구현
### Symtab
```f#
module SymbTab =
val enterScope: SymbTab -> CurLocation -> Scope * SymbTab (* 새 scope 진입 *)
val addSymbol: SymbTab -> Scope -> string -> Info -> SymbTab (* 심볼 추가 *)
val checkSymbol: SymbTab -> string -> bool (* 현재 scope에 정의 여부 확인 *)
val findSymbol: SymbTab -> string -> Info option (* 심볼 정보 조회 *)
val exitScope: SymbTab -> Scope -> SymbTab (* scope 탈출 *)
```
**main함수의 Block Scope 0**
|이름|종류|타입|위치|
|---|---|---|---|
|n|변수|int|line 1|
- `enterScope` → 새 Block Scope 생성
- `addSymbol` → `n: int` 등록 (line 1)
- `checkSymbol "m"` → `false` (현재 scope에 m 미정의)
- 현재 scope에 m이 정의되어 있나요?
- `findSymbol "n"` → `Some (변수, int, line 1)`
- n의 정보는?
- `exitScope` → Block Scope 0 종료
## SYMBOL TABLE 구축 & UNDECLARED IDENTIFIER 분석
bool
```f#
let rec analyzeArithExp exp symbTab =
match exp with
// | ...
| Var varName ->
match SymbTab.findSymbol symbTab varName with
| Some _ -> true
| _ -> false
// | ...
```
대입
```f#
let rec buildSymbTabStmt stmt scope symbTab =
match stmt with
| Assign (varName, exp) ->
let isValid = analyzeArithExp exp symbTab
if not isValid then failwith "Undeclared Variable!"
let isDeclared = SymbTab.checkSymbol symbTab varName
if isDeclared then failwith "Redeclared Variable!"
let symbTab = SymbTab.addSymbol symbTab scope varName (...)
symbTab
// | ...
```
if
```f#
let rec buildSymbTabStmt stmt scope symbTab =
match stmt with
// | ...
| If (exp, stmt1, stmt2) ->
let isValid = analyzeArithExp exp symbTab
if not isValid then failwith "Undeclared Variable!"
let scope_, symbTab1 = enterScope symbTab (...)
let symbTab1 = buildSymbTabStmt stmt1 scope_ symbTab1
let symbTab1 = exitScope symbTab1 scope_
let scope_, symbTab2 = enterScope symbTab1 (...)
let symbTab2 = buildSymbTabStmt stmt2 scope_ symbTab2
let symbTab2 = exitScope symbTab2 scope_
symbTab2
// | ...
```
while
```f#
let rec buildSymbTabStmt stmt scope symbTab =
match stmt with
// | ...
| While (exp, stmt) ->
let isValid = analyzeArithExp exp symbTab
if not isValid then failwith "Undeclared Variable!"
let scope_, symbTab = enterScope stmt scope symbTab
let symbTab = buildSymbTabStmt stmt scope_ symbTab
let symbTab = exitScope symbTab scope_
symbTab
```
# TYPE CHECK
## TYPE?
1. 어떤 값의 범위를 한정시켜주는 것
2. 어떤 값에 적용할 수 있는 연산을 한정시켜주는 것
### DESIGN CHOICES
1. weekly vs. **strongly** typed
2. **statically** vs. dynamically typed
3. **explicitly** vs. implicitly typed
## TYPE을 어떻게 분석?
### 큰 그림에서의 TYPE 분석
1. symbol table에 함수, 변수에 대한 타입 정보 기록
2. 프로그램을 살펴보면서 symbol table에 기록된 타입 정보와 실제 타입의 사용이 일치하는지 확인
1. 프로그램을 살펴보면서 = interpreter
### TYPE 분석에서의 의미
우리의 관심사 = "값이 타입에 맞게 잘 사용되고 있나요?"
- `EXPRESSION` 연산이 타입에 맞게 잘 적용이 되었는지?
- `STATEMENT` 해당 STATEMENT의 구성요소들 (expression, statement)이 타입에 맞게 잘 정의되어 있는지?
### 약속: TYPE 분석의 의미를 표현하는 기호
- 전통적으로 프로그래밍언어론 분야에서 Type 분석의 의미는 다르게 표현합니다.
- 참고) $⟦·⟧_σ$
- Type 분석과 관련된 의미 표현법 세 종류:
- Type의 표현: 이 식이 어떤 타입을 갖는다
- Type의 기록: 심볼 테이블에 기록
- Type의 확인: 심볼 테이블로부터 확인
### 약속 1: Type의 표현
- $\Gamma$라는 type 상태에서 $E$는 $\tau$라는 type을 갖는다.
- 타입 분석에서의 상태는 $\Sigma$가 아니라 $\Gamma$로 표현
- $E$ = **Expression**
$\Gamma \vdash E : \tau$
### 약속 2: Type 상태에 변수의 Type 기록
- Type 상태 $\Gamma$에 변수 $x$의 type이 $\tau$라는 사실을 기록:
- 심볼 테이블에 값을 집어넣는 방식으로 구현이 됨
- 구현: Symbol Table
$\Gamma[x \mapsto \tau]$
### 약속 3: Type 상태에서 변수의 Type 확인
- Type 상태 $\Gamma$에서 변수 $x$의 type이 $\tau$라는 사실을 확인:
- 구현: Symbol Table
$\Gamma(x) = \tau$
### 약속 4: Type의 가정과 결론
- 가정과 결론을 나타내는 형태가 조금 달라요
$\frac{\Gamma \vdash P_1, \ldots}{\Gamma \vdash C}$
## TYPE 의미를 표현해볼까요?
### TWhile (Typed-While) 언어
```
S ::= t x | x := a | x := b | skip | S ; S | if b S S | while b S
a ::= n | x | a + a | a * a | a - a
b ::= true | false | x | a = a | a <= a | ! b | b && b
t ::= int | bool
```
### 상수의 Type
- n의 type은 int, true, false의 의미는 bool입니다.
$\Gamma \vdash n : int$
$\Gamma \vdash true : bool$
$\Gamma \vdash false : bool$
### 변수의 Type
- 변수의 의미는 변수가 존재하는 환경에 따라 달라집니다.
- 타입과 관련된 상태에서, x의 타입이 무엇인지 가져온 다음에, 그게 $\tau$라고 하니 $\Gamma \vdash x : \tau$ 라고 함.
$\frac{\Gamma(x) = \tau}{\Gamma \vdash x : \tau}$
### 산술 계산식의 Type
- 각 산술 계산식의 type은 연산자 양 쪽의 type을 기반으로 계산됩니다.
- $a_1$이 int고, $a_2$도 int면, $a_1 + a_2$가 int라고 함
$\frac{\Gamma \vdash a_1 : int, \quad \Gamma \vdash a_2 : int}{\Gamma \vdash a_1 + a_2 : int}$
### 논리 계산식의 Type
- 각 논리 계산식의 type은 연산자 양 쪽의 type을 기반으로 계산됩니다.
$\frac{\Gamma \vdash a_1 : int, \quad \Gamma \vdash a_2 : int}{\Gamma \vdash a_1 \leq a_2 : bool}$
$\frac{\Gamma \vdash b : bool}{\Gamma \vdash \neg b : bool}$
### skip statement의 Type
- skip statement는 그 자체로 올바르게 정의됩니다.
$\frac{}{\Gamma \vdash skip}$
### Declaration statement의 Type
- `t x` statement는 상태에 변수 $x$가 $\tau$라는 타입을 갖는다는 사실을 추가합니다.
$\frac{\Gamma[x \mapsto \tau] \vdash S}{\Gamma \vdash \tau\ x;\ S}$
### Assign statement의 Type
- `x := a` statement는 a의 타입과 x의 타입이 같을 때 올바릅니다.
- 집어넣어지는 값이랑, 대상이랑 타입이 같을 때
$\frac{\Gamma(x) = \tau_1, \quad \Gamma \vdash a : \tau_2, \quad \tau_1 = \tau_2}{\Gamma \vdash x \mathrel{:=} a}$
### Sequential statement의 Type
- `S ; S` statement는 두 statement가 모두 올바른 경우에 올바릅니다.
$\frac{\Gamma \vdash S_1, \quad \Gamma \vdash S_2}{\Gamma \vdash S_1 ; S_2}$
### if statement의 Type
- `if b S S` statement는 조건 및 각각의 경우가 올바른 경우에 올바릅니다.
$\frac{\Gamma \vdash b : bool, \quad \Gamma \vdash S_1, \quad \Gamma \vdash S_2}{\Gamma \vdash if\ b\ S_1\ S_2}$
### while statement의 Type
- `while b S` statement는 조건 및 루프 내용이 올바를 때 올바릅니다.
$\frac{\Gamma \vdash b : bool, \quad \Gamma \vdash S}{\Gamma \vdash while\ b\ S}$
### 예제: 간단한 TWhile 프로그램 (1) — Declaration
```c
int x; // ← Γ[x ↦ int] ⊢ S / Γ ⊢ int x; S
bool y; // ← Γ[y ↦ bool] ⊢ S / Γ ⊢ bool y; S
x := 10;
y := true;
x := x + y;
if (y)
x := 1
else
x := 0
```
| 이름 | 종류 | 타입 |
|------|------|------|
| x | 변수 | int |
| y | 변수 | bool |
$\frac{\Gamma[x \mapsto \tau] \vdash S}{\Gamma \vdash \tau\ x;\ S}$
### 예제: 간단한 TWhile 프로그램 (2) — Assign
```c
int x;
bool y;
x := 10; // ← Γ(x)=τ₁, Γ⊢a:τ₂, τ₁=τ₂ / Γ ⊢ x := a
y := true;
x := x + y;
if (y)
x := 1
else
x := 0
```
| 이름 | 종류 | 타입 |
| --- | --- | ---- |
| x | 변수 | int |
| y | 변수 | bool |
$\frac{\Gamma(x) = \tau_1, \quad \Gamma \vdash a : \tau_2, \quad \tau_1 = \tau_2}{\Gamma \vdash x \mathrel{:=} a}$
### 예제: 간단한 TWhile 프로그램 (3) — Assign (bool)
```c
int x;
bool y;
x := 10;
y := true; // ← Γ(y)=bool, Γ⊢true:bool, bool=bool → OK
x := x + y;
if (y)
x := 1
else
x := 0
```
| 이름 | 종류 | 타입 |
|------|------|------|
| x | 변수 | int |
| y | 변수 | bool |
$\frac{\Gamma(x) = \tau_1, \quad \Gamma \vdash a : \tau_2, \quad \tau_1 = \tau_2}{\Gamma \vdash x \mathrel{:=} a}$
### 예제: 간단한 TWhile 프로그램 (4) — Type Error
```c
int x;
bool y;
x := 10;
y := true;
x := x + y; // ← Γ(x)=int, Γ⊢(x+y):?, int ≠ bool → TYPE ERROR!
if (y)
...
```
| 이름 | 종류 | 타입 |
| --- | --- | ---- |
| x | 변수 | int |
| y | 변수 | bool |
> ⚠️ **Type Error 발견!** `x`는 `int`인데 `y`는 `bool`이므로 `x + y` 연산 불가
### 예제: 간단한 TWhile 프로그램 (5) — Assign (type mismatch 상세)
```c
int x;
bool y;
x := 10;
y := true;
x := x + y; // ← Γ(x)=int, Γ⊢(x+y):τ₂, int=τ₂ 검사
// → Γ⊢x:int, Γ⊢y:bool → x+y 에서 int≠bool → TYPE ERROR
if (y)
x := 1
else
x := 0
```
| 이름 | 종류 | 타입 |
|------|------|------|
| x | 변수 | int |
| y | 변수 | bool |
$\frac{\Gamma(x) = \tau_1, \quad \Gamma \vdash a : \tau_2, \quad \tau_1 = \tau_2}{\Gamma \vdash x \mathrel{:=} a}$
### 예제: 간단한 TWhile 프로그램 (6) — if statement
```c
int x;
bool y;
x := 10;
y := true;
x := x + y;
if (y) // ← Γ⊢y:bool, Γ⊢(x:=1), Γ⊢(x:=0)
x := 1 // ← S₁
else
x := 0 // ← S₂
```
| 이름 | 종류 | 타입 |
|------|------|------|
| x | 변수 | int |
| y | 변수 | bool |
$\frac{\Gamma \vdash b : bool, \quad \Gamma \vdash S_1, \quad \Gamma \vdash S_2}{\Gamma \vdash if\ b\ S_1\ S_2}$
## TYPE 분석에서의 고민거리들
1. 보다 세밀한 TYPE 정의
1. 같은 종류의 크기가 다른 타입
1. ex. `char` `short` `int` `long long int` -> `(char) x + (short) y = ?`
2. 복잡한 종류의 타입
1. ex. C의 struct type?
2. Implicitly Typed 언어의 타입은 어떻게 검사?
1. ex. F#의 `let add x y = x + y` 이런 것들