SharpChecker: Static analysis tool for C# programs

This paper considers various aspects of static analysis of C# programs in order to detect the maximum number of software bugs in an acceptable time. A complete cycle of software static analysis is described with the main focus being placed on the specifics of the C# language. Some methods are discussed that take into account popular features of C# at all levels of analysis: call graph and control flow graph construction, dataflow analysis, as well as context- and path-sensitive interprocedural analysis. A symbolic execution method is proposed, which is based on the works devoted to the Bounded Model Checking (BMC) and the Saturn Software Analysis Project. A memory model is described that enables an accurate intraprocedural analysis and allows one to create compact representations of error conditions associated with functions, which are essential for interprocedural analysis. A special attention is paid to the optimizations that occur during path-sensitive analysis of error conditions. The conditions need to be optimized in terms of size, because path-sensitive interprocedural analysis requires saving a large number of conditions for each analyzed function. The conditions are resolved using advanced SMT solvers (such as the Microsoft Z3 Prover). This paper also considers various approaches to modeling the behavior of library functions: based on a summary containing a set of properties required for analysis, or based on simplified implementations in C#. All the discussed solutions are implemented in the SharpChecker static analysis tool and are tested on a number of open-source projects from 1.5 thousand to 1.35 million lines of code.