У напечатанной программы две двери, а граница входа стояла только у одной

Напечатанный C зовут двумя способами, и обещания у них разные. ПРЕФИКС_call — вызов по имени из библиотеки: так программу зовёт всякий, кто встраивает flang в код на другом языке. flang_cli — прогонщик, JSON на входе и JSON на выходе. Граница входа (fl_check_entry по таблице объявленных типов) стояла только у прогонщика. Библиотечная дверь не сверяла ничего, и это било ровно по тому сценарию, ради которого печать в C существует.

Улика снята прогоном собранного C на examples/rosetta/factorial-english.flang (Factorial объявлен принимает n: nat). Чужая программа на C, слинкованная с libfactorial.a:

Последняя строка — худшая, и она про доказательство, а не про диагностику. Завершение тотальной доказано по типу: у нат есть потолок 2^53−1, ниже которого н минус 1 точно меньше н, и проверка убывания в такую функцию не печатается вовсе. Значение вне типа уносит вместе с типом и доказательство: 1e300 минус 1 равно 1e300, цепочка вечна. Тотальная функция отказала кодом, отведённым обычной.

Дыра не относится к C: в напечатанном JavaScript то же самое — модуль factorial.js, вызов factorial(-3) даёт 1, а flang_cli.js на том же входе отвечает FLANG_TYPE. Таблицу типов печатают все восемь целей, зовёт её только прогонщик каждой из них.

Отвергнутый путь: сверять прямо в ПРЕФИКС_call. Довод не «дорого», а «мимо цели»: ПРЕФИКС_call обязан отвечать значение в значение так же, как interpret у свидетеля, а interpret объявленных типов тоже не сверяет — замерено: evaluate(программа, "Factorial", {n: -3}) возвращает 1. Сверяет их flang run. Начни _call сверять — у языка стало бы два ответа на вопрос «подходит ли значение типу», и разошлись бы они молча. Поэтому дверь заведена второй функцией ПРЕФИКС_enter = fl_check_entry + ПРЕФИКС_call; та же пара, что flang run и interpret.

Сверка на границе стоит 1,1 мкс на вызов — в 30 раз дороже самого вызова. Замер на examples/measure/natural.flang, функция Сумма пары (два параметра нат, тело — одно сложение), 5 млн вызовов, три прогона, cc 15.2.0 -O2, Linux 7.0.0:

Причина названа и лежит в рантайме, а не в таблице: fl_check_entry (flang/src/emit/c/flang_runtime.c) строит текст будущего отказа для каждого параметра на каждом вызове — fl_label(ctx, "вызов функции «%s»: аргумент «%s»", …), то есть форматирование плюс выделение в арене, — и делает это до того, как выяснилось, что отказывать не в чем. Арена тут ни при чём: с fl_arena_reset на каждом витке вышло 1134—1160 нс, те же числа. Отсюда следующий шаг, если цена станет мешать: строить метку лениво, только на ветви отказа. Прогонщика это не задевало никогда — он платит её раз на запрос, где разбор JSON дороже.

Чем подтверждено. Ветка work/zelenyy-stvol, правка в flang/src/emit/c.mjs (+26 строк) и в близнеце flang/self/emit-c.flang (+3/−2 строки); проверка flang/test/emit-c-library-door.test.mjs — чужая программа на C собирается, линкуется с напечатанной библиотекой и зовёт обе двери по одной сетке. Она краснеет тремя разными способами: убрать дверь — чужая программа не собирается; оставить дверь без fl_check_entry — {"ok":true,"значение":1} вместо отказа; заставить сверять _call — расходится с interpret. Побайтовая сверка с близнецом (self-emit-c.test.mjs) осталась зелёной: 25 проверок из 25.

Цена в байтах: модуль растёт на 1862—1906 байт независимо от размера программы (замерено на пяти программах дерева), точка раскрутки bootstrap/ — на 6998 байт, из них 6346 в compiler_flang.c: текст новой двери едет туда строковыми константами самого генератора.

Чем ограничено. Закрыта библиотечная дверь только у программ, напечатанных свидетелем на Node. У программ, напечатанных двоичным flang emit, таблица объявленных типов пуста ({ NULL, 0, … }) — двоичный говорит об этом сам при печати, — и обе двери там по-прежнему молчат; проверено прогоном собранного bootstrap/flang. Пока таблицаВхода из flang/src/types.mjs не перенесена в flang/self/types.flang, _enter в такой программе сверяет пустую таблицу и возвращает FL_OK. Семь остальных целей печати дверь тоже не получили.

Связано: a-dropped-type-check-gives-a-wrong-answer, a-check-that-skips-a-check-is-a-class, three-number-types, a-removal-must-turn-a-test-red