final-report-sukhanova-2011 (1184403), страница 2
Текст из файла (страница 2)
Как следствие,некорректно считалось число единичных бит в последнем (неполном) числе.Если последнее (неполное) слово по битам занимает меньшеполовины BITS_PER_LONG, то есть меньше UL, то побитовый сдвигпроисходит нормально. Но если последнее слово будет занимать большеполовины BITS_PER_LONG, то при сдвиге в BITMAP_LAST_WORD_MASKпроизойдет ошибка, и получится неверный результат.
Данная ошибкаотлавливается во 2й ветви функциональности, где последнее число занимаетBITS_PER_LONG-20 бит.7Верификация алгоритмаОписание спецификации требований в синтаксисе ACSLСпецификация целевой функции bitmap_weight64:@ requires@(( bits >= 0 ) &&@( (bits%BITS_PER_LONG) ?@\valid_range(bitmap, 0, bits/BITS_PER_LONG) :@\valid_range(bitmap, 0, bits/BITS_PER_LONG-1) ));@ ensures@(\result == bit_list_hweight(@create_bit_list_from_array{Here}(bitmap, bits,0) )@);Предусловие: все указатели на рассматриваемые элементы массива недолжны быть null и должны допускать корректное разыменование, иколичество рассматриваемых бит не должно быть меньше нуля.Постусловие: функция должна возвращать в качестве результата количествоединичных бит в рассматриваемой части массива.Спецификация использующейся в bitmap_weight64 функции hweight64:@ requires \true;@ ensures@(\result == bit_list_hweight (create_bit_list (w, BITS_PER_LONG)));Постусловие: функция должна возвращать в качестве результата количествоединичных бит в числе w.Данные спецификации эквивалентны спецификации, описанной впредыдущей части.Описание ошибок в реализации, которые были выявлены припомощи верификацииВ ходе верификации ошибок в реализации выявлено не было.Описание выбранных инвариантов и вариантовВ целевой функции присутствует один цикл.
Для него были написаныследующие инварианты и варианты:@ loop invariant@ (( 0 <= k <= lim ) &&@ ( w == bit_list_hweight(8@create_bit_list_from_array{Here}(bitmap, k*BITS_PER_LONG,0)) ));@@ loop variant lim - k;В этом цикле просматриваются все числа unsigned long long int, вкоторых нужно рассматривать все биты, и осуществляется подсчетколичества единичных битов в них. Инвариантом цикла является то, что накаждом шаге у нас подсчитано количество единичных бит в ужепросмотренной части массива. Вариант цикла – количество оставшихся дляпросмотра чисел, которое уменьшается на один на каждой итерации, пока непросмотрены все целиковые числа.Описание и обоснование лемм num_ops_*.Лемма num_ops_and_hweight:@lemma num_ops_and_hweight:@\forall unsigned long long w, integer i;@( (0 <= i < 32) ==>@read_num_from_bits(create_bit_list@((w - ((w >> 1) & 0x5555555555555555ull)),BITS_PER_LONG), 2*i, 2) ==@hweight_bits (create_bit_list(w,BITS_PER_LONG), 2*i, 2) );В данной лемме говорится о том, что в каждой паре битов результата,полученного битовыми операциями на первом шаге функции hwight64(unsigned long long int res = w - ((w >> 1) & 0x5555555555555555ull);),находится число, равное количеству единичных битов в этой паре для числаw.Рассмотрим утверждение для некотого i (в условии леммы для iстоит \forall).Из результата, полученного на первом шаге, создается bit_list (спомощью функции create_bit_list), из которого с помощью функцииread_num_from_bits считывается число, которое закодировано текущейпарой битов (начинающейся с индекса 2*i).С другой стороны, из числа w создается bit_list (с помощью функцииcreate_bit_list) и с помощью функции hweight_bits подсчитывается числоединиц в этой паре битов (начинающейся с индекса 2*i).Две величины, полученные слева и справа, должны быть равны длявсех i от 0 до 31 (так как мы берем пары).
Таким образом, в данной леммеутверждается, что после первого шага в каждой паре битов закодированочисло единичных битов в соответствующей паре битов в числе w.Грубо говоря, данная лемма является условием, что мы правильнопонимаем, что именно происходит на первом шаге.Лемма num_ops_for_step2:9@lemma num_ops_for_step2:@\forall unsigned long long res, integer i;@( (0 <= i < 16) ==>@read_num_from_bits(create_bit_list@(((res & 0x3333333333333333ull)@+ ((res >> 2) & 0x3333333333333333ull)),@BITS_PER_LONG),@4*i, 4) ==@read_num_from_bits(create_bit_list@(res,BITS_PER_LONG), 4*i, 2) +@read_num_from_bits(create_bit_list@(res,BITS_PER_LONG), 4*i+2, 2) );В лемме утверждается, что в каждой четверке битов результата,полученного битовыми операциями на втором шаге функции hwight64 (res =(res & 0x3333333333333333ull) + ((res >> 2) & 0x3333333333333333ull);),находится число, равное сумме двух чисел, закодированных в первой и вовторой паре битов из этой четверки в результате res до выполнения второгошага.Рассмотрим утверждение для некотого i (в условии леммы для iстоит \forall).Из результата, полученного на втором шаге, создается bit_list (спомощью функции create_bit_list), из которого с помощью функцииread_num_from_bits считывается число, которое закодировано текущейчетверкой битов (начинающейся с индекса 4*i).С другой стороны, из res (взятого до выполнения 2го шага) создаетсяbit_list (с помощью функции create_bit_list), с помощью функцииread_num_from_bits считывается число, которое закодировано первой паройбитов из этой четверки (начинающейся с индекса 4*i), аналогично – длявторой пары битов из этой четверки (начинающейся с индекса 4*i + 2).Эти числа суммируются.Две величины, полученные слева и справа, должны быть равны длявсех i от 0 до 15 (так как мы берем четверки битов).Таким образом, в данной лемме утверждается, что после второго шагав каждой четверке битов закодировано число единичных битов всоответствующей четверке битов в числе w.Грубо говоря, данная лемма является условием, что мы правильнопонимаем, что именно происходит на втором шаге.
Если после выполненияпервого шага в пары бит записались числа единичных бит в этих парах вчисле w, то сумма чисел из двух пар с указанными индексами будет равначислу единичных битов в четверке в исходном числе w.Лемма num_ops_for_step3:10@lemma num_ops_for_step3:@\forall unsigned long long res;@((\forall integer i;@( (0 <= i < 16) ==>@read_num_from_bits(create_bit_list(res,BITS_PER_LONG), 4*i, 4)<=4))@==>@(\forall integer i1;@( (0 <= i1 < 8) ==>@read_num_from_bits(create_bit_list@((res + (res >> 4)) & 0x0F0F0F0F0F0F0F0Full, BITS_PER_LONG), 8*i1, 8) ==@read_num_from_bits(create_bit_list@(res, BITS_PER_LONG), 8*i1, 4) +@read_num_from_bits(create_bit_list@(res,BITS_PER_LONG), 8*i1+4, 4) )@));В этой лемме говорится о том, что если в каждой четверке битов в resзакодировано число, меньшее или равное 4, то в каждой восьмерке битоврезультата, полученного битовыми операциями на третьем шаге функцииhwight64 (res = (res + (res >> 4)) & 0x0F0F0F0F0F0F0F0Full;), находится число,равное сумме двух чисел, закодированных в первой и во второй четверкахбитов из этой восьмерки в результате res до выполнения третьего шага.Условие о том, что в каждой четверке битов в res закодировано число,меньшее или равное 4, очевидно нужно, потому что здесь мы проверяем,что предыдущие операции прошли успешно.
Ведь очевидно, что в каждойчетверке битов не может быть больше 4 единичных битов.Рассмотрим утверждение для некотого i (в условии леммы для iстоит \forall).Из результата, полученного на третьем шаге, создается bit_list (спомощью функции create_bit_list), из которого с помощью функцииread_num_from_bits считывается число, которое закодировано текущейвосьмеркой битов (начинающейся с индекса 8*i).С другой стороны, из res (взятого до выполнения 3го шага) создаетсяbit_list (с помощью функции create_bit_list), с помощью функцииread_num_from_bits считывается число, которое закодировано первойчетверкой битов из этой восьмерки (начинающейся с индекса 8*i),аналогично – для второй четверки битов из этой восьмерки (начинающейся синдекса 8*i + 4).Эти числа суммируются.Две величины, полученные слева и справа, должны быть равны длявсех i от 0 до 7 (так как мы берем восьмерки битов).Таким образом, в данной лемме утверждается, что после третьего шагав каждой восьмерке битов закодировано число единичных битов всоответствующей восьмерке битов в числе w, при условии, что в каждойчетверке до 3го шага было закодировано число, меньшее или равное 4.11Грубо говоря, данная лемма является условием, что мы правильнопонимаем, что именно происходит на третьем шаге.
Если после выполнениявторого шага в четверки бит записались числа единичных бит в этихчетверках в числе w, то сумма чисел из двух четверок с указаннымииндексами будет равна числу единичных битов в восьмерке в исходномчисле w.Лемма num_ops_for_step4:@lemma num_ops_for_step4:@\forall unsigned long long res;@((\forall integer i;@( (0 <= i < 8) ==>@read_num_from_bits(create_bit_list(res,BITS_PER_LONG), 8*i, 8)<=8))@==>@((\forall integer i1;@( (0 <= i1 < 7) ==>@read_num_from_bits(create_bit_list@((res + (res >> 8)), BITS_PER_LONG), 8*i1, 8) ==@read_num_from_bits(create_bit_list@(res, BITS_PER_LONG), 8*i1, 8) +@read_num_from_bits(create_bit_list@(res,BITS_PER_LONG), 8*i1+8, 8) )@)@&&@( 8 >= read_num_from_bits(create_bit_list@((res + (res >> 8)), BITS_PER_LONG), 8*7, 8) ==@read_num_from_bits(create_bit_list@(res, BITS_PER_LONG), 8*7, 8) )@));Данная лемма говорит о том, что если в каждой восьмерке битов в resзакодировано число, меньшее или равное 8, то к каждой восьмерке битоврезультата, полученного битовыми операциями на четвертом шаге функцииhwight64 (res = res + (res >> 8);), добавляется число, находящееся вследующей за ней восьмерке; к последней восьмерке ничего неприбавляется.Условие о том, что в каждой восьмерке битов в res закодированочисло, меньшее или равное 8, очевидно нужно, потому что здесь мыпроверяем, что предыдущие операции прошли успешно.
Ведь очевидно, чтов каждой восьмерке битов не может быть больше 8 единичных битов.Рассмотрим утверждение для некотого i (в условии леммы для iстоит \forall).Из результата, полученного на четвертом шаге, создается bit_list (спомощью функции create_bit_list), из которого с помощью функции12read_num_from_bits считывается число, которое закодировано текущейвосьмеркой битов (начинающейся с индекса 8*i).С другой стороны, из res (взятого до выполнения 4го шага) создаетсяbit_list (с помощью функции create_bit_list), с помощью функцииread_num_from_bits считывается число, которое закодировано этой жевосьмеркой битов (начинающейся с индекса 8*i), к нему добавляется число,закодированное следующей восьмеркой битов.Две величины, полученные слева и справа, должны быть равны длявсех i от 0 до 6 (так как к последней 8ке мы ничего не добавляем), потому чтона четвертом шаге результат суммируется с тем же результатом, толькосдвинутым на 8 (сложение первой восьмой части числа со второй, второй стретьей, третьей с четвертой и так далее).Таким образом, в данной лемме утверждается, что после четвертогошага в каждой восьмерке битов закодировано число единичных битов всоответствующей восьмерке битов в числе w плюс число битов в следующейза ней восьмерке, при условии, что в каждой восьмерке до 4го шага былозакодировано число, меньшее или равное 8.Грубо говоря, данная лемма является условием, что мы правильнопонимаем, что именно происходит на четвертом шаге.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
