Формализация определения ошибок при статическом символьном выполнении

Аннотация

Данная работа посвящена формализации понятия ошибочной ситуации при статическом анализе исходного кода, основанном на символьном выполнении. При использовании методов символьного выполнения для статического анализа необходимо пересматривать критерий выдачи ошибок, так как оригинальный критерий приводит к чрезмерному числу ложных срабатываний. Для решения этой проблемы предлагаются альтернативные определения ошибочной ситуации, сообщающие об ошибке только в том случае, когда она происходит на некотором множестве значений входных переменных. Примерами таких множеств являются, например, множество значений входных переменных, при которых управление пройдет через заданную точку программы, или множество значений, при которых управление пройдет по заданному пути в графе потока управления. В данной работе рассматриваются различные способы задания таких множеств начальных значений. Анализируются полученные таким образом определения ошибочных ситуаций. Приводятся алгоритмы, обнаруживающие данные ошибочные ситуации, а также доказывается их соответствие. Рассматривается практическое применение приведённых определений ошибочных ситуаций, а именно: классификация срабатываний инструментов статического анализа; учет неизвестных контракта вызова анализируемой функции; использование определения ошибочной ситуации в качестве запроса к SMT-решателю для поиска точного решения в соответствии с данными определением.