kouzdra (kouzdra) wrote,
kouzdra
kouzdra

This journal has been placed in memorial status. New entries cannot be posted to it.

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-солвера.
Tags: saw, verification, Компутерщина, Языки программирования
Subscribe

  • "И все его оставили"

    Чего0то мне кажется, что на Украине жизнь скоро может начать иллюстрировать искусство: Когда случился тот неслыханный скандал, тот крик, и брань, и…

  • Технологии

    "... держать молоток либо какие-то новые технологии...", – считает Володин.

  • Попались обсуждения какого-то

    гопнического сериала про "слова пацанов", там в воспоминательных рассуждаловах всякие личные воспоминание про "с раёнов" - поражает театраьность и…

  • Post a new comment

    Error

    Comments allowed for friends only

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 0 comments