Infer#: межпроцедурный анализ безопасности доступа к памяти для C#

Мы рады объявить о публичном выпуске Infer#, который предоставляет сообществу .NET возможности межпроцедурного статического анализа Infer. Кроме того, в рамках нашей приверженности открытому исходному коду проект был выпущен на GitHub под лицензией MIT.

Статический анализ — это метод, обычно используемый в рабочем процессе разработчика для проверки правильности исходного кода без необходимости его выполнения. Популярные анализаторы в экосистеме .NET — это FxCop и Roslyn. Infer# дополняет эти инструменты, обнаруживая межпроцедурные ошибки безопасности памяти, такие как разыменование null и утечки ресурсов.

Интегрируясь непосредственно в рабочий процесс разработчика для обнаружения ошибок надежности и безопасности перед их отправкой, Infer# поддерживает гибкую разработку для .NET. В самом деле, мы уже наблюдаем многообещающие первые результаты в отношении программного обеспечения Microsoft, такого как Roslyn, .NET SDK и ASP.NET Core.

Мы планируем и дальше расширять Infer#, и в будущем мы будем поддерживать безопасность потоков.

Подробнее под катом.

Межпроцедурный анализ валидации памяти для C#

Infer# в настоящее время обнаруживает нулевые разыменования (null dereferences) и утечки ресурсов. Мы проиллюстрируем каждую возможность ниже с ошибочным фрагментом кода вместе с соответствующим предупреждением, которое Infer# выводит об этом.

Чтобы узнать больше о технической реализации Infer#, посетите нашу вики.

Null Dereference

    static void Main(string[]) args)     {         var returnNull = ReturnNull();         _ = returnNull.Value;     }      private static NullObj ReturnNull()     {         return null;     }  internal class NullObj {     internal string Value { get; set; } }

Переменной returnNull межпроцедурно присваивается значение null, а ссылка на нее разыменовывается посредством чтения поля Value. Это разыменование обнаружено:

/home/runner/work/infersharpaction/infersharpaction/Examples/NullDereference/Program.cs:11: error: NULL_DEREFERENCE (biabduction/Rearrange.ml:1622:55-62:)   pointer 'returnNull' could be null and is dereferenced at line 11, column 13.

Утечка ресурсов

public StreamWriter AllocatedStreamWriter() {     FileStream fs = File.Create("everwhat.txt");     return new StreamWriter(fs); }  public void ResourceLeakBad() {     StreamWriter stream = AllocateStreamWriter();     // FIXME: следует закрыть StreamWriter, вызвав stream.Close(), если stream не равен нулю. }

Переменная Stream StreamWriter возвращается из AllocateStreamWriter, но не закрывается. Infer# сообщает об утечке ресурсов, что позволяет разработчику исправить ошибку:

/home/runner/work/infersharpaction/infersharpaction/Examples/ResourceLeak/Program.cs:11: error: RESOURCE_LEAK   Leaked { %0 -> 1 } resource(s) at type(s) System.IO.StreamWriter.

Далее: нарушения безопасности потоков

Учитывая положительные отзывы, которые мы уже получили о способности Infer# обнаруживать нулевые разыменования и утечки ресурсов, мы работаем над дополнительными сценариями обнаружения дефектов. Нарушение безопасности потоков — это следующий сценарий на горизонте:

public class RaceCondition {     private readonly object __lockobj = new object();     public int intField;     public void WriteToField(int input)     {         lock (__lockObj)         {             intField = input;         }     }      public int ReadFromField()     {         return intField;     } }

Хотя функция все еще находится в разработке, предупреждения будут появляться аналогично тому, как они появляются в Java; Блоки операторов lock() запускают анализ RacerD так же, как блоки Java synchronized().

/.../Examples/RaceCondition/Program.cs:39: error: THREAD_SAFTY_VIOLATION   Read/Write race. Non-private method 'Int32 RaceCondition.ReadFromField()' reads without synchronization from 'this.intField'. Potentially races with write in method 'RaceCondition.WriteToField(...)'.   Reporting because another access to the same memory occurs on a background thread, although this access may not.

Пробуйте Infer#!