TP 2 - Types

The goal of this session is to add typing to our language.

Language

Start by downloading the package here.

The language is the same as last week, but extended with variable declarations. Such declarations are statements of the form:

var var1 [= expr1], var2 [=expr2],...;

A single declaration can declare an arbitrary number of variables var1, var2. Each variable name is optionally followed by an initialization of the form = expr, which behaves similarly to an assignment. If there is no initialization expression, the variable is assumed to be non-initialized (using a non-initialized value in an expression is an error, but not a type error).

A variable declared in a block starts existing at the point of declaration and stops existing at the end of the block ; this is the variable scope. It is important to distinguish variables of the same name, in case several of them exist at the same time (in nested scopes).

The program is dynamically typed, à la Python: upon assignation, a variable takes the type of the value it is assigned. There is a type error in case an integer value is used with a boolean operator, or the converse.

Type analysis

The goal of this exercise is to write a static analyzer that automatically discovers whether the program is type safe (no dynamic type error at execution). The analysis is similar to computing the denotational semantics of a non-deterministic language, but sets of values (integers, booleans, errors) are replaced with abstract values.

  1. Define the type abstract_value of elements of the abstract value lattice. It should represent the type of integers and of booleans, and be closed by intersection and union.
  2. Define the type abstract_env of environments mapping each variable to the type of value (in abstract_value) it contains.
  3. Define the lattice join operator abstact_value_join: abstact_value -> abstract_value -> abstract_value (union of abstract values) and its extension to environments: env_join: abstract_env -> abstract_env -> abstract_env.
  4. Program the functions eval_expr: abstract_env -> expr ext -> abstract_value and eval_stmt: abstract_env -> stmt ext -> abstract_env. These should be very similar to the non-deterministic denotational semantics of last week, but use abstract values and abstract environments instead of sets of values and sets of environments. They are also extended to handle local variable scope.
  5. Evaluate your analyzer on the files in the examples directory. Can you spot the cases where the analyzer cannot prove the safety of the program, despite the program having no type error at execution?
  6. Extension: implement a polymorphic type analysis that propagates sets of type assignments instead of a single one.