kouzdra (kouzdra) wrote,
kouzdra
kouzdra

Category:

"Как они работали в очистке?"

По итогам вчерашних-позавчерашних изучений системки SAW (Software Analysis Workbench) возник вопрос subj.

В смысле - меня попросили посмотреть и по возможности поломать ее верификатор (ради которого она собственно и существует).

Системка по задумке интересная - предназначена для доказательства функциональной эквивалентности разных функций на C, Java и Cryptol* (вещь на сам деле нужная очень - потому ситуация когда есть неэффективная но простая референтная реализация и ее эффективный но совершенно нечитабельный "прикладной" вариант довольно обычна и ловить там баги на расхождениях - удовольствие то еще), ну и на сам деле и несколько более сложных вещей (возможно отпишусь подробнее отдельным постом) и на приведенных в поставке примерах (весьма нетривиальных) демонстрирует вроде бы круть немерянную.

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

Результат оказался впечатляющим - из трех тривиальнейших примеров (все три намного проще ихних) на двух с половиной до собственно верификации дело не дошло - в первом случае функции в одну строчку отработали с аргументами типов int8_t и int16_t, а на (вообще-от естественном как раз) int32_t система сказала ква - судя по всему криво оттраслировав код в Сryptol-based IL - сломалось на проверке типов (там даже примерно понятно в чем лажа).

Остальные два - фиббоначи (рекурсией и циклом) и факториал - циклами "туда" (от 0 до n) и "обратно" (от n до 0) закончились зацикливанием импортера llvm-ного кода. Причем второй - на варианте "туда" ("обратно" как раз загрузился нормально). Первый зациклился на рекурсии.

С жабой тоже самое впрочем.

Потому и возник собственно вопрос - "а как они этим вообще пользуются"
*) Собственно SAW и есть добавка к Cryptol и активно его пользует унутре скриптов - главная идея как я понимаю писать алгоритмы на криптоле и доказывать что их С- и Java- аналоги им эквивалентны
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.
  • 1 comment