Attribute Macro pre::forward

#[forward]

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

Currently this attribute does not work by itself. It needs to be used inside of a context that is annotated by a pre attribute.

The purpose of this attribute is to apply the preconditions defined on items in a extern_crate module to the use of the original item.

It is useful if you want to check preconditions for an existing file without making modifications to the file besides adding attributes.

For most use cases, it is better to just use the item inside of the extern_crate module directly. The only case where this attribute is currently absolutely needed, is if you want to check preconditions for functions and methods defined inside of an impl block in an extern_crate attribute.

Examples

Basic usage:

use pre::pre;

#[pre::extern_crate(std)]
mod new_std {
    mod ptr {
        #[pre(valid_ptr(dst, w))]
        unsafe fn write_unaligned<T>(dst: *mut T, src: T);
    }
}

#[pre]
fn main() {
    // Replacing this with `new_std::ptr::write_unaligned` would make the first `forward`
    // attribute below unnecessary.
    use std::ptr::write_unaligned;

    let mut x = 0;

    // No preconditions are checked here.
    unsafe { write_unaligned(&mut x, 1) };

    // Here the actual function being called is `new_std::ptr::write_unaligned`, which checks
    // the preconditions and is otherwise functionally equivalent to
    // `std::ptr::write_unaligned`.
    #[forward(new_std::ptr)]
    #[assure(
        valid_ptr(dst, w),
        reason = "`dst` is created from a reference"
    )]
    unsafe { write_unaligned(&mut x, 2) };

    // Here the `std` segment of the path is replaced with `new_std`, so again
    // `new_std::ptr::write_unaligned` is called.
    // The same effect could be achieved without a `forward` attribute, by replacing the `std`
    // in the path of the call with `new_std`.
    #[forward(std -> new_std)]
    #[assure(
        valid_ptr(dst, w),
        reason = "`dst` is created from a reference"
    )]
    unsafe { std::ptr::write_unaligned(&mut x, 3) };
}

For functions and methods inside of impl blocks, using the forward attribute with the impl keyword inside is necessary to check the preconditions:

use pre::pre;

#[pre::extern_crate(std)]
mod new_std {
    mod ptr {
        impl<T> NonNull<T> {
            #[pre(!ptr.is_null())]
            const unsafe fn new_unchecked(ptr: *mut T) -> NonNull<T>;
        }
    }
}

#[pre]
fn main() {
    let mut val = 0;

    // Even though this uses the `NonNull` type through the `extern_crate` module, this will
    // unfortunately not check the preconditions.
    let non_null = unsafe { new_std::ptr::NonNull::new_unchecked(&mut val) };

    // This call actually checks the preconditions. Note the `impl` keyword before the path
    // below. This is required, so that the preconditions can be properly checked for a
    // function in an `impl` block inside of a `extern_crate` module.
    #[forward(impl new_std::ptr::NonNull)]
    #[assure(
        !ptr.is_null(),
        reason = "a reference is never null"
    )]
    let non_null = unsafe { new_std::ptr::NonNull::new_unchecked(&mut val) };

    // The same thing also works when using the `NonNull` through the `std::ptr` path.
    #[forward(impl new_std::ptr::NonNull)]
    #[assure(
        !ptr.is_null(),
        reason = "a reference is never null"
    )]
    let non_null = unsafe { std::ptr::NonNull::new_unchecked(&mut val) };
}

Syntax

This attribute has three different forms:

• Direct call
• Path replacement
• Impl call

Direct call

#[forward(<path>)]

How it works

<path> is prepended to the path of the annotated call.

Example

#[forward(abc::def)]
ghi::jkl();

becomes

abc::def::ghi::jkl();

Path replacement

#[forward(<old_path> -> <new_path>)]

How it works

<old_path> is replaced with <new_path> in the path of the annotated call.

Example

#[forward(abc -> def)]
abc::ghi::jkl();

becomes

def::ghi::jkl();

Impl call

#[forward(impl <path>)]

How it works

Instead of checking the preconditions on the original method call, the preconditions are checked for a function or method with the same name located at an impl block at <path>. For this to work, the impl block at <path> must be inside of an extern_crate-annotated module.

Example

let v: SomeType<bool> = SomeType::new();

#[forward(impl some_impl::SomeType)]
#[assure(
    <some_condition>,
    reason = <some_reason>
)]
v.some_method(some_arg);

works similar to

let v: SomeType<bool> = SomeType::new();

#[assure(
    <some_condition>,
    reason = <some_reason>
)]
some_impl::SomeType::some_method(); // Does not actually do anything, just checks the
                                    // preconditions.
v.some_method(some_arg);

The exact inner workings of this are different to make it work in more contexts, but this is a good mental model to think about it.