Верификация оптимизаций LuaJIT с помощью SMT

JIT-компиляторы - сердце современных динамических языков. LuaJIT, например, используется в Tarantool, OpenResty и игровых движках. Но оптимизации JIT могут содержать ошибки, которые проявляются редко и коварно. Как автоматически проверить, что оптимизированный код работает так же, как неоптимизированный?

Мы разработали ljopt - инструмент для верификации оптимизаций LuaJIT методом ограниченной трансляционной валидации (bounded translation validation). Подход прост: запускаем одну и ту же Lua-программу дважды - с оптимизациями и без них. Записываем внутренние IR-трассы компилятора (через штатный jit.util), транслируем их в логические формулы SMT-LIB и передаём SMT-решателю (например Z3). Если формула выполнима (SAT), то найден контрпример и значит есть ошибка в оптимизации или трансляция была выполнена некорректно. Если невыполнима (UNSAT), то оптимизация корректна в пределах модели.

Что удалось сделать?

• Поддержали 78 из 96 IR-инструкций LuaJIT: арифметика, побитовые операции, работа с таблицами, преобразования типов, вызовы математических функций.
• Модель памяти на основе трёхмерных массивов SMT, учитывающая мутабельные таблицы Lua и разделение на локальную и нелокальную память.
• Пробрасывание констант через SMT-контекст - это позволило точно верифицировать свёртку вызовов math.sin() и других трансцендентных функций.
• Реализовали развёртку циклов (loop unrolling) вместо замыканий Хорна из-за ограничений SMT-решателей на смеси теорий.

Результаты на реальных багах LuaJIT

Протестировано 33 известные регрессионные ошибки LuaJIT.

3 ошибки обнаружены методом SMT-верификации: LJ#783 (некорректная свёртка x - (-0.0)), LJ#791 (ошибка конкатенации строк), LJ#1079 (64-битные побитовые сдвиги). 1 ранее неизвестная ошибка найдена (LJ#1432). 2 ошибки обнаружены в самом SMT-решателе Z3 (Z3#9488, Z3#9234) и исправлены мейнтейнерами.

Инструмент не требует модификации компилятора - работает как внешний наблюдатель через jit.attach().

Ограничения: не поддерживаются вызовы произвольных C-функций (CALLS, CALLA), проверка границ массивов (ABC) и метаметоды. Также не ловит ошибки, приводящие к краху самого компилятора (например, переполнение стека в оптимизаторе) - для этого нужны фаззинг и санитайзеры.

Насколько нам известно, ljopt - первая работающая система SMT-валидации трансляции для промышленного трассового JIT-компилятора.

Проект может быть полезен всем, кто использует LuaJIT в продакшене (Tarantool, OpenResty) и хочет повысить доверие к оптимизациям.

Код проекта распространяется под лицензией MIT - ligurio/ljopt.