Upgrade tooclhain to 2024-02-17

[zhassan-aws]

Upgrade toolchain to 2024-02-17. Relevant PR:

rust-lang/rust#120500

Resolves #87

This currently breaks the std lib regression. Keeping it as a draft till we figure out a fix.

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

[zhassan-aws]

This program is sufficient to reproduce the crash in the std lib regression:

use std::sync;

#[cfg_attr(kani, kani::proof)]
fn main() {
    let lock = sync::RwLock::new(5);
    let c = lock.read();
    let i = c.unwrap_or_else(|_| lock.read().unwrap());
    assert!(*i == 5)
}

$ kani rwlock.rs 
Kani Rust Verifier 0.46.0 (standalone)
thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:689:9:
Function call does not type check:
func params: [Parameter { typ: StructTag("tag-_255281828603230393579431802309153866981"), identifier: Some("_RNCNvCsenOrSQPJUev_6rwlock4main0B3_::1::var_1"), base_name: Some("_RNCNvCsenOrSQPJUev_6rwlock4main0B3_::1::var_1") }]
args: [Expr { value: Symbol { identifier: "_RINvMNtCsiW2CYWmqB4c_4core6resultINtB3_6ResultINtNtNtCs4m6LCAw2AAX_3std4sync6rwlock15RwLockReadGuardlEINtNtBN_6poison11PoisonErrorBI_EE14unwrap_or_elseNCNvCsenOrSQPJUev_6rwlock4main0EB2t_::1::var_6" }, typ: StructTag("tag-_255281828603230393579431802309153866981"), location: None, size_of_annotation: None }, Expr { value: Member { lhs: Expr { value: Symbol { identifier: "_RINvMNtCsiW2CYWmqB4c_4core6resultINtB3_6ResultINtNtNtCs4m6LCAw2AAX_3std4sync6rwlock15RwLockReadGuardlEINtNtBN_6poison11PoisonErrorBI_EE14unwrap_or_elseNCNvCsenOrSQPJUev_6rwlock4main0EB2t_::1::var_7" }, typ: StructTag("tag-_146200748798307897826759305399112522164"), location: None, size_of_annotation: None }, field: "0" }, typ: StructTag("tag-_20659776347030360527720706964246510602"), location: None, size_of_annotation: None }]
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
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: std::result::Result::<std::sync::RwLockReadGuard<'_, i32>, std::sync::PoisonError<std::sync::RwLockReadGuard<'_, i32>>>::unwrap_or_else::<{[email protected]:7:30: 7:33}>
_RINvMNtCsiW2CYWmqB4c_4core6resultINtB3_6ResultINtNtNtCs4m6LCAw2AAX_3std4sync6rwlock15RwLockReadGuardlEINtNtBN_6poison11PoisonErrorBI_EE14unwrap_or_elseNCNvCsenOrSQPJUev_6rwlock4main0EB2t_
[Kani] current codegen location: Loc { file: "/home/ubuntu/.rustup/toolchains/nightly-2024-02-17-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs", function: None, start_line: 1427, start_col: Some(5), end_line: 1427, end_col: Some(63) }
error: /home/ubuntu/git/kani/target/kani/bin/kani-compiler exited with status exit status: 101

[tautschnig]

Can you elaborate as to how this fixes #87? Also, this PR should resolve #3028. Thanks!

[zhassan-aws]

Can you elaborate as to how this fixes #87?

The test associated with #87 no longer fails (neither the original nor the simplified one). I'm not sure what changed upstream that caused it be fixed TBH.

Also, this PR should resolve #3028.

Added. Thanks!

[zhassan-aws]

The likely culprit for the crash in the std lib regression is rust-lang/rust#100603.

[zhassan-aws]

A smaller program that produces the same crash:

use std::sync::PoisonError;

#[cfg_attr(kani, kani::proof)]
fn main() {
    let lr = std::sync::LockResult::<i32>::Ok(5);
    let my_clos = |_x: PoisonError<_>| 5;
    let _i = lr.unwrap_or_else(my_clos);
}

The MIR for this program is 95 lines long (vs. 50K for the above one), so should be easier to debug.

[zhassan-aws]

Here's a program that doesn't use sync and reproduces the crash even without the toolchain update (i.e. with 6bea131):

#![feature(never_type)]

pub struct Foo {
    _x: i32,
    _never: !,
}

#[cfg_attr(kani, kani::proof)]
fn main() {
    let res = Result::<i32, Foo>::Ok(3);
    let _x = res.unwrap_or_else(|_f| 5);
}

Kani Rust Verifier 0.46.0 (standalone)
thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:689:9:
Function call does not type check:
func params: []
args: [Expr { value: Member { lhs: Expr { value: Symbol { identifier: "_RINvMNtCs4A47zemGJJh_4core6resultINtB3_6ResultlNtCslwEuWiA9yWG_2nv3FooE14unwrap_or_elseNCNvBL_4main0EBL_::1::var_7" }, typ: StructTag("tag-_133682644016529668577290331323904023019"), location: None, size_of_annotation: None }, field: "0" }, typ: StructTag("tag-_247671360278137032517711891165892296272"), location: None, size_of_annotation: None }]
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Kani unexpectedly panicked during compilation.
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: std::result::Result::<i32, Foo>::unwrap_or_else::<{[email protected]:11:33: 11:37}>
_RINvMNtCs4A47zemGJJh_4core6resultINtB3_6ResultlNtCslwEuWiA9yWG_2nv3FooE14unwrap_or_elseNCNvBL_4main0EBL_
[Kani] current codegen location: Loc { file: "/home/ubuntu/.rustup/toolchains/nightly-2024-02-09-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/result.rs", function: None, start_line: 1423, start_col: Some(5), end_line: 1423, end_col: Some(63) }
error: /home/ubuntu/git/kani/target/kani/bin/kani-compiler exited with status exit status: 101

[zhassan-aws]

I filed the crash as #3034.

This is a blocker for the toolchain upgrade.

[zhassan-aws]

Until we figure out a fix for #3034, I've opened a separate PR (#3036) to advance the toolchain to 2024-02-14 so that it doesn't include the breaking change that is included in the following toolchain version. Once we merge #3036, I'll rebase this PR.

[celinval]

I ended up creating a new PR with the fix: #3040