Corrección del compilador

En informática, la corrección del compilador es la rama de la informática que se ocupa de tratar de demostrar que un compilador se comporta de acuerdo con la especificación de su lenguaje. Las técnicas incluyen el desarrollo del compilador utilizando métodos formales y el uso de pruebas rigurosas (a menudo llamadas validación del compilador) en un compilador existente.

Verificación formal

Dos enfoques principales de verificación formal para establecer la corrección de la compilación son probar la corrección del compilador para todas las entradas y probar la corrección de una compilación de un programa en particular (validación de traducción).

Corrección del compilador para todos los programas de entrada.

La validación del compilador con métodos formales implica una larga cadena de lógica deductiva formal. Sin embargo, dado que la herramienta para encontrar la prueba (probador de teoremas) está implementada en software y es compleja, existe una alta probabilidad de que contenga errores. Un enfoque ha sido utilizar una herramienta que verifica la prueba (un verificador de prueba) que, debido a que es mucho más simple que un buscador de prueba, es menos probable que contenga errores.

Un ejemplo destacado de este enfoque es CompCert, que es un compilador de optimización verificado formalmente de un gran subconjunto de C99.

Otro compilador verificado se desarrolló en el proyecto CakeML, que establece la corrección de un subconjunto sustancial del lenguaje de programación Standard ML utilizando HOL (asistente de prueba).

Otro enfoque para obtener un compilador formalmente correcto es utilizar la generación de compiladores dirigida por semántica.

Validación de traducción: corrección del compilador en un programa dado

En contraste con intentar probar que un compilador es correcto para todos los programas de entrada válidos validación de traducción tiene como objetivo establecer automáticamente que un programa de entrada dado se compila correctamente. Probar la compilación correcta de un programa dado es potencialmente más fácil que probar que un compilador es correcto para todos los programas, pero aún requiere un razonamiento simbólico, porque un programa fijo aún puede funcionar con entradas arbitrariamente grandes y ejecutarse durante un período de tiempo arbitrariamente largo. La validación de traducción puede reutilizar una implementación de compilador existente al generar, para una compilación dada, una prueba de que la compilación fue correcta. La validación de traducción se puede usar incluso con un compilador que a veces genera código incorrecto, siempre que este incorrecto no se manifieste para un programa determinado. Según el programa de entrada, la validación de la traducción puede fallar (porque el código generado es incorrecto o la técnica de validación de la traducción es demasiado débil para mostrar la corrección). Sin embargo,

Pruebas

Las pruebas representan una parte significativa del esfuerzo de envío de un compilador, pero reciben una cobertura comparativamente pequeña en la literatura estándar. La edición de 1986 de Aho, Sethi y Ullman tiene una sección de una sola página sobre pruebas de compiladores, sin ejemplos con nombre. La edición de 2006 omite la sección sobre pruebas, pero enfatiza su importancia: “¡Los compiladores de optimización son tan difíciles de acertar que nos atrevemos a decir que ningún compilador de optimización está completamente libre de errores! Por lo tanto, el objetivo más importante al escribir un compilador es que sea correcto”. Fraser & Hanson 1995 tiene una breve sección sobre pruebas de regresión; el código fuente está disponible. Bailey & Davidson 2003 cubren las pruebas de llamadas a procedimientos Varios artículos confirman que muchos compiladores publicados tienen importantes errores de corrección de código. Sheridan 2007 es probablemente el artículo de revista más reciente sobre pruebas generales de compiladores. Para la mayoría de los propósitos, el mayor cuerpo de información disponible sobre las pruebas del compilador son las suites de validación de Fortran y Cobol.

Otras técnicas comunes cuando se prueban compiladores son el fuzzing (que genera programas aleatorios para tratar de encontrar errores en un compilador) y la reducción de casos de prueba (que intenta minimizar un caso de prueba encontrado para que sea más fácil de entender).