ECE479K Compilers

Spring 2025: Lecture 6

Prof. Mattan Erez

The University of Texas at Austin

Action items:
• Lab 1 (Checkpoint 2)
ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 2

Review and Outline

Review:
• Sequential deterministic execution
• Properly nested procedures
– Variable lifetime equal to scope
– Allocate all memory on the stack while populating symtab
• Still keeping code generation simple
– Be liberal with temporary pseudo-registers and stack allocations
– Optimizations coming pretty soon
• Some optimizations are better done at the AST level
– E.g., short circuiting conditionals
Outline:
• Types and type systems
• Type checking (semantic analysis)
– Probably continue on Wednesday
ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 3

Types
• A type is
– A set of values
– A set of operations on those values
• Classes are an example of the modern concept of types
• Base types are also important
• Why are types important?

Based on Alex Aiken’s Stanford CS143 slides

ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 4

Type systems
• A language’s type system specifies which operations are
valid for which types
• The goal of type checking is to ensure that operations are
used with the correct types
– Enforces intended interpretation of values,
– because nothing else will!
• Enables efficient code generation
– Allocate the right amount of memory/registers
– Specialize operations
– …

Based on Alex Aiken’s Stanford CS143 slides

ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 5

Three kinds of languages w.r.t. types

• Statically typed: all checking done at compile time

• Dynamically typed: all checking done at runtime

• Untyped: No checking (machine code)

Based on Alex Aiken’s Stanford CS143 slides

ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 6

Three kinds of languages w.r.t. types

• Statically typed: all checking done at compile time
– Catch lots of errors at compile time
– Avoid performance overheads for checking types at runtime
– Avoid performance overheads of tracking types at runtime

• Dynamically typed: all checking done at runtime

– Static typing is restrictive (can lead to very ugly/inefficient code)
– More rapid prototyping (more productive programming)

• Untyped: No checking (machine code)

– Unacceptable for high-level lanuguages
Based on Alex Aiken’s Stanford CS143 slides
ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 7

In practice languages mix both static and dynamic

• Unsafe casts in C and Java

• Static type annotations to facilitate optimization

• No perfect answer

Based on Alex Aiken’s Stanford CS143 slides

ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 8

Type semantic analysis

• Type declarations
– Static types: programmer declares types for identifiers
– Dynamic types: runtime tracking of types based on assigned values

• Type inference
– Static types: compiler infers (fills in) a type for every expression
– (auto)
– Dynamic types: runtime infers a type for every expression

• Type checking
– Verify that types are used correctly

Based on Alex Aiken’s Stanford CS143 slides

 9

TYPE SYSTEM
FORMALISM / NOTATION
ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 10

Type inference/checking formalism

• BNF is a formalism for context free grammars
• Type analysis formalism uses logical rules of inference

• Inference rules:
If Hypothesis is true, then Conclusion is true
• Type checking computes via reasoning on a set of rules
If expr1 and expr2 have certain types, then
expr3 has a certain type
– Proves facts about types over the AST (or fails to do so)

• The formal notation compactly expresses such if-then rules

– The notation is straightforward but appears quite complex
Based on Alex Aiken’s Stanford CS143 slides
ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 11

From English to inference rule notation

• Building blocks:
– Symbol ∧ is “and”
– Symbol ⇒ is “if-then”
– X:T is “x has type T”

• Example: if e1 is type Int and e2 is type Int,

then (e1 + e2) has type Int

(e1:Int e2:Int) ⇒ e1+e2:Int

• Special case of Hypothesis1∧Hypothesis2 ∧ … ⇒ Conclusion

Based on Alex Aiken’s Stanford CS143 slides
ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 12

Even more compact notation

• Building blocks:
– Symbol ∧ is “and”
– Symbol ⇒ is “if-then” (also use horizontal line for this purpose)
– X:T is “x has type T”
– ⊢ Hypothesis is “it is provable that Hypothesis is true”

Hypothesis1∧Hypothesis2 ∧ … ⇒ Conclusion

⊢ Hypothesis1 … ⊢ HypothesisN
⊢ Conclusion

Based on Alex Aiken’s Stanford CS143 slides

ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 13

Type inference notation example

[Int] i is an integer literal
⊢ i: Int

Based on Alex Aiken’s Stanford CS143 slides

ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 14

Type inference notation example

[Int] i is an integer literal
⊢ i: Int

[Add] ⊢ e1: Int ⊢ e2: Int

⊢ e1 + e2: Int

Proof of type performed by chaining / stacking up the rules

Based on Alex Aiken’s Stanford CS143 slides

ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 15

Type inference notation example

[Int] i is an integer literal
⊢ i: Int

[Add] ⊢ e1: Int ⊢ e2: Int

⊢ e1 + e2: Int

Proof of type performed by chaining / stacking up the rules

Example : 1 + 2

1 is an integer literal 2 is an integer literal

⊢ i: Int ⊢ i: Int .
⊢ 1 + 2: Int Based on Alex Aiken’s Stanford CS143 slides
ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 16

Soundness
• A type system is sound if:
– Whenever ⊢ e: T
– Then e can only evaluate to a value of type T

• We only want sound rules

– But some rules are better than others

i is an integer literal
⊢ i: Object

Based on Alex Aiken’s Stanford CS143 slides

ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 17

Type checking proofs

• Type checking proves facts e: T
– Proof is on the structure of the AST
– Proof has the shape of the AST
– One type rule is used for each AST node
• In the type rule used for a node e:
– Hypotheses are the proofs of types of e’s subexpressions
– Conclusion is the type of e
• Types are computed in a bottom-up pass over the AST

1 is an integer literal 2 is an integer literal

⊢ i: Int ⊢ i: Int .
⊢ 1 + 2: Int
Based on Alex Aiken’s Stanford CS143 slides
ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 18

Coding up type checking is straightforward

[Add] ⊢ e1: Int ⊢ e2: Int
⊢ e1 + e2: Int

TypeCheck(“add”, e1, e2):

T1 = TypeCheck(e1)
T2 = TypeCheck(e2)
assert T1 == T2 == Int
return Int

Based on Alex Aiken’s Stanford CS143 slides

ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 19

A few more type inference rule examples

A constant: [False] . .
⊢ false: Bool

[new] . ..
⊢ new T: T

[not] . ⊢ e: Bool ..
⊢ !e: Bool

Based on Alex Aiken’s Stanford CS143 slides

ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 20

Each expression must be typed

[while] ⊢ e1: Bool
⊢ e2 : T ..
⊢ while e1 loop e2 pool: Object

Why is the while expression as a whole type Object?

Based on Alex Aiken’s Stanford CS143 slides

 21

TYPE ENVIRONMENTS
ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 22

Type environments
[Var] x is a variable ..
⊢ x: ???

• x is a free variable (unbound and not defined in this rule)

– There isn’t enough information as is

• Bring in x’s type from a type environment .

– Type environment is a function to map objectIDs to types
– Basically the symbol table
• The sentence O ⊢ e: T means:
Under the assumption that variables have the types given by
O, it is provable that the expression e has the type T
Based on Alex Aiken’s Stanford CS143 slides
ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 23

Add the type environment to all inference rules

[Int] i is an integer literal
O ⊢ i: Int

[Add] O⊢ e1: Int O ⊢ e2: Int

O ⊢ e1 + e2: Int

• And can be explicit about type bindings

[Var] O(x) = T ..
O⊢ x: T

Based on Alex Aiken’s Stanford CS143 slides

ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 24

Type environments evolve with the program

Recall the let expression: let x: T0 in e1

[Let-no-Init] O[T0/x] ⊢ e1:T1 ..

O ⊢ let x: T0 in e1: T1

• O[T/x] evolves the environment such that x is type T but any

other variable is unchanged:
O[T/x](x) = T and O[T/x](y) = O(y)

Based on Alex Aiken’s Stanford CS143 slides

ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 25

Let with initialization

• What about let with initialization?
let x: T0 <- e0 in e1

Based on Alex Aiken’s Stanford CS143 slides

ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 26

Let with initialization

• What about let with initialization?
let x: T0 <- e0 in e1

[Let-Init]* O⊢ e0: T0
O[T0/x] ⊢ e1:T1 ..
O⊢ let x: T0 <- e0 in e1: T1

• Truly necessary that we write x: T0?

What about inheritance?
– x could be any class TC from which T0 inheritsBased
(even indirectly)
on Alex Aiken’s Stanford CS143 slides
ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 27

SUBTYPES (INHERITANCE)
ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 28

Subtypes (inheritance)
• Define a new relation for class inheritance: ≤
– X≤X
– X ≤ Y if X inherits from Y
– X ≤ Z if X ≤ Y and Y ≤ Z

• Improved let with initialization

[Let-Init] O ⊢ e0: T0
T0 ≤ T
O[T/x] ⊢ e1:T1 ..
O ⊢ let x: T <- e0 in e1: T1
Based on Alex Aiken’s Stanford CS143 slides
ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 29

Assignment and attribute initialization

[Assign] O(x) = T0
T1 ≤ T0
O ⊢ e1:T1 ..
O ⊢ x <- e1: T1

Based on Alex Aiken’s Stanford CS143 slides

ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 30

Assignment and attribute initialization

[Assign] O(x) = T0
T1 ≤ T0
O ⊢ e1:T1 ..
O ⊢ x <- e1: T1

[Attr-Init] OC(x) = T0
T1 ≤ T0
OC ⊢ e1:T1 ..
OC ⊢ x: T0 <- e1

Based on Alex Aiken’s Stanford CS143 slides

ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 31

Coding up type checking is straightforward

[Let-Init] O ⊢ e0: T0
T0 ≤ T
O[T/x] ⊢ e1:T1 ..
O ⊢ let x: T <- e0 in e1: T1

TypeCheck(Oenv, “let-init”, e0, e1):

T0_ = TypeCheck(Oenv, e0)
Oenv_ = [Link](“x”: T)
T1_ = TypeCheck(Oenv_, e1)
assert subtype(T0_, T)
assert T1_ == T1
return T1
Based on Alex Aiken’s Stanford CS143 slides
ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 32

Type rules for if-then-else

• Consider: if e0 then e1 else e2 fi
– The result is either e0 or e1, so possibly one of two types

• Type checking at compile time is static

• The best we can do is a common ancestor type of e0 and e1

Based on Alex Aiken’s Stanford CS143 slides

ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 33

If-then-else and the least upper bound of types

• Define a new function on types for this common ancestor:
least upper bound (lub)
• Z = lub(X,Y) is the least upper bound of X and Y if:
X ≤ Z ∧ Y ≤ Z (Z is an upper bound)
X ≤ Z’ ∧ Y ≤ Z’ ⇒ Z ≤ Z’ (Z is least among upper bounds)

[if-then-else] O⊢ e0: Bool

O⊢ e1: T1
O⊢ e2:T2 ..
O⊢ if e0 then e1 else e2 fi: lub(T1,T2)

lub(T1,T2) also written as T1 ⊔ T2

Based on Alex Aiken’s Stanford CS143 slides
ECE479K Compilers (Mattan Erez;, heavily based on UIUC CS426 slides by Sasa Misailovic 34

What did we learn

• Semantic analysis
– Part of building the symbol tables
• Every identifier associated with its descriptor (including its type when relevant)
– Checks critical program behavior
– Type systems and type checking notation
– Type environments (a formalism for the symbol table)
• Type checking process
– Prove that all types are acceptable based on the type inference rules
• Type hierarchies
• Static vs. dynamic type checking
• Subtleties and chunkiness