Англійський оригінал змінився після перекладу, тож частина тексту може бути застарілою. Читати англійською

Перекладено з англійського оригіналу · 1e3a39c8-dirty · 2026-10-26

Спеціалізація типів

Режим швидкості (-O2) використовує виведені факти, щоб усувати перевірки під час виконання (доведення, proofs), і може клонувати функцію у варіанти за представленням, захищені перевірками тегів під час виконання. -O0 і --no-type-specialization створюють лише узагальнений код: кожна перевірка лишається, кожен доступ до складеного значення йде через відповідну службу runtime.

Доведення

Доведення походить лише з фактів, які істинні щоразу, коли виконується код:

факти аргументів локальної функції, об'єднані з усіх місць її виклику (Inference::inputs; експортовані функції та функції, названі через fun F/A, їх не мають);
записаний факт виразу (факт операнда записується до того, як операція, що його використовує, звужує його);
перевірка форми раніше в тому самому плані зіставлення: вузли плану виконуються послідовно, тож пройдена перевірка кортежу чи cons-комірки домінує над кожним наступним вузлом.

Специфікації ніколи нічого не доводять. term() і none() (код, який виведення визнало недосяжним) нічого не доводять; тіла анонімних fun не отримують доведень.

Операція	Чим доведено	Згенерований код
`+ - *`	обидва операнди в діапазонах малих цілих, діапазон результату в межах безпосереднього навантаження	декодування, обчислення й кодування вбудовано; без перевірки тегу, переповнення чи запасного шляху
`+ - *`	один або обидва операнди в діапазонах малих цілих	доведені перевірки тегів зникають; перевірка переповнення й запасний шлях через службу лишаються
зразок кортежу	факт аргументу чи значення, що зіставляється: точні кортежі арності зразка	перевірку форми усунуто (недоведене: перевіряється вбудовано)
елемент кортежу	перевірка форми чи факт, що доводить кортеж	вбудоване завантаження елемента
зразок списку	факт: напевно cons-комірка	перевірку форми усунуто (інакше перевірка первинного тегу на кожному рівні)
голова, хвіст	перевірка cons чи факт, що доводить комірку	вбудовані завантаження
точний літерал `[]`, `{}`, мале ціле, атом	завжди (на кожному рівні)	порівняння слів: рівні безпосередні значення — одне слово
генератор списку	факт вхідних даних генератора: правильний список	перевірка cons і читання комірки вбудовано на кожній ітерації

Факти доходять до зразків голів функцій (аргументи, об'єднані з місць виклику), зіставлень у тілі (права частина) і клауз case/try (значення, що зіставляється, або значення тіла try); факти елементів, голови й хвоста слідують за вилученнями. Вбудоване читання зберігається в кореневий слот, як вивід служби, тож пониження фреймів зберігає його як терм крізь точки безпеки (правило перезавантаження). Єдині перетворення на вказівники в згенерованому коді — це ці доведені читання й завантаження заголовків у вбудованих перевірках форми кортежу (proven.cell). Константи розміщення беруться з abi/term.hpp; runtime звіряє їх зі своїми приватними розміщеннями комірок.

Варіанти

Профілі беруться з фактів про місця виклику: аргумент, чий факт містить лише малі цілі (синглтони чи діапазони), доводить, що аргумент є малим цілим. Специфікації (specs), широкий integer(), об'єднання з іншими видами та невідомі типи залишаються узагальненими.
Варіант виправданий лише тоді, коли він усуває реалізовану перевірку: точне порівняння молодшого тегу слова аргументу будь-де в тілі (масив аргументів ніколи не записується, а збирання сміття ніколи не змінює мале ціле).
Обмеження: 3 варіанти на функцію, 32 на модуль, 128 на ціль. Оцінене, а потім фактичне зростання (клон + guards + диспетчеризація + запасний шлях) має залишатися в межах 2x від кількості інструкцій узагальненого коду на функцію та модуль.
Узагальнені тіла завжди зберігаються. Чернетки, що перевищують бюджет, мовчки відкидаються; програма ніколи не завершується збоєм через спеціалізацію.
Вибір детермінований (порядок модуля, символу, профілю).

Клонування/спрощення LLVM замінює доведені перевірки всередині клону. Обмежений диспетчер перевіряє кожен обмежений тег і передає контекст та аргументи варіанту або узагальненому тілу; публічний символ і ABI не змінюються. Жодних припущень зі специфікацій чи прапорців fast-math не вводиться.

Поточний ефект

Доведення діють на реальний вихідний код: локальні функції, яким місця виклику передають малі цілі, кортежі й списки, втрачають перевірки тегів, форми та виклики служб (proofs, перевіряється CTest codegen_proofs і запускається як еталон виконуваного файлу executables_proofs). Варіант має заощадити більше інструкцій, ніж коштує його диспетчеризація; одна усунена перевірка тегу аргументу рідко цього досягає, тож варіанти для вихідного коду зазвичай плануються, а потім відхиляються обмеженням зростання. Цільові фікстури LLVM вставляють повторювані перевірки тегів, щоб перевірити влучання, запасні шляхи та відкат зростання з нативним виконанням.

Еталони виконуваних файлів у повному режимі запускаються за кожної політики; швидкий режим запускає -O0 (узагальнений код) і -O2 зі спеціалізацією (доведення).

codegen_measurements записує measurements/<config>/measurements.json у каталог збірки тестів codegen (час компіляції, байти IR/об'єктного коду, варіанти, доведені читання, нативний час). Часи є описовими, ніколи не пороговими значеннями.