?

Log in

No account? Create an account
nyaload

Журнал Пушыстого

Журнал Пушыстого

Previous Entry Share Flag Next Entry
Верификация С кода - сегодня
nyaload
_winnie
Похоже, появился юзабельный верификатор кода на C.
http://vcc.codeplex.com/

В примерах - доказывается корректость двоичного поиска, сортировку, что-то про межпоточную блокировку. Да! верификатор нацелен на многопоточные программы!

Вот туториал с примерами - http://research.microsoft.com/en-us/um/people/moskal/pdf/vcc-tutorial-2col.pdf

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

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

Например, вот двоичный поиск:
unsigned binary_search(int val, int *arr, unsigned len) //требования на вход requires(is_mutable_array(arr, len)) requires(forall(unsigned i,j; i < j && j < len ==> arr[i] <= arr[j])) //описание результата ( uint(-1) если не найдено, индекс элемента если такой есть ) ensures(result != UINT_MAX ==> arr[result] == val) ensures(result == UINT_MAX ==> forall(unsigned i; i < len ==> arr[i] != val)) { unsigned low, high, mid; low = 0; high = len; while (low < high) //подсказка для прувера (описание того, что происходит с переменными в цикле) invariant(high <= len) invariant(forall(unsigned i; i < low ==> arr[i] < val)) invariant(forall(unsigned i; high <= i && i < len ==> arr[i] >= val)) { mid = low + (high - low) / 2; if (arr[mid] < val) low = mid + 1; else high = mid; } if (low < len && arr[low] == val) return low; else return UINT_MAX; }
_Winnie C++ Colorizer

Хотел попробовать, что будет если добавить тонких ошибок в двоичный поиск. Но не получилось из-за комбинации софта у меня дома и идиотизма web/install-программистов microsoft (нужен dotnetfx 3.5 , который не захотел устанавливаться с сообщением "произошла ошибка", нужен компилятор от VisualC++ 2008 (не 2010, omg wtf), нужен логин microsoft LiveID для скачки компилятора и тд, у меня старые IE6 и WinXP на домашнем компьютере). Думаю, скоро будет более внятная инсталляция.

Тем не менее, выглядит нацеленным на реальное использование, а не на защиту диссертаций. Хвалятся, что их тулза используется для верификации 100 килобайт кода из Hyper-V.

Интересно, если ли подобная работающая тулза под Unix?

Когда-нибудь будет следущий этап, когда достаточно написать только требования, а инварианты верификатор сам придумает :) А затем - ещё и код сам напишет.


  • 1
вау... похоже, что из этапа защиты диссертаций это доросло до хоть кого-нибудь продакшен. тоже хочу узнать ответ на вопрос про юниксовые утилиты.

См. ниже дискуссию о frama-c

А frama-c под линукс не то же самое делает? У нас для сдачи заданий по верификации использовались frama-c + PVS (или ты это тоже сдавал?). Автоматически не все доказывалось, правда.

P.S: Имхо, правда, это все равно полный бред, и курс верификации та ещё муть.

Я бегло прочитал доку, это может быть интересным инструментом для code review и для реверс-инжиниринга куч сишного кода, но я не нашёл примера использования для доказательства какого-нибудь свойства функции (типа корректности сортировки).

Мы сдавали какой-то невнятный RSL, непонятно для чего (на нём можно писать спецификацию, но неясно как это относится к верификации реальных ЯП).

Как оно в сравнении с coverity?

Эм. Я пока что не запустил VCC, а coverity кажется вообще нельзя скачать с сайта ("У кого нет миллиарда долларов, могут идти в жопу").

Очевидно, можно отметить следующее:

1) VCC для C, а не для Java/C++ (но есть конвертеры C++->C)

2) VCC - он для доказательства, что в коде НЕТ ошибок. При этом от человека требуется выписать основные подсказки для доказательства. coverity насколько я вижу из текста на сайте - помогает найти подозрительные места, но не доказывает их отсутствие. И подозреваю не проверяет корректность сложных алгоритмов, что поиск ищет а сортировка сортирует. Но без документации точно не скажешь.


Edited at 2011-01-25 08:40 pm (UTC)

> нужен компилятор от VisualC++ 2008 (не 2010, omg wtf), нужен логин microsoft LiveID для скачки компилятора и тд, у меня старые IE6 и WinXP на домашнем компьютере)

Винни, ты чего? Фреймворк отлично ставится на голую Windows XP SP3. Вот ссылка на standalone дистрибутив: .NET Framework 3.5 Service Pack 1 (Full Package).

Ну, у меня веб-инсталлер скачивал всякое, начинал установку и показывал такое окно: http://dobrokot.ru/pics/nya2011-01-25__23-27-09_13kb.png
Я пробовал смотреть process explorer и читать логи, но не разобрался. BTW, у меня SP2 и SP3 по определённым причинам накатывать не хочу :)

Мне проще на работе посмотреть, а винду дома переставить с нуля, давно на семерку переезжать пора.

Далее, на сайте микрософта есть 2010 Express, а эта VCC сейчас привязана к компилятору от 2008. Гугль находит страничку на MS с версий 2008, но JavaScript на ней глючит и не даёт скачивать. И так же намекается, что надо зарегаться в каком-то MS Passport Live ID, иначе проработает только месяц. Спасибо, я лучше куплю в торрентах Team Edition без регистрации, вопросов о том как зовут мою маму и прохождением тестов на роботов.

Вообщем, я не настроен сейчас проходить квест на переинсталляцию всего ради того, что бы потыкать VCC.


Edited at 2011-01-25 08:42 pm (UTC)

А плюсы он, я так понял, не скушает?

Да, чистый С.

Правда, когда я читал про упомянутый выше frama-c - я наткнулся на упоминание http://llvm.org/docs/FAQ.html#translatecxx

Так же, эти верификаторы - они ИМХО слабо преднадначены для проверки существующих мегоговн С++. Скорее, для того, что бы писать какие-то сложно-алгоритмические и критические вещи с нуля. Потому что что бы выписать инварианты цикла - надо будет досконально разобраться как работает код, и почему он работает самому. А верификатор проверит, что разобрался правильно :)


Нихрена себе! Молодцы!

Я недавно офигел от того, что умеют SMT-солверы, советую заодно google it. См. тж. http://corp.galois.com/blog/2011/1/18/merging-smt-solvers-and-programming-languages.html - вглубь оттуда по ссылкам. Очень круто.

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

Звучит как юнит-тесты :)

Звучит гораздо лучше юнит-тестов, ибо тесты не прогонишь для всех возможных значений аргументов.

А это проверяется при работающей программе? (как ассерции)

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

> Когда-нибудь будет следущий этап, когда достаточно написать только требования, а инварианты верификатор сам придумает :) А затем - ещё и код сам напишет.

Да, я уже сплю и вижу, как такие надёжные, инновационные и применимые в реальной жизни инструменты, как frama-c и PVS отбирают у меня последний кусок хлеба без масла.

Это далеко не первое изобретение которое "отменит" программистов. Вот только выльется оно в то, что потребуются квалифицированные писальщики требований/спецификаций -- те-же самые программисты.

Прикольно.

Вообще не очень удивительно: C же на самом деле намного более высокоуровневая, чем кажется на первый взгляд. Типа, возможность смотреть на всю память как на массив байтов является implementation detail и активно неодобряется стандартом.

Для Linux есть Valgrind

Кстати, VCC можно легко потрогать через web-interface: http://rise4fun.com/vcc

  • 1