sturdy
1.0.0
Sturdy é uma biblioteca para criar análises estáticas sólidas em Haskell. Análises estáticas são ferramentas que produzem informações sobre programas de computador sem realmente executar o programa. Exemplos de análises estáticas são verificadores de tipo, localizadores de bugs (por exemplo, Java FindBugs), análises de segurança (por exemplo, análises de mancha) e análises usadas para otimizações do compilador.
Este projeto se concentra em análises estáticas sonoras . Uma análise estática é sólida se os resultados da análise refletirem o comportamento real do tempo de execução do programa e os usuários podem confiar nos resultados. Por exemplo, se uma análise estática usada para otimizações do compilador não fosse doida, a otimização pode alterar a semântica do programa, o que leva a um comportamento inesperado em tempo de execução. Para esse fim, Sturdy segue a teoria das provas de solidez da composição de intérpretes abstratos e componentes sólidos e reutilizáveis para a interpretação abstrata para simplificar as provas da solidez das análises estáticas.
Robusta fatoriza o intérprete de concreto e o intérprete abstrato (a análise estática) em um intérprete genérico . Esse intérprete genérico é parametrizado por interfaces que contêm operações primitivas que descrevem a semântica do idioma, como try , catch e finally para exceções. O intérprete concreto e abstrato instanciam o intérprete genérico implementando essas interfaces. Essa reorganização não apenas separa diferentes preocupações na implementação da análise estática, mas também simplifica sua prova de solidez. Mais detalhes podem ser encontrados em nosso papel ICFP.
O robusto permite construir análises estáticas modularmente a partir de componentes de análise reutilizável. Cada componente de análise encapsula uma única preocupação de análise e pode ser comprovado que um som independentemente da análise onde é usada. Além disso, a teoria dos componentes da análise garante que uma análise estática seja sólida, se todos os seus componentes de análise forem sólidos. Isso significa que os desenvolvedores de análise não precisam se preocupar com a solidez, desde que reutilizem componentes de análise de som. Mais detalhes podem ser encontrados em nosso artigo Oopsla.
Para construir, instale a ferramenta de construção da pilha e execute stack build no diretório raiz do projeto.
O projeto robusto atualmente contém intérpretes concretos e abstratos e genéricos para os seguintes idiomas:
Para executar os testes de um idioma específico, use stack test sturdy-$(lang) , por exemplo,
stack test sturdy-pcf
Algoritmos de Fixpoint baseados em combinadores para intérpretes abstratos de grande etapa
Sven Keidel, Sebastian Erdweg, Tobias Hombücher
Conferência Internacional sobre Programação Funcional (ICFP). ACM, 2023. [PDF]
Interpretadores de definição abstrato modular para WebAssembly
Katharina Brandl, Sebastian Erdweg, Sven Keidel, Nils Hansen
Conferência Europeia sobre Programação Orientada a Objetos (ECOOP). ACM, 2023. [PDF]
Uma abordagem sistemática para a interpretação abstrata das transformações do programa
Sven Keidel e Sebastian Erdweg.
Verificação, verificação do modelo e interpretação abstrata (VMCAI). Springer, 2020. [PDF]
Componentes som e reutilizáveis para interpretação abstrata
Sven Keidel e Sebastian Erdweg.
Programação, sistemas, idiomas e aplicativos orientados a objetos (OOPSLA). ACM, 2019 [PDF] [Talk]
Provas de solidez da composição de intérpretes abstratos
Sven Keidel, Casper Bach Poulsen e Sebastian Erdweg.
Conferência Internacional sobre Programação Funcional (ICFP). ACM, 2018 [PDF] [Talk]
O projeto robusto é um esforço conjunto das seguintes pessoas (em ordem alfabética):
Casper Bach Poulsen, Jente Hidskes, Matthijs Bijman, Sarah Müller, Sebastian Erdweg, Sven Keidel, Tobias Hombücher, Wouter Raateland
