From 04c49d7d4f4348bad77195d677e5c6e17d0c5328 Mon Sep 17 00:00:00 2001 From: Rob Ede Date: Mon, 6 Jul 2026 07:30:13 +0100 Subject: [PATCH] feat: add combined contract attribute --- CHANGELOG.md | 2 ++ src/implementation/contract.rs | 57 ++++++++++++++++++++++++++++++ src/implementation/mod.rs | 10 ++++-- src/lib.rs | 24 +++++++++++++ tests/issues.rs | 10 +++--- tests/ui/pass/combined_contract.rs | 15 ++++++++ 6 files changed, 112 insertions(+), 6 deletions(-) create mode 100644 src/implementation/contract.rs create mode 100644 tests/ui/pass/combined_contract.rs diff --git a/CHANGELOG.md b/CHANGELOG.md index 9f5fbc7..3a10ebd 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), ## Unreleased +- Add a combined `#[contract(...)]` attribute for declaring multiple contracts. + ## 0.6.8 - Reject contract predicates that are the literal `false` at compile time. diff --git a/src/implementation/contract.rs b/src/implementation/contract.rs new file mode 100644 index 0000000..be9a59e --- /dev/null +++ b/src/implementation/contract.rs @@ -0,0 +1,57 @@ +/* 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::{emit_error, Contract, ContractType, FuncWithContracts}; + +pub(crate) fn contract(attr: TokenStream, toks: TokenStream) -> TokenStream { + let clauses = match syn::parse2::(attr) { + Ok(clauses) => clauses, + Err(err) => return err.to_compile_error(), + }; + + let func: ItemFn = match syn::parse2(toks.clone()) { + Ok(func) => func, + Err(err) => return emit_error(err, toks), + }; + + FuncWithContracts::new_with_contracts(func, clauses.contracts).generate() +} + +struct ContractClauses { + contracts: Vec, +} + +impl Parse for ContractClauses { + fn parse(input: ParseStream<'_>) -> syn::Result { + let mut contracts = Vec::new(); + + while !input.is_empty() { + let ident = input.parse::()?; + 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::()?; + contracts.push(Contract::from_toks(ty, mode, toks)); + + if input.is_empty() { + break; + } + + input.parse::()?; + } + + Ok(Self { contracts }) + } +} diff --git a/src/implementation/mod.rs b/src/implementation/mod.rs index 3a5a8c1..6ad7770 100644 --- a/src/implementation/mod.rs +++ b/src/implementation/mod.rs @@ -3,6 +3,7 @@ * 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; @@ -10,6 +11,7 @@ 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}; @@ -157,17 +159,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 = { + let contracts: Vec = { 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) -> Self { // find all other attributes let contract_attrs = func diff --git a/src/lib.rs b/src/lib.rs index de9690c..c2622e3 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -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 diff --git a/tests/issues.rs b/tests/issues.rs index 7054e34..da7ccb1 100644 --- a/tests/issues.rs +++ b/tests/issues.rs @@ -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; @@ -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(n: T, d: T) -> T where T: Sub diff --git a/tests/ui/pass/combined_contract.rs b/tests/ui/pass/combined_contract.rs new file mode 100644 index 0000000..b7468fe --- /dev/null +++ b/tests/ui/pass/combined_contract.rs @@ -0,0 +1,15 @@ +use contracts::contract; + +#[contract( + requires(x >= 0, "input is non-negative"), + debug_invariant(x >= 0), + ensures(ret >= x), + debug_ensures(ret == x + 1), +)] +fn incr(x: i32) -> i32 { + x + 1 +} + +fn main() { + assert_eq!(incr(1), 2); +}