类型检查

1 .Chap 6: Type Checking/Semantic Analysis Prof. Steven A. Demurjian Computer Science & Engineering Department The University of Connecticut 371 Fairfield Way, Unit 2155 Storrs, CT 06269-3155 steve@engr.uconn.edu http://www.engr.uconn.edu/~steve (860) 486 - 4818 Material for course thanks to: Laurent Michel Aggelos Kiayias Robert LeBarre

2 .Overview Type Checking and Semantic Analysis is a Critical Features of Compilers and Compilation Passing a Syntax Check (Parsing) not Sufficient Type Checking Provides Vital Input Software Engineers Assisted in Debugging Process We’ll Focus on Classical Type Checking Issues Background and Motivation Type Analysis The Notion of a Type System Examining a Simple Type Checker Other Key Typing Concepts Concluding Remarks/Looking Ahead

3 .Background and Motivation Recall....

4 .Background and Motivation What we have achieved All the “words” (Tokens) are known The tree is syntactically correct What we still do not know... Does the program make sense ? What we will not try to find out Is the program correct ? This is Impossible! Our Concern: Does it Compile? Are all Semantic Errors Removed? Do all Types and their Usage Make Sense?

5 .Background and Motivation The program makes “sense” Programmer’s intent is clear Program is semantically unambiguous Data-wise We know what each name denotes We know how to represent everything Flow-wise We know how to execute all the statements Structure-wise Nothing is missing Nothing is multiply defined The program is correct It will produce the expected input

6 .Tasks To Perform Scope Analysis Figure out what each name refers to Understand where Scope Exists (See Chapter 7) Type Analysis Figure out the type of each name Names are functions, variables, types, etc. Completeness Analysis Check that everything is defined Check that nothing is multiply defined

7 .Output ? What the analysis produce Data structures “on the side” To describe the types(resolve the types) To describe what each name denotes (resolve the scopes) A Decorated tree Add annotations in the tree Possibly.... Semantic Errors!

8 .Pictorially

9 .Type Analysis Purpose Find the type of every construction Local variables Actuals for calls Formals of method calls Objects Methods Expressions Rationale Types are useful to catch bugs!

10 .Type Analysis Why Bother ? A type system is a tractable syntactic method for proving the absence of certain program behaviors by classifying phrases according to the kind of values they compute.

11 .Uses Many! Error detection Detect early Detect automatically Detect obvious and subtle flaws Abstraction The skeleton to provide modularity Signature/structure/interface/class/ADT/.... Documentation Program are easier to read Language Safety guarantee Memory layout Bound checking Efficiency

12 .How It works ? Classify programs according to the kind of values computed Set of All Programs Set of All Reasonable Programs Set of All Type-Safe Programs Set of All Correct Programs

13 .How do we do this ? Compute the type of every sentence On the tree With a tree traversal Some information will flow up (synthesized) Some information will flow down (inherited) Questions to answer What is a type ? How do I create types ? How do I compute types ?

14 .Types... Types form a language! With Terminals... Non-terminals.... And a grammar! Alternatively Types can be defined inductively Base types (a.k.a. the terminals) Inductive types (a.k.a. grammatical productions)

15 .Base Types What are the base types ? int float double char void bool error

16 .Inductive Type Definition Purpose Define a type in terms of other simple/smaller types Example array pointer reference Pair (products in the book) structure function methods classes ...

17 .Relation to Grammar ? Type → array ( Type , Type ) → pair ( Type , Type ) → tuple ( Type + ) → struct ( FieldType + ) → fun ( Type ) : Type → method ( ClassType , Type ) : Type → pointer( Type ) → reference( Type ) → ClassType → BasicType ClassType → class ( name [ , Type ] ) FieldType → name : Type BasicType → int | bool | char | float | double | void | error

18 .Type Terms What is that ? It is a sentence in the type language Example int pair(int,int) tuple(int,bool,float) array(int,int) fun(int) : int fun(tuple(int,char)) : int class(“Foo”) method(class(“Foo”), tuple(int,char)) : int

19 .So... If we have Type Term we have a Type Language We can parse it and obtain.... Type Trees! fun(tuple(int,char)) : int

20 .The Notion of a Type System Logical Placement of Type Checker: Role of Type Checker is to Verify Semantic Contexts Incompatible Operator/Operands Existence of Flow-of Control Info (Goto/Labels) Uniqueness w.r.t. Variable Definition, Case Statement Labels/Ranges, etc. Naming Checks Across Blocks (Begin/End) Function Definition vs. Function Call Type Checking can Occur as “Side-Effect” of Parsing via a Judicious Use of Attribute Grammars! Employ Type Synthesis Parser Type Checker Int. Code Generator Token Stream Syntax Tree Syntax Tree Interm. Repres.

21 .Example of type synthesis Assume the program if (1+1 == 2) then 1 + 3 else 2 * 3

22 .Yes... But.... What about identifiers ? Key Idea Type for identifiers are inherited attributes! Inherits From the definition To the use site. int n; .... if (n == 0) then 1 else n

23 .Example int n; .... if (n == 0) then 1 else n

24 .The Notion of a Type System Type System/Checker Based on: Syntactic Language Construct The Notion of Types Rules for Assigning Types to Language Constructs Strength of Type Checking (Strong vs. Weak) Strong vs. Weak Dynamic vs. Static OODBS/OOPLS Offer Many Variants All Expression in Language MUST have Associated Type Basic (int, real, char, etc.) Constructed (from basic and constructed types) How are Type Expression Defined and Constructed?

25 .Type Expressions A Basic Type is a Type Expression Examples: Boolean, Integer, Char, Real Note: TypeError is Basic Type to Represent Errors A Type Expression may have a Type Name which is also a Type Expression A Type Constructor Applied to Type Expression Results in a Type Expression Array(I,T): I is Integer Range, T is Type Expr. Product: T 1  T 2 is Type Expr if T 1 , T 2 Type Exprs. Record: Tuple of Field Names & Respective Type Pointer(T): T is a Type Expr., Pointer(T) also

26 .Type Expressions A Type Constructor Applied to Type Expression Results in a Type Expression (Continued) Functions: May be Mathematically Characterized with Domain Type D and Range Type R F: D  R int  int  int char  char  pointer(int) A Type Expression May Contain Variables whose Values are Type Expressions Called Type Variables We’ll Omit from our Discussion …

27 .Key Issues for Type System Classical Type System Approaches Static Type Checking (Compile Time) Dynamic Type Checking (Run Time) How is each Handled in C? C++? Java? Language Level Issues: Sound Type System (ML) No Dynamic Type Checking is Required All Type Errors are Determined Statically Strongly Typed Language (Java, Ada) Compiler Guarantees no Type Errors During Execution Weakly Typed Language (C, LISP) Allows you to Break Rules at Runtime What about Today’s Web-based Languages?

28 .The Notion of a Type System Types System: Rules Used by the Type Checker to Asign Types to Expressions and Verify Consistency Type Systems are Language/Compiler Dependent Different Versions of Pascal have Different Type Systems Same Language Can have Multiple Levels of Type Systems (C Compiler vs. Lint in Unix) Different Compilers for Same Language May Implement Type Checking Differently GNU C++ vs. MS Studio C++ Sun Java vs. MS Java (until Sun forced off market) What are the Key Issues?

29 .First Example: Simple Type Checker Consider Simplistic Language: What does this Represent? P → D ; E D → D ; D | id: T T → char | int | array [ num] of T |  T E → literal | number | id | E mod E | E [ E ] | E  Key: integer; Key MOD 999; X: character; B: integer; B MOD X; A: array [100] of char; A[20] A[200] Are all of these Legal?