diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e5bf91cc..d2e7e696 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -11,15 +11,20 @@ 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 - cargo-args: "" - - backend: backend-no-checks - cargo-args: "--features backend-no-checks" + toolchain: "+stable" + feature: "" + - backend: no-checks + toolchain: "+stable" + feature: backend-no-checks + - backend: native-contracts + toolchain: "+nightly" + feature: backend-native-contracts steps: - name: Checkout repository uses: actions/checkout@v4 @@ -27,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 }}" 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/mod.rs b/crates/anodized-core/src/backend/mod.rs index 6b153e7f..fc5679d7 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 native_contracts; use syn::ItemFn; @@ -10,6 +11,8 @@ pub enum Backend { Default, /// Anodized instrumentation with no runtime checks. NoChecks, + /// 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,5 +39,6 @@ pub fn handle_fn(backend: Backend, spec: Spec, mut func: ItemFn) -> syn::Result< match backend { Backend::Default | Backend::NoChecks => Ok(func), + Backend::NativeContracts => native_contracts::instrument_fn(&spec, func), } } diff --git a/crates/anodized-core/src/backend/native_contracts/mod.rs b/crates/anodized-core/src/backend/native_contracts/mod.rs new file mode 100644 index 00000000..10e14058 --- /dev/null +++ b/crates/anodized-core/src/backend/native_contracts/mod.rs @@ -0,0 +1,65 @@ +#[cfg(test)] +mod tests; + +use crate::Spec; + +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, core::contracts::requires(#expr))] } + } else { + parse_quote! { #[core::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, core::contracts::requires(#expr))] } + } else { + 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, core::contracts::ensures(#ensures_closure))] } + } else { + parse_quote! { #[core::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, core::contracts::ensures(#closure))] } + } else { + parse_quote! { #[core::contracts::ensures(#closure)] } + }; + attrs.push(attr); + } + + attrs.extend(func.attrs); + func.attrs = attrs; + + Ok(func) +} diff --git a/crates/anodized-core/src/backend/native_contracts/tests.rs b/crates/anodized-core/src/backend/native_contracts/tests.rs new file mode 100644 index 00000000..bd22444a --- /dev/null +++ b/crates/anodized-core/src/backend/native_contracts/tests.rs @@ -0,0 +1,113 @@ +use super::*; + +use crate::test_util::assert_tokens_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! { fn demo() {} }; + + let expected: ItemFn = parse_quote! { + #[core::contracts::requires(CONDITION)] + #func + }; + + let observed = instrument_fn(&spec, func).unwrap(); + + assert_tokens_eq(&observed, &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 expected: ItemFn = parse_quote! { + #[cfg_attr(SETTING, core::contracts::requires(CONDITION))] + #func + }; + + let observed = instrument_fn(&spec, func).unwrap(); + + assert_tokens_eq(&observed, &expected); +} + +#[test] +fn maintains_emits_requires_and_ensures_attributes() { + let spec: Spec = parse_quote! { + maintains: CONDITION, + }; + let func: ItemFn = parse_quote! { fn demo() {} }; + + let expected: ItemFn = parse_quote! { + #[core::contracts::requires(CONDITION)] + #[core::contracts::ensures(|_| CONDITION)] + #func + }; + + let observed = instrument_fn(&spec, func).unwrap(); + + assert_tokens_eq(&observed, &expected); +} + +#[test] +fn ensures_from_expression_uses_generated_closure() { + let spec: Spec = parse_quote! { + binds: PATTERN_1, + ensures: CONDITION_1, + ensures: |PATTERN_2| CONDITION_2, + }; + let func: ItemFn = parse_quote! { fn demo() {} }; + + let expected: ItemFn = parse_quote! { + #[core::contracts::ensures(|PATTERN_1| CONDITION_1)] + #[core::contracts::ensures(|PATTERN_2| CONDITION_2)] + #func + }; + + let observed = instrument_fn(&spec, func).unwrap(); + + assert_tokens_eq(&observed, &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 expected: ItemFn = parse_quote! { + #[core::contracts::requires(CONDITION)] + #func + }; + + let observed = instrument_fn(&spec, func).unwrap(); + + assert_tokens_eq(&observed, &expected); +} + +#[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 a229947c..29ed4b84 100644 --- a/crates/anodized/Cargo.toml +++ b/crates/anodized/Cargo.toml @@ -15,12 +15,14 @@ proc-macro = true [features] backend-no-checks = [] +backend-native-contracts = [] [dependencies] 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 cad2402b..5d0ef2dd 100644 --- a/crates/anodized/src/lib.rs +++ b/crates/anodized/src/lib.rs @@ -12,13 +12,20 @@ use anodized_core::{ }; const _: () = { - let count: u32 = cfg!(feature = "backend-no-checks") as u32; + let count: u32 = cfg!(feature = "backend-no-checks") as u32 + + cfg!(feature = "backend-native-contracts") as u32; if count > 1 { panic!("anodized: backend features are mutually exclusive"); } }; -const BACKEND: Backend = if cfg!(feature = "backend-no-checks") { +#[rustversion::not(nightly)] +#[cfg(feature = "backend-native-contracts")] +compile_error!("the `backend-native-contracts` feature requires a nightly Rust toolchain"); + +const BACKEND: Backend = if cfg!(feature = "backend-native-contracts") { + Backend::NativeContracts +} else if cfg!(feature = "backend-no-checks") { Backend::NoChecks } else { Backend::Default 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( diff --git a/crates/anodized/tests/block_expressions.rs b/crates/anodized/tests/block_expressions.rs index 4cf22821..89ea96b4 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-native-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-native-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]; 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() {}