Исполняемые спецификации на flang Читаем ошибки компилятора
English
 0%

Читаем ошибки компилятора

13 мин 2589 слов
#flang#диагностика#ошибки#отладка#compiler

Читаем ошибки компилятора

Сообщение компилятора — не препятствие, а результат проверки, которую вы сами заказали. Компилятор не угадывает намерение: он называет код, место и расхождение. Дальше нужен только перевод с языка диагностики на язык модели.

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

Как устроена диагностика

Замечание — одна строка:

FLANG_TYPE в файле name1.flang, строка 9, столбец 15: запись «Покупка» не имеет поля «стоимость»

Сначала код (FLANG_TYPE), потом место, потом текст. Код стабилен и годится для программ: по нему пишут обработчики в редакторе и в CI. Текст предназначен человеку. Место есть почти у всего; у несошедшегося примера его нет — он относится к вызову функции, а не к строке файла.

flang check собирает все замечания за один прогон и кончает итоговой строкой:

type2.flang: не проверено — замечаний 2

Одна причина часто даёт цепочку из двух-трёх замечаний. Чините первое и проверяйте снова.

Код возврата — главное, что читает CI:

Код Команда Что значит
0 flang check разбор, типы, завершение и примеры в порядке; о доказательствах обещаний не сказано ничего
0 flang check --proof всё, что обещано, доказано для любых входов
3 flang check --proof часть обещаний держится только на примерах («сетка N») или не проверена ничем
1 любая замечание: ошибка в программе или несошедшийся пример
4 flang check --fast часть проверок нарочно не запускалась
3 flang run программа не доказана, а согласия --trust не было
1 flang facts утверждение опровергнуто или вызов в нём отклонён
2 flang facts, flang run кривой вызов: не тот ключ, не JSON

Ошибки разбора

Пока текст не разобран, никаких проверок смысла не будет.

FLANG_PARSE — у если нет ветки то. Отступ во flang несёт смысл, как в Python, и ветви то и иначе обязаны называться.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  если сумма не меньше 10000
    500
    иначе 0
FLANG_PARSE в файле parse1.flang, строка 7, столбец 5: у 'если' нет ветки 'то'

Починка: то 500.

То же сообщение приходит, когда в условии стоит слово, которого в языке нет. Сравнения во flang закрытым списком: равен, не равен, больше, меньше, не больше, не меньше.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  если сумма превышает 10000
    то 500
    иначе 0
FLANG_PARSE в файле parse2.flang, строка 6, столбец 14: у 'если' нет ветки 'то'

Сообщение здесь сбивает с толку: ветка то на месте, а разбор споткнулся о превышает — столбец 14 указывает ровно на это слово. Читайте столбец, а не только текст. Починка: если сумма больше 10000.

FLANG_UNKNOWN_NAME — неизвестный тип.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: рубли
  возвращает число
  0
FLANG_UNKNOWN_NAME в файле name3.flang, строка 3, столбец 1: неизвестный тип «рубли»

Починка: встроенный тип (число, неотрицательное, строка, признак, сотых для денег в копейках) или свой — тип «Рубли» с вариантами либо объект «Рубли» с полями.

Ошибки модели

Текст разобран, но программа противоречива: имя не найдено, тип не тот, разбор неполон, завершение не доказано.

FLANG_TYPE: нет такого поля — самая частая ошибка после переименования поля.

модуль «Продажи»

объект «Покупка»
  «сумма»: неотрицательное

тотальная функция «Скидка»
  принимает покупка: «Покупка»
  возвращает число
  если покупка.«стоимость» не меньше 10000
    то 500
    иначе 0
FLANG_TYPE в файле name1.flang, строка 9, столбец 15: запись «Покупка» не имеет поля «стоимость»

Починка: назвать поле так, как оно объявлено в объекте, — покупка.«сумма».

FLANG_UNKNOWN_NAME и FLANG_NOT_TOTAL: неизвестная функция. Одна причина — два замечания: функции нет, и поэтому завершение той, что её зовёт, доказать нельзя.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  «Надбавка» от сумма
без доказанного завершения: «Скидка»
FLANG_UNKNOWN_NAME в файле name4.flang, строка 6, столбец 3: неизвестная функция «Надбавка»
FLANG_NOT_TOTAL в файле name4.flang, строка 6, столбец 3: тотальная функция «Скидка» вызывает неизвестную функцию «Надбавка»: завершение доказать нельзя

Починка: объявить «Надбавку» или поправить имя. Второе замечание уйдёт само.

FLANG_TYPE: тело даёт не тот тип. Деление даёт число, даже если делимое неотрицательное.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает неотрицательное
  сумма делить на 10
FLANG_TYPE в файле type1.flang, строка 6, столбец 9: функция «Скидка» объявлена как неотрицательное, а тело даёт число

Починка: возвращает число. Тип неотрицательное — это целые от 0 до 2⁵³−1, и результат деления в него не попадает.

FLANG_TYPE: сравнение порядка над строкой. больше и меньше определены только для чисел.

модуль «Продажи»

тотальная функция «Скидка»
  принимает клиент: строка
  возвращает число
  если клиент больше 10
    то 500
    иначе 0
FLANG_TYPE в файле type2.flang, строка 6, столбец 8: левый операнд сравнения «gt» имеет тип строка: сравнения порядка допустимы только для чисел
FLANG_TYPE в файле type2.flang, строка 6, столбец 15: сравнение «gt» между строка и неотрицательное

Починка: сравнивать числовое поле или строку со строкой через равен.

FLANG_TYPE: поле объявлено дважды.

модуль «Продажи»

объект «Покупка»
  «сумма»: неотрицательное
  «сумма»: число
FLANG_TYPE в файле dup1.flang, строка 3, столбец 1: поле «сумма» объявлено дважды

FLANG_MATCH_NOT_EXHAUSTIVE — разбор назвал не все варианты типа. Это главная причина брать тип с вариантами вместо строки: забытое состояние видно при проверке, а не в проде.

модуль «Исполнение заказа»

тип «Решение»
  вариант «Разрешено»
  вариант «Отказано» содержит причина: строка

тотальная функция «Словами»
  принимает решение: «Решение»
  возвращает строка
  разбор решение
    случай «Разрешено»
      то "можно отгружать"
FLANG_MATCH_NOT_EXHAUSTIVE в файле match1.flang, строка 10, столбец 3: разбор «Решение» не покрывает «Отказано»

Починка: дописать случай вариант «Отказано» с причина как причина и ответ на него.

FLANG_NOT_TOTAL — у функции с пометкой тотальная компилятор не смог доказать завершение. Рекурсия обязана идти к меньшему значению.

модуль «Остаток»

тотальная функция «Ждать оплаты»
  принимает дней: неотрицательное
  возвращает число
  если дней больше 0
    то «Ждать оплаты» от дней
    иначе 0
FLANG_NOT_TOTAL в файле tot1.flang, строка 7, столбец 8: тотальная функция «Ждать оплаты»: рекурсивный вызов «Ждать оплаты» не убывает — аргумент 1 («дней») — это сам параметр «дней», а не его часть. Передавайте часть аргумента: хвост списка из образца «голова и хвост», поле варианта из образца, поле записи или элемент коллекции

Починка: «Ждать оплаты» от (дней минус 1) — спуск по неотрицательное ровно на единицу компилятор принимает. Если рекурсия правилу не нужна, её лучше не писать вовсе: обход списка — свёртка или отобразить.

Ошибки выполнения

Программа проверена, но вызов на конкретном входе нарушил обещание или пришёл не того типа.

flang run требует явного согласия на запуск непроверенной программы. В этом примере flang 0.7.32 находит нарушение обещания уже при flang check.

модуль «Скидка заказа»

тотальная функция «Скидка»
  принимает сумма: неотрицательное, промокод: признак
  возвращает число
  обеспечивает «скидка не больше четверти суммы» результат не больше (сумма делить на 4)
  пример «промокод на крупном заказе»
    дано сумма равно 20000
    дано промокод равно да
    ожидается 500
  если промокод
    то 500
    иначе 0

При flang check код возврата 1. Контрпримером служит заказ на сумму 0 с промокодом. Обычный flang run останавливается с кодом 3 и указывает на замечание проверки.

FLANG_PROPERTY — с согласием --trust вычисление идёт, и обещание проверяется на настоящем входе:

$ flang run run1.flang --trust --function «Скидка» --args '{"сумма":1000,"промокод":true}'
на веру: доказанность не считалась — запуск по ключу --trust
FLANG_PROPERTY: нарушено свойство «скидка не больше четверти суммы» функции «Скидка»

Тот же отказ приходит из напечатанного кода: flang emit кладёт недоказанное обещание проверкой в каждую напечатанную функцию, и вызов из JavaScript бросает ошибку с code: "FLANG_PROPERTY" и тем же текстом. Починка — не в вызывающем коде, а в правиле: промокод на заказе в тысячу рублей правило не предусмотрело.

FLANG_TYPE: аргумент вне типа. Аргументы flang run сверяются с объявленными типами до вычисления:

$ flang run run1.flang --trust --function «Скидка» --args '{"сумма":-1000,"промокод":true}'
FLANG_TYPE: вызов функции «Скидка»: аргумент «сумма»: -1000 вне неотрицательное

Для HTTP-сервиса это ошибка клиента — 400, а не 500.

Ошибки примеров

Пример — часть функции, и flang check прогоняет его на каждой проверке.

FLANG_EXAMPLE — ответ не совпал с ожиданием.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  пример «на двадцать тысяч — две тысячи»
    дано сумма равно 20000
    ожидается 2500
  (сумма умножить на 10) делить на 100
FLANG_EXAMPLE: пример «на двадцать тысяч — две тысячи» функции «Скидка»: значение не совпало с ожидаемым: ожидалось 2500, получено 2000

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

FLANG_EXAMPLE с FLANG_PROPERTY — пример нарушил обещание той же функции.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  обеспечивает «скидка не больше тысячи» результат не больше 1000
  пример «на двадцать тысяч»
    дано сумма равно 20000
    ожидается 2000
  (сумма умножить на 10) делить на 100
FLANG_EXAMPLE: пример «на двадцать тысяч» функции «Скидка»: FLANG_PROPERTY: нарушено свойство «скидка не больше тысячи» функции «Скидка»

Пример и обещание противоречат друг другу, и компилятор не знает, кто прав. Обычно неверно обещание: потолка «не больше тысячи» в правиле нет.

FLANG_TYPE и FLANG_UNKNOWN_NAME в дано — опечатка в имени аргумента даёт два замечания: настоящий аргумент не задан, а заданный неизвестен.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  пример «опечатка в имени аргумента»
    дано сума равно 20000
    ожидается 2000
  (сумма умножить на 10) делить на 100
FLANG_TYPE в файле given1.flang, строка 6, столбец 3: пример «опечатка в имени аргумента» функции «Скидка» не задаёт аргумент «сумма»
FLANG_UNKNOWN_NAME в файле given1.flang, строка 6, столбец 3: пример «опечатка в имени аргумента» функции «Скидка» задаёт неизвестный аргумент «сума»

FLANG_TYPE: в записи не задано поле. Записи во flang без пропусков: необязательное поле объявляется словами иногда является.

модуль «Продажи»

объект «Покупка»
  «сумма»: неотрицательное
  «постоянный клиент»: признак

тотальная функция «Скидка»
  принимает покупка: «Покупка»
  возвращает число
  пример «поле забыто»
    дано покупка равно запись «Покупка» с «сумма» равным 20000
    ожидается 2000
  (покупка.«сумма» умножить на 10) делить на 100
FLANG_TYPE в файле rec1.flang, строка 10, столбец 3: пример «поле забыто»: аргумент «покупка»: не задано поле «постоянный клиент» записи «Покупка»

FLANG_TYPE: значение примера вне типа.

модуль «Продажи»

тотальная функция «Скидка»
  принимает сумма: неотрицательное
  возвращает число
  пример «отрицательная сумма»
    дано сумма равно -5
    ожидается 0
  0
FLANG_TYPE в файле neg1.flang, строка 6, столбец 3: пример «отрицательная сумма»: аргумент «сумма»: -5 вне неотрицательное

Пример на отрицательную сумму для неотрицательное не нужен: такой вход отклоняется на границе, до функции.

Ошибки доказательства

FLANG_PRECONDITION_CALL — вызов не снимает предусловие. Условие требует доказывает вызывающий, и негодный вызов отклоняется до запуска.

модуль «Скидка на вызове»

тотальная функция «Цена со скидкой»
  принимает цена: неотрицательное, скидка: неотрицательное
  возвращает число
  требует «скидка не больше цены» скидка не больше цена
  обеспечивает «цена не уходит в минус» результат не меньше 0
  цена минус скидка

тотальная функция «Цена товара по акции»
  возвращает число
  «Цена со скидкой» от 100 и 300
FLANG_PRECONDITION_CALL в файле pre1.flang, строка 12, столбец 3: вызов «Цена со скидкой» в функции «Цена товара по акции» не снимает предусловие «скидка не больше цены»: …

Сообщение длинное: дальше компилятор перечисляет, какие виды выражений он умеет ограничить и что известно в месте вызова. Читать стоит первую фразу — она называет вызов и условие. Починка: вызвать от 1000 и 300, где скидка не больше цены. Граница этой проверки узкая: предусловие, записанное вызовом своей функции-предиката, компилятор не снимает ни на одном вызове.

FLANG_PROOF_STEP — теорема ссылается на обещание, которого нет.

модуль «Счёт»

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

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

теорема «вдвое не меньше нуля»
  дано цены: список числа
  утверждаем результат не меньше 0
  по свойству «позиций больше нуля»
  следовательно доказано
FLANG_PROOF_STEP в файле proof1.flang, строка 18, столбец 3: шаг 1, теорема «вдвое не меньше нуля»: постусловия «позиций больше нуля» нет ни у одной функции модуля — сослаться не на что. к этому месту не известно ничего, кроме гипотез «дано»

Починка: по свойству «позиций не меньше нуля» — имя обещания слово в слово.

FLANG_PROOF_CLAIM_MISMATCH — теорема утверждает не то, что обещает функция.

модуль «Счёт»

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

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

теорема «вдвое не меньше нуля»
  дано цены: список числа
  утверждаем результат не меньше 1
  по свойству «позиций не меньше нуля»
  следовательно доказано
FLANG_PROOF_CLAIM_MISMATCH в файле proof2.flang, строка 17, столбец 3: теорема «вдвое не меньше нуля» утверждает не то, что обещает функция «Вдвое»: утверждение теоремы и постусловие обязаны совпадать слово в слово. Ядро не решает, что два разных утверждения означают одно и то же

Починка: утверждаем результат не меньше 0 — как в обеспечивает.

«Сетка N» — не ошибка, но и не доказательство. Обещание, которое ядро не вывело, flang check --proof называет так:

  постусловие «скидка ограничена» функции «Рассчитать скидку» — сетка 5 значений (примеры функции): … Это не доказательство — теоремы при утверждении нет

и выходит кодом 3. С ключом --strict четыре исхода разъезжаются кодами: 0 — доказано всё, 1 — опровергнуто, 3 — не удалось доказать, 2 — не поддерживается. Ключ --fast пропускает ядро доказательств и примеры и выходит кодом 4, чтобы пропуск не выглядел зелёным.

Ошибки фактов

flang facts вычисляет утверждения на данных JSON. Код 1 здесь значит не «сломалось», а «утверждение не выполнено», и вердикт всё равно приходит в stdout.

Опровергнуто ("status": "refuted"). Данные не подтверждают утверждение:

$ flang facts order-shipment.flang --facts order-shipment.blocked.facts.json --claims '["«Заказ с номером отгружается» от заказы, номер равно да"]'
"holds": false,
"why": "«Заказ с номером отгружается» от факта «заказы», факта «номер» = нет, а утверждение требует «равно да». …",
"status": "refuted"

Отклонено ("status": "refused"). Утверждение записано неверно: не то число аргументов или функции нет.

"why": "функция «Заказ с номером отгружается» принимает 2 аргумент(ов), а в утверждении их 1"
"why": "функция «Отгрузить» не найдена в программе"

Аргументы в утверждении перечисляются через запятую: от заказы, номер.

Кривой вызов — код 2:

$ flang facts order-shipment.flang --claims 'нет'
flang facts: --claims должен быть JSON-массивом строк

Чего компилятор не ловит

Три случая, на которых проверка зелёная, а читатель ждёт замечания:

  • функция без строки возвращает проходит flang check с кодом 0 — тип результата выводится из тела. Пишите возвращает сами: это часть контракта, а не украшение;
  • файл без первой строки модуль проходит проверку как «без имени модуля»;
  • незнакомое слово в условии (превышает) даёт у 'если' нет ветки 'то', а не «неизвестное сравнение» — место ошибки называет столбец.

Практика в песочнице

Поменяйте в любом примере ожидается и найдите в ответе FLANG_EXAMPLE. Затем верните пример и измените потолок в обещании «скидка ограничена» на 1000 — сломается пример, и ответ назовёт FLANG_PROPERTY.

Удалите строку случай «Разрешено» в «Причине отказа» и прочитайте FLANG_MATCH_NOT_EXHAUSTIVE. Потом поменяйте поле заказ.«оплачен» на заказ.«оплата» и посмотрите, какое замечание придёт первым.

Чек-лист: что проверить, когда модель не проходит

  1. Первая строка — модуль «Имя».
  2. Читать первое замечание и его столбец; остальные часто идут от него.
  3. FLANG_PARSE — отступы, ветви то и иначе, слова сравнения из закрытого списка.
  4. FLANG_UNKNOWN_NAME — опечатка в имени типа, функции, аргумента.
  5. FLANG_TYPE — имя поля, тип результата, сравнение порядка над нечислом, все поля записи в примере.
  6. FLANG_MATCH_NOT_EXHAUSTIVE — разобраны все варианты типа.
  7. FLANG_NOT_TOTAL — рекурсия идёт к меньшему значению.
  8. FLANG_EXAMPLE — сначала решить, кто прав: пример или правило.
  9. Код 3 у flang check --proof — прочитать, какие обещания держатся только на примерах, и решить, принимать ли это.

Кейсы каталога по этой теме

Нашли неточность? Выделите фрагмент текста — рядом появится жучок.

Нужен разбор именно вашей ситуации?

Статья описывает общий случай. Если у вас частный — можно разобрать его отдельно, платно. А если не хватает целого материала, предложите тему: её оплачивают вскладчину, и она выходит открытой для всех.

Доска запросов
Дальше