// returns the index of the first non-zero bit uint32_t ffs_ref(uint32_t word) { int i = 0; if(!word) return 0; for(int cnt = 0; cnt < 32; cnt++) if(((1 << i++) & word) != 0) return i; return 0; // not reached }Все понятно, тупо, прямолинейно и - медленно.
Ну соответственно - известный "ускоренный вариант:
uint32_t ffs_imp(uint32_t i) { char n = 1; if (!(i & 0xffff)) { n += 16; i >>= 16; } if (!(i & 0x00ff)) { n += 8; i >>= 8; } if (!(i & 0x000f)) { n += 4; i >>= 4; } if (!(i & 0x0003)) { n += 2; i >>= 2; } return (i) ? (n+((i+1) & 0x01)) : 0; }После компиляции командой
clang -emit-llvm -c ffs.c -o ffs.bcПолучается файло ffs.bc с кодом виртуальной llvm-машины.
Далее посредством такого-вот участка скрипта для SAW:
l <- llvm_load_module "ffs.bc"; print "Extracting reference term: ffs_ref"; ffs_ref <- crucible_llvm_extract l "ffs_ref"; print "Extracting implementation term: ffs_imp"; ffs_imp <- crucible_llvm_extract l "ffs_imp";В SAW подгружается файл ffs.bc и из него в переменные ffs_ref и ffs_imp извлекается из байт-кода какое-то представление функций (моя личная гипотеза что это какая-то форма AST Криптола, хотя гарантии дать не могу.
Далее продолжение скрипта:
print "Proving equivalence: ffs_ref == ffs_imp"; let thm1 = {{ \x -> ffs_ref x == ffs_imp x }}; result <- prove abc thm1; print result;Производит проверку и выдает ее результат. В данном случае "все ОК":
saw ffs_llvm.saw [04:29:03.592] Loading file "/home/msk/WORK/SNOB/SAW/sl-basic/c/ffs_llvm.saw" [04:29:03.595] Extracting reference term: ffs_ref [04:29:03.701] Extracting implementation term: ffs_imp [04:29:03.710] Proving equivalence: ffs_ref == ffs_imp [04:29:04.039] Valid [04:29:04.040] Done.Ну теперь пример "кода с ошибкой":
uint8_t ffs_bug(uint32_t word) { // injected bug: if (word == 0x101010) return 4; // instead of 5 return ref(word); }
Скрипт приводить не буду, поскольку отличие там только в имени второй функции. На выходе получается:
clang -emit-llvm -c ffs.c -o ffs.bc
saw ffs_llvm.saw
[04:41:22.042] Loading file "/home/msk/WORK/SNOB/SAW/sl-basic/c/ffs_llvm.saw"
[04:41:22.045] Extracting reference term: ref
[04:41:22.143] Extracting implementation term: bug
[04:41:22.188] Proving equivalence: ref == bug
[04:41:22.433] prove: 1 unsolved subgoal(s)
[04:41:22.433] Invalid: [x = 0x101010]
[04:41:22.433] Done.
Работает оно если что не перебором: перебор у меня на машинке занимает около 3 минут. Это причем скомпилированного кода, а не llvm-ной VM.В качестве дополнения замечу, что в примере есть еще два варианта реализации функции - "без переходов":
uint8_t imp_nobranch(uint32_t i) { char n = 1; int s1 = !(i & 0xffff) << 4; n += s1; i >>= s1; int s2 = !(i & 0x00ff) << 3; n += s2; i >>= s2; int s3 = !(i & 0x000f) << 2; n += s3; i >>= s3; int s4 = !(i & 0x0003) << 1; n += s4; i >>= s4; // Still does have one branch... return (i) ? (n+((i+1) & 0x01)) : 0; }И известный хитрожопый хак с совершенным хэшем:
uint8_t musl (uint32_t x) { static const char debruijn32[32] = { 0, 1, 23, 2, 29, 24, 19, 3, 30, 27, 25, 11, 20, 8, 4, 13, 31, 22, 28, 18, 26, 10, 7, 12, 21, 17, 9, 6, 16, 5, 15, 14 }; return x ? debruijn32[(x&-x)*0x076be629 >> 27]+1 : 0; }Что интересно - с обоими справляется, хотя на сам деле в последнем случае я не очень понимаю как - по-моему это лежит за пределами функциональности вменяемого SMT-солвера.