/
Поиск
RU

Под капотом: как устроена kola

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

Конвейер компиляции

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

Следующий этап — чекер. Он проверяет типы и номинальные регионы, ряды эффектов (для приватных функций выводит их сам), линейность ресурсов и владеющих значений с учётом потока управления, дисциплину изменяемости и правило представлений, исчерпывающий match, чистоту assert, выход ссылок за пределы региона при возврате и сохранении, правила константного времени внутри ct fn и запрет на контракты, зависящие от параметра untrusted. kola check выполняет всё это и на этом останавливается.

То, что выходит из чекера, понижается в KIR — типизированное промежуточное представление, в котором имена уже разрешены, у каждого узла есть тип, а каждое обязательство безопасности уже решено. Решает их небольшой прувер на разностных ограничениях, встроенный в компилятор. Через него проходят четыре класса обязательств: границы индексов и срезов, предусловия req, арифметическое переполнение и постусловия ens. Каждое такое место либо доказано, и тогда проверка исчезает, либо остаётся проверкой времени выполнения, на которой срабатывает трап. Молча ничего не выбрасывается. kola ir печатает IR с каждым решением и его причиной, а kola report checks выдаёт те же решения списком по функциям. Подробнее об этом — на странице IR-0: единственное место, где проверку можно снять.

Все компилирующие пути — C-бэкенд, собственный бэкенд и JIT — берут решения о проверках из KIR. Интерпретатор обходит проверенное синтаксическое дерево напрямую, сохраняет все проверки и служит эталоном, с которым сравниваются остальные. Функция, которую IR пока не умеет понижать, всё равно компилируется и работает, только все её проверки остаются на время выполнения; kola check печатает замечание о том, скольких элементов это касается. kola check --require-analyzed превращает это замечание в ошибку.

Компилятор написан на Rust без зависимостей, если не считать Cranelift, который заперт в отдельном крейте. Стандартная библиотека встроена в бинарник: kola, скопированный в пустой каталог, компилирует и запускает программы на kola, и больше ничего ставить не нужно, а библиотека не может разойтись с компилятором, в котором поставляется. --std <dir> (или KOLA_STD) компилирует против другого дерева — так и работают над самой стандартной библиотекой. Без этого флага правки в std/ на диске ни на что не влияют.

Два исполнителя одной программы

Интерпретатор используют kola run и kola test. Это эталонная реализация: она определяет, как ведёт себя язык, и с ней сравнивается каждый бэкенд. Кроме того, во время выполнения он повторно проверяет кое-что из уже доказанного чекером, например линейность ресурсов.

Интерпретатор работает вместе с JIT (just-in-time-компилятором): по ходу выполнения программы он компилирует часть функций в машинный код и вызывает уже их, а не интерпретирует. Функции с пустым рядом эффектов (!{}) компилируются через Cranelift и вызываются из собственного механизма вызовов интерпретатора; всё остальное интерпретируется. Корректность этого держится именно на пустом ряде. Чистая функция устроена как «аргументы на входе, значение на выходе», поэтому там, где в скомпилированном коде сработал бы трап, он не срабатывает: он ставит флаг и возвращает значение-заглушку, а интерпретатор отбрасывает результат и повторяет вызов в интерпретируемом виде. Трап, который видит программа, — всегда собственный трап интерпретатора, с тем же сообщением, видом, местом и восстановлением через domain. Функция с циклом компилируется при первом же вызове, без цикла — после нескольких вызовов. --jit-report показывает, какие функции скомпилированы и почему остальным отказано, --no-jit оставляет чистый обход дерева, а kola test --oracle запускает обход дерева третьим исполнителем и сравнивает с ним два других. JIT окупается на длинных функциях с тяжёлой арифметикой, например в криптографии; на наборе мелких вспомогательных функций затраты на компиляцию могут так и не вернуться.

C-бэкенд генерирует код на C и заголовок среды выполнения kola.h и передаёт их компилятору C. Так программу запускают kola run --native и kola test --native, и этим же путём kola build собирает артефакты.

kola test прогоняет каждый тест на обоих исполнителях и сравнивает результаты пофайлово. Расхождение даёт код выхода 3, а не примечание под зелёной строкой. --interp запускает только интерпретатор (компилятор C не нужен, это быстрый цикл во время работы), --native — только C-бэкенд. Если нативная сторона отказывается собирать файл по правилу карты (например, окно MMIO при запуске под ОС), файл помечается как несравнимый: в силе остаётся вердикт интерпретатора, а в сводке сказано, что сравнения не было. Сбой компилятора C всегда считается ошибкой.

Такое перекрёстное сравнение — основной способ ловить ошибки компилятора. Слепое пятно у него одно: дефект, который есть на обеих сторонах, оно не видит. Случай, когда на одной стороне срабатывает трап, а на другой портится память, KIR и создавался исключать по построению, а не тестированием.

C-бэкенд

C-бэкенд покрывает почти весь язык и служит основным путём сборки для продакшена. Он достаёт до любой платформы, для которой есть компилятор или кросс-компилятор C.

  • kola build file.kl записывает build/<name>.c, заголовок build/<name>.kh с публичными функциями, константами и типами модуля, заголовок среды выполнения и объектный файл (машинный код, который ещё предстоит скомпоновать в программу). --link <path> компонует исполняемый файл со всеми флагами компилятора, которые нужны kola, так что строку cc в сборочный скрипт копировать не придётся.

  • Компилятор C задаётся через --cc=<path>, иначе берётся $KOLA_CC, иначе cc. Подходят и gcc, и clang; флаги, которые понимает только один из них, проверяются на фактически используемом компиляторе. Уровень оптимизации по умолчанию -O3, выбирается через --opt; --cpu x86-64-v3 или --cpu native поднимает базовый набор инструкций.

  • На Linux с clang исполняемый файл компонуется с собственной средой выполнения kola вместо libc (стандартной библиотеки C, от которой зависит большинство программ). Получается статический бинарник: один файл, которому на целевой машине не нужны установленные разделяемые библиотеки. --libc system подключает системную библиотеку C. kola cc --target linux-x64|linux-arm64 — драйвер компилятора C для этих платформ без libc, работающий на любой хост-системе.

  • --freestanding собирает для голого железа, то есть для кода, под которым нет операционной системы, — ядра или прошивки. Здесь нет libc, память выдаёт статический линейный аллокатор, а внешних символов нужно не больше четырёх (обработчик паники k_panic, две функции часов и функция вывода), причём каждый — только если программа его использует. Полностью доказанному чистому модулю не нужен ни один.

  • Каждый сгенерированный .c-файл начинается с комментария о происхождении: версия компилятора, версия карты, хеш встроенной стандартной библиотеки и хеш каждого исходного модуля. Одни и те же входные данные дают побайтно одинаковый результат, где бы ни шла сборка.

  • Шаг компиляции C кешируется в ~/.kola/cc-cache; ключ составляют компилятор, его аргументы и каждый байт входных данных. Перед замерами скорости компилятора выставьте KOLA_CC_CACHE=off.

У некоторых функций стандартной библиотеки есть аппаратные ветки: AES-NI и PCLMULQDQ, SHA-NI, CRC-32C и их аналоги для AArch64. Ветка — это символ на C или ассемблере, названный в сигнатуре функции в предложении hw. Определением при этом остаётся тело на kola: его выполняет интерпретатор, его доказал чекер, и с ним kola test --native сверяет ветку. Ветка выбирается только на процессоре с перечисленными возможностями и только после проверки req функции. --no-hw собирает программу с одними телами на kola. Пакеты могут объявлять собственные ветки тем же способом.

Собственный бэкенд

Собственный бэкенд собирает программы без компилятора C, ассемблера и компоновщика. Именно в эту сторону движется kola: к самостоятельному набору инструментов для x86-64 и AArch64 на Linux, macOS и Windows.

Его конвейер продолжается от KIR. KIR один раз понижается в LIR — более низкоуровневую форму, близкую к машинному коду. LIR записан в форме SSA (static single assignment: каждое значение присваивается ровно один раз, что упрощает оптимизации) над скалярными виртуальными регистрами (неограниченным запасом именованных значений, которые позже отображаются на настоящие регистры процессора). Составные значения в LIR лежат в явных слотах стека, проверки — это явные переходы к трапу, а соглашение о вызовах целевой платформы (правила, в каких регистрах и слотах стека передаются аргументы и результаты) применяется в каждом вызове. Над LIR работает оптимизатор: свёртка констант и ветвлений, встраивание, упрощение, if-conversion, вынос инвариантов из циклов. Затем выбор инструкций (подбор машинных команд для каждой операции) и распределение регистров (назначение значениям регистров процессора) нацеливаются на x86-64 или AArch64, а собственные писатели и компоновщики kola выдают исполняемые файлы в форматах Linux (ELF), macOS (Mach-O) или Windows (PE). Компоновщик — это инструмент, который собирает скомпилированные части в один запускаемый файл; у kola он свой, так что системный ld не нужен. Проверки, снятые прувером, в код вообще не попадают, и работа прувера напрямую окупается в машинном коде.

Как им пользоваться:

  • kola build --link <path> file.kl без флагов, специфичных для C, сначала пробует собственный бэкенд для хост-системы или для --target. Если собственный бэкенд отказывается от программы, сборка идёт через компилятор C и печатает замечание с причиной отказа. Если компилятора C нет, ответом становится сам отказ.

  • kola build --cross --target <triple> --link <path> использует только собственный бэкенд.

  • kola test --own прогоняет тесты через собственный бэкенд без отката на C, по одному тестовому образу за раз, на хосте x86-64 или AArch64.

Весь язык собственный бэкенд пока не покрывает. То, что он принимает, расширяется от релиза к релизу, а всё, что он не принимает, отвергается с указанием причины ещё до записи артефакта. Эталоном того, что делает поставленная программа, остаётся C-бэкенд.

Код с константным временем — причина, по которой собственный бэкенд появился задолго до того, как стал набором инструментов. Оптимизирующий компилятор C вправе превратить код без ветвлений в код, который ветвится по секрету, и флага, запрещающего это, не существует. Собственный бэкенд контролирует каждый проход, затрагивающий ct fn: при каждой компиляции он вычисляет, какие значения параметров и содержимое памяти доходят до ветвления, адреса или аппаратного деления, до оптимизации и после неё, и если у ct fn это множество выросло, она выдаётся без оптимизаций. Отдельный инструмент сборки heterobuild компилирует ct-функции файла собственным бэкендом, всё остальное — C-бэкендом и компонует их в один бинарник.

Другие архитектуры. --cross --target пишет объектные файлы ещё и для riscv64, riscv32, mips64el, mips32el, armv7m (Thumb-2), loongarch64 и wasm32 в форматах ELF, Mach-O, PE-COFF или wasm (--format). Они проходят через более старые генераторы кода, по одному на архитектуру, которые обходят KIR напрямую и ничего не оптимизируют; они нужны для платформ без компилятора C и служат ещё несколькими независимыми исполнителями для сравнения. На 32-битных платформах usize занимает 32 бита, а u64 передаётся парой регистров. Трапы в объектных файлах любого бэкенда вызывают один и тот же символ k_panic, поэтому объектные файлы разных бэкендов компонуются вместе.

Cranelift и браузер

Cranelift (crates/kola-clif) — движок, на котором работает JIT. Он умеет также выдавать детерминированные объектные файлы для x86-64 и AArch64 без компилятора C, а значит, служит ещё одним исполнителем для сравнения. Путём сборки для продакшена он не является.

Песочница — это интерпретатор, скомпилированный в WebAssembly (crates/kola-wasm). Страница web/playground в репозитории содержит редактор, примеры из практикума и кнопки для проверки, запуска и тестов. Всё выполняется в браузере со встроенной стандартной библиотекой, сервера нет.

Целевые платформы

Платформа

Как собрать

Linux, macOS, Windows под ОС

kola build, kola build --link; кросс-компиляция по пути C — забота компилятора C (--target, --cc=)

Linux без libc

по умолчанию для исполняемого файла на Linux с clang; kola cc для исходников на C

Голое железо

kola build --freestanding, компоновка со своим скриптом компоновщика и своим _start

Без компилятора C, x86-64 / AArch64

собственный бэкенд: build --link или build --cross --target <triple> --link

Без компилятора C, другие архитектуры

build --cross --target <triple>, только объектные файлы

Браузер

песочница на WebAssembly

Во что безопасность обходится во время выполнения

Проверки переполнения и границ остаются в машинном коде, если прувер их не снял, и неудачная проверка — это трап, а не неопределённое поведение. На практике проверка, которая никогда не срабатывает, стоит немного. Это хорошо предсказуемое ветвление, а на пути через C компилятор C часто сам ещё раз доказывает тот же диапазон и выбрасывает проверку. Ценность снятой проверки скорее в том, что она доказана при компиляции, чем в выигрыше скорости. По скорости она окупается там, где проверка мешала бы векторизации или где компилятор C не видит границу, а для рецензии окупается везде: kola report checks, дошедший до «0 runtime», — это утверждение о самом коде.

Важнее то, как устроены выделения памяти. Регион — это линейная арена: выделение памяти сводится к сдвигу указателя, а освобождение — к сбросу арены на закрывающей скобке, без учёта отдельных объектов. Опасность в регионе, который живёт дольше работы, ради которой он открыт. Сервер, который на каждый запрос выделяет память в регионе, живущем всё время соединения, удерживает память всех запросов и становится не только больше, но и медленнее, потому что арена растёт с каждым обслуженным байтом. Открывайте регион на запрос или на итерацию цикла: на закрывающей скобке его память возвращается. kola report leaks ищет выделения внутри циклов, регион которых переживает цикл; см. Утечки регионов.

Свои замеры репозиторий хранит в docs/perf-notes.md, и у каждого указаны машина, компилятор и условия. Если вы измеряете kola сами, несколько правил сэкономят время:

  • Называйте компилятор C при каждом числе. gcc и clang дают из одного и того же сгенерированного C заметно разный код, причём в зависимости от нагрузки выигрывает то один, то другой.

  • Сделайте так, чтобы каждый результат микробенчмарка действительно использовался дальше, иначе компилятор C удалит ту работу, которую вы собирались замерить.

  • Замеряйте на простаивающей машине. Число, снятое рядом с идущей компиляцией, — это шум.

  • Замеряйте то, что поставляете. Однострочный бенчмарк можно оптимизировать так, как полную программу не получится.

  • При замерах скорости компилятора отключайте кеш cc (KOLA_CC_CACHE=off), а для любого публикуемого числа оставляйте уровень --opt по умолчанию; именно поэтому при нестандартном уровне печатается замечание.

C и libc: никакого FFI

Вызывать функции на C из kola нельзя. Здесь нет extern "C", нет FFI, нет типа сырого указателя, нет ассемблерных вставок и нет блока unsafe. Причина в том, что на такой границе заканчивается любая гарантия kola. Эффекты, контракты и линейность компилятор может проверить в коде на kola, но не внутри чужой разделяемой библиотеки, а ассемблерное тело может испортить память там, где этого не заметит ни один эталон. Именно закрытая граница позволяет странице Безопасность описывать конечную поверхность атаки без исключений.

Что kola предлагает взамен:

  • Аппаратные ветки для случаев, когда одна инструкция лучше любого количества обычного кода; определением остаётся тело на kola, и ветка тестируется против него.

  • Процессы: чтобы воспользоваться готовой программой на C, её запускают через sys.proc.spawn по выдаче.

  • Обратное направление: C может вызывать kola. kola build выдаёт заголовок с публичными функциями модуля, так что библиотека на kola может жить внутри программы на C. См. Встраивание kola в программу на C.

Собственной среде выполнения kola libc тоже не нужна; см. платформы без libc и freestanding выше.

Режимы разработки

При разработке сервиса помогают два режима kola run. kola run --reload <handler> применяет проверенные правки при следующем вызове названного обработчика без перезапуска процесса; состояние и капабилити сохраняются, а правка, не прошедшая проверку, оставляет работать прежний код. kola run --restart заново проверяет всю программу и на Unix-системах запускает новый процесс, сбрасывая локальное состояние. Подробности и ограничения — в kola help reload. Для состояния, которое должно пережить смену кода, есть LiveState[S]: линейный владелец, который переносит данные фиксированного размера через явные чистые функции преобразования (STD-CARD, LiveState).

Редакторы и инструменты

kola lsp — языковой сервер; его запускает редактор, а не человек. Он отдаёт диагностику, символы документа и подсказки при наведении: сигнатуру функции с рядом эффектов и контрактами, тип, который чекер вывел под курсором, и пометку там, где проверки остаются на время выполнения. Сервер входит в компилятор, так что подсказка — это ответ самого чекера. Переход к определению, поиск ссылок и переименование пока не поддерживаются. Клиенты для VS Code, Neovim и JetBrains (через LSP4IJ) лежат в каталоге editors/ репозитория и ставятся из рабочей копии.

Для инструментов и агентов kola query выдаёт JSON-карты, построенные из фактов самого компилятора: outline, symbol, callers, callees, effects, refs и attack-surface. kola mcp — MCP-сервер над теми же фактами, с индексом проекта, который может ответить, какой код и какие тесты затрагивает изменение. Компилятор отдаёт и собственную документацию: kola help spec-card, kola help std-card, kola help std-index и kola help ai, так что на новой машине не нужно ничего, кроме бинарника.