Skip to content
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
54 changes: 54 additions & 0 deletions src/implementation/contract.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
/* This Source Code Form is subject to the terms of the Mozilla Public
* License, v. 2.0. If a copy of the MPL was not distributed with this
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */

use proc_macro2::{Ident, TokenStream};
use syn::{
parenthesized,
parse::{Parse, ParseStream},
ItemFn, Token,
};

use crate::implementation::{Contract, ContractType, FuncWithContracts};

pub(crate) fn contract(attr: TokenStream, toks: TokenStream) -> TokenStream {
let clauses = match syn::parse2::<ContractClauses>(attr) {
Ok(clauses) => clauses,
Err(err) => return err.to_compile_error(),
};

let func: ItemFn = syn::parse_quote!(#toks);

FuncWithContracts::new_with_contracts(func, clauses.contracts).generate()
}

struct ContractClauses {
contracts: Vec<Contract>,
}

impl Parse for ContractClauses {
fn parse(input: ParseStream<'_>) -> syn::Result<Self> {
let mut contracts = Vec::new();

while !input.is_empty() {
let ident = input.parse::<Ident>()?;
let ident_str = ident.to_string();
let (ty, mode) = ContractType::contract_type_and_mode(&ident_str).ok_or_else(|| {
syn::Error::new_spanned(&ident, format!("unknown contract clause `{}`", ident_str))
})?;

let content;
parenthesized!(content in input);
let toks = content.parse::<TokenStream>()?;
contracts.push(Contract::from_toks(ty, mode, toks));

if input.is_empty() {
break;
}

input.parse::<Token![,]>()?;
}

Ok(Self { contracts })
}
}
10 changes: 8 additions & 2 deletions src/implementation/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,13 +3,15 @@
* file, You can obtain one at http://mozilla.org/MPL/2.0/. */

pub(crate) mod codegen;
pub(crate) mod contract;
pub(crate) mod doc;
pub(crate) mod ensures;
pub(crate) mod invariant;
pub(crate) mod parse;
pub(crate) mod requires;
pub(crate) mod traits;

pub(crate) use contract::contract;
pub(crate) use ensures::ensures;
pub(crate) use invariant::invariant;
use proc_macro2::{Span, TokenStream};
Expand Down Expand Up @@ -149,17 +151,21 @@ impl FuncWithContracts {
/// The initial contract is parsed from the tokens, others will be read from
/// parsed function.
pub(crate) fn new_with_initial_contract(
mut func: ItemFn,
func: ItemFn,
cty: ContractType,
cmode: ContractMode,
ctoks: TokenStream,
) -> Self {
// add in the first attribute
let mut contracts: Vec<Contract> = {
let contracts: Vec<Contract> = {
let initial_contract = Contract::from_toks(cty, cmode, ctoks);
vec![initial_contract]
};

Self::new_with_contracts(func, contracts)
}

pub(crate) fn new_with_contracts(mut func: ItemFn, mut contracts: Vec<Contract>) -> Self {
// find all other attributes

let contract_attrs = func
Expand Down
24 changes: 24 additions & 0 deletions src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -183,6 +183,30 @@ mod implementation;
use implementation::ContractMode;
use proc_macro::TokenStream;

/// Check multiple contracts with a single attribute.
///
/// This is useful when combining pre-conditions and post-conditions because it
/// avoids stacked attribute expansion ordering.
///
/// ## Example
///
/// ```rust
/// # use contracts::contract;
/// #[contract(
/// requires(x > 0, "x must be positive"),
/// ensures(ret > x),
/// )]
/// fn incr(x: i32) -> i32 {
/// x + 1
/// }
/// ```
#[proc_macro_attribute]
pub fn contract(attr: TokenStream, toks: TokenStream) -> TokenStream {
let attr = attr.into();
let toks = toks.into();
implementation::contract(attr, toks).into()
}

/// Pre-conditions are checked before the function body is run.
///
/// ## Example
Expand Down
10 changes: 6 additions & 4 deletions tests/issues.rs
Original file line number Diff line number Diff line change
Expand Up @@ -55,12 +55,12 @@ fn gl_issue_17() {
}
}

#[deny(unused_imports)]
#[test]
fn gl_issue_18() {
use std::ops::{Div, Mul, Rem, Sub};

// use contracts::ensures; // <- unused warning
use contracts::requires;
use contracts::contract;

trait Zero {
fn zero() -> Self;
Expand All @@ -72,8 +72,10 @@ fn gl_issue_18() {
}
}

#[requires( n != T::zero() || d != T::zero() )]
#[ensures( ret != T::zero() && n % ret == T::zero() && d % ret == T::zero() )]
#[contract(
requires(n != T::zero() || d != T::zero()),
ensures(ret != T::zero() && n % ret == T::zero() && d % ret == T::zero()),
)]
fn euclidean<T>(n: T, d: T) -> T
where
T: Sub<Output = T>
Expand Down
14 changes: 14 additions & 0 deletions tests/ui/pass/combined_contract.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
use contracts::contract;

#[contract(
requires(x >= 0, "input is non-negative"),
ensures(ret >= x),
debug_ensures(ret == x + 1),
)]
fn incr(x: i32) -> i32 {
x + 1
}

fn main() {
assert_eq!(incr(1), 2);
}
Loading