Symbiotic 7: Integration of Predator and More

Symbiotic 7 brings improvements in all parts of the tool. In particular, we integrated the advanced shape analysis implemented in Predator to our instrumentation process for memory safety checking. Further, we extended our slicer to correctly handle non-terminating programs. This new slicing is applied in termination analysis, where we also added instrumentation for detection of simple cycles in the program state space. The witness generation process changed as well. 1 Verification Approach Symbiotic 7 follows the same basic schema as all previous versions [4,5]: the program to be verified is first instrumented (if needed), then reduced by static program slicing, and finally symbolically executed using Klee [2]. We describe the main modifications since Symbiotic 5 (participating in SV-COMP 2018) as modifications in Symbiotic 6 (competing in 2019) have not been published. Memory safety checking improvements Symbiotic uses a static pointer analysis to detect instructions that can potentially violate memory safety. To check these instructions, Symbiotic 5 [5,3] instrumented the program with code that keeps records about allocated memory and uses the records to assert the validity of potentially misbehaving instructions. Then we sliced the program with respect to these assertions and called Klee to check assertion validity. Since Symbiotic 6, we slice the program directly with respect to the potentially misbehaving instructions without inserting any additional code. Then we call Klee to check memory safety of the sliced program. Symbiotic 7 newly integrates Predator [6], a static analyzer specialized on memory safety. We first run Predator in its over-approximating mode and M. Chalupa, T. Jašek, P. Ayaziová, and J. Strejček have been supported by the Czech Science Foundation grant GA18-02177S. M. Hruška, V. Šoková, and T. Vojnar have been supported by the IT4Innovations Excellence in Science project (LQ1602) and the FIT BUT internal project FIT-S-20-6427. Jury member and corresponding author: chalupa@fi.muni.cz. c © The Author(s) 2020 A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12079, pp. 413–417, 2020. https://doi.org/10.1007/978-3-030-45237-7_31 in a configuration that analyses all branches in the given program and tries to recover from found errors. If Predator says that the program is safe, we simply answer true. Otherwise, we take bug reports from Predator and combine them with results of our static pointer analysis to get a more precise (i.e., smaller) set of potentially misbehaving instructions. Then we proceed like Symbiotic 6. Symbiotic 7 is also the first version that can distinguish between validmemcleanup and valid-memtrack properties. To do this, our clone of Klee now reconstructs the shape of memory at the program exit if unfreed memory is found: Klee starts with local and global variables and resolves pointers in these (if any). Then it resolves pointers in the pointed memory, etc. This way we can find out if the unfreed memory is reachable via a chain of dereferences or not. Termination analysis Symbiotic 6 introduced a simple support for termination property: a call to VERIFIER error is inserted before trivial infinite loops, e.g., while (true); loops. If the symbolic execution detects that such a call is reachable, Symbiotic answers false as the program can reach an infinite loop. If all paths of the program are explored by symbolic execution without reaching any of these calls, all program executions are clearly terminating and we answer true (an infinite program path cannot be fully explored by symbolic execution). Note that program slicing was disabled for non-termination checking in Symbiotic 6 as the slicer could remove infinite loops in some specific cases. Symbiotic 7 brings two improvements. First, since we extended our slicer to correctly handle non-terminating programs [7], we now apply slicing with slicing criteria set to all exit points (including the instrumented error calls) of the program. Second, we instrument the program with checks for simple cycles in the state space. The instrumentation detects non-nested loops with a single entry for which it can conservatively determine a set {V1, . . . , Vk} that includes all variables potentially modified by the loop. At the beginning of the loop body, we insert assignments that store the value of each variable Vi into a new variable V ′ i . At the end of the loop body, we insert the assertion assert(V1 = V ′ 1 ∨ . . .∨Vk = V ′ k) to check a change in the vector of these variables. If this assertion is violated, the program has a non-terminating execution. Error path replay Although the slicer in Symbiotic now provides algorithms that preserve non-termination properties of programs, outside the Termination category we still use the original non-termination insensitive slicing as it may remove more instructions. The price is, however, that Symbiotic may report false alarms: an unreachable error location situated below an infinite loop may become reachable when the loop is sliced out. To fix this issue, we try to reproduce each error found by symbolic execution in the original (unsliced) program. If the error is reproduced, we report it as a real error. Otherwise, we say unknown. Improved witness generation Symbiotic 5 and 6 generated violation witnesses that describe only the initialization of non-deterministic variables at the 414 M. Chalupa et al.