Под капотом: как устроена 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 под ОС |
|
Linux без libc | по умолчанию для исполняемого файла на Linux с clang; |
Голое железо |
|
Без компилятора C, x86-64 / AArch64 | собственный бэкенд: |
Без компилятора C, другие архитектуры |
|
Браузер | песочница на 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, так что на новой машине не нужно ничего, кроме бинарника.