Мы рады объявить о публичном выпуске Infer#, который предоставляет сообществу .NET возможности межпроцедурного статического анализа Infer. Кроме того, в рамках нашей приверженности открытому исходному коду проект был выпущен на GitHub под лицензией MIT.
Статический анализ — это метод, обычно используемый в рабочем процессе разработчика для проверки правильности исходного кода без необходимости его выполнения. Популярные анализаторы в экосистеме .NET — это FxCop и Roslyn. Infer# дополняет эти инструменты, обнаруживая межпроцедурные ошибки безопасности памяти, такие как разыменование null и утечки ресурсов.
Интегрируясь непосредственно в рабочий процесс разработчика для обнаружения ошибок надежности и безопасности перед их отправкой, Infer# поддерживает гибкую разработку для .NET. В самом деле, мы уже наблюдаем многообещающие первые результаты в отношении программного обеспечения Microsoft, такого как Roslyn, .NET SDK и ASP.NET Core.
Мы планируем и дальше расширять Infer#, и в будущем мы будем поддерживать безопасность потоков.
Подробнее под катом.
![](https://habrastorage.org/r/w780q1/webt/21/_h/u6/21_hu6mi0r6toeblz3tnufvlipo.jpeg)
Infer# в настоящее время обнаруживает нулевые разыменования (null dereferences) и утечки ресурсов. Мы проиллюстрируем каждую возможность ниже с ошибочным фрагментом кода вместе с соответствующим предупреждением, которое Infer# выводит об этом.
Чтобы узнать больше о технической реализации Infer#, посетите нашу вики.
Переменной returnNull межпроцедурно присваивается значение null, а ссылка на нее разыменовывается посредством чтения поля Value. Это разыменование обнаружено:
Переменная Stream StreamWriter возвращается из AllocateStreamWriter, но не закрывается. Infer# сообщает об утечке ресурсов, что позволяет разработчику исправить ошибку:
Учитывая положительные отзывы, которые мы уже получили о способности Infer# обнаруживать нулевые разыменования и утечки ресурсов, мы работаем над дополнительными сценариями обнаружения дефектов. Нарушение безопасности потоков — это следующий сценарий на горизонте:
Хотя функция все еще находится в разработке, предупреждения будут появляться аналогично тому, как они появляются в Java; Блоки операторов lock() запускают анализ RacerD так же, как блоки Java synchronized().
Статический анализ — это метод, обычно используемый в рабочем процессе разработчика для проверки правильности исходного кода без необходимости его выполнения. Популярные анализаторы в экосистеме .NET — это FxCop и Roslyn. Infer# дополняет эти инструменты, обнаруживая межпроцедурные ошибки безопасности памяти, такие как разыменование null и утечки ресурсов.
Интегрируясь непосредственно в рабочий процесс разработчика для обнаружения ошибок надежности и безопасности перед их отправкой, Infer# поддерживает гибкую разработку для .NET. В самом деле, мы уже наблюдаем многообещающие первые результаты в отношении программного обеспечения Microsoft, такого как Roslyn, .NET SDK и ASP.NET Core.
Мы планируем и дальше расширять Infer#, и в будущем мы будем поддерживать безопасность потоков.
Подробнее под катом.
![](https://habrastorage.org/webt/21/_h/u6/21_hu6mi0r6toeblz3tnufvlipo.jpeg)
Межпроцедурный анализ валидации памяти для 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.