Exactitude du compilateur

En informatique , la correction du compilateur est la branche de l'informatique qui consiste à essayer de montrer qu'un compilateur se comporte conformément à sa spécification de langage . Les techniques incluent le développement du compilateur à l'aide de méthodes formelles et l'utilisation de tests rigoureux (souvent appelés validation du compilateur) sur un compilateur existant.

Les deux principales approches de vérification formelle pour établir l'exactitude de la compilation sont la preuve de l'exactitude du compilateur pour toutes les entrées et la preuve de l'exactitude d'une compilation d'un programme particulier (validation de la traduction).

La validation du compilateur avec des méthodes formelles implique une longue chaîne de logique formelle et déductive . Cependant, comme l'outil de recherche de la preuve ( démonstrateur de théorème ) est implémenté dans un logiciel et est complexe, il y a une forte probabilité qu'il contienne des erreurs. Une approche a consisté à utiliser un outil qui vérifie la preuve (un vérificateur de preuve ) qui, parce qu'il est beaucoup plus simple qu'un détecteur de preuve, est moins susceptible de contenir des erreurs.

Un exemple frappant de cette approche est CompCert , qui est un compilateur d'optimisation formellement vérifié d'un grand sous-ensemble de C99 .

Un autre compilateur vérifié a été développé dans le projet CakeML, qui établit l'exactitude d'un sous-ensemble substantiel du langage de programmation ML standard à l'aide du HOL (assistant de preuve) .

Une autre approche pour obtenir un compilateur formellement correct consiste à utiliser la génération de compilateur dirigée par la sémantique.

Contrairement à la tentative de prouver qu'un compilateur est correct pour tous les programmes d'entrée valides, la validation de traduction vise à établir automatiquement qu'un programme d'entrée donné est compilé correctement. Prouver la compilation correcte d'un programme donné est potentiellement plus facile que de prouver qu'un compilateur est correct pour tous les programmes, mais nécessite toujours un raisonnement symbolique, car un programme fixe peut toujours fonctionner sur des entrées arbitrairement grandes et s'exécuter pendant une durée arbitrairement longue. La validation de traduction peut réutiliser une implémentation de compilateur existante en générant, pour une compilation donnée, une preuve que la compilation était correcte. La validation de traduction peut être utilisée même avec un compilateur qui génère parfois du code incorrect, tant que cette erreur ne se manifeste pas pour un programme donné. Selon le programme d'entrée, la validation de traduction peut échouer (parce que le code généré est erroné ou que la technique de validation de traduction est trop faible pour montrer l'exactitude). Cependant, si la validation de traduction réussit, le programme compilé est alors assuré d'être correct pour toutes les entrées.

Les tests représentent une part importante de l'effort de livraison d'un compilateur, mais sont relativement peu traités dans la littérature standard. L'édition 1986 de Aho, Sethi et Ullman comporte une section d'une seule page sur les tests de compilateur, sans exemples nommés. L'édition 2006 omet la section sur les tests, mais souligne son importance : « Les compilateurs optimaux sont si difficiles à réaliser correctement que nous osons dire qu'aucun compilateur optimisant n'est complètement exempt d'erreurs ! Ainsi, l'objectif le plus important dans l'écriture d'un compilateur est qu'il soit correct. » Fraser et Hanson 1995 comportent une brève section sur les tests de régression ; le code source est disponible. Bailey et Davidson 2003 couvrent les tests des appels de procédure Un certain nombre d'articles confirment que de nombreux compilateurs publiés présentent des bogues importants en matière de correction du code. Sheridan 2007 est probablement l'article de journal le plus récent sur les tests généraux des compilateurs. et Cobol constituent le plus grand corpus d'informations disponibles sur les tests de compilateur .

D'autres techniques courantes lors des tests de compilateurs sont le fuzzing (qui génère des programmes aléatoires pour essayer de trouver des bugs dans un compilateur) et la réduction des cas de test (qui essaie de minimiser un cas de test trouvé pour le rendre plus facile à comprendre).