Справочник отказов

Когда компилятор отвергает программу, каждая строка ошибки начинается с кода:

$ flang check docs/examples/diagnostics/type.flang
модуль «Probe»: функций 1, из них с доказанным завершением 1; типов 0
FLANG_TYPE в файле docs/examples/diagnostics/type.flang, строка 6, столбец 3: функция «Удвоить» объявлена как число, а тело даёт строка
docs/examples/diagnostics/type.flang: не проверено — замечаний 1
$ echo $?
1

В строке — код, файл, строка и столбец и что не так. Эта страница переводит каждый код в то, что он значит и что с ним делать. Коды сгруппированы по стадии, которая их сообщает: сначала разбор, потом имена, типы, завершаемость и доказательства.

Коды возврата flang check: 0 — ошибок нет; 1 — найдены ошибки; 2 — кривой вызов (неизвестный ключ, нет файла); 3 — с --proof гарантия не доказана (с --proof --strict — всё, что не «доказано всё»); 4 — часть проверок не запускалась (--fast). Полная таблица для всех команд — в Справочнике команд.

Слова на этой странице: гарантия — строка обеспечивает (postcondition); prover — часть компилятора, которая доказывает гарантии для всех входов, в выводе он называется «ядро»; unit-тест — пример.

Три ловушки, которые стоят дня

Прочтите их, прежде чем искать свой код. В каждой ошибка видна не там, где сделана.

Гарантия, которая зовёт функцию своего модуля, ломает каждый модуль, который ввозит его списком

Сам по себе модуль проверяется чисто. Падает модуль, который его ввозит.

модуль «Core»

тотальная функция «Двойка»
  принимает н: число
  возвращает число
  н умножить на 2

тотальная функция «Учтено»
  принимает н: число
  возвращает число
  обеспечивает «не меньше двойки» результат не меньше («Двойка» от н)
  («Двойка» от н) плюс 1

модуль «Import»
использует «Core» только «Учтено»

тотальная функция «Проба»
  принимает н: число
  возвращает число
  «Учтено» от н

$ flang check docs/examples/diagnostics/core.flang
модуль «Core»: функций 2, из них с доказанным завершением 2; типов 0
docs/examples/diagnostics/core.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

$ flang check docs/examples/diagnostics/import.flang
модуль «Import»: функций 2, из них с доказанным завершением 0; типов 0; файлов вместе с импортами 2
без доказанного завершения: «Учтено» «Проба»
место указано строкой и столбцом, но без файла: вместе с импортами проверено файлов 2, а диагностика компилятора имени файла не несёт
FLANG_UNKNOWN_NAME, строка 12, столбец 4: неизвестная функция «Двойка»
FLANG_UNKNOWN_NAME, строка 11, столбец 56: неизвестная функция «Двойка»
FLANG_NOT_TOTAL, строка 12, столбец 4: тотальная функция «Учтено» вызывает неизвестную функцию «Двойка»: завершение доказать нельзя
docs/examples/diagnostics/import.flang: не проверено — замечаний 3
$ echo $?
1

Ввоз только «Учтено» приносит одно имя. И тело, и гарантия «Учтено» зовут «Двойка», которой у ввозящего модуля нет. Столбец 56 указывает внутрь гарантии. Номера строк — из ввезённого файла, а файл не назван, потому что проверялись два файла вместе.

Чинится одним из трёх способов:

flang check прошёл — не значит, что гарантии доказаны

flang check без ключей проверяет разбор, типы, завершаемость и unit-тесты. Гарантия, которую он не может ни доказать, ни опровергнуть, не делает проверку красной. Гарантия «не меньше двойки» выше не доказана: без --proof файл проходит с кодом 0, с --proof тот же файл выходит с кодом 3.

Чтобы увидеть, что доказано, попросите отчёт о доказательствах:

flang check docs/examples/diagnostics/core.flang --proof

  постусловие «не меньше двойки» функции «Учтено» — объявлено, не доказано: ни теоремы, ни примеров. Его считает рантайм после каждого возврата — на тех входах, которые придут
…
docs/examples/diagnostics/core.flang: НЕ ПРОВЕРЕНО — утверждений 1: доказано 0, условно 0, сетка 0, объявлено, не доказано 1, отвергнуто 0, нарушено 0; законов на сетке 0, на веру 0 — код возврата 3

Как читать итог каждой гарантии: «доказано» — доказано для всех входов; «сетка N» — проверено только на ваших N примерах, это не доказательство; «объявлено, не доказано» — объявлена, и нет ни доказательства, ни примеров. В CI берите flang check --proof --strict: он выходит с 0, только когда доказано всё.

Вторая ловушка в том же выводе: пока стоит ошибка FLANG_UNKNOWN_NAME, функция теряет и доказанное завершение, и её гарантии не доказывает никто. Сначала чините неизвестные имена.

FLANG_BOUND_ON_NAN: в типе число живёт NaN, а NaN не упорядочен

Самая частая неожиданность. Гарантия выглядит очевидно верной, а prover отвечает контрпримером.

модуль «Probe»

тотальная функция «Прибавить один»
  принимает н: число
  возвращает число
  обеспечивает «результат больше довода» результат больше н
  н плюс 1

$ flang check docs/examples/diagnostics/nan.flang
модуль «Probe»: функций 1, из них с доказанным завершением 1; типов 0
FLANG_BOUND_ON_NAN в файле docs/examples/diagnostics/nan.flang, строка 6, столбец 3: постусловие «результат больше довода» функции «Прибавить один» ЛОЖНО, и контрпример назван: «н» объявлен типом «число», а «не число» живёт в этом типе и стоит ВНЕ ПОРЯДКА — оно не больше и не меньше ничего, включая самоё себя. Тело собрано только из арифметики над «н», а всякая арифметическая операция «не число» переносит, значит результат есть «не число», и сравнение с ним ложно. Позовите «Прибавить один» от (0 делить на 0) — рантайм ответит FLANG_PROPERTY. Чинится тремя способами: объявить вход отрезком («неотрицательное», «целое») — тогда «не число» не втащить вовсе; поставить предусловие — за него платит вызывающий; либо оговорить границу, и ядро оговорку читает: обеспечьте «не ((н минус н) равен 0) или (…)»
docs/examples/diagnostics/nan.flang: не проверено — замечаний 1
$ echo $?
1

Причина: тип число — число с плавающей точкой, и в нём есть NaN («не число»). Любая арифметика над NaN даёт NaN, а любое сравнение с NaN ложно. Значит, «результат больше довода» для NaN неверно.

(н минус н) равен 0 ложно ровно тогда, когда н — NaN.

Разбор

модуль «Probe»

тотальная функция «Удвоить»
  принимает н: число
  возвращает число
  если н больше 0 то н умножить на 2

$ flang check docs/examples/diagnostics/parse.flang
FLANG_PARSE в файле docs/examples/diagnostics/parse.flang, строка 7, столбец 1: у 'если' нет ветки 'иначе'
docs/examples/diagnostics/parse.flang: не проверено — замечаний 1
$ echo $?
1

$ flang check docs/examples/diagnostics/lex.flang
FLANG_LEX в файле docs/examples/diagnostics/lex.flang, строка 5, столбец 3: не закрыта кавычка
docs/examples/diagnostics/lex.flang: не проверено — замечаний 1
$ echo $?
1

если … то … — выражение, поэтому иначе у него обязательно.

Имена и ввоз

модуль «Probe»

тотальная функция «Удвоить»
  принимает н: число
  возвращает число
  «Утроить» от н

$ flang check docs/examples/diagnostics/unknown.flang
модуль «Probe»: функций 1, из них с доказанным завершением 0; типов 0
без доказанного завершения: «Удвоить»
FLANG_UNKNOWN_NAME в файле docs/examples/diagnostics/unknown.flang, строка 6, столбец 3: неизвестная функция «Утроить»
FLANG_NOT_TOTAL в файле docs/examples/diagnostics/unknown.flang, строка 6, столбец 3: тотальная функция «Удвоить» вызывает неизвестную функцию «Утроить»: завершение доказать нельзя
docs/examples/diagnostics/unknown.flang: не проверено — замечаний 2
$ echo $?
1

Неизвестное имя всегда тянет вторую ошибку, про завершаемость: компилятор не может доказать, что вызов неизвестной функции завершится. Исправьте первую — и вторая уйдёт.

Если операция записана не в том порядке, компилятор подскажет, как писать:

$ flang check docs/examples/diagnostics/operator-order.flang
FLANG_UNKNOWN_NAME в файле docs/examples/diagnostics/operator-order.flang, строка 10, столбец 3: имя «умножить» не связано: имя вводят 'принимает', 'пусть' или образец 'случай'; а действия языка ('плюс', 'минус', 'умножить на', 'делить на', 'остаток от') пишутся МЕЖДУ значениями — «3.14 умножить на р», а не «умножить 3.14 на р»
docs/examples/diagnostics/operator-order.flang: не проверено — замечаний 1
$ echo $?
1

Типы

$ flang check docs/examples/diagnostics/type.flang
модуль «Probe»: функций 1, из них с доказанным завершением 1; типов 0
FLANG_TYPE в файле docs/examples/diagnostics/type.flang, строка 6, столбец 3: функция «Удвоить» объявлена как число, а тело даёт строка
docs/examples/diagnostics/type.flang: не проверено — замечаний 1
$ echo $?
1

$ flang check docs/examples/diagnostics/duplicate.flang
модуль «Probe»: функций 2, из них с доказанным завершением 2; типов 0
FLANG_TYPE в файле docs/examples/diagnostics/duplicate.flang, строка 8, столбец 1: функция «Удвоить» объявлена дважды
docs/examples/diagnostics/duplicate.flang: не проверено — замечаний 1
$ echo $?
1

$ flang check docs/examples/diagnostics/match.flang
модуль «Probe»: функций 1, из них с доказанным завершением 1; типов 0
FLANG_MATCH_NOT_EXHAUSTIVE в файле docs/examples/diagnostics/match.flang, строка 6, столбец 3: разбор списка не покрывает «пусто»
docs/examples/diagnostics/match.flang: не проверено — замечаний 1
$ echo $?
1

$ flang check docs/examples/diagnostics/example.flang
модуль «Probe»: функций 1, из них с доказанным завершением 1; типов 0
FLANG_EXAMPLE: пример «Двойка» функции «Удвоить»: значение не совпало с ожидаемым: ожидалось 5, получено 4
docs/examples/diagnostics/example.flang: не проверено — замечаний 1
$ echo $?
1

Завершаемость и пределы

модуль «Probe»

тотальная функция «Считать»
  принимает н: число
  возвращает число
  если н равно 0 то 0 иначе («Считать» от (н плюс 1))

$ flang check docs/examples/diagnostics/total.flang
модуль «Probe»: функций 1, из них с доказанным завершением 0; типов 0
без доказанного завершения: «Считать»
FLANG_NOT_TOTAL в файле docs/examples/diagnostics/total.flang, строка 6, столбец 30: тотальная функция «Считать»: рекурсивный вызов «Считать» не убывает — аргумент 1 («н» add 1) увеличивает параметр «н». Передавайте часть аргумента: хвост списка из образца «голова и хвост», поле варианта из образца, поле записи или элемент коллекции
docs/examples/diagnostics/total.flang: не проверено — замечаний 1
$ echo $?
1

н плюс 1 растёт, поэтому компилятор не может показать, что рекурсия кончится.

Чтобы увидеть предел шагов, запустите с маленьким --max-steps. flang run вычисляет только доказанные программы; в этом rec.flang есть недоказанное, поэтому добавлен --trust:

$ flang run docs/examples/diagnostics/recursion.flang --function "Вниз" --args '{"н":100}' --max-steps 5 --trust
на веру: доказанность не считалась — запуск по ключу --trust
FLANG_RECURSION_LIMIT: функция «Вниз» исчерпала лимит шагов (5) на глубине вызовов 1
$ echo $?
1

Гарантии и доказательства

Предусловия (требует), гарантии (обеспечивает) и теоремы.

модуль «Probe»

тотальная функция «Удвоить»
  принимает н: число
  возвращает число
  обеспечивает «удвоенное неотрицательно» если н не меньше 0 то (результат не меньше 0) иначе да
  н умножить на 2

теорема «удвоенное неотрицательно»
  дано н: число
  утверждаем если н не меньше 0 то (результат не меньше 0) иначе да
  следовательно доказано

$ flang check docs/examples/diagnostics/no-steps.flang
модуль «Probe»: функций 1, из них с доказанным завершением 1; типов 0
FLANG_PROOF_STEP: теорема «удвоенное неотрицательно»: ни одного шага
docs/examples/diagnostics/no-steps.flang: не проверено — замечаний 1
$ echo $?
1

$ flang check docs/examples/diagnostics/no-goal.flang
модуль «Probe»: функций 1, из них с доказанным завершением 1; типов 0
FLANG_PROOF_NO_GOAL в файле docs/examples/diagnostics/no-goal.flang, строка 8, столбец 1: теорема «удвоенное неотрицательно» ничего не закрывает: постусловия «удвоенное неотрицательно» нет ни у одной функции модуля. Теорема доказывает названное утверждение, а не утверждение вообще — назовите её так же, как постусловие, которое она закрывает
docs/examples/diagnostics/no-goal.flang: не проверено — замечаний 1
$ echo $?
1

$ flang check docs/examples/diagnostics/ambiguous.flang
модуль «Probe»: функций 2, из них с доказанным завершением 2; типов 0
FLANG_PROOF_AMBIGUOUS в файле docs/examples/diagnostics/ambiguous.flang, строка 15, столбец 1: теорема «неотрицательно» закрывала бы сразу 2 постусловия («Удвоить», «Утроить»), и выбрать нельзя. Дайте постусловиям разные имена
docs/examples/diagnostics/ambiguous.flang: не проверено — замечаний 1
$ echo $?
1

$ flang check docs/examples/diagnostics/mismatch.flang
модуль «Probe»: функций 1, из них с доказанным завершением 1; типов 0
FLANG_PROOF_CLAIM_MISMATCH в файле docs/examples/diagnostics/mismatch.flang, строка 11, столбец 3: теорема «неотрицательно» утверждает не то, что обещает функция «Удвоить»: утверждение теоремы и постусловие обязаны совпадать слово в слово. Ядро не решает, что два разных утверждения означают одно и то же
docs/examples/diagnostics/mismatch.flang: не проверено — замечаний 1
$ echo $?
1

Гарантия, которую prover не доказал, проверяется во время работы. flang run недоказанные программы не запускает, поэтому нужен --trust:

$ flang run docs/examples/diagnostics/property.flang --function "Половина" --args '{"н":0}' --trust
на веру: доказанность не считалась — запуск по ключу --trust
FLANG_PROPERTY: нарушено свойство «результат меньше довода» функции «Половина»
$ echo $?
1

Законы объявленных структур

Эти законы ПРОВЕРЯЮТСЯ на конечном наборе значений, который даёте вы, а не доказываются. Ошибка значит, что нарушение найдено, — контрпример есть всегда.

Планы и ввод-вывод

Ошибки flang io. План возвращает команду как данные, а выполняет её рантайм; коды FLANG_IO_* — отказы рантайма, которые план получает в ответ.

Права отнимаются по одному; по умолчанию можно всё:

flang io план.flang --plan 'Разбор' --no-net --in-dir

Процессы

Командная строка и внутренние ошибки

$ flang check --неткого
flang check: непонятный ключ «--неткого»
$ echo $?
2

Код возврата — 2.

Все коды компилятора

Таблица собрана из исходников компилятора: код в ней есть, пока его поднимает хоть одна строка исходников компилятора flang/self/ или его рантайма bootstrap/flang_*.c вне примеров и постусловий. Текст — шаблоны из каталога сообщений flang/messages/catalog.tsv; прочерк значит, что у кода шаблона в каталоге нет и текст собирается на месте. Код, названный на этой странице, но не найденный в исходниках, роняет docs:check.

Дальше: Prover отказал: чья это ошибка — как читать отвергнутое доказательство и когда ошибка не ваша.