With Infer#, Microsoft extends the choice of static analyzers available within the .NET ecosystem by bringing Facebook Infer's inter-procedural static analysis capabilities to it.
Infer is a static analysis tool open-sourced by Facebook in 2015. It supports Java and C/C++/Objective-C code and is able to detect a number of potential issues, including null pointer exceptions, resource leaks, annotation reachability, missing lock guards, and concurrency race conditions in Android and Java code; and null pointer dereferences, memory leaks, coding conventions, and unavailable API’s for languages belonging to the C-family.
Infer# is not the only static analyzer available for .NET, says Microsoft senior software engineer Xin Shi. However, Infer# brings unique capabilities to the .NET platform. What sets Infer# apart is its focus on cross-function analysis, which is not found in other analyzers, and incremental analysis.
PreFast detects some instances of null derereference exceptions and memory leaks, but its analysis is purely intra-procedural. Meanwhile, JetBrains Resharper heavily relies on developer annotations for its memory safety validation.
For example, Shi describes how Infer# is able to detect a null dereference in the following code snippet involving three different functions:
static void Main(string[]) args)
{
var returnNull = ReturnNull();
_ = returnNull.Value;
}
private static NullObj ReturnNull()
{
return null;
}
internal class NullObj
{
internal string Value { get; set; }
}
Differential workflow is how Facebook dubs Infer's capability to run on two versions of a project and provide a comparison in terms of what issues have been introduced or fixed. This makes it possible to integrate Infer in a CI workflow and have it automatically process a PR before it is accepted into the main branch.
For example, explains Shi, you can get a list of files changed between a feature and the master branch by executing:
git diff --name-only origin/feature..origin/master > files-to-analyze.txt
Then for each branch, you would check it out and run Infer on it:
git checkout <branch>
infer capture -- make -j 4
infer analyze --changed-files-index files-to-analyze.txt
cp infer-out/report.json <branch>-report.json
Finally, you would use Infer's reportdiff command to compare the findings:
infer reportdiff --report-current feature-report.json --report-previous master-report.json
This would output three files with the issues added in the feature branch, the issues fixed in feature, and the issues that remained intact.
The capability to analyze incremental changes is what enables Infer to run effectively on large codebases. In this regard, Microsoft has been using Infer# on a number of its products, including Roslyn, .NET SDK, and ASP.NET Core.
To support both inter-procedural and differential analysis, Infer uses Separation Logic, which makes it possible to reason about manipulations to computer memory and prove certain memory safety conditions. To this aim, Infer translates all code into an intermediate representation called SIL during its capture step. SIL leverages the Smallfoot predicate framework.
The core problem of enabling Infer to analyze .NET source code is that of translating it to the SIL, the language which Infer analyzes. To do this, source language constructs need to be represented in OCaml.
To simplify this process and make it easier to extend Infer# to other .NET languages beyond C#, Microsoft has introduced an intermediate language-agnostic JSON serialization of the SIL.
The advantages of working from a low-level representation of the source code are twofold: first, the CIL underlies all .NET languages (such as Visual Basic and F# in addition to the most common C#), and therefore InferSharp supports all .NET languages this way, and second, the CIL is stripped of any syntactic sugar, which reduces the language content needed to translate and thereby simplifies the translation.
Microsoft SIL serializer is coupled with a deserialization package that extracts the SIL data structures in OCaml and makes them available for Infer's backend analysis.
Currently, Infer# supports null dereference and memory leaks detection, but Microsoft has already announced it will continue extending its capabilities by adding support for race condition and thread safety violation detection.
