3 个不稳定版本
0.2.1 | 2021年9月21日 |
---|---|
0.2.0 | 2020年7月25日 |
0.1.0 | 2020年7月14日 |
在 #compiler-error 中排名 14
每月下载量 966
在 3 个crate中(通过 pre)使用
120KB
2.5K SLoC
pre
pre 是一个帮助程序员正确维护函数调用前提条件的 Rust 库。它主要用于与 unsafe
函数一起使用,因为它们具有无法在编译时检查的前提条件。
动机
有时函数或方法具有无法在类型系统中保证且无法在运行时进行保护的先决条件。这类函数的最典型例子是 unsafe
函数。当正确使用时,unsafe
函数用于 "声明编译器无法检查的合同存在"。这些合同是函数调用的先决条件。未能遵守它们通常会导致内存安全问题和不确定行为。
目前处理 unsafe
函数上的这些先决条件最常用的方案是在函数文档的 Safety
部分中提及它们。然后,使用该函数的程序员需要检查他们需要确保什么才能正确调用该函数。使用该函数的程序员可以在函数旁边留下注释,描述调用为什么是安全的(为什么先决条件成立)。
这种做法甚至被编译器(截至 1.44.1 版本)在 unsafe
块之外使用 unsafe
函数时所宣传。
note: consult the function's documentation for information on how to avoid undefined behavior
这种方法存在多个失败点。其中之一是
- 原始函数无法记录先决条件是什么。
- 使用该函数的程序员可能会忘记查看记录的先决条件。
- 使用该函数的程序员可能会忽略一个或多个先决条件。如果多个先决条件在一个长段落中记录,这种情况并不罕见。
- 程序员在检查先决条件是否成立时可能会出错。
- 更新可能会改变函数所需的先决条件,而函数的使用者可能容易忽略这一事实。
- 程序员可能会忘记(或选择不)记录在调用函数时先决条件成立的理由,这使得其他人更容易在以后更改调用或相关代码时出错。
这个库无法防止所有这些问题,尤其是无法防止1和4。然而,它试图帮助防止2、3、5和6。
方法
这个库通过允许程序员以统一格式指定他们编写的函数上的先决条件来工作。然后,这些先决条件被转换为一个额外的函数参数。函数的调用者随后在调用位置指定相同的先决条件,以及他们为什么认为先决条件得到满足的理由。如果先决条件不匹配或未指定,函数将有无效的参数,代码将无法编译。这应该可以防止上述2、3和5中的问题。因为需要在函数调用位置提供理由,所以问题6至少在某种程度上得到了保护,尽管程序员仍然可以选择不在这方面投入太多精力。
通过添加一个单个的零大小参数来更改函数的签名。这意味着当使用发布模式编译时,这些检查没有运行时成本。它们是一个零成本的抽象。
用法
预crate的基本用法如下
use pre::pre;
#[pre("`arg` is a meaningful value")]
fn foo(arg: i32) {
assert_eq!(arg, 42);
}
#[pre] // Enables `assure`ing preconditions inside the function
fn main() {
#[assure("`arg` is a meaningful value", reason = "42 is very meaningful")]
foo(42);
}
pre
属性用于指定先决条件(在foo
上)并启用assure
属性(在main
上)的使用。要了解为什么第二种用法是必要的,请阅读有关检查功能的文档段落。
使用assure
属性,程序员确保他们已经检查了先决条件,并且先决条件得到满足。如果没有assure
属性,代码将无法编译。
use pre::pre;
#[pre("`arg` must have a meaningful value")]
fn foo(arg: i32) {
assert_eq!(arg, 42);
}
fn main() {
foo(42);
// ^^^^^^^-- this errors
}
assure
属性内的先决条件必须与函数定义中pre
属性内的先决条件完全相同,代码才能编译。然而,如果有多个先决条件,其顺序并不重要。
已知限制
在处理unsafe
代码时,有许多细微之处。pre旨在帮助程序员了解应该查看哪些地方,但它不会做更多的事情。程序员仍然必须手动检查所有unsafe
代码的合约。因此,即使在使用pre的情况下,也应始终检查文档中的“安全性”部分。
pre所能做的也有一些技术限制
-
存在多种形式的
unsafe
代码。pre目前专门关注unsafe
函数。 -
虽然pre在稳定编译器上也能工作,但有许多只有在使用夜间编译器时才能工作的事情。
这是夜间版本和稳定版本之间的主要区别(还有其他一些较小的问题)
-
在
impl
块中的函数前提条件仅在夜间构建版本中有效。此规则不适用于在带有
extern_crate
注解的模块内的impl
块。尽管如此,这些块也有其自身的限制(见下文)。 -
仅在夜间构建版本中,预先警告才有可能出现。
-
在夜间构建版本中,错误可以引用多个位置,提供更好的建议和消息。
-
-
由于预先是通过向函数添加一个额外的参数来工作的,它改变了函数签名。在很多情况下这不会造成影响,但如果您使用函数指针或作为参数传递函数,则其类型将与看似的类型不同。
-
由于当前稳定编译器不支持表达式和语句的属性宏,因此包含
assure
属性的函数必须至少有一个pre
属性,尽管它可以是一个空属性:#[pre]
。 -
预先是为 2018 版本设计的。虽然它也适用于 2015 版本,但如果您还没有,可能需要添加一个
extern crate core
语句。另外,extern_crate
属性 不支持 2015 版本。 -
虽然在使用
cfg_attr
属性 中的任何预先属性时可以工作,但这里有两个限制- 所有
cfg_attr
属性必须具有相同的配置谓词。这里的相同意味着语法相等,所以all(unix, target_endian = "little")
与all(target_endian = "little", unix)
不相同。这可以通过将所有前提条件放在单个cfg_attr
后面来最简单地实现。 - 不支持嵌套的
cfg_attr
属性,因此#[cfg_attr(unix, cfg_attr(target_endian = "little", assure(...)))]
目前不被预先识别。
- 所有
-
在带有
extern_crate
属性 的模块或其父模块中定义的函数和方法的限制有很多。- 对这样的函数/方法的调用会调用原始类型中的原始函数/方法,这意味着前提条件不会得到考虑。使用
forward
属性 来检查这些调用上的前提条件。 - 由于它们的实现方式,这些函数的名称可能与周围模块中的名称冲突。在常规使用中这种情况不太可能发生,但确实可能。如果您遇到这种情况,请提交一个问题,描述遇到的问题。
- 目前,对于
impl
块的所有类型信息都被丢弃。这意味着在带有extern_crate
注解的模块中,多个不重叠(在类型系统意义上)的impl
块可以重叠。
- 对这样的函数/方法的调用会调用原始类型中的原始函数/方法,这意味着前提条件不会得到考虑。使用
理解错误信息
pre试图在其提供的错误信息中提供尽可能多的帮助。不幸的是,在某些情况下,pre没有足够的信息自行生成错误,而必须依赖rustc在编译后期进行。pre对这些消息的外观有非常有限的控制。
如果您难以理解这些错误信息,以下是一个简要概述,说明它们的外观和含义。
error[E0061]: this function takes 2 arguments but 1 argument was supplied
--> src/main.rs:7:5
|
3 | #[pre(x > 41.9)]
| _______-
4 | | fn foo(x: f32) {}
| |_________________- defined here
...
7 | foo(42.0);
| ^^^ ---- supplied 1 argument
| |
| expected 2 arguments
此错误表示函数具有先决条件,但它们没有被assure
确保。
要修复此错误,找出函数的先决条件以及它们是否成立。一旦您确信它们成立,您可以使用带有assure
属性的assure
来确保向pre提供,并在reason
中解释,为什么您确信它们成立。您应该在函数的文档中找到函数的先决条件。
夜间编译器错误
error[E0308]: mismatched types
--> src/main.rs:8:5
|
8 | / #[assure(
9 | | x > 41.0,
10 | | reason = "42.0 > 41.0"
11 | | )]
| |______^ expected `"x > 41.9"`, found `"x > 41.0"`
|
= note: expected struct `std::marker::PhantomData<(pre::BooleanCondition<"x > 41.9">,)>`
found struct `std::marker::PhantomData<(pre::BooleanCondition<"x > 41.0">,)>`
稳定编译器错误
error[E0560]: struct `foo` has no field named `_boolean_x_20_3e_2041_2e0`
--> src/main.rs:9:9
|
9 | x > 41.0,
| ^ help: a field with a similar name exists: `_boolean_x_20_3e_2041_2e9`
此错误表示在调用站点assure
确保的先决条件与函数定义处的先决条件不同。
不幸的是,对于包含大量符号的先决条件,稳定编译器错误的可读性不高。如果您在阅读这些错误信息时遇到困难,建议使用夜间编译器来修复这些错误。一旦修复,您就可以继续使用稳定编译器。
要修复此错误,请确保所有assure
确保的先决条件与函数上的先决条件完全匹配。此外,在修改assure
确保的先决条件时,请确保它们仍然成立。您应该在函数的文档中找到函数的先决条件。
夜间编译器错误
error[E0308]: mismatched types
--> src/main.rs:9:5
|
9 | / #[assure(
10 | | x > 41.9,
11 | | reason = "42.0 > 41.9"
12 | | )]
| |______^ expected a tuple with 2 elements, found one with 1 element
|
= note: expected struct `std::marker::PhantomData<(pre::BooleanCondition<"x < 42.1">, pre::BooleanCondition<"x > 41.9">)>`
found struct `std::marker::PhantomData<(pre::BooleanCondition<"x > 41.9">,)>`
稳定编译器错误
error[E0063]: missing field `_boolean_x_20_3c_2042_2e1` in initializer of `foo`
--> src/main.rs:9:6
|
9 | #[assure(
| ______^
10 | | x > 41.9,
11 | | reason = "42.0 > 41.9"
12 | | )]
| |______^ missing `_boolean_x_20_3c_2042_2e1`
此错误表示对调用仅assure
确保了部分先决条件。
要修复此错误,找出您尚未考虑的先决条件并检查它们是否成立。一旦您确信它们成立,您可以使用带有assure
属性的assure
来确保向pre提供,并在reason
中解释,为什么您确信它们成立。您应该在函数的文档中找到函数的先决条件。
夜间编译器错误
error[E0061]: this function takes 1 argument but 2 arguments were supplied
--> src/main.rs:11:5
|
3 | fn foo(x: f32) {}
| -------------- defined here
...
7 | / #[assure(
8 | | x > 41.9,
9 | | reason = "42.0 > 41.9"
10 | | )]
| |______- supplied 2 arguments
11 | foo(42.0);
| ^^^ ----
| |
| expected 1 argument
稳定编译器错误
error[E0574]: expected struct, variant or union type, found function `foo`
--> src/main.rs:7:6
|
7 | #[assure(
| ______^
8 | | x > 41.9,
9 | | reason = "42.0 > 41.9"
10 | | )]
| |______^ not a struct, variant or union type
error[E0061]: this function takes 1 argument but 2 arguments were supplied
--> src/main.rs:11:5
|
3 | fn foo(x: f32) {}
| -------------- defined here
...
7 | #[assure(
| ______-
8 | | x > 41.9,
9 | | reason = "42.0 > 41.9"
10 | | )]
| |______- supplied 2 arguments
11 | foo(42.0);
| ^^^ ----
| |
| expected 1 argument
此错误表示对没有先决条件的函数assure
确保了先决条件。
要修复此错误,可以将将assure
确保的先决条件作为函数的先决条件添加,或者如果您错误地添加了它,则移除assure
属性。
背景
该库是为我的学士学位论文开发的,论文题目为“在Rust中实现和评估unsafe代码的前置通信”(德语)。论文的第二部分重点评估这样的库是否有用,以及其带来的好处是否值得额外的努力。
如果您对这个库有任何反馈,非常感谢您提交问题,因为这有助于我的评估工作。
lib.rs
:
该crate包含pre
crate中使用的属性的实现。
有关更多信息,请参阅pre
crate的文档。
该crate不是为了独立使用而设计的,在没有pre
crate的情况下使用可能不会正常工作。
依赖项
约2MB
约46K SLoC