Аннотация:
В данной работе рассматривается построение масштабируемого чувствительного к путям анализа дефектов в программах на языке C#. Предложенный метод анализа является адаптацией набора подходов, используемых в инструментах для статического анализа C/C++-программ Saturn, Calysto и Svace. Особое внимание уделяется связи рассматриваемой модели с реальным выполнением программы. Производится формализация дефекта разыменования нулевого указателя и сведение задачи поиска данного дефекта к задаче выполнимости формул логики предикатов. Для проведения формализации вводится модельный язык, на который может быть оттранслирована любая программа на языке С#. Язык представляет собой подмножество языка C#, избавленное от синтаксического сахара. Для упрощения формализации из числовых типов рассматривается только один целочисленный тип. Для решения проблемы анализа циклов используется метод развертки графа потока управления. Предлагается модель абстрактного состояния программы, описывающая множество возможных состояний в данной точке программы. Абстрактное состояние задается состоянием памяти программы, описанным с помощью набора неизвестных входных переменных, и предикатом пути над тем же набором переменных. Для каждой инструкции модельного языка определяются формальная семантика и передаточная функция, отражающая изменение абстрактного состояния в соответствии с семантикой. Каждая функция считается точкой входа в программу, а межпроцедурный анализ основан на методе резюме. Резюме строятся по результатам внутрипроцедурного анализа функций. Поиск дефектов происходит при помощи добавления дополнительной информации к абстрактному состоянию. Решение о выдаче предупреждения принимается на основе выполнимости формулы, описывающей условие возникновения ошибки. Предложенный метод реализован в анализаторе SharpChecker, разработанном в ИСП РАН. Приведены результаты тестирования, подтверждающие применимость метода для анализа промышленных программ.
Полный текст:
PDF файл (872 kB)