{"id":31186,"date":"2020-12-08T10:00:26","date_gmt":"2020-12-08T17:00:26","guid":{"rendered":"https:\/\/devblogs.microsoft.com\/dotnet\/?p=31186"},"modified":"2020-12-07T17:29:46","modified_gmt":"2020-12-08T00:29:46","slug":"infer-interprocedural-memory-safety-analysis-for-c","status":"publish","type":"post","link":"https:\/\/devblogs.microsoft.com\/dotnet\/infer-interprocedural-memory-safety-analysis-for-c\/","title":{"rendered":"Infer#: Interprocedural Memory Safety Analysis For C#"},"content":{"rendered":"

\u201cThe refinement of techniques for the prompt discovery of error serves as well as any other as a hallmark of what we mean by science.\u201d<\/em>\n: -J. Robert Oppenheimer<\/p>\n

We are excited to announce the public release of Infer#, which brings the interprocedural static analysis\ncapabilities of Infer<\/a> to the .NET community. Additionally, as part of our commitment to open-sourcing,\nthe project has been released on GitHub<\/a> under an MIT license.<\/p>\n

Static analysis is a technique commonly used in the developer workflow to validate the correctness of\nsource code without needing to execute it. Popular analyzers within the .NET ecosystem include FxCop\nand Roslyn analyzers. Infer# complements these tools by detecting interprocedural memory\nsafety bugs such as null dereferences and resource leaks.<\/p>\n

By integrating directly in the developer workflow to detect reliability and security bugs before they ship,\nInfer# supports agile development for .NET. Indeed, we already are observing promising early results on\nMicrosoft software such as Roslyn, .NET SDK, and ASP.NET Core.<\/p>\n

We plan to continue expanding Infer#, with support for thread safety coming next.<\/p>\n

Interprocedural Memory Safety Validation For .NET<\/h2>\n

Infer# currently detects null dereferences and resource leaks, with race condition detection in\ndevelopment. We illustrate each capability below with a buggy piece of code along with the\ncorresponding warning Infer# would report on it.<\/p>\n

To learn more about the technical implementation of Infer#, please see our wiki<\/a>.<\/p>\n

Null Dereference<\/h3>\n
    static void Main(string[]) args)\r\n    {\r\n        var returnNull = ReturnNull();\r\n        _ = returnNull.Value;\r\n    }\r\n\r\n    private static NullObj ReturnNull()\r\n    {\r\n        return null;\r\n    }\r\n\r\ninternal class NullObj\r\n{\r\n    internal string Value { get; set; }\r\n}\r\n<\/code><\/pre>\n
The returnNull<\/em> variable is interprocedurally assigned null and is dereferenced via a read on the Value\nfield. This dereference is detected:<\/p>\n
\/home\/runner\/work\/infersharpaction\/infersharpaction\/Examples\/NullDereference\/Program.cs:11: error: NULL_DEREFERENCE (biabduction\/Rearrange.ml:1622:55-62:)\r\n  pointer 'returnNull' could be null and is dereferenced at line 11, column 13.\r\n<\/code><\/pre>\n
Resource Leak<\/h3>\n
public StreamWriter AllocatedStreamWriter()\r\n{\r\n    FileStream fs = File.Create(\"everwhat.txt\");\r\n    return new StreamWriter(fs);\r\n}\r\n\r\npublic void ResourceLeakBad()\r\n{\r\n    StreamWriter stream = AllocateStreamWriter();\r\n    \/\/ FIXME: should close the StreamWriter by calling stream.Close() if stream is not null.\r\n}\r\n<\/code><\/pre>\n
The stream<\/em> StreamWriter variable is returned from AllocateStreamWriter but not\nclosed. Infer# reports the resulting resource leak, enabling the developer to fix the error:<\/p>\n
\/home\/runner\/work\/infersharpaction\/infersharpaction\/Examples\/ResourceLeak\/Program.cs:11: error: RESOURCE_LEAK\r\n  Leaked { %0 -> 1 } resource(s) at type(s) System.IO.StreamWriter.\r\n<\/code><\/pre>\n
Coming next: Thread Safety Violations<\/h2>\n
Given the positive feedback we have already received on Infer#\u2019s ability to catch null dereferences and\nresource leaks, we\u2019re working on additional defect detection scenarios. Thread safety violation is the\nnext scenario on the horizon, which we preview below:<\/p>\n
public class RaceCondition\r\n{\r\n    private readonly object __lockobj = new object();\r\n    public int intField;\r\n    public void WriteToField(int input)\r\n    {\r\n        lock (__lockObj)\r\n        {\r\n            intField = input;\r\n        }\r\n    }\r\n\r\n    public int ReadFromField()\r\n    {\r\n        return intField;\r\n    }\r\n}\r\n<\/code><\/pre>\n
Although the feature is still in development, the warnings will appear analogously to how they do within\nJava; lock() statement blocks will trigger the RacerD<\/a> analysis just as synchronized() Java blocks do.<\/p>\n
\/...\/Examples\/RaceCondition\/Program.cs:39: error: THREAD_SAFTY_VIOLATION\r\n  Read\/Write race. Non-private method 'Int32 RaceCondition.ReadFromField()' reads without synchronization from 'this.intField'. Potentially races\r\nwith write in method 'RaceCondition.WriteToField(...)'.\r\n  Reporting because another access to the same memory occurs on a background thread, although this access may not.\r\n<\/code><\/pre>\n
Trying Infer#<\/h2>\n