Unwind Attribute without Python Changes #846

jaisnan · 2022-02-19T05:29:55Z

Description of changes:

Adds Unwind Attribute without Python Changes. The kani-metadata.json file now has the following structure

{
    "proof_harnesses": [
        {
            "pretty_name": "harness",
            "mangled_name": "harness",
            "original_file": "/home/ubuntu/kani/tests/cargo-kani/simple-unwind-annotation/src/main.rs",
            "original_line": "17",
            "unwind_value": 10
        },
        {
            "pretty_name": "harness_2",
            "mangled_name": "harness_2",
            "original_file": "/home/ubuntu/kani/tests/cargo-kani/simple-unwind-annotation/src/main.rs",
            "original_line": "26",
            "unwind_value": null
        }
    ]
}

Given that the rust library looks like -

#[kani::proof]
#[kani::unwind(10)]
fn harness() {
...
}

#[kani::proof]
fn harness_2() {
...
}

Update - The PR has been updated to include handling for the following scenarios, all of which produce user errors which point to suggestions on how to fix the attribute.

#[kani::proof]
#[kani::unwind(10,5)]
fn harness_3() {
...
}

#[kani::unwind(8)]
fn harness_4() {
...
}

#[kani::proof]
#[kani::proof]
fn harness_5() {
...
}

#[kani::proof(some, argument2)]
fn harness_6() {
...
}

Resolved issues:

Resolves - partly #600 and #689.

Call-outs:

The scripting needs to parse the metadata file and apply the unwind value to the target function.

Testing:

How is this change tested? Somewhat
Is this a refactor change? No

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

library/kani_macros/src/lib.rs

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

adpaco-aws

Unwinding values should be part of the harness metadata and not a separate struct. For me it is okay to keep it a struct (not just a u32 value) since long term we want to support unwinding values for individual loops in addition to this one.

library/kani_macros/src/lib.rs

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

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

tests/kani/Unwind-Attribute/fixme_lib.rs

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

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

…wind-Attribute

jaisnan · 2022-03-01T05:12:15Z

Updated the PR as per suggestions.

library/kani_macros/src/lib.rs

adpaco-aws · 2022-03-01T18:46:57Z

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

+
+        // 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 {


These cases do not seem to overlap so I am not sure why you are using if-then-else statements here. I would also recommend handling them in small functions if possible.

They do overlap as it's necessary to check to how many proof attributes have been declared per harness and depending on the number, there's different handling that needs to happen. The entire function has a single purpose so it didn't seem necessary to factor it out into smaller functions.

@jaisnan, if I understand this code correctly, you are trying to restrict any other kani attribute to things that are tagged with the proof attribute, right?

If that is the case, I would recommend to change this to have something like the following structure:

let attrs: kani_attributes(self.tcx.get_attrs(instance.def_id())); // BTreeMap<&str, &rustc_ast::Attribute> if attrs.contains_key("proof") { // Handle attributes here. } else { if attrs.len() > 0 { // Warning: We currently only support attributes on proof harnesses. The attribute {} will be ignored. } }

So, I am trying to restrict it to kani attribute but also use count information for each of the attributes.

I think using a BTreeMap would prevent us from checking if there are duplicate attributes in the same harness or not. If someone calls two unwind annotations then, the last one is going to be read and parsed if we use a BTreeMap I think.

We ideally should not just check if a key exists but also how many instances of them. Maybe I can use a multimap? https://docs.rs/btreemultimap/latest/btreemultimap/ ? I think using two vectors and a match statement serves these purposes well enough. If we add more options as attributes, we'd just have to expand the match statement and add a handler and that's it.

Let's talk offline about this one. There are other things we can go to simplify the code.

adpaco-aws · 2022-03-01T18:48:57Z

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>,


I thought we agreed having a specific struct for unwind data where this would be an optional value. Also, Option<u32> should be enough.

A struct didn't seem necessary for now as we're just targeting a default value for the entire harness. The struct and related changes will be added with the changes to map each loop to it's own harness.

Maybe create a type alias here that we can extend later.

type UnwindMetadata = usize;

do we wantusize or u32/64. Doesnt usize tie the limit of the unwind value to the target architecture?

I suggested usize because that's usually used to restrict structure sizes, but in practice, I highly doubt someone is going to use a large unwind parameter. So u32 is fine too.

IMO stay an integer. Any future unwinding information (e.g. unwindset) can be provided in separate fields. We're never going to change unwind_value because it's just the thing we pass to cbmc as --unwind and that's it.

CBMC supports min and max unwind notation as well. But I do agree that if we are going to add a type, we should also change this to unwind.

Since min / max is an obvious extension here, maybe we should just add the struct and encode this as a map right away.

I don't know why any future support for those wouldn't just add an unwind_max_value as well. There doesn't seem to be a value to nesting it. We control the producer (kani-compiler) and consumer (cargo-kani) of this structure, so if it's looks like a mistake later, we can just fix it. So simplest choice seems best to me.

But I don't feel strongly about it.

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

adpaco-aws · 2022-03-01T18:51:19Z

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

+    }
+}
+
+// #[kani::proof]


Why is this commented code included? If there is a reason to, add a comment explaining why.

Can we change these to be UI tests that we ensure that Kani prints the correct error message?

tests/kani/Unwind-Attribute/fixme_lib.rs

…wind-Attribute

…to Unwind-Attribute

celinval

Thanks for doing this! I have a few suggestions to clean the code a bit. Let me know if you disagree with any of them. :)

celinval · 2022-03-01T20:56:10Z

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

+                format!("Please use '#kani[proof]' above the annotation {}", attribute_vector[0].0)
+                    .as_str(),
+            );
+        } else {


When do we expect to hit this else? Should we trigger an error?

When neither proof or any other attributes are used. This function handle_kanitool_attributes is called on all instances in codegen_function so raising an error might break a lot of cases. Hence, the empty handling.

Please, either remove the else or add a comment to explain what cases it is covering.

celinval · 2022-03-01T22:00:50Z

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

+
+        // 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 {


@jaisnan, if I understand this code correctly, you are trying to restrict any other kani attribute to things that are tagged with the proof attribute, right?

If that is the case, I would recommend to change this to have something like the following structure:

let attrs: kani_attributes(self.tcx.get_attrs(instance.def_id())); // BTreeMap<&str, &rustc_ast::Attribute> if attrs.contains_key("proof") { // Handle attributes here. } else { if attrs.len() > 0 { // Warning: We currently only support attributes on proof harnesses. The attribute {} will be ignored. } }

celinval · 2022-03-01T22:02:44Z

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

+    }
+}
+
+// #[kani::proof]


Can we change these to be UI tests that we ensure that Kani prints the correct error message?

library/kani_macros/src/lib.rs

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

celinval · 2022-03-01T22:18:43Z

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

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


maybe this should return Option<&str> since we keep converting it to &str.

Returning Option<&str> would return a dangling pointer as the original string would be destroyed once the function returns. We need to return an Owned String so I don't think we can replace the return type.
Reference - https://stackoverflow.com/questions/43079077/proper-way-to-return-a-new-string-in-rust

Indeed, I didn't notice that you changed the code to join the segments. For the original code, the return value would have the same lifetime as the argument attr.

BTW, why did you change it? This code might actually be doing the wrong thing. I.e., let's say you have the following attribute:

#[kanitool::type::sub_type]

I believe that you are going to return the string typesub_type.

Maybe so, but I don't see the need to modify it to potential future attributes when there's no clear consensus on what attributes we're planning on supporting. Imo we can always change this later to adapt to future annotations.

Let me check about the scenario you've posted however.

Talked offline, this is no longer needed. Going to revert the change.

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

celinval · 2022-03-02T08:33:27Z

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

+        // 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![];


BTW, shouldn't this be a boolean?

We need to maintain a count of the instances apart from the attributes themselves, hence vectors.

celinval

Here are some notes from our chat.

celinval · 2022-03-02T18:12:56Z

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

+        else if proof_attribute_vector.len() > 1 {
+            self.tcx
+                .sess
+                .span_err(proof_attribute_vector[0].span, "Only one Proof Attribute allowed");


Reduce this to warning.

celinval · 2022-03-02T18:31:40Z

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

+            _ => None,
+        }
+    }
+    // Return none if there are no unwind attributes or if there's too many unwind attributes


unwind comment in the generic function.

celinval · 2022-03-02T18:32:17Z

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

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


Anyway, not a biggie. Let's move on.

celinval · 2022-03-02T18:38:04Z

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

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


Talked offline, this is no longer needed. Going to revert the change.

…wind-Attribute

…to Unwind-Attribute

jaisnan · 2022-03-04T19:46:57Z

Removed no_mangle
Refactored the parsing into functions, added utility functions
Added documentation for all user cases
Added a test to check failure of harness assert instead of main.

…wind-Attribute

tedinski

Almost there!

tedinski · 2022-03-04T23:18:04Z

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;


was this necessary?

tedinski · 2022-03-04T23:18:58Z

library/kani_macros/src/lib.rs

+// 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.


Doc-comments in Rust use 3 /s not 2, check all your function comments for this.

tedinski · 2022-03-04T23:20:21Z

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

+        let attributes_list = self.tcx.get_attrs(self.current_fn().instance().def_id());
+        let (proof_attribute_vector, attribute_vector) = create_attribute_vectors(attributes_list);


Naming suggestion: don't put the type into the name really.

IMO, these names are clearer as "all_attributes" "proof_attributes" "other_attributes".

tedinski · 2022-03-04T23:23:30Z

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

+        if proof_attribute_count == 1 {
+            self.create_proof_harness(attribute_vector);
+        }


There's a very common programming convention to write functions like:

fn foo() { if error condition { // bail, whatever } if other error { // bail } // etc // no errors: the conventional, expected case. }

So try that. Spot errors, raise them and return. Then just unconditionally create_proof_harness at the end of the function (no need for any empty else). By following the convention, functions are usually a lot easier to read (if only because people expect it)

For the no-op case, can we now early return with the empty parenthesis?

tedinski · 2022-03-04T23:25:00Z

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

    /// 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 {


Function doc comment needs updating. Also, we should rename this, maybe. "default_kanitool_proof" maybe?

tedinski · 2022-03-04T23:25:44Z

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

+        // Check if some unwind value doesnt already exist
+        if harness.unwind_value.is_none() {


Same suggestion as previous comment on handling errors, then the expected case.

Going to wrap the behavior with a match statement.

tedinski · 2022-03-04T23:26:35Z

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

+                assert!(
+                    integer_value < u32::MAX.into(),
+                    "Value above maximum permitted value - u32::MAX"
+                );


Good call. But we might want to span_err instead of assert.

tedinski · 2022-03-04T23:27:05Z

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

+
+// Create two vectors, proof_vector and attribute_vector which seperates the list of attributes into
+// proof and non-proof for easier parsing
+fn create_attribute_vectors(


Rename partition_kanitool_attributes maybe?

Second suggestion: try improving the doc-comment enough that all the comments in the body aren't necessary anymore. This function is small enough this is possible and would very likely be an improvement.

tedinski · 2022-03-04T23:29:33Z

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

+        // 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_metadata = self.handle_kanitool_proof();
+        if attribute_vector.len() > 0 {


unnecessary if

tedinski · 2022-03-04T23:30:22Z

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

+                    "unwind" => {
+                        self.handle_kanitool_unwind(attribute_tuple.1, &mut harness_metadata)
+                    }
+                    _ => {}


maybe we could error or warn?

…wind-Attribute

…ation

tedinski · 2022-03-07T18:01:12Z

tests/ui/unsupported-annotation/main.rs

+}
+
+#[kani::proof]
+#[kani::test_annotation]


FYI: this isn't testing your code, you'd have to write kanitool:: for that

tedinski · 2022-03-07T18:02:23Z

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

+        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",


tedinski

Assuming CI passes, looks largely good. Maybe one last typo.

library/kani_macros/src/lib.rs

addressed changes requested

* Unwind Attribute without Python Changes

Unwind Attribute without Python Changes

9e2e1b1

jaisnan requested a review from a team as a code owner February 19, 2022 05:29

tedinski reviewed Feb 21, 2022

View reviewed changes

library/kani_macros/src/lib.rs Outdated Show resolved Hide resolved

library/kani_macros/src/lib.rs Outdated Show resolved Hide resolved

src/kani-compiler/rustc_codegen_kani/src/context/metadata.rs Outdated Show resolved Hide resolved

adpaco-aws suggested changes Feb 21, 2022

View reviewed changes

jaisnan added 5 commits February 23, 2022 15:46

Merge branch 'main' of https://github.com/model-checking/kani into Un…

89092cf

…wind-Attribute

Fixed metadata schema and addressed overuse issues

05f83b0

Added user error handling and documentation

da43716

Merge branch 'main' of https://github.com/model-checking/kani into Un…

5ca9856

…wind-Attribute

Fixed regression tests

3a2b8b0

Fix lib.rs comments

f4cd7ee

jaisnan requested review from tedinski and adpaco-aws March 1, 2022 15:14

adpaco-aws previously requested changes Mar 1, 2022

View reviewed changes

jaisnan and others added 5 commits March 1, 2022 13:52

Merge branch 'main' into Unwind-Attribute

3deac4e

Addressing PR documentation and review

d870bbe

Removing redundant fixme harnesses

52288e3

Merge branch 'main' of https://github.com/model-checking/kani into Un…

29b2820

…wind-Attribute

Merge branch 'Unwind-Attribute' of https://github.com/jaisnan/kani in…

4de691f

…to Unwind-Attribute

celinval reviewed Mar 1, 2022

View reviewed changes

jaisnan and others added 2 commits March 2, 2022 03:21

Addressing PR concerns and updating comments

f09c7f4

Merge branch 'main' into Unwind-Attribute

e4e69e9

celinval reviewed Mar 2, 2022

View reviewed changes

jaisnan added 3 commits March 4, 2022 19:28

Update PR with comments and refactoring

70f5685

Merge branch 'main' of https://github.com/model-checking/kani into Un…

192d189

…wind-Attribute

Merge branch 'Unwind-Attribute' of https://github.com/jaisnan/kani in…

08a40a3

…to Unwind-Attribute

jaisnan added 2 commits March 4, 2022 20:05

fixed regression tests

51b86ae

Merge branch 'main' of https://github.com/model-checking/kani into Un…

5715249

…wind-Attribute

jaisnan requested a review from adpaco-aws March 4, 2022 20:34

tedinski reviewed Mar 4, 2022

View reviewed changes

jaisnan added 2 commits March 7, 2022 16:24

Merge branch 'main' of https://github.com/model-checking/kani into Un…

ddc97dd

…wind-Attribute

Addressing PR Comments and changing conditional checking and document…

c661d9f

…ation

jaisnan requested a review from tedinski March 7, 2022 17:55

tedinski reviewed Mar 7, 2022

View reviewed changes

Update doc comments and error messages

e637963

tedinski approved these changes Mar 7, 2022

View reviewed changes

library/kani_macros/src/lib.rs Outdated Show resolved Hide resolved

fixing typo

a04b462

jaisnan merged commit 7152657 into model-checking:main Mar 7, 2022

jaisnan mentioned this pull request Apr 8, 2022

Enable Unwind Attribute from Parsing metadata files #1027

Closed

tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 22, 2022

Unwind Attribute without Python Changes (model-checking#846)

de996f0

* Unwind Attribute without Python Changes

tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 25, 2022

Unwind Attribute without Python Changes (model-checking#846)

8d4e6f9

* Unwind Attribute without Python Changes

tedinski pushed a commit to tedinski/rmc that referenced this pull request Apr 26, 2022

Unwind Attribute without Python Changes (model-checking#846)

b68e401

* Unwind Attribute without Python Changes

tedinski pushed a commit that referenced this pull request Apr 27, 2022

Unwind Attribute without Python Changes (#846)

63ed597

* Unwind Attribute without Python Changes

		let attributes_list = self.tcx.get_attrs(self.current_fn().instance().def_id());
		let (proof_attribute_vector, attribute_vector) = create_attribute_vectors(attributes_list);

		// Check if some unwind value doesnt already exist
		if harness.unwind_value.is_none() {

Unwind Attribute without Python Changes #846

Unwind Attribute without Python Changes #846

Conversation

jaisnan commented Feb 19, 2022 • edited Loading

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

adpaco-aws left a comment

Choose a reason for hiding this comment

jaisnan commented Mar 1, 2022

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jaisnan Mar 1, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

celinval Mar 2, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

celinval left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jaisnan Mar 1, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jaisnan Mar 2, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jaisnan Mar 2, 2022 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

celinval left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jaisnan commented Mar 4, 2022

tedinski left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tedinski left a comment

Choose a reason for hiding this comment

jaisnan commented Feb 19, 2022 •

edited

Loading

jaisnan Mar 1, 2022 •

edited

Loading

celinval Mar 2, 2022 •

edited

Loading

jaisnan Mar 1, 2022 •

edited

Loading

jaisnan Mar 2, 2022 •

edited

Loading

jaisnan Mar 2, 2022 •

edited

Loading