Arguments supporting its validity I defined a concretization function linking our abstract domain with the concrete semantics, and I established a paper proof that the operators of the abstract domain are sound. Our abstract domain is able to infer more precise type relationships than the other tools. Once implemented, the modularity of the analysis of functions will provide a significant performance improvement over other static analyzers. The implementation is a work in progress (it does not support the modular analysis yet), and it shows that our analyzer is at least as precise as the state of the art. Python is a big language with a massive standard library, so many features are not supported yet.

. Future work includes developing efficient ways permitting to analyze programs relying on Python's standard library, designing modular analyses of functions and more complex abstract domains.

Static Analysis by Abstract Interpretation

Collecting Types of Python Programs

Raphaël Monat under the supervision of Antoine Miné, APR team, LIP6

March 15 -August 31, 2018

General context Software bugs are costly: they can have disastrous consequences on critical systems, but also on more common applications such as Web servers. It is thus interesting to possess tools helping developers detect those bugs before they ship software into production.

The most common approach to avoid those errors is to use testing, which is inefficient: tests are usually written by hand, taking time, and they cover a few executions of a program, but not all of them.

The approach I undertook during this internship is to design a static analyzer by abstract interpretation for Python. Static analyzers are programs that automatically analyze an input program and report errors this input program may contain (given a certain class of errors the static analyzer may detect). In particular, if a static analyzer is sound and reports no error on a given input, we know that this program does not contain any error from the class the static analyzer is able to discover. Abstract interpretation [START_REF] Cousot | Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[END_REF] is a theory formalizing links between a precise but costly semantics with some computable, approximated counterpart, thus guiding the design and implementation of sound static analyzers.

State of the art static analyzers include Julia [START_REF] Spoto | The Julia Static Analyzer for Java[END_REF] (analyzing Java), Astrée [START_REF] Bertrane | Static Analysis and Verification of Aerospace Software by Abstract Interpretation[END_REF] and Sparrow [START_REF] Oh | Design and implementation of sparse global analyses for C-like languages[END_REF] (for C software). Those are only analyzing statically typed languages. There are no mature static analyzers available for dynamic languages such as JavaScript and Python, although a few static analyses have already been developed and implemented.

def fspath ( p ) :

if isinstance (p , ( str , bytes ) ) : return p elif hasattr (p , " __fspath__ " ) : res = p . __fspath__ () if isinstance ( res , ( str , bytes ) ) : return res else :

raise TypeError ( " ... " ) else :

raise TypeError ( " ... " ) Figure 1: Simplified version of os.fspath

Research problem During this internship, I developed a static analysis of Python programs collecting the types of each variable, and possible type error exceptions. Python is a popular programming language, especially used in teaching and in the scientific community, well-known for its powerful syntax.

Major software projects written in Python include the Django web framework and the SageMath computer algebra system. Python is an object-oriented dynamic language, where every value is an object. Python's dynamism means that undeclared variables, type incompatibilities, . . . are exceptions detected at runtime. Two notions of typing may be used when writing Python programs, and both have operators that may be used at runtime to inspect objects and affect the control-flow, contributing to Python's dynamic nature. Nominal typing is based on the inheritance relation: a class is a subtype of another if its inherits from it. Its associated operator is isinstance, taking an object and a class, and returning true only when the object's class is a subtype of the provided class. Duck typing is more flexible and focuses on attributes. In this setting, an object is a subtype of another if it behaves similarly to the other one, i.e, if the attributes used are the same. hasattr tests if the first parameter has the second parameter as attribute. A typical example of this duality of types is presented in Figure 1. This example is a simplified version of the fspath [2] function defined in the os module of the standard library. This function takes as parameter an object p. If p is already a string (i.e, if it is an instance of str or bytes), it is simply returned. Otherwise, p should have an attribute called __fspath__ (otherwise the TypeError exception at the end is raised), that is called (if it is not a method, another TypeError is raised), and we check that the result is a string as well.

We stress on the fact that we aim at designing a static analysis, and not a type system. The analysis presented here uses an abstract domain of types, and is inspired by works on polymorphic typing and gradual typing, but it is formalized using abstract interpretation, and does not use proofs nor implementation techniques from the world of type systems. This approach differs from the design of a type system in a few different ways we outline now. Contrary to a type system, our analysis will not reject any program, as it reports potential type errors -though it may report false alarms. This is especially useful as type errors may be caught later on during the execution of a Python program, and are potentially not fatal. In the setting of type systems, a more precise type system should reject less programs. Here, a more precise analysis will provide more precise type information, and less false alarms. A soundness proof will be shown in the setting of abstract interpretation, but it is different from a soundness proof of a type system. By reusing abstract domains, our analysis is naturally flow-sensitive, and could be extended to be value-sensitive. The same kind of sensitivity would be non-trivial to achieve using a type system. However, static type analyses of Python are not analyzing functions as modularly as a type system would.

In practice, static analyzers work well when the types of variables are known. There is less work on static analysis of dynamic languages. For Python, a value analysis by abstract interpretation is presented in [START_REF] Fromherz | Static Value Analysis of Python Programs by Abstract Interpretation[END_REF]. Pytype [START_REF]Pytype[END_REF], Typpete [START_REF] Hassan | MaxSMT-Based Type Inference for Python 3[END_REF] and a tool from Fritz and Hage [START_REF] Fritz | Cost versus precision for approximate typing for Python[END_REF] are static analyzers inferring types for Python, but they have not been designed with abstract interpretation. The theoretical part of this work is inspired from Cousot who studied typing of ML-like languages using abstract interpretation [START_REF] Cousot | Types as Abstract Interpretations[END_REF].

We wanted to bring a few novelties by designing a new static type analysis. First, using abstract interpretation, we can provide a proof of soundness linking the concrete semantics of Python with the type analysis. Other works on Python were not stating soundness theorems. While soundness proofs using progress and preservation or logical relations exist for type systems, our proof is a simple inclusion. Second, we used more expressive types, allowing for a more precise analysis. The expressiveness of these types also allows a partially modular analysis of functions, that should bring a performance improvement compared to other tools inlining functions [START_REF]Pytype[END_REF][START_REF] Hassan | MaxSMT-Based Type Inference for Python 3[END_REF][START_REF] Fritz | Cost versus precision for approximate typing for Python[END_REF]. Third, due to the implementation, this analysis supports complex control flow of Python programs. In particular, type errors in Python are raised exceptions that can be caught afterwards, so we wanted to be precise when analyzing exceptionhandling statements. Fourth, we created an analysis that does not restrict Python's language: as an example, thanks to flow-sensitivity of the analysis, variables of both branches of an if statement are not forced to have the same type.

Contribution During this internship, I formalized a new abstract domain permitting a static type analysis of Python programs. This type analysis collects sets of types for each variable (corresponding to the types of the values each variable may have) and type errors. I started by searching into bug reports of Python projects such as Django to find motivating examples. The abstract domain I defined is relational (it can infer relationships between variables), and supports bounded parametric polymorphism. It handles both nominal and duck typing, with a preference for nominal typing, as our types are mainly instances of classes. A partially modular analysis of functions is possible thanks to the polymorphism. In particular, the analysis can express that the function in Figure 1 has for signature α → β, α ∈ { str, bytes, Instance[object, __f spath__] }, β ∈ { str, bytes }. I partially implemented this analysis into a modular static analyzer called MOPSA.

Introduction

I undertook this internship under the supervision of Antoine Miné, in the APR (Algorithms, Programs and Resolution) team, in the LIP6 laboratory. This team works on algorithms and programming languages, on both a theoretical and practical side. Studying concurrent programming languages, programming on new architectures and developing new static analyses are the main research areas of this team. I worked with my supervisor and Abdelraouf Ouadjaout, a post-doc working on the implementation of MOPSA, and in particular on the value analysis of Python programs.

The goal of this internship was to develop a static analysis by abstract interpretation that would find type errors in Python programs. We start by giving some background material on abstract interpretation in Section 2. Then, we propose a concrete semantics for Python, which is mainly based on the semantics of Fromherz et al. [START_REF] Fromherz | Static Value Analysis of Python Programs by Abstract Interpretation[END_REF]. Section 4 defines the abstract domain I developed, allowing for a static type analysis of Python programs. In Section 5 we focus on implementation choices, and on the integration of the analysis into the static analysis framework called MOPSA. We comment on some results provided by the implemented analysis in Section 6. We study the related work in Section 7, and compare our analysis with other static type analyses.

Background on Abstract Interpretation

This part is a short introduction to abstract interpretation. The goal of abstract interpretation is to provide a theory for the approximation of mathematical objects. Most of the time, abstract interpretation applies to the approximation of formal semantics. Using abstract interpretation, we can move from an uncomputable program semantics, called the concrete semantics, to an approximate, computable semantics, called abstract semantics. The latter can then be implemented in a static analyzer. The transition from an uncomputable semantics to a less precise one is provided with guarantees about the approximation of the former semantics by the latter. We will start with a simple example relating P(Z) with intervals, to introduce the main concepts of abstract interpretation. Then, we move to a more elaborate example about static type analysis.

An Abstraction of P(Z) using Intervals

Let us suppose we would like to analyze a program manipulating integers. In that case, we need to represent the set of values each variable may take, so we would like to represent P(Z). If we have variables x and y ranging over values X, Y ∈ P(Z), we can compute the set of values x + y as { x + y | x ∈ X, y ∈ Y }. The problem is that each operation has a cost linear in the size of the input sets, and that the size of the sets is unbounded. Each operation is too costly to perform an efficient program analysis.

An alternative is to use intervals

I = { [a, b] | a ∈ Z ∪ { -∞ }, b ∈ Z ∪ { +∞ }, a ≤ b } ∪ { ⊥ },
where ⊥ represents the empty interval. Of course, intervals will be less precise than elements of P(Z), but each operation has a constant cost, which is much better. Now, if we abstract our sets X and Y by intervals, we would like to have operations such as the addition on intervals as well. Moreover, we would like those interval operations to be sound: if there is z such that z = x + y, x ∈ X, y ∈ Y , we would like z to be in the interval resulting from the interval addition. In this case, intervals act as an overapproximation of a set of integers, and we can find functions converting sets of integers into intervals and conversely.

In 1977, Radhia and Patrick Cousot introduced Abstract Interpretation [START_REF] Cousot | Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[END_REF]. At the heart of this theory is the notion of Galois connection, establishing formally a relationship between an abstract, approximate world and a more concrete world.

Definition 1 (Galois connection). Let (C, ≤) and (A, ) be two partially ordered sets (posets), and α : C → A, γ :

A → C. (α, γ) is a Galois connection if: ∀a ∈ A, ∀c ∈ C, c ≤ γ(a) ⇐⇒ α(c) a This is usually written: (C, ≤) ---→ ← --- α γ (A, ).
C represents the more complicated, concrete object, while A is the simplified, abstracted version. α is called the abstraction function, and γ the concretization function.

Example 2. We use the following order on intervals: ∀x ∈ I, ⊥ x, and

[a, b] [c, d] ⇐⇒ c ≤ a ∧ b ≤ d.
Using this definition, (I, ) is a poset. In our case, we have:

α(∅) = ⊥ γ(⊥) = ∅ α(X) = [inf X; sup X] γ([a, b]) = { x ∈ Z | a ≤ x ≤ b }
We have the following Galois connection:

(P(Z), ⊆) ---→ ← --- α γ (I, ). Proof. Let [a, b] ∈ I, C ∈ P(Z). C ⊆ γ([a, b]) ⇐⇒ ∀c ∈ C, c ∈ γ([a, b]) ⇐⇒ ∀c ∈ C, a ≤ c ≤ b ⇐⇒ a ≤ inf C ∧ sup C ≤ b ⇐⇒ α(C) [a, b]
The case of ⊥ is straightforward:

C ⊆ γ(⊥) ⇐⇒ C = ∅ ⇐⇒ α(C) ⊥
Now, we formally define what a sound abstract operator is:

Definition 3 (Sound operator abstraction). Let γ be a concretization function from an abstract domain (A, ) to a concrete domain (C, ≤). Let f : C → C, and g : A → A. We say that g is a sound abstraction of

f if ∀a ∈ A, f (γ(a)) ≤ γ(g(a)
). Intuitively, this condition says that the concretized result of the abstract operator is an overapproximation of the concrete operator. We can use the definition of Galois connections to see that the best abstraction of an operator f is α • f • γ, thus getting a constructive way to define the best abstraction operators.

Example 4. Let us consider f (X, Y ) = { x + y | x ∈ X, y ∈ Y }. Let [a, b], [c, d] ∈ I (the cases where at least one argument is ⊥ are straightforward). α(f (γ([a, b]), γ([c, d]))) = α({ x + y | a ≤ x ≤ b ∧ c ≤ y ≤ d } = α({ x + y | a + c ≤ x + y ≤ b + d }) = [a + c, b + d] So, f ([a, b], [c, d]) = [a + c, b + d]
is the best abstraction of the addition on intervals. There are other sound abstractions of the addition: for example, f (_, _) = [-∞, +∞] is one, but it is less precise.

Another important concept of abstract interpretation is widening. Widening is an operator accelerating the computation of fixpoints. It does so by extrapolating what it knows. For example, let us consider a while loop incrementing a variable i while i < 1000, we would like to automatically compute the value of i at the end of the loop, assuming that i is initialized to 0. To do so, we would like to find a loop invariant, that is a predicate on i holding whenever the loop body is executed. Supposing that we have a loop invariant I, we want the following equation to hold:

I [i = 0] ∪ S i = i + 1 (C i < 1000 I)
The notation S stmt S is the semantics of stmt, it executes the effect of stmt on the memory state S. C expr filters the input environment to keep the states satisfying expr. We can see that I is a set of memory environments that contains the initial environment (i = 0), and is stable when the loop body is executed (that is, each time the condition is verified and the statement is executed). In particular I = 0 ≤ i ≤ 1000 is a loop invariant, and the tightest one. We can notice that the computation of the tightest loop invariant can be seen as a least fixpoint: I is the least fixpoint of λX.[i = 0] ∪ S i = i + 1 (C i < 1000 X). Thus, the semantics of a while loop can be defined as:

S while e do s done R = C ¬e (lfp λS.R ∪ S s (C e S))

Using a result called Kleene's theorem, we know that we can compute the above least fixpoint as lfp F = ∪ i∈N F i (∅).

Intuitively, this corresponds to executing the body of the loop at most n times, and stopping when the result is stable (here, at n = 1000). However, this computation requires the loop body to be analyzed 1000 times, which is inefficient (even more so if the number of iterations is unbounded). We now define what a widening operator is, we define one on intervals, and we show how it helps in computing loop invariants.

Definition 5 (Widening operator). ∇ : A × A → A is a widening operator on an abstract domain (A, , ) if:

it overapproximates the join: ∀x, y ∈ A, x y x∇y;

it forces convergence in finite time: for any sequence (y i ) i∈N , the sequence x 0 = y 0 , x n+1 = x n ∇y n+1 converges: ∃k, ∀n ≥ k, x k = x n Example 6. We define the following widening operator on intervals:

[a, b]∇[c, d] = a if a ≤ c -∞ otherwise , b if b ≥ d +∞ otherwise
Now, going back to the example of the while loop, let F (X) = [0, 0] ∪ S i = i + 1 (C i < 1000 X) be the semantical interpretation of the while loop, and y i = F i (∅). Using the notations of the previous definition, we have y i = [0, min(i, 1000)]. Applying the widening, we get:

x 0 = [0, 0], x 1 = x 0 ∇y 1 = [0, 0]∇[0, 1] = [0, +∞],
and ∀j ≥ 1, x j = x 1 . So, [0, +∞] is a valid overapproximation of the values of i while in the loop, and we get that after the loop i ∈ [1000, +∞]. To gain back precision, we can perform a decreasing iteration: we inject x 1 back into the loop body F . We see that to enter the loop, i ∈ [0, 999]. After the incrementation, i ∈ [1, 1000], and after applying the loop guard i ∈ [1000, 1000]. Thus, the widening operator accelerates convergence of our computations. This may come with a loss in precision, but in this example, we have seen that we can recover the precise result we wanted using a decreasing iteration.

Static Type Analysis of a Simple Functional Language

Now that we have defined the concepts of Galois connection and soundness of an abstract operator, we show that the semantics of typing of a simple functional language can be seen as an abstraction of the concrete semantics of that same language. This connection is studied in great length in [START_REF] Cousot | Types as Abstract Interpretations[END_REF], we present a simplified case here. Contrary to the previous part where we derived the abstract semantics (on intervals) from the concrete one (on P(Z)), we start by defining the concrete and the abstract semantics before introducing a concretization function and showing the soundness of the abstract semantics with respect to the concrete one.

We study a simple functional language over integers, called FUN, and defined as E in Figure 2. An expression of FUN is either a variable, a binding of a variable to an expression, the application of an expression to another one, an integer, the sum of two expressions, or a conditional expression. The values of FUN are elements of V: they are semantical objects, consisting in integers, functions, or errors (for example if we add a function to an integer). Environments over values are written σ ∈ Σ, they are just mapping from variables to values.

E ::= x ∈ V | fun x → e | e 1 e 2 | z ∈ Z | e 1 + e 2 | if e 1 then e 2 else e 3 V ::= z ∈ Z | λx.f | ω Σ = V → V T ::= int | t 1 → t 2 ∆ = V → T
We define the semantics of FUN in a denotational style in Fig 3 . By definition of the environments, the value of a variable x in a given environment σ is σ(x). Given an environment σ, a function binding variable x to an expression e is interpreted as a function taking an input argument i returning the interpretation of e, in a modified environment σ where x is mapped to i. This modification of the environment corresponds to the substitution by i of x. The semantics of the application is simple: if the first expression e 1 is interpreted as a function, then this function is called with parameter the interpretation of the second expression e. Otherwise, an error is thrown. The semantics of an integer is the corresponding integer, while the interpretation of the addition of two expressions

S expr : Σ → V S x ∈ V σ = σ(x) S fun x → e σ = λi.S e σ[x → i] S e 1 e 2 σ = f [x → S e 2 σ] if S e 1 σ = λx.f ω otherwise S z ∈ Z σ = z S e 1 + e 2 σ = z 1 + z 2 if S e 1 σ = z 1 ∈ Z and S e 2 σ = z 2 ∈ Z ω otherwise S if
T x ∈ V = { δ(x), δ | δ ∈ ∆ } T fun x → e = { m x → m e , δ | (m e , δ[x → m x ]) ∈ T e , m x ∈ T } T e 1 e 2 = { m o , δ | (m 2 , δ) ∈ T e 2 ∧ (m 2 → m o , δ) ∈ T e 1 } T z ∈ Z = { int, δ | δ ∈ ∆ } T e 1 + e 2 = { int, δ | (int, δ) ∈ T e 1 ∩ T e 2 }
T if e 1 then e 2 else e 3 = { (m, δ) | (int, δ) ∈ T e 1 ∧ (m, δ) ∈ T e 2 ∩ T e 3 } Figure 4: Definiton of the abstract semantics of FUN e 1 and e 2 is the sum of these interpretations, provided that both interpretations result in integers (otherwise, an error is thrown). The semantics of conditional statements is straightforward: an error is raised if the conditional expression is not an integer, and otherwise any non-zero integer is interpreted as true, resulting in the execution of the first branch, whereas zero is interpreted as false.

Let us try our semantics on (fun x → fun y → x) 42 43:

S fun x → fun y → x σ = λx i .S fun y → x σ[x → x i ] = λx i .λy i .S x σ[x → x i , y → y i ] = λx i .λy i .x i S (fun x → fun y → x) 42 43 ∅ = (λx i .λy i .x i ) 42 43 = 42
Now, we define the semantics of types for FUN in Fig 4 . It consists in sets of types and environment types (defined as T and ∆ in Figure 2) in which a given expression will not raise any error ω. A variable x has type δ(x), for every possible type environment δ ∈ ∆. The type of a function is an arrow type m x → m e , whenever e has type m e in the type environment δ where x is mapped to type m x . Assuming that e 2 has type m 2 and e 1 has type m 2 → m o , the application of expressions e 1 e 2 has type m o . The type of an integer is int, whatever δ ∈ ∆ is. The type of an addition of two expressions is int, provided that the two expressions are integers as well. The type of a conditional if e 1 then e 2 else e 3 is m, whenever m is the type of both e 2 and e 3 , and whenever e 1 is a valid condition (i.e, e 1 has the integer type). Going back to the example of (fun x → fun y → x) 42 43, we get:

T fun y → x = { (m y → δ(x), δ) | δ ∈ ∆, m y ∈ T } T fun x → fun y → x = { (m x → m e , δ) | (m e , δ[x → m x ]) ∈ T fun y → x , m x ∈ T } = { (m x → m e , δ) | m e = m y → m x , δ ∈ ∆, m x , m y ∈ T } = { (m x → m y → m x , δ) | δ ∈ ∆, m x , m y ∈ T } T (fun x → fun y → x) 42 = { (m o , δ) | (m 2 , δ) ∈ T 42 ∧ (m 2 → m o , δ) ∈ T fun x → fun y → x } = { (m o , δ) | (int → m o , δ) ∈ T fun x → fun y → x } = { (m y → int, δ) | δ ∈ ∆, m y ∈ T } T (fun x → fun y → x) 42 43 = { (int, δ) | δ ∈ ∆ }
We now study the concretization going from the abstract, type based world to the concrete, value-based one. We build the concretizations incrementally, starting from one between values and types. Using these concretizations, we will be able to prove that the semantics of types is a sound abstraction of the concrete semantics of FUN.

γ tv concretizes types into sets of values. As expected, the concretization of integers is the set of integers, while the concretization of functions from t 1 to t 2 is defined recursively as the set of functions that given a value of type t 1 return a value of type t 2 .

γ tv : T → P(V) γ tv (int) = Z γ tv (t 1 → t 2 ) = { λx.f | ∀v 1 ∈ γ tv (t 1 ), f [x → v 1 ] ∈ γ tv (t 2 ) } γ env is just the lifting of γ tv to environments (reminder: ∆ = V → T , Σ = V → V). γ env : ∆ → P(Σ) δ → { σ | ∀x ∈ V, σ(x) ∈ γ tv (δ(x)) }
γ t,env concretizes one type with a given type environment into functions mapping concrete environments to values that respect the type and the type environment. These functions are the semantical interpretations of FUN programs, so we are in a sense, concretizing a type with a type environment into a set of well-typed programs.

γ t,env : T × ∆ → P(Σ → V) (t, δ) → { φ | ∀σ ∈ γ env (δ), φ(σ) ∈ γ tv (t) }
γ concretizes sets of types in their environments to semantical interpretations of FUN programs. In particular, if γ(X) = ∅, this means that the set of types in their environments contains a contradiction. For example, if (int, δ) ∈ X and (t 1 → t 2 , δ) ∈ X, there is no FUN expression having both types, so the result of the concretization is ∅. This previous example shows that defining γ as γ(X) = (t,δ)∈X γ t,env (t, δ) is not what we want, as the contradiction would not be taken into account. Instead, an intersection is necessary to handle the polymorphism that may be expressed by P(T × ∆). For example, the function fun x → x has types X = { (t → t, δ) | δ ∈ ∆, t ∈ T }. While (t, δ) ranges over X, the intersection refines the candidate functions given their types. For example, fun x → 0 is part of γ t,env (int → int, δ), and is kept in the result at this point. However, when considering ((int → int) → (int → int), δ), fun x → 0 will be ruled out.

γ : P(T × ∆) → P(Σ → V) X → (t,δ)∈X γ t,env (t, δ)
Now that γ is defined, we can establish the following soundness theorem:

Theorem 7. T • • • is a sound approximation of S • • • , i.e:
∀expr ∈ E, S expr ∈ γ(T expr )

Proof. By unfolding the definitions of γ and γ t,env , this is equivalent to showing that:

∀expr ∈ E, ∀(t, δ) ∈ T expr , ∀σ ∈ γ env (δ), S expr σ ∈ γ tv (t)
This proof is done by structural induction on the expressions.

-Case x ∈ V: let (δ(x), δ) ∈ T x , σ ∈ γ env (δ). Unfolding γ env , we get that ∀v ∈ V, σ(v) ∈ γ tv (δ(v)).
In particular, we get that S x σ = σ(x) ∈ γ tv (δ(x)).

-Case fun x → e: let m x , m e , δ such that

(m x → m e , δ) ∈ T fun x → e (in particular, (m e , δ[x → m x ]) ∈ T e ). Let σ ∈ γ env (δ), we want to prove that S fun x → e σ = λx i .S e σ[x → x i ] ∈ γ tv (m x → m e ).
We unfold the definition of γ tv : let

v x ∈ γ tv (m x ), we need to show that S e σ[x → v x ] ∈ γ tv (m e ).
By induction hypothesis (with

t, δ = m e , δ[x → m x ]), we get that ∀σ ∈ γ env (δ[x → m x ]), S e σ ∈ γ tv (m e ). As v x ∈ γ tv (m x ), we get σ[x → v x ] ∈ γ env (δ[x → m x ]), so S e σ[x → v x ] ∈ γ tv (m e ).
-Case e 1 e 2 : let m o , m 2 , δ such that (m o , δ) ∈ T e 1 e 2 , and

(m 2 , δ) ∈ T e 2 ∧ (m 2 → m o , δ) ∈ T e 1 . Let σ ∈ γ env (δ), we show that S e 1 e 2 σ ∈ γ tv (m o ). The first induction hypothesis yields S e 1 σ ∈ γ tv (m 2 → m o ) (as (m 2 → m o , δ) ∈ T e 1 ). Unfolding γ tv (m 2 → m o ), we get that S e 1 σ = λx 2 .f , with ∀v 2 ∈ γ tv (m 2 ), f [x 2 → v 2 ] ∈ γ tv (m o ).
Using the second induction hypothesis, we have:

S e 2 σ ∈ γ tv (m 2 ) (as (m 2 , δ) ∈ T e 2 ). Thus S e 1 e 2 σ = f [x 2 → S e 2 σ] ∈ γ tv (m o ). -Case z ∈ Z: let (int, δ) ∈ T z , σ ∈ γ env (δ). S z σ = z ∈ γ tv (int).
-Case e 1 + e 2 : let (int, δ) ∈ T e 1 + e 2 ∩ T e 1 ∩ T e 2 . Let σ ∈ γ env (δ). By induction hypothesis, for all i ∈ { 1, 2 }, S e 1 σ ∈ γ tv (int). Thus S e 1 + e 2 σ = S e 1 σ + S e 2 σ ∈ γ tv (int).

-Case if e 1 then e 2 else e 3 : let (m, δ) ∈ T if e 1 then e 2 else e 3 . We additionally know that (int, δ) ∈ T e 1 , and (m, δ) ∈ T e 2 ∩ T e 3 . Let σ ∈ γ env (δ). By induction hypothesis, we have that S e 1 σ ∈ γ tv (int), and ∀i ∈ { 2, 3 }, S e i σ ∈ γ tv (m). Thus, there exists i ∈ { 2, 3 } such that S if e 1 then e 2 else e 3 σ = S e i σ. In both cases, S e i σ ∈ γ tv (m) Summary This section introduced the main concepts of abstract interpretation, namely Galois connections, sound abstract operators and widening. Subsection 2.1 focused on the abstract domain of intervals I, using a Galois connection, while Subsection 2.2 focused on proving that the semantics of typing was a sound abstraction of the concrete semantics of FUN, using only a concretization function. A useful feature that was used a lot in the last part was to build the concretization functions incrementally and combine them. We will continue to use this incremental approach for both the concretization functions and the definition of abstract operators when defining the type analysis for Python, but we start by introducing the concrete semantics of Python.

Concrete Semantics of Python

The semantics of Python is officially defined as the implementation of Python's official interpreter, called CPython. It is thus not a formal semantics, but just the C code defining CPython. We use a slight evolution from the semantics proposed by Fromherz et al. in [START_REF] Fromherz | Static Value Analysis of Python Programs by Abstract Interpretation[END_REF]. We have changed the semantics to get closer to the real Python language. In the previous semantics, builtin objects such as integers were considered as just a primitive value, without any object structure. A consequence of this restriction was that creating a class inheriting from builtin classes was impossible. In this new semantics, every Python object is represented as a primitive value combined with a representation of the object, so the mentioned limitation is now lifted. We start by defining the memory environment on which a Python program acts, and describe a few parts of the concrete semantics of Python. The rest of the semantics is presented in Appendix B. The memory environment consists in two parts: the environment E and the heap H, formally defined in Figure 5. The environment E is a finite map from variable identifiers Id to addresses Addr. Due to the scope of variables in Python, variable identifiers may also be locally undefined Undef. The heap H maps addresses to tuples of objects Obj and primitive values Val. Although everything is object in Python, we need to keep track of primitive values and store them in the heap. Primitive values are either integers, or strings, or booleans, the None value, or the NotImplemented value. Objects are finite maps from strings (corresponding to attributes and methods) to addresses. To keep track of the complex, non-local control flow of Python programs, while defining semantics by induction on the syntax, we use continuations: in addition to keeping the current state of the analysis, states found before a jump point in the control flow will be kept for later use (for example, the state when an exception is raised will be kept for analysis of later except statements). To store those continuations in the program states, we label states using flow tokens (elements of F), so the states we consider are elements of P(F × E × H) (the semantics of raise and try/except illustrate how these flow tokens may be used, in Figure 24 and Figure 25, Appendix B, page 32 and 33). Flow token cur represents the current flow on which most instructions operate. ret collects the set of states given by a return statement, while brk , cont, exn perform similar collections for the break, continue, raise statements, respectively. We denote by E e the semantics of expression e. This semantics has the following signature: E e : F × E × H → F × E × H × Addr, so E e returns the address where the object associated with e has been allocated. The semantics of statements is written S s and has for signature F × E × H → F × E × H. Note that in the following, both semantics may be implicitly lifted to the powerset.

E def = Id Addr ∪ Undef H def = Addr Obj × Val F def = { cur , ret, brk , cont, exn } Id ⊆ string Obj def = string Addr Val def = Z ∪ string ∪ {True, False, None, NotImpl}
To illustrate the complexity of Python's semantics, we define the semantics of the addition of two expressions e 1 and e 2 in Figure 6. Figure 6 uses the following notation: "letif (f, , σ, a) = ... in ", which unfolds into "let (f, , σ, a) = ... in if f = cur then (f, , σ, a) else ". If the flow token asks for the current evaluation, Python starts by evaluating the expressions e 1 and e 2 . If both expressions evaluate correctly, CPython tries to call the method __add__ of the left argument. If it does not exist or is not implemented, and the types of the evaluated expressions of e 1 and e 2 are not the same, the interpreter tries to call the reflected method __radd__ of the right argument. If none of this works (or the returned result is that the function is not implemented) a TypeError is raised. To show how the flows are handled, we also define the semantics of a variable assignment id = e in Figure 6. The interpreter starts by evaluating the expression e; it then returns the non-current flows found during the evaluation of e, as well as the current flow where the environment is modified to bind id to the address a of the object representing the evaluation of e.

Type Analysis for Python

We define the type abstract domain, before establishing a concretization from the type abstract domain into the concrete environment. We finish by defining some classical abstract operators needed for the type analysis. We opted for an in-depth description of the concretization functions and the abstract operators in subsections 4.2 and 4.3 that we believe is necessary to accurately explain our analysis. In a given Python program, a Python variable may have different types, corresponding to the types of the possible values the variable may hold during any execution of the program, so we are interested in finding the set of possible types for each variable. Moreover, Python programs may catch errors later on during the execution: a program may raise a TypeError in a given context, but this TypeError may be caught later on by an except statement, so we need to collect types of programs. Thus, we are aiming at collecting the set of types of each variable, as well as the type error exceptions. In this regard, our goal is different from the type analysis presented in Section 2.2, which was accepting typable programs and rejecting the others.

E e 1 + e 2 (f, , σ) def = if f = cur then (f, , σ, addr None ) else letif (f 1 , 1 , σ 1 , a 1 ) = E e 1 (f, , σ) in letif (f 2 , 2 , σ 2 , a 2 ) = E e 2 (f 1 , 1 , σ 1 ) in if has_field (a 1 , __add__, σ 2 ) then letif (f 3 , 3 , σ 3 , a 3 ) = E a 1 .__add__(a 2 ) (f 2 , 2 , σ 2 ) in if σ 3 (a 3 ) = (_, NotImpl) then if has_field (a 2 , __radd__, σ 3 ) ∧ typeof (a 1 ) = typeof (a 2 ) then letif (f 4 , 4 , σ 4 , a 4 ) = E a 2 .__radd__(a 1 ) (f 3 , 3 , σ 3 ) in if σ 4 (a 4 ) = (_, NotImpl) then TypeError(f 4 , 4 , σ 4 ) else (f 4 , 4 , σ 4 , a 4 ) else TypeError(f 3 , 3 , σ 3 ) else f 3 , 3 , σ 3 , a 3 else if has_field (a 2 , __radd__, σ 2 ) ∧ typeof a 1 = typeof a 2 then letif (f 3 , 3 , σ 3 , a 3 ) = E a 2 .__radd__(a 1 ) (f 2 , 2 , σ 2 ) in if σ 3 (a 3 ) = (_, NotImpl) then TypeError(f 3 , 3 , σ 3 ) else (f 3 , 3 , σ 3 , a 3 ) else TypeError(f 2 , 2 , σ 2 ) S id = e S def = let S e , A e = E e S in { (f, , σ) | (f, , σ) ∈ S e ∧ f = cur }∪ { (cur , [id] ← a, σ) | (cur , , σ, a) ∈ (S e , A e ) }

Description of the Type Analysis

We start by describing the types a variable may possess. Then, we will define the abstract domain enabling a relational analysis with bounded parametric polymorphism, before giving some examples.

Types The analysis will use both polymorphic and monomorphic types. Polymorphic types are defined in Figure 7. Types can be:

-Top or bottom.

-Class definitions (Eq. ( 2)).

-Standard library containers (such as lists or tuples) holding elements of type v (Eq. ( 3)).

-Instances of another type v that must have some attributes given in AddedAttr and that may have some attributes defined in OptionalAttr. Both AddedAttr and OptionalAttr can be seen as sets of tuples, consisting in attributes with their types. This combination of both an underapproximation (must attributes) and an overapproximation (may attributes) is used to gain precision, and we explain why now. Without an underapproximation of the attributes, we would only know that an attribute may exist. Thus, each attribute access would yield a spurious alarm about an AttributeError, and the analysis would be imprecise. Concerning the need for an overapproximation, let us consider we analyze a conditional statement, where variable x is an instance of a class C that has an attribute a in one branch and variable x is an instance of the same class C without attribute a in the other branch. At the end of the if statement, and due to the flow-sensitivity of our analysis, we would like to have variable x keeping the "union" of both instances. In the concrete, this union would be performed on the two singletons, and would result in a set of length 2. However, this solution is not efficient when describing the abstract operations a static analyzer may perform. In our lattice of types, the abstract union is called the join. Here, if the join is performed (without keeping the overapproximation of attributes), we would get an instance of the class C (as we cannot keep any information on attribute a). This would have the unfortunate consequence of forcing the concretization of a given instance type to be this instance, with arbitrarily many attributes added, resulting in imprecise analyses. Using a combination of an underapproximation and an overapproximation of the attributes, we get that the join is an instance of class C, that may have attribute a. This resolves our precision issues and creates a more precise concretization function, so we keep both approximations.

-Type variables, written using Greek letters (Eq. ( 6)), will be used to express the bounded parametric polymorphism. They will represent sets of types. These type variables are useful to analyze part of Python programs that are polymorphic. For example, let us consider a program where variables x and y have the same type, being either int or float and storing the maximum of both variables into a variable z.

Using type variables, we obtain a very compact representation stating that all three variables have type α ∈ { Instance[int], Instance[f loat] } -the set of monormophic types over which α ranges will be stored in a type variable environment. Moreover, if variables x and y are elements of lists (denoted respectively lx and ly), the type of lx and ly is quite concise: List[α].

-Function summaries (Eq. ( 5)) are used to strike a balance between a fully modular function analysis, and an inlining-based analysis. While the former analysis may be desirable, we would not know anything on the types of the input variables, and the analysis would be too imprecise. The inlining-based analysis offers the best precision but is less efficient. A compromise is to use summaries to memoize the results of the previous analyses of function f . For example, if we go back to the example of os.fspath (Figure 1), and fspath has already been analyzed with a string, the summary would be:

Summary[f spath, [(str, str)]]. Now,
Summary[f spath, [(α, α), (Instance[F oo, __f spath__], str)]] (with α ∈ { str, bytes })
The set of monomorphic types V m , is the set of polymorphic types V , from which type variables V Σ have been removed. We will see that type variables are associated to sets of monomorphic types.

Structure of the abstract domain

The relationality and the bounded parametric polymorphism of our analysis is ensured by splitting our abstract domain into three parts, defined in Figure 8. The relationality of the analysis means that our analysis can express that two variables have the same types.

V = ⊥ | (1) | c, c ∈ Classes (2) | List[v] | T uple[v] | . . . , v ∈ V (3) | Instance[v, AddedAttr, OptionalAttr], v ∈ V (4) | Summary[f, (InputArgs, OutputArgs) list] (5)
| V Σ ∈ { α, β, . . . } (6)
Figure 7: Definition of polymorphic types The first part, D 1 , makes this abstract domain relational by packing variables having the same type into the same group. This partitioning by types is expressed using a mapping from variable identifiers to type identifiers (∈ T ypeId). These partitions can be seen as equivalence classes for the type equality relation. In each equivalence class, we refine the partitions by keeping which variables must alias to each other. In the following, we consider that T ypeId = N and Aliasing = N ⊥ = N ∪ { ⊥ }, where ⊥ stands for variables not aliasing to any other variable.

D = D 1 × D 2 × D 3 D 1 = Id T ypeId × Aliasing D 2 = T ypeId V D 3 = V Σ P(V m )
The second part, D 2 , maps each partition (or each equivalence class) to a polymorphic type. The third part, D 3 , is an environment for polymorphic type variables. It maps each polymorphic type variable (∈ V Σ ) to a set of monomorphic types.

To get a well-formed abstract domain, we impose the following constraints: elements of D 2 and D 3 should be injective mappings. This forces the abstract domain to have an optimal representation. In particular the comparison with T ypeId and equivalence class numbers can be further developed as the first constraint means that two equivalent elements should be in the same equivalence class.

Examples We give two examples of our abstract domain in Table 9.

Example code

Graphical representation Abstract representation

x = A () y = x if * : z = A () else : z = y x, y z Instance[A] d 1 x → (0, 0), y → (0, 0), z → (0, ⊥) d 2 0 → Instance[A] def filter (f , l ) : ret = [] for x in l : if f ( x ) : ret . append ( x ) return ret x l, ret α List[α] {Instance[int], Instance[str]} d 1 x → (0, ⊥), l → (1, ⊥), ret → (1, ⊥) d 2 0 → α, 1 → List[α] d 3 α → {Instance[int], Instance[str]}

Table 9: Examples of abstract elements

We assume that A is a user-defined class. In the first example, variables x and y alias to the same instance of the object A, while variable z is also an instance of A, but it may or may not be aliased to y, depending on the execution of the non-deterministic conditional statement. All three variables have the same type, so d 1 maps each variable to the same partition number which is 0 here. Variable z does not alias, so its aliasing coordinate is ⊥. The concrete environment corresponding to this abstract element is the set of memory environments (x → a, y → a, z → a z ), and the heap contains at most two distinct addresses a and a z pointing to instances of class A.

The second example shows the use of bounded parametric polymorphism. This situation may happen while analyzing a function filtering elements of a list, defined in the first column of Table. 9. l is the input list, x is an element of the list, and ret is the returned list. In that case, we know that x has type α, being either an integer or a string. On the other hand l and ret are either both lists of integers, or both lists of strings. We have two partitions, one being identified with number 0 and the other with number 1. A more concrete representation of this abstract element using only monormophic types is the following:

{ x → Instance[int], l → List[Instance[int]], ret → List[Instance[int]] } ∪ { x → Instance[str], l → List[Instance[str]], ret → List[Instance[str]] }.

Concretization

Due to the structure of the abstract domain, we define the concretization functions incrementally. We start by defining γ v , concretizing monomorphic types into objects having the corresponding type, allocated on the heap at a given address: P(Addr×H). Then γ part concretizes partitions in a given type variable environment (i.e, elements of D 2 × D 3 ) into maps from type identifiers to monotypes, by substituting each type variable by a possible monomorphic type. After that, γ concretizes elements of D into memory environments. All three concretizations are defined in Figure 10.

The definition of γ v stems from the structure of the heap. We define an operator computing addresses and heaps in which an expression e is stored: Ẽ e h = { (a, h) | (cur, _, h, a) ∈ E e (cur, , h ) }. The concretization of an instance of the integer class is any element of Ẽ z h , with z ∈ Z, h ∈ H. The concretization of a list holding elements of type v is the evaluation of any list of arbitrary size, having elements being of type v . c is the inheritance order: a class c is less than d if c inherits from d.

The definition of γ part is more complex, as we want the substitution of type variables to be global on elements of D 2 . If we consider the second example of Figure 9, we want to get two functions:

γ part (d 2 , d 3 ) = { 0 → Instance[int], 1 → List[Instance[int]] } ∪ { 0 → Instance[str], 1 → List[Instance[str]] }. However, we do not want { 0 → Instance[str], 1 → List[Instance[int]]
} to be an element of our concretization function, as this would destroy the purpose of type variables.

In the definition of γ, we want to ensure two things. The first one is that each variable identifier has a good

γ v :                                  V m → P(Addr × H) ⊥ → ∅ → Addr × H Class c → { (a, h) | h(a) = (b, ⊥), b c c } Instance[int] → ∪ h∈H,z∈Z Ẽ int(z) h Instance[Class c, (u 1 : τ 1 , . . . , u n : τ n ), ∅] → { (a, h) | (a, h) ∈ Ẽ c = b(); c.u 1 = t 1 ; . . . ; c.u n = t n ; c h , h ∈ H, ∀1 ≤ i ≤ n, (t i , h) ∈ γ v (τ i ), b c c } Instance[Class c, U, O] → o∈P(O) γ v (Instance[Class c, U ∪ o, ∅]) List[v ] → i∈N,h∈H (a j ,h) 0≤j≤i ∈γv(v ) Ẽ list(a 1 , . . . , a i ) h γ part : D 2 × D 3 → P(T ypeId → V m ) (d 2 , d 3 ) → τ i ∈d 3 (α i ),α i ∈V Σ { λt.d 2 (t)[α i → τ i ] } γ :    D → P(E × H) (d 1 , d 2 , d 3 ) → P ∈γpart(d 2 ,d 3 ) { (e, h) | ∀i ∈ Id, d 1 (i) = (tid, _) =⇒ (e(i), h) ∈ γ v (P (tid))∧ ∀i, j ∈ Id, d 1 (i) = d 1 (j) ∧ snd d 1 (i) = ⊥ =⇒ e(i) = e(j) }
Figure 10: Definition of the concretization of the abstract domain type, while the heap is the same. The second ensures that aliased variables in the abstract are aliased in the concrete memory environment, i.e, they have the same address. Note that aliasing is weak -or equivalently, that we perform a must-alias analysis: if two variables are not explicitly aliased, they may still alias in the concrete. Conversely, if two variables are aliased, they must alias in the concrete. In the case of the example mentioned above, the result of the concretization is the set of memory environments such that variables x, l and ret point to addresses, these addresses respectively pointing to: an integer, a list of integers and a list of integers, or to: a string, a list of strings and a second list of strings.

Abstract Operators

Similarly to concretizations, abstract operators are defined incrementally. However, abstract operators act more locally than the concretization function, so we can define them in a more modular way. As before, we start by working on monomorphic types (V m ). We continue with polymorphic types in a provided type variable environment (V × D 3 , rather than D 2 × D 3 ). Finally, we lift the operator definition to D .

Subset testing This operator is mainly used to check if the analysis of a loop is stabilized or not: in the abstract, the analysis of a loop consists in computing a limit of a function computing a widening. To check if the widening is stable, (using notations of Def. 5) we can weaken the test x n+1 = x n into x n+1 x n (as ∇ overapproximates ).

To test if an element d of D is less than an element d , we check that for every variable v of d, the polymorphic type in d is less than the one in d . The order on polymorphic types p is defined below on V × D 3 , and the type variable environments are left implicit when they are unused.

-∀v ∈ V , ⊥ p v and v p -∀u, v ∈ V , u p v =⇒ List[u] p List[v]
• c p c
• Given a tuple (a, τ ) of an attribute and its type in u, (a, τ ) exists in u and τ p τ

• Given a tuple (a, τ ) in o, (a, τ ) exists in u or o and τ p τ .

-Let α ∈ V Σ , v ∈ V , d 3 , d 3 ∈ D 3 . If ∀m ∈ d 3 (α), (m, d 3 ) p (v, d 3 ), then (α, d 3 ) p (m, d 3 ). -Let α ∈ V Σ , v ∈ V , d 3 , d 3 ∈ D 3 . If v is monormophic, and v ∈ d 3 (α), then (v, d 3 ) p (α, d 3 ). -Let α ∈ V Σ , v ∈ V , d 3 , d 3 ∈ D 3 . If v is not monormophic, and ∀u ∈ γ p (v, d 3 ), (u, d 3 ) p (α, d 3 ), then (v, d 3 ) p (α, d 3 ).
Remark 8 (Lattice of Classes, Nominal Typing). One structure we used during the definition of p is the lattice of classes, (Classes ∪ { ⊥ }, c , ∪ c , ∩ c ). In Python, the top element of this lattice is the object class, as every class inherits from object. The order defined by c is the following: everything is greater than ⊥ and less than object, and a class c is less than c if c inherits from c . The join ∪ c of c and c is defined as the smallest (for c ) class r such that c c r and c c r, while the meet is the biggest of the two. Two graphs showing the inheritance relation for Python are shown in Appendix C, page 34.

Join We show how to define the abstract union operator, called the join. This join is used when multiple control-flow branches that have been analyzed separately need to be merged together (for example, at the end of a conditional statement). This does not happen in a classical type system, but is used in our analysis, due to its flow-sensitivity. The join operator is written ∪ . As the definition of the join on monomorphic types and polymorphic types in a given environment are really similar, we only define the latter, written ∪ v . ∪ v is defined by case analysis:

-(⊥, d 3 ) ∪ v (u, d 3 ) = (u, d 3 ) ∪ v (⊥, d 3 ) = (u, d 3| V ars(u)
), where d 3| V ars(u) is the restriction of d 3 keeping only the type variables used by u.

-( , d 3 ) ∪ v (u, d 3 ) = (u, d 3 ) ∪ v ( , d 3 ) = ( , ∅) -cl ∪ c cl = object =⇒ (Class cl, d 3 ) ∪ v (Class cl , d 3 ) = (Class(cl ∪ c cl ), ∅)
where ∪ c is the least common ancestor of two classes for the inheritance relation.

-

((u, d 3 ) ∪ v (v, d 3 ) = (w, r 3 )) =⇒ (List[u], d 3 ) ∪ v (List[v], d 3 ) = (List[w], r 3 ) -Assuming we have two instances Instance[Class cl, { (u i , τ u i ) }, { (o i , τ o i ) }] and Instance[Class cl , { (u i , τ u i ) } , { (o i , τ o i ) }],
of classes cl and cl such that cl ∪ c cl = object, the result of the join is an instance of a class cl ∪ c cl . The underapproximation of the attributes is the set of attributes that must exist in each instance, with each type being the monormophic join of the two types. The overapproximation of the attributes are the other attributes defined in at least one of the two instances, with each type being the monomorphic join of the two types. The overapproximation of the attributes also contains attributes that are defined by cl or cl , but are not defined in cl ∪ c cl . This set is defined as

A = { (a, τ ) ∈ attrs(cl ∪ c cl ) \ (attr(cl) ∪ attr(cl )) }. More formally: let U = { u i } ∩ { u i } and O = { o i } ∪ { o i } ∪ ({ u i } ∪ { u i }) \ U .
The join of two instances is then:

Instance[Class (cl ∪ c cl ), u∈U,s.t. u=u i =u j { (u, τ u i ∪ v τ u j ) }, o∈O, a,a ∈{ u,o } s.t. o=a i =a j { (o, τ a i ∪ v τ a j ) } ∪ A]
-The join of two summaries of the same function Summary

[f, l 1 ] and Summary[f, l 2 ] is Summary[f, l 1 ∪ l l 2 ],
where ∪ l is the concatenation of two lists where duplicates are removed.

-If none of the cases above apply, we use the following fallback. In this case, u and v are too different types to be joined using one of the previous cases. We make use of the bounded parametric polymorphism to keep both types, by using a fresh type variable α:

(u, d 3 ) ∪ v (v, d 3 ) = α, [α → γ p (u, d 3 ) ∪ γ p (v, d 3 )
]. γ p is the concretization of a polymorphic type, and its definition stems from the one of γ part :

γ p : V × D 3 -→ P(V m ) (v, d 3 ) → { v[α i → τ i ] | α i ∈ V Σ appearing in v, τ i ∈ d 3 (α i ) } Remark 9 (On cl ∪ c cl = object).
The condition cl ∪ c cl = object, used in the cases of the join of two classes or two instances is used to avoid losing too much precision. If two classes have a common parent that is not object, we assume that those classes are still similar enough to be merged into one class. Otherwise, the fallback case will be used, and the two classes will be kept separately using a type variable. This condition could be weakened to perform the join only when a common parent is not "too far" from both classes, and where the fallback case using type variables would be used otherwise.

The proof of soundness of ∪ v is available in Appendix A.1.

To compute the join of two of the types abstract elements (d 1 , d 2 , d 3 ) and (d 1 , d 2 , d 3 ), we proceed roughly as follows. Given the partitions specified by d 1 and d 1 , we compute the intersection of those partitions and store them into r 1 . Then, we iterate over each partition of r 1 . As each partition of r 1 represents just one type identifier for d 1 and for d 1 , we name t and t those type identifiers. We compute the join (d 2 (t), d 3 ) ∪ v (d 2 (t ), d 3 ) of the types for that partition and store it. In the end, the following invariant should hold by construction of the intersection of the partitions:

∀i ∈ Id, (d 2 (d 1 (i)), d 3 ) ∪ v (d 2 (d 1 (i)), d 3 ) p (r 2 (r 1 (i)), r 3 ) (7)
This basically means that for each variable identifier i, the type given by the partition r 1 is more general than the union of the types given by the partition of d 1 and d 1 .

The proof of soundness of the join operator on D is given in Appendix A.2.

Meet The abstract counterpart of the intersection operator is called the meet. It is defined similarly to the join.

Adding a variable To add the fact that variable x has type t in a domain (d 1 , d 2 , d 3 ), we search (in d 2 ) if there is a partition having type t (i.e, we search for i ∈ T ypeId such that d 2 (i) = t). If that is the case, we give back

(d 1 [x → (i, ⊥)], d 2 , d 3 )
. Otherwise, we create a new partition, having a fresh type identifier j ∈ T ypeId, and yield

(d 1 [x → (j, ⊥)], d 2 [j → t], d 3 )
. A similar operator exists to add an equality constraint between two variables (and this time, aliasing has to be taken into account).

Widening As seen in Section 2.1, the widening operator is used to find in a finite number of iterations a (post)fixpoint of a transfer function, such as a loop. For example, if we want to know what type x has after executing x = list(x) n times, we would like to avoid unrolling the loop n times and have an analysis that converges in a small number of steps. The widening operator enjoys an incremental construction similar to that of the join. We describe how to compute x∇y informally. If some partitions given by y are not included in those of x, those partitions are collapsed into one, and mapped to the type. Otherwise, if the partitions are stable but the types are not, we can define a widening on polymorphic types, moving unstable types to . As this widening operator is really unprecise when partitions are unstable, we delay the widening twice, as this may help stabilizing the partitions and result in a more precise analysis. For example, if we have to widen

List[α], α ∈ { Instance[int], Instance[str] } with List[List[Instance[int]]]
, the result will be List[ ]. Another option for this widening operator would be to limit the size of the sets in D 3 : going back to previous example, and assuming that the limit is 4, we would have

List[α]∇List[List[Instance[int]]] = List[β], β ∈ { Instance[int], Instance[str], List[Instance[int]] }. Then, List[β]∇List[List[List[Instance[int]]]] = List[ ].
Filtering Given a condition, filtering operators split a domain into two parts: one where the given condition may be satisfied, and one where the condition may not be satisfied. We defined two filtering operators, handling expressions using isinstance or hasattr. These two filtering operators correspond to the two kinds of typing that may be used in Python, i.e, nominal and duck typing (as mentioned in the cover section). We describe how the instance filtering works on polymorphic types. Given a polymorphic type in a type environment, and a class I, we output two tuples of polymorphic types in their type environment: the first tuple is a subset of the input where all elements are instances of class I, while the second tuple is a subset of the input where all elements are not instances of class I.

-If the input is (⊥, d 3 ) or ( , d 3 ), the output is a copy of the input.

-To filter a list (List[t], d 3 ), we check if the the list class is less than class I using the inheritance order c : if that is the case, the result is (List[t], d 3 ), (⊥, d 3 ), and otherwise the result is (⊥, d 3 ), (List[t], d 3 ).

-Given an instance of a class C, if C c I the first tuple will contain the instance and the second will be at bottom. Otherwise, the two tuples are exchanged.

-Given a polymorphic type variable α in a context d 3 , we proceed as follow: we start by concretizing (using γ p ) the type α, and then we filter this set. The result of this filtering is two sets of types, one being instances of I (called t), and the other not (called f ). Then, we return the type, where the type variable environments have been changed to match t and f , i.e the result is:

(α, d 3 [α → t]), (α, d 3 [α → f ]).
The attribute filtering is quite simple too. Most cases are straightforward. To perform the filtering of classes, we just need to look up the attribute in the class and its parents. To filter an instance I = Instance[c, u, o], we consider the following cases:

1. If the attribute is present in c, we return (I, d 3 ) and (⊥, d 3 ).

2. Otherwise, if the attribute is present in u, we return (I, d 3 ) and (⊥, d 3 ).

3. Otherwise, if the attribute is present in o, we only know that the attribute may be part of the instance, so we have to return (I, d 3 ) and (I, d 3 ).

4. In the last case, we know for sure that the attribute is not present, so we just return (⊥, d 3 ) and (I, d 3 ).

The attribute filtering of a type variable enjoys a construction similar to the instance filtering.

Abstract Semantics

We do not present the abstract semantics of the whole analysis here. It is basically the concrete semantics of Python with abstract operators replacing the concrete ones. For example, parts where the concrete union was used now use the abstract join ∪ , and least fixpoint computations used for loops are replaced by the computation of a limit using a widening operator. In this analysis, the interesting part is the abstract domain on which the analysis relies, rather than the abstract semantics. We will additionally see in Section 5.1 why we do not need to implement again the abstract semantics of Python.

5 Implementation Details

Integration into MOPSA

I implemented the static analysis described in the previous section into a framework called MOPSA (Modular Open Platform for Static Analysis). MOPSA is a work in progress. Its goal is to simplify the construction of static analyzers by offering a modular design. Abstract domains permitting to analyze numerical values, control-flow, pointers, etc. are written separately and are combined during the analysis given a configuration specified by the user. Using this configuration, MOPSA passes statements to each abstract domain until one is capable of analyzing the given statement. MOPSA supports static analysis of different languages which currently are subsets of C and Python. In particular, Python's value analysis [START_REF] Fromherz | Static Value Analysis of Python Programs by Abstract Interpretation[END_REF] has been implemented into MOPSA before my internship.

Due to the modularity of the abstract domains mentioned above, and the implementation of the value analysis of Python into MOPSA, I have been able to reuse some domains dealing with Python constructs. I implemented the abstract domain of types described in the previous section, and the semantics of variable assignments, but I was able to reuse abstract domains handling if statements, while loops, . . . However, the implementation was not straightforward either: some abstract domains were not modular enough, so I have had generalize them (for some), or write an alternative abstract domain compatible with the type analysis. For example, the value analysis used quite concrete addresses (the addresses were abstracted into a finite -but big -set, to be sufficiently precise and to allow a computable analysis), while addresses are abstracted into type identifiers during our analysis. Some abstract domains were not modular in the addresses, and required the addresses used by the value analysis, so I have had to adapt them.

The implementation of the type analysis into MOPSA adds around 1500 lines of OCaml code.

Implementation of the Abstract Domain

The implementation is a bit more involved than the description made in the previous section, although the differences are not of a semantical order but due to implementation and performance concerns. The domain is still a cartesian product of three finite maps, but elements of d 1 do not point to a tuple in T ypeId × Aliasing: if a variable v ∈ Id is aliased with a group of variables v 1 , . . . , v n ∈ Id, the variable with the least identifier (called v * ) is mapped to the type identifier, while all the other variables are mapped to v * . Otherwise, v is mapped to the type identifier. The structure for aliases is currently similar to a union-find but not exactly one. This may be improved in the future if this structure reduces performance; we would then use a union-find structure with fast deletion [START_REF] Amir | A simple and efficient Union-Find-Delete algorithm[END_REF].

To merge the partitions d 1 and d 1 into r 1 , we proceed as follow: we create a mapping H : T ypeId × T ypeId → T ypeId. Given i, a type identifier for a partition in d 1 , and i being the same for d 1 , H(i, i ) represents the type identifier for the partition in r 1 , being the intersection of the partitions i and i . H is updated during the construction of the partitions, meaning that if H(i, i ) is needed but not bound, we create a fresh type identifier n and now use H[(i, i ) → n].

Examples and Experimental Evaluation

A preliminary experimental comparison with other static type analyzers is showed in Table 13. We comment on the results of the analysis on two examples, and delay the comparison to the next section. In this first example (Figure 11), we have a program declaring a class A, and assigning to variable x an instance of A. Then, a non-deterministic choice is done, and y is either aliased to x or assigned to a new instance of A. Afterwards, attribute a is added to the object y points at, and the value of attribute a is the integer 2. Finally, the value of x.a is assigned to z. If y and x are aliased the last assignment z = x.a is valid, as the attribute a has been created at line 6. If y and x are not aliased, then the last assignment will raise an AttributeError. When analyzing this file in MOPSA, the AttributeError is found. In fact, at the end of line 6, we know that: x has type Instance[A, ∅, [a : Instance[int]]], meaning that x is an instance of A that may have attribute a (being an integer), and we know that y has type Instance[A, [a : Instance[int]], ∅], meaning that y is an instance of A that must have attribute a (also an integer). Thus, using these type information, the analyzer is able to conclude that an AttributeError may be raised.

In the second example (Figure 12), a non-deterministic choice is made, and variable x is either an integer or a string, while variable l is either a list of integers or a string. At the end of the analysis, MOPSA finds that x has type α ∈ { Instance[str], Instance[int] }, while l has type List[α]. We can see that variables x and l have been precisely analyzed and related using bounded parametric polymorphism. This example can be expanded: if other non-deterministic choices are made to create new possible types (for example x = [START_REF]Python Enhancement Proposal[END_REF], l = [[2, 3], x]), then the range α would be the only thing to change (into

{ Instance[str], Instance[int], List[Instance[int]] }).
7 Related Work

Typing and Abstract Interpretation

As mentioned in Section 2, [START_REF] Cousot | Types as Abstract Interpretations[END_REF] shows that some kinds of typing for the lambda-calculus can be seen as abstractions of a concrete denotational semantics of lambda-calculus. In that work, some lambda-terms can be untypable, as they will result in errors. In this work, we collect types of programs rather than discard untypable programs, due to Python's capacity to catch errors.

Gradual typing [START_REF] Siek | Gradual Typing for Objects[END_REF] mixes together explicit static typing and dynamic typing: some variables may be statically typed, and others may be typed by the unknown type (written ?), delaying their type checking at runtime (the ? type can be implicitly cast to and from any other type during static type checking). In particular, gradual typing is useful to type programs incrementally. The safety of gradual typing ensures that if a term has a given type, it either reduces to a value of the same type, or a casting error between types has been raised. Using abstract interpretation, Garcia et al. explore a formulation of gradual typing where gradual types such as ? concretize into sets of static types [START_REF] Garcia | Abstracting gradual typing[END_REF]. The approach of [START_REF] Garcia | Abstracting gradual typing[END_REF] ensures type safety by construction. Compared to gradual typing, our approach is purely static. In the worst case, the gradual type ? will correspond to the type of our analysis (and may lead to a high number of false alarms). Contrary to the safety result of gradual typing, if our analysis claims that a program does not contain any type error, no cast error will happen at runtime.

Static Analysis of Other Dynamic Languages

A few static analyses for the JavaScript language have been designed. Contrary to Python, JavaScript is defined by a standard, and its semantics have been formalized in Coq [START_REF] Bodin | A trusted mechanised JavaScript specification[END_REF].

In JavaScript, attributes are always accessed dynamically, so a few different abstract domains for strings where designed and evaluated in [START_REF] Amadini | Combining String Abstract Domains for JavaScript Analysis: An Evaluation[END_REF].

[17] defines a value analysis by abstract interpretation for JavaScript programs. [START_REF] Hackett | Fast and precise hybrid type inference for JavaScript[END_REF] proposes a hybrid type inference engine, performing both a static analysis and runtime checks. In [START_REF] Logozzo | RATA: Rapid Atomic Type Analysis by Abstract Interpretation -Application to JavaScript Optimization[END_REF], Logozzo and Venter use a static type analysis to determine if some numerical variables may be cast from 64-bit floats to 32-bit integers, and optimize the JavaScript code if that is the case, yielding significantly lower running times.

General Static Analysis of Python

In previous work, Fromherz et al. [START_REF] Fromherz | Static Value Analysis of Python Programs by Abstract Interpretation[END_REF] defined a concrete semantics of Python and a value analysis of Python programs by abstract interpretation. This analysis is relational over numerical variables. As such, the analysis developed during this internship is not an abstraction of the value analysis: the analyses are incomparable. The value analysis is more precise in some cases as it keeps tracks of values, and the type analysis can keep track of variable equalities in ways that the value analysis cannot. For example, the value analysis cannot express that variables x and y have the same type, this type being either Instance[C] or Instance [D]. The value analysis is also more costly than the type analysis, and the latter should scale more easily. A future work after this internship is to combine these two analyses, so they can benefit each other.

Typing of Python Programs

Python Ecosystem Python developers have recently been working on adding type annotations to Python programs. Those type hints, defined in the Python Enhancement Proposal 484 [START_REF]Python Enhancement Proposal[END_REF], are purely optional and are just used for documentation and type-checking purposes. There are never used by the interpreter. These type hints are mostly an abstraction of the types used by the analysis we proposed, so we could run our analyzer and then annotate the input program with the type hints our analysis found.

Mypy [START_REF] Mypy | [END_REF] is a static type checker for Python programs using gradual types (without performing the dynamic type checking at runtime). As such, it does not infer types but statically checks that the type hints written in a program are not conflicting. Mypy imposes some restrictions on the input programs: for example, the type of variables cannot change during the execution. Additionally, if a variable is declared in the first branch of an if statement, the type hint should not contradict the use of the same variable in the else branch.

Typeshed [START_REF] Typeshed | [END_REF] provides static types for a part of Python's standard library. It may be useful in the near future to automatically use those type hints to support Python's standard library, although some simplifying assumptions that are made should not be used in our analysis (for example, Python's arbitrary large integers are assumed to be subtype of float in typeshed).

Static Analyzers There are three others static analyzers of Python programs: Typpete [START_REF] Hassan | MaxSMT-Based Type Inference for Python 3[END_REF], Pytype [START_REF]Pytype[END_REF] and a tool from Fritz and Hage [START_REF] Fritz | Cost versus precision for approximate typing for Python[END_REF]. Typpete encodes type inference of Python programs as a SMT problem and lets Z3 solve it. It supports type hints as defined in the PEP 484, so the analysis may be manually guided, contrary to ours. Pytype is a tool developed by engineers at Google, but there is no reference on how it works. We compare the behaviour of these analyzers on a few chosen examples in Table 13. Five examples are taken from Typpete's tests (those are prefixed with in the Program column), and five were handwritten to compare the precision of the four analyzers. means that the analyzer is sound on this example, means that the analyzer is sound, but too unprecise (for example, an integer is declared as being an object), 0 means that the analysis is sound, but a false alarm is generated and means that the analyzer is unsound on this example. False alarms may be due to the analyzer not supporting a feature. For example, Typpete assumes that all attributes are declared statically in the class declaration, and creates a false alarm while analyzing class_attr_ok. The files mentioned in Table 13 are given in Appendix D.

As we can see, the tool from Fritz and Hage and Pytype are unsound on a few programs. Typpete appears to be sound on every example, but it is sometimes unprecise. We can notice that none of the analyzers is capable of analyzing program polyfib correctly (this is due to two facts: the + operator is highly polymorphic and difficult to analyze precisely, and the program calls a recursive function). The false alarms created by our analysis are mainly due to statements that are not supported yet (for example, recursion, iterations on lists, and metaclasses).

Conclusion

We have designed a static type analysis based on abstract interpretation. The abstract domain underlying the analysis is relational, and supports bounded parametric polymorphism. A concretization function explicitly defines what the elements of the abstract domain represent in concrete terms. This type analysis has been partially implemented in the MOPSA static analyzer. Preliminary experimental evaluation shows that this analysis is at least as precise as the state of the art. Future work includes finishing the implementation, supporting a wide range of Python's standard library, and combining this analysis with the value analysis of Fromherz et al.

1. Let i ∈ Id. Let r 1 (i) = (rid, _). Let d 1 (i) = (tid, _). Using Eq. ( 8), we get: (e(i), h) ∈ γ v (P (tid)).

We want to show that (e(i), h) ∈ γ v (P (rid)). Let (τ i ∈ d 3 (α i )) α i ∈V Σ , unfolding the definition of P yields:

P = λt.d 2 (t)[α i → τ i ]. Thus, P (rid) = d 2 (rid)[α i → τ i ]. As d 2 (rid), d 3 ⊇ (d 2 (tid), d 3 ) ∪ v (d 2 (d 1 (i)), d 3 )
, we get that P (rid) ⊇ P (tid), so that (e(i), h) ∈ γ v (P (rid)) (as γ v is monotone).

2. Let i, j ∈ Id, such that r 1 (i) = r 1 (j) and snd r

1 (i) = ⊥. Let a, a , b, b such that r 1 (i) = φ(a, b), r 1 (j) = φ(a , b ). As r 1 (i) = r 1 (j), we get φ(a, b) = φ(a , b
), and by injectivity of φ we can conclude that a = a , so that d 1 (i) = d 1 (j). Using Eq. ( 9), we get that e(i) = e(j).

B Concrete Semantics of Python

As mentioned in Section 3, the concrete semantics of Python described here is a slight evolution from the semantics proposed by Fromherz et al. in [START_REF] Fromherz | Static Value Analysis of Python Programs by Abstract Interpretation[END_REF]. This part is a copy of [START_REF] Fromherz | Static Value Analysis of Python Programs by Abstract Interpretation[END_REF]'s annex, containing minor updates due to the changes on the environment, and some small update on the semantics (especially, on the semantics of attribute accesses). The changes are described in the first paragraph of Section 3. The memory environment consists in two parts: the environment E and the heap H, formally defined in Figure 14. The environment E is a finite map from variable identifiers Id to addresses Addr. Due to the scope of variables in Python, variable identifiers may also be locally undefined Undef. The heap H maps addresses to tuples of objects Obj and primitive values Val. Although everything is object in Python, we need to keep track of primitive values and store them in the heap. Primitive values are either integers, or strings, or booleans, the None value, or the NotImplemented value. Objects are finite maps from strings (corresponding to attributes and methods) to addresses. To keep track of the complex, non-local control flow of Python programs, while defining semantics by induction on the syntax, we use continuations: in addition to keeping the current state of the analysis, states found before a jump point in the control flow will be kept for later use (for example, the state when an exception is raised will be kept for analysis of later except statements). To store those continuations in the program states, we label states using flow tokens (elements of F), so the states we consider are elements of P(F × E × H) (see the semantics of raise and try/except in Figure 24 and Figure 25) Flow token cur represents the current flow on which most instructions operate. ret collects the set of states given by a return statement, while brk , cont, exn perform similar collections for the break, continue, raise statements, respectively.

B.1 Domain

E def = Id Addr ∪ Undef H def = Addr Obj × Val
We denote by E e the semantics of expression e. This semantics has the following signature: E e : (F × E × H) → (F × E × H × Addr), so E e returns the address where e has been allocated. The semantics of statements is written S s and has for signature F × E × H → F × E × H. Note that in the following, both semantics may be implicitly lifted to the powerset.

B.2 Constants

The semantics of constants (Figure 15) returns the address where the constant has been allocated for the current flow, and the address of None for all other flows. We assume that booleans, None and NotImpl are statically allocated, while integers and strings are not (in CPython, things are a bit more complex as integers between -127 and 128 are allocated statically). Allocation of a new address is performed using fa, which returns a new, yet unused address, i.e., in Addr \ dom(σ) (as Addr is infinite).

E True (f, , σ) def = if f = cur then (f, , σ, addr None ) else (f, , σ, addr True ) E False (f, , σ) def = if f = cur then (f, , σ, addr None ) else (f, , σ, addr False ) E i ∈ Z (f, , σ) def = if f = cur then (f, , σ, addr None ) else (f, , σ[fa → (int, i)], fa) E s ∈ string (f, , σ) def = if f = cur then (f, , σ, addr None ) else (f, , σ[fa → (str, s)], fa) E None (f, , σ) def = if f = cur then (f, , σ, addr None ) else (f, , σ, addr None ) E NotImpl (f, , σ) def = if f = cur then (f,

B.3 Expressions

In the rest of the definition of the concrete semantics, we use the following notation: "letif (f, , σ, a) = ... in ", which unfolds into "let (f, , σ, a) = ... in if f = cur then (f, , σ, a) else ".

Figure 16 presents the semantics of tuples. To evaluate a tuple, we evaluate each element from left to right. If an evaluation does not return the current flow (for example, if an exception has been raised), the evaluation is stopped. If all elements have been evaluated successfully, we allocate a new tuple on the heap.

E (e 1 , . . . , e n ) (f, , σ) Figure 17 presents the access to a variable id . If the key id is not present in the map , a NameError exception is constructed and returned, which corresponds to accessing a non-existent variable. If it maps to Undef, then an UnboundLocalError exception is returned instead, which denotes access to a local variable before it has been initialized.

def = if f = cur then (f, , σ, addr None ) else letif (f 1 , 1 , σ 1 , a 1 ) = E e 1 (f, , σ) in . . . letif (f n , n , σ n , a n ) = E e n (f n-1 , n-1 , σ n-1 ) in let σ = σ n [fa] ← (T uple(v 1 , . . . , v n ), ∅) in (f n , n , σ , fa)
E id (f, , σ) def = if f = cur then (f, , σ, addr None ) else if id ∈ dom then NameError(f, , σ) else if (id ) = Undef then UnboundLocalError(f, , σ) else (f, , σ, (id )) NameError(f, , σ) def = let (f 1 , 1 , σ 1 , a 1 ) = E NameError() (f, , σ) in (exn, 1 [exn_var → a 1 ], σ 1 , addr None )
(and similarly for UnboundLocalError and TypeError) An object has several special attributes: a class attribute that points to its class, which is also an object, as well as a mro attribute -for method resolution order -pointing to a list of classes it inherits from. The mro field is used to look up attributes missing in the class -such as inherited methods. We will denote as contains_field the test of whether an object contains a field, without searching in its class and superclasses, and as has_field the test considering the class and superclasses as well. We also recall that lists, functions, generators, classes, and methods are objects; we denote their sets, respectively, as List, Fun, Gen, Class, Method ⊆ Obj. In the following, we denote as Class? v, Fun? v, etc., an operation that tests whether an address v ∈ Addr corresponds to a class, a function, etc.

Figure 18 presents the semantics of accessing an object attribute. We first evaluate the element we are trying to access. If the evaluation is successful, we look for __getattribute__ in the MRO, and try to evaluate it (we know that at least the object class has a __getattribute__ field). If that __getattribute__ fails with an AttributeError, we search for a __getattr__ method in the MRO. If that method does exist we call it; otherwise we just raise an AttributeError. The description of object's __getattribute__ is also given. In that case, we first evaluate the object, and then the attribute. We check that attr is a string, called s. We search for s in the MRO. If the result is a data descriptor (i.e, it has both a __get__ and a __set__), we return that. Otherwise, we search for s in the instance dictionary, and return otherwise the result found during the MRO search. E e.s (f, , σ) Figure 19 presents the semantics of addition and of negation. An addition is implemented by the special method __add__. When evaluating e 1 + e 2 , if e 1 does not support the addition, that is, it does not contain a method __add__ or the method returns NotImpl, and the operands are of different types, we call the reflected method __radd__. If this method is not supported either, the addition is not supported for these objects and we return an exception. Other binary arithmetic operators are similar, replacing respectively __add__ and __radd__ with the corresponding special methods. The negation is slightly simpler, as it only checks for the __neg__ special method. The evaluation of other unary operators is similar, replacing __neg__ with the corresponding special method. Figure 20 presents the semantics of equality ==. The other comparison operators are similar. The evaluation is similar to the addition: If an operation is not supported, we try the reflected operand (__eq__ for __eq__, and __lt__ for __gt__ for instance). If the operands do not have the same type and the right operand's type is a subclass of the left operand's type, we first try the reflected method. Figure 22 presents the semantics of function calls. We first evaluate the called object, and all arguments passed. If these evaluations are successful, the call can now have different effects. If the called object is a function, or a method, we ensure that the number of arguments corresponds to the expected number. If not, a TypeError is raised. If the function called is actually a generator, we create a new generator object on the heap, and set the generator counter to start to indicate that the generator has not been called yet. If not, we execute the body of the function, returning None if no return value was provided. If the called object is a class, we create a new instance of this class, by calling the special method __new__. If __new__ returns an instance of the class, the __init__ method of this new instance is invoked. If __init__ is invoked and does not return a None value, a TypeError is raised. Finally, if none of the above cases apply and the called object emulates a callable object through a __call__ method, we call this method. If not, a TypeError is raised.

def = if f = cur then (f, , σ, None) else letif (f 1 , 1 , σ 1 , v 1 ) = E e (f, , σ) in let c i = mrosearch(v 1 , __getattribute__) in let (f 2 , 2 , σ 2 , v 2 ) = E c i .__getattribute__(v 1 , s) in if f 2 = exn ∧ 2 [exn_var ] = AttributeError then let d i = mrosearch(v 1 , __getattr__) in if Class?d i then let (f 3 , 3 , σ 3 , v 3 ) = E d i .__getattr__(v 1 , s) in if f 3 = exn ∧ 3 [exn_var ] = AttributeError then AttributeError(f 3 , 3 , σ 3 ) else f 3 , 3 , σ 3 , v 3 else AttributeError(f 2 , 2 , σ 2 ) else f 2 , 2 , σ 2 , v 2 E object.__getattribute__(obj, attr) (f, , σ) def = if f = cur then (f, , σ, None) else letif (f 1 , 1 , σ 1 , v 1 ) = E obj (f, , σ) in letif (f 2 , 2 , σ 2 , s) = E attr (f 1 , 1 , σ 1 ) in if str?s then let c i = mrosearch(v 1 , s) in if Class?c i then if contains_f ield(c i .s, __get__) ∧ contains_f ield(c i .s, __set__) then E c i .s.__get__() (f 2 , 2 , σ 2 ) else let (f 3 , 3 , σ 3 , v 3 ) = E v 1 .__dict__[s] in if f 3 = exn ∧ 3 [exn_var ] = KeyError then f 3 , 3 , σ 3 , c i .s else f 3 , 3 , σ 3 , v 3 else let (f 3 , 3 , σ 3 , v 3 ) = E v 1 .__dict__[s] in if f 3 = exn ∧ 3 [exn_var ] = KeyError then AttributeError(f 3 , 3 , σ 3 ) else f 3 , 3 , σ 3 , v 3 else T ypeError(f 2 , 2 , σ 2 )
E e 1 + e 2 (f, , σ) def = if f = cur then (f, , σ, addr None ) else letif (f 1 , 1 , σ 1 , a 1 ) = E e 1 (f, , σ) in letif (f 2 , 2 , σ 2 , a 2 ) = E e 2 (f 1 , 1 , σ 1 ) in if has_field (a 1 , __add__, σ 2 ) then letif (f 3 , 3 , σ 3 , a 3 ) = E a 1 .__add__(a 2 ) (f 2 , 2 , σ 2 ) in if σ 3 (a 3 ) = (_, NotImpl) then if has_field (a 2 , __radd__, σ 3 ) ∧ typeof (a 1 ) = typeof (a 2 ) then letif (f 4 , 4 , σ 4 , a 4 ) = E a 2 .__radd__(a 1 ) (f 3 , 3 , σ 3 ) in if σ 4 (a 4 ) = (_, NotImpl) then TypeError(f 4 , 4 , σ 4 ) else (f 4 , 4 , σ 4 , a 4 ) else TypeError(f 3 , 3 , σ 3 ) else f 3 , 3 , σ 3 , a 3 else if has_field (a 2 , __radd__, σ 2 ) ∧ typeof a 1 = typeof a 2 then letif (f 3 , 3 , σ 3 , a 3 ) = E a 2 .__radd__(a 1 ) (f 2 , 2 , σ 2 ) in if σ 3 (a 3 ) = (_, NotImpl) then TypeError(f 3 , 3 , σ 3 ) else (f 3 , 3 , σ 3 , a 3 ) else TypeError(f 2 , 2 , σ 2 ) E -e (f, , σ) def = if f = cur then (f, , σ, addr None ) else letif (f 1 , 1 , σ 1 , a) = E e (f, , σ) in if has_field (a, __neg__, σ 1 ) then E a.__neg__() (f 1 , 1 , σ 1 ) else TypeError(f 1 , 1 , σ 1 )
E e 1 [e 2 ] (f, , σ) def = if f = cur then (f, , σ, addr None ) else letif (f 1 , 1 , σ 1 , a 1 ) = E e 1 (f, , σ) in letif (f 2 , 2 , σ 2 , a 2 ) = E e 2 (f 1 , 1 , σ 1 ) in if has_field (a 1 , __getitem__) then E a 1 .__getitem__(a 2 ) (f 2 , 2 , σ 2 ) else TypeError(f 2 , 2 , σ 2 )
another state in the current continuation flow. We denote as read _only(v) the function that tests whether the address v corresponds to a builtin object that is not modifiable, such as a frozen set, in order to raise an exception in case of assignment. Figure 24 presents the semantics of statements that store the environment from the current flow into another continuation: return, break, continue, but also exception handing (raise) and generator exit (yield). We denote as inherits_from(v 1 , v 2 ) the function that tests if v 1 is a subclass of v 2 , or if v 1 's type is a subclass of v 2 . When raising an expression e, we set the special variable exn_var to the value of e to propagate the exception to its handler. If the value raised does not inherit from BaseException, a TypeError is raised. Figure 25 gives the definition of compound statements composed of sub-statements: tests, loops, and exception handlers. For exception handling, the try block is first evaluated. If an exception is raised, the first except block is executed. If x 1 is not an exception, i.e., it does not derive from BaseException, this is an error. If it does, we check whether the exception raised by the try block derives from x 1 . If it does, we catch the exception, and evaluate the corresponding block s 1 . If not, we iterate over the other handlers. If the try block was completely executed without interruption, the else block is normally executed.

S pass S

def = S S e S def = { (f, , σ) | (f, , σ, v) ∈ E e S } S id = e S def = let S e , A e = E e S in { (f, , σ) | (f, , σ) ∈ S e ∧ f = cur }∪ { (cur , [id] ← a, σ) | (cur , , σ, a) ∈ (S e , A e ) } S id.s = e S def = let S e , A e = E e S in { (f, , σ) | (f, , σ) ∈ S e ∧ f = cur }∪ { (exn, [exn_var ] ← NameError, σ) | (cur , , σ) ∈ S e ∧ id ßndom }∪ { (exn, [exn_var ] ← UnboundLocalError, σ) | (cur , , σ) ∈ S e ∧ [id] = Undef }∪ { (exn, [exn_var ] ← AttributeError, σ) | (cur , , σ) ∈ S e ∧ read _only( [id]) ∧ [id] = Undef } ∪ { (f 1 , 1 , σ 1 ) | (cur , , σ) ∈ S e ∧ id ∈ dom ∧ [id] = Undef ∧ ¬read _only( [id]) ∧ (f 1 , 1 , σ 1 , _) ∈ E id.__setattr__(s, e) (f, , σ) } S object.__setattr__(obj, attr, expr) S def = if f = cur then (f, , σ, None) else letif (f 1 , 1 , σ 1 , o) = E obj (f, , σ) in letif (f 2 , 2 , σ 2 , a) = E attr (f 1 , 1 , σ 1 ) in letif (f 3 , 3 , σ 3 , e) = E expr (f 2 , 2 , σ 2 ) in if str?a then let c i = mrosearch(o, a) in if Class?c i then if contains_f ield(c i .a, __get__) ∧ contains_f ield(c i .a, __set__) then E c i
S return e S def = let S 1 = return_var ← e S in { (f, , σ) ∈ S 1 | f = cur } ∪ { (ret, , σ) | (cur , , σ) ∈ S 1 } S break S def = { (f, , σ) ∈ S | f = cur } ∪ { (brk , , σ) | (cur , , σ) ∈ S } S continue S def = { (f, , σ) ∈ S | f = cur } ∪ { (cont, , σ) | (cur , , σ) ∈ S } S raise e S def = let S 1 = S exn_var = e S in { (f, , σ) ∈ S 1 | f = cur }∪ { (exn, [exn_var ] ← TypeError, σ) | (cur , , σ) ∈ S 1 ∧ ¬inherits_from( [exn_var ], BaseException) }∪ { (exn, , σ) | (cur , , σ) ∈ S 1 ∧ inherits_from( [exn_var ], BaseException) } S yield i e S def = let S 1 = S yield _var ← e S in { (f, , σ) ∈ S 1 | f = cur , next } ∪ { (yield (i), , σ) | (cur , , σ) ∈ S 1 } ∪ { (cur , , σ) | (next(i), , σ) ∈ S 1 } S s 1 ; s 2 def = S s 2 • S s 1
S if_then_else(e, s 1 , s 2 ) S def = S s 1 (filter (e)(S)) ∪ S s 2 (filter (¬e)(S)) where:

filter (e)(S) def = ∪ (f, ,σ)∈S filter (e)(f, , σ) filter (e)(f, , σ) def = letif (f 1 , 1 , σ 1 , v 1 ) = E e (f, , σ) in letif (f 2 , 2 , σ 2 , v 2 ) = 1 , v 1 , 1 , σ 1 ) in if v 2 = True then {(f 2 , 2 , σ 2 )} else ∅ S while(e, c) S def = let S 0 = { (f, , σ) ∈ S | f / ∈ {brk , cont} } in let S 1 = filter (¬e)(lfp f ) in { (f, , σ) ∈ S 1 | f / ∈ {brk , cont} } ∪ { (cur , , σ) | (brk , , σ) ∈ S 1 } ∪ { (f, , σ) ∈ S 0 | f ∈ {brk , cont} } where:f (S) def = let S 1 = S c (filter (e)(S)) in S 1 ∪ { (cur , , σ) | (cont, , σ) ∈ S 1 } S try_except_else(s try , [(x 1 , s 1 ), . . . , (x n , s n )], s

C Inheritance graph for built-in python classes

The first graph shows built-in python classes, without any exception. The second shows only the exceptions. """ " Return a s t r i n g r e p r e s e n t i n g t h e type o f v e h i c l e t h i s i s . """ r e t u r n ' m o t o r c y c l e ' c a r = Car ( 0 , " " , " " , 2 0 0 4 , 2 0 0 4 ) cp = c a r . s a l e _ p r i c e ( ) t r u c k = Truck ( 1 0 0 0 , " " , " " , 2 0 0 9 , 2 0

Figure 2 :

 2 Figure 2: Definition of the FUN functional language

e 1 then e 2 else e 3 SFigure 3 :

 33 Figure 3: Definition of the concrete semantics of FUN

Figure 5 :

 5 Figure 5: Environment of Python programs

Figure 6 :

 6 Figure 6: Excerpt of the concrete semantics of Python

Figure 8 :

 8 Figure 8: Definition of the abstract domain

-

  ∀cl, cl ∈ Classes, cl c cl =⇒ Class cl p Class cl (where c is the inheritance order for the classes) -Let c, c ∈ v . Instance[c, u, o] p Instance[c , u , o ] if the following conditions are met:

  For example, given a domain d where variable x has a type α ∈ { Instance[bool], Instance[int], Instance[f loat] }, we would get that f ilter_instance(x, int, d) = d , d , where variable x has type α ∈ { Instance[bool], Instance[int] } in d and variable x has type Instance[f loat] in d (because bool is a subclass of int).

Figure 11

 11 Figure 11: class_attr.py

Figure 12 :

 12 Figure 12: poly_lists.py

13 :

 13 Fritz and Hage use a dataflow analysis to collect types for Python. Both Typpete and Pytype are written in Python, while Program Fritz and Hage Pytype Typpete MOPSA -types class_attr_ok 0 Comparison of type inference tools for Python the tool from Fritz and Hage is written in Haskell. In all three cases, the static analyzers proceed by inlining when encountering a function.

F=

  def { cur , ret, brk , cont, exn } Id ⊆ string Obj def = string Addr Val def = Z ∪ string ∪ {True, False, None, NotImpl}

Figure 14 :

 14 Figure 14: Environment of Python programs

Figure 15 :

 15 Figure 15: Concrete semantics of constants

Figure 16 :

 16 Figure 16: Concrete semantics of tuples.

Figure 17 :

 17 Figure 17: Concrete semantics of identifier accesses.

Figure 18 :

 18 Figure 18: Concrete semantics of attribute access.

Figure 19 :

 19 Figure 19: Concrete semantics of addition and negation.

Figure 21 :

 21 Figure 21: Concrete semantics of list access.

  Figure 23: Concrete semantics of atomic statements.

Figure 24 :

 24 Figure 24: Concrete semantics of flow statements.

Figure 26 :

 26 Figure 25: Concrete semantics of composed statements.

#Listing 5 :Listing 7 :Listing 9 :

 579 in the Comparison with Pytype, Typpete and the Tool fromFritz and Hage In the following, the boolean conditions written if * represent a non-deterministic choice. If the analyzer does not evaluate trivial conditions, an expression such as 1 ≥ 0 is sufficient to represent this non-determinism. Listing 2: class_pre_store.py # Coming from Typpete c l a s s A: d e f f ( s e l f ) : r e t u r n B( ) d e f g ( s e l f ) : r e t u r n s e l f . f ( ) . g ( ) c l a s s B(A) : d e f g ( s e l f ) : r e t u r n " s t r i n g " x = A( ) y = x . g ( ) Listing 3: default_args_class # Coming from Typpete c l a s s A: d e f __init__ ( s e l f , x=1) : Coming from Typpete c l a s s MyException ( E x c e p t i o n ) : d e f __init__ ( s e l f ) : s e l f . v a l = 15 t r y : a = 23 r a i s e MyException e x c e p t MyException a s e : b = e . v a l a = b + 2 fspath.py d e f f s p a t h ( p ) : # a s i m p l i f i e d v e r s i o n o f o s . f s p a t h # same example with * * custom * * c l a s s e s would not be a n a l y z a b l e i f i s i n s t a n c e ( p , s t r ) o r i s i n s t a n c e ( p , b y t e s ) : r e t u r n p e l i f h a s a t t r ( p , "__fspath__" ) : r e s = p . __fspath__ ( ) i f i s i n s t a n c e ( r e s , s t r ) o r i s i n s t a n c e ( r e s , b y t e s ) : r e t u r n r e s e l s e : r a i s e TypeError ( "__fspath__ s h o u l d r e t u r n s t r o r b y t e s " ) e l s e : r a i s e TypeError ( " i n p u t s h o u l d have type s t r , b y t e s o r a t t r i b u t e __fspath__ , found type %s i n s t e a d " % type ( p ) .__name__) c l a s s FSPath1 : p a s s c l a s s FSPath2 : d e f __fspath__ ( s e l f ) : r e t u r n 42 c l a s s FSPath3 : d e f __fspath__ ( s e l f ) : r e t u r n " b l i " f 1 = f s p a t h ( " b l a " ) f 2 = f s p a t h ( b ' b l a ' ) f 5 = f s p a t h ( FSPath3 ( ) ) f 3 = f s p a t h ( FSPath1 ( ) ) f 4 = f s p a t h ( FSPath2 ( ) ) i i n [ 1 , 2 , l 2 ] : p a s s L2 = [ 9 , 1 0 , 7 , 1 2 ] f o r i i n [ l 2 + 1 ] : polyfib.py d e f f i b ( n , v0 , v1 ) : i f n <= 0 : r e t u r n v0 e l i f n == 1 : r e t u r n v1 e l s e : r e t u r n f i b ( n-1, v0 , v1 ) + f i b ( n-2, v0 , v1 ) c l a s s AddAbsorb : d e f __add__( s e l f , o t h e r ) : r e t u r n AddAbsorb ( ) i f __name__ == "__main__" : a = f i b ( 6 , 0 , 1 ) b = f i b ( 6 , " " , " " ) c = f i b ( 6 , [ 1 ] , [ [ 1 ] ] ) d = f i b ( 1 0 , AddAbsorb ( ) , [ [ " a " ] ] ) Listing 8: poly_lists.py i f * : x = 1 l = [ 2 , x ] e l i f * : x = " a " l = [ x , " b l a " ] e l s e : x = [ 1 ] l = [ x , [ 2 , 3 ] ] i f i s i n s t a n c e ( x , i n t ) : y = True e l i f i s i n s t a n c e ( x , s t r ) vehicle.py # Coming from Typpete from abc import ABCMeta , a b s t r a c t m e t h o d c l a s s V e h i c l e ( m e t a c l a s s=ABCMeta) : b a s e _ s a l e _ p r i c e = 4000 w h e e l s = 2 d e f v e h i c l e _ t y p e ( s e l f ) :

1 1 )

 1 tp = t r u c k . p u r c h a s e _ p r i c e ( ) m o t o r c y c l e = M o t o r c y c l e ( 5 0 0 0 , " " , " " , 2 0 1 6 , 2 0 1 7 ) mt = m o t o r c y c l e . v e h i c l e _ t y p e ( ) Listing 10: widening.py x = 1 i = 0 w h i l e i < 1 0 0 : x = [ x ] i = i + 1 y = x

  Afterwards, if f spath is called with p being a string, the analysis has already been performed and we can return the result. If f spath is called with p being an instance of bytes, the summary becomes:

if f spath is called with an instance of a class F oo having a method __f spath__ returning a string, we would get: Summary[f spath, [(str, str), (Instance[F oo, __f spath__], str)]].

A Missing Proofs

A.1 Soundness of Join over Polymorphic Types

Proof. We want to prove that ∪ v is an overapproximation of ∪, i.e: ∀t, t , d 3 , d 3 , γ p (t, d 3 ) ∪ γ p (t, d 3 ) p γ p ((t, d 3 ) ∪ v (t , d 3 ))

We prove only some cases: -Fallback case: By definition of γ p , we get:

A.2 Soundness of Join

We now prove the soundness of the join operator on the whole abstract domain: d 3 ) be two abstract domains. In addition to assuming the invariant in Eq. ( 7) holds, we assume that d 2 = d 2 and d 3 = d 3 (this can be easily done by transposing type identifiers and type variables (and substituting accordingly), as both T ypeId and V Σ are infinite sets). Let (r 1 , d 2 , d 3 ) be the result of the join between (d 1 , d 2 , d 3 ) and (d 1 , d 2 , d 3 ). Let φ be a bijection between initial type identifiers and resulting type identifiers: ∀i ∈ Id, φ(d

We show that (e, h) ∈ γ(r 1 , d 2 , d 3 ): Figure 21 presents a list access, which is done by calling the special method __getitem__. We first evaluate the list object, then the index object. If both evaluations are successful, we proceed with the call to the method, if it exists. If not, a TypeError is returned since this operation is not supported. E e(e 1 , . . . , e n ) (f, , σ)

B.4 Statements

The semantics of statements have signature S s : P(F × E × H) → P(F × E × H).

Figure 23 presents the semantics of atomic statements that map a state in the current continuation flow to