Try   HackMD

Experimental Contract Attributes

The MCP-759 proposed the addition of experimental unstable attributes for behaviorial specification, and intrinsics for enabling better tools to validate and verify those specifications.

The goal is to eventually enable Rust, as a language, to allow users to write specifications in formal code-like language. More details can be found in the MCP-759.

Initial Implementation

In the PR #128045, we are introducing a simple form of #[contracts::requires] and #[contracts::ensures], while PR #138374 adds support for contract in constant functions.

While requires expects a side-effect free boolean expression, the ensures expects a side-effect free closure definition that takes the reference to the function return value.

For example, a developer could annotate NonNull methods with the following safety contracts:

#![feature(contracts)]
extern crate core;
use core::contracts;

impl<T: ?Sized> NonNull<T> {
    #[contracts::requires(!ptr.is_null())]
    pub const unsafe fn new_unchecked(ptr: *mut T) -> Self {
        // SAFETY: the caller must guarantee that `ptr` is non-null.
        unsafe {
            NonNull { pointer: ptr as _ }
        }
    }

    #[contracts::ensures(|new_ptr| !new_ptr.is_null())]
    pub const fn as_ptr(self) -> *mut T {
        self.pointer as *mut T
    }
}

A user can optionally turn the contract into runtime checks executed before and after the function annotated with contract has been called.

Additionally, other verification tools can be used in order to check the annotated contracts.

Compilation Stages

In order to turn the contract annotations into runtime checks, we have implemented the following changes.

  1. Built-in Macro: The requires and ensures were implemented as builtin macros that expands the function signature by adding a rustc_contracts_requires and rustc_contracts_ensures clauses respectively, both containing a closure definition.
    The NonNull methods signature from the example above would be expanded to the following in this stage:
    pub const unsafe fn new_unchecked(ptr: *mut T) -> Self
        rustc_contract_requires(|| !ptr.is_null())
    { /* body */ }

    pub const fn as_ptr(self) -> *mut T
        rustc_contract_ensures(|new_ptr| !new_ptr.is_null())
    { /* body */ }
  1. AST Extension: The parser was extended to accept optional rustc_contracts_requires and rustc_contracts_ensures clauses, and store them as part of the function AST node.
    This change to the syntax is perma-unstable. It can be enabled via rustc_contracts_internals unstable feature.
  2. AST Lowering:
    a. Contract closures: During body lowering, the contract clauses lowered to become closures in the function prelude. For the ensures closure, the compile will inject a call to build_check_ensures with the ensures closure to help with type inference.
    b. Requires check: Also in the function prelude, the compiler will inject a call to the new intrinsic contract_check_requires to check the requires closure.
    b. Ensures check: The compiler will insert a call to contract_check_ensures intrinsics at every function return point, as well as at the end of the function.

The NonNull examples above will look like[1] the following after all these stages:

    const unsafe fn new_unchecked(ptr: *mut T) -> Self {
        contract_check_requires(|| !ptr.is_null());
        {
            // SAFETY: the caller must guarantee that `ptr` is non-null.
            unsafe { NonNull{ pointer: ptr as _,} }
        }
    }

    const fn as_ptr(self) -> *mut T {
        let __ensures_checker = contract_build_check_ensures(|new_ptr| !new_ptr.is_null());
        contract_check_ensures({ self.pointer as *mut T }, __ensures_checker)
    }

Feature gates

We have added two feature gates to contracts:

  1. rustc_contracts: Enables the usage of contract attributes.
  2. rustc_contracts_internal: Perma-unstable attribute that enables the explicit usage of the extended signature with contract clauses.

We have also added a new configuration: contract_checks to enable the usage of #[cfg(contract_checks) to check if contract checks are enabled.

Command arguments

We have added a new unstable argument -Zcontract-checks=[yes|no] that allows users to enable / disable the runtime checks. The behavior of this feature is similar to -Zub_checks.

New Intrinsics

We are introducing 3 new intrinsics in this PR.

  1. contract_checks: Returns whether contract's runtime checks have been enabled.
  2. contract_check_requires / contract_check_ensures : Invoke the contract closure to check whether the specification holds.

Limitations

Built-in Macro

The current implementation of the contracts built-in macros is rather fragile. We couldn't implement a more robust solution with the existing macro infrastructure.

The contract macros differ from all the existing attributes like built-in macros.
The input for contracts macro is an arbitrary expression, while existing macros accept a restricted AST as an input (MetaItem).

Expand this for more background on existing implementation.

There are two different ways to define attribute macros in the Rust compiler today:

  1. Attr: A token-based attribute macro. It takes two TokenStream as input, the annotated item, and the content of the attribute. It should produce a new TokenStream for the item.
  2. LegacyAttr: An AST-based attribute macro. It takes a MetaItem and an Annotable item as input representing the content of the attribute and the annotated item. Note that MetaItem is restricted It produces one or more Annotable as a result.
    All the attributes like built-in macros defined in the Rust compiler today implement the this variant.

However, for contracts, the input for the macro is an arbitrary expression. Thus, we had to use the Attr trait.

/// A syntax extension kind.
pub enum SyntaxExtensionKind {
    /// A token-based attribute macro.
    Attr(
        /// An expander with signature (TokenStream, TokenStream) -> TokenStream.
        /// The first TokenStream is the attribute itself, the second is the annotated item.
        /// The produced TokenStream replaces the input TokenStream.
        Box<dyn AttrProcMacro + sync::DynSync + sync::DynSend>,
    ),

    /// An AST-based attribute macro.
    LegacyAttr(
        /// An expander with signature (AST, AST) -> AST.
        /// The first AST fragment is the attribute itself, the second is the annotated item.
        /// The produced AST fragment replaces the input AST fragment.
        Box<dyn MultiItemModifier + sync::DynSync + sync::DynSend>,
    ),
    
    /* .. */
}

/// Trait used by the `Attr` variant.
pub trait AttrProcMacro {
    fn expand<'cx>(
        &self,
        ecx: &'cx mut ExtCtxt<'_>,
        span: Span,
        annotation: TokenStream,
        annotated: TokenStream,
    ) -> Result<TokenStream, ErrorGuaranteed>;
}

/// Trait used by the `LegacyAttr` variant.
pub trait MultiItemModifier {
    /// `meta_item` is the attribute, and `item` is the item being modified.
    fn expand(
        &self,
        ecx: &mut ExtCtxt<'_>,
        span: Span,
        meta_item: &ast::MetaItem,
        item: Annotatable,
        is_derive_const: bool,
    ) -> ExpandResult<Vec<Annotatable>, Annotatable>;
}

We couldn't leverage the Parser either. We were able to use the Parser to retrieve the annotated item, and inject the contract expression in the item, however, there is no easy way to convert the modified AST item back to TokenStream. Calls to TokenStream::from_ast would result in the original TokenStream, and the contract clauses would be lost.

Ideally we should extend the attribute expander to support a TokenStream annotation atop an AST annotated item, so that it would again be trivial to inject the attribute payload into an unambiguous spot in the AST.

Target Functions

In this initial implementation, contracts can only be attached to functions that have a body, excluding foreign functions, many intrinsics and trait declarations.

We would likely to eventually remove that restriction, but it will require redesigning the contract instrumentation. We would also need to decide how to encode the contract check. We could for example add the instrumentation in the callee body.

Alternative Solutions

Initially, we tried to make contract a new hir element, such as a closure, but that required changes to every stage of IR lowering, and we couldn't get a working solution in a reasonable timeline for start early experimentation.

That said, the existing solution is not the one that we are planning to stabilize, and we are currently exploring a more robust solution that would replace the contract AST lowering. One possibility would be to replace the contract instrumentation with a MIR pass.

Future work

  1. Add interface for external tools to retrieve the contract specification.
  2. Improve the existing architecture.
  3. Annotate the standard library with contracts.
    a. Relationship between ub_checks and contracts.
  4. Add support for type invariant.
  5. Add more tests + improve implementation.
  6. Improve error handling and diagnostic messages.
  7. Potential changes to the contract annotation syntax:
    a. Safety vs correctness vs panic freedom
    b. Contract stability

Questions

Please feel free to add any questions you might have

  1. The code below was extracted with -Zunpretty=hir and edited for clarity. ↩︎

Last changed by 
 
Celina G. Val
1
174
Published on HackMD