Статья представляет интервью, взятое у Константина Книжника, сотрудником компании "Системы программной верификации" Андреем Карповым. Затронуты вопросы статического анализа кода, актуальность решений в этой области, а также перспективы использования статического анализа при разработке параллельных приложений.
Поддержка VivaMP была прекращена в 2014 году. По всем возникшим вопросам вы можете обратиться в нашу поддержку.
Компания ООО "Системы программной верификации" (ООО "СиПроВер") занимающаяся разработкой инструментов в области тестирования и верификации программ попросила ответить на некоторые вопросы Константина Книжника, специалиста в области методологии статического анализа кода. Интервью провел и оформил в виде этой статьи Андрей Карпов, являющийся сотрудником ООО "СиПроВер".
В интервью затронуты вопросы статического анализа кода, актуальность решений в этой области. Обсуждаются перспективы использования статического анализа при разработке параллельных приложений. Получена сторонняя оценка инструментов статического анализа Viva64 и VivaMP, разрабатываемых компанией "СиПроВер". А также обсуждены некоторые общие вопросы верификации программ, которые мы надеемся будет интересно узнать читателям изучающим эту область тестирования приложений.
Вопросы задает (вопросы выделены жирным текстом):
К.ф.-м.н., Андрей Карпов. Технический директор компании "СиПроВер", занимается развитием инструментов анализа кода Viva64 и VivaMP для тестирования 64-битных и параллельных приложений. Автор ряда статей по статическому анализу кода.
На вопросы отвечает:
К.ф.-м.н., Константин Книжник. Автор ряда статей, посвященных статическому анализу программного кода, разработчик верификаторов для Java приложений. Участвовал и продолжает участвовать во многих интересных проектах, например, в WebAlta.
Я действительно интересовался темой статического анализа и верификации программ. Началось всё в 1997 году, когда я написал программку jlint - аналог clint для Java.
Программа состояла из двух частей - простейшего синтаксического анализатора для языков с Си-подобным синтаксисом. В языке Си есть как известно много мест в синтаксисе, которые провоцируют программиста на трудно находимые ошибки. Например, написание "=" вместо "==", пустое тело цикла из за неправильно поставленной точки с запятой ";" и так далее. Перечислять не буду, проблематика, думаю, в общем, достаточно известная.
Вторая часть - это был jlint - более-менее полноценный семантический анализатор для Java. Связываться с написанием собственного Java-парсера мне тогда не хотелось, поэтому я пошёл по пути чтения уже скомпилированного байт кода и анализа его. Проверки включают обращение по нулевой ссылке, несовместимые касты, всегда истинные или всегда ложные выражения, потерю точности и тому подобное.
Самое интересное, что было в jlint - это возможность нахождения потенциальных дедлоков в программе. В Java очень простой механизм блокировок - synchronized метод или synchronized(expr) конструкция. На основании анализа этих конструкций, делалась попытка построить граф блокировок (вершины - это блокируемые ресурсы) и поиск циклов в этом графе. Естественно построить точный граф не возможно, поэтому делалась попытка построения приближённого графа, используя классы вместо конкретных экземпляров объектов. К сожалению, в реальных проектах, эта проверка работала не очень хорошо - было много ложных срабатываний.
Через несколько лет мой 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, я участвую в создании объектно-ориентированной СУБД для встраиваемых систем. Есть и другие проекты.
Так как моя работа в TogetherSoft, а потом в Borland-е была непосредственно связана с верификацией программ, то пришлось свой jlint забросить. Кстати, существующий jlint можно скачать с моего сайта по адресу http://www.garret.ru/lang.html.
Хорошо. Кратко попытаюсь перечислить некоторые основные выводы, к которым я пришёл за годы посвящённые проблеме верификации программ.
Новые языки (типа Java и C#) с неявным освобождением памяти и отсутствием адресной арифметики сделали поведение программы почти детерминированным и избавили от необходимости в миллионах человеко-часов затрачиваемых на отладку программы (куда утекает память, кто трёт эту переменную,...), а также инструментах типа BoundsChecker, задачей которых являлась борьба с злоупотреблением возможностями С/С++.
Но, к сожалению, параллельное программирование - создание многопоточных приложений, без которого сейчас не удаётся решить сколь ни будь даже тривиальную задачу, лишает нас этого детерминизма и опять отбрасывает к временам, когда программисту приходится тратить кучу времени на отладку и сутками крутить тесты, чтобы не убедиться в отсутствии ошибок (тест может только показать их наличие, но не доказать их отсутствие), а по большей части для успокоения своей и team leader-а совести.
Более того, если раньше (да по большому счёту и сейчас в С++), написание параллельное программы требовало значительных усилий, то в C#/Java - создать новый поток намного проще. Эта кажущаяся простота создает у программиста иллюзию, что параллельное программирование - это очень просто, но это, к сожалению, не так и до сих пор, насколько мне известно, не было предложено ни одной модели параллелизма, позволяющей сделать то же, что и сборка мусора для обычных программ (ну если конечно не говорить о чисто функциональных языках, где распараллелить выполнение можно автоматически, не отвлекая на это программиста).
Если мы не умеем решить задачу на уровне правильного дизайна языка, то приходится ставить подпорки в виде верификаторов - статических и динамических). Поэтому возможность нахождения дедлоков и race condition-ов в программах представляется мне одной из самых важных задач сегодняшних верификаторов.
Большое спасибо за ссылки на эти статьи - мне они весьма понравились. Я перешлю эти ссылки коллегам, с которым работаю. Я думаю для многих из них, особенно относительно молодых и неопытных эта информация будет весьма полезна. Когда мне довелось работать Digital Equipment я столкнулся с первыми 64-разрядными системами (DEC Alpha). Проекты в основном были связаны с портированием (c VMS/VAX на Digital Unix/Alpha и с RSX/PDP на OpenVMS/Alhpa ). Поэтому все те грабли с портированием на платформу другой разрядности, о которых вы пишите в статьях, нам
пришлось попробовать на собственной шкуре. Дело ещё осложнялось тем, что Альфа требовала жёсткого выравнивания данных.
А вот на сами инструменты Viva64 и VivaMP ещё не смотрел, но обязательно посмотрю. Но по опыту работы с верификатором в TogetherSoft/Borland, я могу сказать (предупредить) что, как и почти в любом коммерческом продукте, в верификаторе примерно 10% действительно интересных идей и алгоритмов и 90% достаточно скучных вещей, без которых, к сожалению, никак нельзя обходится коммерческому продукту:
В общем, как и во всём, получается, что написать какой-то продукт достаточно просто (это в состоянии сделать один человек за несколько месяцев). А вот для того чтоб превратить его в настоящий коммерческий продукт требуется на порядок больше усилий. Причём усилий не самых творческих и интересных. Ну а чтоб это потом ещё научится продавать и зарабатывать на этом деньги, нужен совсем другой талант.
Спасибо. Мне тоже было приятно пообщаться с Вами.
Еще раз хотим поблагодарить Константина за участие в интервью и разрешение разместить этот материал в сети. Многие его советы мы считаем крайне полезными и непременно постараемся воплотить их в наших программных продуктах статического анализа.