November 18th, 2021

Infer# v1.2: Interprocedural Memory Safety Analysis For C#

Xin Shi
Xin Shi
Principal Software Engineer

Last December, we announced the public preview release of Infer#, which brings the interprocedural static analysis of Infer to the .NET community. The project was open sourced on GitHub under an MIT license.

New Feature Highlights

Infer# 1.2 brings race condition detection, improves performance, provides more ways to use, and expands analysis coverage. The full list of improvements can be found on the release page.

Support for Infer# On Windows via WSL2 (Windows Subsystem for Linux)

As the first step in our initiative to provide Windows support for Infer#, you can now run the analysis in WSL2.

Azure Pipelines Integration

We now support Infer# as an Azure Pipelines plugin.

Race Condition

Infer# now supports race condition detection via Infer’s RacerD analyzer.

public class RaceCondition
{
    private readonly object _object = new object();

    public void TestMethod()
    {
        int FirstLocal;
        FirstLocal = TestClass.StaticIntegerField;
    }

    public void FieldWrite()
    {
        lock (_object)
        {
            {
                TestClass.StaticIntegerField = 1;
            }
        }
    }
}
Assets/RaceCondition.cs:12: warning: Thread Safety Violation
  Read/Write race. Non-private method `RaceCondition.TestMethod()` reads without synchronization from `Assets.TestClass.Cilsil.Test.Assets.TestClass.StaticIntegerField`. Potentially races with write in method `RaceCondition.FieldWrite()`.
 Reporting because another access to the same memory occurs on a background thread, although this access may not.

Exception Code Coverage

Infer# now reports warnings on methods with exception-handling constructs (for example, try-catch-finally, and lock).

public void ResourceLeakExcepHandlingBad() {
    StreamWriter stream = AllocateStreamWriter();
    try
    {
        stream.WriteLine(12);
    }
    catch
    {
        Console.WriteLine("Fail to write");
    }
    finally
    {
        // FIXME: should close the stream by calling stream.Close().
    }
}
/.../Examples/Program.cs:39: error: Dotnet Resource Leak
  Leaked { %0 -> 1 } resource(s) at type(s) System.IO.StreamWriter.

Using Infer#

You can find the instructions for all supported scenarios on our GitHub landing page.

Please submit your feedback and feature requests to our GitHub repository. We’re looking at all feature requests from the community and will prioritize next steps based on popularity.

Category
.NET.NET CoreStatic Analysis

Author

Xin Shi
Xin Shi
Principal Software Engineer

Xin Shi is a Software Engineer on the Data & AI team, working on Infer# - an interprocedural and scalable static code analyzer for C#.

12 comments

Discussion is closed. Login to edit/delete existing comments.

Newest
Newest Popular Oldest
  • Tom Pester

    Thank you Xin and colleagues. We are looking forward to see this project thrive and are already using it in our pipelines.

    • Xin ShiMicrosoft employee Author

      Thank you very much!!

  • Christian Schwarz · Edited

    Running on a large .NET Core API project Infer# doesn't yield any results:

    ~/infersharp$ ./run_infersharp.sh /mnt/c/path/to/api/API.dll --enable-null-dereference --enable-dotnet-resource-leak --enable-thread-safety-violation --sarif --debug
    Processing {/mnt/c/path/to/API.dll}
    Copying binaries to a staging folder...\n
    Code translation started...

    Coverage Statistics:

    Method successfully translated: 0 (-2147483648%)
    Method partially translated: 0 (-2147483648%)
    Instructions translated: 0 (-2147483648%)

    Instructions skipped: 0 (-2147483648%)

    Code translation completed. Analyzing...

    No issues found

    Read more
    • Xin ShiMicrosoft employee Author

      Infer# requires the symbol file (.pdb) in addition to its .dll. Assuming both are present, ./run_infersharp.sh /mnt/c/path/to/api/ should do. The argument for the run script is a directory containing the binaries you want to analyze against, instead of a single file.

      • Christian Schwarz

        Thanks Xin, pointing to the directory instead of the DLL solved my issue.

  • Ed Johnson

    when run on a fairly large legacy web app fails with apparent sqllite error, is there a missing dependency (sqllite3 is installed)?

    ./run_infersharp.sh ../Legacy\ TP\ Group/tpc/Source/Code/TPC.Web/bin --sarif
    Processing {../Legacy TP Group/tpc/Source/Code/TPC.Web/bin}
    Copying binaries to a staging folder...\n
    Code translation started...

    Coverage Statistics:

    Method successfully translated: 19321 (87%)
    Method partially translated: 2909 (13%)
    Instructions translated: 285705 (70%)

    Instructions skipped: 125352 (30%)

    Code translation completed. Analyzing...

    Uncaught Internal Error: (Unix.Unix_error "Operation not supported" bind
    "((fd 7) (addr (ADDR_UNIX sqlite_write_socket)))")
    Error backtrace:Read more

    • Xin ShiMicrosoft employee Author

      It is likely that the Infer# executables were placed in the Windows File system. They need to be in the Linux File system instead.

  • Ed Johnson

    fails when installed/run from a path with a space. Extracted in ‘/mnt/d/Legacy TP Group/’ when run results in error :

    Code translation completed. Analyzing…

    ./run_infersharp.sh: line 62: /mnt/d/Legacy: No such file or directory
    mkdir: cannot create directory ‘infer-out/captured’: No such file or directory
    ./run_infersharp.sh: line 64: /mnt/d/Legacy: No such file or directory

    • Xin ShiMicrosoft employee Author

      This is high on our priority list. We are looking at a native VS and VS Code experience. Stay tuned!

  • dexi lin

    console.log("Fail to write"); ?

    Should be Console.WriteLine or console.Log?

    • Xin ShiMicrosoft employee Author

      Good catch! Updated.

Read next