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

Новая форма языка, не доехавшая до генераторов кода, расходится с типами молча — и вылезает у того, кто собирает двоичное

Правило «доступ к полю у суммы из одного варианта» было заведено в проверке типов и в вычислителе. flang check программу принимал, flang run считал правильно — и напечатанный JavaScript падал:

поле «ключ» нельзя взять у варианта «Связь» — нужен разбор

То есть язык говорил «программа верна», а собранная программа отказывала. Хуже всего здесь не сам отказ, а кто его увидит: не тот, кто писал код, а тот, кто собирал двоичное, — возможно, через неделю и на чужой машине.

Почему так вышло. Взятие поля печатается вызовом рантайма ($field в JavaScript, field_get в Python, Elixir и Rust, FieldGet в Go и C#, fieldGet в Java, fl_field_get в C). Рантаймов восемь, и каждый нёс свою копию отказа «нужен разбор». Правка проверки типов их не касается ни строкой.

Сколько это стоило. По 3–8 строк на рантайм. Нужная семантика в каждом уже была отдельной функцией (variant_field, fl_variant_field, VariantField) — её зовёт разбор образцов. То есть новых понятий ноль, и работа свелась к тому, чтобы два ответа на один вопрос перестали расходиться.

Плюс перепечатка точки раскрутки: bootstrap/*.c порождаются из тех же исходников, и ./ярлык раскрутка:проверка краснеет, пока их не перепечатали (node scripts/bootstrap-c.mjs, около трёх минут, 15,4 МБ в семи файлах).

Правило на будущее. Заводя форму языка, пройдите список целиком и отметьте каждый пункт прогоном, а не чтением:

  1. разбор языка — и его двойник на flang (flang/self/parser.flang), иначе побайтовая сверка разойдётся;
  2. проверка типов — и её двойник;
  3. вычислитель — и его двойник;
  4. ядро доказательств, если форма встречается в утверждениях;
  5. восемь генераторов кода, если форма доезжает до печати;
  6. точка раскрутки, если задет любой из исходников, которые в неё входят.

Пункт 5 забывается легче прочих, потому что flang check зелёный, тесты зелёные, и ничто не спрашивает. Проверяется он одним прогоном: напечатать программу с новой формой и запустить напечатанное.

Чем подтверждено. Ветка vypusk/vyrazimost, коммит 1fe31263. До правки напечатанный JavaScript отказывал приведённым выше текстом; после — отдаёт "имя", как вычислитель. Утверждение «напечатанный JavaScript считает то же самое» стоит в flang/test/vyrazimost.test.mjs и печатает программу настоящим генератором, а не читает её текст.

Чем ограничено. Прогоном проверен ближайший генератор — JavaScript — и вручную Python. Остальные шесть держатся своими проверками печати (flang/test/emit-*.test.mjs) и одинаковостью правки, а не отдельным прогоном именно этой формы.

Связано: occupy-a-form-the-parser-already-rejects, a-layer-inside-the-bootstrap-point-is-frozen-until-it-is-reprinted