flang — язык с доказуемым завершением Интерпретатор: явный стек, лимиты, хвостовые вызовы
0%

Интерпретатор: явный стек, лимиты, хвостовые вызовы

Интерпретатор: явный стек, лимиты, хвостовые вызовы

flang run, flang test и примеры внутри flang check считают программу одним и тем же вычислителем. Он написан на самом flang — файл flang/self/interpret.flang, модуль «Вычислитель flang», около 4500 строк, — и собран в двоичный файл вместе с остальным компилятором. Ни Node, ни компилятор C для run не нужны.

Явный стек вместо рекурсии

Наивный интерпретатор — функция «вычислить узел», которая вызывает себя на подузлах. Для языка, где программы обязаны завершаться, этого хватило бы. Но у flang есть и обычные функции, которые могут не завершаться, и единственная защита от них — предел шагов и глубины. Если бы вычислитель рекурсивно звал сам себя, раньше этого предела кончился бы стек самой машины, и вместо понятного отказа программа упала бы на случайной глубине.

Поэтому вычисление — цикл над явным стеком кадров. В flang/self/interpret.flang это видно по типам: значение «Машина» держит «работу» — стопку кадров («Кадр выражения», «Кадр если», «Кадр разбора», «Кадр свёртки», «Кадр возврата» и другие), счётчик витков и текущую глубину. Каждый виток цикла снимает кадр сверху и кладёт новые. Стопка — обычное значение в памяти, поэтому глубину ограничивает только предел, а счётчик шагов растёт на каждом витке — и там, где рекурсия хвостовая и глубина не растёт вовсе.

Формы, которые вычислитель не умеет считать, отвечают кодом FLANG_SELF_EVAL_UNSUPPORTED, а не пропускаются молча (docs/flang/self/SPEC.md).

Пределы

У run и test три предела вычисления:

Ключ Умолчание в 0.7.29 Что ограничивает
--max-steps N 40 000 000 шагов число витков вычислителя
--max-depth N 20 000 глубину вызовов вычисляемой программы
--memory-limit N три четверти памяти машины память прогона, байтами или с буквой K, M, G, T

Не путайте их с --step-limit и --depth-limit: это пределы самого двоичного файла (он тоже программа на flang и тоже считает свои шаги), а не вычисляемой программы. Умолчания выше сняты прогонами ниже.

Заведомо вечная программа:

модуль «Зацикливание»

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

check её пропускает: функция не объявлена тотальной, и компилятор только называет её среди функций без доказанного завершения:

$ flang check вечность.flang
модуль «Зацикливание»: функций 1, из них с доказанным завершением 0; типов 0
без доказанного завершения: «Вечность»
вечность.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

А запуск упирается в предел шагов:

$ flang run вечность.flang --function Вечность --args '{"н": 0}' --max-steps 1000000 --cost
доказано: утверждений 0
FLANG_RECURSION_LIMIT: функция «Вечность» исчерпала лимит шагов (1000000) на глубине вызовов 1
цена прогона: шагов 1000001, пик памяти 12652544 байт, секунд 1.442572
$ echo $?
1

--cost печатает цену прогона: на этой машине вычислитель делает около 700 тысяч шагов в секунду, поэтому до предела по умолчанию, 40 миллионов, вечная функция крутится около минуты (у нас — 57 секунд).

Нехвостовая рекурсия упирается в глубину:

модуль «Глубина»

функция «Башня»
  принимает н: число
  возвращает число
  1 плюс («Башня» от (н плюс 1))
$ flang run глубина.flang --function Башня --args '{"н": 0}' --max-steps 100000000
доказано: утверждений 0
FLANG_RECURSION_LIMIT: функция «Башня» превысила предел глубины вызовов (20000) на глубине 20001

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

модуль «Память»

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

функция «Начать»
  принимает н: число
  возвращает число
  «Копить» от н и []
$ flang run память.flang --function Начать --args '{"н": 0}' --memory-limit 50M
…
FLANG_MEMORY: прогон остановлен на пределе памяти 50 МиБ: занято 49 МиБ, просили ещё 65 568 байт
  считалась функция «Копить», шагов программы 86 648
…
Поднять или снять на один прогон: flang run <файл> --предел-памяти 40G (латиницей
--memory-limit; буквы K, M, G, T; 0 — без предела). Код возврата 5.

У трёх пределов разные коды возврата: шаги и глубина — 1 с кодом FLANG_RECURSION_LIMIT, память — 5 с FLANG_MEMORY.

«На глубине вызовов 1»

В ответе «Вечности» стоит деталь, которая объясняет устройство: функция вызвала себя миллион раз, а глубина осталась единицей. Это хвостовые вызовы. Перед вызовом вычислитель смотрит на стопку: если сверху лежит кадр возврата без постусловий, вызов его переиспользует и глубина не растёт (функции «Это хвостовой вызов» и «Кадр возврата без постусловий» в flang/self/interpret.flang).

Для языка без циклов это условие работоспособности: раз единственный способ пройти список — рекурсия, она обязана идти в постоянной глубине.

Оговорка про постусловия существенна. Функции с постусловием нужно проверить именно свой результат, поэтому её кадр не переиспользуется — и та же вечная функция с постусловием обеспечивает растёт в глубину:

модуль «С постусловием»

функция «Вечность»
  принимает н: число
  возвращает число
  обеспечивает «не меньше нуля» результат не меньше 0
  «Вечность» от (н плюс 1)
$ flang run пост.flang --function Вечность --args '{"н": 0}' --max-steps 100000 --trust
на веру: доказанность не считалась — запуск по ключу --trust
FLANG_RECURSION_LIMIT: функция «Вечность» исчерпала лимит шагов (100000) на глубине вызовов 14286

Без --trust эту программу run не запустит вовсе: постусловие не доказано, и ответ — код 3 со списком недоказанного (глава «Инструмент»).

Какие значения получаются

docs/flang/SPEC.md, раздел «Семантика, которая обязана совпадать у всех слоёв», задаёт решения, общие для вычислителя и всех целей кодогенерации. Главные, проверенные запуском:

Вопрос Решение Прогон на 0.7.29
число IEEE-754 double 0.1 плюс 0.2 равно 0.30000000000000004
равенство скаляров NaN равен NaN, 0 не равен −0 (0.1 плюс 0.2) равно 0.3 — false
равенство списков, записей, вариантов структурное
деление на ноль бесконечность, не ошибка 1 делить на 0 — Infinity
индексация строк и списков с 1, включительно с обоих концов
длина строки в кодовых точках длина "ёж😀" — 3
к строке от признака да / нет к строке да — "да"

Для денег и других расчётов без округления в языке есть точные числа (с 0.7.25): точное целое без потолка и точное дробное — сокращённая дробь. С число они не смешиваются, смешение — отказ FLANG_TYPE:

модуль «Точные числа»

тотальная функция «Сумма целых»
  принимает а: точное целое, б: точное целое
  возвращает точное целое
  пример «2⁵³ + 1 плюс 1 равно 2⁵³ + 2»
    дано а равно [1, 0, 512]
    дано б равно [1]
    ожидается [2, 0, 512]
  а плюс б

тотальная функция «Сумма дробей»
  принимает а: точное дробное, б: точное дробное
  возвращает точное дробное
  пример «одна десятая плюс одна пятая — ровно три десятых»
    дано а равно [[1], [10]]
    дано б равно [[1], [5]]
    ожидается [[3], [10]]
  а плюс б

тотальная функция «Сумма в double»
  принимает а: число, б: число
  возвращает число
  пример «0.1 плюс 0.2 в double — не 0.3»
    дано а равно 0.1
    дано б равно 0.2
    ожидается 0.30000000000000004
  а плюс б
$ flang test точные.flang
точные.flang: примеров 3, прошло 3, не прошло 0

Точное целое записывается разрядами по основанию 2²², младший первым: [1, 0, 512] — это 2⁵³ + 1, числа, которого в double нет. Литерал сверяется с каноном при проверке: несокращённая дробь [[2], [10]] — отказ «дробь не сокращена».

Отказы без перехвата

Отказ встроенной формы прекращает вычисление целиком:

модуль «Семантика»

тотальная функция «Голова»
  принимает н: число
  возвращает число
  голова []
$ flang run семантика.flang --function Голова --args '{"н": 1}'
доказано: утверждений 0
FLANG_BUILTIN_ARGS: «голова»: список пуст

Исключений и перехвата в языке нет. Проверка должна стоять до опасной формы: сначала если пусто xs, потом голова xs, либо функция возвращает вариант из flang/stdlib/optional.flang или flang/stdlib/result.flang. Для факт-чекинга это то, что нужно: детерминированный отказ вместо частично сделанного вычисления.

Что из этого стоит унести

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

Дальше — глава «Кодогенерация»: то же вычисление, но в программе на другом языке.

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

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

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

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