From c4ed7ec2848c91b019ca3726d16b80f78ca51415 Mon Sep 17 00:00:00 2001
From: "Celina G. Val" <celinval@amazon.com>
Date: Fri, 14 Apr 2023 10:56:01 -0700
Subject: [PATCH] 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 |  6 ++++++
 library/kani/src/lib.rs                     |  3 +++
 library/kani_macros/src/lib.rs              | 19 +++++++++++++++----
 3 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs
index 31cc7bd18f24..0b69b856940a 100644
--- a/kani-compiler/src/kani_middle/attributes.rs
+++ b/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
             },
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 5acd07d657ee..e82b57d35457 100644
--- a/library/kani/src/lib.rs
+++ b/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()`
diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs
index c3749daabd18..d54684cbff87 100644
--- a/library/kani_macros/src/lib.rs
+++ b/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);
 }