An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer

Many practical static analyzers are not completely sound by design. Their designers trade soundness in order to increase automation, improve performance, and reduce the number of false positives or the annotation overhead. However, the impact of such design decisions on the effectiveness of an analyzer is not well understood. In this paper, we report on the first systematic effort to document and evaluate the sources of unsoundness in a static analyzer. We present a code Instrumentation that reflects the sources of deliberate unsoundness in the .NET static analyzer Clousot. We have instrumented code from several open source projects to evaluate how often concrete executions violate Clousot’s unsound assumptions. In our experiments, this was the case in 8–29% of all analyzed methods. Our approach and findings can guide users of static analyzers in using them fruitfully, and designers in finding good trade-offs.