После анонса задачи про верификацию оптимизаций в LuaJIT в лаборатории Tarantool мне написал студент Физтеха Алексей и сказал, что хочет взять эту задачу в качестве дипломной работы и с сентября прошлого года мы продолжаем делать верификатор для LuaJIT. Много успели сделать и есть результаты, которыми можно поделиться.

Напомню основную идею - научиться моделировать семантику LuaJIT IR с помощью SMT-LIB, декларативного LISP-подобного языка для SMT-солверов, и тем самым получить возможность проверять эквивалентность программы, представленной в виде LuaJIT до и после оптимизаций. В отличие от сравнительного тестирования верификация с помощью SMT-решателя позволяет проверить корректность на всех допустимых входах, а не только на конкретных тестовых данных.

До Алексея над задачей работали двое студентов, с которыми у нас появились первые результаты - они реализовали трансляцию для части IR инструкций и мы научились воспроизводить с помощью верификатора для реальных бага в LuaJIT. Сразу после начала стажировки Алексей быстро включился в работу, ознакомился с существующим кодом проекта и первым делом исправил проблемы, найденные во время ревью. Потом мы добавили поддержку арифметических инструкций (это было проще всего, потому что в SMT-LIB есть теории с поддержкой операций над целыми числами и числами с плавающей точкой), поддержали работу с памятью и поддержали проверку эквивалентности выходов с трасс и снапшотов. Пока мы не реализовали даже половину IR инструкций, но к сожалению всё смоделировать скорее всего и не получится: для одних инструкций недостаточно информации в IR, другие сложно или невозможно реализовать в SMT-LIB. Но похоже, что часть поведения программы, представленной в IR, мы научились моделировать и теперь хочется доказать работоспособность инструмента. Мы взяли корпус от нашего фаззера по грамматике Lua и Алексей для каждой программы запустил верификатор. Во время такого прогона нашли недочеты в трансляторе и один баг в LuaJIT (баг исправлен). Следующим шагом мы планируем научиться воспроизводить все известные исправленные баги в LuaJIT, связанные с оптимизациями, для этого репродьюсеры для этих багов конвертировали в тесты для ljopt, теперь Алексей будет кропотливо для каждого репродьюсера изучать IR трасс и учиться воспроизводить эти проблемы с помощью SMT-солвера. Надо сказать, что разрабатывая инструмент такого рода нужно пытаться не только заниматься моделированием IR, но и проверять работоспособность инструмента, вот мы и пытаемся всё время усидеть на двух стульях, переключаясь то на моделирование IR, то проверку инструмента.