kouzdra (kouzdra) wrote,
kouzdra
kouzdra

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

Как я уже говорил, я поигрался со своими тестиками:

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

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 15 comments