Path-sensitive bug detection analysis of C# program illustrated by null pointer dereference

This paper proposes an approach for detecting bugs in C# programs and uses null pointer deference as the main example. The approach employs a scalable path-sensitive analysis, which involves symbolic execution with state merging and function summary methods. C/C++ program analyzers like Saturn Software Analysis Project, Calysto or Svace use similar approaches. We analyze functions in backward topological order with account for previously calculated summaries. For summary construction, we use the same analysis engine as for bug detection. The paper contains a formal description of the proposed approach applied to reduced “sugar-free” subset of C# language. For each instruction of the considered language, we define a formal semantics and transfer function according to the symbolic state. During the path-sensitive analysis, we store additional information related to possible bugs in the symbolic state, and the decision whether the warning should be reported is made upon the satisfiability of the corresponding formula. Therefore, we reduce the problem of bug detection to satisfiability of a first-order logical formula defined on atoms, which are arithmetic expressions on function input values. It can be efficiently solved with modern SMT solvers. We have implemented the approach in our Roslyn-based analyzer, called SharpChecker. Evaluation of SharpChecker on open-source commodity applications has shown acceptable scalability and reasonable amount of warnings.