List DILS vous invite à son événement
À propos de cet événement
Frama-C is an open-source extensible and collaborative platform dedicated to source-code analysis of C software. Its first steps are to parse, type, transform and normalize C code into an abstract syntax tree more suitable to be analyzed called Cil. However, instead of performing all those steps separately, using an intermediate AST for each compilation pass, the entire process is implemented as one huge pass, which leads to challenges in maintainability and scalability, even more as Frama-C aims to support multiple languages in the future.
However, minimizing the number of intermediate representations is not without merit. Indeed, for each representation, one would need to maintain all the tools needed to create, manipulate, edit and visit the AST, which could become a huge burden, especially if each new supported language brings its intermediate representations.
Our work is thus focused on splitting the compilation process into several simpler passes without multiplying the number of intermediate representations. We do so using a new AST that relies on OCaml's GADTs to encode for each construction which passes it can exist in, inspired by Catala's approach. All intermediate representations are thus combined into a unique AST, and one can see each pass using the type system as a way to "specialize" it.
In this presentation, we present our prototype on a subset of C.
Proposé par
Le CEA est un organisme de recherche sur la défense et la sécurité, les énergies nucléaire et renouvelables, la recherche technologique pour l’industrie et la recherche fondamentale en sciences de la matière et de la vie.
