feat: backend-native-contracts

.github/workflows/ci.yml

@@ -11,21 +11,29 @@ 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
 
       - 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 }}"

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"

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<ItemFn> {
@@ -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),
     }
 }

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<ItemFn> {
+    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)
+}

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),
+    }
+}

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"

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

crates/anodized/tests/async_function.rs

@@ -1,3 +1,5 @@
+#![cfg_attr(feature = "backend-native-contracts", feature(contracts))]
+
 use anodized::spec;
 
 #[spec(

crates/anodized/tests/basic_function.rs

@@ -1,3 +1,5 @@
+#![cfg_attr(feature = "backend-native-contracts", feature(contracts))]
+
 use anodized::spec;
 
 #[spec(

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<i32>) {
     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<i32>) {
+    vec.push(42);
+}
+
 #[test]
 fn test_block_expressions() {
     let mut vec = vec![1, 2, 3];

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() {}