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. 原始函数无法记录先决条件是什么。
2. 使用该函数的程序员可能会忘记查看记录的先决条件。
3. 使用该函数的程序员可能会忽略一个或多个先决条件。如果有多个先决条件记录在单个长段落中，这不太可能发生。
4. 在检查先决条件是否成立时，程序员可能会犯错误。
5. 更新可能会更改函数所需的先决条件，而函数的使用者可能会轻易错过这一事实。
6. 程序员可能会忘记（或选择不）记录调用函数时为什么先决条件成立，这使得后来更改调用或其周围的代码时更容易犯错误。

这个库无法防止所有这些问题，尤其是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块。尽管如此，它们也有自己的限制（见下文）。

  • 仅在夜间版本上才能产生pre的警告。

  • 在夜间版本上，错误可以引用多个位置，提供更好的建议和消息。

• 由于pre通过向函数添加一个额外的参数来工作，它改变了函数签名。这不会在许多情况下产生影响，但如果使用函数指针或将函数作为参数传递，它的类型将与它看起来不同。

• 由于当前稳定编译器不支持对表达式和语句使用属性宏，因此包含assure属性的函数必须至少有一个pre属性，即使它可以为空： #[pre]。

• pre是为2018版设计的。虽然它与2015版也兼容，但如果你还没有，可能需要添加一个extern crate core语句。另外，extern_crate属性在2015版中不受支持。

• 虽然在cfg_attr属性中使用pre的任何属性都可行，但这也存在两个限制：

  • 所有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(...)))]在当前版本中不被pre识别。

• 在用extern_crate属性标注的模块或其父模块中定义的函数和方法存在多个限制：

  • 对这些函数/方法的调用将调用原始类型对应的原始函数/方法，这意味着不会考虑预条件。使用forward属性来检查这些调用上的预条件。
  • 由于它们的实现方式，这些函数的名称可能与它们周围模块中的名称冲突。这种情况在常规使用中不太可能发生，但有可能。如果你遇到这种情况，请提交一个描述问题的issue。
  • 当前，所有类型信息都丢弃了impl块。这意味着多个非重叠（在类型系统意义上）的impl块可以在一个用extern_crate标注的模块中重叠。

理解错误消息

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 属性向 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 属性向 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 代码的先决条件通信的实施和评估”（德语）开发的。论文的第二部分侧重于评估此类库是否有用以及这些好处是否值得额外的努力。

如果您对任何此库的反馈提出问题，我将非常感激，因为这有助于我的评估工作。