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

К README · Указатель документации

Код на C в flang: перевод, проверка ядром, круг и черновик спеки

Переводчик читает функции на C, печатает их перевод на flang и отдаёт перевод ядру. Каждый вердикт здесь — о переводе: «перевод функции X обладает свойством P». Чтобы вердикт о переводе что-то говорил о самом C, перевод печатается обратно в C и сверяется с исходником на сетке входов. Решение и его границы — ADR-0058.

Как позвать

bootstrap/flang run-script foreign-c:demo     # корпус flang/foreign/c/corpus, отчёт и вердикт
bootstrap/flang run-script foreign-c:census   # доля функций C дерева, попадающих в подмножество

Нужны clang и cc с -fsanitize=undefined. Временные файлы — под FLANG_TMP.

Что лежит в наборе примеров

Что печатает отчёт по каждой функции

  1. Перевод — целиком, тем текстом, который судит ядро. Параметры int несут требования INT_MIN…INT_MAX. Строки обязательство N · строка L: … — места, где C не определён: результат арифметики вне int, делитель ноль, конец функции без return, неопределённость внутри вызванной функции. За функцией в том же модуле идут вспомогательные функции её циклов и копии функций, которые она вызывает.
  2. Утверждения и вердикты. У каждого — слово ядра («доказано ядром» / «не доказано ядром») и, если на сетке нашёлся вход, где утверждение ложно, — сам вход, что сделал на нём C и что сказал на нём flang run по переводу.
  3. Круг C → flang → C. Сколько входов сетки вне требований, на скольких значения сошлись, на скольких C остановлен санитайзером и обязательство это назвало. Расхождение — это ошибка перевода, и план краснеет.
  4. Черновик спецификации. Строки обеспечивает, помеченные ВЫВЕДЕНО из перевода и основанием. Хвост строки говорит, что с ней: доказано ядром, отброшено контрпримером или ВОПРОС ЧЕЛОВЕКУ — ядро не доказало, а сетка не опровергла.
  5. Подделки переводчика. Три ложных переводчика: роняет первую ветвь if, сдвигает первую константу на единицу, переставляет операнды первой некоммутативной операции. Каждый обязан разойтись с C на круге.

Подмножество C

Функции int f(…) с параметрами int и структурами из полей int, переданными по значению. Операторы: return, if/else, блоки, пустой оператор, объявление локальной int с начальным значением и без него, присваивание локальной или параметру (=, +=, -=, *=, /=, %=, ++, -- отдельным оператором), циклы for и while со счётчиком. Выражения: литералы int, параметры и локальные, поле структуры-параметра (r.width), вызов функции, переведённой выше в том же файле, + - * / %, сравнения, && || !, унарные -, +, ?:. На всём прочем переводчик отказывает и называет строку и конструкцию: указатели и массивы, глобальные, другие типы, break, continue, return внутри цикла, do, switch, рекурсия, присваивание внутри выражения.

Присваивание

Каждое присваивание заводит новое имя: x = x + 1; после пусть «x» равно … становится пусть «x 4» равно («x» плюс 1), и всё, что ниже, читает «x 4». Ветви if получают продолжение функции каждая своё, поэтому после ветвей имя у переменной своё на каждом пути. Чтение локальной до первого присваивания — отказ.

Цикл

Цикл переводится, если у него есть счётчик: последний оператор тела (у for — шаг) сдвигает переменную на постоянное число (i++, i--, i += 2, i = i - 3), условие сравнивает её с границей знаком, который ведёт её к границе (<, <= при шаге вверх, >, >= при шаге вниз), счётчик меняется только шагом, а граница в теле не меняется.

Перевод — вспомогательные функции рядом с переводом, по одной на каждую переменную, которую цикл меняет: «factorial loop 4 result» принимает все переменные цикла, при истинном условии вызывает себя на значениях после одного оборота, при ложном отдаёт свою переменную. Завершение у них — объявленной мерой: убывает ((«n» минус «i») плюс 1), расстояние от счётчика до границы, и проверка меры стоит в напечатанном коде. После цикла пусть «result 6» равно («factorial loop 4 result» от …).

Обязательство C внутри тела (result * i в int) должно держаться на каждом обороте. Для него печатается функция-признак «factorial loop 4 duty 1»: обязательство на текущем обороте и она же на следующем. Строка обеспечивает перевода зовёт её на значениях до цикла под тем же именем обязательства.

У цикла без такого счётчика — while (n >= 10) n = n / 10; — меры, выводимой из кода, нет, и переводчик отказывает: «цикл без выводимой меры».

Вызов

Вызвать можно функцию, которая переведена выше в том же файле. В модуль перевода вызывающей кладётся копия вызванной (параметры число, без требований) и функция-признак «width ok»: все обязательства C вызванной на её параметрах. У вызова своё обязательство «вызов width(…) без неопределённого поведения внутри» — этот признак на аргументах вызова.

Структура

Структура из полей int становится записью: объект «struct span» с полями число, поле читается («s».«start»), у каждого поля требования INT_MIN…INT_MAX. На сетке структура раскладывается по полям (s.start, s.length), обвязка C собирает её составным литералом, а контрпример переигрывается через «span_end flat» — обёртку, которая собирает запись из полей.

Сетка у функции с циклом

У функции, в чьём переводе или в переводе вызванных есть цикл, из сетки убираются числа больше 100000 по модулю: обход до INT_MAX шёл бы миллиарды оборотов и в C, и в напечатанном flang. Ошибку переполнения на больших значениях такая сетка видит только тогда, когда она случается раньше, например factorial на 1000.

Как читать «не доказано»

«Не доказано ядром» — не «ошибка». Ядро не берёт условие ветви фактом, поэтому обязательство «делитель не ноль» за проверкой if (count <= 0) return 0; остаётся недоказанным, хотя верно. Ошибкой исход становится, когда сетка нашла вход, на котором утверждение ложно, и flang run на нём назвал нарушенное свойство.

Обязательства внутри цикла ядро сегодня не доказывает ни одного: индукцию оно цепляет к разбор, а вспомогательная функция цикла — ветвление и объявленная мера. Их судит сетка.

Связанное: «flang на чужом коде» · «Требования и спецификации»