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

Xin Shi

November 18th, 202112 0

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.

Xin Shi Principal Software Engineer, Data & AI

Read next

Get to Know EF Core 6
Learn how to download and work with EF Core 6 and new features from improved support for Azure Cosmos DB to increased performance and first-class APIs to SQL Server temporal tables.
Jeremy Likness
November 29, 2021
3 comments

12 comments

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

  • dexi lin 0

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

    Should be Console.WriteLine or console.Log?

    • Xin ShiMicrosoft employee 1

      Good catch! Updated.

    • Xin ShiMicrosoft employee 0

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

  • Ed Johnson 0

    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

  • Ed Johnson 0

    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:
    Raised at Core__Core_unix.improve in file “src/core_unix.ml” (inlined), line 46, characters 4-43
    Called from Core__Core_unix.bind in file “src/core_unix.ml” (inlined), line 2457, characters 2-79
    Called from IBase__DBWriter.Server.server.(fun) in file “src/base/DBWriter.ml”, line 370, characters 33-67
    Called from IBase__Exception.try_finally in file “src/base/Exception.ml” (inlined), line 27, characters 8-12
    Called from IBase__Utils.do_in_dir in file “src/base/Utils.ml”, line 432, characters 2-62
    Re-raised at IStdlib__IExn.reraise_after in file “src/istd/IExn.ml” (inlined), line 13, characters 2-50
    Called from IBase__Exception.try_finally in file “src/base/Exception.ml” (inlined), line 38, characters 6-279
    Called from IBase__Utils.do_in_dir in file “src/base/Utils.ml”, line 432, characters 2-62
    Called from IBase__DBWriter.Server.in_results_dir in file “src/base/DBWriter.ml” (inlined), line 338, characters 26-77
    Called from IBase__DBWriter.Server.server in file “src/base/DBWriter.ml” (inlined), line 370, characters 4-68
    Called from IBase__ForkUtils.protect in file “src/base/ForkUtils.ml” (inlined), line 18, characters 2-5
    Called from IBase__DBWriter.Server.start in file “src/base/DBWriter.ml” (inlined), line 414, characters 8-38
    Called from IBase__DBWriter.start in file “src/base/DBWriter.ml” (inlined), line 428, characters 15-30
    Called from Dune__exe__Infer.setup.(fun) in file “src/infer.ml” (inlined), line 32, characters 8-25
    Called from Dune__exe__Infer.setup in file “src/infer.ml”, line 76, characters 4-15

    Run the command again with --keep-going to try and ignore this error.
    ^CWaiting for Sqlite write daemon to start (0.200000 seconds)
    Waiting for Sqlite write daemon to start (0.400000 seconds)
    Waiting for Sqlite write daemon to start (0.800000 seconds)
    Waiting for Sqlite write daemon to start (1.600000 seconds)
    Waiting for Sqlite write daemon to start (3.200000 seconds)
    Waiting for Sqlite write daemon to start (6.400000 seconds)
    Waiting for Sqlite write daemon to start (12.800000 seconds)
    Uncaught Internal Error: (IBase.Epilogues.Sigint)
    Error backtrace:
    Raised at IBase__Epilogues.(fun) in file “src/base/Epilogues.ml”, line 45, characters 62-74
    Called from Core__Core_unix.unary.(fun) in file “src/core_unix.ml”, line 600, characters 28-43
    Called from Core__Core_unix.unary.(fun) in file “src/core_unix.ml”, line 600, characters 28-43
    Called from IBase__Utils.do_in_dir in file “src/base/Utils.ml”, line 431, characters 2-16
    Called from IBase__DBWriter.Server.in_results_dir in file “src/base/DBWriter.ml” (inlined), line 338, characters 26-77
    Called from IBase__DBWriter.Server.socket_exists in file “src/base/DBWriter.ml” (inlined), line 364, characters 25-86
    Called from IBase__DBWriter.Server.wait_for_server_start in file “src/base/DBWriter.ml”, line 405, characters 11-29
    Called from IBase__DBWriter.Server.wait_for_server_start in file “src/base/DBWriter.ml” (inlined), line 408, characters 6-38
    Called from IBase__DBWriter.Server.wait_for_server_start in file “src/base/DBWriter.ml” (inlined), line 408, characters 6-38
    Called from IBase__DBWriter.Server.start in file “src/base/DBWriter.ml” (inlined), line 417, characters 8-69
    Called from IBase__DBWriter.start in file “src/base/DBWriter.ml” (inlined), line 428, characters 15-30
    Called from Dune__exe__Infer.setup.(fun) in file “src/infer.ml” (inlined), line 32, characters 8-25
    Called from Dune__exe__Infer.setup in file “src/infer.ml”, line 76, characters 4-15

    Run the command again with --keep-going to try and ignore this error.

    • Xin ShiMicrosoft employee 0

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

  • Christian Schwarz 0

    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

    • Xin ShiMicrosoft employee 0

      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 0

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

  • Tom Pester 0

    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 0

      Thank you very much!!

Feedback usabilla icon