Résumé
Dans le troisième cours, nous avons étudié les optimisations dans les compilateurs. Ce sont des transformations de programmes que le compilateur applique automatiquement afin d’améliorer les performances du code engendré. Certaines optimisations s’appliquent sans conditions, mais beaucoup d’autres nécessitent un travail préalable d’analyse statique du programme à compiler, afin d’établir des propriétés vraies de toutes les exécutions du programme et sans lesquelles l’optimisation ne s’appliquerait pas. L’analyse par flux de données (dataflow analysis) est un formalisme classique permettant d’exprimer plusieurs analyses comme des résolutions d’équations de flux guidées par le graphe de contrôle du programme.
Nous avons illustré ces concepts sur une analyse importante, l’analyse de vivacité des variables, et son utilisation pour deux optimisations, l’élimination de code mort et l’allocation de registres. Nous avons ensuite mécanisé en Coq cette analyse, ces deux optimisations et leurs démonstrations de correction sémantique. La caractérisation sémantique de l’analyse de vivacité est intéressante car il s’agit d’une hyper-propriété qui relie deux exécutions d’un même programme dans des états différents.
Finalement, nous avons approfondi le calcul de points fixes de fonctions croissantes, une opération centrale dans de nombreuses analyses statique. Le théorème de Knaster-Tarski montre l’existence de tels points fixes, et une présentation constructive de ce théorème débouche naturellement sur un algorithme de calcul de points fixe.
