[][src]Crate pre

pre is a library to help programmers correctly uphold preconditions for function calls.

Motivation

Sometimes functions or methods have preconditions that cannot be ensured in the type system and cannot be guarded against at runtime. The most prominent example of functions like that are unsafe functions. When used correctly, unsafe functions are used to "declare the existence of contracts the compiler can't check". These contracts are the preconditions for the function call. Failing to uphold them usually results in a violation of memory safety and undefined behavior.

Currently the most used scheme for dealing with these preconditions on unsafe functions is to mention them in the Safety section of the function's documentation. Programmers using the function then have to check what they have to ensure to call the function correctly. The programmer that uses the function may then leave a comment next to the function, describing why the call is safe (why the preconditions hold).

This approach is even advertised by the compiler (as of 1.44.1) when using an unsafe function outside of an unsafe block:

note: consult the function's documentation for information on how to avoid undefined behavior

There are multiple points of failure with this approach. Among others these are:

  1. The original function could not document what the preconditions are.
  2. The programmer using the function could forget to look at the documented preconditions.
  3. The programmer using the function could overlook one or more of the preconditions. This is not unlikely, if multiple preconditions are documented in a single long paragraph.
  4. The programmer could make a mistake when checking whether the preconditions hold.
  5. An update could change the preconditions that the function requires and users of the function could easily miss that fact.
  6. The programmer could forget (or choose not to) document why the preconditions hold when calling the function, making it easier for others to make a mistake when later changing the call or code around it.

This library cannot guard against all of these problems, especially not against 1 and 4. It however attempts to help against 2, 3, 5 and 6.

The approach

This library works by allowing programmers to specify preconditions on functions they write in a unified format. Those preconditions are then transformed into an additional function argument. Callers of the function then specify the same preconditions at the call site, along with a reason why they believe the precondition is upheld. If the preconditions don't match or are not specified, the function will have invalid arguments and the code will not compile. This should protect against problems 2, 3 and 5 from above. Because a reason is required at the function call site, problem 6 is at least partially guarded against, though programmers could still choose to not put too much effort into the reason.

The signature of the functions is changed by adding a single zero-sized parameter. This means that when compiled using the release mode, there is no run-time cost for these checks. They are a zero-cost abstraction.

Usage

The basic usage for the pre crate looks like this:

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);
}

The pre attribute serves to specify preconditions (on foo) and to enable usage of the assure attribute (on main). To learn why the second usage is necessary, read the paragraph about the checking functionality on the documentation of the pre attribute.

With the assure attribute the programmer assures that the precondition was checked by them and is upheld. Without the assure attribute, the code would fail to compile.

This example deliberately fails to compile
use pre::pre;

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

fn main() {
    foo(42);
//  ^^^^^^^-- this errors
}

The precondition inside the assure attribute must be exactly equal to the precondition inside the pre attribute at the function definition for the code to compile. The order of the preconditions, if there are multiple, does not matter however.

Known Limitations

There are many subtleties involved when working with unsafe code. pre is supposed to help programmers know where to look, but it does not do anything beyond that. The programmer still has to manually check all the contracts of the unsafe code. Therefore even when using pre you should still always check the "Safety" section of the documentation.

There are also some technical limitations to what pre can do:

  • There is more than one form of unsafe code. pre currently exclusively focuses on unsafe functions.

  • While pre does work on the stable compiler, there are quite a few things that only work when using the nightly compiler.

    These are the main differences between the nightly version and the stable version (there are other minor ones):

    • Preconditions on functions in impl blocks only work on nightly.

      This does not apply to impl blocks inside of an extern_crate annotated module. These have their own limitations though (see below).

    • Warnings from pre are only possible on nightly.

    • Errors can reference multiple locations providing better suggestions and messages on nightly.

  • Since pre works by adding an additional argument to a function, it changes the function signature. That won't make a difference in many cases, but if you use function pointers or pass a function as an argument, it will have a different type from what it appears to be.

  • Because attribute macros are not supported for expressions and statements on the current stable compiler, functions that contain an assure attribute must have at least one pre attribute, though it could be empty: #[pre].

  • pre was designed with the 2018 edition in mind. While it does work with the 2015 edition, it may be necessary to add an extern crate core statement, if you don't have one yet. Also the extern_crate attribute is not supported with the 2015 edition.

  • While using any of pre's attributes within a cfg_attr attribute works, there are two limitations to that:

    • All cfg_attr attributes must have the same configuration predicates. The same here means syntactic equality, so all(unix, target_endian = "little") is not the same as all(target_endian = "little", unix). This is done easiest, by simply putting all preconditions behind a single cfg_attr.
    • Nested cfg_attr attributes are not supported, so #[cfg_attr(unix, cfg_attr(target_endian = "little", assure(...)))] is currently not recognized by pre.
  • There are multiple limitations for functions and methods defined in a module which is annotated with the extern_crate attribute or has a parent that is:

    • Calls to such functions/methods call the original function/method for the original type, which means that preconditions are not taken into consideration. Use the forward attribute to check the preconditions on these calls.

    • Because of the way they are implemented, it's currently possible for the name of these functions to clash with names in their surrounding module. This is unlikely to occur in regular usage, but possible. If you encounter such a case, please open an issue describing the problem.

    • Currently all type information for the impl block is discarded. This means that multiple non-overlapping (in the type system sense) impl blocks can overlap in an extern_crate annotated module.

      This example deliberately fails to compile
      mod a {
          pub(crate) struct X<T>(T);
      
          impl X<bool> {
              pub(crate) fn foo() {}
          }
      
          impl X<()> {
              pub(crate) fn foo() {}
          }
      }
      
      #[pre::extern_crate(crate::a)]
      mod b {
          impl X<bool> {
              fn foo();
          }
      
          impl X<()> {
              fn foo();
          }
      }

Understanding the error messages

pre tries to be as helpful as possible in the error messages it gives. Unfortunately in some cases pre does not have enough information to generate an error by itself, but has to rely on rustc to do so later in the compilation. pre has very limited control over what these messages look like.

If you have trouble understanding these error messages, here is a little overview what they look like and what they mean:


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

This error means that the function has preconditions, but they are not assured.

To fix this error, find out what preconditions for the function are and whether they hold. Once you're convinced that they hold, you can assure that to pre with an assure attribute and explain in the reason, why you're sure that they hold. You should be able to find the function preconditions in the documentation for the function.


nightly compiler error

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">,)>`

stable compiler error

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`

This error means that the preconditions that were assured at the call site were different from the preconditions at the function definition.

Unfortunately the stable compiler error is not very readable for symbol heavy preconditions. If have trouble reading these error messages, it is recommended to use the nightly compiler to fix these errors. Once they are fixed, you can continue using the stable compiler.

To fix this error, make sure that all assured preconditions match the preconditions on the function exactly. Also when making changes to the assured preconditions, make sure that they still hold. You should be able to find the function preconditions in the documentation for the function.


nightly compiler error

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">,)>`

stable compiler error

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`

This error means that some, but not all, preconditions were assured for a call.

To fix this error, find out what preconditions you didn't consider yet and check whether they hold. Once you're convinced that they hold, you can assure that to pre with an assure attribute and explain in the reason, why you're sure that they hold. You should be able to find the function preconditions in the documentation for the function.


nightly compiler error

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

stable compiler error

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

This error means that one or more preconditions were assured for a function that does not have any preconditions.

To fix this error, either add the assured preconditions as preconditions to the function or remove the assure attribute, if you added it in error.

Wording of preconditions

While you can write any text you like in a custom precondition, it is recommended to word them in a way that makes sense at both the definition and the call site.

Therefore it is recommended not to write how things should be, but rather how they are when everything is going well.

"the elements at old_len..new_len must be initialized"

should instead be written as

"the elements at old_len..new_len are initialized"

Feature flags

If you're planning on using pre in a library, you should consider how the increased compile time might affect your users. If you're planning on making the preconditions part of your public API there is not really a way around that.

If you're only using the preconditions internally to check the correctness of your implementation however, you can add pre as a dev-dependency and perform all those checks behind a cfg_attr. This would not affect users of your library at all.

Here is an example of that:

# Cargo.toml

[dev-dependencies]
pre = "<latest version>"
/* src/lib.rs */

#[cfg(test)]
use pre::pre;

#[cfg_attr(
    test,
    pre("your first condition"),
    pre("your second condition")
)]
fn some_non_pub_fn() {}

#[cfg_attr(
    test,
    pre
)]
pub fn some_pub_fn() {
    #[cfg_attr(
        test,
        assure(
            "your first condition",
            reason = "your reason"
        ),
        assure(
            "your second condition",
            reason = "your reason"
        )
    )]
    some_non_pub_fn();
}

Changing an existing code base to use pre

One problem when changing a code base to use pre is that once a function has preconditions, it needs them assured everywhere. For functions that are used a lot, it can be a big task to check and assure all call sites at once.

There are two ways to work around that, though one is currently only supported on the nightly compiler.

extern_crate for local items

Suppose you have a function some_module::some_fn with a lot of uses that you want to change to use pre without changing all call sites at once.

mod some_module {
    pub(crate) unsafe fn some_fn() {
        /* ... */
    }
}

fn main() {
    use some_module::some_fn;

    // Lots of uses
    unsafe {
        some_fn();
        some_fn();
    }
}

You can use the extern_crate attribute to create a version of some_fn with preconditions.

use pre::pre;

mod some_module {
    pub(crate) unsafe fn some_fn() {
        /* ... */
    }
}

#[pre::extern_crate(crate::some_module)]
mod pre_some_module {
    #[pre("some condition")]
    unsafe fn some_fn();
}

#[pre]
fn main() {
    use some_module::some_fn;

    unsafe {
        // Checks the preconditions of the function.
        #[forward(pre_some_module)]
        #[assure(
            "some condition",
            reason = "the reason you know the condition is true"
        )]
        some_fn();

        // Does not check any preconditions as before the modifications.
        some_fn();
    }
}

When you've converted all call sites and you're ready to fully convert the function, you can simply add the preconditions to the original function and remove the forward attributes.

use pre::pre;

mod some_module {
    use pre::pre;

    #[pre("some condition")]
    pub(crate) unsafe fn some_fn() {
        /* ... */
    }
}

#[pre]
fn main() {
    use some_module::some_fn;

    unsafe {
        #[assure(
            "some condition",
            reason = "the reason you know the condition is true"
        )]
        some_fn();

        #[assure(
            "some condition",
            reason = "the (possibly other) reason you know the condition is true"
        )]
        some_fn();
    }
}

"TODO" as a reason

This paragraph only applies if you use the nightly compiler, because it depends on the proc_macro_diagnostic feature.

Using "TODO" as a reason in an assure attribute will issue a warning, to remind you of checking why you believe the precondition holds.

When changing a function to use pre, you can simply assure all its preconditions at all call sites with "TODO" as the reason. Of course this does not make the use of the function any safer by itself. However it allows everything to compile again and have the compiler warnings remind you what you need to assure still.

Because the warnings only work on the nightly compiler, usage of "TODO" as a reason is discouraged when using the stable compiler.

Modules

alloc

Precondition definitions for unsafe functions in the alloc library.

core

Precondition definitions for unsafe functions in the core library.

std

Precondition definitions for unsafe functions in the std library.

Attribute Macros

assure

Assure that a precondition holds.

extern_crate

Provide preconditions for items in a different crate.

forward

Forward the call to a different function that has the preconditions for the original function.

pre

Specify preconditions on functions and check that they are assured correctly for calls.