?

Log in

No account? Create an account
kouzdra [entries|archive|friends|userinfo]
kouzdra

[ website | www.kouzdra.org ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

SAW: Как оно работает - 2: [Dec. 3rd, 2019|06:50 pm]
kouzdra
[Tags|, , , ]

В общем - разобрался я "что это было и как это называется" (© Леонид Соболев). На деле оказалось не просто "тупо и просто", а "очень тупо и просто" - и довольно коряво, но для своего реального назначения вероятно самое то.

На деле SAW при всей своей интересности жестко заточена под ровно одну задачу: верификацию криптографии, причем в основном той криптографии которую они пишут на Криптоле.

А одна из главных фишек криптола (при всем его хаскелеобразии) - это возможность трансляции его кода в FPGA (ну или просто в жесткую логику). Разумеется - не любого кода, но вполне понятного подмножества: где ширины битовых полей ограничены, циклы по ним тоже невелики, а прочее делается "в потоке данных" (кой поток изображают свертки-зипперы с бесконечной рекурсией). Насколько этого достаточно на все криптографические случаи жизни, я сказать не возьмусь, но понятно что довольно многое туда попадает.

Потому подход там очень простой: он тупо пытается раскрывать итерации и рекурсию путем "псевдоисполнения" просто даже не утруждая себя вопросами остановки. Если что - просто зацикливается.

Если получилось - все хорошо, если нет - зациклится (приведенный мной пример с делением - просто ошибка в процессе развертки). Заодно понял и как оно казавшиеся головоломными примеры из того поста доказывает.

Ну для простоты - на совсем элементарном примере:
int fact(int n) {
  if (n == 0)
    return 1;
  return fact (m, n-1);
}

int fact6 () {
  return fact (6);
}
Если попробовать загрузить функцию fact, saw немедленно зациклится. А вот если fact6:
m <- llvm_load_module "funcs.bc";
fact6 <- crucible_llvm_extract m "fact6";
print_term fact6;
Все рабоает - только результат скучноват:
[15:32:45.440][15:44:02.099] Loading file "/home/msk/WORK/SNOB/MISC/public-files-/SAW/funcs.saw"
[15:44:02.141] Prelude.bvNat 32 1
Оно просто все посчитало.

Чтобы не посчитало (поскольку в содержательных случаях такого обычно не бывает) - ну я просто параметр добавил:
int fact_mul(int m, int n) {
  if (n == 0)
    return 1;
  return m * fact_mul (m, n-1);
}

int fact6_mul (int m) {
  return fact_mul (m, 6);
}
Тут результат вплоне содержательный:
[15:44:02.099] Loading file "/home/msk/WORK/SNOB/MISC/public-files-/SAW/funcs.saw"
[15:44:02.141] \(arg_0 : Prelude.bitvector 32) -> Prelude.bvNat 32 1
[15:44:02.150] \(arg_0 : Prelude.bitvector 32) ->
  Prelude.bvMul 32
    (Prelude.bvMul 32
       (Prelude.bvMul 32
          (Prelude.bvMul 32 (Prelude.bvMul 32 arg_0 arg_0) arg_0)
          arg_0)
       arg_0)
    arg_0
Ну и замечу что интеллекта на сравнения весьма хитроподвывернутых выражений такого рода у saw уже как раз очень хватает (причем делает он это в том примере на порядки быстрее чем "перебором вариантов".

Еще будет наверное короткий комментарий по поводу исходного теста
Файлы с этим добром:

funcs.c
funcs.saw
funcs.saw_tree
Makefile
LinkReply