Allow panic with args to be called in a const context

[zhassan-aws]

Description of changes:

Calling panic! with args, e.g.

panic!("{}", msg)

is allowed by rustc in const contexts, but Kani compilation currently fails. This PR updates Kani's definition of the panic macro to allow this to go through.

Resolved issues:

Resolves #1586

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

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]

Can you please also add a test that panic during const evaluation?

[celinval]

Is this new line on purpose?

[zhassan-aws]

TBH, I have no idea how this new line came about. It's not clear how where those new lines are coming from.

[zhassan-aws]

Can you please also add a test that panic during const evaluation?

Sure.

[celinval]

Awesome!! I was wondering if the compiler will also prune the assert before codegen. 🤞

[zhassan-aws]

Awesome!! I was wondering if the compiler will also prune the assert before codegen. 🤞

Is there a way to examine the MIR that the codegen module receives?

[zhassan-aws]

Looks like it does get pruned, e.g.

$ cat test.rs 
#[kani::proof]
fn main() {
    let x: i32 = kani::any();
    let y = x / 2;
    assert!(y <= x, "This is a message");
}
$ RUSTFLAGS="--emit mir" kani test.rs

This is what main looks like in the output:

fn main() -> () {
    let mut _0: ();                      // return place in scope 0 at test.rs:2:11: 2:11
    let _1: i32;                         // in scope 0 at test.rs:3:9: 3:10
    let mut _3: i32;                     // in scope 0 at test.rs:4:13: 4:14
    let mut _4: bool;                    // in scope 0 at test.rs:4:13: 4:18
    let mut _5: bool;                    // in scope 0 at test.rs:4:13: 4:18
    let mut _6: bool;                    // in scope 0 at test.rs:4:13: 4:18
    let _7: ();                          // in scope 0 at /home/ubuntu/git/kani/library/std/src/lib.rs:44:9: 44:59
    let mut _8: bool;                    // in scope 0 at test.rs:5:13: 5:19
    let mut _9: i32;                     // in scope 0 at test.rs:5:13: 5:14
    let mut _10: i32;                    // in scope 0 at test.rs:5:18: 5:19
    scope 1 {
        debug x => _1;                   // in scope 1 at test.rs:3:9: 3:10
        let _2: i32;                     // in scope 1 at test.rs:4:9: 4:10
        scope 2 {
            debug y => _2;               // in scope 2 at test.rs:4:9: 4:10
        }
    }

    bb0: {
        _1 = kani::any::<i32>() -> bb1;  // scope 0 at test.rs:3:18: 3:29
                                         // mir::Constant
                                         // + span: test.rs:3:18: 3:27
                                         // + literal: Const { ty: fn() -> i32 {kani::any::<i32>}, val: Value(<ZST>) }
    }

    bb1: {
        _3 = _1;                         // scope 1 at test.rs:4:13: 4:14
        _4 = const false;                // scope 1 at test.rs:4:13: 4:18
        _5 = Eq(_3, const i32::MIN);     // scope 1 at test.rs:4:13: 4:18
        _6 = BitAnd(move _4, move _5);   // scope 1 at test.rs:4:13: 4:18
        assert(!move _6, "attempt to compute `{} / {}`, which would overflow", _3, const 2_i32) -> bb2; // scope 1 at test.rs:4:13: 4:18
    }

    bb2: {
        _2 = Div(move _3, const 2_i32);  // scope 1 at test.rs:4:13: 4:18
        _9 = _2;                         // scope 2 at test.rs:5:13: 5:14
        _10 = _1;                        // scope 2 at test.rs:5:18: 5:19
        _8 = Le(move _9, move _10);      // scope 2 at test.rs:5:13: 5:19
        _7 = kani::assert(move _8, const "\"This is a message\"") -> bb3; // scope 2 at /home/ubuntu/git/kani/library/std/src/lib.rs:44:9: 44:59
                                         // mir::Constant
                                         // + span: /home/ubuntu/git/kani/library/std/src/lib.rs:44:9: 44:21
                                         // + literal: Const { ty: fn(bool, &'static str) {kani::assert}, val: Value(<ZST>) }
                                         // mir::Constant
                                         // + span: /home/ubuntu/git/kani/library/std/src/lib.rs:44:29: 44:58
                                         // + literal: Const { ty: &str, val: Value(Slice(..)) }
    }

    bb3: {
        return;                          // scope 0 at test.rs:6:2: 6:2
    }
}