1
Static Checking and Type
Systems
2
3
The Structure of our Compiler
Revisited
Syntax-directed
Character Token static checker Java
stream Lexical analyzer
stream Syntax-directed bytecode
translator
Yacc specification
Lex specification Code JVM specification
Type
generati
checking
on
4
Static versus Dynamic Checking
• Static checking: the compiler enforces
programming language’s static semantics
– Program properties that can be checked at
compile time
• Dynamic semantics: checked at run time
– Compiler generates verification code to enforce
programming language’s dynamic semantics
5
Static Checking
• Typical examples of static checking are
– Type checks
– Flow-of-control checks
– Uniqueness checks
– Name-related checks
6
Type Checking, Overloading,
Coercion, Polymorphism
class X { virtual int m(); } *x;
class Y: public X { virtual int m(); } *y;
int op(int), op(float);
int f(float);
int a, c[10], d;
d = c + d; // FAIL
*d = a; // FAIL
a = op(d); // OK: static overloading (C++)
a = f(d); // OK: coersion of d to float
a = x->m(); // OK: dynamic binding (C++)
vector<int> v; // OK: template instantiation
7
Flow-of-Control Checks
myfunc() myfunc()
{ … { …
break; // ERROR switch (a)
} { case 0:
…
myfunc() break; // OK
{ … case 1:
while (n) …
{ … }
if (i>10) }
break; // OK
}
}
8
Uniqueness Checks
myfunc()
{ int i, j, i; // ERROR
…
}
cnufym(int a, int a) // ERROR
{ …
}
struct myrec
{ int name;
};
struct myrec // ERROR
{ int id;
};
9
Name-Related Checks
LoopA: for (int I = 0; I < n; I++)
{ …
if (a[I] == 0)
break LoopB; // Java labeled loop
…
}
10
One-Pass versus Multi-Pass
Static Checking
• One-pass compiler: static checking in C, Pascal,
Fortran, and many other languages is performed in
one pass while intermediate code is generated
– Influences design of a language: placement constraints
• Multi-pass compiler: static checking in Ada, Java,
and C# is performed in a separate phase,
sometimes by traversing a syntax tree multiple
times
11
Type Expressions
• Type expressions are used in declarations
and type casts to define or refer to a type
– Primitive types, such as int and bool
– Type constructors, such as pointer-to, array-of,
records and classes, templates, and functions
– Type names, such as typedefs in C and named
types in Pascal, refer to type expressions
12
13
14
Graph Representations for Type
Expressions
int *f(char*,char*)
fun fun
args pointer args pointer
pointer pointer int pointer int
char char char
Tree forms DAGs
15
Cyclic Graph Representations
Source program
struct Node
{ int val;
struct Node *next;
};
struct
val next
int pointer
Internal compiler representation of
the Node type: cyclic graph
16
Name Equivalence
• Each type name is a distinct type, even
when the type expressions that the names
refer to are the same
• Types are identical only if names match
• Used by Pascal (inconsistently)
type link = ^node; With name equivalence in Pascal:
var next : link; p ≠ next
last : link; p ≠ last
p : ^node; p = q = r
q, r : ^node; next = last
17
Structural Equivalence of Type
Expressions
• Two types are the same if they are
structurally identical
• Used in C/C++, Java, C#
pointer = pointer
struct struct
val next val next
int pointer int
18
Structural Equivalence of Type
Expressions (cont’d)
• Two structurally equivalent type
expressions have the same pointer address
when constructing graphs by sharing nodes
struct Node p &s
{ int val;
struct Node *next; *p s pointer
};
struct
struct Node s, *p;
p = &s; // OK val next
*p = s; // OK
int
p = s; // ERROR
19
Type Systems
• A type system defines a set of types and
rules to assign types to programming
language constructs
• Informal type system rules, for example “if
both operands of addition are of type
integer, then the result is of type integer”
• Formal type system rules: Post systems
20
21
22
23
24
25
26
27
28
29
A Simple Language Example
P→D;S E → true
D→D;D ⎟ false
⎟ id : T ⎟ literal
T → boolean ⎟ num
⎟ char ⎟ id
⎟ integer ⎟ E and E
⎟ array [ num ] of T ⎟E+E
⎟^T ⎟E[E]
S → id := E ⎟E^
⎟ if E then S
⎟ while E do S Pointer to T Pascal-like pointer
⎟S;S dereference operator
30
Simple Language Example:
Declarations
D → id : T { addtype(id.entry, T.type) }
T → boolean { T.type := boolean }
T → char { T.type := char }
T → integer { T.type := integer }
T → array [ num ] of T1 { T.type := array(1..num.val, T1.type) }
T → ^ T1 { T.type := pointer(T1)
Parametric types:
type constructor
31
Simple Language Example:
Checking Statements
S → id := E { S.type := (if id.type = E.type then void else type_error) }
Note: the type of id is determined by scope’s environment:
id.type = lookup(id.entry)
32
Simple Language Example:
Checking Statements (cont’d)
S → if E then S1 { S.type := (if E.type = boolean then S1.type
else type_error) }
33
Simple Language Example:
Statements (cont’d)
S → while E do S1 { S.type := (if E.type = boolean then S1.type
else type_error) }
34
Simple Language Example:
Checking Statements (cont’d)
S → S1 ; S2{ S.type := (if S1.type = void and S2.type = void
then void else type_error) }
35
Simple Language Example:
Checking Expressions
E → true { E.type = boolean }
E → false { E.type = boolean }
E → literal { E.type = char }
E → num { E.type = integer }
E → id { E.type = lookup(id.entry) }
…
36
Simple Language Example:
Checking Expressions (cont’d)
E → E1 + E2 { E.type := (if E1.type = integer and E2.type = integer
then integer else type_error) }
37
Simple Language Example:
Checking Expressions (cont’d)
E → E1 and E2 { E.type := (if E1.type = boolean and E2.type = boolean
then boolean else type_error) }
38
Simple Language Example:
Checking Expressions (cont’d)
E → E1 [ E2 ] { E.type := (if E1.type = array(s, t) and E2.type = integer
then t else type_error) }
Note: parameter t is set with the unification of
E1.type = array(s, t)
39
Simple Language Example:
Checking Expressions (cont’d)
E → E1 ^ { E.type := (if E1.type = pointer(t) then t
else type_error) }
Note: parameter t is set with the unification of
E1.type = pointer(t)
40
A Simple Language Example:
Functions
T → T -> T E→E(E)
Function type declaration Function call
Example:
v : integer;
odd : integer -> boolean;
if odd(3) then
v := 1;
41
Simple Language Example:
Function Declarations
T → T1 -> T2 { T.type := function(T1.type, T2.type) }
Parametric type:
type constructor
42
Simple Language Example:
Checking Function Invocations
E → E1 ( E2 ) { E.type := (if E1.type = function(s, t) and E2.type = s
then t else type_error) }
43
Type Conversion and Coercion
• Type conversion is explicit, for example
using type casts
• Type coercion is implicitly performed by
the compiler to generate code that converts
types of values at runtime (typically to
narrow or widen a type)
• Both require a type system to check and
infer types from (sub)expressions
44
