sturdy
1.0.0
Sturdy es una biblioteca para crear análisis estáticos sólidos en Haskell. Los análisis estáticos son herramientas que producen información sobre programas de computadora sin ejecutar realmente el programa. Ejemplos de análisis estáticos son los comprobantes de tipo, los buscadores de errores (por ejemplo, Java FindBugs), análisis de seguridad (por ejemplo, análisis de Taint) y análisis que se utilizan para las optimizaciones del compilador.
Este proyecto se centra en los análisis estáticos sólidos . Un análisis estático es sólido si los resultados del análisis reflejan el comportamiento real de tiempo de ejecución del programa y los usuarios pueden confiar en los resultados. Por ejemplo, si un análisis estático utilizado para las optimizaciones del compilador no fuera sana, la optimización podría cambiar la semántica del programa, lo que conduce a un comportamiento inesperado en tiempo de ejecución. Con este fin, Sturdy sigue la teoría de las pruebas de solidez de composición de los intérpretes abstractos y los componentes de sonido y reutilizables para la interpretación abstracta para simplificar las pruebas de solidez de los análisis estáticos.
Sturdy factoriza el intérprete concreto y el intérprete abstracto (el análisis estático) en un intérprete genérico . Este intérprete genérico es parametrizado por interfaces que contienen operaciones primitivas que describen la semántica del lenguaje, como try , catch y finally para excepciones. El intérprete concreto y abstracto luego instancia al intérprete genérico implementando estas interfaces. Esta reorganización no solo desacopla diferentes preocupaciones en la implementación del análisis estático, sino que también simplifica su prueba de solidez. Se pueden encontrar más detalles en nuestro documento ICFP.
Sturdy permite construir análisis estáticos modularmente a partir de componentes de análisis reutilizables. Cada componente de análisis encapsula una sola preocupación de análisis y puede demostrarse que suena independientemente del análisis donde se usa. Además, la teoría de los componentes de análisis garantiza que un análisis estático sea sólido, si todos sus componentes de análisis son sólidos. Esto significa que los desarrolladores de análisis no tienen que preocuparse por la solidez siempre que reutilen los componentes de análisis de sonido. Se pueden encontrar más detalles en nuestro artículo de Oopsla.
Para construir, instale la herramienta de compilación de la pila y ejecute stack build desde el directorio raíz del proyecto.
El proyecto resistente actualmente contiene intérpretes concretos, abstractos y genéricos para los siguientes idiomas:
Para ejecutar las pruebas de una stack test sturdy-$(lang) , por ejemplo,
stack test sturdy-pcf
Algoritmos FixPoint basados en combinador para intérpretes abstractos de gran paso
Sven Keidel, Sebastian Erdweg, Tobias Hombücher
Conferencia internacional sobre programación funcional (ICFP). ACM, 2023. [PDF]
Intérpretes de definición abstractos modulares para websembly
Katharina Brandl, Sebastian Erdweg, Sven Keidel, Nils Hansen
Conferencia europea sobre programación orientada a objetos (ECOOP). ACM, 2023. [PDF]
Un enfoque sistemático para la interpretación abstracta de las transformaciones del programa
Sven Keidel y Sebastian Erdweg.
Verificación, verificación de modelos e interpretación abstracta (VMCAI). Springer, 2020. [PDF]
Componentes sólidos y reutilizables para interpretación abstracta
Sven Keidel y Sebastian Erdweg.
Programación, sistemas, idiomas y aplicaciones orientadas a objetos (OOPSLA). ACM, 2019 [PDF] [Talk]
Pruebas de solidez de composición de intérpretes abstractos
Sven Keidel, Casper Bach Poulsen y Sebastian Erdweg.
Conferencia internacional sobre programación funcional (ICFP). ACM, 2018 [PDF] [Talk]
El proyecto resistente es un esfuerzo conjunto de las siguientes personas (en orden alfabético):
Casper Bach Poulsen, Jente Hidskes, Matthijs Bijman, Sarah Müller, Sebastian Erdweg, Sven Keidel, Tobias Hombücher, Wouter Raateland
