search

model-checking / kani

Kani Rust Verifier
https://model-checking.github.io/kani
Apache License 2.0
2.11k stars 83 forks source link

Toolchain upgrade to nightly-2024-04-22 failed #3161

Closed github-actions[bot] closed 3 months ago

github-actions[bot] commented 4 months ago

Updating Rust toolchain from nightly-2024-04-21 to nightly-2024-04-22 requires source changes. The failed automated run can be found here. Please review the changes at https://github.com/rust-lang/rust from https://github.com/rust-lang/rust/commit/dbce3b43b6cb34dd3ba12c3ec6f708fe68e9c3df up to https://github.com/rust-lang/rust/commit/fb898629a26e4acec59c928ce3ec00a62675d1cc. The log for this commit range is: https://github.com/rust-lang/rust/commit/fb898629a2 Auto merge of #124241 - matthiaskrgr:rollup-xhu90xr, r=matthiaskrgr https://github.com/rust-lang/rust/commit/3315bf961d Rollup merge of #124235 - c410-f3r:tests98765, r=jieyouxu https://github.com/rust-lang/rust/commit/f277f3d653 Rollup merge of #124231 - BoxyUwU:dereview, r=Mark-Simulacrum https://github.com/rust-lang/rust/commit/e96ed6d35d Rollup merge of #124229 - mati865:add-gnullvm-targets-to-manifest, r=Mark-Simulacrum https://github.com/rust-lang/rust/commit/cd92422180 Rollup merge of #124224 - bvanjoi:cleanup, r=fmease https://github.com/rust-lang/rust/commit/67872e740e Rollup merge of #123840 - scottmcm:aggregate-kind-rawptr, r=cjgillot https://github.com/rust-lang/rust/commit/1b3fba066c Auto merge of #124203 - lukas-code:delete-deleting-caches, r=compiler-errors https://github.com/rust-lang/rust/commit/3aaa3941fd Move some tests https://github.com/rust-lang/rust/commit/5e785b1420 Update tests after 123949 https://github.com/rust-lang/rust/commit/1398fe7a5e Address more PR feedback https://github.com/rust-lang/rust/commit/bb8d6f790b Address PR feedback https://github.com/rust-lang/rust/commit/5e1d16ca55 Also handle AggregateKind::RawPtr in cg_cranelift https://github.com/rust-lang/rust/commit/9520cebfc5 InstSimplify from_raw_parts(p, ()) → p as _ https://github.com/rust-lang/rust/commit/de64ff76f8 Use it in the library, and InstSimplify it away in the easy places https://github.com/rust-lang/rust/commit/4f4442655e Add an intrinsic that lowers to AggregateKind::RawPtr https://github.com/rust-lang/rust/commit/e6b2b764ec Add AggregateKind::RawPtr and enough support to compile https://github.com/rust-lang/rust/commit/70df9d9a13 Add a mir-opt test for byte_add on pointers https://github.com/rust-lang/rust/commit/b76faff1b2 Add a MIR pre-codegen test for Vec::deref https://github.com/rust-lang/rust/commit/5800dc1faa New slice indexing pre-codegen MIR test https://github.com/rust-lang/rust/commit/e1d12ffb6c removal https://github.com/rust-lang/rust/commit/f22a0c2d9f Auto merge of #123594 - Urgau:fix-non_local_def-lint-overflow, r=lcnr https://github.com/rust-lang/rust/commit/5a2b335e49 also remap RPITITs nested in other types back to their opaques https://github.com/rust-lang/rust/commit/6ae761cd40 Add gnullvm targets to manifest https://github.com/rust-lang/rust/commit/aa31bad26b Auto merge of #124222 - GuillaumeGomez:rollup-ws1zju7, r=GuillaumeGomez https://github.com/rust-lang/rust/commit/2d5a226f8f cleanup: unnecessary clone during lower generics args https://github.com/rust-lang/rust/commit/43d5e00bac Rollup merge of #124198 - compiler-errors:improve-ty-ct-param-span, r=Nadrieril https://github.com/rust-lang/rust/commit/24b8c54f6d Rollup merge of #124184 - gurry:124152-suggest-unsigned-abs-in-abs-doc, r=jhpratt https://github.com/rust-lang/rust/commit/9efd1477ac Rollup merge of #124089 - simlay:fix-preadv64-and-pwritev64-link-for-watchos-and-visionos, r=workingjubilee https://github.com/rust-lang/rust/commit/f122a5129c Rollup merge of #124069 - onur-ozkan:run-clippy-on-bootstrap, r=albertlarsan68 https://github.com/rust-lang/rust/commit/fecb7b4309 Auto merge of #124193 - RalfJung:miri, r=RalfJung https://github.com/rust-lang/rust/commit/ae37b6ec58 the mir-validation ICE test behaves strangely on Windows hosts https://github.com/rust-lang/rust/commit/b9be3c47e5 Auto merge of #117457 - daxpedda:wasm-nontrapping-fptoint, r=wesleywiser https://github.com/rust-lang/rust/commit/fa53b9f39c Fix watchOS and visionOS for pread64 and pwrite64 calls https://github.com/rust-lang/rust/commit/13eb8c736c Auto merge of #123930 - Mark-Simulacrum:vec-length-invariant, r=jhpratt https://github.com/rust-lang/rust/commit/f1ae5314be Avoid reloading Vec::len across grow_one in push https://github.com/rust-lang/rust/commit/426a698606 Auto merge of #123981 - Kobzol:update-nodejs, r=Mark-Simulacrum https://github.com/rust-lang/rust/commit/453ceafce3 Auto merge of #124208 - jieyouxu:rollup-gbgpu4u, r=jieyouxu https://github.com/rust-lang/rust/commit/c72cfdd46f Rollup merge of #124196 - RalfJung:mir-opt-tests, r=Mark-Simulacrum https://github.com/rust-lang/rust/commit/b3f9117a2d Rollup merge of #124191 - dtolnay:fixup, r=compiler-errors https://github.com/rust-lang/rust/commit/726361caf4 Rollup merge of #124132 - RalfJung:OpBundlesIndirect, r=Mark-Simulacrum https://github.com/rust-lang/rust/commit/418a07861a Rollup merge of #124103 - dtolnay:metadatadebug, r=Mark-Simulacrum https://github.com/rust-lang/rust/commit/29ee276368 Rollup merge of #124071 - kjetilkjeka:llvm_bitcode_linker_build_manifest, r=Mark-Simulacrum https://github.com/rust-lang/rust/commit/f13cd0c8d0 Rollup merge of #124053 - Zalathar:lazy-boolean, r=Mark-Simulacrum https://github.com/rust-lang/rust/commit/871c3e3075 Rollup merge of #123986 - ehuss:lint-renamed, r=Mark-Simulacrum https://github.com/rust-lang/rust/commit/a73aabfa92 Rollup merge of #123976 - ChrisDenton:no-libc-in-std-doc-tests, r=Mark-Simulacrum https://github.com/rust-lang/rust/commit/ccd9880769 Rollup merge of #123967 - RalfJung:static_mut_refs, r=Nilstrieb https://github.com/rust-lang/rust/commit/e9e936cfa8 Rollup merge of #123379 - wutchzone:119266, r=compiler-errors https://github.com/rust-lang/rust/commit/31a05a227a merge two impl blocks https://github.com/rust-lang/rust/commit/57085a06d9 Explicitly mention Self https://github.com/rust-lang/rust/commit/f9ba863c4d remove InferCtxt::clear_caches https://github.com/rust-lang/rust/commit/88b10c1162 include ParamEnv in projection cache key https://github.com/rust-lang/rust/commit/fa0428c9d0 Flip spans for precise capturing syntax not capturing a ty/ct param https://github.com/rust-lang/rust/commit/be564a8add Print note with closure signature on type mismatch https://github.com/rust-lang/rust/commit/75d0fdd967 mir-opt tests: rename unit-test -> test-mir-pass https://github.com/rust-lang/rust/commit/61a7d3d523 ensure the ICE-to-file logic does not affect our test https://github.com/rust-lang/rust/commit/6b0ce8b1e2 Auto merge of #3495 - RalfJung:data-race-clocks, r=RalfJung https://github.com/rust-lang/rust/commit/8cab0d5617 restrict VClock API surface https://github.com/rust-lang/rust/commit/cb1b4a6977 reuse_pool: only do acquire_clock if we reused from a different thread https://github.com/rust-lang/rust/commit/7dcfb54dc6 data_race: make the release/acquire API more clear https://github.com/rust-lang/rust/commit/debdb72ba8 Give a name to each distinct manipulation of pretty-printer FixupContext https://github.com/rust-lang/rust/commit/912c67043b Move pretty-printer FixupContext to a module https://github.com/rust-lang/rust/commit/9713ff45ab Auto merge of #3494 - rust-lang:rustup-2024-04-20, r=RalfJung https://github.com/rust-lang/rust/commit/7952316aff re-bless tests https://github.com/rust-lang/rust/commit/8e1f18dce8 fix clippy warning https://github.com/rust-lang/rust/commit/b63bb1b374 Merge from rustc https://github.com/rust-lang/rust/commit/29e41fbc30 Preparing for merge from rustc https://github.com/rust-lang/rust/commit/02ac46c0c2 Suggest using unsigned_abs in abs documentation https://github.com/rust-lang/rust/commit/e9ebc6f800 Auto merge of #3475 - RalfJung:reduce-reuse-recycle, r=RalfJung https://github.com/rust-lang/rust/commit/c5fdb39120 fix clippy warnings on bootstrap https://github.com/rust-lang/rust/commit/95ae2dd7ff Auto merge of #3489 - rust-lang:rustup-2024-04-19, r=RalfJung https://github.com/rust-lang/rust/commit/fecd7fc937 make test not leak rustc crate hash https://github.com/rust-lang/rust/commit/134ee309c9 Auto merge of #3490 - RalfJung:paths, r=RalfJung https://github.com/rust-lang/rust/commit/b9ed4cd70a share code between win-to-unix and unix-to-win path conversion https://github.com/rust-lang/rust/commit/d0783e8836 Merge from rustc https://github.com/rust-lang/rust/commit/c1cf0a3e38 Preparing for merge from rustc https://github.com/rust-lang/rust/commit/9b419a1b83 when reusing an address, most of the time only reuse from the current thread https://github.com/rust-lang/rust/commit/39f0c4f884 Auto merge of #3488 - RalfJung:os_str_comment, r=RalfJung https://github.com/rust-lang/rust/commit/5067dd21b6 comment clarification and typo fix https://github.com/rust-lang/rust/commit/61def018c1 llvm RustWrapper: explain OpBundlesIndirect argument type https://github.com/rust-lang/rust/commit/d7916fc8cd do not reuse stack addresses; make reuse rate configurable https://github.com/rust-lang/rust/commit/6a52feeac6 Stabilize Wasm phase 4 & 5 proposals https://github.com/rust-lang/rust/commit/48fd549cd3 when an address gets reused, establish a happens-before link in the data race model https://github.com/rust-lang/rust/commit/1ce64e717f Auto merge of #3484 - RalfJung:realloc, r=RalfJung https://github.com/rust-lang/rust/commit/5ff9b2b865 move allocator shim logic into its own file https://github.com/rust-lang/rust/commit/73e333ac44 make realloc with a size of zero fail https://github.com/rust-lang/rust/commit/5c9924a599 Auto merge of #3486 - RalfJung:mir-validate, r=RalfJung https://github.com/rust-lang/rust/commit/5ef38aca35 add test checking that we do run MIR validation https://github.com/rust-lang/rust/commit/5697f731b4 Auto merge of #3485 - RalfJung:read_byte_slice, r=RalfJung https://github.com/rust-lang/rust/commit/a920ed4136 CI: add script for installing NodeJS and update it to v20 https://github.com/rust-lang/rust/commit/62e84d5ca0 move read_byte_slice to general helpers file, next to read_c_str https://github.com/rust-lang/rust/commit/0f44382bca Auto merge of #3483 - RalfJung:drop, r=RalfJung https://github.com/rust-lang/rust/commit/5c352a4e75 add test for Drop terminator on non-drop type https://github.com/rust-lang/rust/commit/fdf93bbde0 Improve std::fs::Metadata Debug representation https://github.com/rust-lang/rust/commit/d261b53081 Auto merge of #3481 - RalfJung:rustup, r=RalfJung https://github.com/rust-lang/rust/commit/7c3c2716ff fmt https://github.com/rust-lang/rust/commit/3d3550ffa0 Merge from rustc https://github.com/rust-lang/rust/commit/6a108a7477 Preparing for merge from rustc https://github.com/rust-lang/rust/commit/4734163006 Add llvm-bitcode-linker to build manifest https://github.com/rust-lang/rust/commit/214bf5a017 enable clippy for bootstrap on CI PRs https://github.com/rust-lang/rust/commit/9776f647e6 Auto merge of #3480 - RalfJung:alloc_error_handler, r=RalfJung https://github.com/rust-lang/rust/commit/14701efcaf Auto merge of #3479 - rust-lang:rustup-2024-04-17, r=RalfJung https://github.com/rust-lang/rust/commit/9f156d38a5 no need to use miri's native stderr here https://github.com/rust-lang/rust/commit/d7f79cc2b2 tests/utils: add fmt::Write implementations for miri's native stdout/stderr https://github.com/rust-lang/rust/commit/d10f61313f alloc_error_handler tests: directly call handle_alloc_error; test more codepaths https://github.com/rust-lang/rust/commit/2cb03ef739 fmt https://github.com/rust-lang/rust/commit/e8739886f2 Merge from rustc https://github.com/rust-lang/rust/commit/af28716f19 Preparing for merge from rustc https://github.com/rust-lang/rust/commit/25b9f84413 coverage: Branch coverage tests for lazy boolean operators https://github.com/rust-lang/rust/commit/40cfc2de77 coverage: Move branch coverage tests into a subdirectory https://github.com/rust-lang/rust/commit/8ad72b24f3 Auto merge of #3478 - RalfJung:alloc_error_handler, r=RalfJung https://github.com/rust-lang/rust/commit/f325c8d4fa implement support for __rust_alloc_error_handler https://github.com/rust-lang/rust/commit/719799028a Auto merge of #3477 - RalfJung:win-no-std, r=RalfJung https://github.com/rust-lang/rust/commit/a7db62810e no_std works on Windows now https://github.com/rust-lang/rust/commit/fee494b2b2 Auto merge of #3472 - RalfJung:deadlock, r=RalfJung https://github.com/rust-lang/rust/commit/811d4de5a0 deadlock: show backtrace for all threads https://github.com/rust-lang/rust/commit/1129faca2b Auto merge of #3471 - RalfJung:blocked, r=RalfJung https://github.com/rust-lang/rust/commit/3d5acebbf1 threads: keep track of why we are blocked, and sanity-check that when waking up https://github.com/rust-lang/rust/commit/88d1a1c6fd Auto merge of #3469 - rust-lang:rustup-2024-04-16, r=RalfJung https://github.com/rust-lang/rust/commit/3d3a584e4d bless test-cargo-miri https://github.com/rust-lang/rust/commit/a1f523dd2c Merge from rustc https://github.com/rust-lang/rust/commit/20f418252f Preparing for merge from rustc https://github.com/rust-lang/rust/commit/232eb59a8f lint-docs: Add redirects for renamed lints. https://github.com/rust-lang/rust/commit/89117f85e3 Use fake libc in core test https://github.com/rust-lang/rust/commit/b4a4645758 static_mut_refs: use raw pointers to remove the remaining FIXME https://github.com/rust-lang/rust/commit/c2e2245fd8 Fix trait solver overflow with non_local_definitions lint

tautschnig commented 4 months ago

https://github.com/rust-lang/rust/commit/5e1d16ca55 might give some guidance on what we'll need to implement.

adpaco-aws commented 4 months ago

Thanks, @tautschnig ! Note that they have added more code in the current implementation.

Despite these examples, it's not totally clear to me what needs to be done to properly handle the AggregateKind::RawPtr case. The only thing I know is that we get two operands (known as data and meta). I'm using the test in tests/kani/Whitespace/main.rs as my preliminary test:

fn main() {
    let mut iter = "A few words".split_whitespace();
    match iter.next() {
        None => assert!(false),
        Some(x) => assert!(x == "A"),
    }
}

I'm surely going to switch to a simpler test case soon (i.e., one that only uses from_raw_parts directly, which is the intrinsic that generates this aggregate type), but using the same code we use for non-enum AggregateKind::Adt(..) / AggregateKind::Tuple doesn't typecheck for me:

thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:851:9:
Error in struct_expr; value type does not match field type.
        StructTag("tag-_133079824658713581498706231541463642518")
        [Field { name: "data", typ: Pointer { typ: Unsignedbv { width: 8 } } }, Field { name: "len", typ: CInteger(SizeT) }]
        [Expr { value: Symbol { identifier: "_ZN4core3ptr8metadata14from_raw_parts17haf035031626b0269E::1::var_1::data_pointer" }, typ: Pointer { typ: StructTag("tag-Unit") }, location: None, size_of_annotation: None }, Expr { value: Symbol { identifier: "_ZN4core3ptr8metadata14from_raw_parts17haf035031626b0269E::1::var_2::metadata" }, typ: CInteger(SizeT), location: None, size_of_annotation: None }]
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Also, casting data doesn't typecheck for me neither. What's weird about this particular test is that the Expr that we generate for data has type Pointer { typ: StructTag("tag-Unit") }. The code from the cranelift backend checks if meta is a ZST, but it doesn't do it for data.

As I said, I'll switch to a simpler example to see if these typechecking problems persist.

adpaco-aws commented 4 months ago

I've switched to a simpler example inspired by another test in our repo:

#[kani::proof]
fn main() {
    let mut v: Vec<u8> = vec![65, 122];
    // Build a `String` using the contents of `v`
    let s = unsafe { String::from_raw_parts(v.as_mut_ptr(), v.len(), v.capacity()) };
    assert_eq!(s, "Az");
}

I've also restored the code I came up with first (ignoring meta completely for now):

            AggregateKind::RawPtr(inner_ty, _) => {
                // We expect two operands: "data" and "meta"
                assert!(operands.len() == 2);
                let typ = self.codegen_ty_stable(res_ty);
                let layout = self.layout_of_stable(res_ty);
                assert!(layout.ty.is_unsafe_ptr());
                let data = self.codegen_operand_stable(&operands[0]);
                data.cast_to(typ)
            }

Unfortunately, that brings me to this "can't cast" problem:

thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:522:13:
Can't cast

Expr { value: Symbol { identifier: "_ZN4core3ptr8metadata14from_raw_parts17haf035031626b0269E::1::var_1::data_pointer" }, typ: Pointer { typ: StructTag("tag-Unit") }, location: None, size_of_annotation: None } (Pointer { typ: StructTag("tag-Unit") })

StructTag("tag-_133079824658713581498706231541463642518")
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Looking at the debug logs, it appears that StructTag("tag-_133079824658713581498706231541463642518") represents a * const [u8]:

2024-05-03T20:57:58.435033Z DEBUG kani_compiler::codegen_cprover_gotoc::codegen::typ: codegen_ty: new type mir_type=*const [u8] gotoc_name="tag-_133079824658713581498706231541463642518" goto_typ=StructTag("tag-_133079824658713581498706231541463642518")

I don't know though why the expression corresponding to data is being codegen'd with type Pointer { typ: StructTag("tag-Unit"). In the debug output below, the ArgAbi for the first argument is kind: RigidTy(RawPtr(Ty { id: 7, kind: RigidTy(Uint(U8)) }, which I'm surprised to have translated like this. This might be an indication that the code to codegen this specific type needs updating, but I haven't been able to find the issue there.

2024-05-03T20:57:58.440991Z DEBUG kani_compiler::codegen_cprover_gotoc::codegen::function: declaring std::slice::from_raw_parts::<'_, u8>; Instance { kind: Item, def: "_ZN4core5slice3raw14from_raw_parts17hbaaf7ce76150d32dE", args: GenericArgs([Lifetime(Region { kind: ReErased }), Type(Ty { id: 7, kind: RigidTy(Uint(U8)) }), Const(Const { kind: Allocated(Allocation { bytes: [Some(1)], provenance: ProvenanceMap { ptrs: [] }, align: 1, mutability: Mut }), ty: Ty { id: 24, kind: RigidTy(Bool) }, id: ConstId(13) })]) }
2024-05-03T20:57:58.441099Z DEBUG kani_compiler::codegen_cprover_gotoc::codegen::function: declare_function krate=Crate { id: 3, name: "core", is_local: false } is_std=true
2024-05-03T20:57:58.441184Z DEBUG kani_compiler::codegen_cprover_gotoc::codegen::typ: fn_typ i=0 arg_abi=ArgAbi { ty: Ty { id: 49, kind: RigidTy(RawPtr(Ty { id: 7, kind: RigidTy(Uint(U8)) }, Not)) }, layout: Layout(1), mode: Direct(ArgAttributes { regular: NoUndef, arg_ext: None, pointee_size: Size(0 bytes), pointee_align: None }) }
2024-05-03T20:57:58.441253Z DEBUG kani_compiler::codegen_cprover_gotoc::codegen::typ: fn_typ i=1 arg_abi=ArgAbi { ty: Ty { id: 18, kind: RigidTy(Uint(Usize)) }, layout: Layout(2), mode: Direct(ArgAttributes { regular: NoUndef, arg_ext: None, pointee_size: Size(0 bytes), pointee_align: None }) }
2024-05-03T20:57:58.441293Z DEBUG kani_compiler::codegen_cprover_gotoc::codegen::typ: function_type params=[Parameter { typ: Pointer { typ: Unsignedbv { width: 8 } }, identifier: Some("_ZN4core5slice3raw14from_raw_parts17hbaaf7ce76150d32dE::1::var_1::data"), base_name: Some("_ZN4core5slice3raw14from_raw_parts17hbaaf7ce76150d32dE::1::var_1::data") }, Parameter { typ: CInteger(SizeT), identifier: Some("_ZN4core5slice3raw14from_raw_parts17hbaaf7ce76150d32dE::1::var_2::len"), base_name: Some("_ZN4core5slice3raw14from_raw_parts17hbaaf7ce76150d32dE::1::var_2::len") }] fn_abi=FnAbi { args: [ArgAbi { ty: Ty { id: 49, kind: RigidTy(RawPtr(Ty { id: 7, kind: RigidTy(Uint(U8)) }, Not)) }, layout: Layout(1), mode: Direct(ArgAttributes { regular: NoUndef, arg_ext: None, pointee_size: Size(0 bytes), pointee_align: None }) }, ArgAbi { ty: Ty { id: 18, kind: RigidTy(Uint(Usize)) }, layout: Layout(2), mode: Direct(ArgAttributes { regular: NoUndef, arg_ext: None, pointee_size: Size(0 bytes), pointee_align: None }) }], ret: ArgAbi { ty: Ty { id: 36, kind: RigidTy(Ref(Region { kind: ReErased }, Ty { id: 27, kind: RigidTy(Slice(Ty { id: 7, kind: RigidTy(Uint(U8)) })) }, Not)) }, layout: Layout(9), mode: Pair(ArgAttributes { regular: NonNull | NoUndef, arg_ext: None, pointee_size: Size(0 bytes), pointee_align: Some(Align(1 bytes)) }, ArgAttributes { regular: NoUndef, arg_ext: None, pointee_size: Size(0 bytes), pointee_align: None }) }, fixed_count: 2, conv: Rust, c_variadic: false }
zhassan-aws commented 4 months ago

Can you try replacing cast_to with codegen_fat_ptr_to_thin_ptr_cast?

zhassan-aws commented 4 months ago

This is a simpler test:

#[kani::proof]
fn main() {
    let a = [1, 2];
    let p = std::ptr::slice_from_raw_parts(a.as_ptr(), a.len());
}
zhassan-aws commented 4 months ago

@adpaco-aws the changes in #3171 address the tests listed above. However, some regressions are still failing.

tautschnig commented 3 months ago

@adpaco-aws the changes in #3171 address the tests listed above. However, some regressions are still failing.

The Rust regressions seem ok now, but benchcomp is falling over (in Python).