Lab 7: Type Analysis
Overview
In this lab, you define name bindings and corresponding constraints for MiniJava in Statix. The concepts you are going to use in Statix are described in the following papers:
- H. van Antwerpen, C. B. Poulsen, A. Rouvoet, E. Visser: Scopes as Types, OOPSLA 2018
- P. Neron, A. Tolmach, E. Visser, G. Wachsmuth: A Theory of Name Resolution, ESOP 2015
- H. van Antwerpen, P. Neron, A. Tolmach, E. Visser, G. Wachsmuth: A Constraint Language for Static Semantic Analysis based on Scope Graphs, PEPM 2016
Update your Spoofax installation for this lab, to get the latest bug fixes. See the update instructions.
Overview
Objectives
Specify type analysis for MiniJava in Statix. The specification should include:
- Name binding constraints for
- method calls.
- Typing constraints for
- integer and boolean literals,
- unary and binary expressions,
- variable and field references,
- object creation,
this
expressions,- method calls,
- and the subtyping relation on classes.
Submission
You need to submit your MiniJava project with a merge request against branch assignment-7-submission
on GitLab.
The Git documentation explains how to file such a request.
The deadline for submission is November 23, 2019, 23:59.
Grading
You can earn up to 100 points for the correctness of your type analysis. Therefore, we run several test cases against your implementation. You earn points, when your implementation passes test cases. The total number of points depends on how many test cases you pass in each of the following groups:
- name binding (20 points)
- method declarations
- method references
- typing rules (35 points)
- literals (4 points)
- unary expressions (5 points)
- binary expressions (8 points)
- variable and field references (4 points)
- object creation (4 point)
this
expression (5 points)- method call (5 points)
- constraints (45 points)
- expressions (10 points)
- statements (10 points)
- subtyping in assignments, return expressions, method calls (10 points)
- cyclic inheritance (2 points)
- method overloading and method overriding (10 points)
- main class usage (3 points)
Early Feedback
We provide early feedback for your language implementation. This feedback gives you an indication which parts of your name and type analysis might still be wrong. It includes a summary on how many tests you pass and how many points you earn by passing them. You have 3 early feedback attempts.
Detailed Instructions
Git Repository
You continue with your work from the previous assignment. See the
Git documentation on how to create the
assignment-7-develop
branch from your previous work.
For the grading to work correctly, you have to pull some changes from the template. See the instructions on how to do that.
Example specification
A complete example specification for the simply typed lambda calculus can be found at STLC. Furthermore, we would recommend looking at the Tiger Statix implementation.
Declaring Types
In this lab we use the scopes as types idea to model class types. Instead of using the syntactic type constructors from the syntax directly, we introduce semantic types. These are the types that we use as the types of declarations and AST nodes. The types you should use are given by the following signature, which you should add to your specification:
signature
sorts TYPE constructors
CLASS : scope -> TYPE
INT : TYPE
BOOL : TYPE
INTARRAY : TYPE
We use scopes as types for classes, where the class is identified by its scope. Sometimes it is useful (and for this lab required for grading) to map the scope back to the original class name. Therefore, you must define a relation that associates the class name with the class scope:
signature
relations
className : -> ID
In the rule for class declarations, use the constraint !className[x] in s_cls
, where x
is the
class name, and s_cls
is the class scope, to store the class name. If you don’t do this, some of
the grading tests will fail!
You also need to add a type constructor for methods. This type should have two arguments, the return type, and a list of argument types of the method. We do not test for this type directly, so you can choose its name yourself.
Predicate Rules for Typing
Building on the predicate rules of lab 5, we need to extend the rules for AST nodes that have types with an extra type parameter. Instead of adding this as a regular parameter to the predicate, we usually prefer to use the functional syntax for these. For example, the predicate for typing expressions would get the following signature and rules:
expOk : scope * Exp -> TYPE
expOk(s, True()) = BOOL().
When using the function syntax, the predicate calls have to be used in term positions. For example,
in an equality constraint like expOk(s, e) == T
. Alternatively, you can use regular predicates and
add an extra parameter. In that case, the signature and rules look like this:
expOk : scope * Exp * TYPE
expOk(s, True(), BOOL()).
In the latter case, the predicate is used as a predicate, not a term, and the usage would be
expOk(s, e, T)
. Although we usually prefer the functional form, both are equivalent, and you are
free to choose either of them. Note that the functional form is translated to the predicate form,
which you can see using the Spoofax > Syntax > Format Normalized AST
menu.
The type is not automatically associated with the AST node. We do this be setting the type
property on an AST node, using the constraint @e.type := T
. For example, the rule for true
could
be written as:
expOk(s, e@True()) = T@BOOL() :- @e.type := T.
The convenience syntax v@t
is inline notation for v == t
, for a variable v
and a term t
.
Typing Declarations
In this lab we need to associate types with the declarations in the scope graph. Therefore, we
replace the decl
and scopeOf
relations with a new type
relation with the following signature:
signature
relations
type : occurrence -> TYPE
Declarations that were introduced with s -> OCCURRENCE
must now add a type as well, using the
syntax s -> OCCURRENCE with type TYPE
. Similarly, resolution queries such as Var{x} in s |-> [(_,
Var{x'})]
, must now query the type
relation as type of Var{x} in s |-> [(_, (Var{x'}, T))]
.
Subtyping
MiniJava supports subtyping between classes. To support this, you will have to implement a predicate to check whether one type is a subtype of another type. This predicate must be used instead of type equality wherever subtyping is allowed.
Subtyping between classes can be checked by using the structure of the scope graph. For this you can use a query that does not query a specific relation, but only considers the final scope of a path. The syntax for that is:
query () filter ... and { s :- ... } min ... and { s1, s2 :- ... } in s |-> ps
where the result ps
has type list((path * scope))
.
Type-dependent Name Resolution
Using types we can now implement resolution of method names. Use the class types to resolve method
names in the right scope. The scopes as types representation of class types should make this
easy. Do not forget to add the @x.ref := x'
property on method references, to ensure editor
resolution and testing work.
Remember that you can check if method resolution works, by Ctrl/Cmd + click on a method call in an example program.
Overriding
Finally, check if overriding is done correctly. If a method overrides a method from the super class, its parameter types must be the same. Also check that the return type is correct. Be careful, it does not have to be the same, but it needs to be co-variant! Incorrect overrides (including overloads) should result in an error.