Unwind Attribute without Python Changes

library/kani_macros/src/lib.rs

@@ -36,9 +36,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 +50,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()
+}
+
+// The attribute '#[kani::unwind(arg)]' can only be called alongside '#[kani::proof]'.
+// arg - Takes in a integer value (u32) that represents the unwind value for the harness.
+// Usage is restricted to proof harnesses only currently.
+#[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(arg)]
+    let insert_string = "#[kanitool::unwind(".to_owned() + &attr.clone().to_string() + ")]";
+    // Add the string that looks like - #[kanitool::unwind(arg)] to the tokenstream
+    result.extend(insert_string.parse::<TokenStream>().unwrap());
+
+    result.extend(item);
+    result
+}

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

@@ -8,9 +8,11 @@ use crate::codegen_cprover_gotoc::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;
+use std::convert::TryInto;
 use std::iter::FromIterator;
 use tracing::{debug, warn};
 
@@ -241,18 +243,54 @@ impl<'tcx> GotocCtx<'tcx> {
     /// Currently, this is only proof harness annotations.
     /// i.e. `#[kani::proof]` (which kani_macros translates to `#[kanitool::proof]` for us to handle here)
     fn handle_kanitool_attributes(&mut self) {
-        let instance = self.current_fn().instance();
+        let all_attributes = self.tcx.get_attrs(self.current_fn().instance().def_id());
+        let (proof_attributes, other_attributes) = partition_kanitool_attributes(all_attributes);
 
-        for attr in self.tcx.get_attrs(instance.def_id()) {
-            match kanitool_attr_name(attr).as_deref() {
-                Some("proof") => self.handle_kanitool_proof(),
-                _ => {}
+        // Early return with empty tuple for instances without any attributes declared
+        if proof_attributes.is_empty() && other_attributes.is_empty() {
+            return;
+        }
+        // User error handling for user cases where there's more than one proof attribute being called
+        if proof_attributes.len() > 1 {
+            self.tcx.sess.span_warn(proof_attributes[0].span, "Only one Proof Attribute allowed");
+            return;
+        }
+        // User error handling for the user case where there's an attribute being called without #kani::tool
+        if proof_attributes.is_empty() && !other_attributes.is_empty() {
+            self.tcx.sess.span_err(
+                other_attributes[0].1.span,
+                "Please use '#kani[proof]' above the annotation",
+            );
+            return;
+        }
+        // Create a proof harness if no user error has been triggered
+        self.create_proof_harness(other_attributes);
+    }
+
+    /// Create the proof harness struct using the handler methods for various attributes
+    fn create_proof_harness(&mut self, other_attributes: Vec<(String, &Attribute)>) {
+        // 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.
+        let mut harness = self.default_kanitool_proof();
+        // loop through all subsequent attributes
+        for attr in other_attributes.iter() {
+            // match with "unwind" attribute and provide the harness for modification
+            match attr.0.as_str() {
+                "unwind" => self.handle_kanitool_unwind(attr.1, &mut harness),
+                _ => {
+                    self.tcx.sess.span_err(
+                        attr.1.span,
+                        format!("Unsupported Annotation -> {}", attr.0.as_str()).as_str(),
+                    );
+                }
             }
         }
+        // Update `self` (the goto context) to add the current function as a listed proof harness
+        self.proof_harnesses.push(harness);
     }
 
-    /// Update `self` (the goto context) to add the current function as a listed proof harness
-    fn handle_kanitool_proof(&mut self) {
+    /// Handler to create the default proof harness and return
+    fn default_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 +301,100 @@ 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() {
+            // 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");
+            return;
+        }
+        // Get Attribute value and if it's not none, assign it to the metadata
+        match extract_integer_argument(attr) {
+            None => {
+                // There are no integers or too many integers given as argument to the annotatio
+                self.tcx
+                    .sess
+                    .span_err(attr.span, "Exactly one Unwind Argument as Integer accepted");
+                return;
+            }
+            Some(unwind_integer_value) => {
+                // Binding integer to u32
+                if unwind_integer_value >= u32::MAX.into() {
+                    self.tcx
+                        .sess
+                        .span_err(attr.span, "Value above maximum permitted value - u32::MAX");
+                    return;
+                }
+                // Expected case
+                harness.unwind_value = Some(unwind_integer_value.try_into().unwrap());
+            }
+        }
     }
 }
 
 /// 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())
         }
         _ => None,
     }
 }
+
+/// Create two vectors, proof_vector and attribute_vector which seperates the list of attributes into
+/// proof and non-proof for easier parsing
+fn partition_kanitool_attributes(
+    all_attributes: &[Attribute],
+) -> (Vec<&Attribute>, Vec<(String, &Attribute)>) {
+    // Vectors for storing instances of each attribute type,
+    // TODO: This can be modifed to use Enums when more options are provided
+    let mut proof_attributes = vec![];
+    let mut other_attributes = vec![];
+
+    // Loop through instances to get all "kanitool::x" attribute strings
+    for attr in all_attributes {
+        // 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_attributes.push(attr);
+            }
+            // Push to attribute vector that can be expanded to a map when more options become available
+            else {
+                other_attributes.push((attribute_string.to_string(), attr));
+            }
+        }
+    }
+
+    (proof_attributes, other_attributes)
+}
+
+/// Extracts the integer value argument from the any attribute provided
+fn extract_integer_argument(attr: &Attribute) -> Option<u128> {
+    // Vector of meta items , that contain metadata about the annotation
+    let attr_args = attr.meta_item_list().map(|x| x.to_vec())?;
+    // Only extracts one integer value as argument
+    if attr_args.len() == 1 {
+        // Returns the integer value that's the argument for the attribute
+        let x = attr_args[0].literal()?;
+        match x.kind {
+            LitKind::Int(y, ..) => Some(y),
+            _ => None,
+        }
+    }
+    // Return none if there are no attributes or if there's too many attributes
+    else {
+        None
+    }
+}

src/kani-compiler/src/codegen_cprover_gotoc/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<u32>,
 }
 
 /// 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,13 @@
+# 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"
+function = "harness"

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

@@ -0,0 +1 @@
+[harness.assertion.2] line 21 assertion failed: counter < 10: FAILURE

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

@@ -0,0 +1,32 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --function harness
+
+// 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(9)]
+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);
+    }
+}

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
+
+// kani-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);
+    }
+}

tests/ui/arguments-proof/expected

@@ -0,0 +1,6 @@
+  --> main.rs:13:1
+   |
+13 | #[kani::proof(some, argument2)]
+   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+   |
+   = help: message: #[kani::proof] does not take any arguments

tests/ui/arguments-proof/main.rs

@@ -0,0 +1,20 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --no-unwinding-checks
+
+// This test is to check Kani's error handling for harnesses that have proof attributes
+// with arguments when the expected declaration takes no arguments.
+
+fn main() {
+    assert!(1 == 2);
+}
+
+#[kani::proof(some, argument2)]
+fn harness() {
+    let mut counter = 0;
+    loop {
+        counter += 1;
+        assert!(counter < 10);
+    }
+}

tests/ui/multiple-proof-attributes/expected

@@ -0,0 +1,9 @@
+warning: Only one Proof Attribute allowed
+  --> main.rs:14:1
+   |
+14 | #[kani::proof]
+   | ^^^^^^^^^^^^^^
+   |
+   = note: this warning originates in the attribute macro `kani::proof` (in Nightly builds, run with -Z macro-backtrace for more info)
+
+warning: 1 warning emitted

tests/ui/multiple-proof-attributes/main.rs

@@ -0,0 +1,21 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --no-unwinding-checks --verbose
+
+// This test is to check Kani's error handling for harnesses that have multiple proof annotations
+// declared.
+
+fn main() {
+    assert!(1 == 2);
+}
+
+#[kani::proof]
+#[kani::proof]
+fn harness() {
+    let mut counter = 0;
+    loop {
+        counter += 1;
+        assert!(counter < 10);
+    }
+}

tests/ui/unsupported-annotation/expected

@@ -0,0 +1,7 @@
+error[E0433]: failed to resolve: could not find `test_annotation` in `kani`
+  --> main.rs:14:9
+   |
+14 | #[kani::test_annotation]
+   |         ^^^^^^^^^^^^^^^ could not find `test_annotation` in `kani`
+
+error: aborting due to previous error

tests/ui/unsupported-annotation/main.rs

@@ -0,0 +1,21 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// kani-flags: --no-unwinding-checks --verbose
+
+// This test is to check Kani's error handling for harnesses that have multiple proof annotations
+// declared.
+
+fn main() {
+    assert!(1 == 2);
+}
+
+#[kani::proof]
+#[kani::test_annotation]
+fn harness() {
+    let mut counter = 0;
+    loop {
+        counter += 1;
+        assert!(counter < 10);
+    }
+}

tests/ui/unwind-multiple-arguments/expected

@@ -0,0 +1,5 @@
+error: Exactly one Unwind Argument as Integer accepted
+  --> main.rs:14:1
+   |
+14 | #[kani::unwind(10,5)]
+   | ^^^^^^^^^^^^^^^^^^^^^