Интеграция решателя задачи КС-достижимости в инструмент статического анализа SVF

Задача достижимости является одной из основных для многих видов статического анализа кода. Например, для различных межпроцедурных анализов потока данных, анализа указателей и т.д. Не так давно Илья Муравьёв в своей работе Оптимизация алгоритма контекстно-свободной достижимости, основанного на операциях линейной алгебры предложил высокопроизводительный алгоритм решения этой задачи. В настоящее время ведётся работа по его реализации в рамках библиотеки LAGraph Предлагается интегрировать данную реализацию в инструмент статического анализа SVF, использующий LLVM. Кроме этого, нужно будет провести сравнение с уже имеющимися аналогами в рамках SVF.

Требования к студенту
  • Хорошие знания языка программирования С++ и соответствующего инструментария разработчика: сборка, отладка, профилирование, проверка стиля кодирования и качества кода.
  • Хорошие знания языка программирования С и соответствующего инструментария разработчика: сборка, отладка, профилирование, проверка стиля кодирования и качества кода.
  • Знания основ статического анализа кода: внутрипроцедурный анализ, межпроцедурный анализ, классические задачи и алгоритмы их решения (анализ указателей, другие анализы потока данных).
  • Знания основ теории графов: ориентированные помеченные графы, представление в виде матрицы смежности, алгоритмы проверки достижимости и поиска путей, алгоритмы обхода графа.
  • Знания основы теории формальных языков: контекстно-свободные грамматики, понятие выводимости в грамматике, нормальные формы грамматик (нормальная форма Хомского, BNF, EBNF).
  • Знакомство с инфраструктурой LLVM.
Уровень

3 курс, Бакалаврская ВКР

Руководитель

Григорьев Семен Вячеславович

Консультант

Grigorev Semyon

Источник

Кафедра системного программирования СПбГУ