Сборники трудов ИСП РАН


Инфраструктура статического анализа программ на языке C#

В. К. Кошелев (ИСП РАН, Москва, Россия)
В. Н. Игнатьев (ИСП РАН, Москва, Россия)
А. И. Борзилов (ИСП РАН, Москва, Россия)

Аннотация

В работе рассмотрены различные аспекты статического анализа программ на языке C# с целью обнаружения максимального количества ошибок за минимально приемлемое время. Описан полный цикл статического анализа программного обеспечения, при этом основное внимание уделяется особенностям, возникающим при анализе языка C#. Рассмотрены методы, позволяющие учитывать популярные возможности языка на всех уровнях анализа: построение графа вызовов и графа потока управления, проведение анализа потоков данных и чувствительного к контексту и путям межпроцедурного анализа. Предлагается метод символьного исполнения, основанный на таких работах, как Bounded Model Checking и Saturn Software Analysis Project. В статье описана организация модели памяти, позволяющая как проводить точный внутрипроцедурный анализ, так и создавать компактные представления для привязанных к функциям условий, используемые при межпроцедурном анализе. Особое внимание уделяется теме оптимизации возникающих на этапе чувствительного к путям анализа условий. Условия необходимо оптимизировать как по размеру, поскольку при межпроцедурном чувствительном к путям анализе необходимо сохранять большое количество условий для каждой проанализированной функции, так и по сложности, поскольку время анализа ограничено. Решение условий производится при помощи современных SMT-решателей, таких как Microsoft Z3 Prover. В статье также рассмотрены различные подходы к моделированию поведения библиотечных функций: при помощи резюме в виде набора признаком или в виде упрощенных реализаций на языке C#. Все приведённые решения реализованы в инструменте статического анализа SharpChecker и протестированы на наборе проектов различного объема (от 1.5 тыс. до 1.35 млн. строк кода) с открытым исходным кодом.

Ключевые слова

Статический анализ; использование нулевого указателя; чувствительность к путям; чувствительность к контексту; резюме функции; поиск дефектов; Roslyn; C#

Издание

Труды Института системного программирования РАН, том 28, вып. 1, 2016, стр. 21-40.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2016-28(1)-2

Полный текст статьи в формате pdf Вернуться к содержанию тома