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

Проверка, переставшая сравнивать, продолжает зеленеть — за один день поймано трижды

Самый опасный класс дефектов в проекте, потому что он не виден по цвету.

Три случая за 15 августа 2026:

  1. Сверка сторожей меры была пустой — она сравнивала два преобразования, ни одно из которых не делало работу: отметку клал анализ, который в тесте не вызывали. После починки 44 программы из 114 реально помечены, и обе стороны совпадают побайтово.
  2. Оценка покрытия врала: обход считал «в срезе» 1490 примеров вместо 2318, потому что виды образцов не попали в список. Обещание «ничего не пропущено молча» держалось на неполном списке.
  3. Проверка оракула мерила не то — «умножение стало сводимым, и её опора ушла из-под неё молча» (коммит 8d219de в ветке сборки).

Плюс родственный случай: пример НОД(1, ∞) перестал проверять то, ради чего написан — граница входа стала отвергать бесконечность раньше вычисления, и с машины шёл FLANG_TYPE вместо проверки меры. Проверка зеленела, перестав проверять.

Как ловить. Требовать от проверки называть число сравнённого, а не только «прошло». «Не найдено нарушений, искали прогоном на всех N» и «нарушений не искали» — разные ответы, и они должны различаться в отчёте.

Четвёртый случай, 16 августа: список названных расхождений съел изъятие

Побайтовая сверка ядра с эталоном на flang устроена честно: список ЗАЗОР называет ПОИМЁННО программы, на которых эталон отстал, и сверяется он deepEqual-ом — разошлась лишняя, красно; сошлась названная, тоже красно. Ослабить сверку он не может.

А изъятия рядом с ним — может. Пятнадцать изъятий ломают по куску В САМОМ ЭТАЛОНЕ и требуют, чтобы сверка дала расхождение СВЕРХ названного зазора. Когда я дописал в ЗАЗОР фикстуру «тело не разбирает переменную индукции» (её текст отказа разошёлся законно — ядро научилось читать вторую форму тела), изъятие «разбор тела перестал требоваться» перестало давать новое имя: сломанный эталон расходился ровно на той фикстуре, которая теперь названа. Изъятие зазеленело, перестав проверять.

Признак класса, по которому третий случай ищется заранее: проверка, чей вердикт считается ВЫЧИТАНИЕМ из списка исключений, слепнет ровно на том, что в этот список попало. Значит дописывать в такой список можно только то, на что не опирается ни одно изъятие, — а проверять это надо прогоном, а не памятью.

Как починено. Не записью в список, а переносом: новый текст отказа перенесён в эталон (flang/self/proofterm.flang), фикстура из ЗАЗОРа убрана, изъятие снова краснеет. Зазор при этом остался названным: на тот день 14 имён, 14 измеренных расхождений из 250 программ; после переноса трёх кусков ядра — 9 имён из 257. Число меняется, приём остаётся.

Пятый случай, 18 августа: порча ушла в первое вхождение и не доехала

Сверка эталона распределённости (flang/test/self-distributed.test.mjs) ломает эталон заменой строки в его исходнике — это способ убедиться, что сверка умеет краснеть. Порча «вариант» заменяла строку то если «Это вариант» от «узел» и давала 0 расхождений, то есть выглядела ровно как исправная сверка на исправном эталоне.

Причина: String.replace меняет ПЕРВОЕ вхождение, а такая строка в файле была в двух местах — в «Метка значения» (её кодирование не зовёт) и в «Закодировать» (её зовёт). Порча ломала мёртвую для этого пути ветку.

Защита от «порча не нашла своего места» (выход кодом 2) здесь не срабатывает: место нашлось, просто не то. Значит проверки «замена применилась» мало — нужна проверка «замена задела то, что считается». После переноса порчи на «Это вариант» расхождений стало 345 из 395 значений корпуса.

Побочная польза: обнаружилось, что «Метка значения» вообще не сверялась ни с чем. Теперь сверяется — с первым элементом кадра свидетеля.

Шестой случай, 18 августа: flang check примеры не гоняет

В эталоне распределённости жила функция «Без последней части» с примером «из трёх остаются две», который не выполнялся: свёртка дописывала все части, а flang check отвечал valid: true с пустым списком диагностик.

Проверено нарочно испорченным примером на двух функциях-тождествах (список и строка): flang check — 0 диагностик, flang check --proof — тоже молчит, flang test — 2 красных из 2. То есть команда, которой проверяют файл чаще всего, примеры не считает вовсе.

Правило на будущее: эталон, к которому написаны примеры, обязан пройти flang test, а не только flang check. Отдельно от этого стоит запомнить: у эталона распределённости 28 примеров, 28 зелёных — но узнать это можно было только третьей командой.

Связано: a-removal-must-turn-a-test-red, byte-for-byte-comparison, a-measured-zero-is-valuable, bottleneck-moved-to-claim-shape, checked-without-checking

Четвёртый признак класса: проверка, написанная на значении, где ОБЕ развязки дают одно и то же

19 августа 2026, flang/stdlib/sha256.flang. Модуль объявляет: всё, что байтом не является, считается нулём — в отличие от C, где (uint8_t)300 даёт 44. Проверка на это была написана так:

assert.equal(sha.heshBaytov([256]), sha.heshBaytov([0]))
assert.notEqual(sha.heshBaytov([256]), sha.heshBaytov([44]))

Она зелёная и не держит ничего: 256 остаток от 256 — это ноль, то есть на числе 256 наша развязка и обрезка по модулю совпадают. Подделка «обрезать как в C» прошла её целиком. С числом 300 (наша развязка даёт 0, обрезка дала бы 44) подделка краснеет сразу.

Признак, по которому такое ищется заранее: если проверка отличает два поведения, подставьте в неё вход, на котором эти два поведения СОВПАДАЮТ, и спросите, не он ли там написан. Круглые числа — 0, 1, 256, степени двойки — именно те, где развязки чаще всего сходятся, и именно они первыми приходят в голову, когда пишешь пример.

Найдено не чтением, а правилом «подделка на каждое правило»: из шести подделок по модулю sha256 две сверку ПРОШЛИ. Вторая — «верхние четыре байта поля длины писать нулями»: её не держал весь корпус целиком, потому что сообщения длиннее 512 МБ в нём нет и быть не может. Обе закрыты прямыми проверками.

Пятый признак класса: программа, выпавшая из корпуса, уносит свои утверждения молча

19 августа 2026, побайтовая сверка ядра с эталоном (flang/test/self-proofterm.test.mjs). Корпус собирается обходом всех .flang дерева, и грузится каждая программа так:

try { программа = await loadProgram(путь) } catch { continue }

continue — и есть дыра. Я завёл в flang/self/proofterm.flang функцию «Приписать вызовы», не заметив, что такое имя уже занято в flang/self/totality.flang. Связывание отвергло FLANG_DUPLICATE_NAME, но отвергло оно flang/self/bootstrap/compiler.flang — единственную программу, которая импортирует ОБА модуля, — и та молча выпала из корпуса вместе со всеми своими утверждениями.

Сверка при этом ЗЕЛЕНЕЛА бы охотнее прежнего: расхождений стало меньше, потому что сравнивать стало нечего. Единственной уликой было число в отчёте:

было: программ 324, строк ведомости 425, доказано 393 стало: программ 323, строк ведомости 408, доказано 376

То есть число сравнённого поймало то, чего не поймал цвет, — ровно так, как предписано в начале этой заметки. Без строки «программ N» правку можно было бы закоммитить, сочтя её улучшением.

Признак, по которому ищется заранее: любая проверка, которая СОБИРАЕТ свой корпус обходом каталога и пропускает то, что не загрузилось, обязана печатать размер корпуса и сличать его с ожидаемым. И отдельно: новое имя функции в flang/self/*.flang надо сверять со всем каталогом, а не с одним файлом, — модули там импортируются друг в друга, и имена у них общие.

Как чинится за минуту: flang check flang/self/bootstrap/compiler.flang называет оба модуля и оба места. Эта команда стоит того, чтобы звать её после любого добавления функции в flang/self/.

Шестой признак класса: разборщик текста, не знающий одной формы записи, читает не то, что обещает

20 августа 2026, сторож жаргона (scripts/jargon-guard.mjs). Он обещает читать из исходника ТОЛЬКО строковые литералы: жаргон в комментариях законен (это разговор разработчиков), а в напечатанной справке — нет. Разбор посимвольный, знает строки и комментарии.

Чего он не знал — литерала-образца. В flang/src/parser.mjs стоит

return message.replace(/'([^']{1,40})'/gu, (целиком, фраза) => …)

и с первой кавычки внутри образца разборщик считал, что вошёл в строку. Дальше он читал КОД как текст для читателя: 54 «находки» в комментариях одного парсера и полное молчание о настоящих строках. По всем .mjs дерева «находок» было 163, после починки — 103.

Цвет при этом ничего не показывал: сторож был зелёным до починки и остался зелёным после. Разошлись бы только числа, а сравнивать их было не с чем.

Признак, по которому такое ищется заранее: если проверка ВЫДЕЛЯЕТ из файла кусок по форме записи (строку, комментарий, блок кода, заголовок), спросите, все ли формы этой записи она знает, — и проверьте на файле, где стоит самая редкая. Одна незнакомая форма переворачивает выделение целиком, а не портит его слегка: после неё «внутри» и «снаружи» меняются местами до конца файла.

Чем закрыто. Образцы разбираются наравне со строками и комментариями, а тест flang/test/jargon-guard.test.mjs проверяет это дважды: на выдуманном куске с образцом-кавычкой и на живом parser.mjs — из его разбора не имеет права вылезти ни одна строка кода.