Update rust toolchain version for Kani 0.17

[adpaco-aws]

Biweekly update for the rust toolchain version. For Kani 0.17, we will target the nightly-2022-12-04 version.

[adpaco-aws]

We decided to skip this update for version 0.17.0 because there are a couple of regressions in our tests. In particular, the two tests failing are:

    [kani] kani/AsyncAwait/main.rs
    [kani] kani/AsyncAwait/manual_spawn.rs

These two are failing for different reasons:

• kani/AsyncAwait/main.rs crashes with:

ERROR cprover_bindings::goto_program::expr Argument doesn't check, param=StructTag("tag-_13802158633106556629"), arg=Pointer { typ: StructTag("tag-_1054006636397192053") }
thread '<unnamed>' panicked at 'Function call does not type check:
func: Expr { value: Symbol { identifier: "_RNCNvNvCs1zWlokZfjXI_4main28test_async_proof_harness_pub28test_async_proof_harness_pub0B5_" }, typ: Code { parameters: [Parameter { typ: StructTag("tag-_14118333604554409965"), identifier: None, base_name: None }, Parameter { typ: StructTag("tag-_13802158633106556629"), identifier: None, base_name: None }], return_type: StructTag("tag-_11125111864767334529") }, location: None }
args: [Expr { value: Symbol { identifier: "_RINvNtCsfYPqN24XPPk_4kani7futures8block_onuNCNvNvCs1zWlokZfjXI_4main28test_async_proof_harness_pub28test_async_proof_harness_pub0EBL_::1::var_10" }, typ: StructTag("tag-_14118333604554409965"), location: None }, Expr { value: Symbol { identifier: "_RINvNtCsfYPqN24XPPk_4kani7futures8block_onuNCNvNvCs1zWlokZfjXI_4main28test_async_proof_harness_pub28test_async_proof_harness_pub0EBL_::1::var_12" }, typ: Pointer { typ: StructTag("tag-_1054006636397192053") }, location: None }]', cprover_bindings/src/goto_program/expr.rs:643:9
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
If you are seeing this message, please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md

[Kani] current codegen item: codegen_function: kani::block_on::<(), [async fn body@main.rs:26:45: 30:2]>
_RINvNtCsfYPqN24XPPk_4kani7futures8block_onuNCNvNvCs1zWlokZfjXI_4main28test_async_proof_harness_pub28test_async_proof_harness_pub0EBL_
[Kani] current codegen location: Loc { file: "/home/ubuntu/kani/library/kani/src/futures.rs", function: None, start_line: 18, start_col: Some(1), end_line: 18, end_col: Some(58) }
warning: 1 warning emitted

Error: /home/ubuntu/kani/target/kani/bin/kani-compiler exited with status exit status: 101

• kani/AsyncAwait/manual_spawn.rs fails verification because of a missing function:

SUMMARY:
 ** 1 of 404 failed (403 undetermined)
Failed Checks: Function `<manual_spawn::Scheduler>::run::<manual_spawn::RoundRobin>` with missing definition is unreachable

VERIFICATION:- FAILED

I don't know if these two problems are related. Will continue to debug this.

[adpaco-aws]

@fzaiser do you have any idea why this is happening?

[fzaiser]

@adpaco-aws No, I don't understand how this function could be missing given that it is defined in the same file as the proof harness.

[adpaco-aws]

Regarding the crash (file main.rs), I'm noticing significant differences in codegen between stable and nightly.

This can be misleading, because I'm not comparing with the previous nightly version (instead of stable), but in the line leading to the crash I'm getting:

        _6 = <impl Future<Output = i32> as Future>::poll(move _7, move _10) -> [return: bb7, unwind: bb22]; // scope 3 at src/main.rs:12:42: 12:48
                                         // mir::Constant
                                         // + span: src/main.rs:12:42: 12:48
                                         // + literal: Const { ty: for<'a, 'b, 'c> fn(Pin<&'a mut impl Future<Output = i32>>, &'b mut Context<'c>) -> Poll<<impl Future<Output = i32> as Future>::Output> {<impl Future<Output = i32> as Future>::poll}, val: Value(<ZST>) }

while in the nightly I get:

        _6 = <[async block@src/main.rs:12:30: 12:42] as Future>::poll(move _7, move _10) -> [return: bb6, unwind: bb20]; // scope 3 at src/main.rs:12:42: 12:48
                                         // mir::Constant
                                         // + span: src/main.rs:12:42: 12:48
                                         // + literal: Const { ty: for<'a, 'b, 'c> fn(Pin<&'a mut [async block@src/main.rs:12:30: 12:42]>, &'b mut Context<'c>) -> Poll<<[async block@src/main.rs:12:30: 12:42] as Future>::Output> {<[async block@src/main.rs:12:30: 12:42] as Future>::poll}, val: Value(<ZST>) }

I will come back to this later.

[adpaco-aws]

Maybe this commit is related, but it's hard to say at this point.

[zhassan-aws]

Won't fix as described above.