Feature : Unwind attribute #1031

jaisnan · 2022-04-11T18:48:38Z

Description of changes:

Cargo-kani and kani do not have the unwind attribute enabled as a feature, this PR enables kani and cargo-kani to read from the metadata and use the unwind attribute.

Tests explicitly pass the unwind value in the flags. with these changes, we can just use the attribute over the harnesses.

Resolved issues:

Resolves #1027

Testing:

How is this change tested? Tests changed to use the unwind attribute

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.

…able-unwind-attribute

celinval

I have a few questions.

Will the command line option --unwind and the property file unwind flag still work?
If so, which one takes precedence?

We should make sure we add tests that cover those cases.

src/cargo-kani/src/metadata.rs

src/cargo-kani/src/call_cbmc_viewer.rs

jaisnan · 2022-04-11T19:04:12Z

I have a few questions.
1. Will the command line option `--unwind` and the property file `unwind` flag still work?

2. If so, which one takes precedence?
We should make sure we add tests that cover those cases.

Thanks for the callout, for now, the flags or the property file values for unwind have been disabled (we can enable them if we want). i didn't know which one should take preference over the other so I disabled the flag for now to prevent confusion.

imo, we should either disable the command line flag or make it have preference over the attribute value. Allowing the command line argument but having it be low preference doesnt make much sense to me.

Would like to know thoughts on how to proceed.

tedinski · 2022-04-11T19:10:32Z

Ah yeah, there are some options for that behavior aren't there?

Since we now run all proof harnesses by default, I propose: (1) We always use the unwind flag on the proof harness if present. (2) if not present, only then do we pay attention to the global command line flag. In short, the command line only sets the global default, a flag on the harness always has precedence.

This might be unexpected behavior if people expect to be able to override the unwind flag from the command line however, but I think that would only make sense to do in some circumstances (like if they've also provided --harness so they're only running one harness?). My vote is for ignoring this case for now and let's see what happens or if customers get confused or want the override behavior?

jaisnan · 2022-04-11T19:14:44Z

Ah yeah, there are some options for that behavior aren't there?

Since we now run all proof harnesses by default, I propose: (1) We always use the unwind flag on the proof harness if present. (2) if not present, only then do we pay attention to the global command line flag. In short, the command line only sets the global default, a flag on the harness always has precedence.

This might be unexpected behavior if people expect to be able to override the unwind flag from the command line however, but I think that would only make sense to do in some circumstances (like if they've also provided --harness so they're only running one harness?). My vote is for ignoring this case for now and let's see what happens or if customers get confused or want the override behavior?

This behavior makes more sense to me now than the one I proposed. command line value for the global value; and attribute value for each harnesses (which should be higher in hierarchy as it's more specific as a request from the user) @celinval, any thoughts?

adpaco-aws

Documentation must be updated to describe the feature, and whatever behavior you agree on for precedence should be noted there as well.

In my opinion, we should not be silent about conflicts and emit a user warning in this scenario (regardless of preference). Otherwise users could become really confused.

adpaco-aws · 2022-04-11T19:26:28Z

tests/ui/check_operations/operations.rs

 extern crate kani;

 use kani::any;

 #[kani::proof]
+#[kani::unwind(3)]
+


Remove newline?

celinval · 2022-04-11T20:00:21Z

IMO, the precedence order should be command line, harness attribute, configuration file. That said, I think it will be hard to implement this today given how we merge the configuration file options with the command line one.

I'm OK with @tedinski 's suggestion but I also agree with @adpaco-aws that we shouldn't be silent about any conflict. My suggestion is to do the following:

Introduce a --default-unwind option if we want to have a weaker behavior that allows harnesses annotations to have higher precedence.
Only allow --unwind in conjunction with --harness. In this case, the command line option would have higher precedence.

jaisnan · 2022-04-11T20:15:44Z

IMO, the precedence order should be command line, harness attribute, configuration file. That said, I think it will be hard to implement this today given how we merge the configuration file options with the command line one.

I'm OK with @tedinski 's suggestion but I also agree with @adpaco-aws that we shouldn't be silent about any conflict. My suggestion is to do the following:
1. Introduce a `--default-unwind` option if we want to have a weaker behavior that allows harnesses annotations to have higher precedence.

2. Only allow `--unwind` in conjunction with `--harness`. In this case, the command line option would have higher precedence.

Alright, this is what I'll implement. Thanks for your inputs everyone.

…able-unwind-attribute

adpaco-aws

Documentation is being added in #1087

tedinski

There's a couple of stray changes that should be cleaned up, but the main thing is the testing.

docs/src/tutorial/arbitrary-variables/Cargo.toml

docs/src/tutorial/loops-unwinding/Cargo.toml

src/kani-driver/src/args.rs

src/kani-driver/src/call_cbmc.rs

src/kani-driver/src/metadata.rs

src/kani-driver/src/args.rs

src/kani-driver/src/metadata.rs

…able-unwind-attribute

Addressing in #1087

* Hook up unwind attribute to Kani * Add tests and make Harness, a required argument * Refactor tests and replace --unwind with --default-unwind

jaisnan added 3 commits April 11, 2022 15:19

Hook up unwind attribute to Kani

716bad7

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

205b8b9

…able-unwind-attribute

Change tests to use unwind attribute

25c6bd3

jaisnan requested a review from a team as a code owner April 11, 2022 18:48

celinval reviewed Apr 11, 2022

View reviewed changes

src/cargo-kani/src/metadata.rs Outdated Show resolved Hide resolved

tedinski reviewed Apr 11, 2022

View reviewed changes

src/cargo-kani/src/call_cbmc_viewer.rs Outdated Show resolved Hide resolved

adpaco-aws previously requested changes Apr 11, 2022

View reviewed changes

jaisnan added 8 commits April 14, 2022 18:27

Checkpoint before bug bash

7763419

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

ecb8d2d

…able-unwind-attribute

Fix regression tests

478cb99

checkpoint-1

d53833f

Add tests and make Harness, a required argument

26ff7a5

rename expected file

e5b1eba

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

fbce977

…able-unwind-attribute

Replace --default-unwind with --unwind

c831e29

jaisnan requested a review from adpaco-aws April 21, 2022 14:35

adpaco-aws reviewed Apr 21, 2022

View reviewed changes

adpaco-aws self-requested a review April 21, 2022 15:35

tedinski reviewed Apr 21, 2022

View reviewed changes

jaisnan added 2 commits April 21, 2022 21:19

Refactor tests and replace --unwind with --default-unwind

f992db1

Remove empty spaces

4947380

tedinski reviewed Apr 21, 2022

View reviewed changes

src/kani-driver/src/args.rs Outdated Show resolved Hide resolved

src/kani-driver/src/args.rs Outdated Show resolved Hide resolved

src/kani-driver/src/metadata.rs Outdated Show resolved Hide resolved

src/kani-driver/src/metadata.rs Outdated Show resolved Hide resolved

jaisnan added 2 commits April 21, 2022 21:42

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

a9b59a7

…able-unwind-attribute

Address review comments

2efaea0

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

35029fa

…able-unwind-attribute

tedinski approved these changes Apr 21, 2022

View reviewed changes

jaisnan merged commit 36bb27c into model-checking:main Apr 21, 2022

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

Feature : Unwind attribute (model-checking#1031)

fc720a6

* Hook up unwind attribute to Kani * Add tests and make Harness, a required argument * Refactor tests and replace --unwind with --default-unwind

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

Feature : Unwind attribute (model-checking#1031)

ba20251

* Hook up unwind attribute to Kani * Add tests and make Harness, a required argument * Refactor tests and replace --unwind with --default-unwind

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

Feature : Unwind attribute (model-checking#1031)

2e33085

* Hook up unwind attribute to Kani * Add tests and make Harness, a required argument * Refactor tests and replace --unwind with --default-unwind

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

Feature : Unwind attribute (#1031)

23472fc

* Hook up unwind attribute to Kani * Add tests and make Harness, a required argument * Refactor tests and replace --unwind with --default-unwind

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Feature : Unwind attribute #1031

Feature : Unwind attribute #1031

jaisnan commented Apr 11, 2022 •

edited

Loading

celinval left a comment

jaisnan commented Apr 11, 2022 •

edited

Loading

tedinski commented Apr 11, 2022

jaisnan commented Apr 11, 2022 •

edited

Loading

adpaco-aws left a comment

adpaco-aws Apr 11, 2022

celinval commented Apr 11, 2022 •

edited

Loading

jaisnan commented Apr 11, 2022

adpaco-aws left a comment

tedinski left a comment

Feature : Unwind attribute #1031

Feature : Unwind attribute #1031

Conversation

jaisnan commented Apr 11, 2022 • edited Loading

Description of changes:

Resolved issues:

Testing:

Checklist

celinval left a comment

Choose a reason for hiding this comment

jaisnan commented Apr 11, 2022 • edited Loading

tedinski commented Apr 11, 2022

jaisnan commented Apr 11, 2022 • edited Loading

adpaco-aws left a comment

Choose a reason for hiding this comment

adpaco-aws Apr 11, 2022

Choose a reason for hiding this comment

celinval commented Apr 11, 2022 • edited Loading

jaisnan commented Apr 11, 2022

adpaco-aws left a comment

Choose a reason for hiding this comment

tedinski left a comment

Choose a reason for hiding this comment

jaisnan commented Apr 11, 2022 •

edited

Loading

jaisnan commented Apr 11, 2022 •

edited

Loading

jaisnan commented Apr 11, 2022 •

edited

Loading

celinval commented Apr 11, 2022 •

edited

Loading