Static analyzer debugging and quality assurance approaches

Написание статических анализаторов затруднено из-за наличия множества эквивалентных преобразований между исходным кодом программы, промежуточным представлением и большими формулами в формате Satisfiability Modulo Theories (SMT). Традиционные методы, такие как использование отладчика, инструментарий и ведение журналов, заставляют разработчиков сосредотачиваться на определенных мелких проблемах. В то же время каждая архитектура анализатора навязывает уникальное представление о том, как следует представлять промежуточные результаты, необходимые для отладки. Таким образом, отладка остается проблемой для каждого исследователя статического анализа. В этой статье представлен наш опыт отладки незавершенного промышленного статического анализатора. Представлено несколько наиболее эффективных методов конструктивной (генерация кода), тестовой (генерация случайных тестовых случаев) групп, а также группы журнализации (объединение и визуальное представление журналов). Генерация кода помогает избежать проблем с копируемым кодом, мы улучшаем его с помощью проверки использования кода. Генерация случайных тестовых наборов на основе целей снижает риски разработки инструмента, сильно смещенного в сторону конкретных вариантов использования конструкции синтаксиса, путем создания проверяемых тестовых программ с утверждениями. Слияние журналов объединяет журналы модулей и устанавливает перекрестные ссылки между ними. Модуль визуального представления показывает объединенный журнал, представляет основные структуры данных и предоставляет отчеты о работоспособности и производительности в форме отпечатков журнала. Эти методы реализованы на основе Equid, платформы статического анализа для промышленных приложений, и используются для внутренних целей. Они представлены в статье, изучены и оценены. Основные вклады включают изучение причин сбоев в авторском проекте, набор методов, их реализации, результаты тестирования и два тематических исследования, демонстрирующие полезность методов.