sys
1.0.0
Se você estiver interessado, confira a (muito muito) nova reimplementação aqui!
Se você deseja instalar o SYS localmente:
--shared . Consulte as funções build() e package() neste arquivo como um exemplo de como instalar o Boolector depois de cloná -lo. No Arch Linux, você pode simplesmente instalar boolector-git a partir do AUR.Como alternativa, você pode usar o Dockerfile de Ralf-Philipp Weinmann.
Depois de instalar todas as dependências, você poderá apenas construir a ferramenta:
stack build
Depois de criar a ferramenta com a qual você pode construir e executar nossos testes:
stack test
Isso executará uma versão completa mais ou menos do nosso conjunto de testes, juntamente com os testes de regressão para todos os bugs que listamos no artigo. A suíte leva um pouco mais de dois minutos no laptop com 64 GB de RAM e 8 fios. Todos os testes com uma exceção-um bug cuja fonte estamos tendo problemas para rastrear-deve passar. Se alguma coisa falhar, tente executar novamente os testes; O solucionador pode ter tempo escapado (isso não aconteceu em nossas máquinas, mas como não podemos lhe dar um login para o anonimato, é uma possibilidade de que isso aconteça na sua máquina).
Se você deseja apenas reproduzir os resultados do papel e nada mais, execute:
stack test --ta '-p End-to-end'
Depois de criar a ferramenta, agora você pode usá -la para encontrar bugs!
stack exec sys
A ferramenta leva várias opções:
-d DIR --libdir=DIR directory (or file) to analyze
-e EXTN --extn=EXTN file extension
-c CHECK --check=CHECK checker to run
-d é usada para especificar o diretório (contendo os arquivos LLVM) ou um único arquivo LLVM.-e é usada para especificar a extensão dos arquivos para verificar. Isso é útil ao criar seu projeto com diferentes níveis de otimizações (por exemplo, .ll-O0 para depuração Build com -O0 e .ll-O0_p para produção).ll corresponde a todos os arquivos *.llO0 corresponde a todos os arquivos *.ll-O0 e *.ll-O0_pO1 corresponde a todos os arquivos *.ll-O1 e *.ll-O1_pO2 corresponde a todos os arquivos *.ll-O2 e *.ll-O2_pO3 corresponde a todos os arquivos *.ll-O3 e *.ll-O3_pOg corresponde a todos os arquivos *.ll-Og e *.ll-Og_pOs corresponde a todos os arquivos *.ll-Os e *.ll-Os_pOz corresponde a todos os arquivos *.ll-Oz e *.ll-Os_zprod corresponde a todos os arquivos *_pany correspondência todos os arquivos-c é usada para especificar o verificador para ser executado, um de:uninit : Verificador de memória não inicializadoheapoob : verificador de Malloc oobconcroob : Índice Negativo OOB verificadoruserinput : verificador de entrada do usuário Para encontrar o bug de acesso à memória não inicializado que nossa ferramenta encontrou na biblioteca PRIO do Firefox:
$ stack exec sys -- -c uninit -e prod -d ./test/Bugs/Uninit/Firefox/serial.ll-O2_p
A ferramenta sinaliza dois bugs. Vejamos o primeiro:
Stack uninit bug
Name "serial_read_mp_array_73"
in
Name "serial_read_mp_array"
path-to-file
[UnName 4,UnName 71]
Se você inspecionar a função Serial_read_mp_array (), o caminho do bloco de buggy será %4 (o primeiro bloco) a %71 , onde usamos [ %73 ].
Não testamos (e provavelmente não testará) Sys em nada além do Arch Linux. Estamos felizes em integrar patches que adicionam suporte para outros sistemas operacionais e construções!
├── app -- Executable used to run the checkers
├── src
│ ├── Checkers -- Static and symbolic checkers
│ ├── Control -- Logging helpers
│ ├── LLVMAST -- LLVM AST interface
│ ├── InternalIR -- Internal IR used to represent paths for both static and symex
│ ├── Static -- Static checker DSL
│ └── Symex -- Symbolic DSL and execution engine
├── community -- Community files
└── test -- Tests
