flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub

«Число» на входной границе напечатанной программы уже, чем «число» внутри языка: NaN и бесконечности внутрь не проходят

Тип число в языке — это IEEE-754, и NaN достижим изнутри без единой диагностики (nan-is-reachable). А входная граница напечатанной программы требует Number.isFinite (flang/src/types.mjs, проверка типа число) и отвечает FLANG_TYPE: аргумент не соответствует типу число. То есть значение, законное внутри, снаружи в ту же функцию не подать.

Замерено на всех восьми целях печати сразу и одинаково. Прогонщику flang_cli каждой цели подавались NaN, +∞, −∞ и минус ноль в аргументе типа число: три первых отвергнуты во всех восьми целях, минус ноль прошёл во всех восьми. Наружу все четыре выходят исправно — {"n":"NaN"}, {"n":"Infinity"}, {"n":"-Infinity"}, {"n":"-0"}.

Чем это било. Сверка провода распределённости на восьми целях (flang/test/self-distributed-celi.test.mjs) сначала краснела ровно на этих трёх значениях и ровно во всех восьми целях — то есть выглядела как расхождение печати, а была границей типов. Отличить одно от другого удалось только потому, что расхождение оказалось одинаковым у всех восьми: одинаковая ошибка у восьми независимых генераторов кода — это не генераторы.

Дверь при этом одна, а не две. Библиотечная дверь ПРЕФИКС_call границы не сверяет вовсе (printed-program-has-two-doors), поэтому через неё те же значения проходят. Значит у одной и той же напечатанной функции два разных множества допустимых входов, и зависит оно от того, каким способом её позвали.

Чем ограничено. Это заметка о наблюдении, а не о решении: правильно ли границе отвергать NaN, здесь не решается. Довод в пользу нынешнего поведения есть и он сильный — значение вне типа уносит с собой доказательство завершения, — но NaN типу число принадлежит, в отличие от −3 для нат. Место решения — flang/self/types.flang и работа «граница типов».

Связано: nan-is-reachable, printed-program-has-two-doors, minus-zero-is-a-class, distribution-splits-into-world-and-wire