MicroTESK

Для примера была использована модель 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))) <--- итоговая склейка двух половин числа