Константин Книжник: статический анализ, взгляд со стороны

Андрей Карпов
Статей: 375



Поддержка VivaMP была прекращена в 2014 году. По всем возникшим вопросам вы можете обратиться в нашу поддержку.

Аннотация

Статья представляет интервью, взятое у Константина Книжника, сотрудником компании "Системы программной верификации" Андреем Карповым. Затронуты вопросы статического анализа кода, актуальность решений в этой области, а также перспективы использования статического анализа при разработке параллельных приложений.

Введение

Компания ООО "Системы программной верификации" (ООО "СиПроВер") занимающаяся разработкой инструментов в области тестирования и верификации программ попросила ответить на некоторые вопросы Константина Книжника, специалиста в области методологии статического анализа кода. Интервью провел и оформил в виде этой статьи Андрей Карпов, являющийся сотрудником ООО "СиПроВер".

В интервью затронуты вопросы статического анализа кода, актуальность решений в этой области. Обсуждаются перспективы использования статического анализа при разработке параллельных приложений. Получена сторонняя оценка инструментов статического анализа Viva64 и VivaMP, разрабатываемых компанией "СиПроВер". А также обсуждены некоторые общие вопросы верификации программ, которые мы надеемся будет интересно узнать читателям изучающим эту область тестирования приложений.

Вопросы задает (вопросы выделены жирным текстом):

К.ф.-м.н., Андрей Карпов. Технический директор компании "СиПроВер", занимается развитием инструментов анализа кода Viva64 и VivaMP для тестирования 64-битных и параллельных приложений. Автор ряда статей по статическому анализу кода.

На вопросы отвечает:

К.ф.-м.н., Константин Книжник. Автор ряда статей, посвященных статическому анализу программного кода, разработчик верификаторов для Java приложений. Участвовал и продолжает участвовать во многих интересных проектах, например, в WebAlta.

Текст интервью

Вы действительно интересовались направлением статического анализа и даже участвовали в создании статического анализатора кода для Java приложений?

Я действительно интересовался темой статического анализа и верификации программ. Началось всё в 1997 году, когда я написал программку jlint - аналог clint для Java.

Расскажите, пожалуйста, о jlint поподробнее

Программа состояла из двух частей - простейшего синтаксического анализатора для языков с Си-подобным синтаксисом. В языке Си есть как известно много мест в синтаксисе, которые провоцируют программиста на трудно находимые ошибки. Например, написание "=" вместо "==", пустое тело цикла из за неправильно поставленной точки с запятой ";" и так далее. Перечислять не буду, проблематика, думаю, в общем, достаточно известная.

Вторая часть - это был jlint - более-менее полноценный семантический анализатор для Java. Связываться с написанием собственного Java-парсера мне тогда не хотелось, поэтому я пошёл по пути чтения уже скомпилированного байт кода и анализа его. Проверки включают обращение по нулевой ссылке, несовместимые касты, всегда истинные или всегда ложные выражения, потерю точности и тому подобное.

Самое интересное, что было в jlint - это возможность нахождения потенциальных дедлоков в программе. В Java очень простой механизм блокировок - synchronized метод или synchronized(expr) конструкция. На основании анализа этих конструкций, делалась попытка построить граф блокировок (вершины - это блокируемые ресурсы) и поиск циклов в этом графе. Естественно построить точный граф не возможно, поэтому делалась попытка построения приближённого графа, используя классы вместо конкретных экземпляров объектов. К сожалению, в реальных проектах, эта проверка работала не очень хорошо - было много ложных срабатываний.

Как связана история создания jlint и Ваша работа в TogetherSoft и Borland над аналогичными проектами? Чем Вы занимались в этих компаниях?

Через несколько лет мой jlint заметил создатель TogetherSoft - компании, которая выпускала UML modeling tool и двигалась в сторону разработки полноценного IDE для Java. И я пошёл работать в TogetherSoft. Правда, сначала я делал для них OODBMS, потом Version Control System и только потом участвовал в разработке верификатора для Java.

Тут уже всё было сделано по-серьёзному, с полноценным синтаксическим разбором, data flow analysis, и.т.д. Число аудитов превышало несколько сотен. Некоторые из них были, конечно, весьма простые, но некоторые претендовали на зачатки искусственного интеллекта. Например, определялись ошибки с перепутыванием индексной переменной во вложенных циклах или выявлялись стандартные последовательности для работы с каким-то из ресурсов (open, read/write, close) и поиск мест, где эта последовательность нарушается.

В общем, много было чего сделано, в том числе и весьма не тривиального. Забавно конечно, когда запускаешь верификатор на исходники, например, JDK и обнаруживаешь с десяток критических ошибок типа обращения по нулевому адресу. В основном, это, конечно, происходит в обработчиках ошибок, т.е. в тех местах, которые в нормальной жизни никогда не выполняются).

Примечательно, что в это время верификаторов Java на рынке не существовало. В общем, были предпосылки на большой успех, но как-то не сложилось.

Компания TogetherSoft была продана компании Borland. Нам пришлось включить поддержку таких языков как С++, Delphi и Visual Basic, интегрироваться с JBuilder-ом и Eclipse. В конце концов, наш верификатор попал пользователям, но в очень убогом виде (в основном из-за того, что приходилось работать над моделью AST предоставляемой нам другими подсистемами, которая работала безобразно медленно и не содержала многой необходимой верификатору информации). Поезд к этому времени уже ушёл, почти для всех популярных IDE для Java уже появились свои собственные верификаторы. И хотя столь глубокий анализ мало кто из них пытался проводить - в основном всё ограничивалось причёсыванием синтаксиса, но эти отличия не так просто было заметить.

А потом в компании Borland начался кризис и вот уже несколько лет, я работаю в совершенно другой области.

Чем Вы занимаетесь в настоящее время?

Сейчас я принимаю участие сразу в нескольких проектах. Например, в компании WebAlta я занимаюсь поисковыми машинами. Помимо WebAlta, я участвую в создании объектно-ориентированной СУБД для встраиваемых систем. Есть и другие проекты.

А какова дальнейшая судьба JLint?

Так как моя работа в TogetherSoft, а потом в Borland-е была непосредственно связана с верификацией программ, то пришлось свой jlint забросить. Кстати, существующий jlint можно скачать с моего сайта по адресу http://www.garret.ru/lang.html.

Как специалист в области статического анализа, какими наблюдениями и советами Вы бы могли поделиться с нами? Что компании СиПроВер следует учитывать, продолжая разработку статических анализаторов Viva64 и VivaMP?

Хорошо. Кратко попытаюсь перечислить некоторые основные выводы, к которым я пришёл за годы посвящённые проблеме верификации программ.

  • Большинство ошибок в реальных больших проектах находят самые "тупые" аудиты. Примером может служить отсутствия break-а в switch-е. Очень полезно, когда такие аудиты работают в среде разработки интерактивно (сразу же подчёркивая проблемные места).
  • Сообщения надо делить по степени достоверности (May-Be-Null, Is-Null, ...) с возможностью отключения и отдельных групп.
  • Для полного анализа необходим символический вычислитель - чтобы можно было понять, что i+1 > i. Я конечно в курсе про переполнение, из-за которого это не всегда так, но ведь задача верификатора состоит в поиске подозрительных мест.
  • Чем хуже язык спроектирован, тем больше в нём работы для верификатора - например синтаксис С провоцирует множество программистских ошибок и на эти грабли наступал по несколько раз любой C/C++ программист. В Java многие эти моменты были исправлены, но не все. Многие наши аудиты занимались тем, что по всяким эвристическим правилам пытались выявить enum-ы (которые до недавнего времени в Java отсутствовали) и провести для них что-то типа статического контроля типов. В С# естественно это всё оказалось совершенно не нужно.
  • Самое важное в верификаторе - это поддерживать разумный баланс подозрительности и болтливости. Если на не очень большой проект мне выдаётся несколько тысяч предупреждений, то, очевидно, что я просто буду не в состоянии их проверить. Тут конечно нужно разбиение по степени критичности. Но даже если взять какую-то достаточно критическую ошибку - например maу-by-null, которая может быть следствием кода типа:

  • if (x == null)
    {
    DoSomething();
    }
    x.InvokeSomeMethod();

  • то надо понимать, что проверив первые несколько подозрительных мест и не найдя в них фактической ошибки, программист больше просто не будет смотреть на оставшиеся сообщения. Поэтому правило "лучше ничего не сказать, чем сказать глупость", или "не уверен - промолчи" для верификатора весьма актуально.

А насколько Вы считаете целесообразным и полезным созданием статических анализаторов, таких как VivaMP, для верификации параллельных программ?

Новые языки (типа Java и C#) с неявным освобождением памяти и отсутствием адресной арифметики сделали поведение программы почти детерминированным и избавили от необходимости в миллионах человеко-часов затрачиваемых на отладку программы (куда утекает память, кто трёт эту переменную,...), а также инструментах типа BoundsChecker, задачей которых являлась борьба с злоупотреблением возможностями С/С++.

Но, к сожалению, параллельное программирование - создание многопоточных приложений, без которого сейчас не удаётся решить сколь ни будь даже тривиальную задачу, лишает нас этого детерминизма и опять отбрасывает к временам, когда программисту приходится тратить кучу времени на отладку и сутками крутить тесты, чтобы не убедиться в отсутствии ошибок (тест может только показать их наличие, но не доказать их отсутствие), а по большей части для успокоения своей и team leader-а совести.

Более того, если раньше (да по большому счёту и сейчас в С++), написание параллельное программы требовало значительных усилий, то в C#/Java - создать новый поток намного проще. Эта кажущаяся простота создает у программиста иллюзию, что параллельное программирование - это очень просто, но это, к сожалению, не так и до сих пор, насколько мне известно, не было предложено ни одной модели параллелизма, позволяющей сделать то же, что и сборка мусора для обычных программ (ну если конечно не говорить о чисто функциональных языках, где распараллелить выполнение можно автоматически, не отвлекая на это программиста).

Если мы не умеем решить задачу на уровне правильного дизайна языка, то приходится ставить подпорки в виде верификаторов - статических и динамических). Поэтому возможность нахождения дедлоков и race condition-ов в программах представляется мне одной из самых важных задач сегодняшних верификаторов.

Вы ознакомились с нашими статьями "20 ловушек переноса Си++ - кода на 64-битную платформу", "32 подводных камня OpenMP при программировании на Си++" и так далее? Можете, как то их прокомментировать и дать оценку?

Большое спасибо за ссылки на эти статьи - мне они весьма понравились. Я перешлю эти ссылки коллегам, с которым работаю. Я думаю для многих из них, особенно относительно молодых и неопытных эта информация будет весьма полезна. Когда мне довелось работать Digital Equipment я столкнулся с первыми 64-разрядными системами (DEC Alpha). Проекты в основном были связаны с портированием (c VMS/VAX на Digital Unix/Alpha и с RSX/PDP на OpenVMS/Alhpa ). Поэтому все те грабли с портированием на платформу другой разрядности, о которых вы пишите в статьях, нам

пришлось попробовать на собственной шкуре. Дело ещё осложнялось тем, что Альфа требовала жёсткого выравнивания данных.

Вы посмотрели на демонстрационные версии Viva64 и VivaMP? Что Вы можете посоветовать, чтобы сделать их более популярными? Какие способы продвижения их на рынке могут оказаться удачными на Ваш взгляд?

А вот на сами инструменты Viva64 и VivaMP ещё не смотрел, но обязательно посмотрю. Но по опыту работы с верификатором в TogetherSoft/Borland, я могу сказать (предупредить) что, как и почти в любом коммерческом продукте, в верификаторе примерно 10% действительно интересных идей и алгоритмов и 90% достаточно скучных вещей, без которых, к сожалению, никак нельзя обходится коммерческому продукту:

  • Интеграция со многими (в идеале со всеми) популярными средами разработки. Это достаточно сложно, так как дело касается не только интерфейсной части, но чтобы быть полноценно интегрированной в IDE необходимо уметь работать с родным внутренним представлением программы (AST).
  • Standalone режим (свой собственный парсер, свой генератор отчетов и т.д.);
  • Возможность инкрементальной работы.
  • Автофиксы (возможность автоматически исправлять простые ошибки).
  • Генерация всевозможных отчётов, графиков, экспорт в Excel и.т.п.
  • Интеграция с системами автоматической сборки.
  • Примеры (на каждое сообщение должно быть по простому и понятному примеру на каждом из поддерживаемых языков);
  • Документация. По каждому сообщению должен быть интерактивная справка, объясняющая почему это сообщение было выдано. Кроме того необходимо общее руководство (users guide).
  • Подробное и удобное "целеуказание". Например, если мы говорим что тут возможен дедлок, то мы должны показать пользователю всю возможную траекторию возникновения дедлока.
  • Масштабируемость. Должна быть возможность обработать проект из нескольких миллионов строк за разумное время.
  • Хороший сайт, с форумом, желательно с блогом одного из ведущих разработчиков, с регулярно обновляемой тематической информацией. Например С-lint в своё время в каждом номере журнала Dr.Dobbs давал рекламу с примером ошибки находящимся c-lint-oм. Выглядело это как ребус и действительно привлекало внимание к продукту.

В общем, как и во всём, получается, что написать какой-то продукт достаточно просто (это в состоянии сделать один человек за несколько месяцев). А вот для того чтоб превратить его в настоящий коммерческий продукт требуется на порядок больше усилий. Причём усилий не самых творческих и интересных. Ну а чтоб это потом ещё научится продавать и зарабатывать на этом деньги, нужен совсем другой талант.

Большое спасибо за беседу, интересные и содержательные ответы

Спасибо. Мне тоже было приятно пообщаться с Вами.

Заключение

Еще раз хотим поблагодарить Константина за участие в интервью и разрешение разместить этот материал в сети. Многие его советы мы считаем крайне полезными и непременно постараемся воплотить их в наших программных продуктах статического анализа.

Библиографический список

  • Домашняя страничка Константина Книжника. http://www.garret.ru/
  • Описание JLint. http://www.garret.ru/jlint/ReadMe.htm
  • Сайт компании ООО "Системы программной верификации". http://www.viva64.com/ru/main/
  • И.В. Абрамов, С.Е. Горелкин, Е.А. Горелкина, К.А. Книжник, А.М. Рахимбердиев. Опыт разработки статического анализатора для поиска ошибок в Java-программах. // Информационные технологии и программирование: Межвузовский сборник статей. Вып. 2 (7) М.: МГИУ, 2003. 62 с.
  • Knizhnik, Konstantin. "Reflection for C++." The Garret Group. 4 Nov. 2005. http://www.garret.ru/cppreflection/docs/reflect.html
  • Андрей Карпов, Евгений Рыжков. 20 ловушек переноса Си++ - кода на 64-битную платформу. http://www.viva64.com/ru/a/0004/
  • Алексей Колосов, Евгений Рыжков, Андрей Карпов. 32 подводных камня OpenMP при программировании на Си++. http://www.viva64.com/ru/a/0054/


Найдите ошибки в своем C, C++, C# и Java коде

Предлагаем попробовать проверить код вашего проекта с помощью анализатора кода PVS-Studio. Одна найденная в нём ошибка скажет вам о пользе методологии статического анализа кода больше, чем десяток статей.

goto PVS-Studio;

Андрей Карпов
Статей: 375


Найденные ошибки

Проверено проектов
361
Собрано ошибок
13 417

А ты совершаешь ошибки в коде?

Проверь с помощью
PVS-Studio

Статический анализ
кода для C, C++, C#
и Java

goto PVS-Studio;