Add #[kani::unstable] attribute (#2373)

Add the #[unstable] attribute that will allow us to mark unstable APIs. This PR only adds the attributes and we still need to add the option to enable them and to error out if the user is trying to use an unstable item without explicitly opting-in.

kani-compiler/src/kani_middle/attributes.rs

@@ -26,6 +26,8 @@ enum KaniAttributeKind {
     ShouldPanic,
     Solver,
     Stub,
+    /// Attribute used to mark unstable APIs.
+    Unstable,
     Unwind,
 }
 
@@ -113,6 +115,10 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> Option<HarnessA
                             parse_unwind(tcx, expect_single(tcx, kind, &attributes))
                     }
                     KaniAttributeKind::Proof => harness.proof = true,
+                    KaniAttributeKind::Unstable => {
+                        // Internal attribute which shouldn't exist here.
+                        unreachable!()
+                    }
                 };
                 harness
             },

library/kani/src/lib.rs

@@ -1,6 +1,9 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+// Required so we can use kani_macros attributes.
+#![feature(register_tool)]
+#![register_tool(kanitool)]
 // Used for rustc_diagnostic_item.
 #![feature(rustc_attrs)]
 // This is required for the optimized version of `any_array()`

library/kani_macros/src/lib.rs

@@ -73,6 +73,15 @@ pub fn stub(attr: TokenStream, item: TokenStream) -> TokenStream {
 pub fn solver(attr: TokenStream, item: TokenStream) -> TokenStream {
     attr_impl::solver(attr, item)
 }
+
+/// Mark an API as unstable. This should only be used inside the Kani sysroot.
+/// See https://model-checking.github.io/kani/rfc/rfcs/0006-unstable-api.html for more details.
+#[doc(hidden)]
+#[proc_macro_attribute]
+pub fn unstable(attr: TokenStream, item: TokenStream) -> TokenStream {
+    attr_impl::unstable(attr, item)
+}
+
 /// Allow users to auto generate Arbitrary implementations by using `#[derive(Arbitrary)]` macro.
 #[proc_macro_error]
 #[proc_macro_derive(Arbitrary)]
@@ -176,9 +185,10 @@ mod sysroot {
     }
 
     kani_attribute!(should_panic, no_args);
-    kani_attribute!(unwind);
-    kani_attribute!(stub);
     kani_attribute!(solver);
+    kani_attribute!(stub);
+    kani_attribute!(unstable);
+    kani_attribute!(unwind);
 }
 
 /// This module provides dummy implementations of Kani attributes which cannot be interpreted by
@@ -207,7 +217,8 @@ mod regular {
     }
 
     no_op!(should_panic);
-    no_op!(unwind);
-    no_op!(stub);
     no_op!(solver);
+    no_op!(stub);
+    no_op!(unstable);
+    no_op!(unwind);
 }