kouzdra (kouzdra) wrote,
kouzdra
kouzdra

Categories:

SAW: Как оно работает - 2:

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

На деле 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
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.
  • 0 comments