Unwind Attribute without Python Changes

library/kani_macros/src/lib.rs

@@ -9,6 +9,7 @@
 //   RUSTFLAGS="-Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(kanitool)"
 
 // proc_macro::quote is nightly-only, so we'll cobble things together instead
+extern crate proc_macro;
 use proc_macro::TokenStream;
 
 #[cfg(all(not(kani), not(test)))]
@@ -36,9 +37,10 @@ pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream {
 
 #[cfg(kani)]
 #[proc_macro_attribute]
-pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream {
+pub fn proof(attr: TokenStream, item: TokenStream) -> TokenStream {
     let mut result = TokenStream::new();
 
+    assert!(attr.to_string().len() == 0, "#[kani::proof] does not take any arguments");
     result.extend("#[kanitool::proof]".parse::<TokenStream>().unwrap());
     // no_mangle is a temporary hack to make the function "public" so it gets codegen'd
     result.extend("#[no_mangle]".parse::<TokenStream>().unwrap());
@@ -49,3 +51,27 @@ pub fn proof(_attr: TokenStream, item: TokenStream) -> TokenStream {
     //     $item
     // )
 }
+
+#[cfg(not(kani))]
+#[proc_macro_attribute]
+pub fn unwind(_attr: TokenStream, _item: TokenStream) -> TokenStream {
+    // This code is never called by default as the config value is set to kani
+    TokenStream::new()
+}
+
+#[cfg(kani)]
+#[proc_macro_attribute]
+pub fn unwind(attr: TokenStream, item: TokenStream) -> TokenStream {
+    let mut result = TokenStream::new();
+
+    // Translate #[kani::unwind(arg)] to #[kanitool::unwind(8)]
+    let insert_string = "#[kanitool::unwind(".to_owned() + &attr.clone().to_string() + ")]";
+
+    // Add the string that looks like - #[kanitool::unwindvalue]
+    result.extend(insert_string.parse::<TokenStream>().unwrap());
+    // No mangle seems to be necessary as removing it prevents all the attributes in a lib from being read
+    result.extend("#[no_mangle]".parse::<TokenStream>().unwrap());
+
+    result.extend(item);
+    result
+}

src/kani-compiler/rustc_codegen_kani/src/codegen/function.rs

@@ -8,6 +8,7 @@ use crate::GotocCtx;
 use cbmc::goto_program::{Expr, Stmt, Symbol};
 use cbmc::InternString;
 use rustc_ast::ast;
+use rustc_ast::{Attribute, LitKind};
 use rustc_middle::mir::{HasLocalDecls, Local};
 use rustc_middle::ty::{self, Instance};
 use std::collections::BTreeMap;
@@ -243,16 +244,65 @@ impl<'tcx> GotocCtx<'tcx> {
     fn handle_kanitool_attributes(&mut self) {
         let instance = self.current_fn().instance();
 
+        // Vectors for storing instances of each attribute type,
+        // TODO: This can be modifed to use Enums when more options are provided
+        let mut attribute_vector = vec![];
+        let mut proof_attribute_vector = vec![];
+
+        // Loop through instances to get all "kanitool::x" attribute strings
         for attr in self.tcx.get_attrs(instance.def_id()) {
-            match kanitool_attr_name(attr).as_deref() {
-                Some("proof") => self.handle_kanitool_proof(),
-                _ => {}
+            // Get the string the appears after "kanitool::" in each attribute string.
+            // Ex - "proof" | "unwind" etc.
+            if let Some(attribute_string) = kanitool_attr_name(attr).as_deref() {
+                // Push to proof vector
+                if attribute_string == "proof" {
+                    proof_attribute_vector.push(attr);
+                }
+                // Push to attribute vector that can be expanded to a map when more options become available
+                else {
+                    attribute_vector.push((attribute_string.to_string(), attr));
+                }
             }
         }
+
+        // In the case when there's only one proof attribute (correct behavior), create harness and modify it
+        // depending on each subsequent attribute that's being called by the user.
+        if proof_attribute_vector.len() == 1 {
+            let mut harness_metadata = self.handle_kanitool_proof();
+            if attribute_vector.len() > 0 {
+                // loop through all subsequent attributes
+                for attribute_tuple in attribute_vector.iter() {
+                    // match with "unwind" attribute and provide the harness for modification
+                    match attribute_tuple.0.as_str() {
+                        "unwind" => {
+                            self.handle_kanitool_unwind(attribute_tuple.1, &mut harness_metadata)
+                        }
+                        _ => {}
+                    }
+                }
+            }
+            // self.proof_harnesses contains the final metadata that's to be parsed
+            self.proof_harnesses.push(harness_metadata);
+        }
+        // User error handling for when there's more than one proof attribute being called
+        else if proof_attribute_vector.len() > 1 {
+            self.tcx
+                .sess
+                .span_err(proof_attribute_vector[0].span, "Only one Proof Attribute allowed");
+        }
+        // User error handling for when there's an attribute being called without #kani::tool
+        else if proof_attribute_vector.len() == 0 && attribute_vector.len() > 0 {
+            self.tcx.sess.span_err(
+                attribute_vector[0].1.span,
+                format!("Please use '#kani[proof]' above the annotation {}", attribute_vector[0].0)
+                    .as_str(),
+            );
+        } else {
+        }
     }
 
     /// Update `self` (the goto context) to add the current function as a listed proof harness
-    fn handle_kanitool_proof(&mut self) {
+    fn handle_kanitool_proof(&mut self) -> HarnessMetadata {
         let current_fn = self.current_fn();
         let pretty_name = current_fn.readable_name().to_owned();
         let mangled_name = current_fn.name();
@@ -263,20 +313,64 @@ impl<'tcx> GotocCtx<'tcx> {
             mangled_name,
             original_file: loc.filename().unwrap(),
             original_line: loc.line().unwrap().to_string(),
+            unwind_value: None,
         };
 
-        self.proof_harnesses.push(harness);
+        harness
+    }
+
+    /// Unwind strings of the format 'unwind_x' and the mangled names are to be parsed for the value 'x'
+    fn handle_kanitool_unwind(&mut self, attr: &Attribute, harness: &mut HarnessMetadata) {
+        // Check if some unwind value doesnt already exist
+        if harness.unwind_value.is_none() {
+            // Get Attribute value and if it's not none, assign it to the metadata
+            if let Some(integer_value) = extract_integer_argument(attr) {
+                harness.unwind_value = Some(integer_value);
+            } else {
+                // Show an Error if there is no integer value assigned to the integer or there's too many values assigned to the annotation
+                self.tcx
+                    .sess
+                    .span_err(attr.span, "Exactly one Unwind Argument as Integer accepted");
+            }
+        } else {
+            // User warning for when there's more than one unwind attribute, in this case, only the first value will be
+            self.tcx.sess.span_err(attr.span, "Use only one Unwind Annotation per Harness");
+        }
     }
 }
 
 /// If the attribute is named `kanitool::name`, this extracts `name`
 fn kanitool_attr_name(attr: &ast::Attribute) -> Option<String> {
     match &attr.kind {
         ast::AttrKind::Normal(ast::AttrItem { path: ast::Path { segments, .. }, .. }, _)
-            if segments.len() == 2 && segments[0].ident.as_str() == "kanitool" =>
+            if (!segments.is_empty()) && segments[0].ident.as_str() == "kanitool" =>
         {
-            Some(segments[1].ident.as_str().to_string())
+            let mut new_string = String::new();
+            for index in 1..segments.len() {
+                new_string.push_str(segments[index].ident.as_str());
+            }
+            Some(new_string)
         }
         _ => None,
     }
 }
+
+/// Extracts the integer value argument from the unwind attribute
+fn extract_integer_argument(attr: &Attribute) -> Option<u128> {
+    // Vector of meta items , that contain metadata about the annotation
+    let attr_args = attr.meta().and_then(|x| x.meta_item_list().map(|x| x.to_vec()))?;
+
+    // Only accept unwind attributes with one integer value as argument
+    if attr_args.len() == 1 {
+        // Returns the integer value that's the argument for the unwind
+        let x = attr_args[0].literal()?;
+        match x.kind {
+            LitKind::Int(y, ..) => Some(y),
+            _ => None,
+        }
+    }
+    // Return none if there are no unwind attributes or if there's too many unwind attributes
+    else {
+        None
+    }
+}

src/kani-compiler/rustc_codegen_kani/src/context/goto_ctx.rs

@@ -15,9 +15,9 @@
 //! this structure as input.
 use super::current_fn::CurrentFnCtx;
 use super::metadata::HarnessMetadata;
-use super::vtable_ctx::VtableCtx;
 use crate::overrides::{fn_hooks, GotocHooks};
 use crate::utils::full_crate_name;
+use crate::VtableCtx;
 use cbmc::goto_program::{DatatypeComponent, Expr, Location, Stmt, Symbol, SymbolTable, Type};
 use cbmc::utils::aggr_tag;
 use cbmc::{InternStringOption, InternedString, NO_PRETTY_NAME};

src/kani-compiler/rustc_codegen_kani/src/context/metadata.rs

@@ -17,6 +17,8 @@ pub struct HarnessMetadata {
     pub original_file: String,
     /// The line in that file where the proof harness begins
     pub original_line: String,
+    /// Optional data to store unwind value
+    pub unwind_value: Option<u128>,
 }
 
 /// The structure of `.kani-metadata.json` files, which are emitted for each crate

tests/cargo-kani/simple-proof-annotation/Cargo.toml

@@ -9,4 +9,4 @@ edition = "2021"
 [dependencies]
 
 [kani.flags]
-output-format = "old"
+output-format = "old"

tests/cargo-kani/simple-unwind-annotation/Cargo.toml

@@ -0,0 +1,12 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "simple-unwind-annotation"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+
+[kani.flags]
+output-format = "old"

tests/cargo-kani/simple-unwind-annotation/main.expected

@@ -0,0 +1 @@
+line 12 assertion failed: 1 == 2: FAILURE

tests/cargo-kani/simple-unwind-annotation/src/main.rs

@@ -0,0 +1,82 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// rmc-flags: --no-unwinding-checks
+
+// The expected file presently looks for "1 == 2" above.
+// But eventually this test may start to fail as we might stop regarding 'main'
+// as a valid proof harness, since it isn't annotated as such.
+// This test should be updated if we go that route.
+
+fn main() {
+    assert!(1 == 2);
+}
+
+#[kani::proof]
+#[kani::unwind(10)]
+fn harness() {
+    let mut counter = 0;
+    loop {
+        counter += 1;
+        assert!(counter < 10);
+    }
+}
+
+#[kani::proof]
+fn harness_2() {
+    let mut counter = 0;
+    loop {
+        counter += 1;
+        assert!(counter < 10);
+    }
+}
+
+// NOTE: These are potentially all scenarios that produce user errors. Uncomment each harness to test how the user error
+// looks like.
+
+// #[kani::proof]
+// #[kani::unwind(10,5)]
+// fn harness_3() {
+//     let mut counter = 0;
+//     loop {
+//         counter += 1;
+//         assert!(counter < 10);
+//     }
+// }
+
+// #[kani::unwind(8)]
+// fn harness_4() {
+//     let mut counter = 0;
+//     for i in 0..7 {
+//         counter += 1;
+//         assert!(counter < 5);
+//     }
+// }
+
+// #[kani::proof]
+// #[kani::proof]
+// fn harness_5() {
+//     let mut counter = 0;
+//     loop {
+//         counter += 1;
+//         assert!(counter < 10);
+//     }
+// }
+
+// #[kani::proof(some, argument2)]
+// fn harness_6() {
+//     let mut counter = 0;
+//     loop {
+//         counter += 1;
+//         assert!(counter < 10);
+//     }
+// }
+
+// // #[kani::unwind(9)]
+// // fn harness_7() {
+// //     let mut counter = 0;
+// //     for i in 0..10 {
+// //         counter += 1;
+// //         assert!(counter < 8);
+// //     }
+// // }

tests/kani/Unwind-Attribute/fixme_lib.rs

@@ -0,0 +1,21 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// rmc-flags: --no-unwinding-checks
+
+// Added to fix me because there are no tests for the annotations themselves.
+// TODO : The unwind value needs to be parsed and the unwind needs to be applied to each harness, we do not test this behavior yet.
+
+fn main() {
+    assert!(1 == 2);
+}
+
+#[kani::proof]
+#[kani::unwind(10)]
+fn harness() {
+    let mut counter = 0;
+    loop {
+        counter += 1;
+        assert!(counter < 10);
+    }
+}