Symbiotic 5: Boosted Instrumentation

The basic approach of Symbiotic remains unchanged [7]: it uses instrumentation to reduce checking of specific properties (e.g. no-overflow or memory safety) to checking reachability of error locations. Then we apply slicing which removes the code that has no influence on reachability of these locations. Finally, we symbolically execute the sliced code using Klee  [1] to refute or confirm that an error location is reachable.

For many years, our attention has been focused mainly on slicing [2, 6, 8]. Only in 2016, we implemented a configurable instrumentation that enabled Symbiotic to check memory safety or, in general, any safety property. Consequently, Symbiotic  4 [4] participated for the first time in the category MemSafety where it won the bronze medal.

The instrumentation used in Symbiotic  4 to check memory safety inserts calls to functions that track every block of allocated memory and calls to functions that check validity of dereferences using the tracked information. A check is not inserted if a static pointer analysis guarantees that the dereferenced pointer points to a memory block that was allocated before. Later we have recognized a flaw of this optimization: a standard pointer analysis ignores memory deallocations and, hence, it can tell that a pointer can point to memory blocks allocated by specific program lines, but it does not tell whether these memory blocks are still allocated. As a result, Symbiotic  4 sometimes does not insert a check even if the dereference may be invalid and thus it may miss some bugs.

In Symbiotic  5, we have fixed and significantly boosted the instrumentation part. First, we have extended the above mentioned pointer analysis such that it takes into account deallocations as well. Second, the instrumentation now works in two stages. The first stage inserts the checks where extended pointer analysis cannot guarantee the dereference safety. Moreover, compared to Symbiotic  4, we use simpler checks if possible. For example, if a pointer analysis says that a given pointer points into a known fixed-size memory block, we just insert a check that the pointer’s offset is within the size of the block (without searching the tracked information about the block). The second stage inserts calls to memory tracking functions only to allocations of the memory blocks that can be accessed by some dereference instrumented in the first stage. Hence, we track only the information that may be possibly used in the checks.

To evaluate the boosted instrumentation, we run the following three configurations of Symbiotic on 393 benchmarks of the SV-COMP 2017 meta category MemSafety and of the category MemSafety-TerminCrafted:

Figure 1 clearly shows that the performance improvement brought by the extended pointer analysis itself is negligible compared to the performance improvement delivered by the extended pointer analysis in combination with staged instrumentation. For a precise description of the boosted instrumentation, experimental setup and results, we refer to [3].

Symbiotic  5 also changed the approach to error witness generation. Symbiotic  4 describes an errorneous run by a sequence of passed program locations. The sequence is often very long and it turned out to be too restrictive for witness checkers. Symbiotic  5 provides only the starting and target locations of the run and return values of some __VERIFIER_nondet* calls. More precisely, we provide return values of calls in main and such that they are called just once in the run. The witnesses are now more often confirmed by witness checkers.

All components of Symbiotic are built on top of llvm  3.9 [9]. We use the clang compiler to compile the analyzed sources into llvm bitcode. Symbiotic consists of scripts written in Python that distribute work to three basic modules, all written in C++:

   

Before and after slicing, we optimize the code using available llvm’s optimizations. The rest of bitcode transformations that we use and whose nature is mostly technical (e.g. replacement of calls inserted by clang’s sanitizer to __VERIFIER_error calls) are implemented as llvm passes. All the components that transform bitcode take a bitcode as an input and give a valid bitcode as an output. This makes Symbiotic highly modular: any part (module) can be easily replaced or used as a stand-alone tool.

The main strength of the approach is its universality and modularity. The instrumentation can reduce any safety property to reachability checks and therefore no special monitors need to be incorporated into the verification backend. Indeed, any tool that can decide reachability of error locations can be plugged-in.

Symbiotic  5 has been developed by M. Chalupa and M. Vitovská under supervision of J. Strejček. The tool and its components are available under Apache-2.0 and MIT Licenses. The project is hosted by the Faculty of Informatics, Masaryk University. llvm and Klee are also available under open-source licenses. The project web page is: https://​github.​com/​staticafi/​symbiotic.