Статический анализ это метод, обычно используемый в рабочем процессе разработчика для проверки правильности исходного кода без необходимости его выполнения. Популярные анализаторы в экосистеме .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 raceswith write in method 'RaceCondition.WriteToField(...)'. Reporting because another access to the same memory occurs on a background thread, although this access may not.
