Allow &bool in asserts

[zhassan-aws]

Description of changes:

From investigating #2108, it turns out that due to how the standard library expands assert!(x) as

    if !x {
        ::core::panicking::panic("assertion failed: x")
    };

the following is valid Rust code:

fn main() {
    let b: bool = true;
    assert!(&b);
}

because it gets expanded to:

fn main() {
    let b: bool = true;
    if !&b {
        ::core::panicking::panic("assertion failed: &b")
    }
}

which, however, is rejected by Kani because &b is not a boolean (only !&b is!).

This PR adds a hacky fix, which is to inject !! (i.e. double negation) before the condition.

Resolved issues:

Resolves #2108

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

TBH, I'm not sure about whether this should be merged as it is quite hacky. We should look into where this occurs, and why it is valid.

Testing:

• How is this change tested? Added a new test

• 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.

[celinval]

Did you try defining kani::assert() using AsRef<bool> instead?

[celinval]

Did you try defining kani::assert() using AsRef<bool> instead?

Actually, I don't think that will work. :(

[tedinski]

Seems fine, can we change the PR name to something slightly more customer-facing in advance of merging? "Accept &bool in asserts, like Rust's assert macro does" perhaps

[zhassan-aws]

can we change the PR name to something slightly more customer-facing in advance of merging?

Done.