En informática , la corrección del compilador es la rama de la informática que se ocupa de intentar demostrar que un compilador se comporta de acuerdo con la especificación de su lenguaje . [ cita requerida ] Las técnicas incluyen desarrollar el compilador usando métodos formales y usando 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 demostrar la corrección del compilador para todas las entradas y demostrar la corrección de una compilación de un programa en particular (validación de la 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 . [1] Sin embargo, dado que la herramienta para encontrar la prueba (demostrador 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 verifique la prueba (un corrector de pruebas ) que, debido a que es mucho más simple que un buscador de pruebas, 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 . [2] [3] [4]
Otro compilador verificado se desarrolló en el proyecto CakeML, [5] que establece la corrección de un subconjunto sustancial del lenguaje de programación ML estándar utilizando el HOL (asistente de prueba) .
Otro enfoque para obtener un compilador formalmente correcto es utilizar la generación de compiladores dirigida por semántica. [6]
Validación de la traducción: corrección del compilador en un programa dado
A diferencia de intentar demostrar que un compilador es correcto para todos los programas de entrada válidos, la validación de la traducción [7] tiene como objetivo establecer automáticamente que un programa de entrada dado se compila correctamente. Demostrar 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 la traducción puede reutilizar una implementación de compilador existente generando, para una compilación determinada, una prueba de que la compilación fue correcta. La validación de la traducción se puede utilizar incluso con un compilador que a veces genera código incorrecto, siempre que este incorrecto no se manifieste para un programa determinado. Dependiendo del 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, si la validación de la traducción tiene éxito, entonces se garantiza que el programa compilador sea correcto para todas las entradas.
Pruebas
Las pruebas representan una parte importante del esfuerzo de envío de un compilador, pero reciben relativamente poca cobertura 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 nombrados. [8] La edición de 2006 omite la sección sobre pruebas, pero enfatiza su importancia: “¡La optimización de los compiladores es tan difícil 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 ". [9] Fraser & Hanson 1995 tiene una breve sección sobre pruebas de regresión ; el código fuente está disponible. [10] Bailey & Davidson 2003 cubren la prueba de llamadas a procedimientos [11] Varios artículos confirman que muchos compiladores publicados tienen errores importantes de corrección de código. [12] Sheridan 2007 es probablemente el artículo de revista más reciente sobre pruebas generales de compiladores. [13] Para la mayoría de los propósitos, el mayor cuerpo de información disponible sobre las pruebas de compiladores son las suites de validación Fortran [14] y Cobol [15] .
Otras técnicas comunes cuando se prueban compiladores son fuzzing [16] (que genera programas aleatorios para tratar de encontrar errores en un compilador) y reducción de casos de prueba (que intenta minimizar un caso de prueba encontrado para hacerlo más fácil de entender). [17]
Ver también
- Compilador
- Verificación y validación (software)
- Corrección (informática)
- Compilador de C de CompCert: compilador de C verificado formalmente
- Reflexiones sobre la confianza en la confianza
Referencias
- ^ De Millo, RA; Lipton, RJ; Perlis, AJ (1979). "Procesos sociales y pruebas de teoremas y programas". Comunicaciones de la ACM . 22 (5): 271–280. doi : 10.1145 / 359104.359106 .
- ^ Leroy, X. (2006). "Certificación formal de un compilador back-end o: programación de un compilador con un asistente de pruebas". Avisos ACM SIGPLAN . 41 : 42–54. doi : 10.1145 / 1111320.1111042 .
- ^ Leroy, Xavier (1 de diciembre de 2009). "Un compilador back-end formalmente verificado". Revista de razonamiento automatizado . 43 (4): 363–446. arXiv : 0902.2137 . doi : 10.1007 / s10817-009-9155-4 . ISSN 0168-7433 .
- ^ "CompCert - El compilador de CompCert C" . compcert.inria.fr . Consultado el 21 de julio de 2017 .
- ^ "CakeML: una implementación verificada de ML" .
- ^ Stephan Diehl, Generación de compiladores y máquinas abstractas dirigida por semántica natural , Aspectos formales de la informática, vol. 12 (2), Springer Verlag, 2000. doi : 10.1007 / PL00003929
- ^ Pnueli, Amir; Siegel, Michael; Cantante, Eli. Validación de traducción . Herramientas y Algoritmos para la Construcción y Análisis de Sistemas, IV Congreso Internacional, TACAS '98.
- ^ Compiladores: principios, técnicas y herramientas , infra 1986, p. 731.
- ^ ibíd., 2006, p. dieciséis.
- ^ Christopher Fraser; David Hanson (1995). Un compilador de C retardable: diseño e implementación . Editorial Benjamin / Cummings. ISBN 978-0-8053-1670-4., págs. 531–3.
- ^ Mark W. Bailey; Jack W. Davidson (2003). "Detección y Diagnóstico Automático de Averías en Código Generado para Llamadas a Procedimientos" (PDF) . Transacciones IEEE sobre ingeniería de software . 29 (11): 1031–1042. CiteSeerX 10.1.1.15.4829 . doi : 10.1109 / tse.2003.1245304 . Archivado desde el original (PDF) el 28 de abril de 2003 . Consultado el 24 de marzo de 2009 ., pag. 1040.
- ^ Por ejemplo, Christian Lindig (2005). "Prueba aleatoria de convenciones de llamadas de C" (PDF) . Actas del Sexto Taller Internacional sobre Depuración Automatizada . ACM. ISBN 1-59593-050-7. Archivado desde el original (PDF) el 11 de julio de 2011 . Consultado el 24 de marzo de 2009 ., y Eric Eide; John Regehr (2008). "Los volátiles están mal compilados y qué hacer al respecto" (PDF) . Actas de la 7ª conferencia internacional ACM sobre software integrado . ACM. ISBN 978-1-60558-468-3. Consultado el 24 de marzo de 2009 .
- ^ Flash Sheridan (2007). "Prueba práctica de un compilador C99 mediante comparación de resultados" (PDF) . Software: práctica y experiencia . 37 (14): 1475–1488. doi : 10.1002 / spe.812 . Consultado el 24 de marzo de 2009 . Bibliografía en http://pobox.com/~flash/compiler_testing_bibliography.html . Consultado el 13 de marzo de 2009 . Falta o vacío
|title=
( ayuda ) . - ^ "Fuente de la suite de validación de Fortran" . Consultado el 1 de septiembre de 2011 .
- ^ "Fuente de la suite de validación Cobol" . Consultado el 1 de septiembre de 2011 .
- ^ Chen, Yang; Groce, Alex; Zhang, Chaoqiang; Wong, Weng-Keen; Fern, Xiaoli; Eide, Eric; Regehr, John (2013). Domando Fuzzers del compilador . Actas de la 34ª Conferencia ACM SIGPLAN sobre diseño e implementación de lenguajes de programación . PLDI '13. Nueva York, NY, EE.UU .: ACM. págs. 197–208. CiteSeerX 10.1.1.308.5541 . doi : 10.1145 / 2491956.2462173 . ISBN 9781450320146.
- ^ Regehr, John; Chen, Yang; Cuoq, Pascal; Eide, Eric; Ellison, Chucky; Yang, Xuejun (2012). Reducción de casos de prueba de errores del compilador C . Actas de la 33ª Conferencia ACM SIGPLAN sobre diseño e implementación de lenguajes de programación . PLDI '12. Nueva York, NY, EE.UU .: ACM. págs. 335–346. doi : 10.1145 / 2254064.2254104 . ISBN 9781450312059.