IR-0: единственное место, где проверку можно снять

Язык, который убирает проверки границ, делает за вас утверждение о безопасности. Эта страница о том, где именно kola его делает. У компилятора есть одно верифицированное промежуточное представление — в проектных документах оно называется IR-0, в исходниках KIR (crates/kola/src/ir.rs), — и только в нём компилятор может решить, что проверку безопасности можно снять. Каждое такое решение принимается один раз для каждого места и записывается вместе с причиной.

Промежуточное представление (IR) — это форма, в которую компилятор переводит программу после чтения исходника и до выдачи машинного кода. У большинства компиляторов их несколько, и каждый бэкенд может по дороге принимать собственные решения. kola нарочно держит это одно решение в одном месте.

Какую задачу оно решает

Поначалу у kola было две написанные вручную реализации одной и той же семантики: интерпретатор, который выполняет программу напрямую, и генератор кода, который переводит её в C. Обе были написаны аккуратно, обе протестированы, но разница между ними оказалась поверхностью атаки. В первом раунде состязательного тестирования все пять найденных нарушений безопасности памяти проявлялись только в нативной сборке: интерпретатор корректно срабатывал трапом, а скомпилированная программа портила память. Каждое из них жило в зазоре между двумя реализациями.

Прогон одних и тех же тестов на обеих реализациях со сравнением результатов (перекрёстный тест) ловит многое, и kola на него опирается. Но у него есть слепое пятно, важное именно здесь: программа, сработавшая трапом, не доходит до сравнения значений. Если одна сторона срабатывает трапом, а другая молча пишет за конец буфера, сравнение значений ничего полезного не увидит. А «трап против порчи памяти» — именно тот класс ошибок, ради которого системный язык и существует, чтобы делать это правильно.

Поэтому исправлением стали не новые тесты. Двум разным фрагментам кода перестали давать каждому самостоятельно решать, какие проверки можно убрать, и это решение стали принимать один раз, в проверенном IR, который читает каждый компилирующий бэкенд. Расхождение в том, снята ли проверка, теперь невозможно выразить, и тестировать его больше не нужно.

Что такое KIR

KIR — это проверенное синтаксическое дерево, а не низкоуровневый граф (SSA), с которым обычно работают оптимизаторы. Деревом оно остаётся для того, чтобы его мог прочитать человек. Проверенным его делает то, что каждый факт, который бэкенду иначе пришлось бы выяснять самому, устанавливается один раз, при понижении программы в KIR, и хранится в узле:

• Типы: у каждого выражения есть разрешённый тип, так что потребителю ничего не нужно выводить.

• Имена: каждая переменная разрешена в пронумерованный слот кадра стека своей функции, а каждый вызов — в пронумерованную функцию, так что потребитель ничего не ищет по имени.

• Арифметика: срабатывает ли трап при переполнении операции или она идёт по модулю, решается для каждого узла (Add или AddW) вместе с разрядностью.

• Обязательства: у каждого индекса есть факт — либо Checked (проверка во время выполнения остаётся), либо Discharged с причиной, и причина печатается.

Решения принимает crates/kola/src/prove.rs — небольшой прувер на разностных ограничениях. Он рассуждает о фактах вида «x минус y не больше c», а этого хватает для проверок границ: i < xs.len, n + 4 <= buf.len и так далее. Это не универсальный доказатель теорем, и именно поэтому он быстрый и предсказуемый. Через него проходят четыре вида обязательств: границы индексов и срезов, предусловия req в местах вызова, арифметическое переполнение и постусловия ens.

В бэкендах нет ни своего прувера, ни своего вывода типов, ни своего разрешения имён. Бэкенд не может разойтись с остальными в том, снята ли проверка, потому что к тому моменту, когда он видит это место, решение уже стало данными.

Как это выглядит

Три функции с одним и тем же выражением индексации и разным количеством доступной информации:

pub fn sum[r](xs: &r [u64]) -> u64 !{} {
    let mut acc: u64 = 0;
    for i in 0..xs.len {
        acc = acc +% xs[i];
    }
    acc
}

pub fn at[r](src: &r [u64], n: usize) -> u64 !{}
    req n < src.len
{
    src[n]
}

pub fn any[r](s: &r [u64], k: usize) -> u64 !{} {
    s[k]
}

kola ir печатает IR с каждым решением. Именно здесь удобно проверять, какие проверки сняты и почему:

$ kola ir slices.kl
fn sum(xs: &[u64]) -> u64
  let acc[1]: u64 = 0u64
  for i[2] in 0usize..xs.len {
    acc[1] = (acc +% xs[i] [discharged: loop guard i < xs.len])
  }
  acc

fn at(src: &[u64], n: usize) -> u64
  req (n < src.len)
  src[n] [discharged: proved n < src.len from req+guards]

fn any(s: &[u64], k: usize) -> u64
  s[k] [checked]

Сгенерированный C несёт те же три решения, а комментарий-маркер доживает до него, так что в сборке можно найти поиском каждую снятую проверку:

$ kola build slices.kl && grep 'IR:discharged\|k_idx_at' build/slices.c
    ... xs__rp[/*IR:discharged*/i] ...
    return src__rp[/*IR:discharged*/n];
    return s__rp[k_idx_at(k, (s).len, K_SITE("\n  --> slices.kl:16"))];

k_idx_at — проверяемая индексация из среды выполнения: если k вне диапазона, срабатывает трап с указанием места в исходнике. kola report checks показывает ту же сводку в виде отчёта:

$ kola report checks slices.kl
fn sum
  proven   xs[i]  [loop guard i < xs.len]
fn at
  proven   src[n]  [proved n < src.len from req+guards]
fn any
  RUNTIME  s[k]

3 index site(s): 2 proven at compile time, 1 runtime

Настоящий отчёт печатает ещё заголовок с именем корневого файла и итоговый список того, что всегда проверяется во время выполнения. Никакой эвристики, запущенной трижды, здесь нет. Для каждого места есть одно решение, оно записано один раз, и его читает каждый бэкенд.

Ошибочному доказательству негде спрятаться

Эталонный потребитель KIR — вычислитель ir::eval_fn, который выполняет IR напрямую. На индексе с пометкой Checked он срабатывает трапом точно так же, как нативная сборка. Индекс с пометкой Discharged он всё равно проверяет во время выполнения, и если факт оказывается ложным, сообщает IrTrap::Ice — внутреннюю ошибку компилятора, которую не спутать ни с одним трапом пользовательской программы.

На этом свойстве держится вся конструкция. Нативный бэкенд убирает ровно те проверки, которые эталонный вычислитель проверяет при каждом выполнении. Поэтому ошибка в прувере проявляется громкой внутренней ошибкой при прогоне тестов через вычислитель, а не тихой порчей памяти в поставленном бинарнике. Модульный тест ir::tests::discharged_fact_false_is_ice строит функцию с заведомо ложным фактом Discharged и требует Ice — не значения и не пользовательского трапа.

Одно место для решения

Когда-то у C-бэкенда был собственный механизм снятия проверок, который лишь сверялся с IR. Это страховка, но двух мнений по-прежнему было два. Второе не стали согласовывать, а удалили: в генераторе кода на C нет ни прувера, ни учёта границ циклов, а правила того, когда факт перестаёт быть верным (например, если переменную переприсвоили или затенили), живут только в понижении в IR.

Тест codegen::tests::ir_fact_is_the_only_elision_authority закрепляет оба направления. Факт Discharged убирает проверку и помечается в C. Без него (если факт переключён в Checked или карта опустошена, как у функции вне IR) у каждого индекса остаётся проверка. Функция, которую KIR не может понизить, сохраняет все свои проверки, а это всегда безопасно.

Всё, что ниже, наследует это решение

Все компилирующие пути берут решения из KIR: C-бэкенд, собственный бэкенд (который понижает KIR дальше, в свой оптимизирующий слой LIR, и никогда не выдаёт снятую проверку), более старые генераторы под отдельные архитектуры и Cranelift. Новый узел IR доходит до всех них, и ни один из них не владеет доказательством.

Нагляднее всего это на примере JIT внутри интерпретатора. Чтобы скомпилировать функцию, ему нужно, чтобы она понижалась в KIR, а не чтобы она была доказана, — а KIR к тому времени уже существовал.

IR записывает и ширину указателя целевой платформы (IrModule.ptr_bits), так что 32-битные платформы, где usize занимает 32 бита, — это свойство IR, а не фикция, которую поддерживает один бэкенд.

Что не покрыто и откуда об этом известно

KIR понижает не весь язык. Важно, что каждая функция вне его попадает в список и никогда не пропадает молча. Функция либо попадает в понижаемое множество, либо оказывается в списке пропущенных с причиной, и этот единственный список питает замечание kola check, счётчики «not analyzed» в kola report leaks и бюджете [leaks], а также kola check --require-analyzed, который превращает любой пропуск в ошибку:

$ kola check --require-analyzed first.kl
error[not analyzed]: `first` does not reach the verified IR: generic over data `T` is outside
  IR-v0; a monomorphization template with no instantiating call site in this file, so no
  instance body was lowered
  = note: nothing is wrong with the fn. A generic fn is lowered per INSTANCE, and this file
    instantiates none — so it is proven at its CALLERS' call sites, not here, ...

Здесь first — обобщённая функция fn first[T: data](xs: &[T]) -> Option[T]. Обобщённый код компилируется мономорфизацией: для каждого типа, с которым функция используется, генерируется отдельная её копия. В файле, где обобщённая функция определена, но ни разу не использована, понижать нечего, поэтому её проверки доказываются там, где её вызывают. Полная диагностика дальше предлагает способы исправления.

Громкий пропуск важен потому, что функция, не попавшая ни в один из списков, занижала бы каждое из этих чисел, то есть объём того, чего анализ не увидел, и рецензент не смог бы этого заметить. Однажды так и случилось: обобщённые функции раньше уходили в третье место, которое не учитывал ни один список, и об утечке региона на каждой итерации в обобщённой функции не сообщало ничто. Правило, которое отсюда вынесено, применимо не только к этому компилятору: если разбиение на два случая должно при сбое закрываться, третий случай — это лазейка.

Сегодня покрытие широкое. Целые модули стандартной библиотеки, включая реализации SHA-256, X25519 и Ed25519, проходят kola check --require-analyzed.

Ограничения

• Продвижение — не обязательство. Все проверки касаются трапов. Цикл, который никогда не продвигается, полностью зелёный в report checks и зависает во время выполнения.

• Согласие двух исполнителей — не доказательство. Однажды изменяемый (&mut) подсрез локального массива проходил через узел, который в вычислителе KIR его копировал, и вызываемая функция писала в копию. kola run и kola run --native согласились друг с другом, и не согласился только вычислитель. Поэтому вычислитель тестируется как отдельный исполнитель, а не считается верным за компанию.

• Прувер работает на разностных ограничениях, это не SMT-решатель (универсальный автоматический доказатель теорем). Если место остаётся RUNTIME, дайте ему факт: усильте req, добавьте проверку-условие или используйте массив фиксированного размера. Значение [T; N] бесплатно даёт факт len == N, и именно это снимает проверки в арифметических циклах фиксированной ширины без каких-либо аннотаций.

Команды