CSE411: Introduction to Compilers

Type Checking

Jooyong Yi (UNIST)

Interface of a Type Checker

      |--------------|           
AST → | Type Checker | → ok / error
      |--------------|         

Example

void foo() {
    int x;
    int y;
    y = x;
}

• Is the above program type-safe?

Example

void foo() {
    int i;
    char *s;
    i = s;
}

• Is the above program type-safe?

Proof

void foo() {
    int x;
    int y;
    y = x;
}

• How do we prove that the above program is type-safe?

Proof Tree

------------------------   ------------------------
 [x:int][y:int] ⊢ y:int     [x:int][y:int] ⊢ x:int
-------------------------------------------------------
                 [x:int][y:int] ⊢ (y = x;): unit
               ----------------------------------
                 [x:int] ⊢ (int y; y = x;): unit
               -----------------------------------
                   ⊢ (int x; int y; y = x;): unit

Judgement

• An assertion about the typing of programs
• Syntax: Γ ⊢ J (we read this as "Γ entails J")
  • Γ: A typing environment
  • J: An assertion

[x:int][y:int] ⊢ x:int
               ⊢ (int x; int y; y = x;): unit

Building a Proof Tree

------------------------   ------------------------
 [x:int][y:int] ⊢ y:int     [x:int][y:int] ⊢ x:int
-------------------------------------------------------
                 [x:int][y:int] ⊢ (y = x;): unit
               ----------------------------------
                 [x:int] ⊢ (int y; y = x;): unit
               -----------------------------------
                   ⊢ (int x; int y; y = x;): unit         # Goal

• Inference rule

      Γ[I:int] ⊢ (S): unit        # premises
---------------------------
      Γ ⊢ (int I; S): unit        # conclusion  

Building a Proof Tree

------------------------   ------------------------
 [x:int][y:int] ⊢ y:int     [x:int][y:int] ⊢ x:int
-------------------------------------------------------
                 [x:int][y:int] ⊢ (y = x;): unit        # Goal
               ----------------------------------
                 [x:int] ⊢ (int y; y = x;): unit
               -----------------------------------
                   ⊢ (int x; int y; y = x;): unit         

• Inference rule

   Γ ⊢ I:τ  Γ ⊢ E:τ            # premises
-------------------------
      Γ ⊢ (I = E;): unit       # conclusion  

Building a Proof Tree

------------------------   ------------------------
 [x:int][y:int] ⊢ y:int     [x:int][y:int] ⊢ x:int     # Goal
-------------------------------------------------------
                 [x:int][y:int] ⊢ (y = x;): unit        
               ----------------------------------
                 [x:int] ⊢ (int y; y = x;): unit
               -----------------------------------
                   ⊢ (int x; int y; y = x;): unit         

• Axiom: a fact that is accepted as true without requiring any further justification.

--------------
 Γ[x:τ] ⊢ x:τ

Failure to Build a Proof Tree

--------------------------      ----------------------------
 [i:int][s:char*] ⊢ i:int       [i:int][s:char*] ⊢ s:char*     
------------------------------------------------------------
                 [i:int][s:char*] ⊢ (i = s;): unit              # Goal
               -------------------------------------
                 [i:int] ⊢ (char *s; i = s;): unit
               ------------------------------------------------
                   ⊢ (int i; char *s; i = s;): unit 

• Inference rule

   Γ ⊢ I:τ  Γ ⊢ E:τ            # premises
-------------------------
      Γ ⊢ (I = E;): unit       # conclusion  

If Statements

 Γ ⊢ E: boolean   Γ ⊢ S
--------------------------
  Γ ⊢ (if (E) S): unit

While Statements

 Γ ⊢ E: boolean   Γ ⊢ S
--------------------------
  Γ ⊢ (while (E) S): unit

Arithmetic Expressions

   Γ ⊢ E1: int   Γ ⊢ E2: int
------------------------------
      Γ ⊢ E1 + E2: int

Equality

    Γ ⊢ E1: τ   Γ ⊢ E2: τ
------------------------------
      Γ ⊢ E1 == E2: boolean

Procedure Invocation

   Γ ⊢ P: τ_1 × τ_2 × ... × τ_n → τ   Γ ⊢ E_k: τ_k (for k = 1, ..., n)
 -----------------------------------------------------------------------
           Γ ⊢ P(E1, E2, ..., En): τ

Integer Constant

-----------------
  Γ ⊢ n: int        # n is an integer constant

I do not want to manually write a proof tree...

Automatic Proof

• Imagine you traverse the AST

------------------------   ------------------------
 [x:int][y:int] ⊢ y:int     [x:int][y:int] ⊢ x:int    
-------------------------------------------------------
                 [x:int][y:int] ⊢ (y = x;): unit        
               ----------------------------------
                 [x:int] ⊢ (int y; y = x;): unit
               -----------------------------------
                   ⊢ (int x; int y; y = x;): unit         

------------------------   ------------------------
 [x:int][y:int] ⊢ y:int     [x:int][y:int] ⊢ x:int    
-------------------------------------------------------
                 [x:int][y:int] ⊢ (y = x;): unit        
               ----------------------------------
                 [x:int] ⊢ (int y; y = x;): unit                                 Γ[I:int] ⊢ (S): unit        
               -----------------------------------                            ---------------------------
                   ⊢ (int x; int y; y = x;): unit         # Goal                 Γ ⊢ (int I; S): unit                             

// Visitor to construct a symbol table
class Visitor extends ASTVisitor {
  ...
  public boolean visit(final VariableDeclarationStatement node) { // e.g., node: int x;
    final VariableDeclarationFragment vdf = (VariableDeclarationFragment) node.fragments().get(0); // e.g., vdf: x
    final String name = vdf.getName().getIdentifier();
    if (this.nameMap.containsKey(name)) {
      // duplicate declaration
      throw new Error(...);
    }
    this.nameMap.put(name, node);
    return false;
  }
  ...
}  

------------------------   ------------------------
 [x:int][y:int] ⊢ y:int     [x:int][y:int] ⊢ x:int    
-------------------------------------------------------
                 [x:int][y:int] ⊢ (y = x;): unit         # Goal
               ----------------------------------
                 [x:int] ⊢ (int y; y = x;): unit                                Γ ⊢ I:τ  Γ ⊢ E:τ            
               -----------------------------------                          -------------------------
                   ⊢ (int x; int y; y = x;): unit                               Γ ⊢ (I = E;): unit                           

class Visitor extends ASTVisitor {
  ...
  public boolean visit(final Assignment node) {
    node.getLeftHandSide().accept(this);
    final Type lhsType = getResult();
    node.getRightHandSide().accept(this);
    final Type rhsType = getResult();
    if (lhsType != rhsType) {
      throw new Error(node, "Type mismatch in \"" + node + "\": " + lhsType + " = " + rhsType);
    }
    return false;
  }
  ...
}  

Benefits of Using Inference Rules

Benefits of Using Inference Rules

• Modular and compositional reasoning
  • With a finite set of rules, we can prove the correctness of any program.

Logical System

• A type-checking system is an example of a logical system.
  • A logical system consists of axioms and inference rules.

Two Fundamental Questions

1. Soundness: P ⊢ Q ⇒ P ⊧ Q
2. Completeness: P ⊧ Q ⇒ P ⊢ Q

Soundness

• ⊢ (int x; int y; y = x;): unit ⇒ ⊧ (int x; int y; y = x;): unit
• The compiler says the given program is type-safe. Is the program really type-safe?

Completeness

• ⊧ (int x; int y; y = x;): unit ⇒ ⊢ (int x; int y; y = x;): unit
• I know that the given program should be type-safe. Can the compiler prove that the program is type-safe?

Completeness

import java.util.List;
import java.util.ArrayList;

public class Incomplete {
    static class C {}
    static class D extends C {}

    public static void main(String args[]) {
        List<C> lst = new ArrayList<>();
        if (args[0].equals("1")) {
            lst.add(new D());
        } else {
            lst.add(new D());
        }
        D d = lst.get(0);
    }
}                                                                                                                   

• Is the above Java program type-safe?

Completeness

import java.util.List;
import java.util.ArrayList;

public class Incomplete {
    static class C {}
    static class D extends C {}

    public static void main(String args[]) {
        List<C> lst = new ArrayList<>();
        if (args[0].equals("1")) {
            lst.add(new D());
        } else {
            lst.add(new D());
        }
        D d = lst.get(0);
    }
}                                                                                                                   

Incomplete.java:15: error: incompatible types: C cannot be converted to D
        D d = lst.get(0);
                     ^
1 error                                                                                                          

Sound Type System: Over-approximation

• A sound type system may reject some programs that are type-safe.