The strength of automated code reviews, backed by static analyzers, is in finding cumbersome bugs that could be missed by human reviewers due to developer fatigue. However, static analyzers are limited in a key dimension. They either provide no explanation to the origin of static analysis alarms or their explanations are too verbose for developers to use effectively. While industrial-strength tools such as Infer provide trace information for each issue; our experience has been that these traces are often too imprecise and verbose for developers to effectively triage and action. Furthermore, even in the case of a true bug, if the developer is not provided with an understandable explanation, they are may very likely to dismiss it as noise, thus zeroing any precision effort on the part of the static analyzer.

In this talk, I present Rinser, a tool developed at Prime Video that aims to improve the evidence developers receive from static analyzers. Specifically, Rinser provides an on-demand method to check the realizability of potential bugs reported by the static analyzer Infer. We have developed an initial version of Rinser as a post-analysis automated-reasoning pass based on refutation reasoning. On industrial code bases, our tool is able to surface possible bugs to developers with evidence traces on average 4x steps shorter than standard Infer traces. Foremost, our tool has eased the adoption of static analyzers at Amazon and driven additional dialogue between engineers on the quality of the code. As a bonus, it has also provided a means to soundly remove many trivial false-positive warnings, thereby also reducing the subsequent triaging effort.

This is joint work with Toan Ngyuen and Evan Chang.

http://psubotic.github.io/