Bug #9787
closedНекорректное восстановление 64-х битных чисел из памяти.
0%
Description
Для примера была использована модель risc-v 64-bit. В архиве содержится бинарный и ассемблерный код функции size_test, которая принимает параметром аргумент типа size_t (64-bit) и его же возвращает в качестве результата. Также приложен вывод функции symexecute - smt-lib код. В подпапке size_test_merged содержатся два smt-lib файла, block_0_target_0.smt2 и block_0_target_0_fixed.smt2, в которых к коду функций была добавлена цель верификации, при этом в файле _fixed ошибка исправлена (получен вердикт unsat).
Суть ошибки:
Ошибка возникает при загрузке из памяти 64-х битных чисел больших, чем 2^32-1. В ассемблерном файле строка 5,
в nml представлении:
tmp_dword<63..32> = MEM[mem_index + 1];
tmp_dword<31..0> = MEM[mem_index];
В smt-lib представлении (block_0_target_0.smt2 строки ~ с 1244 по 1263) с комментариями:
(assert (= %158 (select MEM!25 %157))) ; <--- загрузка из памяти старших 4-х байт числа. (assert (= %160 ; <--- знаковое расширение до 64 битов. в данном случае ошибка не возникает из-за сдвига, ((_ sign_extend 32) %158))) ; однако несколько некорректно - лучше заменить на беззнаковое. (assert (= %161 (bvand tmp_dword!1 #b0000000000000000000000000000000000000000000000000000000000000000))) ; <--- операция не имеет ?? смысла и не влияет на итоговый результат (assert (= %162 (bvshl %160 #b0000000000000000000000000000000000000000000000000000000000100000))) ; <--- побитовый сдвиг на 32 (assert (= %159 (bvor %161 %162))) ; <--- склейка частей, а по факту одной части и ноля (assert (= tmp_dword!2 %159)) (assert (= %163 (select MEM!25 %154))) ; <--- загрузка младших 4-х байт числа. (assert (= %165 ((_ sign_extend 32) %163))) ; <--- знаковое расширение числа. Впоследствии приводит к ошибке при склейке частей. Необходимо заменить на беззнаковое. (assert (= ; <--- а здесь главная ошибка - некорректная битовая маска приводит к занулению %166 ; ранее подготовленных старших 4-х байт числа. корректная маска содержи 32 единицы (bvand %159 #b0000000000000000000000000000000000000000000000000000000000000000))) ; в старших битах. (assert (= %167 (bvshl %165 #b0000000000000000000000000000000000000000000000000000000000000000))) ; <--- сдвиг на 0. (assert (= %164 (bvor %166 %167))) <--- итоговая склейка двух половин числа
Files
Updated by Artem Kotsynyak about 5 years ago
- Status changed from New to Feedback
Updated by Alexander Kamkin about 5 years ago
- Subject changed from Symexecute - некорректное восстановление 64-х битных чисел из памяти. to Некорректное восстановление 64-х битных чисел из памяти.
- Category set to Symexecutor
Updated by Artem Kotsynyak almost 5 years ago
- Status changed from Feedback to Closed