Seminar details

Abstract: Some compilation passes require semantic information on programs. In a verified compilation pipeline, that information needs to be formally proved. This thesis proposes to propagate properties proven at the source level instead of recovering them through analyses. Our first contribution is the definition of a new intermediate representation, called Frag IR, which enables encoding semantic information. This encoding leverages two features of the representation. Firstly, dependent types encode relations between several variables. This approach tracks the hypotheses from which information is derived and makes some transformations reversible. Secondly, Frag IR has a non-standard memory model, without global state. Instead, some program variables store fragments of the memory. This memory model enables encoding aliasing information and dependencies between memory accesses. Frag IR and its meta-theory are formalized within the proof assistant Rocq. Moreover, we implement and prove correct a compilation pipeline from Frag IR to a more standard low-level representation. This pipeline implements memory fragments with a global memory thanks to a defensive verification of their linear usage. As an example of use, we connect the verified compiler Vélus as a front-end of the pipeline, thanks to a translation from one of its representations (Obc, an imperative language) to Frag IR. Our second contribution is a Rocq axiomatization of monads used to define denotational semantics. We use a relational approach to reason on those semantics. This approach enables proving multiple transformations, including inter-procedural ones and loop transformations. Our axiomatization abstracts over the effect of the semantics. It is thus possible to perform a single proof for the same transformation on semantics with different effects. We give a model of the axiomatization, based on transition systems and supporting several effects: divergence, events, non-determinism, and undefined behaviors. We use this axiomatization to define a parameterized intermediate representation in functional Static Single Assignment. By instantiating this representation, we define languages with different effects. Our formalization of Frag IR is one of those instances. We implemented several verified passes on the parameterized representation, including a type-checker, a Dead Code Elimination, and a block-sinking transformation. Those passes have themselves a few parameters, corresponding to parts specific to the instances. By implementing those parameters, we obtain those passes on the instances, in particular on Frag IR.
Jury:
+ Steve ZDANCEWIC, Prof U.Penn, Rapporteur.
+ Matthieu LEMERRE, Ingénieur HDR CEA Saclay, Rapporteur.
+ Delphine DEMANGE, MdC U.Rennes, Examinatrice.
+ Lydie DU BOUSQUET, Prof UGA, Examinatrice.
+ Guillaume MELQUIOND, DR Inria Lyon, Examinateur.
+ Basile PESIN, Mdc ENAC, Examinateur.
+ David MONNIAUX, DR CNRS Verimag, Directeur de thèse.
+ Sylvain BOULMÉ, MdC Grenoble INP, co-directeur de thèse (invité).