SAW: Как оно работает:
(как оно не работает - отдельная тема): возьму пример из их тюториала: функцию поиска первого ненулевого бита в 32-битном слове:
// 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-солвера.
// 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-солвера.