Для начала простейший: как известно знаковое деление на 2 нельзя "оптимизировать" арифметическим сдвигом: на отрицательных числах они округляют в разные стороны потому результат на нечетных отрицательных числах отличается на 1:
typedef int32_t my_int;
my_int ref (my_int n) {
return n/2;
}
my_int imp (my_int n) {
return n>>1;
}Увы: вместо искомого, скрипт выдает:clang -emit-llvm -c div2.c -o div2.bc
saw div2_llvm.saw
[05:06:40.821] Loading file "/home/msk/WORK/SNOB/SAW/sl-basic/c/div2_llvm.saw"
[05:06:40.824] Extracting reference term: ref
[05:06:40.841] Extracting implementation term: imp
[05:06:40.844] Proving equivalence: ref == imp
[05:06:40.869] Cryptol error:
[error] at /home/msk/WORK/SNOB/SAW/sl-basic/c/div2_llvm.saw:11:30--11:33:
Type mismatch:
Expected type: 33
Inferred type: 32
../Makefile.common:9: recipe for target 'saw_c' failed
Замечу, что если заменить тип на int16_t, то оно вполне корректно ругаетсяЖclang -emit-llvm -c div2.c -o div2.bc saw div2_llvm.saw [05:10:20.254] Loading file "/home/msk/WORK/SNOB/SAW/sl-basic/c/div2_llvm.saw" [05:10:20.257] Extracting reference term: ref [05:10:20.275] Extracting implementation term: imp [05:10:20.278] Proving equivalence: ref == imp [05:10:20.484] prove: 1 unsolved subgoal(s) [05:10:20.485] Invalid: [x = 0xd553] [05:10:20.485] Done.Моя личная гипотеза - что в силу "отсутствия запаса по разрядности" в случае полного целого SAW при генерации криптоловского аналога то ли в одном месте добавляет не по делу один разряд, то ли наоборот - забывает добавить. В Криптоле числа представляются битовыми последовательностями константной длины - int16 соответственно имеет тип [16], in32 - [32], ну и вполне вероятно для корректного отображения смешанной семантики int32/uint32 или чего-то в этом роде нужен [33], как адекватно вмещающий и то и другое. Ну и напутали где-то. Получили несоместимость типов [32] и [33].
Второй пример - числа фиббоначи:
int ref (int n) {
if (n == 0 || n == 1)
return 1;
return ref (n-2) + ref (n-1);
}
int imp (int n) {
int a = 1;
int b = 1;
while (n >= 2) {
int t = a + b;
a = b;
b = t;
-- n;
}
return b;
}Тут все просто - умирание на импорте рекурсивного варианта:clang -emit-llvm -c fib.c -o fib.bc saw fib_llvm.saw [05:15:47.539] Loading file "/home/msk/WORK/SNOB/SAW/sl-basic/c/fib_llvm.saw" [05:15:47.566] Extracting implementation term: imp [05:15:47.642] Symbolic simulation completed with side conditions. [05:15:47.651] Extracting reference term: ref ...Несколько по мне странно - но в принципе понятно. А вот с факториалом все чудесатее:
int ref (int n) {
int res = 1;
int i = 1;
while (i <= n) {
res *= i;
++ i;
}
return res;
}
int imp (int n) {
int res = 1;
while (n != 0) {
res *= n;
-- n;
}
return res;
}
Тоже виснет - но на импорте второй функции:saw fact_llvm.saw [05:18:35.596] Loading file "/home/msk/WORK/SNOB/SAW/sl-basic/c/fact_llvm.saw" [05:18:35.598] Extracting reference term: ref [05:18:35.627] Symbolic simulation completed with side conditions. [05:18:35.630] Extracting implementation term: impРазумных отличий я не вижу тут :)
Upd: была бага - засабмитил - пофиксили.