final-report-grechanik-2010 (решения 2010 года)

Московский Государственный Университет имени М.В.ЛомоносоваФакультет Вычислительной Математики и КибернетикиОтчёт по практикумуВерификация программного обеспечения. Функцияbitmap_shift_right.Выполнил:студент 528 группыГречаник Сергей АлександровичПреподаватель:доктор физ.-мат. наукПетренко Александр КонстантиновичМосква, 2010Содержание1 Постановка задачи1.1 Задача по работе с алгоритмом . . . . . .

. . . . . . . . . . . . . . . . . . . .222 Тестирование алгоритма2.1 Описание спецификации целевой функции . . . . . . . . . . . . . . . . . . . .2.1.1 Предусловие . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.1.2 Постусловие . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.2 Обоснование выбранных ветвей функциональности . . . . . . . . . . . . . . .2.3 Характеристики покрытия исходного кода реализации . . . . . . . . . . . . .2.4 Сравнение выбранных ветвей функциональности и ветвей покрытия по исходному коду . . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . . . . . . . .2.5 Описание принципов выбора тестовых данных и их количественных характеристик . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .2.6 Оценки минимальности набора тестовых данных с точки зрения покрытияветвей функциональности и исходного кода . . . . . . . . . . . .

. . . . . . .2.7 Описание ошибок в реализации, которые были выявлены при помощи тестирования . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .4444443 Верификация алгоритма3.1 Описание спецификации требований в синтаксисе ACSL . . . . . . . . . . .3.2 Ошибки в реализации, которые были выявлены при помощи верификации3.3 Описание инвариантов и вариантов . . .

. . . . . . . . . . . . . . . . . . . .3.4 Количество и классификация сгенерированных лемм . . . . . . . . . . . . .3.5 Преобразование функции . . . . . . . . . . . . . . . . . . . . . . . . . . . . .3.6 Неисследованные пути . . . . . . . .

. . . . . . . . . . . . . . . . . . . . . .3.7 Выводы, сделанные по результатам верификации . . . . . . . . . . . . . . .666677884 Заключение.......55551011Постановка задачиЦелевой алгоритм осуществляет сдвиг вправо битового массива. Битовый массив представлен в виде массива чисел типа unsigned long таким образом, что он является конкатенацией битовых представлений соответствующих чисел.void __bitmap_shift_right(unsigned long *dst,const unsigned long *src, int shift, int bits){int k, lim = BITS_TO_LONGS(bits), left = bits % BITS_PER_LONG;int off = shift/BITS_PER_LONG, rem = shift % BITS_PER_LONG;unsigned long mask = (1UL << left) - 1;for (k = 0; off + k < lim; ++k) {unsigned long upper, lower;if (!rem || off + k + 1 >= lim)upper = 0;else {upper = src[off + k + 1];if (off + k + 1 == lim - 1 && left)upper &= mask;}lower = src[off + k];if (left && off + k == lim - 1)lower &= mask;dst[k] = upper << (BITS_PER_LONG - rem) | lower >> rem;if (left && k == lim - 1)dst[k] &= mask;}if (off)memzero(&dst[lim - off], off);}Алгоритм работает следующим образом:1.

Определяется, какое количество элементов нового массива-представления не будутзаведомо нулевыми.2. Для каждого такого элемента считается его значение как некоторая функция отсдвига, количества бит и двух соседних элементов исходного массива-представления.3. Оставшиеся элементы заполняются нулями.1.1Задача по работе с алгоритмом1.

Разработка тестов на основе формальных спецификаций.• Разработка формальной спецификации функциональных требований к работеалгоритма на спецификационном расширении языка Си (SeC).2• Разработка тестовых сценариев, обеспечивающих покрытие всех строк кода реализации алгоритма, с помощью инструмента CTesK.2. Аналитическое доказательство корректности алгоритма.• Добавление в исходный файл с реализацией целевой функции– предусловий и постусловий целевой функции в виде комментариев в соответствии с синтаксисом ACSL– инвариантов и вариантов циклов в целевой функции в виде комментариевв соответствии с синтаксисом ACSL• Проверка того, какие из лемм, сгенерированных инструментом Frama-С, могутбыть доказаны автоматически.• Доказательство оставшихся утверждений при помощи инструмента PVS.32Тестирование алгоритма2.1Описание спецификации целевой функцииvoid __bitmap_shift_right(unsigned long *dst,const unsigned long *src,int shift,int bits);2.1.1Предусловие• Входной массив должен быть битовым массивом длины не менее bits.• Длина массива (bits) должна быть неотрицательной.• Величина сдвига (shift) должна быть неотрицательной и не должна превышатьдлину массива.2.1.2Постусловие• i-й элемент результирующего массива должен быть равен (i + shift)-му элементувходного массива, если он существует, и нулю в противном случае.2.2Обоснование выбранных ветвей функциональностиБыли выбраны следующие ветви функциональности:• Длина массива 0, сдвиг 0.• Длина массива ненулевая, сдвиг 0.• Длина массива ненулевая, сдвиг ненулевой и не равен длине массива.• Длина массива ненулевая, сдвиг равен длине массива.Ветви были выбраны на основе структуры множества допустимых входных параметров.2.3Характеристики покрытия исходного кода реализацииПокрытие исходного кода во время тестирования составляет:• 100% строк исходного кода.• 100% ветвей исходного кода.• 100% вызовов функций исходного кода.42.4Сравнение выбранных ветвей функциональности и ветвей покрытия по исходному кодуВыбранные ветви функциональности соответствуют более высокоуровневому взглядуна алгоритм, поэтому практически ортогональны ветвям покрытия по исходному коду.2.5Описание принципов выбора тестовых данных и их количественных характеристикТестовые данные формировались при помощи отображения множества троек целыхчисел (length, prefix , shift) в домен функции следующим образом:• Входной битовый массив имеет длину length, первые prefix его элементов равны 1,остальные 0• bits = length• shift = shiftНабор троек (length, prefix , shift) формировался следующим образом:• length пробегает от 0 до 3 · BITS_PER_LONG с шагом BITS_PER_LONG/2• prefix пробегает от max(0, length−2·BITS_PER_LONG) до length с шагом BITS_PER_LONG/4• shift пробегает от 0 до length с шагом 1(BITS_PER_LONG - количество бит в unsigned long)Выбор тестовых данных был обусловлен тем, что работа алгоритма сильно зависит отвыравнивания по BITS_PER_LONG.2.6Оценки минимальности набора тестовых данных с точки зрения покрытия ветвей функциональности и исходного кодаНабор тестовых данных не является минимальным, так как его мощность превышаетколичество ветвей функциональности или исходного кода.2.7Описание ошибок в реализации, которые были выявлены припомощи тестированияОшибки в реализации не были выявлены.53Верификация алгоритма3.1Описание спецификации требований в синтаксисе ACSLrequires bits >= 0 && shit >= 0 && shit <= bits&& \valid_range(dst, 0, (bits+31)/32)&& \valid_range(src, 0, (bits+31)/32)&& \base_addr(src) != \base_addr(dst)&& bits + 31 <= 2147483647;ensures same_bits(src, dst, shit, 0, bits);Данная спецификация отличается от предыдущей наличием ограничения на максимальное количество бит, чтобы не произошло арифметическое переполнение.Определения вспомогательных функций:logic integer bit_at{L}(unsigned long* a, integer n, integer k) =k < n ? (a[k / BITS_PER_LONG] >> (k % BITS_PER_LONG)) & 1 : 0;predicate same_bits{L}(unsigned long* a, unsigned long* b,integer sa, integer sb, integer n) =\forall integer k;0 <= k < n ==> bit_at(a, n, sa + k) == bit_at(b, n, sb + k);3.2Ошибки в реализации, которые были выявлены при помощиверификацииБыла выявлена ошибка в следующем операторе:dst[k] = upper << (BITS_PER_LONG - rem) | lower >> rem;Если rem равен 0 (т.е.

сдвиг происходит на количество бит кратное BITS_PER_LONG, топроисходит сдвиг влево на BITS_PER_LONG. Это число равно битовой длине значений типарезультата, а поэтому сдвиг на данное число по стандарту может приводить к неопределённому поведению.3.3Описание инвариантов и вариантовИнвариант цикла выглядит следующим образом:loop invariantk >= 0 &&off + k <= 2147483647 &&k <= lim &&k + 1 <= 2147483647 &&off + k >= 0 &&(\forall integer n; (0 <= n < k) ==>(dst[n] == f(src, shit, bits, lim, left, off, rem, mask, n)));Первые 5 инвариантов устанавливают ограничения на итерационную переменную k.Они вводились по мере возникновения трудностей у автоматического прувера.Последний инвариант описывает, какими значениями заполняется массив dst.Вариант цикла очевиден и записывается следующим образом:loop variant lim - k;63.4Количество и классификация сгенерированных леммТолько для функции __bitmap_shift_right было сгенерировано:• Условия верификации: 24• Условия корректности: 91• Условия завершимости: 2Всего (в том числе и для вспомогательных функций) было сгенерировано 197 лемм.Также было введено 26 вспомогательных лемм.3.5Преобразование функцииИсходная функция содержала большое количество выражений типа bool, что приводило к экспоненциальному увеличению количества генерируемых лемм (более тысячи).Из-за этого возрастало время автоматического доказательства лемм, а также время разбора pvs-файла.