sys
1.0.0
Si vous êtes intéressé, consultez la nouvelle réimplémentation (très très très) ici!
Si vous souhaitez installer SYS localement:
--shared option partagée. Voir les fonctions build() et package() dans ce fichier comme un exemple de la façon d'installer Boolector après l'avoir cloné. Sur Arch Linux, vous pouvez simplement installer boolector-git à partir d'AUR.Alternativement, vous pouvez utiliser le dockerfile de Ralf-Philipp Weinmann.
Une fois que toutes les dépendances sont installées, vous devriez pouvoir simplement construire l'outil:
stack build
Une fois que vous avez construit l'outil, vous pouvez construire et exécuter nos tests avec:
stack test
Cela exécutera une version complète plus ou moins de notre suite de tests, ainsi que des tests de régression pour chaque bogue que nous énumèrent dans le document. La suite prend un peu plus de deux minutes sur un ordinateur portable avec 64 Go de RAM et 8 fils. Tous les tests avec une exception --- un bug dont nous avons du mal à suivre --- devraient passer. Si quoi que ce soit échoue, essayez de relancer les tests; Le solveur a peut-être chronométré (cela ne s'est pas produit sur nos machines, mais comme nous ne pouvons pas vous connecter à l'annonymat, c'est une possibilité que cela se produise sur votre machine).
Si vous voulez juste reproduire les résultats du papier et rien d'autre, courez:
stack test --ta '-p End-to-end'
Une fois que vous avez construit l'outil, vous pouvez maintenant l'utiliser pour trouver des bugs!
stack exec sys
L'outil prend plusieurs options:
-d DIR --libdir=DIR directory (or file) to analyze
-e EXTN --extn=EXTN file extension
-c CHECK --check=CHECK checker to run
-d est utilisée pour spécifier le répertoire (contenant les fichiers LLVM) ou un seul fichier LLVM.-e est utilisée pour spécifier l'extension des fichiers à vérifier. Ceci est utile lors de la construction de votre projet avec différents niveaux d'optimisations (par exemple, .ll-O0 pour la construction de débogage avec -O0 et .ll-O0_p pour la production).ll correspond à tous les fichiers *.llO0 correspond à tous les fichiers *.ll-O0 et *.ll-O0_pO1 correspond à tous les fichiers *.ll-O1 et *.ll-O1_pO2 correspond à tous les fichiers *.ll-O2 et *.ll-O2_pO3 correspond à tous les fichiers *.ll-O3 et *.ll-O3_pOg correspond à tous les fichiers *.ll-Og et *.ll-Og_pOs correspond à tous les fichiers *.ll-Os et *.ll-Os_pOz correspond à tous les fichiers *.ll-Oz et *.ll-Os_zprod correspond à tous les fichiers *_pany correspond à tous les fichiers-c est utilisée pour spécifier le vérificateur à exécuter, l'un des:uninit : vérificateur de mémoire non initialiséheapoob : vérificateur malloc oobconcroob : Vérificateur d'index négatifuserinput : vérificateur d'entrée utilisateur Pour trouver le bug d'accès à la mémoire non initialisé que notre outil a trouvé dans la bibliothèque PRIO de Firefox:
$ stack exec sys -- -c uninit -e prod -d ./test/Bugs/Uninit/Firefox/serial.ll-O2_p
L'outil signale deux bogues. Regardons le premier:
Stack uninit bug
Name "serial_read_mp_array_73"
in
Name "serial_read_mp_array"
path-to-file
[UnName 4,UnName 71]
Si vous inspectez la fonction Serial_Read_MP_Array (), le chemin de bloc buggy est %4 (le premier bloc) à %71 , où nous utilisons [ %73 ].
Nous n'avons pas testé (et ne testerons probablement pas) SYS sur autre chose que Arch Linux. Nous sommes heureux d'intégrer des correctifs qui ajoutent du support pour d'autres systèmes d'exploitation et de construction!
├── 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
