SAW: И как оно не работает - 2:

[kouzdra]

Разобрался с примерчиком про деление. Вкратце - как и ожидалось, просто ошибка в генерации промежуточного кода из-за которой не сходятся типы:

Напомню исходное:
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, то оно вполне корректно ругается...Написал скриптик, который печатает типы подгруженных функций и их деревяшки:

l <- llvm_load_module "div2.bc";
print "Extracting reference term: ref";
ref <- crucible_llvm_extract l "ref";
print_type ref;
print_term ref;
print "";
print "Extracting implementation term: imp";
imp <- crucible_llvm_extract l "imp";
print_type imp;
print_term imp;
Как и ожидалось:

[09:31:09.379] Loading file "/home/msk/WORK/SNOB/SAW/sl-basic/c/d2.saw"
[09:31:09.403] Extracting reference term: ref
[09:31:09.413] (arg_0 : Prelude.bitvector 0x20) -> Prelude.Vec 0x21 Prelude.Bool
[09:31:09.414] \(arg_0 : Prelude.bitvector 0x20) -> Prelude.bvSDiv 0x20 arg_0 (Prelude.bvNat 0x20 0x2)
[09:31:09.415]
[09:31:09.416] Extracting implementation term: imp
[09:31:09.420] (arg_0 : Prelude.bitvector 0x20) -> Prelude.Vec 0x20 Prelude.Bool
[09:31:09.421] \(arg_0 : Prelude.bitvector 0x20) -> Prelude.bvSShr 0x1f arg_0 0x1
Причина - видимо по каким-то причинам в библиотеке ихней знаковое деление имеет тип с разрядностью на 1 больше аргументов. Для сложения-вычитания это даже и необходимо, зачем может понадобиться для деления - не очень понимаю.

В 16-ти же битном варианте генерируется более страхолюдный код с приведением к 32-битному и вырезанию 167 бит из результата обратно (просто потому что в С так положено):

[09:34:40.702] \(arg_0 : Prelude.bitvector 0x10) ->
Prelude.slice Prelude.Bool 0x10 0x10 0x0
(Prelude.bvSDiv 0x20 (Prelude.bvSExt 0x10 0xf arg_0)
(Prelude.bvNat 0x20 0x2))
который естественно имеет правльный тип:

[09:34:40.701] (arg_0 : Prelude.bitvector 0x10) -> Prelude.Vec 0x10 Prelude.Bool

Upd: Если кому-то интересно - исходный код тут:
https://github.com/kouzdra/public-files-/blob/master/SAW/div2.c
https://github.com/kouzdra/public-files-/blob/master/SAW/div2_16.c

ASTs:
https://github.com/kouzdra/public-files-/blob/master/SAW/div2.saw_tree
https://github.com/kouzdra/public-files-/blob/master/SAW/div2_16.saw_tree

Upd: была бага - засабмитил - (говорят) пофиксили.