Mikhail Gadelha

I will present a new option added to the clang static analyzer (CSA) to refute false bug reports, using satisfiability modulo theory (SMT) solvers. In this talk, I will:

(1) give a general overview of the CSA, how it works and its limitations;

(2) show how we extended the existing heuristics to remove spurious bug reports: path constraints produced by CSA are encoded as SMT problems, SMT solvers precisely check them for satisfiability, and bug reports (whose associated path constraints are unsatisfiable) are removed;

(3) show the evaluation of our refutation algorithm when analyzing twelve widely used open-source projects;

(4) show how to set up an automated testing environment using scripts provided by the CSA infrastructure. As an example, I will show how to set up the twelve projects used to evaluate our refutation algorithm: https://github.com/mikhailramalho/analyzer-projects.

The target audience of this talk is anyone interested in learning more about the clang static analyzer and in analyzing their C/C++/ObjectiveC projects.

The clang static analyzer works by symbolically executing a program, collecting the symbols and constraints for every path in the program, and reasoning about bug feasibility using a built-in solver called RangedConstraintManager. It was designed to be fast so that it can provide results for common mistakes (e.g., division by zero or use of uninitialized variables) even in complex programs. However, the speed comes at the expense of precision; it cannot handle some arithmetic operations (e.g, remainders) or bitwise expressions. In these cases, the analyzer discards the constraints and might report false bugs.

The new option works by adding an extra step in the program analysis after the bug is found by the built-in solver but before reporting it to the user; the path and the constraints that trigger the bug are encoded in SMT and checked for satisfiability.

I will present an evaluation of the crosscheck when analyzing twelve C/C++ open-source projects of various size (tmux, redis, openssl, twin, git, postgresql, sqlite3, curl, libWebM, memcached, xerces-c, and XNU). When analyzing these projects with bug validation enabled, the slowdown is negligible in cases where no bug is refuted (average 1.2% slowdown) and, when it finds false bugs, the bug validation gives a small speedup (average 6.2% speedup). On average, 12.2 bugs per program were refuted by the SMT solver, ranging from 1 bug refuted in redis to 51 being refuted in XNU.

Finally, I will present a set of scripts provided by the CSA that can be used to set up an automated testing environment. The scripts are freely available and their presentation will follow the process described in https://github.com/mikhailramalho/analyzer-projects.

ESBMC is a SMT-based context-bounded bounded model checker that aims to provide bit-precise verification of both ANSI-C and C++ programs. The presentation will briefly introduce the tool and then show the usage of libtooling as a frontend for the tool, including the problems we had during the development and what we hope for the future.

On the first half of the talk, I'll describe the tool and present some examples of its usage, including the verification of concurrent programs.

I'll then focus on the tool's new frontend, which generates the AST of the program using clang's libtooling and converts it to an internal format that's used for the verification. This second half of the presentation will be focused on the development of the C frontend and the yet to be C++ frontend, including how we had to adjust to the libtooling API.

The aim of the talk is to present the difficulties that we faced when moving away from our frontend to clang, including limitations we found during the development. I'll end the talk with what we hope for the future, as users of clang, which translates to easier access to some of clang's internals (specially the static analyser).