|
|
|
@@ -1,13 +1,17 @@
|
|
|
|
|
#import "../../requirements.typ": isc-hei-bthesis
|
|
|
|
|
#import isc-hei-bthesis: todo
|
|
|
|
|
#import "@preview/acrostiche:0.7.0": acr
|
|
|
|
|
#import "../../utils.typ": code-ref
|
|
|
|
|
#import "../../utils.typ": code-ref, fn-link
|
|
|
|
|
#import "@preview/codly:1.3.0": codly
|
|
|
|
|
#import "@preview/lovelace:0.3.1": pseudocode-list
|
|
|
|
|
#import "../../appendices/python_typer.typ": python-typer-function-code
|
|
|
|
|
|
|
|
|
|
= Python Type Checking <sec:impl-python>
|
|
|
|
|
|
|
|
|
|
We have now built a type definition language and registry, but it is of no use if we cannot type-check our Python code. In a similar fashion to `MidasTyper`, we must now implement a `PythonTyper`. Its role is to take in some Python source code and the types registry, walk through each statement and expression, infer the type of each term and verify the program's soundness. We will need several tools to concretize this process, such as a resolver to keep track of which value each variable references, and an environment to store the inferred types of local variables.
|
|
|
|
|
|
|
|
|
|
For the sake of readability and conciseness, many parts of the implementation will be omitted from the following sections, focusing instead on the basic principles and most interesting methods. As always, the full source code is available in the repository, mainly in #code-ref(<checker>, "midas/checker").
|
|
|
|
|
|
|
|
|
|
== Parsing Python <sec:python-parsing>
|
|
|
|
|
|
|
|
|
|
For consistency and resource sharing, we will mirror a number of structures and methods used for the Midas language. However, we do not need to implement a lexer and parser for Python as it already provides an `ast` module just for this purpose. Nonetheless, we will implement our own #acr("AST") nodes similar to those discussed in @sec:midas-lexing-parsing. This allows having the same structure as the Midas #acr("AST") and explicitly only implement supported Python constructs. Additionally, it will make some node namings and internal structures clearer.
|
|
|
|
@@ -15,18 +19,252 @@ For consistency and resource sharing, we will mirror a number of structures and
|
|
|
|
|
The same generation script is used to create dataclasses for each node type (see @sec:midas-lexing-parsing).
|
|
|
|
|
|
|
|
|
|
For Python, we will also use three kinds of nodes:
|
|
|
|
|
- Statements (`Stmt`): top-level constructs introduced which can have side-effects in the environment
|
|
|
|
|
- Statements (`Stmt`): top-level constructs which can have side-effects in the environment
|
|
|
|
|
- Expressions (`Expr`): composable building blocks with an inferrable type
|
|
|
|
|
- Types (`MidasType`): type expressions used in annotations
|
|
|
|
|
|
|
|
|
|
The full list of #acr("AST") nodes used for Python is available in @tab:python-ast-nodes and their concrete implementation in the repository in #code-ref(<python-ast>, "midas/ast/python.py").
|
|
|
|
|
|
|
|
|
|
We implement a `PythonParser` class which takes in an #acr("AST") module node generated from Python's own `ast` library, and produces an equivalent tree with our nodes, skipping unsupported constructs and simplifying some elements. Because `ast` also uses statement (`ast.stmt`) and expression (`ast.expr`) nodes, we must implement two methods `parse_expr(node: ast.expr) -> Expr` and `parse_stmt(node: ast.stmt) -> None | Stmt | list[Stmt]`. The latter does not simply return a `Stmt` object to allow single Python statements to be split into multiple nodes (e.g. `ast.AnnAssign` is split into a type assignment and a value assignment) or even not produce any node (e.g. `ast.Pass` nodes are skipped). We leverage again Python's `match` statement for pattern matching.
|
|
|
|
|
|
|
|
|
|
This section will not go into details about the parser's implementation because it is not particularly interesting and quite repetitive. The source code is still available in the repository in #code-ref(<python-parser>, "midas/parser/python.py").
|
|
|
|
|
|
|
|
|
|
== Resolving References <sec:python-resolver>
|
|
|
|
|
|
|
|
|
|
Although we will not _evaluate_ Python expressions, we will need to know what bindings refer to. Following chapter 11 of _Crafting Interpreters_@Nystrom2021, we will implement a resolver class. Its goal is to identify binding declarations, keep a record of which scope that declaration appears in and mark each reference with the binding it actually refers to. For example in @fig:example-scoping, the variable `foo` on @fig:example-scoping:4 refers to the inner variable, not the global one.
|
|
|
|
|
|
|
|
|
|
#figure(
|
|
|
|
|
```python
|
|
|
|
|
foo = 3
|
|
|
|
|
def bar():
|
|
|
|
|
foo = ""
|
|
|
|
|
print(foo)
|
|
|
|
|
```,
|
|
|
|
|
caption: [Example of variable scoping in Python]
|
|
|
|
|
) <fig:example-scoping>
|
|
|
|
|
|
|
|
|
|
The implementation is mostly adapted from a previous project, #fn-link(<pebble-fn>, "https://git.kb28.ch/HEL/pebble")[pebble] and based on Nystrom's@Nystrom2021 tutorial-like approach. We will not describe the whole implementation of our `Resolver`, which is available in the repository in #code-ref(<resolver>, "midas/checker/resolver.py"), but only mention two points of interest.
|
|
|
|
|
|
|
|
|
|
The first point is that this resolver will also perform a form of definite assignment analysis, which is "a data-flow analysis used by compilers to conservatively ensure that a variable or location is always assigned before it is used"@enwiki:1326872870. This is distinguishing variable declaration and definition, which is not explicit in Python's syntax. It allows producing useful error diagnostics such as in @fig:resolver-visit_variable_expr.
|
|
|
|
|
|
|
|
|
|
#figure(
|
|
|
|
|
```python
|
|
|
|
|
def visit_variable_expr(self, expr: p.VariableExpr) -> None:
|
|
|
|
|
if self.is_declared(expr.name) and not self.is_defined(expr.name):
|
|
|
|
|
self.reporter.error(
|
|
|
|
|
expr.location,
|
|
|
|
|
f"Variable '{expr.name}' is declared but may not be defined",
|
|
|
|
|
)
|
|
|
|
|
self.resolve_local(expr, expr.name)
|
|
|
|
|
```,
|
|
|
|
|
caption: [Implementation of `Resolver.visit_variable_expr`]
|
|
|
|
|
) <fig:resolver-visit_variable_expr>
|
|
|
|
|
|
|
|
|
|
Secondly, as stated in #smallcaps[T-IfElse] in @sec:typing-statements, our type checker will not allow leaking variables from inner scopes such as in `if`/`else` statements. Using scopes we can trivially isolate branches and discard inner declarations after such statements. However, we still want to perform assignment analysis. Taking the situation exhibited in @fig:example-if-else-assignment, the resolver can know that `foo` is definitely assigned when reaching @fig:example-if-else-assignment:6 even though no assignment is made outside of the conditional.
|
|
|
|
|
|
|
|
|
|
#figure(
|
|
|
|
|
```python
|
|
|
|
|
foo: str
|
|
|
|
|
if ...:
|
|
|
|
|
foo = "true"
|
|
|
|
|
else:
|
|
|
|
|
foo = "false"
|
|
|
|
|
print(foo)
|
|
|
|
|
```,
|
|
|
|
|
caption: [Example of fully assigned variable in `if` statement]
|
|
|
|
|
) <fig:example-if-else-assignment>
|
|
|
|
|
|
|
|
|
|
More generally, if all sub-branches assign to a variable, we can consider it defined in the parent scope. This is implemented as shown in @fig:resolver-visit_if_stmt. Here, `self.end_scope` returns the inner scope containing declarations and assignments made inside each branch. We then check which variable is defined in both branches and forward the definition.
|
|
|
|
|
|
|
|
|
|
#figure(
|
|
|
|
|
```python
|
|
|
|
|
def visit_if_stmt(self, stmt: p.IfStmt) -> None:
|
|
|
|
|
self.resolve(stmt.test)
|
|
|
|
|
|
|
|
|
|
self.begin_scope()
|
|
|
|
|
self.resolve(*stmt.body)
|
|
|
|
|
body: dict[str, bool] = self.end_scope()
|
|
|
|
|
|
|
|
|
|
self.begin_scope()
|
|
|
|
|
self.resolve(*stmt.orelse)
|
|
|
|
|
else_: dict[str, bool] = self.end_scope()
|
|
|
|
|
|
|
|
|
|
for name, is_defined in body.items():
|
|
|
|
|
if is_defined and else_.get(name, False):
|
|
|
|
|
self.define(name)
|
|
|
|
|
```,
|
|
|
|
|
caption: [Implementation of `Resolver.visit_if_stmt`]
|
|
|
|
|
) <fig:resolver-visit_if_stmt>
|
|
|
|
|
|
|
|
|
|
== Environments <sec:python-env>
|
|
|
|
|
|
|
|
|
|
#todo[]
|
|
|
|
|
|
|
|
|
|
== Type Checking Statements <sec:python-check-stmt>
|
|
|
|
|
#todo[]
|
|
|
|
|
|
|
|
|
|
We now have the tools to start type checking our Python code.
|
|
|
|
|
The input given to `PythonTyper` is basically a sequence of statements (`p.Stmt`). Using the visitor pattern, we make `PythonTyper` extend ```python p.Stmt.Visitor[None]``` and implement all `visit_*_stmt` methods.
|
|
|
|
|
|
|
|
|
|
=== Variable assignment <sec:python-var-assign>
|
|
|
|
|
|
|
|
|
|
One of the main mechanics manipulating the environment is variable declaration and assignment.
|
|
|
|
|
During parsing, a statement such as ```python foo: int = 3```, represented in Python as a single `ast.AnnAssign` node, is split into two #acr("AST") nodes. The first is a type assignment (`p.TypeAssign`), which declares a new variable with the given type. The second is a variable assignment (`p.AssignStmt`). Implementing `visit_type_assign` is straightforward: we first resolve the type annotation expression and then define a new variable in the current environment, as demonstrated in @fig:python-visit_type_assign.
|
|
|
|
|
|
|
|
|
|
#figure(
|
|
|
|
|
```python
|
|
|
|
|
def visit_type_assign(self, stmt: p.TypeAssign) -> None:
|
|
|
|
|
type: Type = self.resolve_type_expr(stmt.type)
|
|
|
|
|
self.env.define(stmt.name, type)
|
|
|
|
|
```,
|
|
|
|
|
caption: [Python Typer: implementation of `visit_type_assign`]
|
|
|
|
|
) <fig:python-visit_type_assign>
|
|
|
|
|
|
|
|
|
|
This method basically materializes #smallcaps[T-Annot] from @tab:typing-statements.
|
|
|
|
|
|
|
|
|
|
Handling the variable assignment part is a bit more involved, because Python (and our type checker) allows both assigning to multiple targets simultaneously (@fig:python-visit_assign_stmt:3) and assigning to attributes and subscripts (not only variables). This is the reason we use a `match` statement in @fig:python-visit_assign_stmt.
|
|
|
|
|
|
|
|
|
|
#codly(
|
|
|
|
|
ranges: (
|
|
|
|
|
(1, 9),
|
|
|
|
|
(19, 30)
|
|
|
|
|
),
|
|
|
|
|
smart-skip: true
|
|
|
|
|
)
|
|
|
|
|
#figure(
|
|
|
|
|
```python
|
|
|
|
|
def visit_assign_stmt(self, stmt: p.AssignStmt) -> None:
|
|
|
|
|
value_type: Type = self.type_of(stmt.value)
|
|
|
|
|
for target in stmt.targets:
|
|
|
|
|
self._assign(stmt.location, target, value_type)
|
|
|
|
|
|
|
|
|
|
def _assign(self, location: Location, target: p.Expr, value_type: Type):
|
|
|
|
|
match target:
|
|
|
|
|
case p.VariableExpr():
|
|
|
|
|
self._assign_var(location, target, value_type)
|
|
|
|
|
case p.GetExpr(object=object, name=name):
|
|
|
|
|
self._assign_attr(location, object, name, value_type)
|
|
|
|
|
case p.SubscriptExpr(object=p.VariableExpr() as var, index=index):
|
|
|
|
|
self._assign_sub(location, var, index, value_type)
|
|
|
|
|
case _:
|
|
|
|
|
self.reporter.warning(
|
|
|
|
|
target.location, f"Unsupported assignment to {target}"
|
|
|
|
|
)
|
|
|
|
|
|
|
|
|
|
def _assign_var(self, location: Location, target: p.VariableExpr, value_type: Type):
|
|
|
|
|
name: str = target.name
|
|
|
|
|
var_type: Optional[Type] = self.look_up_variable(name, target)
|
|
|
|
|
|
|
|
|
|
if var_type is None:
|
|
|
|
|
self.env.define(name, value_type)
|
|
|
|
|
else:
|
|
|
|
|
if not self.is_subtype(value_type, var_type):
|
|
|
|
|
self.reporter.error(
|
|
|
|
|
location,
|
|
|
|
|
f"Cannot assign {value_type} to variable '{name}' of type {var_type}",
|
|
|
|
|
)
|
|
|
|
|
```,
|
|
|
|
|
caption: [Python Typer: implementation of `visit_assign_stmt` (variable target)]
|
|
|
|
|
) <fig:python-visit_assign_stmt>
|
|
|
|
|
|
|
|
|
|
This is also one of the places our subtyping rules come into play. When assigning to an already defined variable, we check that the value's type is a subtype of the variable's type.#footnote[`PythonTyper.is_subtype` is simply a shortcut for calling `is_subtype` on the types registry], emitting an error diagnostics in case of incompatibility.
|
|
|
|
|
|
|
|
|
|
=== Returns <sec:python-returns>
|
|
|
|
|
|
|
|
|
|
One special control flow statement is the ```py return``` keyword.
|
|
|
|
|
Its effect is twofold. First, it cuts a branch short and any further statement in that branch is skipped. Secondly, it provides a possible return type for the parent function. The latter implies that return statements must appear inside functions.
|
|
|
|
|
|
|
|
|
|
To easily implement the first effect, we will take advantage of exceptions and raise one inside `visit_return_stmt` (named `ReturnException`). We must then catch this exception at the closest branching point, i.e. the entry point of a block. In our case, in addition to a method type checking a single statement (`process_stmt`), we can implement a method to type check a whole block (`process_block`). Inside the latter we can then wrap calls `process_stmt` in a `try`/`except` statement. If a `ReturnException` is caught while processing a block and some statements remain to be processed, we can emit a warning to the user indicating that they will be skipped at runtime.
|
|
|
|
|
|
|
|
|
|
@fig:python-visit_return_stmt shows how the exception is raised while @fig:python-process_block shows how the exception is caught.
|
|
|
|
|
|
|
|
|
|
#figure(
|
|
|
|
|
```python
|
|
|
|
|
def visit_return_stmt(self, stmt: p.ReturnStmt) -> None:
|
|
|
|
|
type: Type = self.type_of(stmt.value) if stmt.value is not None else UnitType()
|
|
|
|
|
self.env.return_types.append(type)
|
|
|
|
|
raise ReturnException(stmt)
|
|
|
|
|
```,
|
|
|
|
|
caption: [Python Typer: implementation of `visit_return_stmt`]
|
|
|
|
|
) <fig:python-visit_return_stmt>
|
|
|
|
|
|
|
|
|
|
#figure(
|
|
|
|
|
```python
|
|
|
|
|
def process_block(self, block: list[p.Stmt], env: Environment) -> bool:
|
|
|
|
|
previous_env: Environment = self.env
|
|
|
|
|
self.env = env
|
|
|
|
|
returned: bool = False
|
|
|
|
|
for i, stmt in enumerate(block):
|
|
|
|
|
try:
|
|
|
|
|
self.process_stmt(stmt)
|
|
|
|
|
except ReturnException:
|
|
|
|
|
returned = True
|
|
|
|
|
if i < len(block) - 1:
|
|
|
|
|
self.reporter.warning(
|
|
|
|
|
block[i + 1].location, "Unreachable statement"
|
|
|
|
|
)
|
|
|
|
|
break
|
|
|
|
|
self.env = previous_env
|
|
|
|
|
return returned
|
|
|
|
|
```,
|
|
|
|
|
caption: [Python Typer: implementation of `process_block`]
|
|
|
|
|
) <fig:python-process_block>
|
|
|
|
|
|
|
|
|
|
The second effect of return statements is executed by @fig:python-visit_return_stmt:3 by recording the return value's type in a list of all return types for the current function.
|
|
|
|
|
|
|
|
|
|
Similarly to how we handled variable assignments in `if` branches (see @fig:resolver-visit_if_stmt), if all sub-branches return, then the parent scope must also return, thus the implementation in @fig:python-visit_if_stmt.
|
|
|
|
|
|
|
|
|
|
#figure(
|
|
|
|
|
```python
|
|
|
|
|
def visit_if_stmt(self, stmt: p.IfStmt) -> None:
|
|
|
|
|
test_type: Type = self.type_of(stmt.test)
|
|
|
|
|
|
|
|
|
|
if (
|
|
|
|
|
not self.is_subtype(test_type, self.types.get_type("bool"))
|
|
|
|
|
and test_type != UnknownType()
|
|
|
|
|
):
|
|
|
|
|
self.reporter.error(
|
|
|
|
|
stmt.test.location, f"If test must be a boolean, got {test_type}"
|
|
|
|
|
)
|
|
|
|
|
|
|
|
|
|
env: Environment = Environment(self.env)
|
|
|
|
|
body_returned: bool = self.process_block(stmt.body, env)
|
|
|
|
|
else_returned: bool = self.process_block(stmt.orelse, env)
|
|
|
|
|
self.env.return_types.extend(env.return_types)
|
|
|
|
|
if body_returned and else_returned:
|
|
|
|
|
raise ReturnException(stmt)
|
|
|
|
|
```,
|
|
|
|
|
caption: [Python Typer: implementation of `visit_if_stmt`]
|
|
|
|
|
) <fig:python-visit_if_stmt>
|
|
|
|
|
|
|
|
|
|
=== Function definitions <sec:python-functions>
|
|
|
|
|
|
|
|
|
|
Function definitions include many components from all kinds of parameters, default values return type hints and their bodies. One particular property is the optionality of return type hints and the potential multiplicity of return statements inside a function body.
|
|
|
|
|
What we want for our type checker is to ensure soundness of return types while helping the user by giving them as much freedom as possible by inferring types where not explicitly given.
|
|
|
|
|
|
|
|
|
|
In the case of functions, this means that the user should be allowed to omit the return type hint and let the type checker infer it from return statements inside the body. To do so, we will implement the following method:
|
|
|
|
|
|
|
|
|
|
#[
|
|
|
|
|
+ Type check the function's body, collecting return types in the environment
|
|
|
|
|
+ If no return statement appears in the body, default to `UnitType`
|
|
|
|
|
+ Try and find a #acr("LUB") of all return types, only in this list of types#footnote[We check whether one of the types in the list is a supertype of all the others]
|
|
|
|
|
+ Unique return supertype?
|
|
|
|
|
- *Yes*: use it as the inferred return type
|
|
|
|
|
- *No*: report an error and use `UnknownType` as the inferred return type
|
|
|
|
|
+ Return type hint ?
|
|
|
|
|
- *Yes*: check that the inferred return type is a subtype of the annotated one, use the type hint as the function's return type
|
|
|
|
|
- *No*: use the inferred return type for the function
|
|
|
|
|
]
|
|
|
|
|
|
|
|
|
|
#codly(
|
|
|
|
|
range: (77, 105),
|
|
|
|
|
smart-skip: true
|
|
|
|
|
)
|
|
|
|
|
#figure(
|
|
|
|
|
python-typer-function-code,
|
|
|
|
|
caption: [Python Typer: function return type inference]
|
|
|
|
|
) <fig:python-function-return-type>
|
|
|
|
|
|
|
|
|
|
The complete implementation of `PythonTyper.visit_function` is listed in @fig:python-visit_function.
|
|
|
|
|
|
|
|
|
|
== Type Checking Expressions <sec:python-check-expr>
|
|
|
|
|
#todo[]
|
|
|
|
|
