В докладе "О чём я говорю, когда говорю о тестировании корректности работы компиляторов" я рассказывал про один из способов верификации оптимизаций в компиляторах с помощью SMT-солвера. Такой способ используется на практике для LLVM с помощью Alive2, для GCC с помощью smtgcc, в PyPy и других компиляторах. В LuaJIT есть некоторых набор оптимизаций для IR и не всегда эти оптимизации работают корректно, мы это знаем по проблемам, которые уже были выявлены пользователями LuaJIT и исправлены. Поэтому такой способ верификации хотелось реализовать и для LuaJIT, тем более что технически это возможно - в LuaJIT можно экспортировать IR и управлять как уровнями оптимизаций так и отдельными оптимизациями.

Несколько лет назад мы в Tarantool организовали лабораторию, в рамках которой студенты в течение учебного года решают задачи, которые мы им даём, мы им в этом помогаем и платим стипендию, а по итогам такой работы можем пригласить их на стажировку. Из успешно выполненных задач: фаззеры на основе грамматики для SQL и Lua (это как раз от меня задачи были), инструментирование dlmalloc для ASAN, sysprof и memprof для LuaJIT. Более подробно про саму лабораторию можно почитать на сайте.

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

Пример одного из тех двух багов, которые верификатор уже может выявить:

Тикет: https://github.com/LuaJIT/LuaJIT/issues/783
Патч: https://github.com/tarantool/luajit/commit/ab0c0793a43fc0fb0c7b71b6250339117d99254a

Оптимизация fold x - (-0) ==> x работает некорректно для x = -0 в арифметике с плавающей точкой. Результат выражения будет -0 вместо +0.

Пример ниже воспроизводит проблему с включенной оптимизацией fold:

local minus_zero = -0
local results = {}

for i = 1, 100 do
   local lhs = minus_zero
   local rhs = -1.0 * (2^1016) * 0.
   results[i] = lhs - rhs
end