#prog #rust #rustlib

pre — библиотека для помощи с правильным использованием unsafe кода.

Причина, по которой unsafe может быть в публичном интерфейсе функции, заключается в том, что для корректной работы функции требуются условия, которые не могут быть проверены компилятором или которые проверять очень дорого. В среде разработки на Rust распространена культура использования safety comments. Именно, unsafe функция перечисляет в документации необходимые условия для безопасного использования, а вызовы этой функции перечисляют причины, по которым условия удовлетворены. В clippy есть линт на отсутствующую safety документацию на unsafe определениях, а в tidy (внутреннем линтере для компилятора Rust) есть даже проверка на наличие этих комментариев на вызывающей стороне.

Не смотря на то, что это лучше, чем ничего, это подход довольно хрупок. Помимо того, что не все используют clippy (и уж тем более никто не использует tidy вне разработки самого Rust), эти проверки недостаточно гранулярны: они проверяют лишь наличие комментариев но не их содержимое. Это означает, что если по каким-то причинам условия использования и их обоснования на месте вызова разъедутся, эти инструменты их не отловят. Ну и, разумеется, никакие линтеры by design не могут остановить компиляцию кода (если только не включить их в общий процесс сборки кода). Библиотека pre стремится заполнить этот пробел.

Именно, библиотека позволяет добавлять на unsafe функции атрибуты #[pre], каждый из которых содержит одно условие — в простейшем виде просто в виде словесного описания:

#[pre("`arg` is a meaningful value")]
fn foo(arg: i32) {
    assert_eq!(arg, 42);
}

Эти условия трансформируются в дополнительный аргумент для функции — типа с нулевым размером — значение которого предоставляется на вызывающей стороне при помощи макроса assures:

#[pre] // Enables `assure`ing preconditions inside the function
fn main() {
    #[assure("`arg` is a meaningful value", reason = "42 is very meaningful")]
    foo(42);
}

Подобный подход всё так же полагается на человека в плане непосредственно проверки условий, но за счёт проверки того, что каждое отдельное условие удовлетворено на вызывающей стороне с идентичной формулировкой позволяет синхронно развивать определение unsafe кода и его использование. Именно, за счёт того, что каждое условие становится частью аргумента, изменение списка условий (добавление, удаление или изменение формулировки) становится ошибкой компиляции.

Условия можно записывать не только словесно, но и также в виде предиката или специального синтаксиса для утверждения корректного выравнивания сырых указателей или их валидности для операций чтения и/или записи:

#[pre(valid_ptr(ptr_name, r+w))]
fn foo(ptr_name: *mut i32) {}

#[pre(proper_align(ptr_name))]
fn bar(ptr_name: *mut i32) {}

// Предусловие в виде предиката также
// добавляет в функцию соответствующий
// `debug_assert!`
#[pre(a < b || b > 17)]
fn baz(a: i32, b: i32) {}

Также библиотека даёт способ предоставить предусловия для функций из сторонних библиотек.

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