On Static Analysis for Expressive Pattern Matching

Pattern matching is a widespread programming language construct that enables definitions of values by cases, generalizing if-then-else and case statements. The cases in a pattern matching expression should be exhaustive: when the value does not match any of the cases, the expression throws a run-time exception. Similarly, each pattern should be reachable, and, if possible, patterns should be disjoint to facilitate reasoning. Current compilers use simple analyses to check patterns. Such analyses ignore pattern guards, use static types to approximate possible expression values, and do not take into account properties of user-defined functions. We present a design and implementation of a new analysis of pattern matching expressions. Our analysis detects a wider class of errors and reports fewer false alarms than previous approaches. It checks disjointness, reachability, and exhaustiveness of patterns by expressing these conditions as formulas and proving them using decision procedures and theorem provers. It achieves precision by propagating possible values through nested expressions and approximating pattern-matching guards with formulas. It supports user-defined ``extractor'' functions in patterns by relying on specifications of relationships between the domains of such functions. The result is the first analysis that enables verified, declarative pattern matching with guards in the presence of data abstraction. We have implemented our analysis and describe our experience in checking a range of pattern matching expressions in a subset of the Scala programming language.

Design and implementation of an optimizing type-centric compiler for a high-level language

Dmytro Petrashko

Production compilers for programming languages face multiple requirements. They should be correct, as we rely on them to produce code. They should be fast, in order to provide a good developer experience. They should also be easy to maintain and evolve. This thesis shows how an expressive high level type system can be used to simplify the development of a compiler and demonstrates this on a compiler for Scala. First, it shows how expressive types of high level languages can be used to build internal data structures that provide a statically checked API, ensuring that important properties hold at compile time. Second, we also show how high level language features can be used to abstract the components of a compiler. We demonstrate this by introducing a type-safe layer on top of the bytecode emission phase. This makes it possible to abstract away the implementation details of the compiler frontend and run the same bytecode emission phase in two different Scala compilers. Third, it presents MiniPhases, a novel way to organize transformation passes in a compiler. MiniPhases impose constraints on the organization of passes that are beneficial for maintainability, performance, and testability. We include a detailed performance evaluation of MiniPhases which indicates that their speedup is due to improved cache friendliness and to a lower rate of promotions of objects into the old generations of garbage collectors. Finally, we demonstrate how the expressive type system of the language being compiled can be used for static analysis. We present a novel call graph construction algorithm which uses the typing context for context sensitivity. The resulting algorithm is both substantially faster and more precise than existing alternatives. We demonstrate the applicability of this analysis by extending common subexpression elimination to idempotent expression elimination.

EPFL2017

Compiling scala for the Java virtual machine

Michel Schinz

Scala is a new programming language developed at EPFL and incorporating the most important concepts of object-oriented and functional languages. It aims at integrating well with the Java and .NET platforms: their respective libraries are accessible without glue code, and the compiler can produce programs for both virtual machines. This thesis focuses on the compilation of two important concepts of Scala : mixin inheritance and run time types. The compilation techniques are presented in the context of the Java virtual machine, but could be adapted easily to other similar environments. Mixin inheritance is a relatively recent form of inheritance, offering new capabilities compared to single inheritance, without the complexity of multiple inheritance. We propose two implementation techniques for mixin inheritance: code copying and delegation. The implementation used in the Scala compiler is then presented and justified. Run time types make it possible for a program to examine the type of its values during execution. This possibility is interesting in itself, offering new capabilities to the programmer. Furthermore, run time types are also required to implement other high level concepts, like pattern matching, type-safe serialisation and reflection. We propose an implementation technique based on the representation of types as values, and show how to use the run time types of the underlying virtual machine to implement those of Scala. The techniques presented in this thesis have been implemented in our Scala compiler, scalac. This enabled us to evaluate these techniques, in particular their impact on the performances of programs. This evaluation was performed on several real, non-trivial programs.

EPFL2005

Compiling Regular Patterns to Sequential Machines

Burak Emir

Pattern matching combined with regular expressions has many applications including text and XML processing, lexical analysis, classification of DNA segments and content-based routing. Patterns contain variables to refer to parts of the matching input. But regular patterns pose the problem of ambiguity: Words can be matched against 'overlapping' sections of the pattern in several ways, yielding different variable bindings. A match policy like shortest or longest match disambiguates the outcome of matching. In order to implement the longest/shortest match policies, we propose to compile regular patterns to sequential machines. This intuitive approach %to resolving ambiguities by means of shortest/longest match %policies (and the slightly different ungreedy/greedy match), with lets us derive a compilation scheme with linear runtime complexity. \par The main contributions of this paper are firstly, a decision procedure for unambiguous regular patterns, which can be matched with a single traversal of the input, and secondly, algorithms to obtain deterministic sequential machines from ambiguous patterns. These produce the shortest(longest) match in two consecutive runs. The first run produces an intermediary result from which all possible variable bindings can be reproduced. The second run then chooses the unique binding which adheres to the given match policy. In the general case, this approach is optimal.

2004

Design and implementation of an optimizing type-centric compiler for a high-level language

Dmytro Petrashko

EPFL2017