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

flang test на слое, у которого нет своих примеров, зеленеет всегда — а таких слоёв 11 683 строки

Команда flang test <файл> печатает число прогнанных примеров, и число это включает примеры ввезённых модулей, а не только свои. Слой, у которого своих примеров ноль, показывает поэтому зелёный ответ с ненулевым счётом — и выглядит проверенным, не будучи проверенным ничем.

Это тот же класс, что и «проверка, переставшая сравнивать, продолжает зеленеть», но опаснее: здесь зеленеет не одна проверка, а вся команда, которой в проекте собираются заменить проверки на JavaScript.

Чем подтверждено. Ветка vypusk/zamestit-proverki, дерево на коммите 4780c595, двоичный собран из bootstrap/.

Замер своих примеров (grep -c 'пример «') по 77 файлам .flang в flang/self, flang/proof, flang/core, flang/stdlib: девять файлов, ноль своих примеров, и общий их объём — одиннадцать тысяч шестьсот восемьдесят три строки. Из них пять — весь слой доказательств:

строк своих примеров что показывает ведомость 3970 0 flang/self/proof-kernel.flang 5 5 0 2702 0 flang/self/proofterm.flang 23 23 0 1948 0 flang/self/proof-initial.flang 5 5 0 1420 0 flang/self/factcheck.flang 18 18 0 536 0 flang/self/obligations.flang 5 5 0 176 0 flang/self/carriers.flang 91 91 0

Все числа справа — примеры ввезённых модулей. Своих там нет ни одного.

Снял правку и посмотрел, что покраснеет. В flang/self/obligations.flang (536 строк, своих примеров ноль) разделитель в функции «Через запятую» заменён с ", " на " ; " — то есть текст всякого перечисления в диагностиках обязательств испорчен:

./bootstrap/flang test flang/self/obligations.flang → примеров 40, прошло 40, не прошло 0 ЗЕЛЕНО node --test flang/test/self-obligations.test.mjs → not ok 1 — второе мнение на JavaScript сходится с рабочим слоем на flang ПОБАЙТОВО на всём корпусе; pass 13, fail 1 КРАСНО

То есть испорченный слой держит сегодня только проверка на JavaScript, и ровно её выбрасывают вместе со второй реализацией.

Чем ограничено. Замер про свои примеры, а не про покрытие: файл со своими примерами тоже может проверять ими мало. И обратное: слой без своих примеров может быть покрыт сверкой в self-*.test.mjs побайтово — как раз это и есть сегодняшнее положение. Утверждение узкое: после выброса JavaScript у этих 11 683 строк не остаётся ни одной проверки, а команда flang test продолжит печатать про них зелёные числа.

Что из этого следует для работы: слой, переносимый на flang, не считается перенесённым, пока в нём нет своих примеров. Число «примеров прогнано N» у flang test для этого не годится — годится только «своих примеров N», и его надо считать отдельно.

Связано: checks-that-stopped-comparing, a-removal-must-turn-a-test-red, a-measured-zero-is-valuable, two-language-rules-live-only-in-the-javascript-implementation