< Retour au sommaire

Toward multi-language support in Frama-C : Unify compilation steps using GADTs

Thibault Martin le

Lieu: Salle 1073

Suivre en visio

Abstract

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.