sys
1.0.0
Si está interesado, ¡consulte la nueva reimplementación (muy, muy, muy, muy, muy)!
Si desea instalar SYS localmente:
--shared . Vea las funciones build() y package() en este archivo como un ejemplo de cómo instalar boolector después de clonarlo. En Arch Linux, solo puede instalar boolector-git desde AUR.Alternativamente, puede usar DockerFile de Ralf-Philipp Weinmann.
Una vez que tenga todas las dependencias instaladas, debería poder construir la herramienta:
stack build
Una vez que construyó la herramienta, puede construir y ejecutar nuestras pruebas con:
stack test
Esto ejecutará una versión completa más o menos de nuestro conjunto de pruebas, junto con pruebas de regresión para cada error que enumeremos en el documento. La suite toma un poco más de dos minutos en la computadora portátil con 64 GB de RAM y 8 hilos. Todas las pruebas con una excepción --- Un error cuya fuente tenemos problemas para rastrear --- deberían pasar. Si algo más falla, intente volver a ejecutar las pruebas; El solucionador puede haberse agotado (esto no ha sucedido en nuestras máquinas, pero dado que no podemos darle un inicio de sesión para el anonimato, es una posibilidad de que suceda en su máquina).
Si solo desea reproducir los resultados del papel y nada más, ejecute:
stack test --ta '-p End-to-end'
¡Una vez que construyó la herramienta, ahora puede usarla para encontrar errores!
stack exec sys
La herramienta toma varias opciones:
-d DIR --libdir=DIR directory (or file) to analyze
-e EXTN --extn=EXTN file extension
-c CHECK --check=CHECK checker to run
-d se usa para especificar el directorio (que contiene los archivos LLVM) o un solo archivo LLVM.-e se usa para especificar la extensión de los archivos para verificar. Esto es útil al construir su proyecto con diferentes niveles de optimizaciones (por ejemplo, .ll-O0 para la construcción de depuración con -O0 y .ll-O0_p para la producción).ll coincide con todos los archivos *.llO0 coincide con todos los archivos *.ll-O0 y *.ll-O0_pO1 coincide con todos los archivos *.ll-O1 y *.ll-O1_pO2 coincide con todos los archivos *.ll-O2 y *.ll-O2_pO3 coincide con todos los archivos *.ll-O3 y *.ll-O3_pOg coincide con todos los archivos *.ll-Og y *.ll-Og_pOs coincide con todos los archivos *.ll-Os y *.ll-Os_pOz coincide con todos los archivos *.ll-Oz y *.ll-Os_zprod coincide con todos los archivos *_pany coincide con todos los archivos-c se usa para especificar el verificador para ejecutar, uno de:uninit : verificador de memoria no inicializadoheapoob : verificador de OOB de mallocconcroob : CHECKER DE OOB DE INDEXA NEGOTOuserinput : Verificador de entrada de usuario Para encontrar el error de acceso de memoria no inicializado que nuestra herramienta encontró en la biblioteca Prio de Firefox:
$ stack exec sys -- -c uninit -e prod -d ./test/Bugs/Uninit/Firefox/serial.ll-O2_p
La herramienta marca dos errores. Veamos el primero:
Stack uninit bug
Name "serial_read_mp_array_73"
in
Name "serial_read_mp_array"
path-to-file
[UnName 4,UnName 71]
Si inspecciona la función serial_read_mp_array (), la ruta de bloque de errores es %4 (el primer bloque) a %71 , donde usamos [ %73 ].
No hemos probado (y probablemente no probemos) SYS en nada más que Arch Linux. ¡Sin embargo, nos complace integrar parches que agregan soporte para otros sistemas de OSS y construcción!
├── 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
