There is contention between the "European school" of language design, who prefer LL-based grammars, and the "US-school", who predominantly prefer LR-based grammars. This is largely due to teaching traditions and the detailed description of specific methods and tools in certain text books; another influence may be Niklaus Wirth at ETH Zürich in Switzerland, whose research has described a number of ways of optimising LL(1) languages and compilers.

LL parser article in wikipedia.

Удаление ложных путей в Goanna

Для заданного контр-примера строится система уравнений интервального анализа. Если наименьшее решение является пустым множеством, то анализируемый контр-пример считается ложным.

В отличии от CEGAR, использующего SAT-решатели, и от подхода на основе аппроксимации многогранниками, предлагаемый в [1] подход имеет меньшие вычислительные затраты.

Формальной моделью является размеченная система переходов LTS (S, S0, A, R, F), являющаяся конечным автоматом над конечными словами.

Вводится понятие интервального автомата:
IA = (L, l0, X, E, update), где L - множество позиций в исходном коде, I0 - начальная позиция, X - множество интервальных переменных, E - множество дуг (определено на L * L), update - функция эффекта (E -> X * C(X)), C(X) - множество выражений над X.

Для интервального автомата определяется функция означивания v: X -> I.

Интервальному автомату P соответствует размеченная система переходов LTS(P) = (S, S0, A, R, F), где S равно множеству пар (l, v), где l - позиция в исходном коде, v - функция означивания. S0 - равно (l0. [-inf, inf]), A - подмножество E, R = S * A * S - множество кортежей вида ((l1, v1), (l1, l2), (l2, v2)). для переходов (l1, l2) из E, таких что v2 = v1[lhs(e) <- [rhsexpr(e)]_v1] и [rhsexpr(e)]_v2 не пусто; F = S.

Построенный автомат принимает только такие слова, которые соответствуют системам интервальных уравнений с непустым решением. Слова, которые соответствуют системам уравнений с пустым решением называются конфликтами.

Программе соответствует интервальный автомат LTS(P). Так как интервальные автоматы имеют бесконечное число состояний, используется конечная аппроксимация P^. Для заданного автомата P = (L, l0, X, E, update) строится абстракция P^ = (L, l0, E, E', L). где E' = {(l1, (l1, l2), l2) | (l1,l2) in E} - отношение переходов. В статье [1] описан итеративный алгоритм уточнения абстракций.

[1] A. Fehnker, R. Huuck, S. Seefried Counterexample Guided Path Reduction for Static Program Analysis // In the Festschrift of Correctness, Concurrency, and Compositionality for Willem-Paul de Roever, Kiel, Germany, 2008.

Goanna: синтаксический model checker

Goanna использует model checking для обнаружения дефектов, зависящих от потока управления, таких как: утечки памяти, использование неинициализированной переменной, возможное разыменование нулевого указателя. Атомарные предикаты формируются путем поиска по шаблону конструкций выделения, использования и освобождения ресурса p.

В статье [1] приводится пример формулы CTL для описания корректной работы с памятью:

AG(malloc_p => AG(free_p => !EF used_p))

Кстати, на мой взгляд в формуле есть ошибка в темпоральном операторе перед предикатом free_p.

Для обнаружения ошибок типа переполнения буфера используется интервальный анализ (на основе абстрактной интерпретации). Простые циклы анализируются без использования техники расширения (widening).

Для уменьшения числа ложных обнаружений используется статический анализ контр-примера. По результатам этого анализа строится автомат-наблюдатель (observer automaton), который в дальнейшем используется для удаления ложных путей. Выполняется проверка синхронного произведения автоматов-наблюдателей и исходной модели программы. Процесс уточнения повторяется до тех пор пока перестают обнаруживаться новые дефекты и перестают удаляться ложные пути.

[1] A. Fehnker, J. Brauer, R. Huuck, S. Seefried Goanna: Syntactic Software Model Checking //
6th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2008 Seoul, Korea.

Третий день SECR 2010

В третий день (15 октября) изначально было мало заинтересовавших меня докладов.

Первым из посещенных мною докладов был доклад Евгения Зуева из Интерстрон "Семантические интерфейсы языков программирования". Семантический интерфейс -- это набор классов С++, который соответствует узлам AST с небольшими дополнениями. Одной из задач исследований автора было использование XML для хранения модели и XSLT для преобразований кода. Выступление было сильно затянуто, и даже не хватило времени на вопросы. Пришлось задавать вопросы в коридоре. Готового парсера пока нет, он находится в разработке. Почему в качестве тестовой задачи для фреймворка было выбрана задача реинжиниринга UML, а не рефакторинг или какая-нибудь задача статического анализа выяснить не удалось. Почему нужно самим разрабатывать парсер, а не использовать готовый (GCC, Eclipse CDT, OpenCpp) также не очевидно. Ответ, что там теряется информация меня не очень устраивает.

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

Как всегда зажигал на конференции Стас Фомин. Умеет человек рассказывать интересно! Хотя, по большому счету, сказать что он предлагает что-то интересное и оригинальное нельзя: использовать вики для презентаций,делать презентации быстро и повторно использовать в следующий раз, тестировать знания в процессе обучения/самообучения.

В завершение был доклад Бьярна Страуструпа "Введение в C++0x". Было довольно интересно посмотреть на Бьярна и послушать про новый стандарт от создателя языка. Появилось желание почитать стандарт и попробовать фичи, реализованные в GCC.

CEE-SECR 2010. День второй

На мой взгляд, лучшими докладами второго дня были:

• Марат Ахин "Обнаружение клонов: современное состояние дел"


• Денис Тимофеев "Технология модификации программного кода, основанного на параметризуемых шаблонах"


• Михаил Моисеев "Обнаружение дефектов в многопоточных программах с синхронизацией на основе семафоров"

Их комментировать не буду.

Доклад про манифеcт SOA был для меня бесполезен. И тема SOA в целом не очень интересна, и обсуждение манифеста тем более!

Доклад Наталии Вегериной (Инфострой) "Экспертная система анализа качества исходного кода" был посвящен странной задаче: выдаче рекомендаций по улучшению качества исходного кода на основе анализа метрик.

Ирина Кузьмина (ФТИИ) поведала об особенностях реализации процесса интеграции при разработке сложных программно-аппаратных комплексов. Это доклад о том, как в конкретной организации пришли к Continuous Integration с использованием ClearCase, Putty и CruiseControl.NET.

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

Интересным событием второго дня стал круглый стол "Написание статей по программной инженерии: курс молодого бойца". Круглый стол показал отсутствие единой точки зрения как в самом программном комитете, так и среди участников. Возможно, это поможет сформировать единые критерии рецензирования и повысить статус конференции.

CEE-SECR 2010

Конференция в целом оставила хорошие впечатления. Доклады на конференции были разной тематики, различного уровня и интересности. Конференция немного изменилась по сравнению с CEE-SECR 2009, который был совмещенным с SQA-Days: уменьшилось количество тестировщиков как среди участников, так и среди докладчиков. Кроме того, уменьшилось число докладчиков из научной среды. Сложилось впечатление, что уменьшился средний уровень докладов, хотя хорошие и интересные доклады были и на этой конференции.

Яркими пятнами первого дня конференции (13 октября) стали выступления:

• Андрея Уразова из компании Parasoft "Программирование, ориентированное на качество"


• Владимира Рубанова из ИСП РАН "Автоматическая генерация базовых тестов для программных
  интерфейсов библиотек на основе заголовочных файлов"

Эти два доклада показались интересными как своей тематикой, так и подготовкой докладчиков, хорошими ответами на вопросы.

Андрея Уразова спрашивали про точность и полноту обнаружения их средства статического анализа. По его примерным оценкам точность средства 80%. Измерений полноты анализа не выполнялось.

На сайте компании перечислены типы обнаруживаемых дефектов для С/С++:

• uninitialized or invalid memory


• null pointer dereferencing


• array and buffer overflows


• division by zero, memory and resource leaks, and dead code.

Владимира Рубанова спрашивали о смысле предлагаемого тестирования (функция вызывается с какими-то параметрами, результат не проверяется или проверяется слабо). Есть возможность как-то вручную управлять способом получения параметров. Применяется для свободно-распространямого ПО, в котором совсем нет тестов. Какие-то тесты лучше, чем никакие. Применение разработанного инструмента -- API Sanity Autotest -- позволило найти баги в реальных проектах. Сам проект свободно-распространяемый.

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

В завершении первого дня выступали Алексей Алексеев и Николай Гребнев из CustIS. Тема их доклада -- "Уменьшение влияния человеческого фактора" -- не очень совпадала с содержимым. Основной интерес для меня в их докладе был в использовании modelchecking для проверки бизнес-логики. В их подходе задаются аннотации к методам: StateTransition(fromState, toState) и StateRequire(CTL-formula). Первая аннотация означает, что вызов метода изменяет состояние с fromState в toState. Вторая аннотация описывает предусловие, которое должно выполняться в состоянии перед вызовом метода. Предусловие описывается CTL-формулой. Используется собственная реализация алгоритма CTL modelchecking.

Goanna. Обнаружитель дефектов на основе modelchecking

Goanna позволяет обнаруживать следующие типы дефектов в программах на С/С++:

• ошибки выхода за границу массива


• арифметические ошибки


• ошибки копирования


• ошибки непредсказуемого поведения (неинициализированные переменные)


• ошибки работы с памятью


• ошибки с указателями на функции


• ошибки неправильного использования указателей


• ошибки неспецифицированного порядка выполнения.

Для обнаружения дефектов используется верификатор NuSMV. Подробнее использование верификатора описано в статье Goanna: Syntactic Software Model Checking

Разработчики проверяли средство на свободно-распространяемых проектах, в том числе на Firefox.Плотность обнаружения дефектов составила 0.3-2 дефекта на 1000 строк исходного кода.

Для получения более объективной картины ниже приведены результаты средства на простых тестах (менее 20 строк кода, 1 функция):

• Выход за границу массива -- находятся случаи, когда реально выходят за границу массива и не находятся случаи, когда выходят за границу размерности (например, a[1][-1] в массиве размера 2x2)


• Разыменование указателя, выведенного за границу объекта -- не обнаруживается вообще


• Переполнения буфера для memcpy не обнаруживается


• Сравнение и вычитание указателей на различные объекты не обнаруживается


• Использование неинициализированной переменной (памяти)




• через указатель не находит


• в виде параметров функции находит


• не находится при копировании неинициализированной памяти с помощью memcpy




• Разыменование неинициализированного указателя -- находится


• Разыменование нулевого указателя -- находится в простых случаях, при использовании результата malloc, но не находится для статического указателя (инициализируется нулем)

Необходимо отметить, что ошибки выхода за границу массива достаточно хорошо обнаруживаются средством в рамках одной функции, но не находятся при межпроцедурном варианте теста.

В средстве реализовано обнаружение множества дефектов, то есть после нахождения одного дефекта анализ продолжается. Например, в коде

#include
int main(void)
{
int *p = NULL;
int *q = NULL;
*p = 0;
*q = 0;
return 0;
}

Обнаруживаются ошибки для обоих указателей, хотя после разыменования p программа упадет.

Средство порадовало отсутствием ложных обнаружений, хотя понятно, что для тестирования использовались простые программы, в которых у качественного анализатора не должно быть ложных обнаружений. Если посмотреть возможности обнаружения дефектов, то они весьма средние. Например, крайне сложные и важные для языка C ошибки выхода за границу объекта не обнаруживаются вообще.
Для тестирования использовалась версия goanna-cmdline-linux-2.1.tgz с интерфейсом командной строки.