From 030a65f44abdef56809fbd69cd70426b41479027 Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Sun, 21 Sep 2025 19:03:29 +0900 Subject: [PATCH 01/17] refactor to support multiple backends --- Cargo.toml | 1 + .../anodized-core/src/backend/anodized/mod.rs | 139 +++++++++++++++++ .../anodized}/test_instrument_fn.rs | 0 crates/anodized-core/src/backend/mod.rs | 40 +++++ crates/anodized-core/src/lib.rs | 140 +----------------- crates/anodized/Cargo.toml | 1 + crates/anodized/src/lib.rs | 69 ++++----- 7 files changed, 209 insertions(+), 181 deletions(-) create mode 100644 crates/anodized-core/src/backend/anodized/mod.rs rename crates/anodized-core/src/{ => backend/anodized}/test_instrument_fn.rs (100%) create mode 100644 crates/anodized-core/src/backend/mod.rs diff --git a/Cargo.toml b/Cargo.toml index 7481d877..aa64b97f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -19,3 +19,4 @@ anodized-core = { version = "0.2.1", path = "crates/anodized-core" } proc-macro2 = "1.0" quote = "1.0" syn = { version = "2.0", features = ["extra-traits", "full"] } +rustversion = "1.0" diff --git a/crates/anodized-core/src/backend/anodized/mod.rs b/crates/anodized-core/src/backend/anodized/mod.rs new file mode 100644 index 00000000..02b912ae --- /dev/null +++ b/crates/anodized-core/src/backend/anodized/mod.rs @@ -0,0 +1,139 @@ +#[cfg(test)] +mod test_instrument_fn; + +use crate::Spec; + +use proc_macro2::{Span, TokenStream as TokenStream2}; +use quote::{ToTokens, quote}; +use syn::{Block, Ident, Meta, parse::Result, parse_quote}; + +/// Takes the spec and the original body and returns a new instrumented function body. +pub fn instrument_fn_body( + spec: &Spec, + original_body: &Block, + is_async: bool, + return_type: &syn::Type, + disable_runtime_checks: bool, +) -> Result { + // The identifier for the return value binding. + let output_ident = Ident::new("__anodized_output", Span::mixed_site()); + + // --- Generate Precondition Checks --- + let guard_assert = |assert_stmt: TokenStream2, cfg: Option<&Meta>| { + if disable_runtime_checks { + quote! { if false { #assert_stmt } } + } else if let Some(cfg) = cfg { + quote! { if cfg!(#cfg) { #assert_stmt } } + } else { + assert_stmt + } + }; + + let preconditions = spec + .requires + .iter() + .map(|condition| { + let expr = &condition.expr; + let expr_str = expr.to_token_stream().to_string(); + let assert = quote! { assert!(#expr, "Precondition failed: {}", #expr_str); }; + guard_assert(assert, condition.cfg.as_ref()) + }) + .chain(spec.maintains.iter().map(|condition| { + let expr = &condition.expr; + let expr_str = expr.to_token_stream().to_string(); + let assert = quote! { assert!(#expr, "Pre-invariant failed: {}", #expr_str); }; + guard_assert(assert, condition.cfg.as_ref()) + })); + + // --- Generate Combined Body and Capture Statement --- + // Capture values and execute body in a single tuple assignment + // This ensures captured values aren't accessible to the body itself + + // Chain capture aliases with output binding + let aliases = spec + .captures + .iter() + .map(|cb| &cb.alias) + .chain(std::iter::once(&output_ident)); + + // Chain capture expressions with body expression + let capture_exprs = spec.captures.iter().map(|cb| { + let expr = &cb.expr; + quote! { #expr } + }); + + // Chain underscore types with return type for tuple type annotation + let types = spec + .captures + .iter() + .map(|_| quote! { _ }) + .chain(std::iter::once(quote! { #return_type })); + + let body_expr = if is_async { + quote! { async #original_body.await } + } else { + quote! { #original_body } + }; + + let exprs = capture_exprs.chain(std::iter::once(body_expr)); + + // Build tuple assignment with type annotation on the tuple + let body_and_captures = quote! { + let (#(#aliases),*): (#(#types),*) = (#(#exprs),*); + }; + + // --- Generate Postcondition Checks --- + let postconditions = spec + .maintains + .iter() + .map(|condition| { + let expr = &condition.expr; + let expr_str = expr.to_token_stream().to_string(); + let assert = quote! { assert!(#expr, "Post-invariant failed: {}", #expr_str); }; + guard_assert(assert, condition.cfg.as_ref()) + }) + .chain(spec.ensures.iter().map(|postcondition| { + let closure = annotate_postcondition_closure_argument( + postcondition.closure.clone(), + return_type.clone(), + ); + let closure_str = postcondition.closure.to_token_stream().to_string(); + + let assert = quote! { + assert!((#closure)(&#output_ident), "Postcondition failed: {}", #closure_str); + }; + guard_assert(assert, postcondition.cfg.as_ref()) + })); + + Ok(parse_quote! { + { + #(#preconditions)* + #body_and_captures + #(#postconditions)* + #output_ident + } + }) +} + +fn annotate_postcondition_closure_argument( + mut closure: syn::ExprClosure, + return_type: syn::Type, +) -> syn::ExprClosure { + // Add type annotation: convert |param| to |param: &ReturnType|. + if let Some(first_input) = closure.inputs.first_mut() { + // Wrap the pattern with a type annotation + let pattern = first_input.clone(); + *first_input = syn::Pat::Type(syn::PatType { + attrs: vec![], + pat: Box::new(pattern), + colon_token: Default::default(), + ty: Box::new(syn::Type::Reference(syn::TypeReference { + and_token: Default::default(), + lifetime: None, + mutability: None, + elem: Box::new(return_type), + })), + }); + } + closure +} diff --git a/crates/anodized-core/src/test_instrument_fn.rs b/crates/anodized-core/src/backend/anodized/test_instrument_fn.rs similarity index 100% rename from crates/anodized-core/src/test_instrument_fn.rs rename to crates/anodized-core/src/backend/anodized/test_instrument_fn.rs diff --git a/crates/anodized-core/src/backend/mod.rs b/crates/anodized-core/src/backend/mod.rs new file mode 100644 index 00000000..6b07dac2 --- /dev/null +++ b/crates/anodized-core/src/backend/mod.rs @@ -0,0 +1,40 @@ +pub mod anodized; + +use syn::ItemFn; + +use crate::Spec; + +#[derive(Copy, Clone, Debug, Eq, PartialEq)] +pub enum Backend { + Default, + NoChecks, + NightlyContracts, +} + +pub fn handle_fn(backend: Backend, spec: Spec, mut func: ItemFn) -> syn::Result { + let is_async = func.sig.asyncness.is_some(); + + // Extract the return type from the function signature + let return_type = match &func.sig.output { + syn::ReturnType::Default => syn::parse_quote!(()), + syn::ReturnType::Type(_, ty) => ty.as_ref().clone(), + }; + + // Generate the new, instrumented function body. + let disable_runtime_checks = backend != Backend::Default; + let new_body = anodized::instrument_fn_body( + &spec, + &func.block, + is_async, + &return_type, + disable_runtime_checks, + )?; + + // Replace the old function body with the new one. + *func.block = new_body; + + match backend { + Backend::Default | Backend::NoChecks => Ok(func), + Backend::NightlyContracts => todo!(), + } +} diff --git a/crates/anodized-core/src/lib.rs b/crates/anodized-core/src/lib.rs index 28daef1b..d8ea1763 100644 --- a/crates/anodized-core/src/lib.rs +++ b/crates/anodized-core/src/lib.rs @@ -2,11 +2,11 @@ //! #![doc = include_str!("../README.md")] +pub mod backend; + use proc_macro2::Span; -use proc_macro2::TokenStream as TokenStream2; -use quote::{ToTokens, quote}; use syn::{ - Attribute, Block, Expr, Ident, Meta, Pat, Token, + Attribute, Expr, Ident, Meta, Pat, Token, parse::{Parse, ParseStream, Result}, parse_quote, punctuated::Punctuated, @@ -407,142 +407,8 @@ mod kw { syn::custom_keyword!(ensures); } -/// Takes the spec and the original body and returns a new instrumented function body. -pub fn instrument_fn_body( - spec: &Spec, - original_body: &Block, - is_async: bool, - return_type: &syn::Type, - disable_runtime_checks: bool, -) -> Result { - // The identifier for the return value binding. - let output_ident = Ident::new("__anodized_output", Span::mixed_site()); - - // --- Generate Precondition Checks --- - let guard_assert = |assert_stmt: TokenStream2, cfg: Option<&Meta>| { - if disable_runtime_checks { - quote! { if false { #assert_stmt } } - } else if let Some(cfg) = cfg { - quote! { if cfg!(#cfg) { #assert_stmt } } - } else { - assert_stmt - } - }; - - let preconditions = spec - .requires - .iter() - .map(|condition| { - let expr = &condition.expr; - let expr_str = expr.to_token_stream().to_string(); - let assert = quote! { assert!(#expr, "Precondition failed: {}", #expr_str); }; - guard_assert(assert, condition.cfg.as_ref()) - }) - .chain(spec.maintains.iter().map(|condition| { - let expr = &condition.expr; - let expr_str = expr.to_token_stream().to_string(); - let assert = quote! { assert!(#expr, "Pre-invariant failed: {}", #expr_str); }; - guard_assert(assert, condition.cfg.as_ref()) - })); - - // --- Generate Combined Body and Capture Statement --- - // Capture values and execute body in a single tuple assignment - // This ensures captured values aren't accessible to the body itself - - // Chain capture aliases with output binding - let aliases = spec - .captures - .iter() - .map(|cb| &cb.alias) - .chain(std::iter::once(&output_ident)); - - // Chain capture expressions with body expression - let capture_exprs = spec.captures.iter().map(|cb| { - let expr = &cb.expr; - quote! { #expr } - }); - - // Chain underscore types with return type for tuple type annotation - let types = spec - .captures - .iter() - .map(|_| quote! { _ }) - .chain(std::iter::once(quote! { #return_type })); - - let body_expr = if is_async { - quote! { async #original_body.await } - } else { - quote! { #original_body } - }; - - let exprs = capture_exprs.chain(std::iter::once(body_expr)); - - // Build tuple assignment with type annotation on the tuple - let body_and_captures = quote! { - let (#(#aliases),*): (#(#types),*) = (#(#exprs),*); - }; - - // --- Generate Postcondition Checks --- - let postconditions = spec - .maintains - .iter() - .map(|condition| { - let expr = &condition.expr; - let expr_str = expr.to_token_stream().to_string(); - let assert = quote! { assert!(#expr, "Post-invariant failed: {}", #expr_str); }; - guard_assert(assert, condition.cfg.as_ref()) - }) - .chain(spec.ensures.iter().map(|postcondition| { - let closure = annotate_postcondition_closure_argument( - postcondition.closure.clone(), - return_type.clone(), - ); - let closure_str = postcondition.closure.to_token_stream().to_string(); - - let assert = quote! { - assert!((#closure)(&#output_ident), "Postcondition failed: {}", #closure_str); - }; - guard_assert(assert, postcondition.cfg.as_ref()) - })); - - Ok(parse_quote! { - { - #(#preconditions)* - #body_and_captures - #(#postconditions)* - #output_ident - } - }) -} - -fn annotate_postcondition_closure_argument( - mut closure: syn::ExprClosure, - return_type: syn::Type, -) -> syn::ExprClosure { - // Add type annotation: convert |param| to |param: &ReturnType|. - if let Some(first_input) = closure.inputs.first_mut() { - // Wrap the pattern with a type annotation - let pattern = first_input.clone(); - *first_input = syn::Pat::Type(syn::PatType { - attrs: vec![], - pat: Box::new(pattern), - colon_token: Default::default(), - ty: Box::new(syn::Type::Reference(syn::TypeReference { - and_token: Default::default(), - lifetime: None, - mutability: None, - elem: Box::new(return_type), - })), - }); - } - closure -} - #[cfg(test)] mod test_parse_spec; -#[cfg(test)] -mod test_instrument_fn; - #[cfg(test)] mod test_util; diff --git a/crates/anodized/Cargo.toml b/crates/anodized/Cargo.toml index a229947c..17c842d2 100644 --- a/crates/anodized/Cargo.toml +++ b/crates/anodized/Cargo.toml @@ -15,6 +15,7 @@ proc-macro = true [features] backend-no-checks = [] +backend-nightly-contracts = [] [dependencies] anodized-core.workspace = true diff --git a/crates/anodized/src/lib.rs b/crates/anodized/src/lib.rs index c54b6f64..8fbefd45 100644 --- a/crates/anodized/src/lib.rs +++ b/crates/anodized/src/lib.rs @@ -4,24 +4,27 @@ use proc_macro::TokenStream; use quote::ToTokens; -use syn::{Item, ItemFn, parse_macro_input}; +use syn::{Item, parse_macro_input}; -use anodized_core::{Spec, instrument_fn_body}; - -#[derive(Copy, Clone, Debug, Eq, PartialEq)] -enum Backend { - Default, - NoChecks, -} +use anodized_core::{ + Spec, + backend::{Backend, handle_fn}, +}; const _: () = { - let count: u32 = cfg!(feature = "backend-no-checks") as u32; + let count: u32 = cfg!(feature = "backend-no-checks") as u32 + + cfg!(feature = "backend-nightly-contracts") as u32; if count > 1 { panic!("anodized: backend features are mutually exclusive"); } }; -const BACKEND: Backend = if cfg!(feature = "backend-no-checks") { +#[cfg(all(feature = "backend-nightly-contracts", not(nightly)))] +compile_error!("the `backend-nightly-contracts` feature requires a nightly Rust toolchain"); + +const BACKEND: Backend = if cfg!(feature = "backend-nightly-contracts") { + Backend::NightlyContracts +} else if cfg!(feature = "backend-no-checks") { Backend::NoChecks } else { Backend::Default @@ -36,49 +39,27 @@ pub fn spec(args: TokenStream, input: TokenStream) -> TokenStream { // Parse the item to which the attribute is attached. let item = parse_macro_input!(input as Item); - match item { - Item::Fn(func) => handle_fn(args, func), - item => { - let item_type = item_to_string(&item); + let result = match item { + Item::Fn(func) => { + let spec = parse_macro_input!(args as Spec); + handle_fn(BACKEND, spec, func) + } + unsupported_item => { + let item_type = item_to_string(&unsupported_item); let msg = format!( r#"The `#[spec]` attribute doesn't yet support this item: `{}`. If this is a problem for your use case, please open a feature request at https://github.com/mkovaxx/anodized/issues/new"#, item_type ); - syn::Error::new_spanned(item, msg).to_compile_error().into() + Err(syn::Error::new_spanned(unsupported_item, msg)) } - } -} - -fn handle_fn(args: TokenStream, mut func: ItemFn) -> TokenStream { - let spec = parse_macro_input!(args as Spec); - let is_async = func.sig.asyncness.is_some(); - - // Extract the return type from the function signature - let return_type = match &func.sig.output { - syn::ReturnType::Default => syn::parse_quote!(()), - syn::ReturnType::Type(_, ty) => ty.as_ref().clone(), }; - // Generate the new, instrumented function body. - let disable_runtime_checks = matches!(BACKEND, Backend::NoChecks); - let new_body = match instrument_fn_body( - &spec, - &func.block, - is_async, - &return_type, - disable_runtime_checks, - ) { - Ok(body) => body, - Err(e) => return e.to_compile_error().into(), - }; - - // Replace the old function body with the new one. - *func.block = new_body; - - // Return the modified function. - func.into_token_stream().into() + match result { + Ok(item) => item.into_token_stream().into(), + Err(e) => e.to_compile_error().into(), + } } fn item_to_string(item: &Item) -> &str { From 0eb4bac1068357dec67f71e5077d22c88b8c4bad Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Sun, 21 Sep 2025 19:10:35 +0900 Subject: [PATCH 02/17] introduce backend nightly_contracts --- crates/anodized-core/src/backend/mod.rs | 3 ++- .../anodized-core/src/backend/nightly_contracts/mod.rs | 10 ++++++++++ 2 files changed, 12 insertions(+), 1 deletion(-) create mode 100644 crates/anodized-core/src/backend/nightly_contracts/mod.rs diff --git a/crates/anodized-core/src/backend/mod.rs b/crates/anodized-core/src/backend/mod.rs index 6b07dac2..0196a731 100644 --- a/crates/anodized-core/src/backend/mod.rs +++ b/crates/anodized-core/src/backend/mod.rs @@ -1,4 +1,5 @@ pub mod anodized; +pub mod nightly_contracts; use syn::ItemFn; @@ -35,6 +36,6 @@ pub fn handle_fn(backend: Backend, spec: Spec, mut func: ItemFn) -> syn::Result< match backend { Backend::Default | Backend::NoChecks => Ok(func), - Backend::NightlyContracts => todo!(), + Backend::NightlyContracts => nightly_contracts::instrument_fn(&spec, func), } } diff --git a/crates/anodized-core/src/backend/nightly_contracts/mod.rs b/crates/anodized-core/src/backend/nightly_contracts/mod.rs new file mode 100644 index 00000000..4bcbed1f --- /dev/null +++ b/crates/anodized-core/src/backend/nightly_contracts/mod.rs @@ -0,0 +1,10 @@ +use crate::Spec; + +use proc_macro2::{Span, TokenStream as TokenStream2}; +use quote::{ToTokens, quote}; +use syn::{Block, Ident, ItemFn, Meta, parse::Result, parse_quote}; + +/// Takes the spec and the original function and returns a new instrumented function. +pub fn instrument_fn(spec: &Spec, original_fn: ItemFn) -> Result { + todo!() +} From c152abfeb529dad27f219627382302ce90422137 Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Sun, 21 Sep 2025 22:32:35 +0900 Subject: [PATCH 03/17] add nightly_contracts backend and unit tests --- .../src/backend/nightly_contracts/mod.rs | 67 ++++++++- .../src/backend/nightly_contracts/tests.rs | 133 ++++++++++++++++++ crates/anodized/Cargo.toml | 1 + crates/anodized/src/lib.rs | 3 +- 4 files changed, 197 insertions(+), 7 deletions(-) create mode 100644 crates/anodized-core/src/backend/nightly_contracts/tests.rs diff --git a/crates/anodized-core/src/backend/nightly_contracts/mod.rs b/crates/anodized-core/src/backend/nightly_contracts/mod.rs index 4bcbed1f..070e901a 100644 --- a/crates/anodized-core/src/backend/nightly_contracts/mod.rs +++ b/crates/anodized-core/src/backend/nightly_contracts/mod.rs @@ -1,10 +1,65 @@ +#[cfg(test)] +mod tests; + use crate::Spec; -use proc_macro2::{Span, TokenStream as TokenStream2}; -use quote::{ToTokens, quote}; -use syn::{Block, Ident, ItemFn, Meta, parse::Result, parse_quote}; +use syn::{Error, Expr, ExprClosure, ItemFn, Result, parse_quote}; + +/// Takes the spec and the original function and returns the instrumented function. +pub fn instrument_fn(spec: &Spec, mut func: ItemFn) -> Result { + if let Some(capture) = spec.captures.first() { + return Err(Error::new_spanned( + &capture.expr, + "`captures` are not supported by the nightly contracts backend", + )); + } + + let mut attrs = Vec::new(); + + for condition in &spec.requires { + let expr = &condition.expr; + + let attr = if let Some(cfg) = &condition.cfg { + parse_quote! { #[cfg_attr(#cfg, contracts::requires(#expr))] } + } else { + parse_quote! { #[contracts::requires(#expr)] } + }; + + attrs.push(attr); + } + + for condition in &spec.maintains { + let expr = &condition.expr; + + let requires_attr = if let Some(cfg) = &condition.cfg { + parse_quote! { #[cfg_attr(#cfg, contracts::requires(#expr))] } + } else { + parse_quote! { #[contracts::requires(#expr)] } + }; + attrs.push(requires_attr); + + let ensures_closure: Expr = parse_quote! { |_| #expr }; + let ensures_attr = if let Some(cfg) = &condition.cfg { + parse_quote! { #[cfg_attr(#cfg, contracts::ensures(#ensures_closure))] } + } else { + parse_quote! { #[contracts::ensures(#ensures_closure)] } + }; + attrs.push(ensures_attr); + } + + for postcondition in &spec.ensures { + let closure: ExprClosure = postcondition.closure.clone(); + + let attr = if let Some(cfg) = &postcondition.cfg { + parse_quote! { #[cfg_attr(#cfg, contracts::ensures(#closure))] } + } else { + parse_quote! { #[contracts::ensures(#closure)] } + }; + attrs.push(attr); + } + + attrs.extend(func.attrs); + func.attrs = attrs; -/// Takes the spec and the original function and returns a new instrumented function. -pub fn instrument_fn(spec: &Spec, original_fn: ItemFn) -> Result { - todo!() + Ok(func) } diff --git a/crates/anodized-core/src/backend/nightly_contracts/tests.rs b/crates/anodized-core/src/backend/nightly_contracts/tests.rs new file mode 100644 index 00000000..91b07510 --- /dev/null +++ b/crates/anodized-core/src/backend/nightly_contracts/tests.rs @@ -0,0 +1,133 @@ +use super::*; + +use quote::ToTokens; +use syn::{Attribute, ItemFn, parse_quote}; + +fn assert_attr_eq(actual: &Attribute, expected: &Attribute) { + assert_eq!( + actual.to_token_stream().to_string(), + expected.to_token_stream().to_string() + ); +} + +#[test] +fn requires_clause_emits_contracts_attribute() { + let spec: Spec = parse_quote! { + requires: CONDITION, + }; + let func: ItemFn = parse_quote! { + fn demo() {} + }; + + let instrumented = instrument_fn(&spec, func).expect("requires should succeed"); + + let expected: Attribute = parse_quote! { #[contracts::requires(CONDITION)] }; + assert_eq!(instrumented.attrs.len(), 1); + assert_attr_eq(&instrumented.attrs[0], &expected); +} + +#[test] +fn requires_with_cfg_emits_cfg_attr_contracts_attribute() { + let spec: Spec = parse_quote! { + #[cfg(SETTING)] + requires: CONDITION, + }; + let func: ItemFn = parse_quote! { + fn demo() {} + }; + + let instrumented = instrument_fn(&spec, func).expect("requires should succeed"); + + let expected: Attribute = parse_quote! { #[cfg_attr(SETTING, contracts::requires(CONDITION))] }; + assert_eq!(instrumented.attrs.len(), 1); + assert_attr_eq(&instrumented.attrs[0], &expected); +} + +#[test] +fn maintains_emits_requires_and_ensures_attributes() { + let spec: Spec = parse_quote! { + maintains: CONDITION, + }; + let func: ItemFn = parse_quote! { + fn demo() {} + }; + + let instrumented = instrument_fn(&spec, func).expect("maintains should succeed"); + + let expected_requires: Attribute = parse_quote! { #[contracts::requires(CONDITION)] }; + let expected_ensures: Attribute = parse_quote! { #[contracts::ensures(|_| CONDITION)] }; + + assert_eq!(instrumented.attrs.len(), 2); + assert_attr_eq(&instrumented.attrs[0], &expected_requires); + assert_attr_eq(&instrumented.attrs[1], &expected_ensures); +} + +#[test] +fn ensures_from_expression_uses_generated_closure() { + let spec: Spec = parse_quote! { + ensures: CONDITION, + }; + let func: ItemFn = parse_quote! { + fn demo() {} + }; + + let instrumented = instrument_fn(&spec, func).expect("ensures should succeed"); + + let expected: Attribute = parse_quote! { #[contracts::ensures(|output| CONDITION)] }; + + assert_eq!(instrumented.attrs.len(), 1); + assert_attr_eq(&instrumented.attrs[0], &expected); +} + +#[test] +fn ensures_with_custom_closure_is_preserved() { + let spec: Spec = parse_quote! { + ensures: |result| result.is_ok(), + }; + let func: ItemFn = parse_quote! { + fn demo() {} + }; + + let instrumented = instrument_fn(&spec, func).expect("ensures should succeed"); + + let expected: Attribute = parse_quote! { #[contracts::ensures(|result| result.is_ok())] }; + + assert_eq!(instrumented.attrs.len(), 1); + assert_attr_eq(&instrumented.attrs[0], &expected); +} + +#[test] +fn existing_attributes_are_preserved_after_contracts_attributes() { + let spec: Spec = parse_quote! { + requires: CONDITION, + }; + let func: ItemFn = parse_quote! { + #[inline] + fn demo() {} + }; + + let instrumented = instrument_fn(&spec, func).expect("requires should succeed"); + + assert_eq!(instrumented.attrs.len(), 2); + + let expected_requires: Attribute = parse_quote! { #[contracts::requires(CONDITION)] }; + assert_attr_eq(&instrumented.attrs[0], &expected_requires); + let expected_inline: Attribute = parse_quote! { #[inline] }; + assert_attr_eq(&instrumented.attrs[1], &expected_inline); +} + +#[test] +#[should_panic(expected = "not supported by the nightly contracts backend")] +fn reject_captures() { + let spec: Spec = parse_quote! { + captures: value as old_value, + }; + let func: ItemFn = parse_quote! { + fn demo() {} + }; + + match instrument_fn(&spec, func) { + Ok(_) => panic!("expected captures to be rejected"), + Err(err) => panic!("{}", err), + } +} diff --git a/crates/anodized/Cargo.toml b/crates/anodized/Cargo.toml index 17c842d2..3e98f42a 100644 --- a/crates/anodized/Cargo.toml +++ b/crates/anodized/Cargo.toml @@ -22,6 +22,7 @@ anodized-core.workspace = true proc-macro2.workspace = true quote.workspace = true syn.workspace = true +rustversion.workspace = true [dev-dependencies] trybuild = "1.0" diff --git a/crates/anodized/src/lib.rs b/crates/anodized/src/lib.rs index 8fbefd45..0bde4885 100644 --- a/crates/anodized/src/lib.rs +++ b/crates/anodized/src/lib.rs @@ -19,7 +19,8 @@ const _: () = { } }; -#[cfg(all(feature = "backend-nightly-contracts", not(nightly)))] +#[rustversion::not(nightly)] +#[cfg(feature = "backend-nightly-contracts")] compile_error!("the `backend-nightly-contracts` feature requires a nightly Rust toolchain"); const BACKEND: Backend = if cfg!(feature = "backend-nightly-contracts") { From 06242f2ca094d20b6f8ec43565f5ed8410669e53 Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Sun, 21 Sep 2025 22:52:38 +0900 Subject: [PATCH 04/17] checkpoint --- .../src/backend/nightly_contracts/tests.rs | 95 +++++++++---------- crates/anodized-core/src/test_util.rs | 21 +++- 2 files changed, 65 insertions(+), 51 deletions(-) diff --git a/crates/anodized-core/src/backend/nightly_contracts/tests.rs b/crates/anodized-core/src/backend/nightly_contracts/tests.rs index 91b07510..8ee1eaf8 100644 --- a/crates/anodized-core/src/backend/nightly_contracts/tests.rs +++ b/crates/anodized-core/src/backend/nightly_contracts/tests.rs @@ -1,29 +1,23 @@ use super::*; -use quote::ToTokens; -use syn::{Attribute, ItemFn, parse_quote}; - -fn assert_attr_eq(actual: &Attribute, expected: &Attribute) { - assert_eq!( - actual.to_token_stream().to_string(), - expected.to_token_stream().to_string() - ); -} +use crate::test_util::assert_fn_eq; +use syn::{ItemFn, parse_quote}; #[test] fn requires_clause_emits_contracts_attribute() { let spec: Spec = parse_quote! { requires: CONDITION, }; - let func: ItemFn = parse_quote! { + let func: ItemFn = parse_quote! { fn demo() {} }; + + let observed = instrument_fn(&spec, func).expect("requires should succeed"); + + let expected: ItemFn = parse_quote! { + #[contracts::requires(CONDITION)] fn demo() {} }; - let instrumented = instrument_fn(&spec, func).expect("requires should succeed"); - - let expected: Attribute = parse_quote! { #[contracts::requires(CONDITION)] }; - assert_eq!(instrumented.attrs.len(), 1); - assert_attr_eq(&instrumented.attrs[0], &expected); + assert_fn_eq(&observed, &expected); } #[test] @@ -32,15 +26,16 @@ fn requires_with_cfg_emits_cfg_attr_contracts_attribute() { #[cfg(SETTING)] requires: CONDITION, }; - let func: ItemFn = parse_quote! { + let func: ItemFn = parse_quote! { fn demo() {} }; + + let observed = instrument_fn(&spec, func).expect("requires should succeed"); + + let expected: ItemFn = parse_quote! { + #[cfg_attr(SETTING, contracts::requires(CONDITION))] fn demo() {} }; - let instrumented = instrument_fn(&spec, func).expect("requires should succeed"); - - let expected: Attribute = parse_quote! { #[cfg_attr(SETTING, contracts::requires(CONDITION))] }; - assert_eq!(instrumented.attrs.len(), 1); - assert_attr_eq(&instrumented.attrs[0], &expected); + assert_fn_eq(&observed, &expected); } #[test] @@ -48,18 +43,17 @@ fn maintains_emits_requires_and_ensures_attributes() { let spec: Spec = parse_quote! { maintains: CONDITION, }; - let func: ItemFn = parse_quote! { - fn demo() {} - }; + let func: ItemFn = parse_quote! { fn demo() {} }; - let instrumented = instrument_fn(&spec, func).expect("maintains should succeed"); + let observed = instrument_fn(&spec, func).expect("maintains should succeed"); - let expected_requires: Attribute = parse_quote! { #[contracts::requires(CONDITION)] }; - let expected_ensures: Attribute = parse_quote! { #[contracts::ensures(|_| CONDITION)] }; + let expected: ItemFn = parse_quote! { + #[contracts::requires(CONDITION)] + #[contracts::ensures(|_| CONDITION)] + fn demo() {} + }; - assert_eq!(instrumented.attrs.len(), 2); - assert_attr_eq(&instrumented.attrs[0], &expected_requires); - assert_attr_eq(&instrumented.attrs[1], &expected_ensures); + assert_fn_eq(&observed, &expected); } #[test] @@ -67,16 +61,16 @@ fn ensures_from_expression_uses_generated_closure() { let spec: Spec = parse_quote! { ensures: CONDITION, }; - let func: ItemFn = parse_quote! { - fn demo() {} - }; + let func: ItemFn = parse_quote! { fn demo() {} }; - let instrumented = instrument_fn(&spec, func).expect("ensures should succeed"); + let observed = instrument_fn(&spec, func).expect("ensures should succeed"); - let expected: Attribute = parse_quote! { #[contracts::ensures(|output| CONDITION)] }; + let expected: ItemFn = parse_quote! { + #[contracts::ensures(|output| CONDITION)] + fn demo() {} + }; - assert_eq!(instrumented.attrs.len(), 1); - assert_attr_eq(&instrumented.attrs[0], &expected); + assert_fn_eq(&observed, &expected); } #[test] @@ -84,16 +78,16 @@ fn ensures_with_custom_closure_is_preserved() { let spec: Spec = parse_quote! { ensures: |result| result.is_ok(), }; - let func: ItemFn = parse_quote! { - fn demo() {} - }; + let func: ItemFn = parse_quote! { fn demo() {} }; - let instrumented = instrument_fn(&spec, func).expect("ensures should succeed"); + let observed = instrument_fn(&spec, func).expect("ensures should succeed"); - let expected: Attribute = parse_quote! { #[contracts::ensures(|result| result.is_ok())] }; + let expected: ItemFn = parse_quote! { + #[contracts::ensures(|result| result.is_ok())] + fn demo() {} + }; - assert_eq!(instrumented.attrs.len(), 1); - assert_attr_eq(&instrumented.attrs[0], &expected); + assert_fn_eq(&observed, &expected); } #[test] @@ -106,14 +100,15 @@ fn existing_attributes_are_preserved_after_contracts_attributes() { fn demo() {} }; - let instrumented = instrument_fn(&spec, func).expect("requires should succeed"); + let observed = instrument_fn(&spec, func).expect("requires should succeed"); - assert_eq!(instrumented.attrs.len(), 2); + let expected: ItemFn = parse_quote! { + #[contracts::requires(CONDITION)] + #[inline] + fn demo() {} + }; - let expected_requires: Attribute = parse_quote! { #[contracts::requires(CONDITION)] }; - assert_attr_eq(&instrumented.attrs[0], &expected_requires); - let expected_inline: Attribute = parse_quote! { #[inline] }; - assert_attr_eq(&instrumented.attrs[1], &expected_inline); + assert_fn_eq(&observed, &expected); } #[test] diff --git a/crates/anodized-core/src/test_util.rs b/crates/anodized-core/src/test_util.rs index 7553086b..4f0986ad 100644 --- a/crates/anodized-core/src/test_util.rs +++ b/crates/anodized-core/src/test_util.rs @@ -1,7 +1,7 @@ use crate::{Capture, Condition, PostCondition, Spec}; use quote::ToTokens; use syn::{ - Block, + Attribute, Block, ItemFn, parse::{Parse, ParseStream, Result}, }; @@ -20,6 +20,12 @@ pub fn assert_block_eq(left: &Block, right: &Block) { assert_eq!(left_str, right_str); } +pub fn assert_fn_eq(left: &ItemFn, right: &ItemFn) { + let left_str = left.to_token_stream().to_string(); + let right_str = right.to_token_stream().to_string(); + assert_eq!(left_str, right_str); +} + pub fn assert_spec_eq(left: &Spec, right: &Spec) { // Destructure to ensure we handle all fields - compilation will fail if fields are added let Spec { @@ -79,6 +85,19 @@ where } } +pub fn assert_attrs_eq(left: &[Attribute], right: &[Attribute]) { + assert_slice_eq(left, right, "attribute", &assert_attr_eq); +} + +pub fn assert_attr_eq(left: &Attribute, right: &Attribute, msg_prefix: &str) { + assert_eq!( + left.to_token_stream().to_string(), + right.to_token_stream().to_string(), + "{}tokens do not match", + msg_prefix + ); +} + fn assert_condition_eq(left: &Condition, right: &Condition, msg_prefix: &str) { // Destructure to ensure we handle all fields let Condition { From 87a2727ed10f8d594fcef141b9bf5c7525b94907 Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Sun, 21 Sep 2025 23:14:34 +0900 Subject: [PATCH 05/17] simplify test_util --- .../backend/anodized/test_instrument_fn.rs | 34 ++++++------- .../src/backend/nightly_contracts/tests.rs | 51 +++++++++---------- crates/anodized-core/src/test_util.rs | 26 +--------- 3 files changed, 44 insertions(+), 67 deletions(-) diff --git a/crates/anodized-core/src/backend/anodized/test_instrument_fn.rs b/crates/anodized-core/src/backend/anodized/test_instrument_fn.rs index dfae7707..0280e219 100644 --- a/crates/anodized-core/src/backend/anodized/test_instrument_fn.rs +++ b/crates/anodized-core/src/backend/anodized/test_instrument_fn.rs @@ -1,4 +1,4 @@ -use crate::test_util::assert_block_eq; +use crate::test_util::assert_tokens_eq; use super::*; use syn::{Block, Type, parse_quote}; @@ -33,7 +33,7 @@ fn test_instrument_simple_requires() { }; let observed = instrument_fn_body(&spec, &body, is_async, &ret_type, false).unwrap(); - assert_block_eq(&observed, &expected); + assert_tokens_eq(&observed, &expected); } #[test] @@ -56,7 +56,7 @@ fn test_instrument_requires_disable_runtime_checks() { }; let observed = instrument_fn_body(&spec, &body, is_async, &ret_type, true).unwrap(); - assert_block_eq(&observed, &expected); + assert_tokens_eq(&observed, &expected); } #[test] @@ -78,7 +78,7 @@ fn test_instrument_simple_maintains() { }; let observed = instrument_fn_body(&spec, &body, is_async, &ret_type, false).unwrap(); - assert_block_eq(&observed, &expected); + assert_tokens_eq(&observed, &expected); } #[test] @@ -99,7 +99,7 @@ fn test_instrument_simple_ensures() { }; let observed = instrument_fn_body(&spec, &body, is_async, &ret_type, false).unwrap(); - assert_block_eq(&observed, &expected); + assert_tokens_eq(&observed, &expected); } #[test] @@ -123,7 +123,7 @@ fn test_instrument_simple_requires_and_maintains() { }; let observed = instrument_fn_body(&spec, &body, is_async, &ret_type, false).unwrap(); - assert_block_eq(&observed, &expected); + assert_tokens_eq(&observed, &expected); } #[test] @@ -146,7 +146,7 @@ fn test_instrument_simple_requires_and_ensures() { }; let observed = instrument_fn_body(&spec, &body, is_async, &ret_type, false).unwrap(); - assert_block_eq(&observed, &expected); + assert_tokens_eq(&observed, &expected); } #[test] @@ -170,7 +170,7 @@ fn test_instrument_simple_maintains_and_ensures() { }; let observed = instrument_fn_body(&spec, &body, is_async, &ret_type, false).unwrap(); - assert_block_eq(&observed, &expected); + assert_tokens_eq(&observed, &expected); } #[test] @@ -196,7 +196,7 @@ fn test_instrument_simple_requires_maintains_and_ensures() { }; let observed = instrument_fn_body(&spec, &body, is_async, &ret_type, false).unwrap(); - assert_block_eq(&observed, &expected); + assert_tokens_eq(&observed, &expected); } #[test] @@ -222,7 +222,7 @@ fn test_instrument_simple_async_requires_maintains_and_ensures() { }; let observed = instrument_fn_body(&spec, &body, is_async, &ret_type, false).unwrap(); - assert_block_eq(&observed, &expected); + assert_tokens_eq(&observed, &expected); } #[test] @@ -252,7 +252,7 @@ fn test_instrument_multiple_conditions_in_clauses() { }; let observed = instrument_fn_body(&spec, &body, is_async, &ret_type, false).unwrap(); - assert_block_eq(&observed, &expected); + assert_tokens_eq(&observed, &expected); } #[test] @@ -274,7 +274,7 @@ fn test_instrument_with_binds_parameter() { }; let observed = instrument_fn_body(&spec, &body, is_async, &ret_type, false).unwrap(); - assert_block_eq(&observed, &expected); + assert_tokens_eq(&observed, &expected); } #[test] @@ -303,7 +303,7 @@ fn test_instrument_ensures_with_mixed_conditions() { }; let observed = instrument_fn_body(&spec, &body, is_async, &ret_type, false).unwrap(); - assert_block_eq(&observed, &expected); + assert_tokens_eq(&observed, &expected); } #[test] @@ -340,7 +340,7 @@ fn test_instrument_with_cfg_attributes() { }; let observed = instrument_fn_body(&spec, &body, is_async, &ret_type, false).unwrap(); - assert_block_eq(&observed, &expected); + assert_tokens_eq(&observed, &expected); } #[test] @@ -377,7 +377,7 @@ fn test_instrument_with_cfg_on_single_and_list_conditions() { }; let observed = instrument_fn_body(&spec, &body, is_async, &ret_type, false).unwrap(); - assert_block_eq(&observed, &expected); + assert_tokens_eq(&observed, &expected); } #[test] @@ -429,7 +429,7 @@ fn test_instrument_with_complex_mixed_conditions() { }; let observed = instrument_fn_body(&spec, &body, is_async, &ret_type, false).unwrap(); - assert_block_eq(&observed, &expected); + assert_tokens_eq(&observed, &expected); } #[test] @@ -460,5 +460,5 @@ fn test_instrument_with_captures() { }; let observed = instrument_fn_body(&spec, &body, is_async, &ret_type, false).unwrap(); - assert_block_eq(&observed, &expected); + assert_tokens_eq(&observed, &expected); } diff --git a/crates/anodized-core/src/backend/nightly_contracts/tests.rs b/crates/anodized-core/src/backend/nightly_contracts/tests.rs index 8ee1eaf8..618647ed 100644 --- a/crates/anodized-core/src/backend/nightly_contracts/tests.rs +++ b/crates/anodized-core/src/backend/nightly_contracts/tests.rs @@ -1,6 +1,6 @@ use super::*; -use crate::test_util::assert_fn_eq; +use crate::test_util::assert_tokens_eq; use syn::{ItemFn, parse_quote}; #[test] @@ -10,14 +10,14 @@ fn requires_clause_emits_contracts_attribute() { }; let func: ItemFn = parse_quote! { fn demo() {} }; - let observed = instrument_fn(&spec, func).expect("requires should succeed"); - let expected: ItemFn = parse_quote! { #[contracts::requires(CONDITION)] - fn demo() {} + #func }; - assert_fn_eq(&observed, &expected); + let observed = instrument_fn(&spec, func).unwrap(); + + assert_tokens_eq(&observed, &expected); } #[test] @@ -28,14 +28,14 @@ fn requires_with_cfg_emits_cfg_attr_contracts_attribute() { }; let func: ItemFn = parse_quote! { fn demo() {} }; - let observed = instrument_fn(&spec, func).expect("requires should succeed"); - let expected: ItemFn = parse_quote! { #[cfg_attr(SETTING, contracts::requires(CONDITION))] - fn demo() {} + #func }; - assert_fn_eq(&observed, &expected); + let observed = instrument_fn(&spec, func).unwrap(); + + assert_tokens_eq(&observed, &expected); } #[test] @@ -45,15 +45,15 @@ fn maintains_emits_requires_and_ensures_attributes() { }; let func: ItemFn = parse_quote! { fn demo() {} }; - let observed = instrument_fn(&spec, func).expect("maintains should succeed"); - let expected: ItemFn = parse_quote! { #[contracts::requires(CONDITION)] #[contracts::ensures(|_| CONDITION)] - fn demo() {} + #func }; - assert_fn_eq(&observed, &expected); + let observed = instrument_fn(&spec, func).unwrap(); + + assert_tokens_eq(&observed, &expected); } #[test] @@ -63,14 +63,14 @@ fn ensures_from_expression_uses_generated_closure() { }; let func: ItemFn = parse_quote! { fn demo() {} }; - let observed = instrument_fn(&spec, func).expect("ensures should succeed"); - let expected: ItemFn = parse_quote! { #[contracts::ensures(|output| CONDITION)] - fn demo() {} + #func }; - assert_fn_eq(&observed, &expected); + let observed = instrument_fn(&spec, func).unwrap(); + + assert_tokens_eq(&observed, &expected); } #[test] @@ -80,14 +80,14 @@ fn ensures_with_custom_closure_is_preserved() { }; let func: ItemFn = parse_quote! { fn demo() {} }; - let observed = instrument_fn(&spec, func).expect("ensures should succeed"); - let expected: ItemFn = parse_quote! { #[contracts::ensures(|result| result.is_ok())] - fn demo() {} + #func }; - assert_fn_eq(&observed, &expected); + let observed = instrument_fn(&spec, func).unwrap(); + + assert_tokens_eq(&observed, &expected); } #[test] @@ -100,15 +100,14 @@ fn existing_attributes_are_preserved_after_contracts_attributes() { fn demo() {} }; - let observed = instrument_fn(&spec, func).expect("requires should succeed"); - let expected: ItemFn = parse_quote! { #[contracts::requires(CONDITION)] - #[inline] - fn demo() {} + #func }; - assert_fn_eq(&observed, &expected); + let observed = instrument_fn(&spec, func).unwrap(); + + assert_tokens_eq(&observed, &expected); } #[test] diff --git a/crates/anodized-core/src/test_util.rs b/crates/anodized-core/src/test_util.rs index 4f0986ad..281fa7a3 100644 --- a/crates/anodized-core/src/test_util.rs +++ b/crates/anodized-core/src/test_util.rs @@ -1,9 +1,6 @@ use crate::{Capture, Condition, PostCondition, Spec}; use quote::ToTokens; -use syn::{ - Attribute, Block, ItemFn, - parse::{Parse, ParseStream, Result}, -}; +use syn::parse::{Parse, ParseStream, Result}; impl Parse for Condition { fn parse(input: ParseStream) -> Result { @@ -14,13 +11,7 @@ impl Parse for Condition { } } -pub fn assert_block_eq(left: &Block, right: &Block) { - let left_str = left.to_token_stream().to_string(); - let right_str = right.to_token_stream().to_string(); - assert_eq!(left_str, right_str); -} - -pub fn assert_fn_eq(left: &ItemFn, right: &ItemFn) { +pub fn assert_tokens_eq(left: &impl ToTokens, right: &impl ToTokens) { let left_str = left.to_token_stream().to_string(); let right_str = right.to_token_stream().to_string(); assert_eq!(left_str, right_str); @@ -85,19 +76,6 @@ where } } -pub fn assert_attrs_eq(left: &[Attribute], right: &[Attribute]) { - assert_slice_eq(left, right, "attribute", &assert_attr_eq); -} - -pub fn assert_attr_eq(left: &Attribute, right: &Attribute, msg_prefix: &str) { - assert_eq!( - left.to_token_stream().to_string(), - right.to_token_stream().to_string(), - "{}tokens do not match", - msg_prefix - ); -} - fn assert_condition_eq(left: &Condition, right: &Condition, msg_prefix: &str) { // Destructure to ensure we handle all fields let Condition { From aa30026c8bcbee2b91c78a62d645e2575794574b Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Sun, 21 Sep 2025 23:17:55 +0900 Subject: [PATCH 06/17] simplify tests --- .../src/backend/nightly_contracts/tests.rs | 24 ++++--------------- 1 file changed, 5 insertions(+), 19 deletions(-) diff --git a/crates/anodized-core/src/backend/nightly_contracts/tests.rs b/crates/anodized-core/src/backend/nightly_contracts/tests.rs index 618647ed..70e5fc9e 100644 --- a/crates/anodized-core/src/backend/nightly_contracts/tests.rs +++ b/crates/anodized-core/src/backend/nightly_contracts/tests.rs @@ -59,29 +59,15 @@ fn maintains_emits_requires_and_ensures_attributes() { #[test] fn ensures_from_expression_uses_generated_closure() { let spec: Spec = parse_quote! { - ensures: CONDITION, + binds: PATTERN_1, + ensures: CONDITION_1, + ensures: |PATTERN_2| CONDITION_2, }; let func: ItemFn = parse_quote! { fn demo() {} }; let expected: ItemFn = parse_quote! { - #[contracts::ensures(|output| CONDITION)] - #func - }; - - let observed = instrument_fn(&spec, func).unwrap(); - - assert_tokens_eq(&observed, &expected); -} - -#[test] -fn ensures_with_custom_closure_is_preserved() { - let spec: Spec = parse_quote! { - ensures: |result| result.is_ok(), - }; - let func: ItemFn = parse_quote! { fn demo() {} }; - - let expected: ItemFn = parse_quote! { - #[contracts::ensures(|result| result.is_ok())] + #[contracts::ensures(|PATTERN_1| CONDITION_1)] + #[contracts::ensures(|PATTERN_2| CONDITION_2)] #func }; From fb94f80e2cfb0e54afec3e33a4af52e3ddefeec5 Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Sun, 21 Sep 2025 23:50:21 +0900 Subject: [PATCH 07/17] use fully qualified name --- .../src/backend/nightly_contracts/mod.rs | 16 ++++++++-------- .../src/backend/nightly_contracts/tests.rs | 14 +++++++------- 2 files changed, 15 insertions(+), 15 deletions(-) diff --git a/crates/anodized-core/src/backend/nightly_contracts/mod.rs b/crates/anodized-core/src/backend/nightly_contracts/mod.rs index 070e901a..10e14058 100644 --- a/crates/anodized-core/src/backend/nightly_contracts/mod.rs +++ b/crates/anodized-core/src/backend/nightly_contracts/mod.rs @@ -20,9 +20,9 @@ pub fn instrument_fn(spec: &Spec, mut func: ItemFn) -> Result { let expr = &condition.expr; let attr = if let Some(cfg) = &condition.cfg { - parse_quote! { #[cfg_attr(#cfg, contracts::requires(#expr))] } + parse_quote! { #[cfg_attr(#cfg, core::contracts::requires(#expr))] } } else { - parse_quote! { #[contracts::requires(#expr)] } + parse_quote! { #[core::contracts::requires(#expr)] } }; attrs.push(attr); @@ -32,17 +32,17 @@ pub fn instrument_fn(spec: &Spec, mut func: ItemFn) -> Result { let expr = &condition.expr; let requires_attr = if let Some(cfg) = &condition.cfg { - parse_quote! { #[cfg_attr(#cfg, contracts::requires(#expr))] } + parse_quote! { #[cfg_attr(#cfg, core::contracts::requires(#expr))] } } else { - parse_quote! { #[contracts::requires(#expr)] } + parse_quote! { #[core::contracts::requires(#expr)] } }; attrs.push(requires_attr); let ensures_closure: Expr = parse_quote! { |_| #expr }; let ensures_attr = if let Some(cfg) = &condition.cfg { - parse_quote! { #[cfg_attr(#cfg, contracts::ensures(#ensures_closure))] } + parse_quote! { #[cfg_attr(#cfg, core::contracts::ensures(#ensures_closure))] } } else { - parse_quote! { #[contracts::ensures(#ensures_closure)] } + parse_quote! { #[core::contracts::ensures(#ensures_closure)] } }; attrs.push(ensures_attr); } @@ -51,9 +51,9 @@ pub fn instrument_fn(spec: &Spec, mut func: ItemFn) -> Result { let closure: ExprClosure = postcondition.closure.clone(); let attr = if let Some(cfg) = &postcondition.cfg { - parse_quote! { #[cfg_attr(#cfg, contracts::ensures(#closure))] } + parse_quote! { #[cfg_attr(#cfg, core::contracts::ensures(#closure))] } } else { - parse_quote! { #[contracts::ensures(#closure)] } + parse_quote! { #[core::contracts::ensures(#closure)] } }; attrs.push(attr); } diff --git a/crates/anodized-core/src/backend/nightly_contracts/tests.rs b/crates/anodized-core/src/backend/nightly_contracts/tests.rs index 70e5fc9e..bd22444a 100644 --- a/crates/anodized-core/src/backend/nightly_contracts/tests.rs +++ b/crates/anodized-core/src/backend/nightly_contracts/tests.rs @@ -11,7 +11,7 @@ fn requires_clause_emits_contracts_attribute() { let func: ItemFn = parse_quote! { fn demo() {} }; let expected: ItemFn = parse_quote! { - #[contracts::requires(CONDITION)] + #[core::contracts::requires(CONDITION)] #func }; @@ -29,7 +29,7 @@ fn requires_with_cfg_emits_cfg_attr_contracts_attribute() { let func: ItemFn = parse_quote! { fn demo() {} }; let expected: ItemFn = parse_quote! { - #[cfg_attr(SETTING, contracts::requires(CONDITION))] + #[cfg_attr(SETTING, core::contracts::requires(CONDITION))] #func }; @@ -46,8 +46,8 @@ fn maintains_emits_requires_and_ensures_attributes() { let func: ItemFn = parse_quote! { fn demo() {} }; let expected: ItemFn = parse_quote! { - #[contracts::requires(CONDITION)] - #[contracts::ensures(|_| CONDITION)] + #[core::contracts::requires(CONDITION)] + #[core::contracts::ensures(|_| CONDITION)] #func }; @@ -66,8 +66,8 @@ fn ensures_from_expression_uses_generated_closure() { let func: ItemFn = parse_quote! { fn demo() {} }; let expected: ItemFn = parse_quote! { - #[contracts::ensures(|PATTERN_1| CONDITION_1)] - #[contracts::ensures(|PATTERN_2| CONDITION_2)] + #[core::contracts::ensures(|PATTERN_1| CONDITION_1)] + #[core::contracts::ensures(|PATTERN_2| CONDITION_2)] #func }; @@ -87,7 +87,7 @@ fn existing_attributes_are_preserved_after_contracts_attributes() { }; let expected: ItemFn = parse_quote! { - #[contracts::requires(CONDITION)] + #[core::contracts::requires(CONDITION)] #func }; From 8516bf0b78e676ca501188d815e12ddfbafd5e10 Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Mon, 22 Sep 2025 00:14:20 +0900 Subject: [PATCH 08/17] do not test captures on backend-nightly-contracts --- crates/anodized/tests/block_expressions.rs | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/crates/anodized/tests/block_expressions.rs b/crates/anodized/tests/block_expressions.rs index 4cf22821..bdf6c951 100644 --- a/crates/anodized/tests/block_expressions.rs +++ b/crates/anodized/tests/block_expressions.rs @@ -1,5 +1,6 @@ use anodized::spec; +#[cfg(not(feature = "backend-nightly-contracts"))] #[spec( requires: { // Just a longer way of writing `true` :) @@ -23,6 +24,26 @@ fn function_with_blocks(vec: &mut Vec) { vec.push(42); } +#[cfg(feature = "backend-nightly-contracts")] +#[spec( + requires: { + // Just a longer way of writing `true` :) + let x = 5; + x > 0 + }, + maintains: { + let length = vec.len(); + length < 100 + }, + ensures: { + let length = vec.len(); + length > 0 + }, +)] +fn function_with_blocks(vec: &mut Vec) { + vec.push(42); +} + #[test] fn test_block_expressions() { let mut vec = vec![1, 2, 3]; From 488c9929e5911b320164d1f752910241d51a0782 Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Mon, 22 Sep 2025 00:35:56 +0900 Subject: [PATCH 09/17] rename feature to backend-native-contracts --- crates/anodized-core/src/backend/mod.rs | 9 ++++++--- .../{nightly_contracts => native_contracts}/mod.rs | 0 .../{nightly_contracts => native_contracts}/tests.rs | 0 crates/anodized/Cargo.toml | 2 +- crates/anodized/src/lib.rs | 10 +++++----- crates/anodized/tests/block_expressions.rs | 4 ++-- 6 files changed, 14 insertions(+), 11 deletions(-) rename crates/anodized-core/src/backend/{nightly_contracts => native_contracts}/mod.rs (100%) rename crates/anodized-core/src/backend/{nightly_contracts => native_contracts}/tests.rs (100%) diff --git a/crates/anodized-core/src/backend/mod.rs b/crates/anodized-core/src/backend/mod.rs index 0196a731..fc5679d7 100644 --- a/crates/anodized-core/src/backend/mod.rs +++ b/crates/anodized-core/src/backend/mod.rs @@ -1,5 +1,5 @@ pub mod anodized; -pub mod nightly_contracts; +pub mod native_contracts; use syn::ItemFn; @@ -7,9 +7,12 @@ use crate::Spec; #[derive(Copy, Clone, Debug, Eq, PartialEq)] pub enum Backend { + /// Anodized instrumentation with runtime checks. Default, + /// Anodized instrumentation with no runtime checks. NoChecks, - NightlyContracts, + /// Experimental Rust-native contracts, see https://github.com/rust-lang/rust/issues/128044. + NativeContracts, } pub fn handle_fn(backend: Backend, spec: Spec, mut func: ItemFn) -> syn::Result { @@ -36,6 +39,6 @@ pub fn handle_fn(backend: Backend, spec: Spec, mut func: ItemFn) -> syn::Result< match backend { Backend::Default | Backend::NoChecks => Ok(func), - Backend::NightlyContracts => nightly_contracts::instrument_fn(&spec, func), + Backend::NativeContracts => native_contracts::instrument_fn(&spec, func), } } diff --git a/crates/anodized-core/src/backend/nightly_contracts/mod.rs b/crates/anodized-core/src/backend/native_contracts/mod.rs similarity index 100% rename from crates/anodized-core/src/backend/nightly_contracts/mod.rs rename to crates/anodized-core/src/backend/native_contracts/mod.rs diff --git a/crates/anodized-core/src/backend/nightly_contracts/tests.rs b/crates/anodized-core/src/backend/native_contracts/tests.rs similarity index 100% rename from crates/anodized-core/src/backend/nightly_contracts/tests.rs rename to crates/anodized-core/src/backend/native_contracts/tests.rs diff --git a/crates/anodized/Cargo.toml b/crates/anodized/Cargo.toml index 3e98f42a..29ed4b84 100644 --- a/crates/anodized/Cargo.toml +++ b/crates/anodized/Cargo.toml @@ -15,7 +15,7 @@ proc-macro = true [features] backend-no-checks = [] -backend-nightly-contracts = [] +backend-native-contracts = [] [dependencies] anodized-core.workspace = true diff --git a/crates/anodized/src/lib.rs b/crates/anodized/src/lib.rs index 0bde4885..5d0ef2dd 100644 --- a/crates/anodized/src/lib.rs +++ b/crates/anodized/src/lib.rs @@ -13,18 +13,18 @@ use anodized_core::{ const _: () = { let count: u32 = cfg!(feature = "backend-no-checks") as u32 - + cfg!(feature = "backend-nightly-contracts") as u32; + + cfg!(feature = "backend-native-contracts") as u32; if count > 1 { panic!("anodized: backend features are mutually exclusive"); } }; #[rustversion::not(nightly)] -#[cfg(feature = "backend-nightly-contracts")] -compile_error!("the `backend-nightly-contracts` feature requires a nightly Rust toolchain"); +#[cfg(feature = "backend-native-contracts")] +compile_error!("the `backend-native-contracts` feature requires a nightly Rust toolchain"); -const BACKEND: Backend = if cfg!(feature = "backend-nightly-contracts") { - Backend::NightlyContracts +const BACKEND: Backend = if cfg!(feature = "backend-native-contracts") { + Backend::NativeContracts } else if cfg!(feature = "backend-no-checks") { Backend::NoChecks } else { diff --git a/crates/anodized/tests/block_expressions.rs b/crates/anodized/tests/block_expressions.rs index bdf6c951..89ea96b4 100644 --- a/crates/anodized/tests/block_expressions.rs +++ b/crates/anodized/tests/block_expressions.rs @@ -1,6 +1,6 @@ use anodized::spec; -#[cfg(not(feature = "backend-nightly-contracts"))] +#[cfg(not(feature = "backend-native-contracts"))] #[spec( requires: { // Just a longer way of writing `true` :) @@ -24,7 +24,7 @@ fn function_with_blocks(vec: &mut Vec) { vec.push(42); } -#[cfg(feature = "backend-nightly-contracts")] +#[cfg(feature = "backend-native-contracts")] #[spec( requires: { // Just a longer way of writing `true` :) From ded7d572135731faae6bd8c5d5ac71e92f5322da Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Mon, 22 Sep 2025 01:19:39 +0900 Subject: [PATCH 10/17] ensure existing tests pass with backend-no-checks --- crates/anodized/tests/basic_enum.rs | 1 + crates/anodized/tests/basic_function.rs | 1 + crates/anodized/tests/captures_feature.rs | 2 ++ crates/anodized/tests/default_output_pattern.rs | 1 + crates/anodized/tests/execution_order.rs | 1 + crates/anodized/tests/explicit_binding_in_postcondition.rs | 1 + crates/anodized/tests/method_call_invariant.rs | 2 ++ crates/anodized/tests/method_with_invariant.rs | 2 ++ crates/anodized/tests/multiple_conditions.rs | 2 ++ crates/anodized/tests/rename_return_value.rs | 1 + 10 files changed, 14 insertions(+) diff --git a/crates/anodized/tests/basic_enum.rs b/crates/anodized/tests/basic_enum.rs index c357f163..d6a594fc 100644 --- a/crates/anodized/tests/basic_enum.rs +++ b/crates/anodized/tests/basic_enum.rs @@ -29,6 +29,7 @@ fn test_job_start_success() { job.start(); } +#[cfg(not(feature = "backend-no-checks"))] #[test] #[should_panic(expected = "Precondition failed: matches! (self.state, State::Idle)")] fn test_job_start_panics_if_not_idle() { diff --git a/crates/anodized/tests/basic_function.rs b/crates/anodized/tests/basic_function.rs index f0b858db..683cfa57 100644 --- a/crates/anodized/tests/basic_function.rs +++ b/crates/anodized/tests/basic_function.rs @@ -13,6 +13,7 @@ fn test_divide_success() { checked_divide(10, 2); } +#[cfg(not(feature = "backend-no-checks"))] #[test] #[should_panic(expected = "Precondition failed: divisor != 0")] fn test_divide_by_zero_panics() { diff --git a/crates/anodized/tests/captures_feature.rs b/crates/anodized/tests/captures_feature.rs index 70b3a70f..125173ba 100644 --- a/crates/anodized/tests/captures_feature.rs +++ b/crates/anodized/tests/captures_feature.rs @@ -116,6 +116,7 @@ fn test_captures_with_preconditions() { assert_eq!(container.counter, 51); } +#[cfg(not(feature = "backend-no-checks"))] #[test] #[should_panic(expected = "Postcondition failed")] fn test_capture_postcondition_failure() { @@ -132,6 +133,7 @@ fn test_capture_postcondition_failure() { bad_increment(&mut val); } +#[cfg(not(feature = "backend-no-checks"))] #[test] #[should_panic(expected = "Precondition failed")] fn test_precondition_runs_before_captures() { diff --git a/crates/anodized/tests/default_output_pattern.rs b/crates/anodized/tests/default_output_pattern.rs index 5712762e..e9ae5b4e 100644 --- a/crates/anodized/tests/default_output_pattern.rs +++ b/crates/anodized/tests/default_output_pattern.rs @@ -12,6 +12,7 @@ fn sort_pair(pair: (i32, i32)) -> (i32, i32) { pair } +#[cfg(not(feature = "backend-no-checks"))] #[test] #[should_panic(expected = "Postcondition failed: | (a, b) | a <= b")] fn test_sort_fail_postcondition() { diff --git a/crates/anodized/tests/execution_order.rs b/crates/anodized/tests/execution_order.rs index bee18815..37703a2e 100644 --- a/crates/anodized/tests/execution_order.rs +++ b/crates/anodized/tests/execution_order.rs @@ -22,6 +22,7 @@ fn instrumented_function(log: &mut Vec<&'static str>) { log.push("body"); } +#[cfg(not(feature = "backend-no-checks"))] #[test] fn test_execution_order() { let mut log = Vec::new(); diff --git a/crates/anodized/tests/explicit_binding_in_postcondition.rs b/crates/anodized/tests/explicit_binding_in_postcondition.rs index 628f831a..ecfdb013 100644 --- a/crates/anodized/tests/explicit_binding_in_postcondition.rs +++ b/crates/anodized/tests/explicit_binding_in_postcondition.rs @@ -12,6 +12,7 @@ fn sort_pair(pair: (i32, i32)) -> (i32, i32) { (b, a) } +#[cfg(not(feature = "backend-no-checks"))] #[test] #[should_panic(expected = "Postcondition failed: | (a, b) | a <= b")] fn test_sort_fail_postcondition() { diff --git a/crates/anodized/tests/method_call_invariant.rs b/crates/anodized/tests/method_call_invariant.rs index f929390f..d85281fa 100644 --- a/crates/anodized/tests/method_call_invariant.rs +++ b/crates/anodized/tests/method_call_invariant.rs @@ -17,6 +17,7 @@ impl Validator { } } +#[cfg(not(feature = "backend-no-checks"))] #[test] #[should_panic(expected = "Post-invariant failed: self.is_valid()")] fn test_violates_post_invariant() { @@ -25,6 +26,7 @@ fn test_violates_post_invariant() { v.set_validity(false); } +#[cfg(not(feature = "backend-no-checks"))] #[test] #[should_panic(expected = "Pre-invariant failed: self.is_valid()")] fn test_violates_pre_invariant() { diff --git a/crates/anodized/tests/method_with_invariant.rs b/crates/anodized/tests/method_with_invariant.rs index 1bb08a50..3c5917a5 100644 --- a/crates/anodized/tests/method_with_invariant.rs +++ b/crates/anodized/tests/method_with_invariant.rs @@ -23,6 +23,7 @@ fn test_increment_success() { c.increment(); } +#[cfg(not(feature = "backend-no-checks"))] #[test] #[should_panic(expected = "Post-invariant failed: self.count <= self.capacity")] fn test_increment_violates_invariant() { @@ -33,6 +34,7 @@ fn test_increment_violates_invariant() { c.increment(); // This will make count 11, violating the invariant on exit. } +#[cfg(not(feature = "backend-no-checks"))] #[test] #[should_panic(expected = "Pre-invariant failed: self.count <= self.capacity")] fn test_increment_violates_pre_invariant() { diff --git a/crates/anodized/tests/multiple_conditions.rs b/crates/anodized/tests/multiple_conditions.rs index a5c1bc5a..bc06bb69 100644 --- a/crates/anodized/tests/multiple_conditions.rs +++ b/crates/anodized/tests/multiple_conditions.rs @@ -30,6 +30,7 @@ fn test_get_element_success() { buffer.get_element(1); } +#[cfg(not(feature = "backend-no-checks"))] #[test] #[should_panic(expected = "Precondition failed: ! self.locked")] fn test_get_element_panics_when_locked() { @@ -41,6 +42,7 @@ fn test_get_element_panics_when_locked() { buffer.get_element(1); } +#[cfg(not(feature = "backend-no-checks"))] #[test] #[should_panic(expected = "Precondition failed: index < self.items.len()")] fn test_get_element_panics_on_out_of_bounds() { diff --git a/crates/anodized/tests/rename_return_value.rs b/crates/anodized/tests/rename_return_value.rs index 454062cd..d52fe527 100644 --- a/crates/anodized/tests/rename_return_value.rs +++ b/crates/anodized/tests/rename_return_value.rs @@ -33,6 +33,7 @@ fn calculate_odd_result(output: i32) -> i32 { } } +#[cfg(not(feature = "backend-no-checks"))] #[test] #[should_panic(expected = "Postcondition failed: | result | * result % 2 == 0")] fn test_rename_panics_if_not_even() { From f52b13833d0f8dd3f9bb3de37c9d1c4069f231ee Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Mon, 22 Sep 2025 14:19:10 +0900 Subject: [PATCH 11/17] rename --- crates/anodized-core/src/backend/anodized/mod.rs | 2 +- .../src/backend/anodized/{test_instrument_fn.rs => test.rs} | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename crates/anodized-core/src/backend/anodized/{test_instrument_fn.rs => test.rs} (100%) diff --git a/crates/anodized-core/src/backend/anodized/mod.rs b/crates/anodized-core/src/backend/anodized/mod.rs index 02b912ae..51cffcea 100644 --- a/crates/anodized-core/src/backend/anodized/mod.rs +++ b/crates/anodized-core/src/backend/anodized/mod.rs @@ -1,5 +1,5 @@ #[cfg(test)] -mod test_instrument_fn; +mod test; use crate::Spec; diff --git a/crates/anodized-core/src/backend/anodized/test_instrument_fn.rs b/crates/anodized-core/src/backend/anodized/test.rs similarity index 100% rename from crates/anodized-core/src/backend/anodized/test_instrument_fn.rs rename to crates/anodized-core/src/backend/anodized/test.rs From 94ba0fa05ed18585cf1352bcba81c196c32cde89 Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Mon, 22 Sep 2025 14:24:58 +0900 Subject: [PATCH 12/17] test backend-native-contracts in CI --- .github/workflows/ci.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e5bf91cc..07c2a531 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -20,6 +20,8 @@ jobs: cargo-args: "" - backend: backend-no-checks cargo-args: "--features backend-no-checks" + - backend: backend-native-contracts + cargo-args: "--features backend-native-contracts" steps: - name: Checkout repository uses: actions/checkout@v4 From 56587ac37b2757d6384f582999f676821205ceb2 Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Mon, 22 Sep 2025 15:14:24 +0900 Subject: [PATCH 13/17] fix CI setup --- .github/workflows/ci.yml | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 07c2a531..c5e95106 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -17,11 +17,14 @@ jobs: matrix: include: - backend: default - cargo-args: "" + toolchain: "+stable" + feature: "" - backend: backend-no-checks - cargo-args: "--features backend-no-checks" + toolchain: "+stable" + feature: backend-no-checks - backend: backend-native-contracts - cargo-args: "--features backend-native-contracts" + toolchain: "+nightly" + feature: backend-native-contracts steps: - name: Checkout repository uses: actions/checkout@v4 @@ -29,5 +32,8 @@ jobs: - name: Install Rust toolchain uses: dtolnay/rust-toolchain@stable - - name: Cargo test feature `${{ matrix.backend }}` - run: cargo test --no-fail-fast ${{ matrix.cargo-args }} + - name: Install Rust toolchain + uses: dtolnay/rust-toolchain@nightly + + - name: Cargo test backend `${{ matrix.backend }}` + run: cargo ${{ matrix.toolchain }} test --no-fail-fast --features "${{ matrix.feature }}" From ee1c35b2c496432fed5cc18ecb38b62497d8a15e Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Mon, 22 Sep 2025 15:17:22 +0900 Subject: [PATCH 14/17] nit --- .github/workflows/ci.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index c5e95106..fdcc0a21 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -11,18 +11,18 @@ env: jobs: test: - name: Run tests with feature `${{ matrix.backend }}` + name: Run tests for backend `${{ matrix.backend }}` runs-on: ubuntu-latest strategy: matrix: include: - - backend: default + - backend: toolchain: "+stable" feature: "" - - backend: backend-no-checks + - backend: no-checks toolchain: "+stable" feature: backend-no-checks - - backend: backend-native-contracts + - backend: native-contracts toolchain: "+nightly" feature: backend-native-contracts steps: From cb6e56eb4269873ddbda877a695ea64731eb73e4 Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Mon, 22 Sep 2025 15:18:02 +0900 Subject: [PATCH 15/17] more nit --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index fdcc0a21..d2e7e696 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -16,7 +16,7 @@ jobs: strategy: matrix: include: - - backend: + - backend: default toolchain: "+stable" feature: "" - backend: no-checks From 357cd3d7044b57b75d3645b98337ab2cc9b25bca Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Mon, 22 Sep 2025 16:49:46 +0900 Subject: [PATCH 16/17] make it past some errors --- crates/anodized/tests/async_function.rs | 2 ++ crates/anodized/tests/basic_function.rs | 2 ++ 2 files changed, 4 insertions(+) diff --git a/crates/anodized/tests/async_function.rs b/crates/anodized/tests/async_function.rs index 3667ce7b..e1aac6a0 100644 --- a/crates/anodized/tests/async_function.rs +++ b/crates/anodized/tests/async_function.rs @@ -1,3 +1,5 @@ +#![cfg_attr(feature = "backend-native-contracts", feature(contracts))] + use anodized::spec; #[spec( diff --git a/crates/anodized/tests/basic_function.rs b/crates/anodized/tests/basic_function.rs index 683cfa57..c9482e3e 100644 --- a/crates/anodized/tests/basic_function.rs +++ b/crates/anodized/tests/basic_function.rs @@ -1,3 +1,5 @@ +#![cfg_attr(feature = "backend-native-contracts", feature(contracts))] + use anodized::spec; #[spec( From 4dccba63159146b65cff873b322c61d9f3605925 Mon Sep 17 00:00:00 2001 From: Mate Kovacs Date: Tue, 23 Sep 2025 01:07:20 +0900 Subject: [PATCH 17/17] check in simple_test.rs for sanity-checking the nightly contracts feature --- crates/anodized/tests/simple_test.rs | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 crates/anodized/tests/simple_test.rs diff --git a/crates/anodized/tests/simple_test.rs b/crates/anodized/tests/simple_test.rs new file mode 100644 index 00000000..2a8a51fa --- /dev/null +++ b/crates/anodized/tests/simple_test.rs @@ -0,0 +1,9 @@ +#![feature(contracts)] + +use core::contracts::*; + +#[requires(true)] +#[requires(true)] // This line causes an error. +#[ensures(|_| true)] +#[ensures(|_| true)] +fn some_function() {}