Notice: file_put_contents(): Write of 5391 bytes failed with errno=28 No space left on device in /var/www/tgoop/post.php on line 50

Warning: file_put_contents(): Only 16384 of 21775 bytes written, possibly out of free disk space in /var/www/tgoop/post.php on line 50
Блог*@dereference_pointer_there P.8281
DEREFERENCE_POINTER_THERE Telegram 8281
#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 в публичных интерфейсах.
👍5🤔2



tgoop.com/dereference_pointer_there/8281
Create:
Last Update:

#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 в публичных интерфейсах.

BY Блог*


Share with your friend now:
tgoop.com/dereference_pointer_there/8281

View MORE
Open in Telegram


Telegram News

Date: |

There have been several contributions to the group with members posting voice notes of screaming, yelling, groaning, and wailing in different rhythms and pitches. Calling out the “degenerate” community or the crypto obsessives that engage in high-risk trading, Co-founder of NFT renting protocol Rentable World emiliano.eth shared this group on his Twitter. He wrote: “hey degen, are you stressed? Just let it out all out. Voice only tg channel for screaming”. In the next window, choose the type of your channel. If you want your channel to be public, you need to develop a link for it. In the screenshot below, it’s ”/catmarketing.” If your selected link is unavailable, you’ll need to suggest another option. The channel also called on people to turn out for illegal assemblies and listed the things that participants should bring along with them, showing prior planning was in the works for riots. The messages also incited people to hurl toxic gas bombs at police and MTR stations, he added. Public channels are public to the internet, regardless of whether or not they are subscribed. A public channel is displayed in search results and has a short address (link). The imprisonment came as Telegram said it was "surprised" by claims that privacy commissioner Ada Chung Lai-ling is seeking to block the messaging app due to doxxing content targeting police and politicians.
from us


Telegram Блог*
FROM American