charon

Patinir, E., 1515-1524, ландшафт с хароном, пересекающим стиль [масло на дереве]. Museo del Prado, Мадрид. Источник

Харон

Харон действует как интерфейс между компилятором Rustc и проектами проверки программы. Его цель состоит в том, чтобы обработать ящики ржавчины и преобразовать их в файлы, легко обрабатывать программные проверки. Он реализован как пользовательский драйвер для компилятора Rustc.

Харон, в греческой мифологии, старик, несущий души покойного, приобретает Стикс, реку, разделяющую мир жизни от мира мертвых. В настоящем контексте Харон позволяет нам перейти от мира ржавчин в мир формальной проверки.

Мы открыты для вкладов ! Пожалуйста, свяжитесь с нами, чтобы мы могли координировать себя, если вы готовы внести свой вклад. Для этого вы можете присоединиться к Zulip.

LLBC

Charon преобразует код miR в ULLBC (неструктурированное исчисление заменов низкого уровня), затем в LLBC. Оба AST могут быть выведены Charon.

ULLBC - это слегка упрощенный miR, где мы стараемся удалить как можно больше избыточных средств. Например, мы радикально упрощаем представление констант, исходящих от компилятора ржавчины.

LLBC-это ULLBC, где мы реструктурировали потоки управления с петлями, if ... then ... else ... и т. Д. Вместо Gotos. Следовательно, мы объединяем операторы MIR и терминаторы в один тип оператора LLBC. Мы также выполняем некоторые дополнительные модификации, некоторые из которых перечислены ниже:

Примечание : Большинство преобразований, которые превращают miR в ULLBC, затем LLBC реализованы с помощью микропроходов. В зависимости от необходимости, мы могли бы сделать их необязательными и контролировать их флагами. Если вы хотите узнать больше о деталях, см. translate в src/driver.rs , который применяет микропроходы один за другим.

Примечание : если вы хотите узнать полную информацию о (U) LLBC, посмотрите на: types.rs , values.rs , expressions.rs , ullbc_ast.rs и llbc_ast.rs .

Извлеченный AST сериализован в файлах .ullbc и .llbc (с использованием формата JSON). Мы извлекаем целый ящик в один файл.

Структура проекта

• charon : реализация ржавчины.
• charon-ml : библиотека ML. Предоставляет коммунальные услуги для извлечения и манипулирования AST в OCAML (десериализация, печать и т. Д.).
• tests и tests-polonius : каталоги тестирования файлов. tests-polonius содержит код, который требует проверки заемных заем Полония.

Установка и сборка

Сначала вам нужно установить rustup .

Поскольку Charon настроен с грузом, Rustup автоматически загрузит и установит соответствующие пакеты при создании проекта. Если вы хотите только построить проект Rust (в ./charon ), просто запустите make build-charon-rust в верхнем каталоге.

Если вы также хотите построить библиотеку ML (в ./charon-ml ), вам нужно будет установить OCAML и соответствующие зависимости.

Мы предлагаем вам следовать этим инструкциям и установить Opam на пути (те же инструкции).

Для Charon-ML мы используем OCAML 4.13.1 : opam switch create 4.13.1+options

Зависимости могут быть установлены со следующей командой:

 opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc menhir unionFind

Затем вы можете запустить make build-charon-ml , чтобы построить библиотеку ML или даже просто make , чтобы создать весь проект (Rust и OCAML). Наконец, вы можете запустить тесты с помощью make test .

В качестве альтернативы, вы можете использовать NIX и сделать nix develop (или использовать https://direnv.net/ и direnv allow ), и все зависимости должны быть доступны.

Документация

Вы можете получить доступ к документации Rust онлайн.

Вы также можете запустить make , чтобы сгенерировать документацию локально. Он будет генерировать документацию, доступную от doc-rust.html (для проекта Rust) и doc-ml.html (для библиотеки ML).

Использование

Чтобы запустить Charon, вы должны запустить бинарный шарон изнутри ящика, который вы хотите скомпилировать, как если бы вы хотели построить ящик с cargo build . Руководитель Charon находится в bin/charon .

Харон построит ящик и его зависимости, а затем извлечет AST. Charon предоставляет различные варианты и флаги, чтобы настроить его поведение: вы можете отобразить подробную документацию с помощью --help . В частности, вы можете распечатать LLBC, сгенерированный Charon с --print-llbc .

Если в корне вашего проекта есть файл Charon.toml , Харон также возьмет на себя варианты. Файл поддерживает те же параметры в интерфейсе CLI, за исключением параметров, которые относятся к входу/выводу, например --print-llbc . Пример Charon.toml :

[ charon ]
extract_opaque_bodies = true
[ rustc ]
flags = [ " --cfg " , " abc " ]

Замечание : Поскольку Харон составлен с Rust Nigthly (это необходимо внедрить водитель Rustc), он построит ваш ящик с ночью Rust. Вы можете найти ночную версию, прикрепленную для Charon в rust-toolchain.template .